awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
commute_half_left :
  ∀ (a : α),
    @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
rw :
  HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
    (HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)) +
        HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α)) +
      HMul.hMul (β := α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
        ((unsym : (a : αˢʸᵐ) → α) a : α))
| HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
    (HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α)) +
      HMul.hMul (β := α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
        ((unsym : (a : αˢʸᵐ) → α) a : α))

Tactic:
rw [mul_add (unsym a)]

Premises used: SymAlg.unsym, mul_add, DFunLike.coe
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
commute_half_left :
  ∀ (a : α),
    @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
⊢ HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
      0 =
    0

Tactic:
mul_zero (⅟(2 : α) * ⅟(2 : α))

Premises used: HMul.hMul, Invertible.invOf, MulZeroClass.mul_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
commute_half_left :
  ∀ (a : α),
    @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
calc_3 :
  HMul.hMul (β := αˢʸᵐ) a
      ((sym : (a : α) → αˢʸᵐ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))) :
        αˢʸᵐ) =
    a * (b * (a * a))
calc_3₁ calc_3₂ : a * (b * (a * a)) = a * (b * (a * a))
⊢ (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
            ((unsym : (a : αˢʸᵐ) → α)
                ((sym : (a : α) → αˢʸᵐ)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                          ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                          ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                  αˢʸᵐ) :
              α) +
          HMul.hMul (α := α) (β := α)
            ((unsym : (a : αˢʸᵐ) → α)
                ((sym : (a : α) → αˢʸᵐ)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                          ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                          ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                  αˢʸᵐ) :
              α)
            ((unsym : (a : αˢʸᵐ) → α) a : α))) =
    a * (b * (a * a))

Tactic:
rw [← mul_def, ← mul_def]

Premises used: SymAlg.mul_def
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
r : R
m : M
⊢ fst (r, m) = r

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
r : R
m : M
⊢ snd (r, m) = m

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
x y : tsze R M
h1 : x.fst = y.fst
h2 : x.snd = y.snd
⊢ x = y

Tactic:
Prod.ext h1 h2

Premises used: TrivSqZeroExt, Prod.ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero M
r : R
⊢ fst.{u, v} (M := M) (inl r) = r

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero M
r : R
⊢ Eq.{v + 1} (α := M) (snd (inl r)) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero M
⊢ Eq.{u + 1} (α := R → R) (Function.comp (β := tsze R M) fst inl) id

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero M
⊢ Eq (α := R → M) (snd ∘ inl) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero R
m : M
⊢ Eq.{u + 1} (α := R) (fst (inr m)) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero R
m : M
⊢ snd.{u, v} (R := R) (inr m) = m

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero R
⊢ Eq (α := M → R) (fst ∘ inr) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero R
⊢ Eq.{v + 1} (α := M → M) (Function.comp (β := tsze R M) snd inr) id

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Nonempty M
⊢ Function.Surjective (α := tsze R M) fst

Tactic:
Prod.fst_surjective

Premises used: Prod.fst_surjective, TrivSqZeroExt, TrivSqZeroExt.fst
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Nonempty R
⊢ Function.Surjective (α := tsze R M) snd

Tactic:
Prod.snd_surjective

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, Prod.snd_surjective
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero M
⊢ Function.Injective (α := R) (β := tsze R M) inl

Tactic:
Function.LeftInverse.injective <| fst_inl _

Premises used: Function.LeftInverse.injective, TrivSqZeroExt.fst_inl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero R
⊢ Function.Injective (α := M) (β := tsze R M) inr

Tactic:
Function.LeftInverse.injective <| snd_inr _

Premises used: Function.LeftInverse.injective, TrivSqZeroExt.snd_inr
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
T : Type u_1
S : Type u_2
R : Type u
M : Type v
inst : SMul T R
inst_1 : SMul T M
inst_2 : SMul S R
inst_3 : SMul S M
inst_4 : SMul T S
inst_5 : IsScalarTower T S R
inst_6 : IsScalarTower T S M
⊢ IsScalarTower T S (tsze R M)

Tactic:
inferInstanceAs <| IsScalarTower T S (R × M)

