awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
M₅ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
N₄ : Type u_10
N₅ : Type u_11
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : AddCommGroup M₅
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R M₃
inst_9 : Module R M₄
inst_10 : Module R M₅
inst_11 : AddCommGroup N₁
inst_12 : AddCommGroup N₂
inst_13 : AddCommGroup N₃
inst_14 : AddCommGroup N₄
inst_15 : AddCommGroup N₅
inst_16 : Module R N₁
inst_17 : Module R N₂
inst_18 : Module R N₃
inst_19 : Module R N₄
inst_20 : Module R N₅
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M₄
f₄ : M₄ →ₗ[R] M₅
g₁ : N₁ →ₗ[R] N₂
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₄
i₅ : M₅ →ₗ[R] N₅
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
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₄)
hf₃ : Function.Exact.{u_4, u_5, u_6} (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₄)
hg₃ : Function.Exact.{u_9, u_10, u_11} (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₂)
hi₄ : Function.Bijective.{u_5 + 1, u_10 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
hi₅ : Function.Injective.{u_6 + 1, u_11 + 1} (α := M₅) (β := N₅) (⇑i₅ : (a : M₅) → N₅)
⊢ Function.Bijective.{u_4 + 1, u_9 + 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: And.right, And.left, And.intro, Function.Bijective, LinearMap.injective_of_surjective_of_injective_of_injective, LinearMap.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.Bijective.{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₃)
hf₀ : Function.Injective.{u_2 + 1, u_3 + 1} (α := M₁) (β := M₂) (⇑f₁ : (a : M₁) → M₂)
hg₀ : Function.Injective.{u_7 + 1, u_8 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
⊢ Function.Bijective.{u_2 + 1, u_7 + 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: congrArg, id, And.right, And.left, And.intro, Function.Bijective, Eq.symm, DFunLike.coe, LinearMap.surjective_of_surjective_of_injective_of_left_exact, 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_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₃)

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: And.left, LinearMap.injective_of_surjective_of_injective_of_right_exact, And.intro, Function.Bijective
-- 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.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₃)
refine : ∀ (y : N₃), ∃ (a : M₃), (i₃ : (a : M₃) → N₃) a = y
⊢ Function.Bijective.{u_4 + 1, u_9 + 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:
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₃
obtain : ∀ (y : N₂), ∃ (a : M₃), Eq.{u_9 + 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:
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₂
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₃)
⊢ ∃ (a : M₃), Eq.{u_9 + 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:
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 : 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:
⟨f₂ y, congr($hc₂ y).symm⟩

Premises used: congrArg, id, Exists.intro, Eq.symm, DFunLike.coe
-- 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.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 : 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:
exact ⟨f₂ y, congr($hc₂ y).symm⟩
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x y : FreeMagma α
⊢ x.mul y = x * y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Mul β
f g : MulHom.{u, v} (FreeMagma α) β
h : Eq (α := α → β) ((⇑f : (a : FreeMagma α) → β) ∘ of) ((⇑g : (a : FreeMagma α) → β) ∘ of)
x x_1 y : FreeMagma α
h_1 : Eq.{v + 1} (α := β) ((f : (a : FreeMagma α) → β) x_1 : β) ((g : (a : FreeMagma α) → β) x_1 : β)
h_2 : Eq.{v + 1} (α := β) ((f : (a : FreeMagma α) → β) y : β) ((g : (a : FreeMagma α) → β) y : β)
⊢ Eq.{v + 1} (α := β) ((f : (a : FreeMagma α) → β) (x_1 * y) : β) ((g : (a : FreeMagma α) → β) (x_1 * y) : β)

Tactic:
simp only [map_mul, *]

Premises used: map_mul
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Mul β
f : α → β
x : α
⊢ (((lift : (a : α → β) → FreeMagma α →ₙ* β) f : MulHom.{u, v} (FreeMagma α) β) : (a : FreeMagma α) → β) (of x) = f x

Tactic:
rfl

Premises used: FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Mul β
f : α → β
⊢ (⇑((lift : (a : α → β) → FreeMagma α →ₙ* β) f : MulHom.{u, v} (FreeMagma α) β) : (a : FreeMagma α) → β) ∘ of = f

Tactic:
rfl

Premises used: FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Mul β
f : MulHom.{u, v} (FreeMagma α) β
⊢ (lift : (a : α → β) → FreeMagma α →ₙ* β) ((⇑f : (a : FreeMagma α) → β) ∘ of) = f

Tactic:
lift.apply_symm_apply f

Premises used: FreeMagma.lift, Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
f : α → β
x : α
⊢ (map f : (a : FreeMagma α) → FreeMagma β) (of x) = of (f x)

Tactic:
rfl

Premises used: FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f : α → β
x : α
⊢ Eq (α := FreeMagma β) (f <$> pure x) (pure (f x))

Tactic:
rfl

Premises used: FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f : α → β
x y : FreeMagma α
⊢ f <$> (x * y) = f <$> x * f <$> y

Tactic:
rfl

Premises used: FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f : α → FreeMagma β
x : α
⊢ pure x >>= f = f x

Tactic:
rfl

Premises used: FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f : α → FreeMagma β
x y : FreeMagma α
⊢ x * y >>= f = (x >>= f) * (y >>= f)

Tactic:
rfl

Premises used: FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f : α → β
x : FreeMagma α
⊢ pure f <*> x = f <$> x

Tactic:
rfl

Premises used: FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f g : FreeMagma (α → β)
x : FreeMagma α
⊢ f * g <*> x = (f <*> x) * (g <*> x)

Tactic:
rfl

Premises used: FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
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
rw₂ rw₃ : x * y = x * y
⊢ id <$> (x * y) = x * y

Tactic:
rw [map_mul', ih1, ih2]

Premises used: FreeMagma.map_mul'
-- Module: Mathlib.Algebra.Free
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)
rw₄ 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)
⊢ x * y >>= f >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rw [mul_bind, mul_bind, mul_bind, ih1, ih2]

Premises used: FreeMagma.mul_bind
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
x : α
⊢ Eq (α := m (FreeMagma β)) (traverse F (pure x)) (pure <$> F x)

Tactic:
rfl

Premises used: FreeMagma.traverse, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
⊢ Eq (α := α → m (FreeMagma β)) (traverse F ∘ pure) fun (x : α) ↦ pure <$> F x

Tactic:
rfl

Premises used: FreeMagma.traverse, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
x y : FreeMagma α
⊢ traverse F (x * y) = (fun (x1 x2 : FreeMagma β) ↦ x1 * x2) <$> traverse F x <*> traverse F y

Tactic:
rfl

Premises used: FreeMagma.traverse, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
⊢ Eq (α := FreeMagma α → FreeMagma α → m (FreeMagma β)) (Function.comp (traverse F) ∘ HMul.hMul)
    fun (x y : FreeMagma α) ↦ (fun (x1 x2 : FreeMagma β) ↦ x1 * x2) <$> traverse F x <*> traverse F y

Tactic:
rfl

Premises used: FreeMagma.traverse, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
x : FreeMagma α
⊢ FreeMagma.traverse F x = traverse F x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Free
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))
rw₂ : Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x <*> pure y) (pure (x * y))
rw₃ :
  Eq (α := Id (FreeMagma α_1))
    ((fun (h : FreeMagma α_1 → FreeMagma α_1) ↦ h y) <$> (fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x)
    (pure (x * y))
rw₄ :
  Eq (α := Id (FreeMagma α_1))
    ((fun (h : FreeMagma α_1 → FreeMagma α_1) ↦ h y) <$> pure fun (x2 : FreeMagma α_1) ↦ x * x2) (pure (x * y))
rw₅ rw₆ : Eq (α := Id (FreeMagma α_1)) (pure ((fun (x2 : FreeMagma α_1) ↦ x * x2) y)) (pure (x * y))
⊢ Eq (α := Id (FreeMagma α_1)) (traverse pure (x * y)) (pure (x * y))

Tactic:
rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]

Premises used: FreeMagma.traverse_mul, LawfulApplicative.seq_pure, LawfulApplicative.map_pure
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
α_1 β_1 γ : Type u
f : β_1 → F_1 γ
g : α_1 → G β_1
x_1 : FreeMagma α_1
x : α_1
⊢ Eq (α := Functor.Comp G F_1 (FreeMagma γ)) (traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x))
    (Functor.Comp.mk (traverse f <$> traverse g (pure x)))

Tactic:
simp only [Function.comp_def, traverse_pure, functor_norm]

Premises used: Function.comp_def, FreeMagma.traverse_pure
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
α_1 β_1 γ : Type u
f : β_1 → F_1 γ
g : α_1 → G β_1
x_1 x y : FreeMagma α_1
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
rw :
  Eq (α := Functor.Comp G F_1 (FreeMagma γ))
    ((fun (x1 x2 : FreeMagma γ) ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g x) <*>
      Functor.Comp.mk (traverse f <$> traverse g y))
    (Functor.Comp.mk (traverse f <$> ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse g x <*> traverse g y)))
⊢ traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (x * y) = Functor.Comp.mk (traverse f <$> traverse g (x * y))

Tactic:
rw [traverse_mul, ih1, ih2, traverse_mul]

Premises used: FreeMagma.traverse_mul
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
α_1 β_1 γ : Type u
f : β_1 → F_1 γ
g : α_1 → G β_1
x_1 x y : FreeMagma α_1
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ Eq (α := Functor.Comp G F_1 (FreeMagma γ))
    ((fun (x1 x2 : FreeMagma γ) ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g x) <*>
      Functor.Comp.mk (traverse f <$> traverse g y))
    (Functor.Comp.mk (traverse f <$> ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse g x <*> traverse g y)))

