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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ StronglyMeasurable
    (if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯ else 0)

Tactic:
split_ifs with hfi hfm

Goal state after:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ StronglyMeasurable f

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
⊢ StronglyMeasurable (AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯)

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ StronglyMeasurable 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝¹ : SigmaFinite (μ.trim hm)
this✝ : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
this : sᶜ.indicator μ[sᶜ.indicator f | m] =ᵐ[μ] μ[sᶜ.indicator f | m]
x : α
hx : sᶜ.indicator μ[sᶜ.indicator f | m] x = μ[sᶜ.indicator f | m] x
hxs : x ∈ s
⊢ s.indicator μ[sᶜ.indicator f | m] x = s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) x

Tactic:
simp only [hx, hxs, Set.indicator_of_mem]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this✝ : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
a✝ : ν (g ⁻¹' t) < ∞
⊢ ∫ (y : 𝓨) in t, ((Measure.map g μ).rnDeriv (Measure.map g ν) y).toReal ∂Measure.map g ν =
    ∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B : LinearMap.BilinForm R M
f : M₁ ≃ₗ[R] M
n✝ m✝ : M
⊢ ((B.comp ↑f ↑f) ((↑f.symm).toFun n✝)) ((↑f.symm).toFun m✝) = (B n✝) m✝

Tactic:
simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe,
        f.apply_symm_apply]

Goal state after:
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
s : AffineSubspace k P
p : ↥s
c : P
r : k
⊢ s.shift c r = map (↑(AffineEquiv.constVAdd k P ((1 - r) • (c -ᵥ ↑p)))) s

Tactic:
have h : Nonempty s := ⟨p⟩
  simp only [shift, h, ↓reduceDIte]
  ext q
  simp only [mem_map, AffineEquiv.coe_toAffineMap, AffineEquiv.constVAdd_apply]
  constructor <;> intro ⟨x, hx, heq⟩ <;> rw [← heq]
  · refine ⟨(1 - r) • (p.val -ᵥ h.some.val) +ᵥ x, ?_, ?_⟩
    · exact vadd_mem_of_mem_direction (smul_mem _ _ (vsub_mem_direction p.prop h.some.prop)) hx
    · rw [vadd_vadd, ← smul_add, vsub_add_vsub_cancel]
  · refine ⟨(1 - r) • (h.some.val -ᵥ p.val) +ᵥ x, ?_, ?_⟩
    · exact vadd_mem_of_mem_direction (smul_mem _ _ (vsub_mem_direction h.some.prop p.prop)) hx
    · rw [vadd_vadd, ← smul_add, vsub_add_vsub_cancel]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: 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 : ι
⊢ ((algebraMap R S) ((b.repr v) i) • (basis b ibc).repr (ε (b i))) i = (algebraMap R S) ((b.repr v) i)

Tactic:
← ibc.basis_apply

Goal state after:
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 : ι
⊢ ((algebraMap R S) ((b.repr v) i) • (basis b ibc).repr ((basis b ibc) i)) i = (algebraMap R S) ((b.repr v) i)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inl
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
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Subsingleton k
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) (1 - w i)

pp: case inr
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
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) (1 - w i)

Tactic:
· suffices (affineSpan k <| p '' {i}ᶜ) = ⊤ by simp [this]
    have : Subsingleton P := (AddTorsor.subsingleton_iff V P).mp <| Module.subsingleton k V
    simp

Goal state after:
case inr
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
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) (1 - w i)
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
h : i' ≠ i
⊢ ((algebraMap R S) ((b.repr v) i') • (basis b ibc).repr (ε (b i'))) i = 0

