awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
m : M
simp_rw : IsUnit.{u} (M := R) (fst (inr m)) ↔ Subsingleton R
simp_rw₁ : IsUnit.{u} (M := R) 0 ↔ Subsingleton R
simp_rw₂ : Eq.{u + 1} (α := R) 0 1 ↔ Subsingleton R
⊢ IsUnit (M := tsze R M) (inr m) ↔ Subsingleton R

Tactic:
simp_rw [isUnit_iff_isUnit_fst, fst_inr, isUnit_zero_iff, subsingleton_iff_zero_eq_one]

Premises used: TrivSqZeroExt.fst_inr, isUnit_zero_iff, subsingleton_iff_zero_eq_one, TrivSqZeroExt.isUnit_iff_isUnit_fst
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
h1 : fst.{u, v} (M := M) (inl r)⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
h2 : Eq.{v + 1} (α := M) (snd (inl r)⁻¹) (snd (inl r⁻¹))
⊢ Eq (α := tsze R M) (inl r)⁻¹ (inl r⁻¹)

Tactic:
ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
h1 : (fst.{u, v} (M := M) (inl r))⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
h1₁ : r⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
h1₂ h1₃ : r⁻¹ = r⁻¹
⊢ fst.{u, v} (M := M) (inl r)⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)

Tactic:
rw [fst_inv, fst_inl, fst_inl]

Premises used: TrivSqZeroExt.fst_inv, TrivSqZeroExt.fst_inl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
r : R
h2 : -((fst.{u, v} (M := M) (inl r))⁻¹ •> snd (inl r) <• (fst.{u, v} (M := M) (inl r))⁻¹) = snd (inl r⁻¹)
h2₁ : -(r⁻¹ •> snd (inl r) <• r⁻¹) = snd (inl r⁻¹)
h2₂ : -(r⁻¹ •> 0 <• r⁻¹) = snd (inl r⁻¹)
h2₃ : -(r⁻¹ •> 0 <• r⁻¹) = 0
h2₄ : -(0 <• r⁻¹) = 0
h2₅ : Eq.{v + 1} (α := M) (-0) 0
h2₆ h2₇ : Eq.{v + 1} (α := M) 0 0
⊢ Eq.{v + 1} (α := M) (snd (inl r)⁻¹) (snd (inl r⁻¹))

Tactic:
rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_zero]

Premises used: smul_zero, TrivSqZeroExt.snd_inv, TrivSqZeroExt.snd_inl, TrivSqZeroExt.fst_inl, neg_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
m : M
h1 : Eq.{u + 1} (α := R) (fst (inr m)⁻¹) (fst.{u, v} (M := M) 0)
h2 : snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0
⊢ Eq (α := tsze R M) (inr m)⁻¹ 0

Tactic:
ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
m : M
h1 : Eq.{u + 1} (α := R) (fst (inr m))⁻¹ (fst.{u, v} (M := M) 0)
h1₁ : Eq.{u + 1} (α := R) 0⁻¹ (fst.{u, v} (M := M) 0)
h1₂ : Eq.{u + 1} (α := R) 0⁻¹ 0
h1₃ h1₄ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) (fst (inr m)⁻¹) (fst.{u, v} (M := M) 0)

Tactic:
rw [fst_inv, fst_inr, fst_zero, inv_zero]

Premises used: inv_zero, TrivSqZeroExt.fst_inr, TrivSqZeroExt.fst_inv, TrivSqZeroExt.fst_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
m : M
h2 : -((fst (inr m))⁻¹ •> snd.{u, v} (R := R) (inr m) <• (fst (inr m))⁻¹) = snd.{u, v} (R := R) 0
h2₁ : -((fst (inr m))⁻¹ •> m <• (fst (inr m))⁻¹) = snd.{u, v} (R := R) 0
h2₂ : -(0⁻¹ •> m <• 0⁻¹) = snd.{u, v} (R := R) 0
h2₃ : -(0 •> m <• 0) = snd.{u, v} (R := R) 0
h2₄ : -(0 •> 0 •> m) = snd.{u, v} (R := R) 0
h2₅ : Eq.{v + 1} (α := M) (-0) (snd.{u, v} (R := R) 0)
h2₆ : Eq.{v + 1} (α := M) (-0) 0
h2₇ h2₈ : Eq.{v + 1} (α := M) 0 0
⊢ snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0

Tactic:
rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_zero]

Premises used: TrivSqZeroExt.snd_inr, inv_zero, TrivSqZeroExt.fst_inr, MulOpposite.op_zero, TrivSqZeroExt.snd_inv, zero_smul, neg_zero, TrivSqZeroExt.snd_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
rw : Eq (α := tsze R M) (inl 0)⁻¹ (inl 0)
rw₁ : Eq (α := tsze R M) (inl 0⁻¹) (inl 0)
rw₂ rw₃ : Eq (α := tsze R M) (inl 0) (inl 0)
⊢ Eq (α := tsze R M) 0⁻¹ 0

