awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    List.sum
      (List.map
        (fun (x : tsze R M × ℕ) ↦
          (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx)
⊢ List.sum
        (List.map
          ((fun (x_1 : M) ↦ x.fst •> x_1) ∘ fun (x : tsze R M × ℕ) ↦
            (List.take x.2 (List.map fst xs)).prod •> (x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod))
          xs.zipIdx) +
      x.snd <• (List.map fst xs).prod =
    x.snd <• (List.map fst xs).prod +
      List.sum
        (List.map
          (fun (x_1 : tsze R M × ℕ) ↦
            x.fst •>
              (List.take x_1.2 (List.map fst xs)).prod •> (x_1.1.snd <• (List.drop (x_1.2 + 1) (List.map fst xs)).prod))
          xs.zipIdx)

Tactic:
exact add_comm _ _

Premises used: add_comm
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
l : List (tsze R M)
nil :
  Eq.{v + 1} (α := M) (snd.{u, v} (R := R) (List.prod []))
    (List.sum
      (List.map
        (fun (x : tsze R M × ℕ) ↦
          List.prod (List.take x.2 (List.map (α := tsze R M) fst [])) •> x.1.snd <•
            List.prod (List.drop x.2.succ (List.map (α := tsze R M) fst [])))
        (List.zipIdx [])))
cons :
  ∀ (x : tsze R M) (xs : List (tsze R M))
    (ih :
      xs.prod.snd =
        List.sum
          (List.map
            (fun (x : tsze R M × ℕ) ↦
              (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
            xs.zipIdx)),
    (x :: xs).prod.snd =
      List.sum
        (List.map
          (fun (x_1 : tsze R M × ℕ) ↦
            (List.take x_1.2 (List.map fst (x :: xs))).prod •> x_1.1.snd <•
              (List.drop x_1.2.succ (List.map fst (x :: xs))).prod)
          (x :: xs).zipIdx)
⊢ l.prod.snd =
    List.sum
      (List.map
        (fun (x : tsze R M × ℕ) ↦
          (List.take x.2 (List.map fst l)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst l)).prod)
        l.zipIdx)

Tactic:
induction l with
  | nil => simp
  | cons x xs ih =>
    rw [List.zipIdx_cons']
    simp_rw [List.map_cons, List.map_map, Function.comp_def, Prod.map_snd, Prod.map_fst, id,
      List.take_zero, List.take_succ_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul,
      List.drop, mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map,
      ← smul_comm (_ : R) (_ : Rᵐᵒᵖ)]
    exact add_comm _ _

Premises used: Prod.map_snd, List.take_succ_cons, List.map_cons, TrivSqZeroExt.fst_list_prod, id, List.map_map, List.take_zero, add_comm, one_smul, Function.comp_def, TrivSqZeroExt.snd_mul, List.drop, List.sum_cons, List.prod_nil, Prod.map_fst, List.zipIdx_cons', SMulCommClass.smul_comm, List.prod_cons, List.smul_sum, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
rw₂ 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

Tactic:
rw [op_smul_eq_smul, op_smul_eq_smul, add_comm]

Premises used: add_comm, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Neg M
inst_1 : Inv R
inst_2 : SMul.{u, v} Rᵐᵒᵖ M
inst_3 : SMul R M
x : tsze R M
⊢ x⁻¹.fst = x.fst⁻¹

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Neg M
inst_1 : Inv R
inst_2 : SMul.{u, v} Rᵐᵒᵖ M
inst_3 : SMul R M
x : tsze R M
⊢ x⁻¹.snd = -(x.fst⁻¹ •> x.snd <• x.fst⁻¹)

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt.fst, rfl
-- 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
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
rw₂ rw₃ : Eq.{u + 1} (α := R) 1 1
⊢ (@Invertible.invOf _ mul one x _).fst * x.fst = 1

Tactic:
rw [← fst_mul, invOf_mul_self, fst_one]

Premises used: invOf_mul_self, TrivSqZeroExt.fst_one, TrivSqZeroExt.fst_mul
-- 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
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
rw₂ rw₃ : Eq.{u + 1} (α := R) 1 1
⊢ x.fst * (@Invertible.invOf _ mul one x _).fst = 1

Tactic:
rw [← fst_mul, mul_invOf_self, fst_one]

Premises used: TrivSqZeroExt.fst_one, mul_invOf_self, TrivSqZeroExt.fst_mul
-- 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
x : tsze R M
inst_4 : Invertible x
inst_5 : Invertible x.fst
this : Invertible x.fst := x.invertibleFstOfInvertible
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _

Tactic:
(rfl : _ = ⅟x.fst)

Premises used: rfl
-- 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
x : tsze R M
inst_4 : Invertible x
inst_5 : Invertible x.fst
this : Invertible x.fst := x.invertibleFstOfInvertible
⊢ (@Invertible.invOf _ mul one x _).fst = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _

Tactic:
convert! (rfl : _ = ⅟x.fst)

Premises used: rfl
-- 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
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
h2 : ((inl r + inr (-(r •> x.snd <• r))) * x).snd = snd.{u, v} (R := R) 1
⊢ (inl r + inr (-(r •> x.snd <• r))) * x = 1

Tactic:
ext
-- 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
r : R
x : tsze R M
h : r * x.fst = 1
h1 : (r + 0) * x.fst = 1
⊢ ((inl r + inr (-(r •> x.snd <• r))) * x).fst = fst.{u, v} (M := M) 1

Tactic:
dsimp
-- 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
r : R
x : tsze R M
h : r * x.fst = 1
h2 : (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
⊢ ((inl r + inr (-(r •> x.snd <• r))) * x).snd = snd.{u, v} (R := R) 1

Tactic:
dsimp
-- 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
r : R
x : tsze R M
h h1 : r * x.fst = 1
h1₁ h1₂ : Eq.{u + 1} (α := R) 1 1
⊢ (r + 0) * x.fst = 1

Tactic:
rw [add_zero, h]

Premises used: add_zero
-- 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
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
h2₇ h2₈ : Eq.{v + 1} (α := M) 0 0
⊢ (r + 0) •> 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]

Premises used: add_neg_cancel, smul_neg, op_smul_op_smul, zero_add, one_smul, MulOpposite.op_one, add_zero
-- 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
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
h2 : (x * (inl r + inr (-(r •> (x.snd <• r))))).snd = snd.{u, v} (R := R) 1
⊢ x * (inl r + inr (-(r •> (x.snd <• r)))) = 1

Tactic:
ext
-- 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
x : tsze R M
r : R
h : x.fst * r = 1
h1 : x.fst * (r + 0) = 1
⊢ (x * (inl r + inr (-(r •> (x.snd <• r))))).fst = fst.{u, v} (M := M) 1

Tactic:
dsimp
-- 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
x : tsze R M
r : R
h : x.fst * r = 1
h2 : x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0
⊢ (x * (inl r + inr (-(r •> (x.snd <• r))))).snd = snd.{u, v} (R := R) 1

Tactic:
dsimp
-- 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
x : tsze R M
r : R
h h1 : x.fst * r = 1
h1₁ h1₂ : Eq.{u + 1} (α := R) 1 1
⊢ x.fst * (r + 0) = 1

Tactic:
rw [add_zero, h]

Premises used: add_zero
-- 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
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
h2₆ h2₇ : Eq.{v + 1} (α := M) 0 0
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0

Tactic:
rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]

Premises used: smul_smul, smul_neg, zero_add, one_smul, neg_add_cancel, add_zero
-- 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
x : tsze R M
inst_5 : Invertible 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 _))) *
      x =
    1

