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 ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ)
      ((RingHom.comp (includeLeftRingHom 𝒜 ℬ) (algebraMap R A) : (a : R) → 𝒜 ᵍ⊗[R] ℬ) r : 𝒜 ᵍ⊗[R] ℬ) x =
    HMul.hMul (β := 𝒜 ᵍ⊗[R] ℬ) x
      ((RingHom.comp (includeLeftRingHom 𝒜 ℬ) (algebraMap R A) : (a : R) → 𝒜 ᵍ⊗[R] ℬ) r : 𝒜 ᵍ⊗[R] ℬ)
have dsimp : Eq (α := 𝒜 ᵍ⊗[R] ℬ)
  ((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))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((algebraMap R A : (a : R) → A) r) ⊗ₜ[R]
                (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) :
            ((⨁ (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)) x)) :
    𝒜 ᵍ⊗[R] ℬ)
  ((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))
        ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((algebraMap R A : (a : R) → A) r) ⊗ₜ[R]
          (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1)) :
    𝒜 ᵍ⊗[R] ℬ)
Tactic: dsimp [mul_def, mulHom_apply, auxEquiv_tmul]
-- 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 ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ)
      ((RingHom.comp (includeLeftRingHom 𝒜 ℬ) (algebraMap R A) : (a : R) → 𝒜 ᵍ⊗[R] ℬ) r : 𝒜 ᵍ⊗[R] ℬ) x
have dsimp : r • x =
  (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))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((algebraMap R A : (a : R) → A) r) ⊗ₜ[R]
              (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) :
          ((⨁ (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)) x))
Tactic: dsimp [mul_def, mulHom_apply, auxEquiv_tmul]
-- 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 ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x =
    (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))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((algebraMap R A : (a : R) → A) r) ⊗ₜ[R]
                (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) :
            ((⨁ (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)) x))
have simp_rw : r • x =
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
    (HSMul.hSMul (β := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) r
      ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x :
        (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)))
Tactic: simp_rw [DirectSum.decompose_algebraMap, DirectSum.decompose_one, algebraMap_gradedMul]
-- 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 ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x =
    (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      (HSMul.hSMul (β := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) r
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x :
          (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)))
have rw : r • x =
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) r
    ((LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
      𝒜 ᵍ⊗[R] ℬ)
Tactic: rw [LinearEquiv.map_smul]
-- 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 y : B),
    ({ toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } : (a : B) → 𝒜 ᵍ⊗[R] ℬ) (x * y) =
      HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ)
        (({ toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } :
              (a : B) → 𝒜 ᵍ⊗[R] ℬ)
            x :
          𝒜 ᵍ⊗[R] ℬ)
        (({ toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } :
              (a : B) → 𝒜 ᵍ⊗[R] ℬ)
            y :
          𝒜 ᵍ⊗[R] ℬ)
have rw : Eq (α := B →ₗ[R] B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)
  (LinearMap.compr₂ (LinearMap.mul R B) { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := sorry, map_smul' := sorry })
  (LinearMap.compl₂ (σ₄₂ := RingHom.id R)
    (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ
      { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := sorry, map_smul' := sorry : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ })
    { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := sorry, map_smul' := sorry })
Tactic: rw [LinearMap.map_mul_iff]
-- 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 ℤˣ)
⊢ Eq (α := B →ₗ[R] B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)
    (LinearMap.compr₂ (LinearMap.mul R B) { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ })
    (LinearMap.compl₂ (σ₄₂ := RingHom.id R)
      (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ
        { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ })
      { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ })
have refine : ∀ (i₁ : ι),
  Eq (α := ↥(ℬ i₁) →ₗ[R] B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)
    (LinearMap.compr₂ (LinearMap.mul R B)
        { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := sorry, map_smul' := sorry : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } ∘ₗ
      (ℬ i₁).subtype)
    (LinearMap.compl₂ (σ₄₂ := RingHom.id R)
        (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ
          { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := sorry, map_smul' := sorry : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ })
        { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := sorry, map_smul' := sorry : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } ∘ₗ
      (ℬ i₁).subtype)
Tactic: refine DirectSum.decompose_lhom_ext ℬ fun 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 ℤˣ)
i₁ : ι
⊢ Eq (α := ↥(ℬ i₁) →ₗ[R] B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)
    (LinearMap.compr₂ (LinearMap.mul R B)
        { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } ∘ₗ
      (ℬ i₁).subtype)
    (LinearMap.compl₂ (σ₄₂ := RingHom.id R)
        (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ
          { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ })
        { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } ∘ₗ
      (ℬ i₁).subtype)
have h : ∀ (b₁ : ↥(ℬ i₁)) (b₂ : B),
  Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    ((((LinearMap.compr₂ (LinearMap.mul R B)
                    { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := sorry, map_smul' := sorry : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } ∘ₗ
                  (ℬ i₁).subtype :
                (a : ↥(ℬ i₁)) → B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)
              b₁ :
            B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
          (a : B) → 𝒜 ᵍ⊗[R] ℬ)
        b₂ :
      𝒜 ᵍ⊗[R] ℬ)
    ((((LinearMap.compl₂ (σ₄₂ := RingHom.id R)
                    (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ
                      { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := sorry, map_smul' := sorry : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ })
                    { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := sorry, map_smul' := sorry : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } ∘ₗ
                  (ℬ i₁).subtype :
                (a : ↥(ℬ i₁)) → B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)
              b₁ :
            B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
          (a : B) → 𝒜 ᵍ⊗[R] ℬ)
        b₂ :
      𝒜 ᵍ⊗[R] ℬ)
Tactic: ext b₁ b₂ : 2
-- 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 ℤˣ)
i₁ : ι
b₁ : ↥(ℬ i₁)
b₂ : B
⊢ Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    ((((LinearMap.compr₂ (LinearMap.mul R B)
                    { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } ∘ₗ
                  (ℬ i₁).subtype :
                (a : ↥(ℬ i₁)) → B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)
              b₁ :
            B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
          (a : B) → 𝒜 ᵍ⊗[R] ℬ)
        b₂ :
      𝒜 ᵍ⊗[R] ℬ)
    ((((LinearMap.compl₂ (σ₄₂ := RingHom.id R)
                    (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ
                      { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ })
                    { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } ∘ₗ
                  (ℬ i₁).subtype :
                (a : ↥(ℬ i₁)) → B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)
              b₁ :
            B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
          (a : B) → 𝒜 ᵍ⊗[R] ℬ)
        b₂ :
      𝒜 ᵍ⊗[R] ℬ)
have h : 1 ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂) = HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] (↑b₁ : B)) (1 ᵍ⊗ₜ[R] b₂)
Tactic: dsimp
-- 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 ℤˣ)
i₁ : ι
b₁ : ↥(ℬ i₁)
b₂ : B
⊢ 1 ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂) = HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] (↑b₁ : B)) (1 ᵍ⊗ₜ[R] b₂)
have h : Eq (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) (1 ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂))
Tactic: rw [tmul_coe_mul_one_tmul]
-- 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 ℤˣ)
C : Type u_5
inst_10 : Ring C
inst_11 : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ HMul.hMul (α := C) (β := C) (((F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)).1 : (a : A) → C) (↑a : A) : C)
      (((F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)).2 : (a : B) → C) (↑b : B) : C) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) (((F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)).2 : (a : B) → C) (↑b : B) : C)
        (((F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)).1 : (a : A) → C) (↑a : A) : C)
have dsimp : HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
    ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C) =
  HPow.hPow (α := ℤˣ) (-1) (j * i) •
    HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
Tactic: dsimp
-- 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 ℤˣ)
C : Type u_5
inst_10 : Ring C
inst_11 : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
have rw : (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
  HPow.hPow (α := ℤˣ) (-1) (j * i) •
    HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
Tactic: rw [← map_mul, ← map_mul F, tmul_coe_mul_coe_tmul, one_mul, mul_one, AlgHom.map_smul_of_tower,
      tmul_one_mul_one_tmul, smul_smul, Int.units_mul_self, one_smul]
-- 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 ℤˣ)
C : Type u_5
inst_10 : Ring C
inst_11 : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
rw :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
⊢ HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
have rw₁ : (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
  HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
    ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] (↑b : B)) ((↑a : A) ᵍ⊗ₜ[R] 1)) : C)
Tactic: rw [← map_mul, ← map_mul F, tmul_coe_mul_coe_tmul, one_mul, mul_one, AlgHom.map_smul_of_tower,
      tmul_one_mul_one_tmul, smul_smul, Int.units_mul_self, one_smul]
-- 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 ℤˣ)
C : Type u_5
inst_10 : Ring C
inst_11 : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
rw :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
rw₁ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] (↑b : B)) ((↑a : A) ᵍ⊗ₜ[R] 1)) : C)
⊢ HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
have rw₂ : (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
  HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
    ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C)
        (HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((1 * (↑a : A)) ᵍ⊗ₜ[R] ((↑b : B) * 1))) :
      C)
Tactic: rw [← map_mul, ← map_mul F, tmul_coe_mul_coe_tmul, one_mul, mul_one, AlgHom.map_smul_of_tower,
      tmul_one_mul_one_tmul, smul_smul, Int.units_mul_self, one_smul]
-- 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 ℤˣ)
C : Type u_5
inst_10 : Ring C
inst_11 : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
rw :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
rw₁ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] (↑b : B)) ((↑a : A) ᵍ⊗ₜ[R] 1)) : C)
rw₂ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C)
          (HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((1 * (↑a : A)) ᵍ⊗ₜ[R] ((↑b : B) * 1))) :
        C)
⊢ HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
have rw₃ : (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
  HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
    ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C)
        (HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((↑a : A) ᵍ⊗ₜ[R] ((↑b : B) * 1))) :
      C)
Tactic: rw [← map_mul, ← map_mul F, tmul_coe_mul_coe_tmul, one_mul, mul_one, AlgHom.map_smul_of_tower,
      tmul_one_mul_one_tmul, smul_smul, Int.units_mul_self, one_smul]
-- 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 ℤˣ)
C : Type u_5
inst_10 : Ring C
inst_11 : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
rw :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
rw₁ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] (↑b : B)) ((↑a : A) ᵍ⊗ₜ[R] 1)) : C)
rw₂ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C)
          (HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((1 * (↑a : A)) ᵍ⊗ₜ[R] ((↑b : B) * 1))) :
        C)
rw₃ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C)
          (HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((↑a : A) ᵍ⊗ₜ[R] ((↑b : B) * 1))) :
        C)
⊢ HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
have rw₄ : (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
  HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
    ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C)
        (HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B))) :
      C)
Tactic: rw [← map_mul, ← map_mul F, tmul_coe_mul_coe_tmul, one_mul, mul_one, AlgHom.map_smul_of_tower,
      tmul_one_mul_one_tmul, smul_smul, Int.units_mul_self, one_smul]