Proposed statement of the five lemma

five_lemma_statement.lean

import tactic
import tactic.find
import init.function
import algebra.group
import group_theory.subgroup

open function

section five_lemma

universes u

variables {A B : Type u} [group A] [group B]
definition ker (f : A  → B) [is_group_hom f] := is_group_hom.ker f
definition im (f : A → B) [is_group_hom f] :=  f '' (@set.univ A)


variables {A₁ B₁ C₁ D₁ E₁ : Type u}
variables {A₂ B₂ C₂ D₂ E₂ : Type u}

variables  [group A₁]    {f₁ : A₁ → B₁}   [group B₁]    {g₁ : B₁ → C₁}   [group C₁]    {h₁ : C₁ → D₁}   [group D₁]    {i₁ : D₁ → E₁}   [group E₁]
variables {j : A₁ → A₂}                  {k : B₁ → B₂}                  {l : C₁ → C₂}                  {m : D₁ → D₂}                  {n : E₁ → E₂}
variables  [group A₂]    {f₂ : A₂ → B₂}   [group B₂]    {g₂ : B₂ → C₂}   [group C₂]    {h₂ : C₂ → D₂}   [group D₂]    {i₂ : D₂ → E₂}   [group E₂]

variables [is_group_hom f₁] [is_group_hom g₁] [is_group_hom h₁] [is_group_hom i₁]
variables [is_group_hom f₂] [is_group_hom g₂] [is_group_hom h₂] [is_group_hom i₂]
variables [is_group_hom j] [is_group_hom k] [is_group_hom l] [is_group_hom m] [is_group_hom n]


lemma five_lemma
(com₁ : k ∘ f₁ = f₂ ∘ j)
(com₂ : l ∘ g₁ = g₂ ∘ k)
(com₃ : m ∘ h₁ = h₂ ∘ l)
(com₄ : n ∘ i₁ = i₂ ∘ m)
(eB₁ : im f₁ = ker g₁)
(eC₁ : im g₁ = ker h₁)
(eD₁ : im h₁ = ker i₁)
(eB₂ : im f₂ = ker g₂)
(eC₂ : im g₂ = ker h₂)
(eD₂ : im h₂ = ker i₂)
(hj : surjective j)
(hk : bijective k)
(hm : bijective m)
(hn : injective n)
: bijective l :=
begin
 have := is_group_hom.one f₁,
 have := is_group_hom.one g₁,
 have := is_group_hom.one h₁,
 have := is_group_hom.one i₁,
 have := is_group_hom.one f₂,
 have := is_group_hom.one g₂,
 have := is_group_hom.one h₂,
 have := is_group_hom.one i₂,
 have := is_group_hom.one j,
 have := is_group_hom.one k,
 have := is_group_hom.one l,
 have := is_group_hom.one m,
 have := is_group_hom.one n,
 split, {
  apply is_group_hom.inj_of_trivial_ker l,
  apply set.ext, intro x,
  split, { -- x ∈ ker n → x = 1
   intro hx,
   rw is_group_hom.mem_ker at hx,
   simp,
   have : (h₂ ∘ l) x = 1, unfold comp, cc,
   have : (m ∘ h₁) x = 1, cc,
   have : m (h₁ x) = 1, apply_assumption,
   have : h₁ x = 1,
   have y : g₁ 
  }, { -- x = 1 → x ∈ ker
   intro hx,
   simp at hx,
   rw is_group_hom.mem_ker,
   have := is_group_hom.one l,
   cc
  }
 }, {
 }
end

end five_lemma

Just trying to follow the flow of logic, I refactored the central part and renamed variables:

