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 ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (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)) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B))) :
            ((⨁ (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)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂))) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂))
have dsimp : (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
    (((LinearEquiv.symm
            (TensorProduct.congr (↑(decomposeAlgEquiv 𝒜) : A ≃ₗ[R] ⨁ (i : ι), ↥(𝒜 i))
              (↑(decomposeAlgEquiv ℬ) : B ≃ₗ[R] ⨁ (i : ι), ↥(ℬ i))) :
          ((⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) ≃ₗ[R] A ⊗[R] B) :
        (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → A ⊗[R] B)
      ((((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)) a₁ ⊗ₜ[R]
                (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) (↑b₁ : B)) :
            ((⨁ (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)) (↑a₂ : A) ⊗ₜ[R] (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂))) =
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[R] ℬ)
Tactic: dsimp [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 ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          (((LinearEquiv.symm (↑(decomposeAlgEquiv 𝒜) : A ≃ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) : (⨁ (i : ι), ↥(𝒜 i)) ≃ₗ[R] A) :
                (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
              (HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
                ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₁ : ⨁ (i : ι), ↥(𝒜 i))
                (((DirectSum.of.{u_2, u_3} (fun (x : ι) ↦ ↥(𝒜 x)) i₂ : ↥(𝒜 i₂) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 i₂)) → ⨁ (i : ι), ↥(𝒜 i))
                    a₂ :
                  ⨁ (i : ι), ↥(𝒜 i))) ⊗ₜ[R]
            ((LinearEquiv.symm (↑(decomposeAlgEquiv ℬ) : B ≃ₗ[R] ⨁ (i : ι), ↥(ℬ i)) : (⨁ (i : ι), ↥(ℬ i)) ≃ₗ[R] B) :
                (a : ⨁ (i : ι), ↥(ℬ i)) → B)
              (HMul.hMul (α := ⨁ (i : ι), ↥(ℬ i)) (β := ⨁ (i : ι), ↥(ℬ i))
                (((DirectSum.of.{u_2, u_4} (fun (x : ι) ↦ ↥(ℬ x)) j₁ : ↥(ℬ j₁) →+ ⨁ (i : ι), ↥(ℬ i)) :
                      (a : ↥(ℬ j₁)) → ⨁ (i : ι), ↥(ℬ i))
                    b₁ :
                  ⨁ (i : ι), ↥(ℬ i))
                ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂ : ⨁ (i : ι), ↥(ℬ i)))) :
        𝒜 ᵍ⊗[R] ℬ) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[R] ℬ)
have dsimp : HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
            (HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₁ : ⨁ (i : ι), ↥(𝒜 i))
              (((DirectSum.of.{u_2, u_3} (fun (x : ι) ↦ ↥(𝒜 x)) i₂ : ↥(𝒜 i₂) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 i₂)) → ⨁ (i : ι), ↥(𝒜 i))
                  a₂ :
                ⨁ (i : ι), ↥(𝒜 i))) ⊗ₜ[R]
          (Equiv.symm (decompose ℬ) : (a : ⨁ (i : ι), ↥(ℬ i)) → B)
            (HMul.hMul (α := ⨁ (i : ι), ↥(ℬ i)) (β := ⨁ (i : ι), ↥(ℬ i))
              (((DirectSum.of.{u_2, u_4} (fun (x : ι) ↦ ↥(ℬ x)) j₁ : ↥(ℬ j₁) →+ ⨁ (i : ι), ↥(ℬ i)) :
                    (a : ↥(ℬ j₁)) → ⨁ (i : ι), ↥(ℬ i))
                  b₁ :
                ⨁ (i : ι), ↥(ℬ i))
              ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂ : ⨁ (i : ι), ↥(ℬ i)))) :
      𝒜 ᵍ⊗[R] ℬ) =
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[R] ℬ)
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 ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
              (HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
                ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₁ : ⨁ (i : ι), ↥(𝒜 i))
                (((DirectSum.of.{u_2, u_3} (fun (x : ι) ↦ ↥(𝒜 x)) i₂ : ↥(𝒜 i₂) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 i₂)) → ⨁ (i : ι), ↥(𝒜 i))
                    a₂ :
                  ⨁ (i : ι), ↥(𝒜 i))) ⊗ₜ[R]
            (Equiv.symm (decompose ℬ) : (a : ⨁ (i : ι), ↥(ℬ i)) → B)
              (HMul.hMul (α := ⨁ (i : ι), ↥(ℬ i)) (β := ⨁ (i : ι), ↥(ℬ i))
                (((DirectSum.of.{u_2, u_4} (fun (x : ι) ↦ ↥(ℬ x)) j₁ : ↥(ℬ j₁) →+ ⨁ (i : ι), ↥(ℬ i)) :
                      (a : ↥(ℬ j₁)) → ⨁ (i : ι), ↥(ℬ i))
                    b₁ :
                  ⨁ (i : ι), ↥(ℬ i))
                ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂ : ⨁ (i : ι), ↥(ℬ i)))) :
        𝒜 ᵍ⊗[R] ℬ) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[R] ℬ)
have simp_rw : HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        (HMul.hMul (α := A) (β := A)
            ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
                ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₁ : ⨁ (i : ι), ↥(𝒜 i)) :
              A)
            ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
                (((DirectSum.of.{u_2, u_3} (fun (x : ι) ↦ ↥(𝒜 x)) i₂ : ↥(𝒜 i₂) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 i₂)) → ⨁ (i : ι), ↥(𝒜 i))
                    a₂ :
                  ⨁ (i : ι), ↥(𝒜 i)) :
              A) ⊗ₜ[R]
          HMul.hMul (α := B) (β := B)
            ((Equiv.symm (decompose ℬ) : (a : ⨁ (i : ι), ↥(ℬ i)) → B)
                (((DirectSum.of.{u_2, u_4} (fun (x : ι) ↦ ↥(ℬ x)) j₁ : ↥(ℬ j₁) →+ ⨁ (i : ι), ↥(ℬ i)) :
                      (a : ↥(ℬ j₁)) → ⨁ (i : ι), ↥(ℬ i))
                    b₁ :
                  ⨁ (i : ι), ↥(ℬ i)) :
              B)
            ((Equiv.symm (decompose ℬ) : (a : ⨁ (i : ι), ↥(ℬ i)) → B)
                ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂ : ⨁ (i : ι), ↥(ℬ i)) :
              B)) :
      𝒜 ᵍ⊗[R] ℬ) =
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[R] ℬ)
Tactic: simp_rw [decompose_symm_mul, decompose_symm_of, Equiv.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 ℤˣ)
i₂ : ι
a₁ : A
b₁ : ↥(ℬ 0)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
have rw : HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (0 * i₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
  (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
Tactic: rw [tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, 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 ℤˣ)
i₂ : ι
a₁ : A
b₁ : ↥(ℬ 0)
a₂ : ↥(𝒜 i₂)
b₂ : B
rw :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (0 * i₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
have rw₁ : HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
    ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
  (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
Tactic: rw [tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, 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 ℤˣ)
i₂ : ι
a₁ : A
b₁ : ↥(ℬ 0)
a₂ : ↥(𝒜 i₂)
b₂ : B
rw :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (0 * i₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₁ :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
      ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
have rw₂ : HSMul.hSMul (α := ℤˣ) (β := 𝒜 ᵍ⊗[R] ℬ) 1 ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
  (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
Tactic: rw [tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, 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 ℤˣ)
i₂ : ι
a₁ : A
b₁ : ↥(ℬ 0)
a₂ : ↥(𝒜 i₂)
b₂ : B
rw :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (0 * i₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₁ :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
      ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₂ :
  HSMul.hSMul (α := ℤˣ) (β := 𝒜 ᵍ⊗[R] ℬ) 1 ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
have rw₃ : Eq (α := 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂))
Tactic: rw [tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, 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 ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 0)
b₂ : B
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
have rw : HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * 0)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
  (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
Tactic: rw [tmul_coe_mul_coe_tmul, mul_zero, uzpow_zero, 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 ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 0)
b₂ : B
rw :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * 0)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
have rw₁ : HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
    ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
  (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
Tactic: rw [tmul_coe_mul_coe_tmul, mul_zero, uzpow_zero, 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 ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 0)
b₂ : B
rw :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * 0)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₁ :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
      ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
have rw₂ : HSMul.hSMul (α := ℤˣ) (β := 𝒜 ᵍ⊗[R] ℬ) 1 ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
  (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
Tactic: rw [tmul_coe_mul_coe_tmul, mul_zero, uzpow_zero, 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 ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 0)
b₂ : B
rw :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * 0)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₁ :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
      ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₂ :
  HSMul.hSMul (α := ℤˣ) (β := 𝒜 ᵍ⊗[R] ℬ) 1 ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
have rw₃ : Eq (α := 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂))
Tactic: rw [tmul_coe_mul_coe_tmul, mul_zero, uzpow_zero, 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 ℤˣ)
i₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] b₂
have h : b₂ = (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) * b₂
Tactic: convert! tmul_zero_coe_mul_coe_tmul 𝒜 ℬ a₁ (@GradedMonoid.GOne.one _ (ℬ ·) _ _) a₂ b₂
-- 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₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ b₂ = (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) * b₂
have h : b₂ = 1 * 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 ℤˣ)
i₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
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 ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) (1 ᵍ⊗ₜ[R] b₂) = a₁ ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
have h : a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)
Tactic: convert! tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ b₁ (@GradedMonoid.GOne.one _ (𝒜 ·) _ _) b₂
-- 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 ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
⊢ a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)
have h : a₁ = a₁ * 1
Tactic: rw [SetLike.coe_gOne, mul_one]
-- 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 ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
h : a₁ = a₁ * 1
⊢ a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)
have h₁ : a₁ = a₁
Tactic: rw [SetLike.coe_gOne, mul_one]
-- 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
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] b₂) = a₁ ᵍ⊗ₜ[R] b₂
have h : a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)
Tactic: convert!
    tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ (GradedMonoid.GOne.one (A := (ℬ ·)))
      (GradedMonoid.GOne.one (A := (𝒜 ·))) b₂
-- 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 : a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] b₂) = a₁ ᵍ⊗ₜ[R] b₂
have h₁ : b₂ = (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) * b₂
Tactic: convert!
    tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ (GradedMonoid.GOne.one (A := (ℬ ·)))
      (GradedMonoid.GOne.one (A := (𝒜 ·))) b₂
-- 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
⊢ a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)
have h : a₁ = a₁ * 1
Tactic: rw [SetLike.coe_gOne, mul_one]
-- 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 : a₁ = a₁ * 1
⊢ a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)
have h₁ : a₁ = a₁
Tactic: rw [SetLike.coe_gOne, mul_one]
-- 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
⊢ b₂ = (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) * b₂
have h : b₂ = 1 * b₂
Tactic: rw [SetLike.coe_gOne, one_mul]