silly identity stuff

silly_id.lean

open function

variables {α β : Type}
def inverse (g : β → α) (f : α → β) := left_inverse g f ∧ right_inverse g f
def inverse_comp (f : α → β) (g : β → α) (gf_inv : inverse g f)
  : (∀ a, (g ∘ f) a = a) ∧ (∀ b, (f ∘ g) b = b) :=
    ⟨gf_inv.left, gf_inv.right⟩

  def inverse_comp_id {f : α → β} {g : β → α} (gf_inv  : inverse g f)
  : (g ∘ f = id) ∧ (f ∘ g = id)
  := ⟨funext (λ a, by rw [(inverse_comp f g gf_inv).left, id]),
      funext (λ b, by rw [(inverse_comp f g gf_inv).right, id])⟩
      
  /- A dumb example, if inverse (f ∘ g) (f ∘ g) 
     and (f ∘ g) = id,
     and id = (g ∘ f) 
     why not transitively, inverse (f ∘ g) (g ∘ f)
  -/
  def inverse_comp_inv {α : Type*} {β : Type*}
  : ∀ (f : α → β) (g : β → α), inverse f g → inverse (f ∘ g) (f ∘ g)
  := (λ f g, λ inv,
      /- because the types differ, -/
      have comp_fg : β → β, from f ∘ g,
      have comp_gf : α → α, from g ∘ f,
      -- where as for id we have something like:
      have id' : ∀(z : Type), z → z, from @id,
      have fog_eq_id : (f ∘ g = id), from (inverse_comp_id inv).left,
      have gof_eq_id : (id = g ∘ f), from eq.symm ((inverse_comp_id inv).right),
      -- So this eq.trans isn't going to type check, even though we have proofs of the necessary arguments.      
      -- have fog_eq_gof : (f ∘ g) = g ∘ f, from eq.trans fog_eq_id gof_eq_id,
      have fog_comp_id : ∀ x, (f ∘ g)((f ∘ g) x) = x,
        from (λ x, calc (f ∘ g) ((f ∘ g) x) = (id (id x)) : by rw (inverse_comp_id inv).left
                          ... = id x : by refl
                          ... = x : by refl),
      and.intro fog_comp_id fog_comp_id)