mathlib-initiative/mathlib-tactics huggingface dataset:
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 : IsUnit (1 + f v)
x : V
⊢ (LinearMap.transvection f (-h.unit⁻¹ • v)) ((LinearMap.transvection f v) x) = x

Tactic:
nth_rewrite 3 [← one_smul R v]

Goal state after:
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 : IsUnit (1 + f v)
x : V
⊢ (LinearMap.transvection f (-h.unit⁻¹ • v)) ((LinearMap.transvection f (1 • v)) x) = x
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 = ⊥
⊢ finrank K V = 1 + finrank K ↥(ker f)

Tactic:
← f.finrank_ker_add_one_of_ne_zero,

Goal state after:
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 = ⊥
⊢ finrank K ↥(ker f) + 1 = 1 + finrank K ↥(ker f)

case hf
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 = ⊥
⊢ f ≠ 0
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
v : M
x fx : CliffordAlgebra Q
⊢ d v • ((ι Q) v * x) - ((ι Q) v * d v • x - (ι Q) v * ((ι Q) v * fx)) = Q v • fx

Tactic:
← mul_assoc,

Goal state after:
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
v : M
x fx : CliffordAlgebra Q
⊢ d v • ((ι Q) v * x) - ((ι Q) v * d v • x - (ι Q) v * (ι Q) v * fx) = Q v • fx
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) (x✝ + y✝) =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) (x✝ + y✝) + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) (x✝ + y✝)

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) (x✝ + y✝) + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) (x✝ + y✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) (x✝ + y✝) + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) (x✝ + y✝)

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ +
      (foldr' Q (contractLeftAux Q d₂) ⋯ 0) (x✝ + y✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ +
      (foldr' Q (contractLeftAux Q d₂) ⋯ 0) (x✝ + y✝)

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ +
      ((foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
hy : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) (x✝ + y✝) = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) (x✝ + y✝)

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
hy : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ =
    c • (foldr' Q (contractLeftAux Q d) ⋯ 0) (x✝ + y✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
hy : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ =
    c • (foldr' Q (contractLeftAux Q d) ⋯ 0) (x✝ + y✝)

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
hy : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ =
    c • ((foldr' Q (contractLeftAux Q d) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝)
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
-- Porting note: Lean cannot figure out anymore the third argument
  refine (foldr'_algebraMap _ _ ?_ _ _).trans <| smul_zero _
  exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

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

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d) x✝) = 0
hy : (contractLeft d) ((contractLeft d) y✝) = 0
⊢ (contractLeft d) ((contractLeft d) (x✝ + y✝)) = 0

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d) x✝) = 0
hy : (contractLeft d) ((contractLeft d) y✝) = 0
⊢ (contractLeft d) ((contractLeft d) x✝ + (contractLeft d) y✝) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d) x✝) = 0
hy : (contractLeft d) ((contractLeft d) y✝) = 0
⊢ (contractLeft d) ((contractLeft d) x✝ + (contractLeft d) y✝) = 0

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d) x✝) = 0
hy : (contractLeft d) ((contractLeft d) y✝) = 0
⊢ (contractLeft d) ((contractLeft d) x✝) + (contractLeft d) ((contractLeft d) y✝) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case mul
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 * (x₁ * x₂)

Tactic:
← mul_assoc,