Premises used: _private.0.TrivSqZeroExt.isScalarTower._proof_1
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
T : Type u_1
S : Type u_2
R : Type u
M : Type v
inst : SMul T R
inst_1 : SMul T M
inst_2 : SMul S R
inst_3 : SMul S M
inst_4 : SMulCommClass T S R
inst_5 : SMulCommClass T S M
⊢ SMulCommClass T S (tsze R M)

Tactic:
inferInstanceAs <| SMulCommClass T S (R × M)

Premises used: _private.0.TrivSqZeroExt.smulCommClass._proof_1
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
T : Type u_1
S : Type u_2
R : Type u
M : Type v
inst : SMul S R
inst_1 : SMul S M
inst_2 : SMul.{u_2, u} Sᵐᵒᵖ R
inst_3 : SMul.{u_2, v} Sᵐᵒᵖ M
inst_4 : IsCentralScalar S R
inst_5 : IsCentralScalar S M
⊢ IsCentralScalar S (tsze R M)

Tactic:
inferInstanceAs <| IsCentralScalar S (R × M)

Premises used: _private.0.TrivSqZeroExt.isCentralScalar._proof_1
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
T : Type u_1
S : Type u_2
R_1 : Type u
M_1 : Type v
R : Type u_3
M : Type u_4
inst : Nontrivial R
inst_1 : Nonempty M
⊢ Nontrivial (tsze R M)

Tactic:
inferInstanceAs <| Nontrivial (R × M)

Premises used: _private.0.TrivSqZeroExt.instNontrivial_of_left._proof_1
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
T : Type u_1
S : Type u_2
R_1 : Type u
M_1 : Type v
R : Type u_3
M : Type u_4
inst : Nonempty R
inst_1 : Nontrivial M
⊢ Nontrivial (tsze R M)

Tactic:
inferInstanceAs <| Nontrivial (R × M)

Premises used: _private.0.TrivSqZeroExt.instNontrivial_of_right._proof_1
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero R
inst_1 : Zero M
⊢ Eq.{u + 1} (α := R) (fst.{u, v} (M := M) 0) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero R
inst_1 : Zero M
⊢ Eq.{v + 1} (α := M) (snd.{u, v} (R := R) 0) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Add R
inst_1 : Add M
x₁ x₂ : tsze R M
⊢ (x₁ + x₂).fst = x₁.fst + x₂.fst

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Add R
inst_1 : Add M
x₁ x₂ : tsze R M
⊢ (x₁ + x₂).snd = x₁.snd + x₂.snd

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Neg R
inst_1 : Neg 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 R
inst_1 : Neg M
x : tsze R M
⊢ (-x).snd = -x.snd

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Sub R
inst_1 : Sub M
x₁ x₂ : tsze R M
⊢ (x₁ - x₂).fst = x₁.fst - x₂.fst

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Sub R
inst_1 : Sub M
x₁ x₂ : tsze R M
⊢ (x₁ - x₂).snd = x₁.snd - x₂.snd

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
S : Type u_2
R : Type u
M : Type v
inst : SMul S R
inst_1 : SMul S M
s : S
x : tsze R M
⊢ (s •> x).fst = s •> x.fst

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
S : Type u_2
R : Type u
M : Type v
inst : SMul S R
inst_1 : SMul S M
s : S
x : tsze R M
⊢ (s •> x).snd = s •> x.snd

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
ι : Type u_3
inst : AddCommMonoid R
inst_1 : AddCommMonoid M
s : Finset ι
f : ι → tsze R M
⊢ Eq.{u + 1} (α := R) (fst.{u, v} (M := M) (∑ i ∈ s, f i)) (∑ i ∈ s, (f i).fst)

Tactic:
Prod.fst_sum

Premises used: TrivSqZeroExt, TrivSqZeroExt.fst, Prod.fst_sum
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
ι : Type u_3
inst : AddCommMonoid R
inst_1 : AddCommMonoid M
s : Finset ι
f : ι → tsze R M
⊢ Eq.{v + 1} (α := M) (snd.{u, v} (R := R) (∑ i ∈ s, f i)) (∑ i ∈ s, (f i).snd)

