mathlib-initiative/mathlib-tactics huggingface dataset:
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' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm h') ((changeForm h) (x✝ + y✝)) = (changeForm ⋯) (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' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm h') ((changeForm h) x✝ + (changeForm h) y✝) = (changeForm ⋯) (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' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm h') ((changeForm h) x✝ + (changeForm h) y✝) = (changeForm ⋯) (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' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm h') ((changeForm h) x✝) + (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) (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' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm h') ((changeForm h) x✝) + (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) (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' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm h') ((changeForm h) x✝) + (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) x✝ + (changeForm ⋯) y✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case mk.add
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
x✝ val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx : (((foldr Q (fFold f) ⋯) (((foldr Q (fFold f) ⋯) (1, 0)) val✝)) x).1 = (aux f) ⟨x, hx⟩ * (aux f) ⟨val✝, property✝⟩
ihy : (((foldr Q (fFold f) ⋯) (((foldr Q (fFold f) ⋯) (1, 0)) val✝)) y).1 = (aux f) ⟨y, hy⟩ * (aux f) ⟨val✝, property✝⟩
⊢ (((foldr Q (fFold f) ⋯) (((foldr Q (fFold f) ⋯) (1, 0)) val✝)) (x + y)).1 =
    (aux f) ⟨x + y, ⋯⟩ * (aux f) ⟨val✝, property✝⟩

Tactic:
map_add,

Goal state after:
case mk.add
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
x✝ val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx : (((foldr Q (fFold f) ⋯) (((foldr Q (fFold f) ⋯) (1, 0)) val✝)) x).1 = (aux f) ⟨x, hx⟩ * (aux f) ⟨val✝, property✝⟩
ihy : (((foldr Q (fFold f) ⋯) (((foldr Q (fFold f) ⋯) (1, 0)) val✝)) y).1 = (aux f) ⟨y, hy⟩ * (aux f) ⟨val✝, property✝⟩
⊢ (((foldr Q (fFold f) ⋯) (((foldr Q (fFold f) ⋯) (1, 0)) val✝)) x +
        ((foldr Q (fFold f) ⋯) (((foldr Q (fFold f) ⋯) (1, 0)) val✝)) y).1 =
    (aux f) ⟨x + y, ⋯⟩ * (aux f) ⟨val✝, property✝⟩
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B' m✝)) ((changeForm ⋯) x✝) + (changeForm h') ((contractLeft (B m✝)) ((changeForm h) x✝))) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ - (contractLeft (B m✝ + B' m✝)) ((changeForm ⋯) x✝)

Tactic:
map_add,

Goal state after:
case ι_mul
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
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B' m✝)) ((changeForm ⋯) x✝) + (changeForm h') ((contractLeft (B m✝)) ((changeForm h) x✝))) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ - (contractLeft (B m✝) + contractLeft (B' m✝)) ((changeForm ⋯) x✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) * ((ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2) *
      (((ι Q) m₂.1 + (algebraMap R (CliffordAlgebra Q)) m₂.2) *
        ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)) =
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
      (Q' Q) m₂ • ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)

Tactic:
← mul_assoc,

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) * ((ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2) *
        ((ι Q) m₂.1 + (algebraMap R (CliffordAlgebra Q)) m₂.2) *
      ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2) =
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
      (Q' Q) m₂ • ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)
Module: Mathlib.LinearAlgebra.Transvection.Basic

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

Tactic:
map_add,

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
        ((ι Q) m₂.1 * (ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2 * (algebraMap R (CliffordAlgebra Q)) m₂.2) *
      ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2) =
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
      ((algebraMap R (CliffordAlgebra Q)) ((Q' Q) m₂) * ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2))

Tactic:
← mul_assoc,

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
        ((ι Q) m₂.1 * (ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2 * (algebraMap R (CliffordAlgebra Q)) m₂.2) *
      ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2) =
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) * (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m₂) *
      ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)
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
⊢ ↑((toEven Q) ((ι Q) (m₁, r₁).1 + (algebraMap R (CliffordAlgebra Q)) (m₁, r₁).2) *
        (toEven Q) ((ι Q) (m₂, r₂).1 - (algebraMap R (CliffordAlgebra Q)) (m₂, r₂).2)) =
    (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂)

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
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ ↑(((toEven Q) ((ι Q) (m₁, r₁).1) + (toEven Q) ((algebraMap R (CliffordAlgebra Q)) (m₁, r₁).2)) *
        (toEven Q) ((ι Q) (m₂, r₂).1 - (algebraMap R (CliffordAlgebra Q)) (m₂, r₂).2)) =
    (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) 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₂) = (v Q) m₁ * (v Q) m₂

Tactic:
← mul_assoc,

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₂ = (v Q) m₁ * (v Q) m₂
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✝ + y✝) * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) (x✝ + y✝))

Tactic:
map_add,

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₁) y✝) * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * ((map f₁) x✝ + (map f₁) y✝))
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✝ + y✝) * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) (x✝ + y✝))

Tactic:
map_add,

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₁) y✝) * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * ((map f₁) x✝ + (map f₁) y✝))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul
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
ih₁ : (map f₁) x₁ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i) • ((map f₂) m₂ * (map f₁) x₁)
v₁ : M₁
⊢ (-1) ^ (i₂ * ↑i) • ((ι Qₙ) (f₁ v₁) * ((map f₂) m₂ * (map f₁) x₁)) =
    (-1) ^ (i₂ * ↑i) • (-1) ^ i₂ • ((map f₂) m₂ * ((ι Qₙ) (f₁ v₁) * (map f₁) x₁))

Tactic:
← mul_assoc,

Goal state after:
case mem.mem_mul
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
ih₁ : (map f₁) x₁ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i) • ((map f₂) m₂ * (map f₁) x₁)
v₁ : M₁
⊢ (-1) ^ (i₂ * ↑i) • ((ι Qₙ) (f₁ v₁) * (map f₂) m₂ * (map f₁) x₁) =
    (-1) ^ (i₂ * ↑i) • (-1) ^ i₂ • ((map f₂) m₂ * ((ι Qₙ) (f₁ v₁) * (map f₁) x₁))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul
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
ih₁ : (map f₁) x₁ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i) • ((map f₂) m₂ * (map f₁) x₁)
v₁ : M₁
⊢ (-1) ^ (i₂ * ↑i) • ((ι Qₙ) (f₁ v₁) * (map f₂) m₂ * (map f₁) x₁) =
    (-1) ^ (i₂ * ↑i) • (-1) ^ i₂ • ((map f₂) m₂ * ((ι Qₙ) (f₁ v₁) * (map f₁) x₁))

Tactic:
← mul_assoc,

Goal state after:
case mem.mem_mul
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
ih₁ : (map f₁) x₁ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i) • ((map f₂) m₂ * (map f₁) x₁)
v₁ : M₁
⊢ (-1) ^ (i₂ * ↑i) • ((ι Qₙ) (f₁ v₁) * (map f₂) m₂ * (map f₁) x₁) =
    (-1) ^ (i₂ * ↑i) • (-1) ^ i₂ • ((map f₂) m₂ * (ι Qₙ) (f₁ v₁) * (map f₁) x₁)
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✝ + y✝) = (-1) ^ i₂ • ((map f₂) (x✝ + y✝) * (ι Qₙ) (f₁ v₁))

Tactic:
map_add,

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✝ + (map f₂) y✝) * (ι Qₙ) (f₁ v₁))