awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
⊢ ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)

Tactic:
1 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
⊢ ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)

Tactic:
tfae_have 1 → 3
  | ⟨hf, l, hl⟩ => ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
⊢ Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
⊢ ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
⊢ ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
⊢ ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)

Tactic:
tfae_have 2 → 3
  | ⟨hg, l, hl⟩ => ⟨_, (h.splitInjectiveEquiv hg ⟨l, hl⟩).2⟩
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
⊢ ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
⊢ Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
⊢ ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
e : N ≃ₗ[R] M × P
e₁ : f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
⊢ Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
e : N ≃ₗ[R] M × P
e₁ : f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
this : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id

Tactic:
⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩

Premises used: Subtype.mk, And.intro, Exists.intro, Equiv.symm, Function.Exact.splitSurjectiveEquiv, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
e : N ≃ₗ[R] M × P
e₁ : f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
this : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id

Tactic:
exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
⊢ ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id

Tactic:
tfae_have 3 → 1
  | ⟨e, e₁, e₂⟩ => by
    have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective
    exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_3_to_1 :
  ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id
⊢ ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_3_to_1 :
  ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id
⊢ Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_3_to_1 :
  ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id
⊢ ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id

Tactic:
3 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_3_to_1 :
  ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id
e : N ≃ₗ[R] M × P
e₁ : f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
⊢ Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)

Tactic:
have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_3_to_1 :
  ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id
e : N ≃ₗ[R] M × P
e₁ : f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
this : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id

Tactic:
⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩

Premises used: Subtype.mk, And.intro, Exists.intro, Equiv.symm, Function.Exact.splitInjectiveEquiv, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_3_to_1 :
  ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id
e : N ≃ₗ[R] M × P
e₁ : f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
this : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id

Tactic:
exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id),
    ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)
tfae_3_to_1 :
  ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id
⊢ ∀ (a : ∃ (e : N ≃ₗ[R] M × P), f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)),
    Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id

Tactic:
tfae_have 3 → 2
  | ⟨e, e₁, e₂⟩ => by
    have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective
    exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