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_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₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (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.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
y : M₃
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) y : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
⊢ Eq.{u_4 + 1} (α := M₄) ((f₃ : (a : M₃) → M₄) y : M₄) (1 : M₄)

Tactic:
simpa [hy, hg₂.apply_apply_eq_one, map_eq_one_iff _ hi₄] using (DFunLike.congr_fun hc₃ y).symm

Premises used: DFunLike.congr_fun, map_eq_one_iff, Eq.symm, Function.MulExact.apply_apply_eq_one
-- 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_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₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (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.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
y : M₃
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) y : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
obtain :
  ∀ (a : M₂)
    (hy :
      Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)),
    ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
⊢ ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x

Tactic:
obtain ⟨a, rfl⟩ : y ∈ Set.range f₂ := (hf₂ _).mp <| by
    simpa [hy, hg₂.apply_apply_eq_one, map_eq_one_iff _ hi₄] using (DFunLike.congr_fun hc₃ y).symm

Premises used: Iff.mp, Set.range, DFunLike.coe, 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_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₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (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.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
a : M₂
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
⊢ Eq.{u_8 + 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_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₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (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.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
a : M₂
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
⊢ Eq.{u_8 + 1} (α := N₃) ((g₂ : (a : N₂) → N₃) (HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)) : N₃) (1 : N₃)

Tactic:
simp [← hy, show g₂ (i₂ a) = i₃ (f₂ a) by simpa using DFunLike.congr_fun hc₂ a]
-- 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_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₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (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.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
a : M₂
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
obtain :
  ∀ (b : N₁) (hb : (g₁ : (a : N₁) → N₂) b = HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)),
    ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
⊢ ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x

Tactic:
obtain ⟨b, hb⟩ : x / i₂ a ∈ Set.range g₁ := (hg₁ _).mp <| by
    simp [← hy, show g₂ (i₂ a) = i₃ (f₂ a) by simpa using DFunLike.congr_fun hc₂ a]

Premises used: Iff.mp, Set.range, DFunLike.coe
-- 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_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₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (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.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
a : M₂
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
b : N₁
hb : (g₁ : (a : N₁) → N₂) b = HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)
obtain :
  ∀ (o : M₁)
    (hb : (g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) o : N₁) = HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)),
    ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
⊢ ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x

Tactic:
obtain ⟨o, rfl⟩ := hi₁ b

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_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₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (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.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
a : M₂
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
o : M₁
hb : (g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) o : N₁) = HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)
h : (i₂ : (a : M₂) → N₂) (HMul.hMul (α := M₂) ((f₁ : (a : M₁) → M₂) o : M₂) a) = x
⊢ ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x

Tactic:
use f₁ o * a

Premises used: DFunLike.coe
-- 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_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₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (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.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
a : M₂
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
o : M₁
hb : (g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) o : N₁) = HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)
⊢ Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) o : N₁) : N₂)
    ((i₂ : (a : M₂) → N₂) ((f₁ : (a : M₁) → M₂) o : M₂) : N₂)

Tactic:
simpa using DFunLike.congr_fun hc₁ o

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_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₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (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.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
a : M₂
hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) a : M₃) : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)
o : M₁
hb : (g₁ : (a : N₁) → N₂) ((i₁ : (a : M₁) → N₁) o : N₁) = HDiv.hDiv (β := N₂) x ((i₂ : (a : M₂) → N₂) a : N₂)
⊢ (i₂ : (a : M₂) → N₂) (HMul.hMul (α := M₂) ((f₁ : (a : M₁) → M₂) o : M₂) a) = x

