mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case refine_3
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), w j ∈ Set.Icc 0 1

Tactic:
suffices ∀ j, 0 ≤ w j from
      fun j ↦ ⟨this j, hw ▸ Finset.single_le_sum (fun j _ ↦ this j) (mem_univ j)⟩

Goal state after:
case refine_3
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), 0 ≤ w 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
f : Dual R V
v : V
h : f v = 0
x : V
⊢ (LinearMap.transvection f (-v)) ((LinearMap.transvection f v) x) = x

Tactic:
by
    simp [comp_of_left_eq_apply h]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case neg
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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
i j : ι
hij : ¬i = j
⊢ f (b j) = (b.coord i) (f (b i)) • b j

Tactic:
· have := h' i j hij 1
      simp only [mul_one, one_mul] at this
      rw [feq, ← this]

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

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ (x₁ + x₂) * y = y * x₁ + y * x₂

Tactic:
add_mul,

Goal state after:
case add
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ x₁ * y + x₂ * y = y * x₁ + y * x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

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

Tactic:
rw [ι_eq_zero, LinearMap.comp_zero, LinearMap.comp_zero]

Goal state after:
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
⊢ ↑((toEven Q) ((ι Q) m)) = e0 Q * (v Q) m

Tactic:
simp only [toEven, CliffordAlgebra.lift_ι_apply, ← even_toSubmodule]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑((LinearMap.codRestrict (Subalgebra.toSubmodule (even (Q' Q))) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯) m) =
    e0 Q * (v Q) m
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: 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)
i : Fin n
⊢ γ (MvPolynomial.X (Sum.inl i)) = f (b i)

Tactic:
apply MvPolynomial.aeval_X

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

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
inst✝ : Invertible (Q m)
⊢ (algebraMap R (CliffordAlgebra Q)) (⅟(Q m) * Q m) = 1

Tactic:
invOf_mul_self,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
m : M
inst✝ : Invertible (Q m)
⊢ (algebraMap R (CliffordAlgebra Q)) 1 = 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion

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
a b : M
inst✝¹ : Invertible ((ι Q) a)
inst✝ : Invertible (Q a)
⊢ (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - (⅟(Q a) * Q a) • b) =
    (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)

Tactic:
invOf_mul_self,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
a b : M
inst✝¹ : Invertible ((ι Q) a)
inst✝ : Invertible (Q a)
⊢ (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - 1 • b) = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: 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
i : Fin n
⊢ ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v)) (MvPolynomial.X (Sum.inr i)) = b.equivFun v i

Tactic:
apply MvPolynomial.aeval_X

Goal state after:
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₂) -
      (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) * (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:
add_mul,

Goal state after:
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₁ * (e0 Q * (v Q) m₂) + (algebraMap R (CliffordAlgebra (Q' Q))) r₁ * (e0 Q * (v Q) m₂) -
      (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) * (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₂)
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₁ * (e0 Q * (v Q) m₂) + (algebraMap R (CliffordAlgebra (Q' Q))) r₁ * (e0 Q * (v Q) m₂) -
      (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) * (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:
add_mul,

Goal state after:
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₁ * (e0 Q * (v Q) m₂) + (algebraMap R (CliffordAlgebra (Q' Q))) r₁ * (e0 Q * (v Q) m₂) -
      (e0 Q * (v Q) m₁ * (algebraMap R (CliffordAlgebra (Q' Q))) r₂ +
        (algebraMap R (CliffordAlgebra (Q' Q))) r₁ * (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₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case add
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₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
x✝ y✝ : CliffordAlgebra Q₁
hx✝ : x✝ ∈ ⨆ i, (ι Q₁).range ^ ↑i
hy✝ : y✝ ∈ ⨆ i, (ι Q₁).range ^ ↑i
ihx : (map f₁) x✝ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) x✝)
ihy : (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) y✝)
⊢ ((map f₁) x✝ + (map f₁) y✝) * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * ((map f₁) x✝ + (map f₁) y✝))

Tactic:
add_mul,

Goal state after:
case add
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₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
x✝ y✝ : CliffordAlgebra Q₁
hx✝ : x✝ ∈ ⨆ i, (ι Q₁).range ^ ↑i
hy✝ : y✝ ∈ ⨆ i, (ι Q₁).range ^ ↑i
ihx : (map f₁) x✝ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) x✝)
ihy : (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) y✝)
⊢ (map f₁) x✝ * (map f₂) m₂ + (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * ((map f₁) x✝ + (map f₁) y✝))
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
⊢ (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q =
    ((v Q) m₁ + r₁ • e0 Q) * (v Q) m₂ + ((v Q) m₁ + r₁ • e0 Q) * r₂ • e0 Q

Tactic:
add_mul,

Goal state after:
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
⊢ (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q =
    (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + ((v Q) m₁ + r₁ • e0 Q) * r₂ • e0 Q
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
⊢ (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q =
    (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + ((v Q) m₁ + r₁ • e0 Q) * r₂ • e0 Q

Tactic:
add_mul,

Goal state after:
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
⊢ (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q =
    (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + ((v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.add
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 : ℕ
x✝ y✝ : CliffordAlgebra Q₁
i✝ : ℕ
hx✝ : x✝ ∈ (ι Q₁).range ^ i✝
hy✝ : y✝ ∈ (ι Q₁).range ^ i✝
ihx : (map f₁) x✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) x✝)
ihy : (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) y✝)
⊢ ((map f₁) x✝ + (map f₁) y✝) * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * ((map f₁) x✝ + (map f₁) y✝))

Tactic:
add_mul,

Goal state after:
case mem.add
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 : ℕ
x✝ y✝ : CliffordAlgebra Q₁
i✝ : ℕ
hx✝ : x✝ ∈ (ι Q₁).range ^ i✝
hy✝ : y✝ ∈ (ι Q₁).range ^ i✝
ihx : (map f₁) x✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) x✝)
ihy : (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) y✝)
⊢ (map f₁) x✝ * (map f₂) m₂ + (map f₁) y✝ * (map f₂) m₂ =
    (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * ((map f₁) x✝ + (map f₁) y✝))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case 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
⊢ ↑x * (ι Q) m * ↑x⁻¹ ∈ (ι Q).range

Tactic:
let := x.invertible

Goal state after:
case 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
⊢ ↑x * (ι Q) m * ↑x⁻¹ ∈ (ι Q).range
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
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ (ι Q).range

Tactic:
let := x.invertible

Goal state after:
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
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul.e_a.e_a.add
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₁
x✝ y✝ : CliffordAlgebra Q₂
hx✝ : x✝ ∈ ⨆ i, (ι Q₂).range ^ ↑i
hy✝ : y✝ ∈ ⨆ i, (ι Q₂).range ^ ↑i
ihx : (ι Qₙ) (f₁ v₁) * (map f₂) x✝ = (-1) ^ i₂ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁))
ihy : (ι Qₙ) (f₁ v₁) * (map f₂) y✝ = (-1) ^ i₂ • ((map f₂) y✝ * (ι Qₙ) (f₁ v₁))
⊢ (ι Qₙ) (f₁ v₁) * ((map f₂) x✝ + (map f₂) y✝) = (-1) ^ i₂ • (((map f₂) x✝ + (map f₂) y✝) * (ι Qₙ) (f₁ v₁))

Tactic:
add_mul,

Goal state after:
case mem.mem_mul.e_a.e_a.add
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₁
x✝ y✝ : CliffordAlgebra Q₂
hx✝ : x✝ ∈ ⨆ i, (ι Q₂).range ^ ↑i
hy✝ : y✝ ∈ ⨆ i, (ι Q₂).range ^ ↑i
ihx : (ι Qₙ) (f₁ v₁) * (map f₂) x✝ = (-1) ^ i₂ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁))
ihy : (ι Qₙ) (f₁ v₁) * (map f₂) y✝ = (-1) ^ i₂ • ((map f₂) y✝ * (ι Qₙ) (f₁ v₁))
⊢ (ι Qₙ) (f₁ v₁) * ((map f₂) x✝ + (map f₂) y✝) =
    (-1) ^ i₂ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁) + (map f₂) y✝ * (ι Qₙ) (f₁ v₁))
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 + (ixb + iyb) * iza) •
      ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
        ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb)) =
    (-1) ^ (iyb * iza + ixb * (iya + iza)) •
      ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
        ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))

Tactic:
add_mul,

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 + (ixb * iza + iyb * iza)) •
      ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
        ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb)) =
    (-1) ^ (iyb * iza + ixb * (iya + iza)) •
      ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
        ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
⊢ involute ↑x * (ι Q) b * ↑x⁻¹ ∈ (ι Q).range

Tactic:
let := x.invertible

Goal state after:
case mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this : Invertible ↑x := x.invertible
⊢ involute ↑x * (ι Q) b * ↑x⁻¹ ∈ (ι Q).range
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
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ (ι Q).range

Tactic:
let := x.invertible

Goal state after:
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
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this : Invertible ↑x := x.invertible
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

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

Tactic:
add_mul,

Goal state after:
case mem.mem_mul.e_a.e_a.mem.add
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₁ m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n : ℕ
x✝ y✝ : CliffordAlgebra Q₂
i✝ : ℕ
hx✝ : x✝ ∈ (ι Q₂).range ^ i✝
hy✝ : y✝ ∈ (ι Q₂).range ^ i✝
ihx : (ι Qₙ) (f₁ v₁) * (map f₂) x✝ = (-1) ^ ↑i✝ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁))
ihy : (ι Qₙ) (f₁ v₁) * (map f₂) y✝ = (-1) ^ ↑i✝ • ((map f₂) y✝ * (ι Qₙ) (f₁ v₁))
⊢ (ι Qₙ) (f₁ v₁) * ((map f₂) x✝ + (map f₂) y✝) =
    (-1) ^ ↑i✝ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁) + (map f₂) y✝ * (ι Qₙ) (f₁ v₁))
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₂ + ((j₁ + j₂) * i₁ + (j₁ + j₂) * i₂)) •
      ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) =
    (-1) ^ (j₂ * i₂ + (j₁ * i₁ + i₁ * j₂)) •
      ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂)

Tactic:
add_mul,

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₂ + (j₁ * i₁ + j₂ * i₁ + (j₁ * i₂ + j₂ * i₂))) •
      ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) =
    (-1) ^ (j₂ * i₂ + (j₁ * i₁ + i₁ * j₂)) •
      ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂)