awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
simp_rw :
  ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x - y ≠ 0) ∧
          x - z ≠ 0) ∧
        y - z ≠ 0) ∧
      (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x - y ≠ 0) ∧
          x - z ≠ 0) ∧
        y - z ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw₁ :
  ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x ≠ y) ∧
          x ≠ z) ∧
        y ≠ z) ∧
      (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x ≠ y) ∧
          x ≠ z) ∧
        y ≠ z ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw₂ :
  ((((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z) ∧ (((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw₃ : ((P.a ≠ 0 ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw₄ : (x ≠ y ∧ x ≠ z) ∧ y ≠ z ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
⊢ HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) * (y - z) *
        (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
          (y - z)) ≠
      0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha,
    and_assoc]

Premises used: sub_ne_zero, and_iff_right, and_assoc, map_ne_zero, and_self_iff, mul_ne_zero_iff
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
have : ∀ (x y z : K) (h3 : (map φ P).roots = {x, y, z}), P.discr ≠ 0 ↔ (map φ P).roots.Nodup
⊢ P.discr ≠ 0 ↔ (map φ P).roots.Nodup

Tactic:
have ⟨x, y, z, h3⟩ := (splits_iff_roots_eq_three ha).mp hP
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
rw : x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ Nodup (α := K) {x, y, z}
⊢ P.discr ≠ 0 ↔ (map φ P).roots.Nodup

Tactic:
rw [discr_ne_zero_iff_roots_ne ha h3, h3]

Premises used: Cubic.discr_ne_zero_iff_roots_ne
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
rw : x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ Nodup (α := K) {z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ (x ::ₘ y ::ₘ {z}).Nodup

Tactic:
rw [nodup_cons, nodup_cons, mem_cons, mem_singleton, mem_singleton]

Premises used: Multiset.nodup_cons, Multiset.mem_cons, Multiset.mem_singleton
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
simp : x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ Nodup (α := K) {z}

Tactic:
simp only [nodup_singleton]

Premises used: Multiset.nodup_singleton
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
mp : x ≠ y ∧ x ≠ z ∧ y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mpr : ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True → x ≠ y ∧ x ≠ z ∧ y ≠ z
mp₁ mp₂ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mp₃ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z)
mp₄ : x ≠ y → x ≠ z → y ≠ z → ¬y = z
mpr₁ mpr₂ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ y ∧ x ≠ z ∧ y ≠ z
mpr₃ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ y
mpr₄ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ z
mpr₅ : ¬(x = y ∨ x = z) → ¬y = z → True → y ≠ z
mp₅ : x ≠ y → x ≠ z → y ≠ z → x = y → False
mp₆ : x ≠ y → x ≠ z → y ≠ z → x = z → False
mpr₆ : ¬y = z → True → x = y → ¬x = y → ¬x = z → False
mpr₇ : ¬y = z → True → x = z → ¬x = y → ¬x = z → False
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True

Tactic:
tauto
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
inst_2 : DecidableEq K
ha : P.a ≠ 0
h3 : (Polynomial.map φ P.toPoly).Splits
hd : P.discr ≠ 0
rwa : (map φ P).roots.card = 3
rwa₁ rwa₂ rwa₃ rwa₄ : (Polynomial.map φ P.toPoly).Splits
⊢ (map φ P).roots.toFinset.card = 3

Tactic:
rwa [toFinset_card_of_nodup <| (discr_ne_zero_iff_roots_nodup ha h3).mp hd,
    ← splits_iff_card_roots ha]

Premises used: Cubic.splits_iff_card_roots, Multiset.toFinset_card_of_nodup, Iff.mp, Cubic.discr_ne_zero_iff_roots_nodup
-- Module: Mathlib.Algebra.DirectSum.AddChar
Goal:
ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommGroup (G i)
inst_2 : CommMonoid R
⊢ Injective (α := (i : ι) → AddChar.{u_3, u_2} (G i) R) (directSum (G := G))

Tactic:
toAddMonoidHomEquiv.symm.injective.comp <| DirectSum.toAddMonoid_injective.comp ?_

Premises used: AddChar.toAddMonoidHomEquiv, AddChar.directSum, Function.Injective.comp, Equiv.injective, Equiv.symm, DirectSum.toAddMonoid_injective
-- Module: Mathlib.Algebra.DirectSum.AddChar
Goal:
ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommGroup (G i)
inst_2 : CommMonoid R
refine :
  Injective (β := (i : ι) → AddMonoidHom.{u_3, u_2} (G i) (Additive R))
    fun (ψ : (i : ι) → AddChar.{u_3, u_2} (G i) R) (i : ι) ↦
    (toAddMonoidHomEquiv : (a : AddChar (G i) R) → G i →+ Additive R) (ψ i)
⊢ Injective (α := (i : ι) → AddChar.{u_3, u_2} (G i) R) (directSum (G := G))

Tactic:
refine toAddMonoidHomEquiv.symm.injective.comp <| DirectSum.toAddMonoid_injective.comp ?_

Premises used: AddChar.toAddMonoidHomEquiv, Function.Injective.comp, Equiv.injective, Equiv.symm, DirectSum.toAddMonoid_injective
-- Module: Mathlib.Algebra.DirectSum.AddChar
Goal:
ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommGroup (G i)
inst_2 : CommMonoid R
ψ χ : (i : ι) → AddChar.{u_3, u_2} (G i) R
h :
  Eq (α := (i : ι) → AddMonoidHom.{u_3, u_2} (G i) (Additive R))
    ((fun (ψ : (i : ι) → AddChar.{u_3, u_2} (G i) R) (i : ι) ↦
        ((toAddMonoidHomEquiv : (a : AddChar (G i) R) → G i →+ Additive R) (ψ i) :
          AddMonoidHom.{u_3, u_2} (G i) (Additive R)))
      ψ)
    ((fun (ψ : (i : ι) → AddChar.{u_3, u_2} (G i) R) (i : ι) ↦
        ((toAddMonoidHomEquiv : (a : AddChar (G i) R) → G i →+ Additive R) (ψ i) :
          AddMonoidHom.{u_3, u_2} (G i) (Additive R)))
      χ)
⊢ ψ = χ

Tactic:
simpa [funext_iff] using h

Premises used: funext_iff
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
s : R
x y : GradedMonoid A
dsimp : s • (x * y) = x * s • y
⊢ s • x • y = x • s • y

Tactic:
dsimp
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
s : R
x y : GradedMonoid A
rw :
  HMul.hMul (α := GradedMonoid A)
      (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
      (x * y) =
    x * s • y
rw₁ :
  HMul.hMul (α := GradedMonoid A)
      (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
      (x * y) =
    x *
      HMul.hMul (α := GradedMonoid A)
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
        y
rw₂ :
  HMul.hMul (α := GradedMonoid A)
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
        x *
      y =
    x *
      HMul.hMul (α := GradedMonoid A)
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
        y
rw₃ :
  HMul.hMul (β := GradedMonoid A) x
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) :
          GradedMonoid A) *
      y =
    x *
      HMul.hMul (α := GradedMonoid A)
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
        y
rw₄ rw₅ :
  x *
      HMul.hMul (α := GradedMonoid A)
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
        y =
    x *
      HMul.hMul (α := GradedMonoid A)
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
        y
⊢ s • (x * y) = x * s • y

Tactic:
rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc, GAlgebra.commutes, mul_assoc]

Premises used: mul_assoc, DirectSum.GAlgebra.smul_def, DirectSum.GAlgebra.commutes
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
s : R
x y : GradedMonoid A
dsimp : s • x * y = s • (x * y)
⊢ (s • x) • y = s • x • y

Tactic:
dsimp
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
s : R
x y : GradedMonoid A
rw :
  HMul.hMul (α := GradedMonoid A)
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
        x *
      y =
    s • (x * y)
rw₁ :
  HMul.hMul (α := GradedMonoid A)
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
        x *
      y =
    HMul.hMul (α := GradedMonoid A)
      (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
      (x * y)
rw₂ rw₃ :
  HMul.hMul (α := GradedMonoid A)
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
        x *
      y =
    HMul.hMul (α := GradedMonoid A)
        (GradedMonoid.mk (A := A) 0 ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) s) : GradedMonoid A)
        x *
      y
⊢ s • x * y = s • (x * y)

Tactic:
rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc]

Premises used: mul_assoc, DirectSum.GAlgebra.smul_def
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
a b : R
simp :
  (of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) (a * b)) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) a) :
        ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) b) :
        ⨁ (i : ι), A i)