Tactic:
mul_left_eq_one _ _ (invOf_mul_self x.fst)

Premises used: TrivSqZeroExt.mul_left_eq_one, invOf_mul_self, TrivSqZeroExt.fst
-- 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
x : tsze R M
inst_5 : Invertible x.fst
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 _))
⊢ (@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

Tactic:
convert! mul_left_eq_one _ _ (invOf_mul_self x.fst)

Premises used: TrivSqZeroExt.mul_left_eq_one, invOf_mul_self, TrivSqZeroExt.fst
-- 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
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
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
⊢ (@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:
ext
-- 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
x : tsze R M
inst_5 : Invertible 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 _))).fst

Tactic:
simp
-- 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
x : tsze R M
inst_5 : Invertible x.fst
⊢ 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:
simp
-- 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
x : tsze R M
inst_5 : Invertible x.fst
⊢ x *
      (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 _)))) =
    1

Tactic:
mul_right_eq_one _ _ (mul_invOf_self x.fst)

Premises used: mul_invOf_self, TrivSqZeroExt.fst, TrivSqZeroExt.mul_right_eq_one
-- 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
x : tsze R M
inst_5 : Invertible x.fst
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 _)))
⊢ 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

Tactic:
convert! mul_right_eq_one _ _ (mul_invOf_self x.fst)

Premises used: mul_invOf_self, TrivSqZeroExt.fst, TrivSqZeroExt.mul_right_eq_one
-- 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
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
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
⊢ (@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:
ext
-- 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
x : tsze R M
inst_5 : Invertible 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 _)))).fst

Tactic:
simp [smul_comm]

Premises used: SMulCommClass.smul_comm
-- 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
x : tsze R M
inst_5 : Invertible x.fst
⊢ 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:
simp [smul_comm]

Premises used: SMulCommClass.smul_comm
-- 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
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 _ mul one x _).snd

Tactic:
congr_arg (TrivSqZeroExt.snd (R := R) (M := M)) (_ : _ = ⅟x)

Premises used: TrivSqZeroExt.snd, congr_arg
-- 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
x : tsze R M
inst_5 : Invertible x
inst_6 : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
convert_2 : @Invertible.invOf _ mul one x _ = @Invertible.invOf _ mul one x _
⊢ (@Invertible.invOf _ mul one x _).snd =
    -(@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ •> x.snd <•
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _)

Tactic:
convert! congr_arg (TrivSqZeroExt.snd (R := R) (M := M)) (_ : _ = ⅟x)

Premises used: TrivSqZeroExt.snd, congr_arg
-- 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
x : tsze R M
inst_5 : Invertible x
inst_6 : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
⊢ @Invertible.invOf _ mul one x _ = @Invertible.invOf _ mul one x _

Tactic:
rfl

Premises used: rfl
-- 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
x : tsze R M
inst_5 : Invertible x
inst_6 : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
⊢ @Invertible.invOf _ mul one x _ = @Invertible.invOf _ mul one x _

Tactic:
convert! rfl

Premises used: rfl
-- 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
x : tsze R M
⊢ IsUnit x ↔ IsUnit x.fst

Tactic:
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivInvertibleFst x).nonempty_congr]

Premises used: TrivSqZeroExt.invertibleEquivInvertibleFst, nonempty_invertible_iff_isUnit, Equiv.nonempty_congr
-- 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
r : R
rw : IsUnit (fst.{u, v} (M := M) (inl r)) ↔ IsUnit r
rw₁ rw₂ : IsUnit r ↔ IsUnit r
⊢ IsUnit (M := tsze R M) (inl r) ↔ IsUnit r

Tactic:
rw [isUnit_iff_isUnit_fst, fst_inl]

Premises used: TrivSqZeroExt.fst_inl, TrivSqZeroExt.isUnit_iff_isUnit_fst