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 ℬ
rw :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) 1))
    1
rw₁ :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
        ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (1 ⊗ₜ[R] 1)) :
      (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    (1 : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
⊢ Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) 1
have rw₂ : Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
  ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1 ⊗ₜ[R] (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) 1
Tactic: rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one,
    DirectSum.decompose_one, Algebra.TensorProduct.one_def]
-- 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 ℬ
rw :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) 1))
    1
rw₁ :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
        ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (1 ⊗ₜ[R] 1)) :
      (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    (1 : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
rw₂ :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1 ⊗ₜ[R] (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) 1
⊢ Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) 1
have rw₃ : Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (1 ⊗ₜ[R] (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) 1
Tactic: rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one,
    DirectSum.decompose_one, Algebra.TensorProduct.one_def]
-- 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 ℬ
rw :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) 1))
    1
rw₁ :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
        ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (1 ⊗ₜ[R] 1)) :
      (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    (1 : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
rw₂ :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1 ⊗ₜ[R] (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) 1
rw₃ : Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (1 ⊗ₜ[R] (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) 1
⊢ Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) 1
have rw₄ : Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (1 ⊗ₜ[R] 1) 1
Tactic: rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one,
    DirectSum.decompose_one, Algebra.TensorProduct.one_def]
-- 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 ℬ
rw :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) 1))
    1
rw₁ :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
        ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (1 ⊗ₜ[R] 1)) :
      (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    (1 : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
rw₂ :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1 ⊗ₜ[R] (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) 1
rw₃ : Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (1 ⊗ₜ[R] (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) 1
rw₄ : Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (1 ⊗ₜ[R] 1) 1
⊢ Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) 1
have rw₅ : Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] 1)
Tactic: rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one,
    DirectSum.decompose_one, Algebra.TensorProduct.one_def]
-- 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 ℤˣ)
fAB1 : 𝒜 ᵍ⊗[R] ℬ ≃ₗ[R] (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i) := auxEquiv R 𝒜 ℬ
⊢ 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ
have have : (this : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ
Tactic: have := ((gradedMul R (𝒜 ·) (ℬ ·)).compl₁₂ fAB1.toLinearMap fAB1.toLinearMap).compr₂
    fAB1.symm.toLinearMap
-- 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
⊢ 1 * x = x
have rw : ((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) 1 : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ) x = x
Tactic: rw [mul_def, mulHom_apply, auxEquiv_one, one_gradedMul, LinearEquiv.symm_apply_apply]
-- 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
rw : ((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) 1 : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ) x = x
⊢ 1 * x = x
have rw₁ : (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
    (((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
            (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
              ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
          ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) :
        (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
      ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) =
  x
Tactic: rw [mul_def, mulHom_apply, auxEquiv_one, one_gradedMul, LinearEquiv.symm_apply_apply]
-- 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
rw : ((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) 1 : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ) x = x
rw₁ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      (((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
              (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
            ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) =
    x
⊢ 1 * x = x
have rw₂ : (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
    (((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
            (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
              ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
          1 :
        (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
      ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) =
  x
Tactic: rw [mul_def, mulHom_apply, auxEquiv_one, one_gradedMul, LinearEquiv.symm_apply_apply]
-- 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
rw : ((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) 1 : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ) x = x
rw₁ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      (((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
              (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
            ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) =
    x
rw₂ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      (((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
              (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
            1 :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) =
    x
⊢ 1 * x = x
have rw₃ : (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) =
  x
Tactic: rw [mul_def, mulHom_apply, auxEquiv_one, one_gradedMul, LinearEquiv.symm_apply_apply]
-- 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
rw : ((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) 1 : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ) x = x
rw₁ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      (((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
              (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
            ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) =
    x
rw₂ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      (((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
              (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
            1 :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) =
    x
rw₃ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) =
    x
⊢ 1 * x = x
have rw₄ : x = x
Tactic: rw [mul_def, mulHom_apply, auxEquiv_one, one_gradedMul, LinearEquiv.symm_apply_apply]
-- 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
⊢ x * 1 = x
have rw : (((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) x : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
      (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ)
    1 =
  x
Tactic: rw [mul_def, mulHom_apply, auxEquiv_one, gradedMul_one, LinearEquiv.symm_apply_apply]
-- 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
rw :
  (((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) x : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
        (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ)
      1 =
    x
⊢ x * 1 = x
have rw₁ : (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
    ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
              (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
            ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
          ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
        (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
      ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1)) =
  x
Tactic: rw [mul_def, mulHom_apply, auxEquiv_one, gradedMul_one, LinearEquiv.symm_apply_apply]
-- 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
rw :
  (((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) x : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
        (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ)
      1 =
    x
rw₁ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
                (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                  ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
              ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
            ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1)) =
    x
⊢ x * 1 = x
have rw₂ : (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
    ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
              (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
            ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
          ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
        (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
      1) =
  x
Tactic: rw [mul_def, mulHom_apply, auxEquiv_one, gradedMul_one, LinearEquiv.symm_apply_apply]
-- 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
rw :
  (((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) x : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
        (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ)
      1 =
    x
rw₁ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
                (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                  ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
              ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
            ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1)) =
    x
rw₂ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
                (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                  ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
              ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
            ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        1) =
    x
⊢ x * 1 = x
have rw₃ : (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) =
  x
Tactic: rw [mul_def, mulHom_apply, auxEquiv_one, gradedMul_one, LinearEquiv.symm_apply_apply]
-- 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
rw :
  (((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) x : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
        (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ)
      1 =
    x
rw₁ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
                (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                  ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
              ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
            ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1)) =
    x
rw₂ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
                (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                  ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
              ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
            ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        1) =
    x
rw₃ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) =
    x
⊢ x * 1 = x
have rw₄ : x = x
Tactic: rw [mul_def, mulHom_apply, auxEquiv_one, gradedMul_one, LinearEquiv.symm_apply_apply]