Tactic:
rw [← inl_zero, TrivSqZeroExt.inv_inl, inv_zero]

Premises used: TrivSqZeroExt.inv_inl, inv_zero, TrivSqZeroExt.inl_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
rw : Eq (α := tsze R M) (inl 1)⁻¹ (inl 1)
rw₁ : Eq (α := tsze R M) (inl 1⁻¹) (inl 1)
rw₂ rw₃ : Eq (α := tsze R M) (inl 1) (inl 1)
⊢ Eq (α := tsze R M) 1⁻¹ 1

Tactic:
rw [← inl_one, TrivSqZeroExt.inv_inl, inv_one]

Premises used: TrivSqZeroExt.inv_inl, inv_one, TrivSqZeroExt.inl_one
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))) * x = 1

Tactic:
mul_left_eq_one _ _ (_root_.inv_mul_cancel₀ hx)

Premises used: TrivSqZeroExt.mul_left_eq_one, inv_mul_cancel₀
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
hx : x.fst ≠ 0
h : x⁻¹ = inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))
⊢ x⁻¹ * x = 1

Tactic:
convert! mul_left_eq_one _ _ (_root_.inv_mul_cancel₀ hx) using 2

Premises used: TrivSqZeroExt.mul_left_eq_one, inv_mul_cancel₀
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
hx : x.fst ≠ 0
h : x⁻¹.fst = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).fst
h₁ : x⁻¹.snd = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).snd
⊢ x⁻¹ = inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))

Tactic:
ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.fst = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).fst

Tactic:
simp
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.snd = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).snd

Tactic:
simp
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
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
this : Invertible x.fst := x.invertibleFstOfInvertible
h1 : (@Invertible.invOf _ mul one x _).fst = x⁻¹.fst
h2 : (@Invertible.invOf _ mul one x _).snd = x⁻¹.snd
⊢ @Invertible.invOf _ mul one x _ = x⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
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
this : Invertible x.fst := x.invertibleFstOfInvertible
⊢ (@Invertible.invOf _ mul one x _).fst = x⁻¹.fst

Tactic:
simp [fst_invOf, snd_invOf]

Premises used: TrivSqZeroExt.fst_invOf, TrivSqZeroExt.snd_invOf
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
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
this : Invertible x.fst := x.invertibleFstOfInvertible
⊢ (@Invertible.invOf _ mul one x _).snd = x⁻¹.snd

Tactic:
simp [fst_invOf, snd_invOf]

Premises used: TrivSqZeroExt.fst_invOf, TrivSqZeroExt.snd_invOf
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
have : ∀ (this : Invertible x.fst), x * x⁻¹ = 1
⊢ x * x⁻¹ = 1

Tactic:
have : Invertible x.fst := Units.invertible (.mk0 _ hx)
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
this : Invertible x.fst
have : ∀ (this : Invertible x), x * x⁻¹ = 1
⊢ x * x⁻¹ = 1

Tactic:
have := invertibleOfInvertibleFst x
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
this_1 : Invertible x.fst
this : Invertible x
rw : x * @Invertible.invOf _ mul one x _ = 1
rw₁ rw₂ : Eq (α := tsze R M) 1 1
⊢ x * x⁻¹ = 1

Tactic:
rw [← invOf_eq_inv, mul_invOf_self]

Premises used: mul_invOf_self, TrivSqZeroExt.invOf_eq_inv
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
h1 : (a * b)⁻¹.fst = (b⁻¹ * a⁻¹).fst
h2 : (a * b)⁻¹.snd = (b⁻¹ * a⁻¹).snd
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
h1 : (a * b).fst⁻¹ = (b⁻¹ * a⁻¹).fst
h1₁ : (a.fst * b.fst)⁻¹ = (b⁻¹ * a⁻¹).fst
h1₂ : (a.fst * b.fst)⁻¹ = b⁻¹.fst * a⁻¹.fst
h1₃ : b.fst⁻¹ * a.fst⁻¹ = b⁻¹.fst * a⁻¹.fst
h1₄ : b.fst⁻¹ * a.fst⁻¹ = b.fst⁻¹ * a⁻¹.fst
h1₅ h1₆ : b.fst⁻¹ * a.fst⁻¹ = b.fst⁻¹ * a.fst⁻¹
⊢ (a * b)⁻¹.fst = (b⁻¹ * a⁻¹).fst

Tactic:
rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]

Premises used: TrivSqZeroExt.fst_inv, mul_inv_rev, TrivSqZeroExt.fst_mul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
h2 :
  -((a.fst * b.fst)⁻¹ •> (a.fst •> b.snd + a.snd <• b.fst) <• (a.fst * b.fst)⁻¹) =
    b.fst⁻¹ •> -(a.fst⁻¹ •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• b.fst⁻¹) <• a.fst⁻¹
⊢ (a * b)⁻¹.snd = (b⁻¹ * a⁻¹).snd

Tactic:
simp only [snd_inv, snd_mul, fst_mul, fst_inv]

Premises used: TrivSqZeroExt.snd_inv, TrivSqZeroExt.fst_inv, TrivSqZeroExt.snd_mul, TrivSqZeroExt.fst_mul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
h2 :
  -((a.fst * b.fst)⁻¹ •> a.fst •> b.snd <• (a.fst * b.fst)⁻¹ +
        (a.fst * b.fst)⁻¹ •> (a.snd <• b.fst) <• (a.fst * b.fst)⁻¹) =
    -(b.fst⁻¹ •> (a.fst⁻¹ •> a.snd <• a.fst⁻¹)) + -(b.fst⁻¹ •> b.snd <• b.fst⁻¹ <• a.fst⁻¹)
⊢ -((a.fst * b.fst)⁻¹ •> (a.fst •> b.snd + a.snd <• b.fst) <• (a.fst * b.fst)⁻¹) =
    b.fst⁻¹ •> -(a.fst⁻¹ •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• b.fst⁻¹) <• a.fst⁻¹

Tactic:
simp only [smul_neg, smul_add]

Premises used: smul_neg, smul_add
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
h2 :
  -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
⊢ -((a.fst * b.fst)⁻¹ •> a.fst •> b.snd <• (a.fst * b.fst)⁻¹ +
        (a.fst * b.fst)⁻¹ •> (a.snd <• b.fst) <• (a.fst * b.fst)⁻¹) =
    -(b.fst⁻¹ •> (a.fst⁻¹ •> a.snd <• a.fst⁻¹)) + -(b.fst⁻¹ •> b.snd <• b.fst⁻¹ <• a.fst⁻¹)

Tactic:
simp_rw [mul_inv_rev, smul_comm (_ : R), op_smul_op_smul, smul_smul, add_comm, neg_add]

Premises used: smul_smul, neg_add, op_smul_op_smul, add_comm, mul_inv_rev, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
h2 :
  ∀ (ha0 : a.fst = 0),
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
        -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
      -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
h2₁ :
  ∀ (ha : a.fst ≠ 0),
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
        -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
      -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
obtain ha0 | ha := eq_or_ne (fst a) 0

Premises used: TrivSqZeroExt.fst, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha0 : a.fst = 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
simp [ha0]
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
h2 :
  ∀ (hb0 : b.fst = 0),
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
        -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
      -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
h2₁ :
  ∀ (hb : b.fst ≠ 0),
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
        -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
      -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
obtain hb0 | hb := eq_or_ne (fst b) 0

Premises used: TrivSqZeroExt.fst, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb0 : b.fst = 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
simp [hb0]
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb : b.fst ≠ 0
h2 :
  -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
h2₁ h2₂ :
  -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
rw [inv_mul_cancel_right₀ ha, mul_inv_cancel_left₀ hb]

Premises used: mul_inv_cancel_left₀, inv_mul_cancel_right₀
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
rw rw₁ : x⁻¹⁻¹ = x⁻¹⁻¹
⊢ x⁻¹⁻¹ = 1 * x⁻¹⁻¹

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
rw rw₁ : 1 * x⁻¹⁻¹ = 1 * x⁻¹⁻¹
⊢ 1 * x⁻¹⁻¹ = x * x⁻¹ * x⁻¹⁻¹

Tactic:
rw [TrivSqZeroExt.mul_inv_cancel hx]

Premises used: TrivSqZeroExt.mul_inv_cancel
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
rw : x⁻¹.fst ≠ 0
⊢ x * x⁻¹ * x⁻¹⁻¹ = x

Tactic:
rw [mul_assoc, TrivSqZeroExt.mul_inv_cancel, mul_one]

Premises used: mul_assoc, TrivSqZeroExt.mul_inv_cancel, mul_one
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
rw : x.fst⁻¹ ≠ 0
⊢ x⁻¹.fst ≠ 0

Tactic:
rw [fst_inv]

Premises used: TrivSqZeroExt.fst_inv
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x.fst⁻¹ ≠ 0

Tactic:
apply inv_ne_zero hx

Premises used: inv_ne_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
simp_rw : IsUnit x⁻¹.fst ↔ IsUnit x.fst
simp_rw₁ : IsUnit x.fst⁻¹ ↔ IsUnit x.fst
simp_rw₂ : x.fst⁻¹ ≠ 0 ↔ x.fst ≠ 0
simp_rw₃ : ¬x.fst⁻¹ = 0 ↔ ¬x.fst = 0
⊢ IsUnit x⁻¹ ↔ IsUnit x

