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
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
hfv : f v = 0
⊢ e ∈ transvections K V

Tactic:
by

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 : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x = ((RingHom.id R) c • foldr' Q (contractLeftAux Q d) ⋯ 0) x

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ (contractLeft d) ((ι Q) a * b) = d a • b - (ι Q) a * (contractLeft d) b

Tactic:
by

Goal state after:
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
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
this : e w - w ∈ ker f
⊢ f v = 0

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ (contractRight (b * (ι Q) a)) d = d a • b - (contractRight b) d * (ι Q) a

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
r : R
b : CliffordAlgebra Q
⊢ (contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r * b) =
    (algebraMap R (CliffordAlgebra Q)) r * (contractLeft d) b

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
a : CliffordAlgebra Q
r : R
⊢ (contractLeft d) (a * (algebraMap R (CliffordAlgebra Q)) r) =
    (contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
r : R
b : CliffordAlgebra Q
⊢ (contractRight ((algebraMap R (CliffordAlgebra Q)) r * b)) d =
    (algebraMap R (CliffordAlgebra Q)) r * (contractRight b) d

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
a : CliffordAlgebra Q
r : R
⊢ (contractRight (a * (algebraMap R (CliffordAlgebra Q)) r)) d =
    (contractRight a) d * (algebraMap R (CliffordAlgebra Q)) r

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ ((contractLeftAux Q d) x) (1, 0) = (algebraMap R (CliffordAlgebra Q)) (d x)

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ (contractLeft d) ((ι Q) x) = (algebraMap R (CliffordAlgebra Q)) (d x)

Tactic:
by

Goal state after:
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
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
⊢ e ∈ transvections K V ↔ e ∈ dilatransvections K V ∧ e.fixedReduce = 1

Tactic:
by

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

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 : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ (contractRight ((ι Q) x)) d = (algebraMap R (CliffordAlgebra Q)) (d x)

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
r : R
⊢ (contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r) = 0

Tactic:
by

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
W : Type u_6
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
⊢ ibc.endHom (LinearMap.transvection f v) = LinearMap.transvection (ibc.toDual f) (ε v)

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
r : R
⊢ (contractRight ((algebraMap R (CliffordAlgebra Q)) r)) d = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
V : Type u_4
A : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : Dual R V
v : V
h : f v = 0
hA : ((Dual.baseChange A) f) (1 ⊗ₜ[R] v) = 0
⊢ LinearEquiv.baseChange R A V V (transvection h) = transvection hA

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
⊢ (contractLeft d) 1 = 0

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
⊢ (contractRight 1) d = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
V : Type u_4
A : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : CommRing A
inst✝ : Algebra R A
e : V ≃ₗ[R] V
he : e ∈ dilatransvections R V
⊢ LinearEquiv.baseChange R A V V e ∈ dilatransvections A (A ⊗[R] V)

Tactic:
by

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

Goal state before:
pp: 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 ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.transvection i j 1
⊢ ((toMatrix b b) (transvection f v)).det = 1 + f v

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : CliffordAlgebra 0
⊢ x * y = y * x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : CliffordAlgebra 0
⊢ reverse x = x

Tactic:
by

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

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

Goal state after:
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, ⋯⟩) = AlgHom.id R (CliffordAlgebra 0)

Tactic:
by

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

Goal state before:
pp: r : ℝ
⊢ (LinearMap.toSpanSingleton ℝ ℂ Complex.I) r * (LinearMap.toSpanSingleton ℝ ℂ Complex.I) r = (algebraMap ℝ ℂ) (Q r)

Tactic:
by

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

Goal state before:
pp: c : CliffordAlgebra Q
⊢ toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))

Tactic:
by

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

Goal state before:
pp: c : CliffordAlgebra Q
this✝ : toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))
this : toComplex.comp involute = (↑Complex.conjAe).comp toComplex
⊢ toComplex (involute c) = (starRingEnd ℂ) (toComplex c)

Tactic:
by

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

Goal state before:
pp: c : CliffordAlgebra Q
⊢ toComplex (involute c) = (starRingEnd ℂ) (toComplex c)

Tactic:
by

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

Goal state before:
pp: ⊢ (ι Q) 1 * (ι Q) 1 = -1

Tactic:
by

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

Goal state before:
pp: ⊢ ↑⟨(ι Q) 1, ofComplex._proof_1⟩ * ↑⟨(ι Q) 1, ofComplex._proof_1⟩ = -1

Tactic:
by

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

Goal state before:
pp: ⊢ toComplex.comp ofComplex = AlgHom.id ℝ ℂ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : CliffordAlgebra Q
⊢ CliffordAlgebraComplex.equiv (x * y) = CliffordAlgebraComplex.equiv (y * x)

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (contractLeft d) ((contractLeft d) x) = 0

Tactic:
by

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 : QuadraticForm R M
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (contractRight ((contractRight x) d)) d = 0

Tactic:
by

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

Goal state before:
pp: x : CliffordAlgebra Q
⊢ reverse x = x