Tactic:
Prod.snd_sum

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, Prod.snd_sum
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero R
inst_1 : Zero M
⊢ Eq (α := tsze R M) (inl 0) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.inl, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Add R
inst_1 : AddZeroClass M
r₁ r₂ : R
⊢ inl (r₁ + r₂) = HAdd.hAdd (α := tsze R M) (inl r₁) (inl r₂)

Tactic:
ext rfl (add_zero 0).symm

Premises used: TrivSqZeroExt.ext, add_zero, OfNat.ofNat, Eq.symm, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Neg R
inst_1 : NegZeroClass M
r : R
⊢ Eq (α := tsze R M) (inl (-r)) (-inl r)

Tactic:
ext rfl neg_zero.symm

Premises used: TrivSqZeroExt.ext, Eq.symm, neg_zero, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Sub R
inst_1 : SubNegZeroMonoid M
r₁ r₂ : R
⊢ inl (r₁ - r₂) = HSub.hSub (α := tsze R M) (inl r₁) (inl r₂)

Tactic:
ext rfl (sub_zero _).symm

Premises used: TrivSqZeroExt.ext, sub_zero, Eq.symm, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
S : Type u_2
R : Type u
M : Type v
inst : Monoid S
inst_1 : AddMonoid M
inst_2 : SMul S R
inst_3 : DistribMulAction S M
s : S
r : R
⊢ inl (s •> r) = s •> inl r

Tactic:
ext rfl (smul_zero s).symm

Premises used: TrivSqZeroExt.ext, smul_zero, Eq.symm, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
ι : Type u_3
inst : AddCommMonoid R
inst_1 : AddCommMonoid M
s : Finset ι
f : ι → R
⊢ Eq (α := tsze R M) (inl (∑ i ∈ s, f i)) (∑ i ∈ s, inl (f i))

Tactic:
map_sum (LinearMap.inl ℕ _ _) _ _

Premises used: Multiset.sum, Multiset.foldr, TrivSqZeroExt, LinearMap.inl, TrivSqZeroExt.inl, map_sum, Nat, Function.prod, Finset.sum
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Zero R
inst_1 : Zero M
⊢ Eq (α := tsze R M) (inr 0) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.inr, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddZeroClass R
inst_1 : Add M
m₁ m₂ : M
⊢ inr (m₁ + m₂) = HAdd.hAdd (α := tsze R M) (inr m₁) (inr m₂)

Tactic:
ext (add_zero 0).symm rfl

Premises used: TrivSqZeroExt.ext, add_zero, OfNat.ofNat, Eq.symm, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : NegZeroClass R
inst_1 : Neg M
m : M
⊢ Eq (α := tsze R M) (inr (-m)) (-inr m)

Tactic:
ext neg_zero.symm rfl

Premises used: TrivSqZeroExt.ext, Eq.symm, neg_zero, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : SubNegZeroMonoid R
inst_1 : Sub M
m₁ m₂ : M
⊢ inr (m₁ - m₂) = HSub.hSub (α := tsze R M) (inr m₁) (inr m₂)

Tactic:
ext (sub_zero _).symm rfl

Premises used: TrivSqZeroExt.ext, sub_zero, Eq.symm, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
S : Type u_2
R : Type u
M : Type v
inst : Zero R
inst_1 : SMulZeroClass S R
inst_2 : SMul S M
r : S
m : M
⊢ inr (r •> m) = r •> inr m

Tactic:
ext (smul_zero _).symm rfl

Premises used: TrivSqZeroExt.ext, smul_zero, Eq.symm, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
ι : Type u_3
inst : AddCommMonoid R
inst_1 : AddCommMonoid M
s : Finset ι
f : ι → M
⊢ Eq (α := tsze R M) (inr (∑ i ∈ s, f i)) (∑ i ∈ s, inr (f i))

Tactic:
map_sum (LinearMap.inr ℕ _ _) _ _

Premises used: Multiset.sum, Multiset.foldr, TrivSqZeroExt.inr, TrivSqZeroExt, map_sum, Nat, Function.prod, LinearMap.inr, Finset.sum
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddZeroClass R
inst_1 : AddZeroClass M
x : tsze R M
⊢ inl x.fst + inr x.snd = x

Tactic:
ext (add_zero x.1) (zero_add x.2)