variables {A₁ B₁ C₁ D₁ E₁ : Type u}
variables {A₂ B₂ C₂ D₂ E₂ : Type u}
variables [group A₁] [group B₁] [group C₁] [group D₁] [group E₁]
variables [group A₂] [group B₂] [group C₂] [group D₂] [group E₂]
variables {b₁a₁ : A₁ → B₁} {c₁b₁ : B₁ → C₁} {d₁c₁ : C₁ → D₁} {e₁d₁ : D₁ → E₁}
variables {b₂a₂ : A₂ → B₂} {c₂b₂ : B₂ → C₂} {d₂c₂ : C₂ → D₂} {e₂d₂ : D₂ → E₂}
variables {a₂a₁ : A₁ → A₂} {b₂b₁ : B₁ → B₂} {c₂c₁ : C₁ → C₂} {d₂d₁ : D₁ → D₂} {e₂e₁ : E₁ → E₂}
variables [is_group_hom b₁a₁] [is_group_hom c₁b₁] [is_group_hom d₁c₁] [is_group_hom e₁d₁]
variables [is_group_hom b₂a₂] [is_group_hom c₂b₂] [is_group_hom d₂c₂] [is_group_hom e₂d₂]
variables [is_group_hom a₂a₁] [is_group_hom b₂b₁] [is_group_hom c₂c₁] [is_group_hom d₂d₁] [is_group_hom e₂e₁]

definition ker (f : A → B) [is_group_hom f] := is_group_hom.ker f
definition im (f : A → B) [is_group_hom f] :=  f '' (@set.univ A)

lemma five_lemma
(com_b₂a₁ : b₂b₁ ∘ b₁a₁ = b₂a₂ ∘ a₂a₁)
(com_c₂b₁ : c₂c₁ ∘ c₁b₁ = c₂b₂ ∘ b₂b₁)
(com_d₂c₁ : d₂d₁ ∘ d₁c₁ = d₂c₂ ∘ c₂c₁)
(com_e₂d₁ : e₂e₁ ∘ e₁d₁ = e₂d₂ ∘ d₂d₁)
(eb₁ : im b₁a₁ = ker c₁b₁)
(ec₁ : im c₁b₁ = ker d₁c₁)
(ed₁ : im d₁c₁ = ker e₁d₁)
(eb₂ : im b₂a₂ = ker c₂b₂)
(ec₂ : im c₂b₂ = ker d₂c₂)
(ed₂ : im d₂c₂ = ker e₂d₂)
(ha₂a₁ : function.surjective a₂a₁)
(hb₂b₁ : function.bijective b₂b₁)
(hd₂d₁ : function.bijective d₂d₁)
(he₂e₁ : function.injective e₂e₁)
: function.bijective c₂c₁ := sorry

How about this layout:

variables {A₁ B₁ C₁ D₁ E₁ : Type u}
variables {A₂ B₂ C₂ D₂ E₂ : Type u}

variables    [group A₁]    {b₁a₁ : A₁ → B₁}    [group B₁]    {c₁b₁ : B₁ → C₁}    [group C₁]    {d₁c₁ : C₁ → D₁}    [group D₁]    {e₁d₁ : D₁ → E₁}    [group E₁]
variables {a₂a₁ : A₁ → A₂}                  {b₂b₁ : B₁ → B₂}                  {c₂c₁ : C₁ → C₂}                  {d₂d₁ : D₁ → D₂}                  {e₂e₁ : E₁ → E₂}
variables    [group A₂]    {b₂a₂ : A₂ → B₂}    [group B₂]    {c₂b₂ : B₂ → C₂}    [group C₂]    {d₂c₂ : C₂ → D₂}    [group D₂]    {e₂d₂ : D₂ → E₂}    [group E₂]

variables [is_group_hom b₁a₁] [is_group_hom c₁b₁] [is_group_hom d₁c₁] [is_group_hom e₁d₁]
variables [is_group_hom b₂a₂] [is_group_hom c₂b₂] [is_group_hom d₂c₂] [is_group_hom e₂d₂]
variables [is_group_hom a₂a₁] [is_group_hom b₂b₁] [is_group_hom c₂c₁] [is_group_hom d₂d₁] [is_group_hom e₂e₁]

Now all we need is the tactic which proves it ;-)

Update:

import tactic
import tactic.find
import init.function
import algebra.group
import group_theory.subgroup

open function

section five_lemma

universes u

variables {A B : Type u} [group A] [group B]
definition im (f : A → B) := set.range f


variables {A₁ B₁ C₁ D₁ E₁ : Type u}
variables {A₂ B₂ C₂ D₂ E₂ : Type u}