Goal state after:
case mul
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 * (x₁ * x₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ (contractLeft d) ((contractLeft d') (x✝ + y✝)) = -(contractLeft d') ((contractLeft d) (x✝ + y✝))

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ (contractLeft d) ((contractLeft d') x✝ + (contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) (x✝ + y✝))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ (contractLeft d) ((contractLeft d') x✝ + (contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) (x✝ + y✝))

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ (contractLeft d) ((contractLeft d') x✝) + (contractLeft d) ((contractLeft d') y✝) =
    -(contractLeft d') ((contractLeft d) (x✝ + y✝))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ (contractLeft d) ((contractLeft d') x✝) + (contractLeft d) ((contractLeft d') y✝) =
    -(contractLeft d') ((contractLeft d) (x✝ + y✝))

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ (contractLeft d) ((contractLeft d') x✝) + (contractLeft d) ((contractLeft d') y✝) =
    -(contractLeft d') ((contractLeft d) x✝ + (contractLeft d) y✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ (contractLeft d) ((contractLeft d') x✝) + (contractLeft d) ((contractLeft d') y✝) =
    -(contractLeft d') ((contractLeft d) x✝ + (contractLeft d) y✝)

Tactic:
map_add,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ (contractLeft d) ((contractLeft d') x✝) + (contractLeft d) ((contractLeft d') y✝) =
    -((contractLeft d') ((contractLeft d) x✝) + (contractLeft d') ((contractLeft d) y✝))
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
⊢ (ι Q) v * ((ι Q) v * x) - (ι Q) v * (contractLeft (B v)) x -
      (contractLeft (B v)) ((ι Q) v * x - (contractLeft (B v)) x) =
    (Q v - (B v) v) • x

Tactic:
← mul_assoc,

Goal state after:
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
⊢ (ι Q) v * (ι Q) v * x - (ι Q) v * (contractLeft (B v)) x -
      (contractLeft (B v)) ((ι Q) v * x - (contractLeft (B v)) x) =
    (Q v - (B v) v) • x
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (changeForm h) ((contractLeft d) (x✝ + y✝)) = (contractLeft d) ((changeForm h) (x✝ + y✝))

Tactic:
map_add,

Goal state after:
case add
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
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (changeForm h) ((contractLeft d) x✝ + (contractLeft d) y✝) = (contractLeft d) ((changeForm h) (x✝ + y✝))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (changeForm h) ((contractLeft d) x✝ + (contractLeft d) y✝) = (contractLeft d) ((changeForm h) (x✝ + y✝))

Tactic:
map_add,

Goal state after:
case add
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
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (changeForm h) ((contractLeft d) x✝) + (changeForm h) ((contractLeft d) y✝) =
    (contractLeft d) ((changeForm h) (x✝ + y✝))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (changeForm h) ((contractLeft d) x✝) + (changeForm h) ((contractLeft d) y✝) =
    (contractLeft d) ((changeForm h) (x✝ + y✝))

Tactic:
map_add,

Goal state after:
case add
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
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (changeForm h) ((contractLeft d) x✝) + (changeForm h) ((contractLeft d) y✝) =
    (contractLeft d) ((changeForm h) x✝ + (changeForm h) y✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
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
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (changeForm h) ((contractLeft d) x✝) + (changeForm h) ((contractLeft d) y✝) =
    (contractLeft d) ((changeForm h) x✝ + (changeForm h) y✝)

Tactic:
map_add,

Goal state after:
case add
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
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (changeForm h) ((contractLeft d) x✝) + (changeForm h) ((contractLeft d) y✝) =
    (contractLeft d) ((changeForm h) x✝) + (contractLeft d) ((changeForm h) y✝)
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
f : EvenHom Q A
m₁ m₂ : M
a : A × ↥(S f)
m₃ : M
⊢ (f.bilin m₃) (m₁ + m₂) * a.1 = (f.bilin m₃) m₁ * a.1 + (f.bilin m₃) m₂ * a.1

Tactic:
map_add,

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 : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m₁ m₂ : M
a : A × ↥(S f)
m₃ : M
⊢ ((f.bilin m₃) m₁ + (f.bilin m₃) m₂) * a.1 = (f.bilin m₃) m₁ * a.1 + (f.bilin m₃) m₂ * a.1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case snd.refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
b : A
m₃ : M
⊢ (f.bilin m₁) m * ((f.bilin m) m₃ * b) = Q m • (f.bilin m₁) m₃ * b

Tactic:
← mul_assoc,

Goal state after:
case snd.refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
b : A
m₃ : M
⊢ (f.bilin m₁) m * (f.bilin m) m₃ * b = Q m • (f.bilin m₁) m₃ * b
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm ⋯) x✝ = x✝
hy : (changeForm ⋯) y✝ = y✝
⊢ (changeForm ⋯) (x✝ + y✝) = x✝ + y✝

Tactic:
map_add,

Goal state after:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm ⋯) x✝ = x✝
hy : (changeForm ⋯) y✝ = y✝
⊢ (changeForm ⋯) x✝ + (changeForm ⋯) y✝ = x✝ + y✝