awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommMonoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x₁ x₂ : tsze R M
rw : x₁.1 •> x₂.2 + x₂.1 •> x₁.2 = x₂.1 •> x₁.2 + x₂.2 <• x₁.1
⊢ x₁.1 •> x₂.2 + x₁.2 <• x₂.1 = x₂.1 •> x₁.2 + x₂.2 <• x₁.1
have rw₁ : x₁.1 •> x₂.2 + x₂.1 •> x₁.2 = x₂.1 •> x₁.2 + x₁.1 •> x₂.2
Tactic: rw [op_smul_eq_smul, op_smul_eq_smul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommMonoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x₁ x₂ : tsze R M
rw : x₁.1 •> x₂.2 + x₂.1 •> x₁.2 = x₂.1 •> x₁.2 + x₂.2 <• x₁.1
rw₁ : x₁.1 •> x₂.2 + x₂.1 •> x₁.2 = x₂.1 •> x₁.2 + x₁.1 •> x₂.2
⊢ x₁.1 •> x₂.2 + x₁.2 <• x₂.1 = x₂.1 •> x₁.2 + x₂.2 <• x₁.1
have rw₂ : x₂.1 •> x₁.2 + x₁.1 •> x₂.2 = x₂.1 •> x₁.2 + x₁.1 •> x₂.2
Tactic: rw [op_smul_eq_smul, op_smul_eq_smul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
inst_4 : Invertible x
⊢ (@Invertible.invOf _ mul one x _).fst * x.fst = 1
have rw : (@Invertible.invOf _ mul one x _ * x).fst = 1
Tactic: rw [← fst_mul, invOf_mul_self, fst_one]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
inst_4 : Invertible x
rw : (@Invertible.invOf _ mul one x _ * x).fst = 1
⊢ (@Invertible.invOf _ mul one x _).fst * x.fst = 1
have rw₁ : Eq.{u + 1} (α := R) (fst.{u, v} (M := M) 1) 1
Tactic: rw [← fst_mul, invOf_mul_self, fst_one]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
inst_4 : Invertible x
rw : (@Invertible.invOf _ mul one x _ * x).fst = 1
rw₁ : Eq.{u + 1} (α := R) (fst.{u, v} (M := M) 1) 1
⊢ (@Invertible.invOf _ mul one x _).fst * x.fst = 1
have rw₂ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [← fst_mul, invOf_mul_self, fst_one]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
inst_4 : Invertible x
⊢ x.fst * (@Invertible.invOf _ mul one x _).fst = 1
have rw : (x * @Invertible.invOf _ mul one x _).fst = 1
Tactic: rw [← fst_mul, mul_invOf_self, fst_one]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
inst_4 : Invertible x
rw : (x * @Invertible.invOf _ mul one x _).fst = 1
⊢ x.fst * (@Invertible.invOf _ mul one x _).fst = 1
have rw₁ : Eq.{u + 1} (α := R) (fst.{u, v} (M := M) 1) 1
Tactic: rw [← fst_mul, mul_invOf_self, fst_one]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
inst_4 : Invertible x
rw : (x * @Invertible.invOf _ mul one x _).fst = 1
rw₁ : Eq.{u + 1} (α := R) (fst.{u, v} (M := M) 1) 1
⊢ x.fst * (@Invertible.invOf _ mul one x _).fst = 1
have rw₂ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [← fst_mul, mul_invOf_self, fst_one]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (inl r + inr (-(r •> x.snd <• r))) * x = 1
have h1 : ((inl r + inr (-(r •> x.snd <• r))) * x).fst = fst.{u, v} (M := M) 1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
h1 : ((inl r + inr (-(r •> x.snd <• r))) * x).fst = fst.{u, v} (M := M) 1
⊢ (inl r + inr (-(r •> x.snd <• r))) * x = 1
have h2 : ((inl r + inr (-(r •> x.snd <• r))) * x).snd = snd.{u, v} (R := R) 1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ ((inl r + inr (-(r •> x.snd <• r))) * x).fst = fst.{u, v} (M := M) 1
have h1 : (r + 0) * x.fst = 1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ ((inl r + inr (-(r •> x.snd <• r))) * x).snd = snd.{u, v} (R := R) 1
have h2 : (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h h1 : r * x.fst = 1
⊢ (r + 0) * x.fst = 1
have h1₁ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [add_zero, h]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
have h2 : r •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
Tactic: rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
h2 : r •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
have h2₁ : r •> x.snd + -(r •> x.snd <• r) <• x.fst = 0
Tactic: rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
h2 : r •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
h2₁ : r •> x.snd + -(r •> x.snd <• r) <• x.fst = 0
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
have h2₂ : r •> x.snd + -(r •> x.snd <• r <• x.fst) = 0
Tactic: rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
h2 : r •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
h2₁ : r •> x.snd + -(r •> x.snd <• r) <• x.fst = 0
h2₂ : r •> x.snd + -(r •> x.snd <• r <• x.fst) = 0
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
have h2₃ : r •> x.snd + -(r •> x.snd <• (r * x.fst)) = 0
Tactic: rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
h2 : r •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
h2₁ : r •> x.snd + -(r •> x.snd <• r) <• x.fst = 0
h2₂ : r •> x.snd + -(r •> x.snd <• r <• x.fst) = 0
h2₃ : r •> x.snd + -(r •> x.snd <• (r * x.fst)) = 0
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
have h2₄ : r •> x.snd + -(r •> x.snd <• 1) = 0
Tactic: rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
h2 : r •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
h2₁ : r •> x.snd + -(r •> x.snd <• r) <• x.fst = 0
h2₂ : r •> x.snd + -(r •> x.snd <• r <• x.fst) = 0
h2₃ : r •> x.snd + -(r •> x.snd <• (r * x.fst)) = 0
h2₄ : r •> x.snd + -(r •> x.snd <• 1) = 0
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
have h2₅ : r •> x.snd + -(1 •> r •> x.snd) = 0
Tactic: rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
h2 : r •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
h2₁ : r •> x.snd + -(r •> x.snd <• r) <• x.fst = 0
h2₂ : r •> x.snd + -(r •> x.snd <• r <• x.fst) = 0
h2₃ : r •> x.snd + -(r •> x.snd <• (r * x.fst)) = 0
h2₄ : r •> x.snd + -(r •> x.snd <• 1) = 0
h2₅ : r •> x.snd + -(1 •> r •> x.snd) = 0
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
have h2₆ : r •> x.snd + -(r •> x.snd) = 0
Tactic: rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
h2 : r •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
h2₁ : r •> x.snd + -(r •> x.snd <• r) <• x.fst = 0
h2₂ : r •> x.snd + -(r •> x.snd <• r <• x.fst) = 0
h2₃ : r •> x.snd + -(r •> x.snd <• (r * x.fst)) = 0
h2₄ : r •> x.snd + -(r •> x.snd <• 1) = 0
h2₅ : r •> x.snd + -(1 •> r •> x.snd) = 0
h2₆ : r •> x.snd + -(r •> x.snd) = 0
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
have h2₇ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x * (inl r + inr (-(r •> (x.snd <• r)))) = 1
have h1 : (x * (inl r + inr (-(r •> (x.snd <• r))))).fst = fst.{u, v} (M := M) 1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
h1 : (x * (inl r + inr (-(r •> (x.snd <• r))))).fst = fst.{u, v} (M := M) 1
⊢ x * (inl r + inr (-(r •> (x.snd <• r)))) = 1
have h2 : (x * (inl r + inr (-(r •> (x.snd <• r))))).snd = snd.{u, v} (R := R) 1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ (x * (inl r + inr (-(r •> (x.snd <• r))))).fst = fst.{u, v} (M := M) 1
have h1 : x.fst * (r + 0) = 1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ (x * (inl r + inr (-(r •> (x.snd <• r))))).snd = snd.{u, v} (R := R) 1
have h2 : x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h h1 : x.fst * r = 1
⊢ x.fst * (r + 0) = 1
have h1₁ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [add_zero, h]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0
have h2 : x.fst •> (0 + -(r •> (x.snd <• r))) + x.snd <• r = 0
Tactic: rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
h2 : x.fst •> (0 + -(r •> (x.snd <• r))) + x.snd <• r = 0
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0
have h2₁ : x.fst •> -(r •> (x.snd <• r)) + x.snd <• r = 0
Tactic: rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
h2 : x.fst •> (0 + -(r •> (x.snd <• r))) + x.snd <• r = 0
h2₁ : x.fst •> -(r •> (x.snd <• r)) + x.snd <• r = 0
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0
have h2₂ : -(x.fst •> r •> (x.snd <• r)) + x.snd <• r = 0
Tactic: rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
h2 : x.fst •> (0 + -(r •> (x.snd <• r))) + x.snd <• r = 0
h2₁ : x.fst •> -(r •> (x.snd <• r)) + x.snd <• r = 0
h2₂ : -(x.fst •> r •> (x.snd <• r)) + x.snd <• r = 0
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0
have h2₃ : -((x.fst * r) •> (x.snd <• r)) + x.snd <• r = 0
Tactic: rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
h2 : x.fst •> (0 + -(r •> (x.snd <• r))) + x.snd <• r = 0
h2₁ : x.fst •> -(r •> (x.snd <• r)) + x.snd <• r = 0
h2₂ : -(x.fst •> r •> (x.snd <• r)) + x.snd <• r = 0
h2₃ : -((x.fst * r) •> (x.snd <• r)) + x.snd <• r = 0
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0
have h2₄ : -(1 •> (x.snd <• r)) + x.snd <• r = 0
Tactic: rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
h2 : x.fst •> (0 + -(r •> (x.snd <• r))) + x.snd <• r = 0
h2₁ : x.fst •> -(r •> (x.snd <• r)) + x.snd <• r = 0
h2₂ : -(x.fst •> r •> (x.snd <• r)) + x.snd <• r = 0
h2₃ : -((x.fst * r) •> (x.snd <• r)) + x.snd <• r = 0
h2₄ : -(1 •> (x.snd <• r)) + x.snd <• r = 0
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0
have h2₅ : -(x.snd <• r) + x.snd <• r = 0
Tactic: rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
h2 : x.fst •> (0 + -(r •> (x.snd <• r))) + x.snd <• r = 0
h2₁ : x.fst •> -(r •> (x.snd <• r)) + x.snd <• r = 0
h2₂ : -(x.fst •> r •> (x.snd <• r)) + x.snd <• r = 0
h2₃ : -((x.fst * r) •> (x.snd <• r)) + x.snd <• r = 0
h2₄ : -(1 •> (x.snd <• r)) + x.snd <• r = 0
h2₅ : -(x.snd <• r) + x.snd <• r = 0
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0
have h2₆ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst_5 : Invertible x.fst
⊢ (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
        -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) *
      x =
    1
have h : (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
    -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) =
  inl (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) +
    inr
      (-(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _))
Tactic: convert! mul_left_eq_one _ _ (invOf_mul_self x.fst)
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst_5 : Invertible x.fst
⊢ (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
      -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) =
    inl (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) +
      inr
        (-(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _))
have h : fst
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
      -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) =
  (inl (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) +
      inr
        (-(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _))).fst
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst_5 : Invertible x.fst
h :
  fst
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
        -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) =
    (inl (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) +
        inr
          (-(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
              @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _))).fst
⊢ (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
      -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) =
    inl (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) +
      inr
        (-(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _))
have h₁ : snd
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
      -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) =
  (inl (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) +
      inr
        (-(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _))).snd
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst_5 : Invertible x.fst
⊢ x *
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
        -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) =
    1
have h : (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
    -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) =
  inl (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) +
    inr
      (-(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •>
          (x.snd <• @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)))
Tactic: convert! mul_right_eq_one _ _ (mul_invOf_self x.fst)
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddCommGroup M
inst_1 : Semiring R
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst_5 : Invertible x.fst
⊢ (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
      -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) =
    inl (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) +
      inr
        (-(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •>
            (x.snd <• @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)))
have h : fst
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _,
      -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)) =
  (inl (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) +
      inr
        (-(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •>
            (x.snd <• @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)))).fst
Tactic: ext