awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ : A
b₂ : B
h : b₂ = 1 * b₂
⊢ b₂ = (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) * b₂
have h₁ : b₂ = b₂
Tactic: rw [SetLike.coe_gOne, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
⊢ (a₁ * a₂) ᵍ⊗ₜ[R] 1 = HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) (a₂ ᵍ⊗ₜ[R] 1)
have rw : (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
      a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
    1 =
  HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
    ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1)
Tactic: rw [← DirectSum.sum_support_decompose 𝒜 a₂, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
⊢ (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
        a₁ *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1 =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
      ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        1)
have simp_rw : Eq (α := 𝒜 ᵍ⊗[R] ℬ)
  (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
    (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
        1))
  (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            1) :
        𝒜 ᵍ⊗[R] ℬ))
Tactic: simp_rw [tmul, sum_tmul, map_sum, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
⊢ Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
      (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
          1))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
      HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
        ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
            ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
              1) :
          𝒜 ᵍ⊗[R] ℬ))
have e_f : Eq (α := ι → 𝒜 ᵍ⊗[R] ℬ)
  (fun (x : ι) ↦
    (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
        1))
  fun (i : ι) ↦
  HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R] 1) :
      𝒜 ᵍ⊗[R] ℬ)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
⊢ Eq (α := ι → 𝒜 ᵍ⊗[R] ℬ)
    (fun (x : ι) ↦
      (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
          1))
    fun (i : ι) ↦
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            1) :
        𝒜 ᵍ⊗[R] ℬ)
have e_f : ∀ (i : ι),
  (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        1) =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            1) :
        𝒜 ᵍ⊗[R] ℬ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
i : ι
⊢ (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        1) =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            1) :
        𝒜 ᵍ⊗[R] ℬ)
have e_f : (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
    ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
      (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) =
  HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ)
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        (a₁ ⊗ₜ[R] (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) :
      𝒜 ᵍ⊗[R] ℬ)
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
          (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) :
      𝒜 ᵍ⊗[R] ℬ)
Tactic: rw [← SetLike.coe_gOne ℬ, tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul,
      SetLike.coe_gOne, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
i : ι
e_f :
  (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          (a₁ ⊗ₜ[R] (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) :
        𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) :
        𝒜 ᵍ⊗[R] ℬ)
⊢ (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        1) =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            1) :
        𝒜 ᵍ⊗[R] ℬ)
have e_f₁ : (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
    ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
      (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) =
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (0 * i))
    ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      HMul.hMul (α := B) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)
        (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B))
Tactic: rw [← SetLike.coe_gOne ℬ, tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul,
      SetLike.coe_gOne, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
i : ι
e_f :
  (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          (a₁ ⊗ₜ[R] (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) :
        𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) :
        𝒜 ᵍ⊗[R] ℬ)
e_f₁ :
  (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (0 * i))
      ((a₁ *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        HMul.hMul (α := B) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)
          (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B))
⊢ (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        1) =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            1) :
        𝒜 ᵍ⊗[R] ℬ)
have e_f₂ : (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
    ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
      (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) =
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
    ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      HMul.hMul (α := B) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)
        (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B))
Tactic: rw [← SetLike.coe_gOne ℬ, tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul,
      SetLike.coe_gOne, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
⊢ (a₁ * a₂) ᵍ⊗ₜ[R] 1 = HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) (a₂ ᵍ⊗ₜ[R] 1)
have rw : (a₁ *
      ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
    1 =
  HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
    ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1)
Tactic: classical
    rw [← DirectSum.sum_support_decompose 𝒜 a₂, Finset.mul_sum]
    simp_rw [tmul, sum_tmul, map_sum, Finset.mul_sum]
    congr
    ext i
    rw [← SetLike.coe_gOne ℬ, tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul,
      SetLike.coe_gOne, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
rw :
  (a₁ *
        ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1 =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
      ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        1)
⊢ (a₁ * a₂) ᵍ⊗ₜ[R] 1 = HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) (a₂ ᵍ⊗ₜ[R] 1)
have rw₁ : (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
      a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
    1 =
  HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
    ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1)
Tactic: classical
    rw [← DirectSum.sum_support_decompose 𝒜 a₂, Finset.mul_sum]
    simp_rw [tmul, sum_tmul, map_sum, Finset.mul_sum]
    congr
    ext i
    rw [← SetLike.coe_gOne ℬ, tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul,
      SetLike.coe_gOne, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
rw :
  (a₁ *
        ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1 =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
      ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        1)
rw₁ rw₂ rw₃ :
  (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
        a₁ *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1 =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
      ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        1)
⊢ (a₁ * a₂) ᵍ⊗ₜ[R] 1 = HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) (a₂ ᵍ⊗ₜ[R] 1)
have rw₄ : Eq (α := 𝒜 ᵍ⊗[R] ℬ)
  (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
    (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
        1))
  (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            1) :
        𝒜 ᵍ⊗[R] ℬ))
Tactic: classical
    rw [← DirectSum.sum_support_decompose 𝒜 a₂, Finset.mul_sum]
    simp_rw [tmul, sum_tmul, map_sum, Finset.mul_sum]
    congr
    ext i
    rw [← SetLike.coe_gOne ℬ, tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul,
      SetLike.coe_gOne, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
rw :
  (a₁ *
        ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1 =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
      ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        1)
rw₁ rw₂ rw₃ :
  (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
        a₁ *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1 =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
      ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        1)
rw₄ :
  Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
      (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
          1))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
      HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
        ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
            ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
              1) :
          𝒜 ᵍ⊗[R] ℬ))
⊢ (a₁ * a₂) ᵍ⊗ₜ[R] 1 = HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) (a₂ ᵍ⊗ₜ[R] 1)
have e_f : Eq (α := ι → 𝒜 ᵍ⊗[R] ℬ)
  (fun (x : ι) ↦
    (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
        1))
  fun (i : ι) ↦
  HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R] 1) :
      𝒜 ᵍ⊗[R] ℬ)
Tactic: classical
    rw [← DirectSum.sum_support_decompose 𝒜 a₂, Finset.mul_sum]
    simp_rw [tmul, sum_tmul, map_sum, Finset.mul_sum]
    congr
    ext i
    rw [← SetLike.coe_gOne ℬ, tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul,
      SetLike.coe_gOne, one_mul]