variables  [group A₁]    {f₁ : A₁ → B₁}   [group B₁]    {g₁ : B₁ → C₁}   [group C₁]    {h₁ : C₁ → D₁}   [group D₁]    {i₁ : D₁ → E₁}   [group E₁]
variables {j : A₁ → A₂}                  {k : B₁ → B₂}                  {l : C₁ → C₂}                  {m : D₁ → D₂}                  {n : E₁ → E₂}
variables  [group A₂]    {f₂ : A₂ → B₂}   [group B₂]    {g₂ : B₂ → C₂}   [group C₂]    {h₂ : C₂ → D₂}   [group D₂]    {i₂ : D₂ → E₂}   [group E₂]

variables [is_group_hom f₁] [is_group_hom g₁] [is_group_hom h₁] [is_group_hom i₁]
variables [is_group_hom f₂] [is_group_hom g₂] [is_group_hom h₂] [is_group_hom i₂]
variables [is_group_hom j] [is_group_hom k] [is_group_hom l] [is_group_hom m] [is_group_hom n]


open is_group_hom

lemma x_is_1_if_fx_is_1_and_f_injective
 (f : A → B) [is_group_hom f] [injective f] (x : A)
 : f x = 1 → x = 1 :=
begin
 intro hfx,
 have := one f, apply_assumption, cc
end

lemma five_lemma
(com₁ : k ∘ f₁ = f₂ ∘ j)
(com₂ : l ∘ g₁ = g₂ ∘ k)
(com₃ : m ∘ h₁ = h₂ ∘ l)
(com₄ : n ∘ i₁ = i₂ ∘ m)
(eB₁ : im f₁ = ker g₁)
(eC₁ : im g₁ = ker h₁)
(eD₁ : im h₁ = ker i₁)
(eB₂ : im f₂ = ker g₂)
(eC₂ : im g₂ = ker h₂)
(eD₂ : im h₂ = ker i₂)
(hj : surjective j)
(hk : bijective k)
(hm : bijective m)
(hn : injective n)
: bijective l :=
begin
 have := one f₁,
 have := one g₁,
 have := one h₁,
 have := one i₁,
 have := one f₂,
 have := one g₂,
 have := one h₂,
 have := one i₂,
 have := one j,
 have := one k,
 have := one l,
 have := one m,
 have := one n,
 split, {
  apply inj_of_trivial_ker l,
  apply set.ext, intro x,
  split, { -- x ∈ ker l → x = 1
   intro hx,
   rw mem_ker at hx,
   simp,
   have : (h₂ ∘ l) x = 1, unfold comp, cc,
   have : (m ∘ h₁) x = 1, cc,
   have : m (h₁ x) = 1, apply_assumption,
   have : injective m, apply hm.1,
   have : h₁ x = 1, apply_assumption, cc,
   have : x ∈ ker h₁, rwa mem_ker h₁,
   have : x ∈ im g₁, cc,
   have : ∃ y : B₁, g₁ y = x, apply_assumption,
   cases this with y,
   have : (l ∘ g₁) y = 1, unfold comp, cc,
   have : (g₂ ∘ k) y = 1, cc,
   have : g₂ (k y) = 1, apply_assumption,
   have : k y ∈ ker g₂, rwa mem_ker g₂,
   have : k y ∈ im f₂, cc,
   have : ∃ z : A₂, f₂ z = k y, apply_assumption,
   cases this with z,
   have : ∃ w : A₁, j w = z, apply_assumption,
   cases this with w,
   have : (f₂ ∘ j) w = k y, unfold comp, cc,
   have : (k ∘ f₁) w = k y, cc,
   have : k (f₁ w) = k y, apply_assumption,
   have : injective k, apply hk.1,
   have : f₁ w = y, apply_assumption,
   have : f₁ w ∈ im f₁, show f₁ w ∈ set.range f₁, simp,
   have : y ∈ im f₁, admit, -- this should be easy, but apply_assumption fails.
   have : y ∈ ker g₁, cc,
   have : g₁ y = 1, rwa ←mem_ker g₁,
   have : x = 1, cc,
  }, { -- x = 1 → x ∈ ker l
   intro hx,
   simp at hx,
   rw is_group_hom.mem_ker,
   have := is_group_hom.one l,
   cc
  }
 }, {
 }
end

end five_lemma