Premises used: TrivSqZeroExt.ext, zero_add, Prod.fst, add_zero, Prod.snd
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u_3
M : Type u_4
inst : AddZeroClass R
inst_1 : AddZeroClass M
P : tsze R M → Prop
inl_add_inr : ∀ (r : R) (m : M), P (inl r + inr m)
x : tsze R M
⊢ P x

Tactic:
inl_fst_add_inr_snd_eq x ▸ inl_add_inr x.1 x.2

Premises used: TrivSqZeroExt.inl_fst_add_inr_snd_eq, Eq.rec, Prod.fst, Prod.snd
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
S : Type u_2
R : Type u
M : Type v
N : Type u_3
inst : Semiring S
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module S R
inst_5 : Module S M
inst_6 : Module S N
f g : tsze R M →ₗ[S] N
hl : ∀ (r : R), Eq.{u_3 + 1} (α := N) ((f : (a : tsze R M) → N) (inl r) : N) ((g : (a : tsze R M) → N) (inl r) : N)
hr : ∀ (m : M), Eq.{u_3 + 1} (α := N) ((f : (a : tsze R M) → N) (inr m) : N) ((g : (a : tsze R M) → N) (inr m) : N)
⊢ f = g

Tactic:
LinearMap.prod_ext (LinearMap.ext hl) (LinearMap.ext hr)

Premises used: TrivSqZeroExt, LinearMap.ext, LinearMap.prod_ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : One R
inst_1 : Zero M
⊢ Eq.{u + 1} (α := R) (fst.{u, v} (M := M) 1) 1

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : One R
inst_1 : Zero M
⊢ Eq.{v + 1} (α := M) (snd.{u, v} (R := R) 1) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Mul R
inst_1 : Add M
inst_2 : SMul R M
inst_3 : SMul.{u, v} Rᵐᵒᵖ M
x₁ x₂ : tsze R M
⊢ (x₁ * x₂).fst = x₁.fst * x₂.fst

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Mul R
inst_1 : Add M
inst_2 : SMul R M
inst_3 : SMul.{u, v} Rᵐᵒᵖ M
x₁ x₂ : tsze R M
⊢ (x₁ * x₂).snd = x₁.fst •> x₂.snd + 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 : One R
inst_1 : Zero M
⊢ Eq (α := tsze R M) (inl 1) 1

Tactic:
rfl

Premises used: TrivSqZeroExt.inl, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r₁ r₂ : R
rw : 0 = 0 + 0 <• r₂
rw₁ : 0 = 0 <• r₂
rw₂ rw₃ : Eq.{v + 1} (α := M) 0 0
⊢ 0 = r₁ •> 0 + 0 <• r₂

Tactic:
rw [smul_zero, zero_add, smul_zero]

Premises used: smul_zero, zero_add
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r₁ r₂ : R
⊢ HMul.hMul (α := tsze R M) (inl r₁) (inl r₂) = inl (r₁ * r₂)

Tactic:
(inl_mul M r₁ r₂).symm

Premises used: TrivSqZeroExt.inl_mul, Eq.symm
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
m₁ m₂ : M
rw : 0 + m₁ <• 0 = 0
rw₁ : m₁ <• 0 = 0
rw₂ : 0 •> m₁ = 0
rw₃ rw₄ : Eq.{v + 1} (α := M) 0 0
⊢ 0 •> m₂ + m₁ <• 0 = 0

Tactic:
rw [zero_smul, zero_add, op_zero, zero_smul]

Premises used: MulOpposite.op_zero, zero_add, zero_smul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : MonoidWithZero R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
m : M
rw : r •> m + 0 = r •> m
rw₁ rw₂ : r •> m = r •> m
⊢ r •> m + 0 •> 0 = r •> m

Tactic:
rw [smul_zero, add_zero]

Premises used: smul_zero, add_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : MonoidWithZero R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
m : M
rw : 0 + m <• r = m <• r
rw₁ rw₂ : m <• r = m <• r
⊢ 0 •> 0 + m <• r = m <• r

Tactic:
rw [smul_zero, zero_add]

Premises used: smul_zero, zero_add
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
x : tsze R M
dsimp : r •> x.snd + 0 <• x.fst = r •> x.snd
⊢ (inl r * x).snd = (r •> x).snd

Tactic:
dsimp
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
x : tsze R M
rw : r •> x.snd + 0 = r •> x.snd
rw₁ rw₂ : r •> x.snd = r •> x.snd
⊢ r •> x.snd + 0 <• x.fst = r •> x.snd

Tactic:
rw [smul_zero, add_zero]

Premises used: smul_zero, add_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
r : R
dsimp : x.fst •> 0 + x.snd <• r = x.snd <• r
⊢ (x * inl r).snd = (x <• r).snd

Tactic:
dsimp
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
r : R
rw : 0 + x.snd <• r = x.snd <• r
rw₁ rw₂ : x.snd <• r = x.snd <• r
⊢ x.fst •> 0 + x.snd <• r = x.snd <• r

Tactic:
rw [smul_zero, zero_add]

Premises used: smul_zero, zero_add
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : x.2 + 0 <• x.1 = x.2
rw₁ : x.2 + 0 = x.2
rw₂ rw₃ : x.2 = x.2
⊢ 1 •> x.2 + 0 <• x.1 = x.2

Tactic:
rw [one_smul, smul_zero, add_zero]

Premises used: smul_zero, one_smul, add_zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : 0 + x.2 <• 1 = x.2
rw₁ : x.2 <• 1 = x.2
rw₂ : 1 •> x.2 = x.2
rw₃ rw₄ : x.2 = x.2
⊢ x.1 •> 0 + x.2 <• 1 = x.2

Tactic:
rw [smul_zero, zero_add, op_one, one_smul]

Premises used: smul_zero, zero_add, one_smul, MulOpposite.op_one
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddMonoidWithOne R
inst_1 : AddMonoid M
⊢ Eq (α := tsze R M) (inl (↑0 : R)) 0

Tactic:
simp [Nat.cast]

Premises used: Nat.cast
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddMonoidWithOne R
inst_1 : AddMonoid M
x : ℕ
h1 : fst.{u, v} (M := M) (inl (↑(x + 1) : R)) = (HAdd.hAdd (α := tsze R M) (inl (↑x : R)) 1).fst
h2 : snd.{u, v} (R := R) (inl (↑(x + 1) : R)) = (HAdd.hAdd (α := tsze R M) (inl (↑x : R)) 1).snd
⊢ inl (↑(x + 1) : R) = HAdd.hAdd (α := tsze R M) (inl (↑x : R)) 1

Tactic:
ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddMonoidWithOne R
inst_1 : AddMonoid M
x : ℕ
⊢ fst.{u, v} (M := M) (inl (↑(x + 1) : R)) = (HAdd.hAdd (α := tsze R M) (inl (↑x : R)) 1).fst

Tactic:
simp [Nat.cast]

Premises used: Nat.cast
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddMonoidWithOne R
inst_1 : AddMonoid M
x : ℕ
⊢ snd.{u, v} (R := R) (inl (↑(x + 1) : R)) = (HAdd.hAdd (α := tsze R M) (inl (↑x : R)) 1).snd

Tactic:
simp [Nat.cast]

Premises used: Nat.cast
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddMonoidWithOne R
inst_1 : AddMonoid M
n : ℕ
⊢ Eq.{u + 1} (α := R) (fst.{u, v} (M := M) (↑n : tsze R M)) (↑n : R)

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddMonoidWithOne R
inst_1 : AddMonoid M
n : ℕ
⊢ Eq.{v + 1} (α := M) (snd.{u, v} (R := R) (↑n : tsze R M)) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddMonoidWithOne R
inst_1 : AddMonoid M
n : ℕ
⊢ Eq (α := tsze R M) (inl (↑n : R)) (↑n : tsze R M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddGroupWithOne R
inst_1 : AddGroup M
z : ℤ
⊢ Eq.{u + 1} (α := R) (fst.{u, v} (M := M) (↑z : tsze R M)) (↑z : R)

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddGroupWithOne R
inst_1 : AddGroup M
z : ℤ
⊢ Eq.{v + 1} (α := M) (snd.{u, v} (R := R) (↑z : tsze R M)) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : AddGroupWithOne R
inst_1 : AddGroup M
z : ℤ
⊢ Eq (α := tsze R M) (inl (↑z : R)) (↑z : tsze R M)

Tactic:
rfl

Premises used: rfl