awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
x : M
y : N
⊢ ∃ (a : N), Eq (α := M × P) (((↑l : N →ₗ[R] M).prod g : (a : N) → M × P) a : M × P) ((x, (g : (a : N) → P) y) : M × P)

Tactic:
refine ⟨f x + y - f (l.1 y), by ext <;> simp [h₁, h₂]⟩
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
refine_2 : f = (↑(LinearEquiv.symm (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯)) : M × P →ₗ[R] N) ∘ₗ inl R M P
refine_2₁ : g = snd R M P ∘ₗ (↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P)
⊢ f = (↑(LinearEquiv.symm (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯)) : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
    g = snd R M P ∘ₗ (↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P)

Tactic:
constructor
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
refine_2 : (↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P) ∘ₗ f = inl R M P
⊢ f = (↑(LinearEquiv.symm (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯)) : M × P →ₗ[R] N) ∘ₗ inl R M P

Tactic:
rw [LinearEquiv.eq_toLinearMap_symm_comp]

Premises used: LinearEquiv.eq_toLinearMap_symm_comp
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
refine_2 :
  ∀ (x : M),
    Eq.{u_9 + 1} (α := M)
      (((↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P) ∘ₗ f : (a : M) → M × P) x).1
      ((inl R M P : (a : M) → M × P) x).1
refine_2₁ :
  ∀ (x : M),
    Eq.{u_11 + 1} (α := P)
      (((↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P) ∘ₗ f : (a : M) → M × P) x).2
      ((inl R M P : (a : M) → M × P) x).2
⊢ (↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P) ∘ₗ f = inl R M P

Tactic:
ext
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
x : M
⊢ Eq.{u_9 + 1} (α := M)
    (((↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P) ∘ₗ f : (a : M) → M × P) x).1
    ((inl R M P : (a : M) → M × P) x).1

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
x : M
⊢ Eq.{u_11 + 1} (α := P)
    (((↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P) ∘ₗ f : (a : M) → M × P) x).2
    ((inl R M P : (a : M) → M × P) x).2

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
refine_2 :
  ∀ (x : N),
    Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) x : P)
      ((snd R M P ∘ₗ (↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P) : (a : N) → P) x : P)
⊢ g = snd R M P ∘ₗ (↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P)

Tactic:
ext
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
x : N
⊢ Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) x : P)
    ((snd R M P ∘ₗ (↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) : N →ₗ[R] M × P) : (a : N) → P) x : P)

Tactic:
simp
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
e : { 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) }
refine_3 : Eq (α := M →ₗ[R] M) (fst R M P ∘ₗ inl R M P) LinearMap.id
⊢ (fst R M P ∘ₗ (↑(↑e : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ∘ₗ f = LinearMap.id

Tactic:
rw [LinearMap.comp_assoc, (LinearEquiv.eq_toLinearMap_symm_comp _ _).mp e.2.1]

Premises used: LinearMap.comp_assoc, LinearEquiv.eq_toLinearMap_symm_comp, And.left, Iff.mp, Subtype.property
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
e : { 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) }
⊢ Eq (α := M →ₗ[R] M) (fst R M P ∘ₗ inl R M P) LinearMap.id

Tactic:
rfl
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }
refine_4 :
  ∀ (x_1 : N),
    Eq.{u_9 + 1} (α := M)
      (((↑((fun
                      (e :
                        { 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) }) ↦
                    (Subtype.mk (p := fun (l : N →ₗ[R] M) ↦ l ∘ₗ f = LinearMap.id)
                        (fst R M P ∘ₗ (↑(↑e : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ⋯ :
                      { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }))
                  ((fun (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }) ↦
                      (Subtype.mk (p := fun (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))
                          (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) ⋯ :
                        { 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) }))
                    x)) :
              N →ₗ[R] M) :
            (a : N) → M)
          x_1 :
        M)
      (((↑x : N →ₗ[R] M) : (a : N) → M) x_1 : M)
⊢ (fun
          (e :
            { 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) }) ↦
        (Subtype.mk (p := fun (l : N →ₗ[R] M) ↦ l ∘ₗ f = LinearMap.id)
            (fst R M P ∘ₗ (↑(↑e : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ⋯ :
          { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }))
      ((fun (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }) ↦
          (Subtype.mk (p := fun (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))
              (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) ⋯ :
            { 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) }))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }
x_1 : N
⊢ Eq.{u_9 + 1} (α := M)
    (((↑((fun
                    (e :
                      { 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) }) ↦
                  (Subtype.mk (p := fun (l : N →ₗ[R] M) ↦ l ∘ₗ f = LinearMap.id)
                      (fst R M P ∘ₗ (↑(↑e : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ⋯ :
                    { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }))
                ((fun (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }) ↦
                    (Subtype.mk (p := fun (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))
                        (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) ⋯) ⋯ :
                      { 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) }))
                  x)) :
            N →ₗ[R] M) :
          (a : N) → M)
        x_1 :
      M)
    (((↑x : N →ₗ[R] M) : (a : N) → M) x_1 : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f : M_1 →ₗ[R_1] N_1
g : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
e : N ≃ₗ[R] M × P
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑(snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
h :
  Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P) : (a : M) → N)
    (⇑(snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
x : N
⊢ Eq.{u_9 + 1} (α := M)
    (((↑((fun (l : { l : N →ₗ[R] M // l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id }) ↦
                  (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                      (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                        snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                      (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P))) ⋯) ⋯ :
                    { e_1 : N ≃ₗ[R] M × P //
                      (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                        snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) }))
                ((fun
                      (e_1 :
                        { e_1 : N ≃ₗ[R] M × P //
                          (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                            snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) }) ↦
                    (Subtype.mk (p := fun (l : N →ₗ[R] M) ↦ l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id)
                        (fst R M P ∘ₗ (↑(↑e_1 : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ⋯ :
                      { l : N →ₗ[R] M // l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id }))
                  (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                    (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                      snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                    e ⋯))) :
            N ≃ₗ[R] M × P) :
          (a : N) → M × P)
        x).1
    (((↑(Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                  snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                e ⋯) :
            N ≃ₗ[R] M × P) :
          (a : N) → M × P)
        x).1

Tactic:
simp
-- Module: Mathlib.Algebra.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f : M_1 →ₗ[R_1] N_1
g : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
e : N ≃ₗ[R] M × P
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑(snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
h :
  Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P) : (a : M) → N)
    (⇑(snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
x : N
⊢ Eq.{u_11 + 1} (α := P)
    (((↑((fun (l : { l : N →ₗ[R] M // l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id }) ↦
                  (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                      (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                        snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                      (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P))) ⋯) ⋯ :
                    { e_1 : N ≃ₗ[R] M × P //
                      (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                        snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) }))
                ((fun
                      (e_1 :
                        { e_1 : N ≃ₗ[R] M × P //
                          (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                            snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) }) ↦
                    (Subtype.mk (p := fun (l : N →ₗ[R] M) ↦ l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id)
                        (fst R M P ∘ₗ (↑(↑e_1 : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ⋯ :
                      { l : N →ₗ[R] M // l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id }))
                  (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                    (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                      snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                    e ⋯))) :
            N ≃ₗ[R] M × P) :
          (a : N) → M × P)
        x).2
    (((↑(Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                  snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                e ⋯) :
            N ≃ₗ[R] M × P) :
          (a : N) → M × P)
        x).2

Tactic:
simp
-- 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)
⊢ 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)
⊢ ∃ (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