awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (hypothesis)
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_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
have hy₁ : 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
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (hypothesis)
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₂)
⊢ Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
have hy₁ : (f₁ : (a : M₁) → M₂) a = x
Tactic: apply hi₂ at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
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
⊢ Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) x : M₃) (1 : M₃)
have 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₃)
Tactic: subst hy
Cleared hypotheses: x, hm, hy
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
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₃)
⊢ Eq.{u_3 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) ((f₁ : (a : M₁) → M₂) a : M₂) : M₃) (1 : M₃)
have rw : Eq.{u_3 + 1} (α := M₃) 1 1
Tactic: rw [hf₁.apply_apply_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
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.Bijective.{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₃)
hg₂ : Function.Surjective.{u_7 + 1, u_8 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
⊢ Function.Bijective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
have refine : ∀ (y : N₃), ∃ (a : M₃), (i₃ : (a : M₃) → N₃) a = y
Tactic: refine ⟨injective_of_surjective_of_injective_of_right_exact f₁ f₂ g₁ g₂ i₁ i₂ i₃
    hc₁ hc₂ hf₁ hg₁ hi₁ hi₂.1 hf₂, fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
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.Bijective.{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₃)
hg₂ : Function.Surjective.{u_7 + 1, u_8 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
y : N₃
⊢ ∃ (a : M₃), (i₃ : (a : M₃) → N₃) a = y
have obtain : ∀ (y : N₂), ∃ (a : M₃), Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) a : N₃) ((g₂ : (a : N₂) → N₃) y : N₃)
Tactic: obtain ⟨y, rfl⟩ := hg₂ y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
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.Bijective.{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₃)
hg₂ : Function.Surjective.{u_7 + 1, u_8 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
y : N₂
⊢ ∃ (a : M₃), Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) a : N₃) ((g₂ : (a : N₂) → N₃) y : N₃)
have obtain : ∀ (y : M₂),
  ∃ (a : M₃),
    Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) a : N₃) ((g₂ : (a : N₂) → N₃) ((i₂ : (a : M₂) → N₂) y : N₂) : N₃)
