awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
m : M₃
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) m : N₃) (1 : N₃)
⊢ Eq.{u_9 + 1} (α := N₄) ((g₃ : (a : N₃) → N₄) ((i₃ : (a : M₃) → N₃) m : N₃) : N₄)
    ((i₄ : (a : M₄) → N₄) ((f₃ : (a : M₃) → M₄) m : M₄) : N₄)

Tactic:
simpa using DFunLike.congr_fun hc₃ m

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
m : M₃
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) m : N₃) (1 : N₃)
⊢ Eq.{u_9 + 1} (α := N₄) ((i₄ : (a : M₄) → N₄) ((f₃ : (a : M₃) → M₄) m : M₄) : N₄) (1 : N₄)

Tactic:
simp [← show g₃ (i₃ m) = i₄ (f₃ m) by simpa using DFunLike.congr_fun hc₃ m, hm]
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
m : M₃
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) m : N₃) (1 : N₃)
obtain :
  ∀ (x : M₂) (hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)),
    Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
⊢ m = 1

Tactic:
obtain ⟨x, rfl⟩ := (hf₂ m).mp <| by
    suffices h : i₄ (f₃ m) = 1 by rwa [map_eq_one_iff _ hi₄] at h
    simp [← show g₃ (i₃ m) = i₄ (f₃ m) by simpa using DFunLike.congr_fun hc₃ m, hm]

Premises used: Iff.mp, rfl
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : M₂
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
⊢ Eq.{u_8 + 1} (α := N₃) ((g₂ : (a : N₂) → N₃) ((i₂ : (a : M₂) → N₂) x : N₂) : N₃)
    ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃)

Tactic:
simpa using DFunLike.congr_fun hc₂ x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : M₂
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
rwa rwa₁ rwa₂ rwa₃ : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
⊢ Eq.{u_8 + 1} (α := N₃) ((g₂ : (a : N₂) → N₃) ((i₂ : (a : M₂) → N₂) x : N₂) : N₃) (1 : N₃)

Tactic:
rwa [show g₂ (i₂ x) = i₃ (f₂ x) by simpa using DFunLike.congr_fun hc₂ x]
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : M₂
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
obtain :
  ∀ (y : N₁) (hy : Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) ((i₂ : (a : M₂) → N₂) x : N₂)),
    Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
⊢ Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)

Tactic:
obtain ⟨y, hy⟩ := (hg₁ _).mp <| by
    rwa [show g₂ (i₂ x) = i₃ (f₂ x) by simpa using DFunLike.congr_fun hc₂ x]

Premises used: Iff.mp
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : M₂
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
y : N₁
hy : Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) ((i₂ : (a : M₂) → N₂) x : N₂)
obtain :
  ∀ (a : M₁)
    (hy :
      Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) a : N₁) : N₂) ((i₂ : (a : M₂) → N₂) x : N₂)),
    Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
⊢ Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)

Tactic:
obtain ⟨a, rfl⟩ := hi₁ y

Premises used: rfl
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : M₂
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
a : M₁
hy : Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) a : N₁) : N₂) ((i₂ : (a : M₂) → N₂) x : N₂)
⊢ Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) a : N₁) : N₂)
    ((i₂ : (a : M₂) → N₂) ((f₁ : (a : M₁) → M₂) a : M₂) : N₂)

Tactic:
simpa using DFunLike.congr_fun hc₁ a

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : M₂
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
a : M₁
hy : Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) a : N₁) : N₂) ((i₂ : (a : M₂) → N₂) x : N₂)
⊢ Eq.{u_7 + 1} (α := N₂) ((i₂ : (a : M₂) → N₂) ((f₁ : (a : M₁) → M₂) a : M₂) : N₂) ((i₂ : (a : M₂) → N₂) x : N₂)

Tactic:
rw [show g₁ (i₁ a) = i₂ (f₁ a) by simpa using DFunLike.congr_fun hc₁ a] at hy
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : M₂
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
a : M₁
hy : Eq.{u_7 + 1} (α := N₂) ((i₂ : (a : M₂) → N₂) ((f₁ : (a : M₁) → M₂) a : M₂) : N₂) ((i₂ : (a : M₂) → N₂) x : N₂)
⊢ (f₁ : (a : M₁) → M₂) a = x

