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 ℤˣ)
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)
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)
⊢ 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) •
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑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]
-- 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)
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)
rw₅ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B)) : 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) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B)) =
  HPow.hPow (α := ℤˣ) (-1) (j * i) •
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑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]
-- 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
fg :
  { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
    ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
      HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C) ((fg.2 : (a : B) → C) (↑b : B) : C) =
        HPow.hPow (α := ℤˣ) (-1) (j * i) •
          HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C) ((fg.1 : (a : A) → C) (↑a : A) : C) }
x : A
⊢ Eq.{u_5 + 1} (α := C)
    (((↑((fun (F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C) ↦
                    (Subtype.mk (p := fun (fg : (A →ₐ[R] C) × (B →ₐ[R] C)) ↦
                        ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                          HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C)
                              ((fg.2 : (a : B) → C) (↑b : B) : C) =
                            HPow.hPow (α := ℤˣ) (-1) (j * i) •
                              HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                                ((fg.1 : (a : A) → C) (↑a : A) : C))
                        (F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)) ⋯ :
                      { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
                        ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                          HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C)
                              ((fg.2 : (a : B) → C) (↑b : B) : C) =
                            HPow.hPow (α := ℤˣ) (-1) (j * i) •
                              HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                                ((fg.1 : (a : A) → C) (↑a : A) : C) }))
                  ((fun
                        (fg :
                          { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
                            ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                              HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C)
                                  ((fg.2 : (a : B) → C) (↑b : B) : C) =
                                HPow.hPow (α := ℤˣ) (-1) (j * i) •
                                  HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                                    ((fg.1 : (a : A) → C) (↑a : A) : C) }) ↦
                      (lift 𝒜 ℬ (↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).2 ⋯ :
                        𝒜 ᵍ⊗[R] ℬ →ₐ[R] C))
                    fg)) :
              (A →ₐ[R] C) × (B →ₐ[R] C)).1 :
          (a : A) → C)
        x :
      C)
    (((↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).1 : (a : A) → C) x : C)
have a : HMul.hMul (α := C) (β := C) (((↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).1 : (a : A) → C) x : C)
    (((↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).2 : (a : B) → C) 1 : C) =
  ((↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).1 : (a : A) → C) x
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
fg :
  { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
    ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
      HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C) ((fg.2 : (a : B) → C) (↑b : B) : C) =
        HPow.hPow (α := ℤˣ) (-1) (j * i) •
          HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C) ((fg.1 : (a : A) → C) (↑a : A) : C) }
x : B
⊢ Eq.{u_5 + 1} (α := C)
    (((↑((fun (F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C) ↦
                    (Subtype.mk (p := fun (fg : (A →ₐ[R] C) × (B →ₐ[R] C)) ↦
                        ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                          HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C)
                              ((fg.2 : (a : B) → C) (↑b : B) : C) =
                            HPow.hPow (α := ℤˣ) (-1) (j * i) •
                              HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                                ((fg.1 : (a : A) → C) (↑a : A) : C))
                        (F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)) ⋯ :
                      { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
                        ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                          HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C)
                              ((fg.2 : (a : B) → C) (↑b : B) : C) =
                            HPow.hPow (α := ℤˣ) (-1) (j * i) •
                              HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                                ((fg.1 : (a : A) → C) (↑a : A) : C) }))
                  ((fun
                        (fg :
                          { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
                            ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                              HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C)
                                  ((fg.2 : (a : B) → C) (↑b : B) : C) =
                                HPow.hPow (α := ℤˣ) (-1) (j * i) •
                                  HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                                    ((fg.1 : (a : A) → C) (↑a : A) : C) }) ↦
                      (lift 𝒜 ℬ (↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).2 ⋯ :
                        𝒜 ᵍ⊗[R] ℬ →ₐ[R] C))
                    fg)) :
              (A →ₐ[R] C) × (B →ₐ[R] C)).2 :
          (a : B) → C)
        x :
      C)
    (((↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).2 : (a : B) → C) x : C)
have a : HMul.hMul (α := C) (β := C) (((↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).1 : (a : A) → C) 1 : C)
    (((↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).2 : (a : B) → C) x : C) =
  ((↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).2 : (a : B) → C) x
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
x : A
x_1 : B
⊢ HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (x ᵍ⊗ₜ[R] 1) : C)
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] x_1) : C) =
    (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (x ⊗ₜ[R] x_1) : 𝒜 ᵍ⊗[R] ℬ)
have a : Eq.{u_5 + 1} (α := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (x ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] x_1)) : C)
  ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (x ⊗ₜ[R] x_1) : 𝒜 ᵍ⊗[R] ℬ) : C)
Tactic: rw [← map_mul, tmul_one_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
x : A
x_1 : B
a :
  Eq.{u_5 + 1} (α := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (x ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] x_1)) : C)
    ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (x ⊗ₜ[R] x_1) : 𝒜 ᵍ⊗[R] ℬ) : C)
⊢ HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (x ᵍ⊗ₜ[R] 1) : C)
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] x_1) : C) =
    (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (x ⊗ₜ[R] x_1) : 𝒜 ᵍ⊗[R] ℬ)
have a₁ : Eq.{u_5 + 1} (α := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (x ᵍ⊗ₜ[R] x_1) : C)
  ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (x ⊗ₜ[R] x_1) : 𝒜 ᵍ⊗[R] ℬ) : C)
