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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
h : AffineIndependent k p
i : ι
w : ι → k
hw : ∑ i, w i = 1
c : k
j : ι
hj : j ≠ i
t : Finset ι
w' : ι → k
ht✝ : ↑t ⊆ {i}ᶜ
hw' : ∑ i ∈ t, w' i = 1
hqmem : (affineCombination k t p) w' ∈ affineSpan k (p '' {i}ᶜ)
heq : ∀ i_1 ∈ univ, ((1 - c) • (Pi.single i 1 - Pi.single j 1) + (↑t).indicator w') i_1 = w i_1
ht : (↑t).indicator w' i = 0
⊢ w i = 1 - c

pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
h : AffineIndependent k p
i : ι
w : ι → k
hw : ∑ i, w i = 1
c : k
j : ι
hj : j ≠ i
t : Finset ι
w' : ι → k
ht✝ : ↑t ⊆ {i}ᶜ
hw' : ∑ i ∈ t, w' i = 1
hqmem : (affineCombination k t p) w' ∈ affineSpan k (p '' {i}ᶜ)
heq :
  (affineCombination k univ p) ((1 - c) • (Pi.single i 1 - Pi.single j 1) + (↑t).indicator w') =
    (affineCombination k univ p) w
ht : (↑t).indicator w' i = 0
⊢ ∑ i_1, ((1 - c) • (Pi.single i 1 - Pi.single j 1) + (↑t).indicator w') i_1 = 1

Tactic:
· simpa [hj.symm, ht] using (heq i (mem_univ i)).symm

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
h : AffineIndependent k p
i : ι
w : ι → k
hw : ∑ i, w i = 1
c : k
j : ι
hj : j ≠ i
t : Finset ι
w' : ι → k
ht✝ : ↑t ⊆ {i}ᶜ
hw' : ∑ i ∈ t, w' i = 1
hqmem : (affineCombination k t p) w' ∈ affineSpan k (p '' {i}ᶜ)
heq :
  (affineCombination k univ p) ((1 - c) • (Pi.single i 1 - Pi.single j 1) + (↑t).indicator w') =
    (affineCombination k univ p) w
ht : (↑t).indicator w' i = 0
⊢ ∑ i_1, ((1 - c) • (Pi.single i 1 - Pi.single j 1) + (↑t).indicator w') i_1 = 1
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f g : V →ₗ[R] V
⊢ f.fixedSubmodule ⊓ g.fixedSubmodule ≤ (f ∘ₗ g).fixedSubmodule

Tactic:
by
  intro; simp_all

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
i j : ι
h✝ : ∀ (v : V), ∃ x x_1, ∃ (_ : x • v + x_1 • f v = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
h : s • b i + t • f (b i) = 0
h' : ¬(s = 0 ∧ t = 0)
hj : ¬i = j
⊢ (b.repr (f (b i))) j = 0

Tactic:
have : t = 0 ∨ b.repr (f (b i)) j = 0 := by
        rw [b.ext_elem_iff] at h
        simpa [single_eq_of_ne' hj] using h j

Goal state after:
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
i j : ι
h✝ : ∀ (v : V), ∃ x x_1, ∃ (_ : x • v + x_1 • f v = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
h : s • b i + t • f (b i) = 0
h' : ¬(s = 0 ∧ t = 0)
hj : ¬i = j
this : t = 0 ∨ (b.repr (f (b i))) j = 0
⊢ (b.repr (f (b i))) j = 0
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
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
hfv : f (b i) * (b.repr v) i = 0
this : ∀ (x : V), x = (b.repr x) i • b i
⊢ ((b.repr x) i * f (b i) * (b.repr v) i) • b i = 0

Tactic:
mul_assoc,

Goal state after:
R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
hfv : f (b i) * (b.repr v) i = 0
this : ∀ (x : V), x = (b.repr x) i • b i
⊢ ((b.repr x) i * (f (b i) * (b.repr v) i)) • b i = 0
Module: Mathlib.LinearAlgebra.Center

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

Tactic:
mul_assoc,

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

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

Tactic:
mul_assoc,

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ f x * ↑(-h.unit⁻¹) + (f x * 1 + f x * ↑(-h.unit⁻¹) * f v) = 0

Tactic:
mul_assoc,

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
⊢ f x * ↑(-h.unit⁻¹) + (f x * 1 + f x * (↑(-h.unit⁻¹) * f v)) = 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 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:
| add _ _ hx hy =>

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✝ 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:
| add _ _ hx hy =>

Goal state after:
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₁ * x₂ * y = 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₁ * (x₂ * y) = 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 : 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:
| add _ _ hx hy =>

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:
induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
  | mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
  | add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]

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 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:
| add _ _ hx hy =>

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:
rw [e0, v, LinearMap.comp_apply, LinearMap.inl_apply, ← map_smul, Prod.smul_mk,
    smul_zero, smul_eq_mul, mul_one, ← map_add, Prod.mk_add_mk, zero_add, add_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
⊢ -(v Q) m * e0 Q * e0 Q = (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
⊢ -(v Q) m * (e0 Q * e0 Q) = (v Q) m
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:
| add _ _ hx hy =>

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

Goal state before:
pp: case snd.refine_3
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
⊢ ∀ (x y : M →ₗ[R] A),
    x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)} →
      y ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)} →
        (f.bilin m₁) m * x m = Q m • x m₁ →
          (f.bilin m₁) m * y m = Q m • y m₁ → (f.bilin m₁) m * (x + y) m = Q m • (x + y) m₁

Tactic:
rintro x y _hx _hy ihx ihy

Goal state after:
case snd.refine_3
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
x y : M →ₗ[R] A
_hx : x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
_hy : y ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * x m = Q m • x m₁
ihy : (f.bilin m₁) m * y m = Q m • y m₁
⊢ (f.bilin m₁) m * (x + y) m = Q m • (x + y) m₁
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:
| add _ _ hx hy =>

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 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:
| add _ _ hx hy =>

Goal state after:
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₁
⊢ (map f₁) ((ι Q₁) v₁) * (map f₁) x₁ * (map f₂) m₂ =
    (-1) ^ (i₂ * ↑i.succ) • ((map f₂) m₂ * ((map f₁) ((ι Q₁) 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₁
⊢ (map f₁) ((ι Q₁) v₁) * ((map f₁) x₁ * (map f₂) m₂) =
    (-1) ^ (i₂ * ↑i.succ) • ((map f₂) m₂ * ((map f₁) ((ι Q₁) v₁) * (map f₁) x₁))
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
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a m) • a - m) ∈ (ι Q).range

Tactic:
LinearMap.mem_range_self

Goal state after:
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
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a m) • a - m) ∈ (ι Q).range

Tactic:
LinearMap.mem_range_self

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

Goal state before:
pp: case one
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
m : M
⊢ (ι Q) m ∈ (ι Q).range

Tactic:
LinearMap.mem_range_self

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

Goal state before:
pp: case mul
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
y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (m : M), ↑y * (ι Q) m * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (m : M), ↑z * (ι Q) m * ↑z⁻¹ ∈ (ι Q).range
m z' : M
hz' : (ι Q) z' = ↑z * (ι Q) m * ↑z⁻¹
y' : M
hy' : (ι Q) y' = ↑y * (ι Q) z' * ↑y⁻¹
⊢ (ι Q) y' ∈ (ι Q).range

Tactic:
LinearMap.mem_range_self

Goal state after:
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
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ (ι Q) (-((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)) ∈ (ι Q).range

Tactic:
LinearMap.mem_range_self

Goal state after:
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
this✝³ : Invertible ↑x := x.invertible
this✝² : Invertible ((ι Q) a) := ⋯.mpr this✝³
this✝¹ : Invertible (Q a) := invertibleOfInvertibleι Q a
this✝ : Invertible (-(ι Q) a) := invertibleNeg ((ι Q) a)
this : Invertible (involute ((ι Q) a)) := Invertible.map involute ((ι Q) a)
⊢ (ι Q) (-((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)) ∈ (ι Q).range

Tactic:
LinearMap.mem_range_self

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

Goal state before:
pp: case one
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 : (CliffordAlgebra Q)ˣ
b : M
⊢ (ι Q) b ∈ (ι Q).range

Tactic:
LinearMap.mem_range_self

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

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

Tactic:
mul_assoc,

Goal state after:
case mem.mem_mul.e_a.e_a.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₁ m₁' : CliffordAlgebra Q₁
i₁n i✝ : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i✝
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n i : ℕ
x₂ : CliffordAlgebra Q₂
_hx₂ : x₂ ∈ (ι Q₂).range ^ i
ih₂ : (ι Qₙ) (f₁ v₁) * (map f₂) x₂ = (-1) ^ ↑i • ((map f₂) x₂ * (ι Qₙ) (f₁ v₁))
v₂ : M₂
⊢ -((ι Qₙ) (f₂ v₂) * ((ι Qₙ) (f₁ v₁) * (map f₂) x₂)) = (-1) ^ (↑i + 1) • ((ι Qₙ) (f₂ v₂) * (map f₂) x₂ * (ι Qₙ) (f₁ v₁))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case mul
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 y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ (ι Q).range
b z' : M
hz' : (ι Q) z' = involute ↑z * (ι Q) b * ↑z⁻¹
y' : M
hy' : (ι Q) y' = involute ↑y * (ι Q) z' * ↑y⁻¹
⊢ (ι Q) y' ∈ (ι Q).range

Tactic:
LinearMap.mem_range_self

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
I : Type u_3
inst✝³ : LinearOrder I
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis I R M
s : Finset I
⊢ b.ExteriorAlgebra s = ιMulti_family R s.card (⇑b) (ofCard ⋯)

Tactic:
simp [basis_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case h.inl
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ (A.submatrix f g).det = 0

Tactic:
← det_transpose,

Goal state after:
case h.inl
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ (A.submatrix f g)ᵀ.det = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ (M.submatrix id j₁.succAbove).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det

Tactic:
← det_transpose,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ (M.submatrix id j₁.succAbove)ᵀ.det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det