mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
⊢ ∑ i, (domCoprod.summand a b i) v = 0

Tactic:
exact
        Finset.sum_involution (fun σ _ => Equiv.swap i j • σ)
          (fun σ _ => domCoprod.summand_add_swap_smul_eq_zero a b σ hv hij)
          (fun σ _ => mt <| domCoprod.summand_eq_zero_of_smul_invariant a b σ hv hij)
          (fun σ _ => Finset.mem_univ _) fun σ _ =>
          Equiv.swap_smul_involutive i j σ

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case pos
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : w i = 1 - x
hj : ∀ (j : Fin n), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1
j : Fin n
hji : j = i
⊢ 0 ≤ w j

pp: case neg
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : w i = 1 - x
hj : ∀ (j : Fin n), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1
j : Fin n
hji : ¬j = i
⊢ 0 ≤ w j

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : w i = 1 - x
hj : ∀ (j : Fin n), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1
j : Fin n
hji : j = i
⊢ 0 ≤ w j

case neg
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : w i = 1 - x
hj : ∀ (j : Fin n), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1
j : Fin n
hji : ¬j = i
⊢ 0 ≤ w j
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ ↑(alternatization (a.domCoprod b)) = ↑((alternatization a).domCoprod (alternatization b))

Tactic:
rw [domCoprod_coe, MultilinearMap.alternatization_coe,
    Finset.sum_partition (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)]

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ ∑ xbar ∈ Finset.image (Quotient.mk (QuotientGroup.leftRel (sumCongrHom ιa ιb).range)) Finset.univ,
      ∑ y with ⟦y⟧ = xbar, sign y • domDomCongr y (a.domCoprod b) =
    ∑ σ, domCoprod.summand (alternatization a) (alternatization b) σ
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v x✝ : V
⊢ (transvection 0 v) x✝ = id x✝

Tactic:
simp [transvection]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
x✝ : V
⊢ (transvection f 0) x✝ = id x✝

Tactic:
simp [transvection]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
⊢ ((Finsupp.single i 1).sum fun i a ↦ a • b i) + r • b j = b i + r • b j + (Finsupp.single i 1) j • b j

pp: case hg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
⊢ ∀ (i : ι), 0 • b i = 0

pp: case hgg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
⊢ ∀ (j : ι) (a₁ a₂ : R), (a₁ + a₂) • b j = a₁ • b j + a₂ • b j

Tactic:
<;>

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
⊢ ((Finsupp.single i 1).sum fun i a ↦ a • b i) + r • b j = b i + r • b j + (Finsupp.single i 1) j • b j

case hg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
⊢ ∀ (i : ι), 0 • b i = 0

case hgg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
⊢ ∀ (j : ι) (a₁ a₂ : R), (a₁ + a₂) • b j = a₁ • b j + a₂ • b j
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
v : V
hv : 0 v = 0
x✝ : V
⊢ (transvection hv) x✝ = (refl R V) x✝

Tactic:
simp [transvection]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
hf : f 0 = 0
x✝ : V
⊢ (transvection hf) x✝ = (refl R V) x✝

Tactic:
simp [transvection]

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

Goal state before:
pp: case h
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e✝ e : V ≃ₗ[R] V
f : Dual R V
v : V
he : ↑e = LinearMap.transvection f v
x : V
⊢ x = e x - f x • v

Tactic:
rw [eq_comm, sub_eq_iff_eq_add, ← coe_coe, he, LinearMap.transvection.apply]

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

Goal state before:
pp: case h₀
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
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : ↑(u.rangeRestrict x) = u x
⊢ ∀ (b_1 : Unit), (b.repr (u.rangeRestrict x)) b_1 ≠ 0 → b_1 ≠ default → (b.repr (u.rangeRestrict x)) b_1 • b b_1 = 0

pp: case h₁
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
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : ↑(u.rangeRestrict x) = u x
⊢ (b.repr (u.rangeRestrict x)) default = 0 → 0 • b default = 0

Tactic:
<;>

