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 : 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
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
have h2 : (a * b)⁻¹.snd = (b⁻¹ * a⁻¹).snd
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ (a * b)⁻¹.fst = (b⁻¹ * a⁻¹).fst
have h1 : (a * b).fst⁻¹ = (b⁻¹ * a⁻¹).fst
Tactic: rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ (a * b)⁻¹.fst = (b⁻¹ * a⁻¹).fst
have h1₁ : (a.fst * b.fst)⁻¹ = (b⁻¹ * a⁻¹).fst
Tactic: rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ (a * b)⁻¹.fst = (b⁻¹ * a⁻¹).fst
have h1₂ : (a.fst * b.fst)⁻¹ = b⁻¹.fst * a⁻¹.fst
Tactic: rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ (a * b)⁻¹.fst = (b⁻¹ * a⁻¹).fst
have h1₃ : b.fst⁻¹ * a.fst⁻¹ = b⁻¹.fst * a⁻¹.fst
Tactic: rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ (a * b)⁻¹.fst = (b⁻¹ * a⁻¹).fst
have h1₄ : b.fst⁻¹ * a.fst⁻¹ = b.fst⁻¹ * a⁻¹.fst
Tactic: rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ (a * b)⁻¹.fst = (b⁻¹ * a⁻¹).fst
have h1₅ : b.fst⁻¹ * a.fst⁻¹ = b.fst⁻¹ * a.fst⁻¹
Tactic: rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ (a * b)⁻¹.snd = (b⁻¹ * a⁻¹).snd
have 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⁻¹
Tactic: simp only [snd_inv, snd_mul, fst_mul, fst_inv]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ -((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⁻¹
have 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⁻¹)
Tactic: simp only [smul_neg, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ -((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⁻¹)
have 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⁻¹))
Tactic: simp_rw [mul_inv_rev, smul_comm (_ : R), op_smul_op_smul, smul_smul, add_comm, neg_add]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ -((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⁻¹))
have 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⁻¹))
Tactic: obtain ha0 | ha := eq_or_ne (fst a) 0
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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⁻¹))
⊢ -((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⁻¹))
have 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⁻¹))
Tactic: obtain ha0 | ha := eq_or_ne (fst a) 0
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ -((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⁻¹))
have 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⁻¹))
Tactic: obtain hb0 | hb := eq_or_ne (fst b) 0
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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⁻¹))
⊢ -((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⁻¹))
have 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⁻¹))
Tactic: obtain hb0 | hb := eq_or_ne (fst b) 0
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ -((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⁻¹))
have 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⁻¹))
Tactic: rw [inv_mul_cancel_right₀ ha, mul_inv_cancel_left₀ hb]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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⁻¹))
⊢ -((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⁻¹))
have 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⁻¹))
Tactic: rw [inv_mul_cancel_right₀ ha, mul_inv_cancel_left₀ hb]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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⁻¹⁻¹ = 1 * x⁻¹⁻¹
have rw : x⁻¹⁻¹ = x⁻¹⁻¹
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ 1 * x⁻¹⁻¹ = x * x⁻¹ * x⁻¹⁻¹
have rw : 1 * x⁻¹⁻¹ = 1 * x⁻¹⁻¹
Tactic: rw [TrivSqZeroExt.mul_inv_cancel hx]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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 * x⁻¹ * x⁻¹⁻¹ = x
have rw : x⁻¹.fst ≠ 0
Tactic: rw [mul_assoc, TrivSqZeroExt.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
have rw : x.fst⁻¹ ≠ 0
Tactic: rw [fst_inv]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ IsUnit x⁻¹ ↔ IsUnit x
have simp_rw : IsUnit x⁻¹.fst ↔ IsUnit x.fst
Tactic: simp_rw [isUnit_iff_isUnit_fst, fst_inv, isUnit_iff_ne_zero, ne_eq, inv_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ IsUnit x⁻¹ ↔ IsUnit x
have simp_rw₁ : IsUnit x.fst⁻¹ ↔ IsUnit x.fst
Tactic: simp_rw [isUnit_iff_isUnit_fst, fst_inv, isUnit_iff_ne_zero, ne_eq, inv_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ IsUnit x⁻¹ ↔ IsUnit x
have simp_rw₂ : x.fst⁻¹ ≠ 0 ↔ x.fst ≠ 0
Tactic: simp_rw [isUnit_iff_isUnit_fst, fst_inv, isUnit_iff_ne_zero, ne_eq, inv_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ IsUnit x⁻¹ ↔ IsUnit x
have simp_rw₃ : ¬x.fst⁻¹ = 0 ↔ ¬x.fst = 0
Tactic: simp_rw [isUnit_iff_isUnit_fst, fst_inv, isUnit_iff_ne_zero, ne_eq, inv_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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)⁻¹ = -x⁻¹
have h1 : (-x)⁻¹.fst = (-x⁻¹).fst
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ (-x)⁻¹ = -x⁻¹
have h2 : (-x)⁻¹.snd = (-x⁻¹).snd
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ ((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
have rw : ((algebraMap S R : (a : S) → R) s : R) •> x.snd = x.snd <• (algebraMap S R : (a : S) → R) s
Tactic: rw [smul_zero, smul_zero, add_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ ((algebraMap S R : (a : S) → R) s : R) •> x.snd = x.snd <• (algebraMap S R : (a : S) → R) s
have rw : (s •> 1) •> x.snd = x.snd <• s •> 1
Tactic: rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, op_one, smul_assoc,
          one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ ((algebraMap S R : (a : S) → R) s : R) •> x.snd = x.snd <• (algebraMap S R : (a : S) → R) s
have rw₁ : (s •> 1) •> x.snd = (s •> op 1) •> x.snd
Tactic: rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, op_one, smul_assoc,
          one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ ((algebraMap S R : (a : S) → R) s : R) •> x.snd = x.snd <• (algebraMap S R : (a : S) → R) s
have rw₂ : (s •> 1) •> x.snd = (s •> 1) •> x.snd
Tactic: rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, op_one, smul_assoc,
          one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ ((algebraMap S R : (a : S) → R) s : R) •> x.snd = x.snd <• (algebraMap S R : (a : S) → R) s
have rw₃ : s •> 1 •> x.snd = (s •> 1) •> x.snd
Tactic: rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, op_one, smul_assoc,
          one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ ((algebraMap S R : (a : S) → R) s : R) •> x.snd = x.snd <• (algebraMap S R : (a : S) → R) s
have rw₄ : s •> x.snd = (s •> 1) •> x.snd
Tactic: rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, op_one, smul_assoc,
          one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ ((algebraMap S R : (a : S) → R) s : R) •> x.snd = x.snd <• (algebraMap S R : (a : S) → R) s
have rw₅ : s •> x.snd = s •> 1 •> x.snd
Tactic: rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, op_one, smul_assoc,
          one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ ((algebraMap S R : (a : S) → R) s : R) •> x.snd = x.snd <• (algebraMap S R : (a : S) → R) s
have rw₆ : s •> x.snd = s •> x.snd
Tactic: rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, op_one, smul_assoc,
          one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ s •> x.snd = ((algebraMap S R : (a : S) → R) s : R) •> x.snd + 0 <• x.fst
have rw : s •> x.snd = ((algebraMap S R : (a : S) → R) s : R) •> x.snd + 0
Tactic: rw [smul_zero, add_zero, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ s •> x.snd = ((algebraMap S R : (a : S) → R) s : R) •> x.snd + 0 <• x.fst
have rw₁ : s •> x.snd = ((algebraMap S R : (a : S) → R) s : R) •> x.snd
Tactic: rw [smul_zero, add_zero, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
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
⊢ s •> x.snd = ((algebraMap S R : (a : S) → R) s : R) •> x.snd + 0 <• x.fst
have rw₂ : s •> x.snd = s •> x.snd
Tactic: rw [smul_zero, add_zero, algebraMap_smul]