awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.Bijective.{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₃)
hf₀ : Function.Injective.{u_1 + 1, u_2 + 1} (α := M₁) (β := M₂) (⇑f₁ : (a : M₁) → M₂)
hg₀ : Function.Injective.{u_6 + 1, u_7 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
⊢ Function.Bijective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)

Tactic:
⟨fun {x y} h ↦ (hf₀ (hi₂.1 (congr($hc₁ x).symm.trans (congr(g₁ $h).trans congr($hc₁ y))))),
    surjective_of_surjective_of_injective_of_left_exact f₁ f₂ g₁ g₂ i₁ i₂ i₃
      hc₁ hc₂ hf₁ hg₁ hi₂.2 hi₃ hg₀⟩

Premises used: MonoidHom.surjective_of_surjective_of_injective_of_left_exact, congrArg, id, And.right, And.left, And.intro, Function.Bijective, Eq.symm, DFunLike.coe, 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_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₃)

Tactic:
⟨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 ↦ ?_⟩

Premises used: MonoidHom.injective_of_surjective_of_injective_of_right_exact, And.left, And.intro, Function.Bijective
-- 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.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₃)
refine : ∀ (y : N₃), ∃ (a : M₃), (i₃ : (a : M₃) → N₃) a = y
⊢ Function.Bijective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)

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 ↦ ?_⟩
-- 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.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₃
obtain : ∀ (y : N₂), ∃ (a : M₃), Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) a : N₃) ((g₂ : (a : N₂) → N₃) y : N₃)
⊢ ∃ (a : M₃), (i₃ : (a : M₃) → N₃) a = y

Tactic:
obtain ⟨y, rfl⟩ := hg₂ y

Premises used: 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_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₂
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₃)
⊢ ∃ (a : M₃), Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) a : N₃) ((g₂ : (a : N₂) → N₃) y : N₃)

Tactic:
obtain ⟨y, rfl⟩ := hi₂.2 y

Premises used: And.right, 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_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 : 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:
⟨f₂ y, congr($hc₂ y).symm⟩

Premises used: congrArg, id, Exists.intro, Eq.symm, DFunLike.coe
-- 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.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 : 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:
exact ⟨f₂ y, congr($hc₂ y).symm⟩
-- Module: Mathlib.Algebra.FiveLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
M₄ : Type u_5
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
N₄ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : AddCommGroup N₁
inst_10 : AddCommGroup N₂
inst_11 : AddCommGroup N₃
inst_12 : AddCommGroup N₄
inst_13 : Module R N₁
inst_14 : Module R N₂
inst_15 : Module R N₃
inst_16 : Module R N₄
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M₄
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
g₃ : N₃ →ₗ[R] N₄
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
i₄ : M₄ →ₗ[R] N₄
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hc₃ : g₃ ∘ₗ i₃ = i₄ ∘ₗ f₃
hf₂ : Function.Exact.{u_3, u_4, u_5} (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₃)
hg₂ : Function.Exact.{u_8, u_9, u_10} (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.Surjective.{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.Surjective.{u_3 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)

Tactic:
AddMonoidHom.surjective_of_surjective_of_surjective_of_injective
    f₁.toAddMonoidHom f₂.toAddMonoidHom f₃.toAddMonoidHom g₁.toAddMonoidHom g₂.toAddMonoidHom
    g₃.toAddMonoidHom i₁.toAddMonoidHom i₂.toAddMonoidHom i₃.toAddMonoidHom i₄.toAddMonoidHom
    (AddMonoidHom.ext fun x ↦ DFunLike.congr_fun hc₁ x)
    (AddMonoidHom.ext fun x ↦ DFunLike.congr_fun hc₂ x)
    (AddMonoidHom.ext fun x ↦ DFunLike.congr_fun hc₃ x) hf₂ hg₁ hg₂ hi₁ hi₃ hi₄

Premises used: LinearMap.toAddMonoidHom, DFunLike.congr_fun, AddMonoidHom.ext, AddMonoidHom.surjective_of_surjective_of_surjective_of_injective
-- Module: Mathlib.Algebra.FiveLemma
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₂)
⊢ Eq (α := Unit →ₗ[R] N₁) (0 ∘ₗ 0) (i₁ ∘ₗ 0)

Tactic:
simp
-- Module: Mathlib.Algebra.FiveLemma
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₂)
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
⊢ Function.Surjective.{u_2 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)

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₃

