awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mp₅ : x ≠ y → x ≠ z → y ≠ z → x = y → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mp₆ : x ≠ y → x ≠ z → y ≠ z → x = z → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mpr₆ : ¬y = z → True → x = y → ¬x = y → ¬x = z → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mpr₇ : ¬y = z → True → x = z → ¬x = y → ¬x = z → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ (map φ P).roots.toFinset.card = 3
have rwa : (map φ P).roots.card = 3
Tactic: rwa [toFinset_card_of_nodup <| (discr_ne_zero_iff_roots_nodup ha h3).mp hd,
    ← splits_iff_card_roots ha]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.AddChar (goal)
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))
have 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)
Tactic: refine toAddMonoidHomEquiv.symm.injective.comp <| DirectSum.toAddMonoid_injective.comp ?_
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ s • x • y = x • s • y
have dsimp : s • (x * y) = x * s • y
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ s • (x * y) = x * s • y
have 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
Tactic: rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc, GAlgebra.commutes, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ s • (x * y) = x * s • y
have 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
Tactic: rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc, GAlgebra.commutes, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ s • (x * y) = x * s • y
have 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
Tactic: rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc, GAlgebra.commutes, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ s • (x * y) = x * s • y
have 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
Tactic: rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc, GAlgebra.commutes, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ s • (x * y) = x * s • y
have 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
Tactic: rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc, GAlgebra.commutes, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ (s • x) • y = s • x • y
have dsimp : s • x * y = s • (x * y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ s • x * y = s • (x * y)
have 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)
Tactic: rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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)
⊢ s • x * y = s • (x * y)
have 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)
Tactic: rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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)
⊢ s • x * y = s • (x * y)
have 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
Tactic: rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ (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)
have 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)
Tactic: simp only [AddMonoidHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ (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)
have 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)
Tactic: rw [of_mul_of]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have 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)
Tactic: change AddMonoidHom.mul (DirectSum.of _ _ _) x = AddMonoidHom.mul.flip (DirectSum.of _ _ _) x
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have 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)
Tactic: apply DFunLike.congr_fun _ x
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have 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)
Tactic: ext i xi : 2