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 : 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
inst_6 : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
⊢ (@Invertible.invOf _ mul one x _).snd =
    -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)
have convert_2 : @Invertible.invOf _ mul one x _ = @Invertible.invOf _ mul one x _
Tactic: convert! congr_arg (TrivSqZeroExt.snd (R := R) (M := M)) (_ : _ = ⅟x)
-- 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
r : R
⊢ IsUnit (M := tsze R M) (inl r) ↔ IsUnit r
have rw : IsUnit (fst.{u, v} (M := M) (inl r)) ↔ IsUnit r
Tactic: rw [isUnit_iff_isUnit_fst, fst_inl]
-- 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
r : R
rw : IsUnit (fst.{u, v} (M := M) (inl r)) ↔ IsUnit r
⊢ IsUnit (M := tsze R M) (inl r) ↔ IsUnit r
have rw₁ : IsUnit r ↔ IsUnit r
Tactic: rw [isUnit_iff_isUnit_fst, fst_inl]
-- 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
m : M
⊢ IsUnit (M := tsze R M) (inr m) ↔ Subsingleton R
have simp_rw : IsUnit.{u} (M := R) (fst (inr m)) ↔ Subsingleton R
Tactic: simp_rw [isUnit_iff_isUnit_fst, fst_inr, isUnit_zero_iff, subsingleton_iff_zero_eq_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
inst_4 : SMulCommClass R Rᵐᵒᵖ M
m : M
simp_rw : IsUnit.{u} (M := R) (fst (inr m)) ↔ Subsingleton R
⊢ IsUnit (M := tsze R M) (inr m) ↔ Subsingleton R
have simp_rw₁ : IsUnit.{u} (M := R) 0 ↔ Subsingleton R
Tactic: simp_rw [isUnit_iff_isUnit_fst, fst_inr, isUnit_zero_iff, subsingleton_iff_zero_eq_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
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
⊢ IsUnit (M := tsze R M) (inr m) ↔ Subsingleton R
have simp_rw₂ : Eq.{u + 1} (α := R) 0 1 ↔ Subsingleton R
Tactic: simp_rw [isUnit_iff_isUnit_fst, fst_inr, isUnit_zero_iff, subsingleton_iff_zero_eq_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
r : R
⊢ Eq (α := tsze R M) (inl r)⁻¹ (inl r⁻¹)
have h1 : fst.{u, v} (M := M) (inl r)⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
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
r : R
h1 : fst.{u, v} (M := M) (inl r)⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
⊢ Eq (α := tsze R M) (inl r)⁻¹ (inl r⁻¹)
have h2 : Eq.{v + 1} (α := M) (snd (inl r)⁻¹) (snd (inl r⁻¹))
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
r : R
⊢ fst.{u, v} (M := M) (inl r)⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
have h1 : (fst.{u, v} (M := M) (inl r))⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
Tactic: rw [fst_inv, fst_inl, fst_inl]
-- 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
r : R
h1 : (fst.{u, v} (M := M) (inl r))⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
⊢ fst.{u, v} (M := M) (inl r)⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
have h1₁ : r⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
Tactic: rw [fst_inv, fst_inl, fst_inl]
-- 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
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⁻¹)
⊢ fst.{u, v} (M := M) (inl r)⁻¹ = fst.{u, v} (M := M) (inl r⁻¹)
have h1₂ : r⁻¹ = r⁻¹
Tactic: rw [fst_inv, fst_inl, fst_inl]
-- 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
r : R
⊢ Eq.{v + 1} (α := M) (snd (inl r)⁻¹) (snd (inl r⁻¹))
have h2 : -((fst.{u, v} (M := M) (inl r))⁻¹ •> snd (inl r) <• (fst.{u, v} (M := M) (inl r))⁻¹) = snd (inl r⁻¹)
Tactic: rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_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
r : R
h2 : -((fst.{u, v} (M := M) (inl r))⁻¹ •> snd (inl r) <• (fst.{u, v} (M := M) (inl r))⁻¹) = snd (inl r⁻¹)
⊢ Eq.{v + 1} (α := M) (snd (inl r)⁻¹) (snd (inl r⁻¹))
have h2₁ : -(r⁻¹ •> snd (inl r) <• r⁻¹) = snd (inl r⁻¹)
Tactic: rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_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
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⁻¹)
⊢ Eq.{v + 1} (α := M) (snd (inl r)⁻¹) (snd (inl r⁻¹))
have h2₂ : -(r⁻¹ •> 0 <• r⁻¹) = snd (inl r⁻¹)
Tactic: rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_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
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⁻¹)
⊢ Eq.{v + 1} (α := M) (snd (inl r)⁻¹) (snd (inl r⁻¹))
have h2₃ : -(r⁻¹ •> 0 <• r⁻¹) = 0
Tactic: rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_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
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
⊢ Eq.{v + 1} (α := M) (snd (inl r)⁻¹) (snd (inl r⁻¹))
have h2₄ : -(0 <• r⁻¹) = 0
Tactic: rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_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
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
⊢ Eq.{v + 1} (α := M) (snd (inl r)⁻¹) (snd (inl r⁻¹))
have h2₅ : Eq.{v + 1} (α := M) (-0) 0
Tactic: rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_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
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
⊢ Eq.{v + 1} (α := M) (snd (inl r)⁻¹) (snd (inl r⁻¹))
have h2₆ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_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
m : M
⊢ Eq (α := tsze R M) (inr m)⁻¹ 0
have h1 : Eq.{u + 1} (α := R) (fst (inr m)⁻¹) (fst.{u, v} (M := M) 0)
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
m : M
h1 : Eq.{u + 1} (α := R) (fst (inr m)⁻¹) (fst.{u, v} (M := M) 0)
⊢ Eq (α := tsze R M) (inr m)⁻¹ 0
have h2 : snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0
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
m : M
⊢ Eq.{u + 1} (α := R) (fst (inr m)⁻¹) (fst.{u, v} (M := M) 0)
have h1 : Eq.{u + 1} (α := R) (fst (inr m))⁻¹ (fst.{u, v} (M := M) 0)
Tactic: rw [fst_inv, fst_inr, fst_zero, inv_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
m : M
h1 : Eq.{u + 1} (α := R) (fst (inr m))⁻¹ (fst.{u, v} (M := M) 0)
⊢ Eq.{u + 1} (α := R) (fst (inr m)⁻¹) (fst.{u, v} (M := M) 0)
have h1₁ : Eq.{u + 1} (α := R) 0⁻¹ (fst.{u, v} (M := M) 0)
Tactic: rw [fst_inv, fst_inr, fst_zero, inv_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
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)
⊢ Eq.{u + 1} (α := R) (fst (inr m)⁻¹) (fst.{u, v} (M := M) 0)
have h1₂ : Eq.{u + 1} (α := R) 0⁻¹ 0
Tactic: rw [fst_inv, fst_inr, fst_zero, inv_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
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
⊢ Eq.{u + 1} (α := R) (fst (inr m)⁻¹) (fst.{u, v} (M := M) 0)
have h1₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [fst_inv, fst_inr, fst_zero, inv_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
m : M
⊢ snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0
have h2 : -((fst (inr m))⁻¹ •> snd.{u, v} (R := R) (inr m) <• (fst (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]
-- 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
m : M
h2 : -((fst (inr m))⁻¹ •> snd.{u, v} (R := R) (inr m) <• (fst (inr m))⁻¹) = snd.{u, v} (R := R) 0
⊢ snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0
have h2₁ : -((fst (inr m))⁻¹ •> m <• (fst (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]
-- 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
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
⊢ snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0
have h2₂ : -(0⁻¹ •> m <• 0⁻¹) = snd.{u, v} (R := R) 0
Tactic: rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_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
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
⊢ snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0
have h2₃ : -(0 •> m <• 0) = snd.{u, v} (R := R) 0
Tactic: rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_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
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
⊢ snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0
have h2₄ : -(0 •> 0 •> 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]
-- 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
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
⊢ snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0
have h2₅ : Eq.{v + 1} (α := M) (-0) (snd.{u, v} (R := R) 0)
Tactic: rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_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
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)
⊢ snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0
have h2₆ : Eq.{v + 1} (α := M) (-0) 0
Tactic: rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_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
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
⊢ snd.{u, v} (R := R) (inr m)⁻¹ = snd.{u, v} (R := R) 0
have h2₇ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_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
⊢ Eq (α := tsze R M) 0⁻¹ 0
have rw : Eq (α := tsze R M) (inl 0)⁻¹ (inl 0)
Tactic: rw [← inl_zero, TrivSqZeroExt.inv_inl, inv_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
rw : Eq (α := tsze R M) (inl 0)⁻¹ (inl 0)
⊢ Eq (α := tsze R M) 0⁻¹ 0
have rw₁ : Eq (α := tsze R M) (inl 0⁻¹) (inl 0)
Tactic: rw [← inl_zero, TrivSqZeroExt.inv_inl, inv_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
rw : Eq (α := tsze R M) (inl 0)⁻¹ (inl 0)
rw₁ : Eq (α := tsze R M) (inl 0⁻¹) (inl 0)
⊢ Eq (α := tsze R M) 0⁻¹ 0
have rw₂ : Eq (α := tsze R M) (inl 0) (inl 0)
Tactic: rw [← inl_zero, TrivSqZeroExt.inv_inl, inv_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
⊢ Eq (α := tsze R M) 1⁻¹ 1
have rw : Eq (α := tsze R M) (inl 1)⁻¹ (inl 1)
Tactic: rw [← inl_one, TrivSqZeroExt.inv_inl, inv_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
rw : Eq (α := tsze R M) (inl 1)⁻¹ (inl 1)
⊢ Eq (α := tsze R M) 1⁻¹ 1
have rw₁ : Eq (α := tsze R M) (inl 1⁻¹) (inl 1)
Tactic: rw [← inl_one, TrivSqZeroExt.inv_inl, inv_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
rw : Eq (α := tsze R M) (inl 1)⁻¹ (inl 1)
rw₁ : Eq (α := tsze R M) (inl 1⁻¹) (inl 1)
⊢ Eq (α := tsze R M) 1⁻¹ 1
have rw₂ : Eq (α := tsze R M) (inl 1) (inl 1)
Tactic: rw [← inl_one, TrivSqZeroExt.inv_inl, inv_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
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹ * x = 1
have h : x⁻¹ = inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))
Tactic: convert! mul_left_eq_one _ _ (_root_.inv_mul_cancel₀ hx) using 2
-- 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
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹ = inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))
have h : x⁻¹.fst = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).fst
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
x : tsze R M
hx : x.fst ≠ 0
h : x⁻¹.fst = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).fst
⊢ x⁻¹ = inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))
have h₁ : x⁻¹.snd = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).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
x : tsze R M
inst_5 : Invertible x
this : Invertible x.fst := x.invertibleFstOfInvertible
⊢ @Invertible.invOf _ mul one x _ = x⁻¹
have h1 : (@Invertible.invOf _ mul one x _).fst = x⁻¹.fst
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
x : tsze R M
inst_5 : Invertible x
this : Invertible x.fst := x.invertibleFstOfInvertible
h1 : (@Invertible.invOf _ mul one x _).fst = x⁻¹.fst
⊢ @Invertible.invOf _ mul one x _ = x⁻¹
have h2 : (@Invertible.invOf _ mul one x _).snd = x⁻¹.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
x : tsze R M
hx : x.fst ≠ 0
⊢ x * x⁻¹ = 1
have have : ∀ (this : Invertible x.fst), x * x⁻¹ = 1
Tactic: have : Invertible x.fst := Units.invertible (.mk0 _ 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
this : Invertible x.fst
⊢ x * x⁻¹ = 1
have have : ∀ (this : Invertible x), x * x⁻¹ = 1
Tactic: have := invertibleOfInvertibleFst x
-- 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
this_1 : Invertible x.fst
this : Invertible x
⊢ x * x⁻¹ = 1
have rw : x * @Invertible.invOf _ mul one x _ = 1
Tactic: rw [← invOf_eq_inv, mul_invOf_self]
-- 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
this_1 : Invertible x.fst
this : Invertible x
rw : x * @Invertible.invOf _ mul one x _ = 1
⊢ x * x⁻¹ = 1
have rw₁ : Eq (α := tsze R M) 1 1
Tactic: rw [← invOf_eq_inv, mul_invOf_self]
-- 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)⁻¹ = b⁻¹ * a⁻¹
have h1 : (a * b)⁻¹.fst = (b⁻¹ * a⁻¹).fst
Tactic: ext