Premises used: Exists, _private.0.MonoidHom.surjective_of_surjective_of_injective_of_left_exact.match_1, Exists.intro, LinearMap.surjective_of_surjective_of_surjective_of_injective, OfNat.ofNat, Eq, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.FiveLemma
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₁
simp : Eq.{u_8 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) y : N₂) (0 : N₂) ↔ 0 = y
⊢ 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:
simp only [Set.mem_range, zero_apply, exists_const]

Premises used: LinearMap.zero_apply, Set.mem_range, exists_const
-- Module: Mathlib.Algebra.FiveLemma
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₂) ↔ 0 = y

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

Premises used: Eq.rec, map_zero, Iff.intro, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.FiveLemma
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₂) ↔ 0 = y

Tactic:
exact ⟨fun h ↦ (hg₀ ((map_zero _).trans h.symm)), fun h ↦ h ▸ (map_zero _)⟩
-- Module: Mathlib.Algebra.FiveLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
M₄ : Type u_5
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
N₄ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : AddCommGroup N₁
inst_10 : AddCommGroup N₂
inst_11 : AddCommGroup N₃
inst_12 : AddCommGroup N₄
inst_13 : Module R N₁
inst_14 : Module R N₂
inst_15 : Module R N₃
inst_16 : Module R N₄
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M₄
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
g₃ : N₃ →ₗ[R] N₄
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
i₄ : M₄ →ₗ[R] N₄
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
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₃)
hf₂ : Function.Exact.{u_3, u_4, u_5} (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.Injective.{u_3 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
hi₄ : Function.Injective.{u_5 + 1, u_10 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
⊢ Function.Injective.{u_4 + 1, u_9 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)

Tactic:
AddMonoidHom.injective_of_surjective_of_injective_of_injective
    f₁.toAddMonoidHom f₂.toAddMonoidHom f₃.toAddMonoidHom g₁.toAddMonoidHom g₂.toAddMonoidHom
    g₃.toAddMonoidHom i₁.toAddMonoidHom i₂.toAddMonoidHom i₃.toAddMonoidHom i₄.toAddMonoidHom
    (AddMonoidHom.ext fun x ↦ DFunLike.congr_fun hc₁ x)
    (AddMonoidHom.ext fun x ↦ DFunLike.congr_fun hc₂ x)
    (AddMonoidHom.ext fun x ↦ DFunLike.congr_fun hc₃ x) hf₁ hf₂ hg₁ hi₁ hi₂ hi₄

Premises used: LinearMap.toAddMonoidHom, DFunLike.congr_fun, AddMonoidHom.injective_of_surjective_of_injective_of_injective, AddMonoidHom.ext
-- Module: Mathlib.Algebra.FiveLemma
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.Injective.{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₃)
⊢ Eq (α := M₃ →ₗ[R] Unit) (0 ∘ₗ i₃) (0 ∘ₗ 0)

Tactic:
simp
-- Module: Mathlib.Algebra.FiveLemma
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.Injective.{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₃)
y : M₃
⊢ Eq (α := Unit) ((0 : (a : M₃) → Unit) y : Unit) (0 : Unit) ↔
    Membership.mem (γ := Set M₃) (Set.range.{u_4, u_3 + 1} (ι := M₂) (⇑f₂ : (a : M₂) → M₃)) y

Tactic:
simpa using hf₂ y
-- Module: Mathlib.Algebra.FiveLemma
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.Injective.{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₃)
⊢ ∀ ⦃a₂ : Unit⦄, Eq (α := Unit) ((0 : (a : Unit) → Unit) () : Unit) ((0 : (a : Unit) → Unit) a₂ : Unit) → () = a₂

Tactic:
simp