Goal state after:
case h₀
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
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : ↑(u.rangeRestrict x) = u x
⊢ ∀ (b_1 : Unit), (b.repr (u.rangeRestrict x)) b_1 ≠ 0 → b_1 ≠ default → (b.repr (u.rangeRestrict x)) b_1 • b b_1 = 0

case h₁
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
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : ↑(u.rangeRestrict x) = u x
⊢ (b.repr (u.rangeRestrict x)) default = 0 → 0 • b default = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg.inl
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
h : ¬(i = x ∧ j = y)
h' : ¬i = x
⊢ (Finsupp.single i ((Finsupp.single y 1) j)) x = Matrix.single i j 1 x y

pp: case neg.inr
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
h : ¬(i = x ∧ j = y)
h' : ¬j = y
⊢ (Finsupp.single i ((Finsupp.single y 1) j)) x = Matrix.single i j 1 x y

Tactic:
<;>

Goal state after:
case neg.inl
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
h : ¬(i = x ∧ j = y)
h' : ¬i = x
⊢ (Finsupp.single i ((Finsupp.single y 1) j)) x = Matrix.single i j 1 x y

case neg.inr
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
h : ¬(i = x ∧ j = y)
h' : ¬j = y
⊢ (Finsupp.single i ((Finsupp.single y 1) j)) x = Matrix.single i j 1 x y
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

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:
<;>

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 =
    ((AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R

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

Goal state before:
pp: case hi
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (toQuaternion.comp ofQuaternion) (Basis.self R).i = (AlgHom.id R ℍ[R,c₁,c₂]) (Basis.self R).i

pp: case hj
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (toQuaternion.comp ofQuaternion) (Basis.self R).j = (AlgHom.id R ℍ[R,c₁,c₂]) (Basis.self R).j

Tactic:
<;>

Goal state after:
case hi
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (toQuaternion.comp ofQuaternion) (Basis.self R).i = (AlgHom.id R ℍ[R,c₁,c₂]) (Basis.self R).i

case hj
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (toQuaternion.comp ofQuaternion) (Basis.self R).j = (AlgHom.id R ℍ[R,c₁,c₂]) (Basis.self R).j
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂) =
    e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ -
      (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂)

Tactic:
rw [mul_sub, add_mul, add_mul, ← Algebra.commutes, ← Algebra.smul_def, ← map_mul, ←
                  Algebra.smul_def, sub_add_eq_sub_sub, smul_mul_assoc, smul_mul_assoc]

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 ℬ
x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ↑↑((-1) ^ (ixb * iya)) •
      (-1) ^ ((ixb + iyb) * iza) •
        ((DirectSum.of 𝒜 (ixa + iya)) (GradedMonoid.GMul.mul xa ya) * (DirectSum.of 𝒜 iza) za) ⊗ₜ[R]
          ((DirectSum.of ℬ (ixb + iyb)) (GradedMonoid.GMul.mul xb yb) * (DirectSum.of ℬ izb) zb) =
    ↑↑((-1) ^ (iyb * iza)) •
      (-1) ^ (ixb * (iya + iza)) •
        ((DirectSum.of 𝒜 ixa) xa * (DirectSum.of 𝒜 (iya + iza)) (GradedMonoid.GMul.mul ya za)) ⊗ₜ[R]
          ((DirectSum.of ℬ ixb) xb * (DirectSum.of ℬ (iyb + izb)) (GradedMonoid.GMul.mul yb zb))

Tactic:
← DirectSum.of_mul_of,

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 z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ↑↑((-1) ^ (ixb * iya)) •
      (-1) ^ ((ixb + iyb) * iza) •
        ((DirectSum.of 𝒜 ixa) xa * (DirectSum.of 𝒜 iya) ya * (DirectSum.of 𝒜 iza) za) ⊗ₜ[R]
          ((DirectSum.of ℬ ixb) xb * (DirectSum.of ℬ iyb) yb * (DirectSum.of ℬ izb) zb) =
    ↑↑((-1) ^ (iyb * iza)) •
      (-1) ^ (ixb * (iya + iza)) •
        ((DirectSum.of 𝒜 ixa) xa * ((DirectSum.of 𝒜 iya) ya * (DirectSum.of 𝒜 iza) za)) ⊗ₜ[R]
          ((DirectSum.of ℬ ixb) xb * ((DirectSum.of ℬ iyb) yb * (DirectSum.of ℬ izb) zb))
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₂
⊢ ((-1) ^ (j₁ * i₂) * (-1) ^ ((j₁ + j₂) * (i₁ + i₂))) •
      (DirectSum.of ℬ (j₁ + j₂)) (GradedMonoid.GMul.mul b₁ b₂) ⊗ₜ[R]
        (DirectSum.of 𝒜 (i₁ + i₂)) (GradedMonoid.GMul.mul a₁ a₂) =
    ((-1) ^ (j₂ * i₂) * ((-1) ^ (j₁ * i₁) * (-1) ^ (i₁ * j₂))) •
      ((DirectSum.of ℬ j₁) b₁ * (DirectSum.of ℬ j₂) b₂) ⊗ₜ[R] ((DirectSum.of 𝒜 i₁) a₁ * (DirectSum.of 𝒜 i₂) a₂)

Tactic:
← DirectSum.of_mul_of,

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₂
⊢ ((-1) ^ (j₁ * i₂) * (-1) ^ ((j₁ + j₂) * (i₁ + i₂))) •
      ((DirectSum.of ℬ j₁) b₁ * (DirectSum.of ℬ j₂) b₂) ⊗ₜ[R] ((DirectSum.of 𝒜 i₁) a₁ * (DirectSum.of 𝒜 i₂) a₂) =
    ((-1) ^ (j₂ * i₂) * ((-1) ^ (j₁ * i₁) * (-1) ^ (i₁ * j₂))) •
      ((DirectSum.of ℬ j₁) b₁ * (DirectSum.of ℬ j₂) b₂) ⊗ₜ[R] ((DirectSum.of 𝒜 i₁) a₁ * (DirectSum.of 𝒜 i₂) a₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul.e_a.e_a
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
hm₂ : m₂ ∈ evenOdd Q₂ i₂
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) m₂ = (-1) ^ i₂ • ((map f₂) m₂ * (ι Qₙ) (f₁ v₁))

Tactic:
induction hm₂ using Submodule.iSup_induction' with

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
a✝ : Nontrivial R
x✝ : { s // LinearIndepOn R id s }
s : Set M
hs✝ : LinearIndepOn R id s
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
⊢ ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ x ∈ s_1, M'.mkQ (g x • ↑x) = 0 → ∀ i ∈ s_1, g i = 0

Tactic:
← map_sum,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
a✝ : Nontrivial R
x✝ : { s // LinearIndepOn R id s }
s : Set M
hs✝ : LinearIndepOn R id s
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
⊢ ∀ (s_1 : Finset ↑s) (g : ↑s → R), M'.mkQ (∑ x ∈ s_1, g x • ↑x) = 0 → ∀ i ∈ s_1, g i = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case hl
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₂
m : M₁
⊢ ((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inl R M₁ M₂) m =
    (((AlgHom.id R (CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
        LinearMap.inl R M₁ M₂)
      m

pp: case hr
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₂
m : M₂
⊢ ((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inr R M₁ M₂) m =
    (((AlgHom.id R (CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
        LinearMap.inr R M₁ M₂)
      m

Tactic:
<;>

Goal state after:
case hl
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₂
m : M₁
⊢ ((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inl R M₁ M₂) m =
    (((AlgHom.id R (CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
        LinearMap.inl R M₁ M₂)
      m

case hr
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₂
m : M₂
⊢ ((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inr R M₁ M₂) m =
    (((AlgHom.id R (CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
        LinearMap.inr R M₁ M₂)
      m
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

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

pp: 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✝

Tactic:
<;>

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✝