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

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