⊢ (AddMonoidHom.comp (N := A 0) (of A 0) (@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _) : (a : R) → ⨁ (i : ι), A i)
      (a * b) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((AddMonoidHom.comp (N := A 0) (of A 0) (@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _) : (a : R) → ⨁ (i : ι), A i)
          a :
        ⨁ (i : ι), A i)
      ((AddMonoidHom.comp (N := A 0) (of A 0) (@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _) : (a : R) → ⨁ (i : ι), A i)
          b :
        ⨁ (i : ι), A i)

Tactic:
simp only [AddMonoidHom.comp_apply]

Premises used: AddMonoidHom.comp_apply
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
a b : R
rw :
  Eq (α := ⨁ (i : ι), A i)
    ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) (a * b)) :
      ⨁ (i : ι), A i)
    ((of A (HAdd.hAdd (α := ι) 0 0) : (a : A (0 + 0)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) a)
          ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) b)) :
      ⨁ (i : ι), A i)
⊢ (of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) (a * b)) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) a) :
        ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) b) :
        ⨁ (i : ι), A i)

Tactic:
rw [of_mul_of]

Premises used: DirectSum.of_mul_of
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
a b : R
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) (a * b)) :
      ⨁ (i : ι), A i)
    ((of A (HAdd.hAdd (α := ι) 0 0) : (a : A (0 + 0)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) a)
          ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) b)) :
      ⨁ (i : ι), A i)