Tactic:
← ibc.basis_apply

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
⊢ ((algebraMap R S) ((b.repr v) i') • (basis b ibc).repr ((basis b ibc) 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
h : (Perm.sumCongrHom ιa ιb) (sl, sr) = σ₁⁻¹ * σ₂
v : ιa ⊕ ιb → Mᵢ
⊢ (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:
replace h := inv_mul_eq_iff_eq_mul.mp h.symm

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)
⊢ (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: case inr.mpr.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : r • (x -ᵥ c) +ᵥ c = p
⊢ (c -ᵥ ↑h.some) +ᵥ r • (x -ᵥ ↑h.some + (↑h.some -ᵥ c)) +ᵥ ↑h.some = r • (x -ᵥ c) +ᵥ c

Tactic:
vsub_add_vsub_cancel,

Goal state after:
case inr.mpr.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : r • (x -ᵥ c) +ᵥ c = p
⊢ (c -ᵥ ↑h.some) +ᵥ r • (x -ᵥ c) +ᵥ ↑h.some = r • (x -ᵥ c) +ᵥ c
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)
⊢ dilatransvection h ∈ dilatransvections R V

Tactic:
simp only [dilatransvections, Set.mem_ofPred_eq]

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)
⊢ ∃ f_1 v_1, ↑(dilatransvection h) = LinearMap.transvection f_1 v_1
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.tmul (LinearMap.mul A A) (associated Q) = BilinForm.baseChange A (associated Q)

Tactic:
exact rfl

Goal state after:
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
z : A
v : V
⊢ (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z * (ofBaseChangeAux A Q) ((ι Q) v) =
    (ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)

Tactic:
ofBaseChangeAux_ι,

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
z : A
v : V
⊢ (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z * (ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v) =
    (ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)
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
⊢ -1 ⊗ₜ[R] (ι Q) v = (Algebra.TensorProduct.map (AlgHom.id A A) involute) (1 ⊗ₜ[R] (ι Q) v)

Tactic:
Algebra.TensorProduct.map_tmul,

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
⊢ -1 ⊗ₜ[R] (ι Q) v = (AlgHom.id A A) 1 ⊗ₜ[R] involute ((ι Q) v)
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
⊢ op (1 ⊗ₜ[R] (ι Q) v) =
    (Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))
      ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp) (1 ⊗ₜ[R] (ι Q) v))

Tactic:
Algebra.TensorProduct.map_tmul,

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 (1 ⊗ₜ[R] (ι Q) v) =
    (Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))
      (↑(AlgEquiv.toOpposite A A) 1 ⊗ₜ[R] reverseOp ((ι Q) 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' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x

Tactic:
induction x using CliffordAlgebra.left_induction with

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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x

Tactic:
induction x using CliffordAlgebra.left_induction with

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

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

Tactic:
obtain ⟨f, v, he⟩ := he
  use (f.baseChange A), (1 ⊗ₜ[R] v)
  simp [he, LinearMap.transvection.baseChange]

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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (contractLeft d) ((contractLeft d) x) = 0

Tactic:
induction x using CliffordAlgebra.left_induction with

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

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

Tactic:
by
  ext
  dsimp only [LinearMap.comp_apply, Subtype.coe_mk, AlgHom.id_apply, AlgHom.toLinearMap_apply,
    AlgHom.comp_apply]
  rw [toComplex_ι, one_smul, ofComplex_I]

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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ (contractLeft d) ((contractLeft d') x) = -(contractLeft d') ((contractLeft d) x)

Tactic:
induction x using CliffordAlgebra.left_induction with

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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (changeForm h) ((contractLeft d) x) = (contractLeft d) ((changeForm h) x)

Tactic:
induction x using CliffordAlgebra.left_induction with

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

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

Tactic:
induction x using CliffordAlgebra.left_induction with

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

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

Tactic:
by
  induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [changeForm_algebraMap]
  | add _ _ hx hy => rw [map_add, hx, hy]
  | ι_mul _ _ hx => rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      sub_zero]

Goal state after:
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✝)) ((changeForm ⋯) x✝) + (contractLeft (B' m✝)) ((changeForm ⋯) x✝))

Tactic:
changeForm_contractLeft,

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✝) + (contractLeft (B m✝)) ((changeForm h') ((changeForm h) x✝))) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B m✝)) ((changeForm ⋯) x✝) + (contractLeft (B' m✝)) ((changeForm ⋯) x✝))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

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

Tactic:
induction x using CliffordAlgebra.left_induction with

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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
⊢ ∀ (x y : 𝒜 ᵍ⊗[R] ℬ),
    (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) (x * y) =
      (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) x *
        (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) y

Tactic:
by
      rw [LinearMap.map_mul_iff]
      ext a₁ : 3
      refine DirectSum.decompose_lhom_ext ℬ fun j₁ => ?_
      ext b₁ : 3
      refine DirectSum.decompose_lhom_ext 𝒜 fun i₂ => ?_
      ext a₂ b₂ : 2
      dsimp
      rw [tmul_coe_mul_coe_tmul]
      rw [@Units.smul_def _ _ (_) (_), ← Int.cast_smul_eq_zsmul R, map_smul, map_smul, map_smul]
      rw [Int.cast_smul_eq_zsmul R, ← @Units.smul_def _ _ (_) (_)]
      rw [of_symm_of, map_tmul, LinearMap.mul'_apply]
      simp_rw [AlgHom.toLinearMap_apply, map_mul]
      simp_rw [mul_assoc (f a₁), ← mul_assoc _ _ (g b₂), h_anti_commutes, mul_smul_comm,
        smul_mul_assoc, smul_smul, Int.units_mul_self, one_smul]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
⊢ (if a = i then -∑ x, M (i.succ.succAbove x) (id b) else M (i.succ.succAbove a) (id b)) =
    M (i.castSucc.succAbove a) (id b)

Tactic:
id_eq

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
⊢ (if a = i then -∑ x, M (i.succ.succAbove x) b else M (i.succ.succAbove a) b) = M (i.castSucc.succAbove a) b
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LT m
inst✝ : LT n
i : m
c : n
hA : A.IsPivotedBy l
hc : l i = ↑c
j : n
hj : j < c
⊢ ↑j < ↑c

Tactic:
exact_mod_cast hj

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
this : Fintype ι
bN : Module.Basis (Fin (Fintype.card ι)) ℤ ↥N
⊢ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
exact ⟨(bN.reindex (Fintype.equivFin _).symm).equivFun⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ ∑ x₁, ∑ x₂, A i x₁ * (B i' x₂ * Bᴴ x₂ j') * Aᴴ x₁ j = if i' = j' then ∑ x, A i x * (Fintype.card n • Aᴴ) x j else 0

Tactic:
by
        simp [← Finset.sum_mul, ← Finset.mul_sum, ← mul_apply, hB.mul_conjTranspose,
          one_apply, mul_assoc _ (Fintype.card n : R), -conjTranspose_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.WithConv

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
⊢ (star f).ofConv i j = f.ofConv i j

Tactic:
obtain (h | h) := hf i j <;> simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
⊢ Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Tactic:
wlog hf : Finite V
  · have : Infinite (ℙ k V) := by
      contrapose! hf
      rwa [finite_iff_of_finite] at hf
    have : n = 0 := by
      rw [← h]
      apply Module.finrank_of_not_finite
      contrapose hf
      simpa using Module.finite_of_finite k
    simp [this]
  have : 1 < Nat.card k := Finite.one_lt_card
  refine Nat.mul_right_cancel (m := Nat.card k - 1) (by lia) ?_
  let e : V ≃ₗ[k] (Fin n → k) := LinearEquiv.ofFinrankEq _ _ (by simpa)
  have hc : Nat.card V = Nat.card k ^ n := by simp [Nat.card_congr e.toEquiv, Nat.card_fun]
  zify
  conv_rhs => rw [Int.natCast_sub this.le, Int.natCast_one, geom_sum_mul]
  rw [← Int.natCast_mul, ← card k V, hc]
  simp

Goal state after: