awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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' := ⋯ })

Tactic:
DirectSum.decompose_lhom_ext ℬ fun i₁ => ?_

Premises used: DirectSum.decompose_lhom_ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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 ℤˣ)
refine :
  ∀ (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)
⊢ 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' := ⋯ })

Tactic:
refine DirectSum.decompose_lhom_ext ℬ fun i₁ => ?_

Premises used: DirectSum.decompose_lhom_ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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₁ : ι
h :
  ∀ (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] ℬ)
⊢ 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)

Tactic:
ext b₁ b₂ : 2
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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
h : 1 ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂) = HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] (↑b₁ : B)) (1 ᵍ⊗ₜ[R] 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] ℬ)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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
h h₁ : Eq (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) (1 ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂))
⊢ 1 ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂) = HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] (↑b₁ : B)) (1 ᵍ⊗ₜ[R] b₂)

Tactic:
rw [tmul_coe_mul_one_tmul]

Premises used: GradedTensorProduct.tmul_coe_mul_one_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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
⊢ Eq (α := 𝒜 ᵍ⊗[R] ℬ) ((algebraMap R (𝒜 ᵍ⊗[R] ℬ) : (a : R) → 𝒜 ᵍ⊗[R] ℬ) r : 𝒜 ᵍ⊗[R] ℬ)
    (1 ᵍ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : 𝒜 ᵍ⊗[R] ℬ)

Tactic:
(includeRight 𝒜 ℬ).commutes r |>.symm

Premises used: GradedTensorProduct.includeRight, AlgHom.commutes, TensorProduct.tmul, Eq.symm, AddCon.toQuotient
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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 : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes :
  ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) (↑a : A) : C) ((g : (a : B) → C) (↑b : B) : C) =
      HPow.hPow (α := ℤˣ) (-1) (j * i) •
        HMul.hMul (α := C) (β := C) ((g : (a : B) → C) (↑b : B) : C) ((f : (a : A) → C) (↑a : A) : C)
a : A
b : B
⊢ (lift 𝒜 ℬ f g h_anti_commutes : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (a ᵍ⊗ₜ[R] b) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a : C) ((g : (a : B) → C) b : C)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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)
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)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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
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
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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
⊢ 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:
simp only [map_one, mul_one, one_mul]

Premises used: map_one, mul_one, one_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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
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
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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
⊢ 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:
simp only [map_one, mul_one, one_mul]

Premises used: map_one, mul_one, one_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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)
a₁ 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)
⊢ 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] ℬ)

Tactic:
rw [← map_mul, tmul_one_mul_one_tmul]

Premises used: GradedTensorProduct.tmul_one_mul_one_tmul, map_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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 g : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
ha : f.comp (includeLeft 𝒜 ℬ) = g.comp (includeLeft 𝒜 ℬ)
hb : f.comp (includeRight 𝒜 ℬ) = g.comp (includeRight 𝒜 ℬ)
⊢ f = g

Tactic:
(liftEquiv 𝒜 ℬ).symm.injective <| Subtype.ext <| Prod.ext ha hb

Premises used: GradedTensorProduct.liftEquiv, Prod.ext, Equiv.injective, Equiv.symm, Subtype.ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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
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
⊢ Eq (α := ℬ ᵍ⊗[R] 𝒜)
    (((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i)) ≪≫ₗ
          LinearEquiv.symm (auxEquiv R ℬ 𝒜) :
        (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜)
      1)
    1

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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
simp_rw₁ :
  Eq (α := ℬ ᵍ⊗[R] 𝒜)
    ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜) 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

Tactic:
simp_rw [auxEquiv_one, gradedComm_one, auxEquiv_symm_one]

Premises used: GradedTensorProduct.auxEquiv_one, GradedTensorProduct.auxEquiv_symm_one, TensorProduct.gradedComm_one