mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) ((ι Q) m✝ * x✝) =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) ((ι Q) m✝ * x✝) + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) ((ι Q) m✝ * x✝)

Tactic:
rw [foldr'_ι_mul, foldr'_ι_mul, foldr'_ι_mul, hx]
        dsimp only [contractLeftAux_apply_apply]
        rw [sub_add_sub_comm, mul_add, LinearMap.add_apply, add_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : Dual R V
v : V
⊢ LinearMap.baseChange A (transvection f v) = transvection ((Dual.baseChange A) f) (1 ⊗ₜ[R] v)

Tactic:
ext

Goal state after:
R : Type u_3
V : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : Dual R V
v x✝ : V
⊢ ((TensorProduct.AlgebraTensorModule.curry (LinearMap.baseChange A (transvection f v))) 1) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (transvection ((Dual.baseChange A) f) (1 ⊗ₜ[R] v))) 1) x✝
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 : QuadraticForm R M
d : Module.Dual R M
⊢ (contractRight 1) d = 0

Tactic:
by
  simpa only [map_one] using contractRight_algebraMap Q d 1

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ involute = AlgHom.id R (CliffordAlgebra 0)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
x✝ : Unit
⊢ (involute.toLinearMap ∘ₗ ι 0) x✝ = ((AlgHom.id R (CliffordAlgebra 0)).toLinearMap ∘ₗ ι 0) x✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ((lift 0) ⟨0, ⋯⟩).comp (Algebra.ofId R (CliffordAlgebra 0)) = AlgHom.id R R

Tactic:
ext

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

Goal state before:
pp: ⊢ ofComplex.comp toComplex = AlgHom.id ℝ (CliffordAlgebra Q)

Tactic:
ext

Goal state after:
⊢ ((ofComplex.comp toComplex).toLinearMap ∘ₗ ι Q) 1 = ((AlgHom.id ℝ (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q) 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: 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))

Tactic:
ext