Tactic:
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.map_mul a b)

Premises used: DFinsupp.single_eq_of_sigma_eq, DirectSum.GAlgebra.map_mul
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
change :
  Eq (α := ⨁ (i : ι), A i)
    ((((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i)
                ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        x :
      ⨁ (i : ι), A i)
    ((((AddMonoidHom.flip AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i)
                ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        x :
      ⨁ (i : ι), A i)
⊢ HMul.hMul (α := ⨁ (i : ι), A i)
      (({
              toFun :=
                (⇑(AddMonoidHom.comp (N := A 0) (of A 0) (@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _)) :
                  (a : R) → ⨁ (i : ι), A i),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : R →+* ⨁ (i : ι), A i } :
            (a : R) → ⨁ (i : ι), A i)
          r :
        ⨁ (i : ι), A i)
      x =
    HMul.hMul (β := ⨁ (i : ι), A i) x
      (({
              toFun :=
                (⇑(AddMonoidHom.comp (N := A 0) (of A 0) (@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _)) :
                  (a : R) → ⨁ (i : ι), A i),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : R) → ⨁ (i : ι), A i)
          r :
        ⨁ (i : ι), A i)

Tactic:
change AddMonoidHom.mul (DirectSum.of _ _ _) x = AddMonoidHom.mul.flip (DirectSum.of _ _ _) x

Premises used: AddMonoidHom.mul, AddMonoidHom.flip, DirectSum.of, DFunLike.coe
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
apply :
  Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
    ((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
      (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
    ((AddMonoidHom.flip AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
      (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i)
                ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        x :
      ⨁ (i : ι), A i)
    ((((AddMonoidHom.flip AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i)
                ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        x :
      ⨁ (i : ι), A i)

Tactic:
apply DFunLike.congr_fun _ x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
H :
  ∀ (i : ι) (xi : A i),
    Eq (α := ⨁ (i : ι), A i)
      ((AddMonoidHom.comp
              ((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                ((of A 0 : (a : A 0) → ⨁ (i : ι), A i)
                  ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)))
              (of A i) :
            (a : A i) → ⨁ (i : ι), A i)
          xi :
        ⨁ (i : ι), A i)
      ((AddMonoidHom.comp
              ((AddMonoidHom.flip AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                ((of A 0 : (a : A 0) → ⨁ (i : ι), A i)
                  ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)))
              (of A i) :
            (a : A i) → ⨁ (i : ι), A i)
          xi :
        ⨁ (i : ι), A i)
⊢ Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
    ((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
      (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
    ((AddMonoidHom.flip AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
      (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)

Tactic:
ext i xi : 2
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
H :
  HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) :
        ⨁ (i : ι), A i)
      ((of A i : (a : A i) → ⨁ (i : ι), A i) xi : ⨁ (i : ι), A i) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) xi : ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) :
        ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((AddMonoidHom.comp
            ((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)))
            (of A i) :
          (a : A i) → ⨁ (i : ι), A i)
        xi :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.comp
            ((AddMonoidHom.flip AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)))
            (of A i) :
          (a : A i) → ⨁ (i : ι), A i)
        xi :
      ⨁ (i : ι), A i)

Tactic:
dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.mul_apply, AddMonoidHom.flip_apply]

Premises used: AddMonoidHom.flip_apply, AddMonoidHom.mul_apply, AddMonoidHom.comp_apply
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
H :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (0 + i) : (a : A (0 + i)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) xi) :
      ⨁ (i : ι), A i)
    ((of A (i + 0) : (a : A (i + 0)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) xi ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
      ⨁ (i : ι), A i)
⊢ HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) :
        ⨁ (i : ι), A i)
      ((of A i : (a : A i) → ⨁ (i : ι), A i) xi : ⨁ (i : ι), A i) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) xi : ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) :
        ⨁ (i : ι), A i)

Tactic:
rw [of_mul_of, of_mul_of]

Premises used: DirectSum.of_mul_of