Tactic: obtain ⟨y, rfl⟩ := hi₂.2 y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : AddCommGroup N₂
inst_9 : AddCommGroup N₃
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Function.Exact.{u_7, u_8, u_9} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → 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₃)
hg₀ : Function.Injective.{u_7 + 1, u_8 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
⊢ Function.Surjective.{u_2 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
have refine : ∀ (y : N₁),
  Eq.{u_8 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (0 : N₂) ↔
    Membership.mem (γ := Set N₁) (Set.range (ι := Unit) (⇑0 : (a : Unit) → N₁)) y
Tactic: refine surjective_of_surjective_of_surjective_of_injective (0 : Unit →ₗ[R] M₁) f₁ f₂
    (0 : Unit →ₗ[R] N₁) g₁ g₂ 0 i₁ i₂ i₃ (by simp) hc₁ hc₂ hf₁ (fun y ↦ ?_) hg₁
    (fun | .unit => ⟨0, rfl⟩) hi₂ hi₃
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : AddCommGroup N₂
inst_9 : AddCommGroup N₃
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Function.Exact.{u_7, u_8, u_9} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → 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₃)
hg₀ : Function.Injective.{u_7 + 1, u_8 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
y : N₁
⊢ Eq.{u_8 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (0 : N₂) ↔
    Membership.mem (γ := Set N₁) (Set.range (ι := Unit) (⇑0 : (a : Unit) → N₁)) y
have simp : Eq.{u_8 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (0 : N₂) ↔ 0 = y
Tactic: simp only [Set.mem_range, zero_apply, exists_const]
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : AddCommGroup N₂
inst_9 : AddCommGroup N₃
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Function.Exact.{u_7, u_8, u_9} (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.Bijective.{u_3 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hf₂ : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hg₂ : Function.Surjective.{u_8 + 1, u_9 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
⊢ Function.Bijective.{u_4 + 1, u_9 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
have refine : ∀ (y : N₃), ∃ (a : M₃), (i₃ : (a : M₃) → N₃) a = y
Tactic: refine ⟨injective_of_surjective_of_injective_of_right_exact f₁ f₂ g₁ g₂ i₁ i₂ i₃
    hc₁ hc₂ hf₁ hg₁ hi₁ hi₂.1 hf₂, fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : AddCommGroup N₂
inst_9 : AddCommGroup N₃
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Function.Exact.{u_7, u_8, u_9} (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.Bijective.{u_3 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hf₂ : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hg₂ : Function.Surjective.{u_8 + 1, u_9 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
y : N₃
⊢ ∃ (a : M₃), (i₃ : (a : M₃) → N₃) a = y
have obtain : ∀ (y : N₂), ∃ (a : M₃), Eq.{u_9 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) a : N₃) ((g₂ : (a : N₂) → N₃) y : N₃)
Tactic: obtain ⟨y, rfl⟩ := hg₂ y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.FiveLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : AddCommGroup N₂
inst_9 : AddCommGroup N₃
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Function.Exact.{u_7, u_8, u_9} (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.Bijective.{u_3 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hf₂ : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hg₂ : Function.Surjective.{u_8 + 1, u_9 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
y : N₂
⊢ ∃ (a : M₃), Eq.{u_9 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) a : N₃) ((g₂ : (a : N₂) → N₃) y : N₃)
have obtain : ∀ (y : M₂),
  ∃ (a : M₃),
    Eq.{u_9 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) a : N₃) ((g₂ : (a : N₂) → N₃) ((i₂ : (a : M₂) → N₂) y : N₂) : N₃)
Tactic: obtain ⟨y, rfl⟩ := hi₂.2 y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 : Type u
x_1 x y : FreeMagma α_1
ih1 : id <$> x = x
ih2 : id <$> y = y
⊢ id <$> (x * y) = x * y
have rw : id <$> x * id <$> y = x * y
Tactic: rw [map_mul', ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 : Type u
x_1 x y : FreeMagma α_1
ih1 : id <$> x = x
ih2 : id <$> y = y
rw : id <$> x * id <$> y = x * y
⊢ id <$> (x * y) = x * y
have rw₁ : x * id <$> y = x * y
Tactic: rw [map_mul', ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 : Type u
x_1 x y : FreeMagma α_1
ih1 : id <$> x = x
ih2 : id <$> y = y
rw : id <$> x * id <$> y = x * y
rw₁ : x * id <$> y = x * y
⊢ id <$> (x * y) = x * y
have rw₂ : x * y = x * y
Tactic: rw [map_mul', ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeMagma α_1
f : α_1 → FreeMagma β_1
g : β_1 → FreeMagma γ
x y : FreeMagma α_1
ih1 : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
⊢ x * y >>= f >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
have rw : (x >>= f) * (y >>= f) >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
Tactic: rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeMagma α_1
f : α_1 → FreeMagma β_1
g : β_1 → FreeMagma γ
x y : FreeMagma α_1
ih1 : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
rw : (x >>= f) * (y >>= f) >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
⊢ x * y >>= f >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
have rw₁ : (x >>= f >>= g) * (y >>= f >>= g) = x * y >>= fun (x : α_1) ↦ f x >>= g
Tactic: rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeMagma α_1
f : α_1 → FreeMagma β_1
g : β_1 → FreeMagma γ
x y : FreeMagma α_1
ih1 : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
rw : (x >>= f) * (y >>= f) >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
rw₁ : (x >>= f >>= g) * (y >>= f >>= g) = x * y >>= fun (x : α_1) ↦ f x >>= g
⊢ x * y >>= f >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
have rw₂ : (x >>= f >>= g) * (y >>= f >>= g) =
  HMul.hMul (α := FreeMagma γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g)
Tactic: rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeMagma α_1
f : α_1 → FreeMagma β_1
g : β_1 → FreeMagma γ
x y : FreeMagma α_1
ih1 : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
rw : (x >>= f) * (y >>= f) >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
rw₁ : (x >>= f >>= g) * (y >>= f >>= g) = x * y >>= fun (x : α_1) ↦ f x >>= g
rw₂ :
  (x >>= f >>= g) * (y >>= f >>= g) =
    HMul.hMul (α := FreeMagma γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g)
⊢ x * y >>= f >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
have rw₃ : (x >>= fun (x : α_1) ↦ f x >>= g) * (y >>= f >>= g) =
  HMul.hMul (α := FreeMagma γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g)
Tactic: rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeMagma α_1
f : α_1 → FreeMagma β_1
g : β_1 → FreeMagma γ
x y : FreeMagma α_1
ih1 : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
rw : (x >>= f) * (y >>= f) >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
rw₁ : (x >>= f >>= g) * (y >>= f >>= g) = x * y >>= fun (x : α_1) ↦ f x >>= g
rw₂ :
  (x >>= f >>= g) * (y >>= f >>= g) =
    HMul.hMul (α := FreeMagma γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g)
rw₃ :
  (x >>= fun (x : α_1) ↦ f x >>= g) * (y >>= f >>= g) =
    HMul.hMul (α := FreeMagma γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g)
⊢ x * y >>= f >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
have rw₄ : HMul.hMul (α := FreeMagma γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g) =
  HMul.hMul (α := FreeMagma γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g)
Tactic: rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 : Type u
x_1 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma α_1)) (traverse pure x) (pure x)
ih2 : Eq (α := Id (FreeMagma α_1)) (traverse pure y) (pure y)
⊢ Eq (α := Id (FreeMagma α_1)) (traverse pure (x * y)) (pure (x * y))
have rw : Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> traverse pure x <*> traverse pure y)
  (pure (x * y))
Tactic: rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 : Type u
x_1 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma α_1)) (traverse pure x) (pure x)
ih2 : Eq (α := Id (FreeMagma α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> traverse pure x <*> traverse pure y)
    (pure (x * y))
⊢ Eq (α := Id (FreeMagma α_1)) (traverse pure (x * y)) (pure (x * y))
have rw₁ : Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x <*> traverse pure y) (pure (x * y))
Tactic: rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 : Type u
x_1 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma α_1)) (traverse pure x) (pure x)
ih2 : Eq (α := Id (FreeMagma α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> traverse pure x <*> traverse pure y)
    (pure (x * y))
rw₁ :
  Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x <*> traverse pure y) (pure (x * y))
⊢ Eq (α := Id (FreeMagma α_1)) (traverse pure (x * y)) (pure (x * y))
have rw₂ : Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x <*> pure y) (pure (x * y))
Tactic: rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]