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

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ∞
i : ℕ
⊢ ∀ ⦃b : ℕ⦄, i ≤ b → (fun i ↦ S i ∩ s) i ⊆ (fun i ↦ S i ∩ s) b

Tactic:
j

Goal state after:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ∞
i j : ℕ
⊢ i ≤ j → (fun i ↦ S i ∩ s) i ⊆ (fun i ↦ S i ∩ s) j
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E'
⊢ ↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) =
    (toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))

Tactic:
ext1
  refine (condExpL2_indicator_ae_eq_smul 𝕜 hm hs hμs x).trans ?_
  have h_comp := (toSpanSingleton ℝ x).coeFn_compLp
    (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α →₂[μ] ℝ)
  rw [← EventuallyEq] at h_comp
  refine EventuallyEq.trans ?_ h_comp.symm
  filter_upwards with y using rfl

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : ¬Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
klDiv_of_not_integrable h_int

Goal state after:
case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : ¬Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case pos
α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : f =ᵐ[μ] 0
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Tactic:
apply stronglyMeasurable_zero.aestronglyMeasurable.congr
    simp only [condExpL1_congr_ae hm hf', condExpL1_zero, ZeroMemClass.coe_zero]
    exact (coeFn_zero _ 1 _).symm

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 ν)
⊢ (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) =ᵐ[ν]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]

Tactic:
have : SigmaFinite (ν.trim hg.comap_le) := by
    rw [← map_trim_comap hg] at hσ
    refine SigmaFinite.of_map (ν.trim hg.comap_le) ?_ hσ
    refine Measurable.aemeasurable ?_
    exact measurable_iff_comap_le.mpr le_rfl

Goal state after:
𝓧 : 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 ⋯)
⊢ (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) =ᵐ[ν]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable ((fun x ↦ f ((∂Measure.map g μ/∂Measure.map g ν) x).toReal) ∘ g) ν

Tactic:
refine integrable_of_le_of_le (f := fun x ↦ f ((∂μ.map g/∂ν.map g) (g x)).toReal)
    (g₁ := fun x ↦ c * ((∂μ.map g/∂ν.map g) (g x)).toReal + c')
    (g₂ := fun x ↦ (ν[fun x ↦ f (μ.rnDeriv ν x).toReal | m𝓨.comap g]) x)
    ?_ ?_ ?_ ?_ integrable_condExp

Goal state after:
case refine_1
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ AEStronglyMeasurable (fun x ↦ f ((∂Measure.map g μ/∂Measure.map g ν) (g x)).toReal) ν

case refine_2
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ (fun x ↦ c * ((∂Measure.map g μ/∂Measure.map g ν) (g x)).toReal + c') ≤ᵐ[ν] fun x ↦
    f ((∂Measure.map g μ/∂Measure.map g ν) (g x)).toReal

case refine_3
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ (fun x ↦ f ((∂Measure.map g μ/∂Measure.map g ν) (g x)).toReal) ≤ᵐ[ν] fun x ↦
    ν[fun x ↦ f ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x

case refine_4
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (fun x ↦ c * ((∂Measure.map g μ/∂Measure.map g ν) (g x)).toReal + c') ν
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)
this : Perm.sign (σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) = Perm.sign σ₁ * (Perm.sign sl * Perm.sign sr)
⊢ ((Perm.sign sl • a ((fun i₁ ↦ v (σ₁ (Sum.inl i₁))) ∘ ⇑sl)) ⊗ₜ[R'] b fun i₂ ↦ v (σ₁ (Sum.inr i₂))) =
    (Perm.sign sl • a fun i₁ ↦ v ((σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inl i₁))) ⊗ₜ[R']
      (Perm.sign sr • b fun i₂ ↦ v ((σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inr i₂)))

Tactic:
b.map_congr_perm _ sr

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 sl • a ((fun i₁ ↦ v (σ₁ (Sum.inl i₁))) ∘ ⇑sl)) ⊗ₜ[R']
      (Perm.sign sr • b ((fun i₂ ↦ v (σ₁ (Sum.inr i₂))) ∘ ⇑sr)) =
    (Perm.sign sl • a fun i₁ ↦ v ((σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inl i₁))) ⊗ₜ[R']
      (Perm.sign sr • b fun i₂ ↦ v ((σ₁ * (Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inr i₂)))
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: 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

Tactic:
rcases hj : σ⁻¹ j with j' | j'

Goal state after:
case h.inl.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'
j' : ιa
hj : σ⁻¹ j = Sum.inl j'
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0

case h.inl.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' : ιa
hi : σ⁻¹ i = Sum.inl i'
j' : ιb
hj : σ⁻¹ j = Sum.inr j'
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: 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

Tactic:
rcases hj : σ⁻¹ j with j' | j'

Goal state after:
case h.inr.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' : ιb
hi : σ⁻¹ i = Sum.inr i'
j' : ιa
hj : σ⁻¹ j = Sum.inl j'
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0

case h.inr.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'
j' : ιb
hj : σ⁻¹ j = Sum.inr j'
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr.mp.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 : (1 - r) • (c -ᵥ ↑h.some) +ᵥ x = p
⊢ r • ((t • (x -ᵥ ↑h.some) +ᵥ ↑h.some) -ᵥ c) +ᵥ c = (1 - r) • (c -ᵥ ↑h.some) +ᵥ x

Tactic:
rw [vadd_vsub_assoc, smul_add, smul_smul, ht, sub_eq_add_neg, add_smul, one_smul, one_smul,
        neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]
      simp_rw [add_comm _ (r • (h.some.val -ᵥ c)), ← vadd_vadd, vsub_vadd_comm x h.some.val c]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
V : Type u_2
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
W : Type u_3
inst✝⁵ : AddCommMonoid W
inst✝⁴ : Module R W
A : Type u_4
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
f : Dual R V
v : V
⊢ (ibc.toDual f) (j v) = (algebraMap R A) (f v)

Tactic:
simp [toDual, linearMapLeftRightHom_comp_apply]

Goal state after:
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
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e).fixedSubmodule
⊢ e ∈ stabilizer (V ≃ₗ[R] V) W

Tactic:
rw [mem_stabilizer_submodule_iff_map_eq]

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e).fixedSubmodule
⊢ map (DistribSMul.toLinearMap R V e) W = W
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_6
inst✝¹⁰ : CommRing R
S : Type u_7
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_8
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
P : Type u_9
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
⊢ LinearMap.det (j.endHom f) = (algebraMap R S) (LinearMap.det f)

Tactic:
by
  rcases subsingleton_or_nontrivial R with hR | hR
  · have : f = 1 := by
      have : Subsingleton M := Module.subsingleton R M
      exact Subsingleton.eq_one f
    simp [this, endHom_one]
  let b := Module.finBasis R M
  rw [← f.det_toMatrix b, ← (j.endHom f).det_toMatrix (j.basis b),
    endHom_toMatrix, ← RingHom.mapMatrix_apply, ← RingHom.map_det]

Goal state after:
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₂
⊢ associated (QuadraticForm.tmul QuadraticMap.sq Q) = BilinForm.baseChange A (associated Q)

Tactic:
associated_tmul (QuadraticMap.sq (R := A)) Q,

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.tmul (associated QuadraticMap.sq) (associated Q) = BilinForm.baseChange A (associated Q)
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
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
hpure_tensor :
  ∀ (v w : V),
    (1 * 1) ⊗ₜ[R] ((ι Q) v * (ι Q) w) + (1 * 1) ⊗ₜ[R] ((ι Q) w * (ι Q) v) =
      ((QuadraticMap.polarBilin (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1
⊢ ∀ (m : A ⊗[R] V),
    (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) m *
        (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) m =
      (algebraMap A (A ⊗[R] CliffordAlgebra Q)) ((QuadraticForm.baseChange A Q) m)

Tactic:
by
      -- the crux is that by converting to a statement about linear maps instead of quadratic forms,
      -- we then have access to all the partially-applied `ext` lemmas.
      rw [CliffordAlgebra.forall_mul_self_eq_iff (isUnit_of_invertible _)]
      refine TensorProduct.AlgebraTensorModule.curry_injective ?_
      ext v w
      dsimp
      exact hpure_tensor v w

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

Goal state before:
pp: case refine_2
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : e ∈ dilatransvections K V
he' : e.fixedReduce = 1
⊢ e ∈ transvections K V

Tactic:
· by_cases he_one : e = 1
    · use 0, 0, by simp, by aesop
    have hefixed_ne_top : e.fixedSubmodule ≠ ⊤ := by
      rwa [ne_eq, LinearEquiv.fixedSubmodule_eq_top_iff]
    obtain ⟨w : V, hw : w ∉ e.fixedSubmodule⟩ :=
      SetLike.exists_not_mem_of_ne_top e.fixedSubmodule hefixed_ne_top rfl
    obtain ⟨f, hfw, hf⟩ := Submodule.exists_dual_map_eq_bot_of_notMem hw inferInstance
    rw [mem_dilatransvections_iff_finrank_quotient] at he
    have hf' : e.fixedSubmodule = LinearMap.ker f := by
      suffices finrank K (V ⧸ LinearMap.ker f) = 1 by
        apply Submodule.eq_of_le_of_finrank_le
        · intro x
          rw [mem_ker, ← Submodule.mem_bot K, ← hf]
          exact mem_map_of_mem
        rw [← Nat.add_le_add_iff_right, finrank_quotient_add_finrank] at he
        have := (LinearMap.ker f).finrank_quotient_add_finrank
        linarith
      rw [← Nat.add_left_inj, Submodule.finrank_quotient_add_finrank]
      rw [← f.finrank_ker_add_one_of_ne_zero, add_comm]
      aesop
    have eq_top : e.fixedSubmodule ⊔ Submodule.span K {w} = ⊤ := by
      rw [Submodule.sup_span_singleton_eq_top_iff hw]
      apply le_antisymm he
      apply Nat.one_le_of_lt
      rw [← Nat.ne_zero_iff_zero_lt]
      contrapose hefixed_ne_top
      apply eq_top_of_finrank_eq
      rw [← Nat.add_left_cancel_iff, finrank_quotient_add_finrank, hefixed_ne_top, zero_add]
    set v := (f w)⁻¹ • (e w - w)
    suffices hfv : f v = 0 by
      use f, v, hfv
      rw [← LinearEquiv.toLinearMap_inj,
        ← sub_eq_zero, ← LinearMap.ker_eq_top, eq_top_iff, ← eq_top]
      simp only [LinearEquiv.transvection.coe_toLinearMap,
        sup_le_iff, Submodule.span_singleton_le_iff_mem, LinearMap.mem_ker, LinearMap.sub_apply,
        LinearEquiv.coe_coe]
      constructor
      · intro x hx
        suffices f x = 0 by
          simpa [this, LinearMap.transvection.apply, sub_eq_zero] using hx
        rwa [hf', LinearMap.mem_ker] at hx
      · simp_all [v, LinearMap.transvection.apply]
    suffices e w - w ∈ LinearMap.ker f by
      simp only [LinearMap.mem_ker, map_sub] at this
      simp only [v, LinearMap.map_smul, map_sub, this, smul_zero]
    rw [← hf', ← Submodule.ker_mkQ e.fixedSubmodule, LinearMap.mem_ker]
    simp [Submodule.mkQ_apply, Submodule.Quotient.mk_sub, ← fixedReduce_mk, he']

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

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

Tactic:
by_cases h : x = y
      · rw [h]; simp
      · rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
⊢ CliffordAlgebraDualNumber.equiv ((ι 0) r) = r • ε

Tactic:
dsimp [CliffordAlgebraDualNumber.equiv, AlgEquiv.ofAlgHom]

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
⊢ ((CliffordAlgebra.lift 0) ⟨inrHom R R, ⋯⟩) ((ι 0) r) = r • ε
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
⊢ CliffordAlgebraDualNumber.equiv ((ι 0) r) = r • ε

Tactic:
by
  dsimp [CliffordAlgebraDualNumber.equiv, AlgEquiv.ofAlgHom]
  exact (lift_ι_apply _ _ r).trans (inr_eq_smul_eps _)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ CliffordAlgebraDualNumber.equiv.symm ε = (ι 0) 1

Tactic:
dsimp [CliffordAlgebraDualNumber.equiv, AlgEquiv.ofAlgHom]

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ (DualNumber.lift ⟨(Algebra.ofId R (CliffordAlgebra 0), (ι 0) 1), ⋯⟩) ε = (ι 0) 1
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✝
⊢ (changeForm h') ((changeForm h) ((ι Q) m✝ * x✝)) = (changeForm ⋯) ((ι Q) m✝ * x✝)

Tactic:
rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub,
      LinearMap.add_apply, map_add, LinearMap.add_apply, changeForm_contractLeft, hx,
      add_comm (_ : CliffordAlgebra Q'')]

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

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hfv : f v = 0
⊢ ↑(LinearEquiv.det (LinearEquiv.transvection hfv)) = ↑1

Tactic:
LinearEquiv.coe_det,

Goal state after:
R : Type u_3
V : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hfv : f v = 0
⊢ LinearMap.det ↑(LinearEquiv.transvection hfv) = ↑1