Goal state after:
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

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

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

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
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case hl
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ((ofQuaternion.comp toQuaternion).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R =
    ((AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R

Tactic:
ext

Goal state after:
case hl
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (((ofQuaternion.comp toQuaternion).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R) 1 =
    (((AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R) 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case hr
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ((ofQuaternion.comp toQuaternion).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R =
    ((AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R

Tactic:
ext

Goal state after:
case hr
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (((ofQuaternion.comp toQuaternion).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R) 1 =
    (((AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R) 1
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ 1 + (algebraMap S R) (fM vM) = 1 + (ibc.toDual fM) (ε vM)

Tactic:
add_right_inj,

Goal state after:
case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ (algebraMap S R) (fM vM) = (ibc.toDual fM) (ε vM)
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
⊢ ((curry
          (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)) ∘ₗ
            ↑(TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm ∘ₗ
              LinearMap.lTensor (⨁ (i : ι), 𝒜 i)
                  (↑(TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i)) ∘ₗ
                    LinearMap.rTensor (⨁ (i : ι), ℬ i) ↑(gradedComm R ℬ 𝒜) ∘ₗ
                      ↑(TensorProduct.assoc R (DirectSum ι ℬ) (DirectSum ι 𝒜) (DirectSum ι ℬ)).symm) ∘ₗ
                ↑(TensorProduct.assoc R (DirectSum ι 𝒜) (DirectSum ι ℬ) (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ))))
        (a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁))
      ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] b₂) =
    (-1) ^ (j₁ * i₂) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)

Tactic:
dsimp only [curry_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_tmul,
    map_tmul, LinearMap.id_coe, id_eq, assoc_symm_tmul, LinearMap.rTensor_tmul,
    LinearMap.lTensor_tmul]

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 ℬ
j₁ i₂ : ι
a₁ : ⨁ (i : ι), 𝒜 i
b₁ : ℬ j₁
a₂ : 𝒜 i₂
b₂ : ⨁ (i : ι), ℬ i
⊢ (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))
            ((gradedComm R ℬ 𝒜) ((lof R ι ℬ j₁) b₁ ⊗ₜ[R] (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] b₂))) =
    (-1) ^ (j₁ * i₂) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * 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
⊢ (gradedMul R 𝒜 ℬ).flip ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) =
    DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r

Tactic:
ext

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✝
⊢ ((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✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case inv_mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ (ι Q).range

Tactic:
simp_rw [← invOf_units x, inv_inv, ← ha, invOf_ι_mul_ι_mul_ι, LinearMap.mem_range_self]

Goal state after:
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 𝒜 ℬ)
        ((TensorProduct.congr ↑(decomposeAlgEquiv 𝒜) ↑(decomposeAlgEquiv ℬ)).symm
          (((decompose 𝒜) a₁ * (DirectSum.of (fun x ↦ ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R]
            ((DirectSum.of (fun x ↦ ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂))) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))

Tactic:
rw [congr_symm_tmul]

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 𝒜 ℬ)
        ((↑(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₂))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul.e_a.e_a.mem
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
i₂' : { n // ↑n = i₂ }
m₂' : CliffordAlgebra Q₂
hm₂ : m₂' ∈ (ι Q₂).range ^ ↑i₂'
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) m₂' = (-1) ^ i₂ • ((map f₂) m₂' * (ι Qₙ) (f₁ v₁))

Tactic:
| mem i₂' m₂' hm₂ =>

Goal state after:
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 ℤˣ)
⊢ ∀ (m : R) (x : B), 1 ᵍ⊗ₜ[R] (m • x) = (RingHom.id R) m • 1 ᵍ⊗ₜ[R] x

Tactic:
by simp [tmul, TensorProduct.tmul_smul]

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ (ofProd Q₁ Q₂).comp (toProd Q₁ Q₂) = AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)

Tactic:
ext

Goal state after:
case ha
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
x✝ : M₁
⊢ ((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
            (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
        ι Q₁)
      x✝ =
    (((AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)).comp
            (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
        ι Q₁)
      x✝

case hb
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
x✝ : M₂
⊢ ((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
            (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
        ι Q₂)
      x✝ =
    (((AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)).comp
            (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
        ι Q₂)
      x✝
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
fg : { fg // ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), fg.1 ↑a * fg.2 ↑b = (-1) ^ (j * i) • (fg.2 ↑b * fg.1 ↑a) }
⊢ (fun F ↦ ⟨(F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)), ⋯⟩) ((fun fg ↦ lift 𝒜 ℬ (↑fg).1 (↑fg).2 ⋯) fg) = fg

Tactic:
ext

Goal state after:
case fst
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
fg : { fg // ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), fg.1 ↑a * fg.2 ↑b = (-1) ^ (j * i) • (fg.2 ↑b * fg.1 ↑a) }
x✝ : A
⊢ (↑((fun F ↦ ⟨(F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)), ⋯⟩) ((fun fg ↦ lift 𝒜 ℬ (↑fg).1 (↑fg).2 ⋯) fg))).1
      x✝ =
    (↑fg).1 x✝

case snd
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
fg : { fg // ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), fg.1 ↑a * fg.2 ↑b = (-1) ^ (j * i) • (fg.2 ↑b * fg.1 ↑a) }
x✝ : B
⊢ (↑((fun F ↦ ⟨(F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)), ⋯⟩) ((fun fg ↦ lift 𝒜 ℬ (↑fg).1 (↑fg).2 ⋯) fg))).2
      x✝ =
    (↑fg).2 x✝
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
⊢ ((fun fg ↦ lift 𝒜 ℬ (↑fg).1 (↑fg).2 ⋯)
        ((fun F ↦ ⟨(F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)), ⋯⟩) F)).toLinearMap =
    F.toLinearMap

Tactic:
ext

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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
x✝¹ : A
x✝ : B
⊢ ((AlgebraTensorModule.curry
          (((fun fg ↦ lift 𝒜 ℬ (↑fg).1 (↑fg).2 ⋯)
                ((fun F ↦ ⟨(F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)), ⋯⟩) F)).toLinearMap ∘ₗ
            ↑(of R 𝒜 ℬ)))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry (F.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ))) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ofDirectSum.comp toDirectSum = AlgHom.id R (TensorAlgebra R M)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ((ofDirectSum.comp toDirectSum).toLinearMap ∘ₗ ι R) x✝ = ((AlgHom.id R (TensorAlgebra R M)).toLinearMap ∘ₗ ι R) x✝
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ toDirectSum.comp ofDirectSum = AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝¹ : ℕ
x✝ : Fin i✝¹ → M
i✝ : ℕ
⊢ ((((toDirectSum.comp ofDirectSum).toLinearMap ∘ₗ DirectSum.lof R ℕ (fun i ↦ ⨂[R]^i M) i✝¹).compMultilinearMap
          (PiTensorProduct.tprod R))
        x✝)
      i✝ =
    ((((AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)).toLinearMap ∘ₗ DirectSum.lof R ℕ (fun i ↦ ⨂[R]^i M) i✝¹).compMultilinearMap
          (PiTensorProduct.tprod R))
        x✝)
      i✝
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: case homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑(Submodule.span R (Set.range ⇑(ιMulti R i✝))) ⊆ ↑(Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd))

Tactic:
refine Submodule.span_mono fun _ hx ↦ ?_

Goal state after:
case homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
x✝ : ExteriorAlgebra R M
hx : x✝ ∈ Set.range ⇑(ιMulti R i✝)
⊢ x✝ ∈ Set.range fun x ↦ (ιMulti R x.fst) x.snd
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
⊢ ⇑b' ∘ v' = fun i ↦ ⇑(algebraMap K L) ∘ v i

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
x✝¹ : ι
x✝ : ι'
⊢ (⇑b' ∘ v') x✝¹ x✝ = (⇑(algebraMap K L) ∘ v x✝¹) x✝