Tactic:
simp [Functor.Comp.map_mk, Functor.map_map, Function.comp_def, Comp.seq_mk, seq_map_assoc,
            map_seq, traverse_mul]

Premises used: FreeMagma.traverse_mul, Function.comp_def, Functor.map_map, Comp.seq_mk, seq_map_assoc, Functor.Comp.map_mk, map_seq
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 β_1 : Type u
f : α_1 → β_1
x_1 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) x) (pure (f <$> x))
ih2 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeMagma β_1))
    ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) x <*> traverse (pure ∘ f) y) (pure (f <$> (x * y)))
rw₁ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (x * y)))
rw₂ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
    (pure (f <$> (x * y)))
rw₃ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
    (pure (f <$> x * f <$> y))
rw₄ :
  Eq (α := Id (FreeMagma β_1)) ((pure fun (x2 : FreeMagma β_1) ↦ f <$> x * x2) <*> pure (f <$> y))
    (pure (f <$> x * f <$> y))
rw₅ :
  Eq (α := Id (FreeMagma β_1))
    ((fun (h : FreeMagma β_1 → FreeMagma β_1) ↦ h (f <$> y)) <$> pure fun (x2 : FreeMagma β_1) ↦ f <$> x * x2)
    (pure (f <$> x * f <$> y))
rw₆ rw₇ :
  Eq (α := Id (FreeMagma β_1)) (pure ((fun (x2 : FreeMagma β_1) ↦ f <$> x * x2) (f <$> y))) (pure (f <$> x * f <$> y))
⊢ Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) (x * y)) (pure (f <$> (x * y)))

Tactic:
rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]

Premises used: FreeMagma.traverse_mul, FreeMagma.map_mul', LawfulApplicative.seq_pure, LawfulApplicative.map_pure
-- Module: Mathlib.Algebra.Free
Goal:
α_1 β_1 : Type u
m : Type u → Type u
inst : Applicative m
F : α_1 → m β_1
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α β : Type u
f : α → F_1 β
x_1 : FreeMagma α
x : α
⊢ Eq (α := G (FreeMagma β)) ((fun {α : Type u} ↦ η.app α) (traverse f (pure x)))
    (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (pure x))

Tactic:
simp only [traverse_pure, functor_norm, Function.comp_apply]

Premises used: FreeMagma.traverse_pure, Function.comp_apply