mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
⊢ e ∈ dilatransvections K V ↔ Module.rank K ↥(↑e - LinearMap.id).range ≤ 1

Tactic:
simp only [dilatransvections]

Goal state after:
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
⊢ e ∈ {e | ∃ f v, ↑e = LinearMap.transvection f v} ↔ Module.rank K ↥(↑e - LinearMap.id).range ≤ 1
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = ↑e
hr : Module.rank K ↥u.range = 0
x : V
this : u x = 0
⊢ ↑e x = (LinearMap.transvection 0 0) x

Tactic:
by simp [← hu, this]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ 2 • BilinForm.tmul (associated Q₁) (associated Q₂) =
    ⅟2 • 2 • 2 • (BilinForm.tensorDistrib R A) ((associatedHom A) Q₁ ⊗ₜ[R] (associatedHom R) Q₂)

Tactic:
smul_comm (_ : A) (_ : ℕ),

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ 2 • BilinForm.tmul (associated Q₁) (associated Q₂) =
    2 • ⅟2 • 2 • (BilinForm.tensorDistrib R A) ((associatedHom A) Q₁ ⊗ₜ[R] (associatedHom R) Q₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
hpure_tensor :
  ∀ (v w : V),
    (1 * 1) ⊗ₜ[R] ((ι Q) v * (ι Q) w) + (1 * 1) ⊗ₜ[R] ((ι Q) w * (ι Q) v) =
      ((QuadraticMap.polarBilin (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1
v w : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry
                ((LinearMap.mul A (A ⊗[R] CliffordAlgebra Q)).compl₂
                      (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
                    TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q) +
                  (LinearMap.mul A (A ⊗[R] CliffordAlgebra Q)).flip.compl₂
                      (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
                    TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)))
              1)
            v))
        1)
      w =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry
                (LinearMap.compr₂ (QuadraticMap.polarBilin (QuadraticForm.baseChange A Q))
                  (Algebra.linearMap A (A ⊗[R] CliffordAlgebra Q))))
              1)
            v))
        1)
      w

Tactic:
dsimp

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
hpure_tensor :
  ∀ (v w : V),
    (1 * 1) ⊗ₜ[R] ((ι Q) v * (ι Q) w) + (1 * 1) ⊗ₜ[R] ((ι Q) w * (ι Q) v) =
      ((QuadraticMap.polarBilin (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1
v w : V
⊢ (1 * 1) ⊗ₜ[R] ((ι Q) v * (ι Q) w) + (1 * 1) ⊗ₜ[R] ((ι Q) w * (ι Q) v) =
    QuadraticMap.polar (⇑(QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ ↑(opLinearEquiv A))
        (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      (↑(toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)

Tactic:
dsimp

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A ≪≫ₗ (opLinearEquiv A).symm))
        (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      ((toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ r : R
v : R × R
⊢ { re := 0, imI := (r • v).1, imJ := (r • v).2, imK := 0 } =
    (RingHom.id R) r • { re := 0, imI := v.1, imJ := v.2, imK := 0 }

Tactic:
dsimp

Goal state after:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ r : R
v : R × R
⊢ { re := 0, imI := r * v.1, imJ := r * v.2, imK := 0 } = { re := r * 0, imI := r * v.1, imJ := r * v.2, imK := r * 0 }
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { toFun := fun v ↦ { re := 0, imI := v.1, imJ := v.2, imK := 0 }, map_add' := ⋯, map_smul' := ⋯ } v *
      { toFun := fun v ↦ { re := 0, imI := v.1, imJ := v.2, imK := 0 }, map_add' := ⋯, map_smul' := ⋯ } v =
    (algebraMap R ℍ[R,c₁,c₂]) ((Q c₁ c₂) v)

Tactic:
dsimp

Goal state after:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
      imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
      imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
      imK := 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 } =
    ↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case re
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 }.re =
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2))).re

Tactic:
dsimp

Goal state after:
case re
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0 = c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case imI
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 }.imI =
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2))).imI

Tactic:
dsimp

Goal state after:
case imI
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2 = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case imJ
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 }.imJ =
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2))).imJ

Tactic:
dsimp

Goal state after:
case imJ
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1 = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case imK
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 }.imK =
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2))).imK

Tactic:
dsimp

Goal state after:
case imK
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
q : ℍ[R,c₁,c₂]
⊢ CliffordAlgebraQuaternion.equiv (ofQuaternion (star q)) = CliffordAlgebraQuaternion.equiv (star (ofQuaternion q))

Tactic:
rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion,
      toQuaternion_ofQuaternion]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case snd.refine_4
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
x : R
hx : M →ₗ[R] A
_c : hx ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * hx m = Q m • hx m₁
⊢ (f.bilin m₁) m * (x • hx) m = Q m • (x • hx) m₁

Tactic:
rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q'
⊢ (changeForm h) ((changeForm ⋯) x) = x

Tactic:
by
      exact (changeForm_changeForm _ _ x).trans <|
        by simp_rw [(neg_add_cancel B), changeForm_self_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i✝ : ι × ι
⊢ (((AlgebraTensorModule.curry
            ((gradedCommAux R 𝒜 ℬ ∘ₗ gradedCommAux R ℬ 𝒜) ∘ₗ lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) i))
          a)
        b)
      i✝ =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) i)) a) b) i✝

Tactic:
dsimp

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i✝ : ι × ι
⊢ ((gradedCommAux R 𝒜 ℬ) ((gradedCommAux R ℬ 𝒜) ((lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) i) (a ⊗ₜ[R] b)))) i✝ =
    ((lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) i) (a ⊗ₜ[R] b)) i✝
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
⊢ gradedCommAux R 𝒜 ℬ ∘ₗ gradedCommAux R ℬ 𝒜 = LinearMap.id

Tactic:
ext i a b
  dsimp
  rw [gradedCommAux_lof_tmul, LinearMap.map_smul_of_tower, gradedCommAux_lof_tmul, smul_smul,
    mul_comm i.2 i.1, Int.units_mul_self, one_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a✝ : ⨁ (i : ι), 𝒜 i
b : ℬ 0
i : ι
a : 𝒜 i
⊢ ((↑(gradedComm R 𝒜 ℬ) ∘ₗ (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)).flip ((lof R ι ℬ 0) b)) ∘ₗ lof R ι 𝒜 i) a =
    ((mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)) ((lof R ι ℬ 0) b) ∘ₗ lof R ι 𝒜 i) a

Tactic:
dsimp

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a✝ : ⨁ (i : ι), 𝒜 i
b : ℬ 0
i : ι
a : 𝒜 i
⊢ (gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ 0) b) = (lof R ι ℬ 0) b ⊗ₜ[R] (lof R ι 𝒜 i) a
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a : 𝒜 0
b✝ : ⨁ (i : ι), ℬ i
i : ι
b : ℬ i
⊢ ((↑(gradedComm R 𝒜 ℬ) ∘ₗ (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)) ((lof R ι 𝒜 0) a)) ∘ₗ lof R ι ℬ i) b =
    ((mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)).flip ((lof R ι 𝒜 0) a) ∘ₗ lof R ι ℬ i) b

Tactic:
dsimp

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a : 𝒜 0
b✝ : ⨁ (i : ι), ℬ i
i : ι
b : ℬ i
⊢ (gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 0) a ⊗ₜ[R] (lof R ι ℬ i) b) = (lof R ι ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0) a
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
j₁ i₂ : ι
a₁ : ⨁ (i : ι), 𝒜 i
b₁ : ℬ j₁
a₂ : 𝒜 i₂
b₂ : ⨁ (i : ι), ℬ i
⊢ ↑↑((-1) ^ (i₂ * j₁)) •
      (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)))
        ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm
          (a₁ ⊗ₜ[R]
            (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i))
              ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₁) b₁ ⊗ₜ[R] b₂))) =
    ↑↑((-1) ^ (i₂ * j₁)) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)

Tactic:
dsimp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
⊢ ((AlgebraTensorModule.curry ((gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) ∘ₗ lof R ι 𝒜 ia) a ∘ₗ
        lof R ι ℬ ib)
      b =
    ((AlgebraTensorModule.curry (DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r) ∘ₗ lof R ι 𝒜 ia) a ∘ₗ
        lof R ι ℬ ib)
      b

Tactic:
dsimp

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
⊢ ((gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) ((lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b) =
    r • (lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ ((AlgebraTensorModule.curry ((gradedMul R 𝒜 ℬ).flip ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) ∘ₗ lof R ι 𝒜 i✝¹)
          x✝¹ ∘ₗ
        lof R ι ℬ i✝)
      x✝ =
    ((AlgebraTensorModule.curry (DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r) ∘ₗ lof R ι 𝒜 i✝¹)
          x✝¹ ∘ₗ
        lof R ι ℬ i✝)
      x✝

Tactic:
dsimp

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ ((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝)) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) =
    r • (lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ ((AlgebraTensorModule.curry
              (((AlgebraTensorModule.curry ((gradedMul R 𝒜 ℬ).compr₂ ↑(gradedComm R 𝒜 ℬ)) ∘ₗ lof R ι 𝒜 i₁) a₁ ∘ₗ
                  lof R ι ℬ j₁)
                b₁) ∘ₗ
            lof R ι 𝒜 i₂)
          a₂ ∘ₗ
        lof R ι ℬ j₂)
      b₂ =
    ((AlgebraTensorModule.curry
              (((AlgebraTensorModule.curry ((gradedMul R ℬ 𝒜 ∘ₗ ↑(gradedComm R 𝒜 ℬ)).compl₂ ↑(gradedComm R 𝒜 ℬ)) ∘ₗ
                      lof R ι 𝒜 i₁)
                    a₁ ∘ₗ
                  lof R ι ℬ j₁)
                b₁) ∘ₗ
            lof R ι 𝒜 i₂)
          a₂ ∘ₗ
        lof R ι ℬ j₂)
      b₂

Tactic:
dsimp

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (gradedComm R 𝒜 ℬ)
      (((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 i₁) a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁)) ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₂) b₂)) =
    ((gradedMul R ℬ 𝒜) ((gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i₁) a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁)))
      ((gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₂) b₂))
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (-1) ^ (j₁ * i₂) •
      (of R 𝒜 ℬ)
        ((↑(decomposeAlgEquiv 𝒜)).symm ((decompose 𝒜) a₁ * (DirectSum.of (fun x ↦ ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R]
          (↑(decomposeAlgEquiv ℬ)).symm ((DirectSum.of (fun x ↦ ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂)) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))

Tactic:
dsimp

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (-1) ^ (j₁ * i₂) •
      (of R 𝒜 ℬ)
        ((decompose 𝒜).symm ((decompose 𝒜) a₁ * (DirectSum.of (fun x ↦ ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R]
          (decompose ℬ).symm ((DirectSum.of (fun x ↦ ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂)) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
i₁ : ι
b₁ : ↥(ℬ i₁)
b₂ : B
⊢ (((LinearMap.mul R B).compr₂ { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ (ℬ i₁).subtype) b₁)
      b₂ =
    (((LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ }).compl₂
            { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
          (ℬ i₁).subtype)
        b₁)
      b₂

Tactic:
dsimp

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
i₁ : ι
b₁ : ↥(ℬ i₁)
b₂ : B
⊢ 1 ᵍ⊗ₜ[R] (↑b₁ * b₂) = 1 ᵍ⊗ₜ[R] ↑b₁ * 1 ᵍ⊗ₜ[R] b₂