Tactic:
by

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

Goal state before:
pp: c : ℂ
⊢ CliffordAlgebraComplex.equiv (ofComplex ((starRingEnd ℂ) c)) = CliffordAlgebraComplex.equiv (involute (ofComplex c))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ι (Q c₁ c₂)) (1, 0) * (ι (Q c₁ c₂)) (1, 0) = c₁ • 1 + 0 • (ι (Q c₁ c₂)) (1, 0)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ι (Q c₁ c₂)) (0, 1) * (ι (Q c₁ c₂)) (0, 1) = c₂ • 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ι (Q c₁ c₂)) (0, 1) * (ι (Q c₁ c₂)) (1, 0) = 0 • (ι (Q c₁ c₂)) (0, 1) - (ι (Q c₁ c₂)) (1, 0) * (ι (Q c₁ c₂)) (0, 1)

Tactic:
by

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

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

Tactic:
by

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

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

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (Q c₁ c₂)
⊢ toQuaternion (star c) = star (toQuaternion c)

Tactic:
by

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 : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ (contractLeft d) ((contractLeft d') x) = -(contractLeft d') ((contractLeft d) x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ofQuaternion.comp toQuaternion = AlgHom.id R (CliffordAlgebra (Q c₁ c₂))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ toQuaternion.comp ofQuaternion = AlgHom.id R ℍ[R,c₁,c₂]

Tactic:
by

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

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r₁ r₂ : R
⊢ (ι 0) r₁ * (ι 0) r₂ = 0

Tactic:
by

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

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

Tactic:
by

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 : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ (contractRight ((contractRight x) d)) d' = -(contractRight ((contractRight x) d')) d

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
⊢ CliffordAlgebraDualNumber.equiv ((ι 0) r) = r • ε

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ CliffordAlgebraDualNumber.equiv.symm ε = (ι 0) 1

Tactic:
by

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 : QuadraticForm R M
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ ((changeFormAux Q B) v) (((changeFormAux Q B) v) x) = (Q v - (B v) v) • x

Tactic:
by

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
m : M
x : CliffordAlgebra Q'
⊢ (Q' m - (B m) m) • x = Q m • x

Tactic:
by

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 : QuadraticForm R M
inst✝ : Invertible 2
⊢ (QuadraticMap.associated (-Q)).toQuadraticMap = 0 - Q

Tactic:
by

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' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
⊢ (changeForm h) 1 = 1

Tactic:
by

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' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
⊢ (ι Q') m = ((changeFormAux Q' B) m) 1

Tactic:
by

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

Goal state before:
pp: 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
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this✝ : Fintype ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
⊢ ((toMatrix b b) (transvection f v)).det = 1 + f v

Tactic:
by

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' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q
⊢ ((foldr Q (changeFormAux Q' B) ⋯) (((foldr Q (changeFormAux Q' B) ⋯) 1) x)) ((ι Q) m) =
    (ι Q') m * (changeForm h) x - (contractLeft (B m)) ((changeForm h) x)

Tactic:
by

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' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m₁ m₂ : M
⊢ (changeForm h) ((ι Q) m₁ * (ι Q) m₂) = (ι Q') m₁ * (ι Q') m₂ - (algebraMap R (CliffordAlgebra Q')) ((B m₁) m₂)

Tactic:
by

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
r : R
⊢ (ι (Q' Q)) (m, r) = (v Q) m + r • e0 Q

Tactic:
by

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
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) ((Q' Q) (0, 1)) = -1

Tactic:
by

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
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) ((Q' Q) ((LinearMap.inl R M R) m)) =
    (algebraMap R (CliffordAlgebra (Q' Q))) (Q m)

Tactic:
by

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
⊢ -(e0 Q * (v Q) m) = (v Q) m * e0 Q

Tactic:
by

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

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 : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) (x✝² + x✝¹) * (CliffordAlgebra.ι Q) x✝, ⋯⟩ =
    ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝, ⋯⟩ +
      ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
by

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
⊢ -((v Q) m * e0 Q) = e0 Q * (v Q) m

Tactic:
by

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

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 : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) (x✝² • x✝¹) * (CliffordAlgebra.ι Q) x✝, ⋯⟩ =
    x✝² • ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
by

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
⊢ e0 Q * (v Q) m * e0 Q = (v Q) m

Tactic:
by

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

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 : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) (x✝¹ + x✝), ⋯⟩ =
    ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝¹, ⋯⟩ +
      ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
by

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

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 : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) (x✝² • x✝), ⋯⟩ =
    x✝² • ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
by

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

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 : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
m₁ m₂ m₃ : M
⊢ (CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * ((CliffordAlgebra.ι Q) m₂ * (CliffordAlgebra.ι Q) m₃) =
    (CliffordAlgebra.ι Q) m₁ * ((CliffordAlgebra.ι Q) m₂ * (CliffordAlgebra.ι Q) m₂ * (CliffordAlgebra.ι Q) m₃)

Tactic:
by

Goal state after: