mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hφ_cont : UpperSemicontinuous φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
a : α
⊢ ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a → μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a → μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a

Tactic:
h

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hφ_cont : UpperSemicontinuous φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
a : α
h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a
⊢ μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a → μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
inst✝¹ : FiniteDimensional ℝ E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
a : α
⊢ ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a → μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a → μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a

Tactic:
h

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
inst✝¹ : FiniteDimensional ℝ E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
a : α
h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a
⊢ μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a → μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: case h₀
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i i' : ι
a✝ : (b.repr v) i' ≠ 0
⊢ i' ≠ i → ((basis b ibc).repr ((b.repr v) i' • ε (b i'))) i = 0

Tactic:
h

Goal state after:
case h₀
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i i' : ι
a✝ : (b.repr v) i' ≠ 0
h : i' ≠ i
⊢ ((basis b ibc).repr ((b.repr v) i' • ε (b i'))) i = 0
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : ιa ⊕ ιb → Mᵢ
h : σ₂ = σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)
⊢ (Perm.sign σ₁ • (a fun i₁ ↦ v (σ₁ (Sum.inl i₁))) ⊗ₜ[R'] b fun i₂ ↦ v (σ₁ (Sum.inr i₂))) =
    Perm.sign σ₂ • (a fun i₁ ↦ v (σ₂ (Sum.inl i₁))) ⊗ₜ[R'] b fun i₂ ↦ v (σ₂ (Sum.inr i₂))

Tactic:
have : Equiv.Perm.sign (σ₁ * Perm.sumCongrHom _ _ (sl, sr))
      = Equiv.Perm.sign σ₁ * (Equiv.Perm.sign sl * Equiv.Perm.sign sr) := by simp

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : ιa ⊕ ιb → Mᵢ
h : σ₂ = σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)
this : Perm.sign (σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) = Perm.sign σ₁ * (Perm.sign sl * Perm.sign sr)
⊢ (Perm.sign σ₁ • (a fun i₁ ↦ v (σ₁ (Sum.inl i₁))) ⊗ₜ[R'] b fun i₂ ↦ v (σ₁ (Sum.inr i₂))) =
    Perm.sign σ₂ • (a fun i₁ ↦ v (σ₂ (Sum.inl i₁))) ⊗ₜ[R'] b fun i₂ ↦ v (σ₂ (Sum.inr i₂))
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
q : P
hqmem : q ∈ affineSpan k (p '' {i}ᶜ)
⊢ (1 - c) • (p i -ᵥ p j) +ᵥ q = (affineCombination k univ p) w → w i = 1 - c

Tactic:
heq

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
q : P
hqmem : q ∈ affineSpan k (p '' {i}ᶜ)
heq : (1 - c) • (p i -ᵥ p j) +ᵥ q = (affineCombination k univ p) w
⊢ w i = 1 - c
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
σ : Perm (ιa ⊕ ιb)
hσ✝ : swap i j • Quotient.mk'' σ = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ : (Perm.sumCongrHom ιa ιb) (sl, sr) = ((fun x ↦ swap i j • x) σ)⁻¹ * σ
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0

Tactic:
rcases hi : σ⁻¹ i with i' | i'

Goal state after:
case h.inl
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
σ : Perm (ιa ⊕ ιb)
hσ✝ : swap i j • Quotient.mk'' σ = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ : (Perm.sumCongrHom ιa ιb) (sl, sr) = ((fun x ↦ swap i j • x) σ)⁻¹ * σ
i' : ιa
hi : σ⁻¹ i = Sum.inl i'
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0

case h.inr
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
σ : Perm (ιa ⊕ ιb)
hσ✝ : swap i j • Quotient.mk'' σ = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ : (Perm.sumCongrHom ιa ιb) (sl, sr) = ((fun x ↦ swap i j • x) σ)⁻¹ * σ
i' : ιb
hi : σ⁻¹ i = Sum.inr i'
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 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
this : s + t * (b.repr (f (b i))) i = -(t * r * (b.repr (f (b j))) i)
⊢ -(t * r * (b.repr (f (b j))) i) = 0

Tactic:
feq

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
this : s + t * (b.repr (f (b i))) i = -(t * r * (b.repr (f (b j))) i)
⊢ -(t * r * (b.repr ((b.coord j) (f (b j)) • b j)) 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)) = 0
this : s * r + t * r * (b.repr (f (b j))) j = -(t * (b.repr (f (b i))) j)
⊢ -(t * (b.repr (f (b i))) j) = 0

Tactic:
feq

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)) = 0
this : s * r + t * r * (b.repr (f (b j))) j = -(t * (b.repr (f (b i))) j)
⊢ -(t * (b.repr ((b.coord i) (f (b i)) • b i)) j) = 0
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 (1 • v)) x) = x

Tactic:
rw [← LinearMap.comp_apply, Units.smul_def, LinearMap.transvection.comp_smul_smul]

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⁻¹) + 1 + 1 * f v * ↑(-h.unit⁻¹)) • v)) x = x
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ (BilinForm.tensorDistrib R A) ((⅟2 • 2 • LinearMap.mul A A) ⊗ₜ[R] polarBilin Q) =
    BilinForm.tmul (LinearMap.mul A A) (polarBilin Q)

Tactic:
smul_comm,

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ (BilinForm.tensorDistrib R A) ((2 • ⅟2 • LinearMap.mul A A) ⊗ₜ[R] polarBilin Q) =
    BilinForm.tmul (LinearMap.mul A A) (polarBilin Q)
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)
a : A
m : M₂
⊢ (a * a) • Q₁ (1 ⊗ₜ[R] m) = (a * a) • Q₂ (1 ⊗ₜ[R] m)

Tactic:
h

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)
a : A
m : M₂
⊢ (a * a) • Q₂ (1 ⊗ₜ[R] m) = (a * a) • Q₂ (1 ⊗ₜ[R] m)
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
e : V ≃ₗ[K] V
⊢ e ∈ dilatransvections K V ↔ Module.rank K (V ⧸ (↑e).fixedSubmodule) ≤ 1

Tactic:
by
  rw [mem_dilatransvections_iff_rank, ← (quotKerEquivRange _).rank_eq, ← fixedSubmodule_eq_ker]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
x✝¹ x✝ : M₂
⊢ Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₁ (1 ⊗ₜ[R] x✝) =
    Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₂ (1 ⊗ₜ[R] x✝)

Tactic:
h

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
x✝¹ x✝ : M₂
⊢ Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₂ (1 ⊗ₜ[R] x✝) =
    Q₂ (1 ⊗ₜ[R] (x✝¹ + x✝)) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₂ (1 ⊗ₜ[R] x✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((AlgHom.op (toBaseChange A Q)).comp reverseOp).toLinearMap ∘ₗ ι (QuadraticForm.baseChange A Q)))
        1)
      v =
    ((TensorProduct.AlgebraTensorModule.curry
          (((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
                ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp
                  (toBaseChange A Q))).toLinearMap ∘ₗ
            ι (QuadraticForm.baseChange A Q)))
        1)
      v

Tactic:
change op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) =
    Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)
      (Algebra.TensorProduct.map (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))
        (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v))))

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ op ((toBaseChange A Q) (reverse ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)))) =
    (Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))
      ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp)
        ((toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v))))
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:
rw [LinearMap.smul_apply, RingHom.id_apply]
      induction x using CliffordAlgebra.left_induction with
      | algebraMap => simp_rw [foldr'_algebraMap, smul_zero]
      | add _ _ hx hy => rw [map_add, map_add, smul_add, hx, hy]
      | ι_mul _ _ hx =>
        rw [foldr'_ι_mul, foldr'_ι_mul, hx]
        dsimp only [contractLeftAux_apply_apply]
        rw [LinearMap.smul_apply, smul_assoc, mul_smul_comm, smul_sub]

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

Goal state before:
pp: case algebraMap
R : Type u_1
inst✝ : CommRing R
y : CliffordAlgebra 0
r : R
⊢ (algebraMap R (CliffordAlgebra 0)) r * y = y * (algebraMap R (CliffordAlgebra 0)) r

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case algebraMap
R : Type u_1
inst✝ : CommRing R
r : R
⊢ reverse ((algebraMap R (CliffordAlgebra 0)) r) = (algebraMap R (CliffordAlgebra 0)) r

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case pos
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 ↑ι
x y : ↑ι
h : x = y
⊢ (Finsupp.single y 1) x = 1 x y

Tactic:
h

Goal state after:
case pos
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 ↑ι
x y : ↑ι
h : x = y
⊢ (Finsupp.single y 1) y = 1 y y
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case algebraMap
r : ℝ
⊢ reverse ((algebraMap ℝ (CliffordAlgebra Q)) r) = (algebraMap ℝ (CliffordAlgebra Q)) r

Tactic:
| algebraMap r =>

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

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

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case algebraMap
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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x : CliffordAlgebra Q
r : R
⊢ f ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩ = g ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case mk.algebraMap
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
r : R
⊢ (((foldr Q (fFold f) ⋯) (((foldr Q (fFold f) ⋯) (1, 0)) val✝)) ((algebraMap R (CliffordAlgebra Q)) r)).1 =
    (aux f) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩ * (aux f) ⟨val✝, property✝⟩

Tactic:
| algebraMap r =>

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ (DirectSum.toModule R (ι × ι) (⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) fun i ↦
        have o := lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) (i.2, i.1);
        have s := (-1) ^ (i.1 * i.2);
        (s • o) ∘ₗ ↑(TensorProduct.comm R (𝒜 i.1) (ℬ i.2)))
      ((lof R (ι × ι) (fun i ↦ 𝒜 i.1 ⊗[R] ℬ i.2) (i, j)) (a ⊗ₜ[R] b)) =
    (-1) ^ (j * i) • (lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) (j, i)) (b ⊗ₜ[R] a)

Tactic:
simp [mul_comm i j]

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

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r : R
⊢ ↑((toEven Q) (reverse (involute ((algebraMap R (CliffordAlgebra Q)) r)))) =
    reverse ↑((toEven Q) ((algebraMap R (CliffordAlgebra Q)) r))

Tactic:
| algebraMap r =>

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
x y z : 𝒜 ᵍ⊗[R] ℬ
⊢ x * y * z = x * (y * z)

Tactic:
simp_rw [mul_def, mulHom_apply, LinearEquiv.apply_symm_apply]

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
x y z : 𝒜 ᵍ⊗[R] ℬ
⊢ (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x))
          (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) x)) ((auxEquiv R 𝒜 ℬ) y)))
        ((auxEquiv R 𝒜 ℬ) z)) =
    (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) x))
        (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) y)) ((auxEquiv R 𝒜 ℬ) z)))
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
⊢ ↑1 * (ι Q) m * ↑1⁻¹ ∈ (ι Q).range

Tactic:
inv_one,

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

Tactic:
inv_one,

Goal state after:
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
⊢ involute ↑1 * (ι Q) b * ↑1 ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
a✝ : Nontrivial R
x✝ : { s // LinearIndepOn R id s }
s : Set M
hs✝ : LinearIndepOn R id s
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
⊢ LinearIndependent R fun (x : ↑↑⟨s, hs✝⟩) ↦ M'.mkQ ↑x

Tactic:
simp_rw [linearIndependent_iff', ← map_smul, ← map_sum, mkQ_apply, Quotient.mk_eq_zero]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
a✝ : Nontrivial R
x✝ : { s // LinearIndepOn R id s }
s : Set M
hs✝ : LinearIndepOn R id s
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
⊢ ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ x ∈ s_1, g x • ↑x ∈ M' → ∀ i ∈ s_1, g i = 0