awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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)
refine_1 :
  ∀ (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }),
    Bijective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
refine_2 :
  ∀ (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }),
    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)
⊢ { 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) }
have refine_3 : ∀ (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) }),
  (fst R M P ∘ₗ (↑(↑e : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ∘ₗ f = LinearMap.id
Tactic: refine
  { toFun := fun l ↦ ⟨(LinearEquiv.ofBijective (l.1.prod g) ?_), ?_⟩
    invFun := fun e ↦ ⟨fst R M P ∘ₗ e.1, ?_⟩
    left_inv := ?_
    right_inv := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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)
refine_1 :
  ∀ (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }),
    Bijective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
refine_2 :
  ∀ (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }),
    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)
refine_3 :
  ∀ (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) }),
    (fst R M P ∘ₗ (↑(↑e : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ∘ₗ f = LinearMap.id
⊢ { 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) }
have refine_4 : LeftInverse
  (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))
      sorry)
  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) sorry) sorry
Tactic: refine
  { toFun := fun l ↦ ⟨(LinearEquiv.ofBijective (l.1.prod g) ?_), ?_⟩
    invFun := fun e ↦ ⟨fst R M P ∘ₗ e.1, ?_⟩
    left_inv := ?_
    right_inv := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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)
refine_1 :
  ∀ (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }),
    Bijective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
refine_2 :
  ∀ (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }),
    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)
refine_3 :
  ∀ (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) }),
    (fst R M P ∘ₗ (↑(↑e : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ∘ₗ f = LinearMap.id
refine_4 :
  LeftInverse
    (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)) ⋯)
    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) ⋯) ⋯
⊢ { 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) }
have refine_5 : RightInverse
  (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))
      sorry)
  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) sorry) sorry
Tactic: refine
  { toFun := fun l ↦ ⟨(LinearEquiv.ofBijective (l.1.prod g) ?_), ?_⟩
    invFun := fun e ↦ ⟨fst R M P ∘ₗ e.1, ?_⟩
    left_inv := ?_
    right_inv := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
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 }
⊢ Bijective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
have h₁ : ∀ (x : M), ((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) x : N) = x
Tactic: have h₁ : ∀ x, l.1 (f x) = x := LinearMap.congr_fun l.2
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
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
⊢ Bijective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
have h₂ : ∀ (x : M), Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
Tactic: have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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)
⊢ Bijective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
have refine_1 : Injective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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_1 : Injective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
⊢ Bijective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
have refine_1₁ : Surjective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
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 y : N
e :
  Eq (α := M × P) (((↑l : N →ₗ[R] M).prod g : (a : N) → M × P) x : M × P)
    (((↑l : N →ₗ[R] M).prod g : (a : N) → M × P) y : M × P)
⊢ x = y
have e₁ : Eq.{u_9 + 1} (α := M) (((↑l : N →ₗ[R] M) : (a : N) → M) x : M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M) ∧
  Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) x : P) ((g : (a : N) → P) y : P)
Tactic: simp only [LinearMap.prod_apply, Function.prod_apply, Prod.mk.injEq] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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 y : N
e :
  Eq.{u_9 + 1} (α := M) (((↑l : N →ₗ[R] M) : (a : N) → M) x : M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M) ∧
    Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) x : P) ((g : (a : N) → P) y : P)
⊢ x = y
have refine_1 : ∀ (z : M) (hz : (f : (a : M) → N) z = x - y), x = y
Tactic: obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2)
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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 y : N
e :
  Eq.{u_9 + 1} (α := M) (((↑l : N →ₗ[R] M) : (a : N) → M) x : M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M) ∧
    Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) x : P) ((g : (a : N) → P) y : P)
z : M
hz : (f : (a : M) → N) z = x - y
⊢ x = y
have refine_1 : x - y = 0
Tactic: rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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 y : N
e :
  Eq.{u_9 + 1} (α := M) (((↑l : N →ₗ[R] M) : (a : N) → M) x : M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M) ∧
    Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) x : P) ((g : (a : N) → P) y : P)
z : M
hz : (f : (a : M) → N) z = x - y
refine_1 : x - y = 0
⊢ x = y
have refine_1₁ : Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) z : N) (0 : N)
Tactic: rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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 y : N
e :
  Eq.{u_9 + 1} (α := M) (((↑l : N →ₗ[R] M) : (a : N) → M) x : M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M) ∧
    Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) x : P) ((g : (a : N) → P) y : P)
z : M
hz : (f : (a : M) → N) z = x - y
refine_1 : x - y = 0
refine_1₁ : Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) z : N) (0 : N)
⊢ x = y
have refine_1₂ : Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) (((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) z : N) : M) : N) (0 : N)
Tactic: rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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 y : N
e :
  Eq.{u_9 + 1} (α := M) (((↑l : N →ₗ[R] M) : (a : N) → M) x : M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M) ∧
    Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) x : P) ((g : (a : N) → P) y : P)
z : M
hz : (f : (a : M) → N) z = x - y
refine_1 : x - y = 0
refine_1₁ : Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) z : N) (0 : N)
refine_1₂ :
  Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) (((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) z : N) : M) : N)
    (0 : N)
⊢ x = y
have refine_1₃ : Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) (((↑l : N →ₗ[R] M) : (a : N) → M) (x - y) : M) : N) (0 : N)
Tactic: rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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 y : N
e :
  Eq.{u_9 + 1} (α := M) (((↑l : N →ₗ[R] M) : (a : N) → M) x : M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M) ∧
    Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) x : P) ((g : (a : N) → P) y : P)
z : M
hz : (f : (a : M) → N) z = x - y
refine_1 : x - y = 0
refine_1₁ : Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) z : N) (0 : N)
refine_1₂ :
  Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) (((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) z : N) : M) : N)
    (0 : N)
refine_1₃ : Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) (((↑l : N →ₗ[R] M) : (a : N) → M) (x - y) : M) : N) (0 : N)
⊢ x = y
have refine_1₄ : Eq.{u_10 + 1} (α := N)
  ((f : (a : M) → N)
      (HSub.hSub (α := M) (β := M) (((↑l : N →ₗ[R] M) : (a : N) → M) x : M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M)) :
    N)
  (0 : N)
Tactic: rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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 y : N
e :
  Eq.{u_9 + 1} (α := M) (((↑l : N →ₗ[R] M) : (a : N) → M) x : M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M) ∧
    Eq.{u_11 + 1} (α := P) ((g : (a : N) → P) x : P) ((g : (a : N) → P) y : P)
z : M
hz : (f : (a : M) → N) z = x - y
refine_1 : x - y = 0
refine_1₁ : Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) z : N) (0 : N)
refine_1₂ :
  Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) (((↑l : N →ₗ[R] M) : (a : N) → M) ((f : (a : M) → N) z : N) : M) : N)
    (0 : N)
refine_1₃ : Eq.{u_10 + 1} (α := N) ((f : (a : M) → N) (((↑l : N →ₗ[R] M) : (a : N) → M) (x - y) : M) : N) (0 : N)
refine_1₄ :
  Eq.{u_10 + 1} (α := N)
    ((f : (a : M) → N)
        (HSub.hSub (α := M) (β := M) (((↑l : N →ₗ[R] M) : (a : N) → M) x : M)
          (((↑l : N →ₗ[R] M) : (a : N) → M) y : M)) :
      N)
    (0 : N)
⊢ x = y
have refine_1₅ : Eq.{u_10 + 1} (α := N)
  ((f : (a : M) → N)
      (HSub.hSub (α := M) (β := M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M) (((↑l : N →ₗ[R] M) : (a : N) → M) y : M)) :
    N)
  (0 : N)
Tactic: rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]