Tactic:
apply hi₂ at hy
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : M₂
hm : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) x : M₃) : N₃) (1 : N₃)
a : M₁
hy : (f₁ : (a : M₁) → M₂) a = x
subst :
  ∀
    (hm :
      Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) ((f₁ : (a : M₁) → M₂) a : M₂) : M₃) : N₃)
        (1 : N₃)),
    Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) ((f₁ : (a : M₁) → M₂) a : M₂) : M₃) (1 : M₃)
⊢ Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)

Tactic:
subst hy
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
a : M₁
hm :
  Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) ((f₁ : (a : M₁) → M₂) a : M₂) : M₃) : N₃) (1 : N₃)
rw rw₁ : Eq.{u_3 + 1} (α := M₃) 1 1
⊢ Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) ((f₁ : (a : M₁) → M₂) a : M₂) : M₃) (1 : M₃)

Tactic:
rw [hf₁.apply_apply_eq_one]

Premises used: Function.MulExact.apply_apply_eq_one
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group N₁
inst_4 : Group N₂
inst_5 : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hf₂ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
⊢ Eq (α := M₃ →* Unit) (comp 1 i₃) (comp (N := Unit) 1 1)

Tactic:
simp
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group N₁
inst_4 : Group N₂
inst_5 : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hf₂ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
y : M₃
⊢ Eq (α := Unit) ((1 : (a : M₃) → Unit) y : Unit) (1 : Unit) ↔
    Membership.mem (γ := Set M₃) (Set.range.{u_3, u_2 + 1} (ι := M₂) (⇑f₂ : (a : M₂) → M₃)) y

Tactic:
simpa using hf₂ y
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group N₁
inst_4 : Group N₂
inst_5 : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Injective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hf₂ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
⊢ ∀ ⦃a₂ : Unit⦄, Eq (α := Unit) ((1 : (a : Unit) → Unit) () : Unit) ((1 : (a : Unit) → Unit) a₂ : Unit) → () = a₂

Tactic:
simp
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
M₅ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
N₅ : Type u_10
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group M₅
inst_5 : Group N₁
inst_6 : Group N₂
inst_7 : Group N₃
inst_8 : Group N₄
inst_9 : Group N₅
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
f₄ : M₄ →* M₅
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
g₄ : N₄ →* N₅
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
i₅ : M₅ →* N₅
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hc₄ : g₄.comp i₄ = i₅.comp f₄
hf₁ : Function.MulExact.{u_1, u_2, u_3} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hf₃ : Function.MulExact.{u_3, u_4, u_5} (M := M₃) (N := M₄) (P := M₅) (⇑f₃ : (a : M₃) → M₄) (⇑f₄ : (a : M₄) → M₅)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (M := N₂) (N := N₃) (P := N₄) (⇑g₂ : (a : N₂) → N₃) (⇑g₃ : (a : N₃) → N₄)
hg₃ : Function.MulExact.{u_8, u_9, u_10} (M := N₃) (N := N₄) (P := N₅) (⇑g₃ : (a : N₃) → N₄) (⇑g₄ : (a : N₄) → N₅)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₂ : Function.Bijective.{u_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Bijective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
hi₅ : Function.Injective.{u_5 + 1, u_10 + 1} (α := M₅) (β := N₅) (⇑i₅ : (a : M₅) → N₅)
⊢ Function.Bijective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)

Tactic:
⟨injective_of_surjective_of_injective_of_injective f₁ f₂ f₃ g₁ g₂ g₃ i₁ i₂ i₃ i₄
      hc₁ hc₂ hc₃ hf₁ hf₂ hg₁ hi₁ hi₂.1 hi₄.1,
    surjective_of_surjective_of_surjective_of_injective f₂ f₃ f₄ g₂ g₃ g₄ i₂ i₃ i₄ i₅
      hc₂ hc₃ hc₄ hf₃ hg₂ hg₃ hi₂.2 hi₄.2 hi₅⟩

Premises used: MonoidHom.surjective_of_surjective_of_surjective_of_injective, MonoidHom.injective_of_surjective_of_injective_of_injective, And.right, And.left, And.intro, Function.Bijective