Tactic:
simp [← show g₁ (i₁ o) = i₂ (f₁ o) by simpa using DFunLike.congr_fun hc₁ o, hb]
-- 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_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₃ : Function.Injective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hg₀ : Function.Injective.{u_6 + 1, u_7 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
⊢ Eq (α := Unit →* N₁) (comp (N := Unit) 1 1) (i₁.comp 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_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₃ : Function.Injective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hg₀ : Function.Injective.{u_6 + 1, u_7 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
refine :
  ∀ (y : N₁),
    Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (1 : N₂) ↔
      Membership.mem (γ := Set N₁) (Set.range (ι := Unit) (⇑1 : (a : Unit) → N₁)) y
⊢ Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)

Tactic:
refine surjective_of_surjective_of_surjective_of_injective (1 : Unit →* M₁) f₁ f₂ (1 : Unit →* N₁)
    g₁ g₂ 1 i₁ i₂ i₃ (by simp) hc₁ hc₂ hf₁ (fun y ↦ ?_) hg₁ (fun | .unit => ⟨0, rfl⟩) hi₂ hi₃

Premises used: Exists, _private.0.MonoidHom.surjective_of_surjective_of_injective_of_left_exact.match_1, MonoidHom.surjective_of_surjective_of_surjective_of_injective, Exists.intro, OfNat.ofNat, Eq, DFunLike.coe, rfl
-- 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_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₃ : Function.Injective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hg₀ : Function.Injective.{u_6 + 1, u_7 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
y : N₁
simp : Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (1 : N₂) ↔ 1 = y
⊢ Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (1 : N₂) ↔
    Membership.mem (γ := Set N₁) (Set.range (ι := Unit) (⇑1 : (a : Unit) → N₁)) y

Tactic:
simp only [Set.mem_range, one_apply, exists_const]

Premises used: Set.mem_range, exists_const, MonoidHom.one_apply
-- 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_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₃ : Function.Injective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hg₀ : Function.Injective.{u_6 + 1, u_7 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
y : N₁
⊢ Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (1 : N₂) ↔ 1 = y

Tactic:
⟨fun h ↦ (hg₀ ((map_one _).trans h.symm)), fun h ↦ h ▸ (map_one _)⟩

Premises used: Eq.rec, map_one, Iff.intro, Eq.symm, Eq.trans
-- 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_2 + 1, u_7 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₃ : Function.Injective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hg₀ : Function.Injective.{u_6 + 1, u_7 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
y : N₁
⊢ Eq.{u_7 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (1 : N₂) ↔ 1 = y

Tactic:
exact ⟨fun h ↦ (hg₀ ((map_one _).trans h.symm)), fun h ↦ h ▸ (map_one _)⟩
-- 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₄)
rw : ∀ (a : M₃), Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) a : N₃) (1 : N₃) → a = 1
⊢ Function.Injective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)

Tactic:
rw [injective_iff_map_eq_one]

Premises used: injective_iff_map_eq_one
-- 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₃)
h : Eq.{u_9 + 1} (α := N₄) ((i₄ : (a : M₄) → N₄) ((f₃ : (a : M₃) → M₄) m : M₄) : N₄) (1 : N₄)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : Eq.{u_4 + 1} (α := M₄) ((f₃ : (a : M₃) → M₄) m : M₄) (1 : M₄)),
    Eq.{u_4 + 1} (α := M₄) ((f₃ : (a : M₃) → M₄) m : M₄) (1 : M₄)
⊢ Eq.{u_4 + 1} (α := M₄) ((f₃ : (a : M₃) → M₄) m : M₄) (1 : M₄)

Tactic:
rwa [map_eq_one_iff _ hi₄] at h

Premises used: map_eq_one_iff
-- 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₃)
suffices : Eq.{u_9 + 1} (α := N₄) ((i₄ : (a : M₄) → N₄) ((f₃ : (a : M₃) → M₄) m : M₄) : N₄) (1 : N₄)
⊢ Eq.{u_4 + 1} (α := M₄) ((f₃ : (a : M₃) → M₄) m : M₄) (1 : M₄)

Tactic:
suffices h : i₄ (f₃ m) = 1 by rwa [map_eq_one_iff _ hi₄] at h