Tactic:
simp_rw [isUnit_iff_isUnit_fst, fst_inv, isUnit_iff_ne_zero, ne_eq, inv_eq_zero]

Premises used: inv_eq_zero, isUnit_iff_ne_zero, ne_eq, TrivSqZeroExt.fst_inv, TrivSqZeroExt.isUnit_iff_isUnit_fst
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionRing R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
h1 : (-x)⁻¹.fst = (-x⁻¹).fst
h2 : (-x)⁻¹.snd = (-x⁻¹).snd
⊢ (-x)⁻¹ = -x⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionRing R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
⊢ (-x)⁻¹.fst = (-x⁻¹).fst

Tactic:
simp [inv_neg]

Premises used: inv_neg
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : DivisionRing R
inst_1 : AddCommGroup M
inst_2 : Module.{u, v} Rᵐᵒᵖ M
inst_3 : Module R M
x : tsze R M
⊢ (-x)⁻¹.snd = (-x⁻¹).snd

Tactic:
simp [inv_neg]

Premises used: inv_neg
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
s : S
x : tsze R M
rw : ((algebraMap S R : (a : S) → R) s : R) •> x.snd = x.snd <• (algebraMap S R : (a : S) → R) s
⊢ ((algebraMap S R : (a : S) → R) s : R) •> x.snd + 0 <• x.fst = x.fst •> 0 + x.snd <• (algebraMap S R : (a : S) → R) s

Tactic:
rw [smul_zero, smul_zero, add_zero, zero_add]

Premises used: smul_zero, zero_add, add_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
s : S
x : tsze R M
rw : (s •> 1) •> x.snd = x.snd <• s •> 1
rw₁ : (s •> 1) •> x.snd = (s •> op 1) •> x.snd
rw₂ : (s •> 1) •> x.snd = (s •> 1) •> x.snd
rw₃ : s •> 1 •> x.snd = (s •> 1) •> x.snd
rw₄ : s •> x.snd = (s •> 1) •> x.snd
rw₅ : s •> x.snd = s •> 1 •> x.snd
rw₆ rw₇ : s •> x.snd = s •> x.snd
⊢ ((algebraMap S R : (a : S) → R) s : R) •> x.snd = x.snd <• (algebraMap S R : (a : S) → R) s

Tactic:
rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, op_one, smul_assoc,
          one_smul, smul_assoc, one_smul]

Premises used: smul_assoc, MulOpposite.op_smul, one_smul, Algebra.algebraMap_eq_smul_one, MulOpposite.op_one
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
s : S
x : tsze R M
rw : s •> x.snd = ((algebraMap S R : (a : S) → R) s : R) •> x.snd + 0
rw₁ : s •> x.snd = ((algebraMap S R : (a : S) → R) s : R) •> x.snd
rw₂ rw₃ : s •> x.snd = s •> x.snd
⊢ s •> x.snd = ((algebraMap S R : (a : S) → R) s : R) •> x.snd + 0 <• x.fst

Tactic:
rw [smul_zero, add_zero, algebraMap_smul]

Premises used: smul_zero, algebraMap_smul, add_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
⊢ Eq (α := (a : R') → tsze R' M) (⇑(algebraMap R' (tsze R' M)) : (a : R') → tsze R' M) inl

Tactic:
rfl

Premises used: TrivSqZeroExt.inl, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
⊢ Eq (α := R' →+* tsze R' M) (algebraMap R' (tsze R' M)) (inlHom R' M)

Tactic:
rfl

Premises used: TrivSqZeroExt.inl, TrivSqZeroExt.inlHom, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
s : S
⊢ Eq (α := tsze R M) ((algebraMap S (tsze R M) : (a : S) → tsze R M) s : tsze R M)
    (inl ((algebraMap S R : (a : S) → R) s) : tsze R M)

Tactic:
rfl

Premises used: TrivSqZeroExt.inl, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
A : Type u_2
inst_5 : Semiring A
inst_6 : Algebra R' A
f g : tsze R' M →ₐ[R'] A
h : ∀ (m : M), Eq.{u_2 + 1} (α := A) ((f : (a : tsze R' M) → A) (inr m) : A) ((g : (a : tsze R' M) → A) (inr m) : A)
⊢ f = g

Tactic:
AlgHom.toLinearMap_injective <|
    linearMap_ext (fun _r => (f.commutes _).trans (g.commutes _).symm) h

Premises used: TrivSqZeroExt.linearMap_ext, AlgHom.toLinearMap_injective, AlgHom.commutes, Eq.symm, Eq.trans