Tactic: rw [← map_mul, tmul_one_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.445607
inst_10 : Ring C
inst_11 : Algebra R C
⊢ Eq (α := ℬ ᵍ⊗[R] 𝒜)
    (((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i)) ≪≫ₗ
          LinearEquiv.symm (auxEquiv R ℬ 𝒜) :
        (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜)
      1)
    1
have dsimp : Eq (α := ℬ ᵍ⊗[R] 𝒜)
  ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
    ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
        (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1)))
  1
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.445607
inst_10 : Ring C
inst_11 : Algebra R C
⊢ Eq (α := ℬ ᵍ⊗[R] 𝒜)
    ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
      ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
          (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1)))
    1
have simp_rw : Eq (α := ℬ ᵍ⊗[R] 𝒜)
  ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
    ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
        (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      1))
  1
Tactic: simp_rw [auxEquiv_one, gradedComm_one, auxEquiv_symm_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 ℤˣ)
C : Type ?u.445607
inst_10 : Ring C
inst_11 : Algebra R C
simp_rw :
  Eq (α := ℬ ᵍ⊗[R] 𝒜)
    ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
      ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
          (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
        1))
    1
⊢ Eq (α := ℬ ᵍ⊗[R] 𝒜)
    ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
      ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
          (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1)))
    1
have simp_rw₁ : Eq (α := ℬ ᵍ⊗[R] 𝒜)
  ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜) 1) 1
Tactic: simp_rw [auxEquiv_one, gradedComm_one, auxEquiv_symm_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 ℤˣ)
C : Type ?u.445607
inst_10 : Ring C
inst_11 : Algebra R C
x y : 𝒜 ᵍ⊗[R] ℬ
⊢ ((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i)) ≪≫ₗ LinearEquiv.symm (auxEquiv R ℬ 𝒜) :
        (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜)
      (x * y) =
    HMul.hMul (α := ℬ ᵍ⊗[R] 𝒜) (β := ℬ ᵍ⊗[R] 𝒜)
      (((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i)) ≪≫ₗ
              LinearEquiv.symm (auxEquiv R ℬ 𝒜) :
            (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜)
          x :
        ℬ ᵍ⊗[R] 𝒜)
      (((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i)) ≪≫ₗ
              LinearEquiv.symm (auxEquiv R ℬ 𝒜) :
            (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜)
          y :
        ℬ ᵍ⊗[R] 𝒜)
have dsimp : (LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
    ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
        (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (x * y))) =
  HMul.hMul (α := ℬ ᵍ⊗[R] 𝒜) (β := ℬ ᵍ⊗[R] 𝒜)
    ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
        ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
            (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
          ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) :
      ℬ ᵍ⊗[R] 𝒜)
    ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
        ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
            (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
          ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) y)) :
      ℬ ᵍ⊗[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 ℤˣ)
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ Eq (α := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
    ((auxEquiv R ℬ 𝒜 : (a : ℬ ᵍ⊗[R] 𝒜) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
        ((comm 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B))) :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
    ((auxEquiv R ℬ 𝒜 : (a : ℬ ᵍ⊗[R] 𝒜) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
        (HSMul.hSMul (β := ℬ ᵍ⊗[R] 𝒜) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((↑b : B) ᵍ⊗ₜ[R] (↑a : A))) :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
have simp_rw : HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
    (((lof.{u_1, u_2, u_4} R ι (fun (x : ι) ↦ ↥(ℬ x)) j : ↥(ℬ j) →ₗ[R] ⨁ (i : ι), ↥(ℬ i)) :
            (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
          b ⊗ₜ[R]
        ((lof.{u_1, u_2, u_3} R ι (fun (x : ι) ↦ ↥(𝒜 x)) i : ↥(𝒜 i) →ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          a :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) =
  (auxEquiv R ℬ 𝒜 : (a : ℬ ᵍ⊗[R] 𝒜) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
    (HSMul.hSMul (α := R) (β := ℬ ᵍ⊗[R] 𝒜) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R) ((↑b : B) ᵍ⊗ₜ[R] (↑a : A)))
Tactic: simp_rw [auxEquiv_comm, auxEquiv_tmul, decompose_coe, ← lof_eq_of R, gradedComm_of_tmul_of,
      @Units.smul_def _ _ (_) (_), ← Int.cast_smul_eq_zsmul R]
-- 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 j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      (((lof.{u_1, u_2, u_4} R ι (fun (x : ι) ↦ ↥(ℬ x)) j : ↥(ℬ j) →ₗ[R] ⨁ (i : ι), ↥(ℬ i)) :
              (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
            b ⊗ₜ[R]
          ((lof.{u_1, u_2, u_3} R ι (fun (x : ι) ↦ ↥(𝒜 x)) i : ↥(𝒜 i) →ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            a :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) =
    (auxEquiv R ℬ 𝒜 : (a : ℬ ᵍ⊗[R] 𝒜) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (HSMul.hSMul (α := R) (β := ℬ ᵍ⊗[R] 𝒜) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
        ((↑b : B) ᵍ⊗ₜ[R] (↑a : A)))
have rw : HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
    (((lof.{u_1, u_2, u_4} R ι (fun (x : ι) ↦ ↥(ℬ x)) j : ↥(ℬ j) →ₗ[R] ⨁ (i : ι), ↥(ℬ i)) :
            (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
          b ⊗ₜ[R]
        ((lof.{u_1, u_2, u_3} R ι (fun (x : ι) ↦ ↥(𝒜 x)) i : ↥(𝒜 i) →ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          a :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) =
  HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
    (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
    ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) (↑b : B) ⊗ₜ[R] (decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
Tactic: rw [LinearEquiv.map_smul, auxEquiv_tmul]