mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
a✝ : MeasurableSet s
⊢ ((κ.map g) (f x)) s = (((κ.comap f hf).map g) x) s

Tactic:
map_apply _ hg,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
a✝ : MeasurableSet s
⊢ (Measure.map g (κ (f x))) s = (((κ.comap f hf).map g) x) s
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
a✝ : MeasurableSet s
⊢ (Measure.map g (κ (f x))) s = (((κ.comap f hf).map g) x) s

Tactic:
map_apply _ hg,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
a✝ : MeasurableSet s
⊢ (Measure.map g (κ (f x))) s = (Measure.map g ((κ.comap f hf) x)) s
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (μ ⊗ₘ κ) (s ×ˢ univ) = 0
⊢ μ s = 0

Tactic:
rw [Measure.compProd_apply_prod hs MeasurableSet.univ, lintegral_eq_zero_iff] at h2

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (fun a ↦ (κ a) univ) =ᵐ[μ.restrict s] 0
⊢ μ s = 0

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : ∫⁻ (a : α) in s, (κ a) univ ∂μ = 0
⊢ Measurable fun a ↦ (κ a) univ
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
⊢ ∀ᵐ (x : α) ∂ξ, κ x ⟂ₘ η x

Tactic:
by
  have hs : MeasurableSet h.nullSet := h.measurableSet_nullSet
  have hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0 := h.measure_nullSet
  have hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0 := h.measure_compl_nullSet
  rw [compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero
  · filter_upwards [hμ hμ_zero, hν hν_zero] with x hxμ hxν
    exact ⟨Prod.mk x ⁻¹' h.nullSet, measurable_prodMk_left hs, ⟨hxμ, hxν⟩⟩
  · exact (Kernel.measurable_kernel_prodMk_left hs.compl).aemeasurable
  · exact (Kernel.measurable_kernel_prodMk_left hs).aemeasurable
  · exact hs.compl
  · exact hs

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
hp : MeasurableSet {z | p z}
h : ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂κ y, p z
⊢ ∀ᵐ (z : β) ∂(κ ∘ₖ Kernel.const Unit μ) (), p z

Tactic:
exact Kernel.ae_comp_of_ae_ae hp h

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ μ.tilted f = 0

Tactic:
by
  rw [Measure.tilted, integral_undef hf]
  simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
⊢ ∫ (x : α) in Set.univ, g x ∂μ.tilted f = ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
setIntegral_tilted' f g MeasurableSet.univ,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
⊢ ∫ (x : α) in Set.univ, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ =
    ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ ⊗ₘ κ)
⊢ ∫ (x : α × β), f x ∂μ ⊗ₘ κ = ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ

Tactic:
rw [Measure.compProd, ProbabilityTheory.integral_compProd hf]
  simp

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

Goal state before:
pp: case neg.h_int
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ Integrable (llr (c • μ) ν) (c • μ)

Tactic:
refine Integrable.smul_measure_nnreal ?_
    rw [integrable_congr (llr_smul_nnreal_left hμν c (by simpa))]
    fun_prop

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

Goal state before:
pp: α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
⊢ f =ᵐ[μ] g

Tactic:
rw [← ae_eq_trim_iff_of_aestronglyMeasurable hm hfm hgm]

Goal state after:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable.mk f hfm =ᵐ[μ.trim hm] AEStronglyMeasurable.mk g hgm
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case inl
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ 0[f | ⊥] =ᵐ[0] fun x ↦ (Measure.real 0 Set.univ)⁻¹ • ∫ (x : α), f x ∂0

Tactic:
rw [ae_zero]; exact eventually_bot

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst✝⁴ : NormedAddCommGroup E
inst✝³ : PartialOrder E
inst✝² : NormedSpace ℝ E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
hx : 0 ≤ x
⊢ 0 ≤ᵐ[μ] ↑↑(condExpIndSMul hm hs hμs x)

Tactic:
refine EventuallyLE.trans_eq ?_ (condExpIndSMul_ae_eq_smul hm hs hμs x).symm

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst✝⁴ : NormedAddCommGroup E
inst✝³ : PartialOrder E
inst✝² : NormedSpace ℝ E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
hx : 0 ≤ x
⊢ 0 ≤ᵐ[μ] fun a ↦ ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : 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 (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (fun p ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ =
    ∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ + ∫ (p : 𝓧 × 𝓨), log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ

Tactic:
rw [integral_add h_int1]

Goal state after:
𝓧 : 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 (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (fun p ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ Integrable (fun p ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) (μ ⊗ₘ κ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst✝ : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : Integrable f μ
⊢ μ[μ[f | m₂] | m₁] =ᵐ[μ] μ[f | m₁]

Tactic:
refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' (hm₁₂.trans hm₂)
    (fun s _ _ => integrable_condExp.integrableOn) (fun s _ _ => integrable_condExp.integrableOn) ?_
    stronglyMeasurable_condExp.aestronglyMeasurable
    stronglyMeasurable_condExp.aestronglyMeasurable

Goal state after:
case pos
α : Type u_1
E : Type u_3
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst✝ : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : Integrable f μ
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, μ[μ[f | m₂] | m₁] x ∂μ = ∫ (x : α) in s, μ[f | m₁] x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case refine_1
α : 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]
⊢ s.indicator f =ᵐ[μ.restrict sᶜ] 0

pp: case refine_2
α : 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]
⊢ μ[s.indicator (s.indicator f) | m] =ᵐ[μ] μ[s.indicator f | m]

Tactic:
· exact indicator_ae_eq_restrict_compl (hm _ hs)

Goal state after:
case refine_2
α : 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]
⊢ μ[s.indicator (s.indicator f) | m] =ᵐ[μ] μ[s.indicator f | m]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, (c • P⁻[X | mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (c • X) ω ∂P

Tactic:
simp only [Pi.smul_apply, smul_eq_mul]

Goal state after:
case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, c * P⁻[X | mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, (c • P⁻[X | mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (c • X) ω ∂P

Tactic:
simp only [Pi.smul_apply, smul_eq_mul]

Goal state after:
case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, c * P⁻[X | mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hl : LowerSemicontinuousOn (fun x ↦ x ^ p) (Ici 0)
this : (fun x ↦ x ^ p) ∘ μ[fun a ↦ ‖f a‖ | m] ≤ᵐ[μ] μ[(fun x ↦ x ^ p) ∘ fun a ↦ ‖f a‖ | m]
⊢ (fun x ↦ ‖μ[f | m] x‖ ^ p) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ ^ p | m]

Tactic:
filter_upwards [norm_condExp_le f, this] with a ha hb

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hl : LowerSemicontinuousOn (fun x ↦ x ^ p) (Ici 0)
this : (fun x ↦ x ^ p) ∘ μ[fun a ↦ ‖f a‖ | m] ≤ᵐ[μ] μ[(fun x ↦ x ^ p) ∘ fun a ↦ ‖f a‖ | m]
a : α
ha : ‖μ[f | ?m.214] a‖ ≤ μ[fun x ↦ ‖f x‖ | ?m.214] a
hb : ((fun x ↦ x ^ p) ∘ μ[fun a ↦ ‖f a‖ | m]) a ≤ μ[(fun x ↦ x ^ p) ∘ fun a ↦ ‖f a‖ | m] a
⊢ ‖μ[f | m] a‖ ^ p ≤ μ[fun x ↦ ‖f x‖ ^ p | m] a
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
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:
obtain ⟨j, hj⟩ := exists_ne i

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
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) (1 - w 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
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) c → w i = 1 - c

Tactic:
obtain ⟨j, hj⟩ := exists_ne i

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
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) c → w i = 1 - c
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ (Finsupp.llift N R R ι).symm
⊢ Function.Bijective ⇑(linearMapRightBaseChangeHom S M ε)

Tactic:
let f := (b.repr.congrLeft P S).trans (Finsupp.llift P R S ι).symm

Goal state after:
R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ (Finsupp.llift N R R ι).symm
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ (Finsupp.llift P R S ι).symm
⊢ Function.Bijective ⇑(linearMapRightBaseChangeHom S M ε)
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 = 0 ∨ r * (b.coord j) (f (b j)) - (b.coord i) (f (b i)) * r = 0
⊢ (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))

Tactic:
sub_eq_zero

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 = 0 ∨ r * (b.coord j) (f (b j)) = (b.coord i) (f (b i)) * r
⊢ (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
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
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ ↑↑(AlgEquiv.toOpposite A A))
        (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      (↑(toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)

Tactic:
AlgEquiv.toLinearEquiv_toOpposite

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
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ ↑(opLinearEquiv A))
        (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      (↑(toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) 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 : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ ((contractLeftAux Q d) x) (1, 0) = (algebraMap R (CliffordAlgebra Q)) (d x)

Tactic:
simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero,
      Algebra.algebraMap_eq_smul_one]

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
f : Dual R V
v : V
h : f v = 0
hA : ((Dual.baseChange A) f) (1 ⊗ₜ[R] v) = 0
⊢ LinearEquiv.baseChange R A V V (transvection h) = transvection hA

Tactic:
simp [← toLinearMap_inj, coe_baseChange,
    LinearEquiv.transvection.coe_toLinearMap, LinearMap.transvection.baseChange]

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ M →ₗ[R] ↥(even (Q' Q))

Tactic:
refine LinearMap.codRestrict _ ?_ fun m => Submodule.mem_iSup_of_mem ⟨2, rfl⟩ ?_

Goal state after:
case refine_1.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ M →ₗ[R] CliffordAlgebra (Q' Q)

case refine_1.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ?refine_1.refine_1 m ∈ (ι (Q' Q)).range ^ ↑⟨2, ⋯⟩
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)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
⊢ ((gradedMul R 𝒜 ℬ) 1) x = x

Tactic:
simpa only [RingHom.map_one, one_smul] using! algebraMap_gradedMul 𝒜 ℬ 1 x

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 : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
x✝¹ : A
x✝ : B
⊢ F (x✝¹ ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] x✝) = F ((of R 𝒜 ℬ) (x✝¹ ⊗ₜ[R] x✝))

Tactic:
tmul_one_mul_one_tmul

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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
x✝¹ : A
x✝ : B
⊢ F (x✝¹ ᵍ⊗ₜ[R] x✝) = F ((of R 𝒜 ℬ) (x✝¹ ⊗ₜ[R] x✝))
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Basic

Goal state before:
pp: case inr
m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝³ : Zero R
inst✝² : LinearOrder m
inst✝¹ : LT n
inst✝ : One R
i₁ i₂ : m
c : n
hA : A.IsReducedRowEchelon
hne : i₁ ≠ i₂
hlead : A.IsLeadingEntry i₂ c
hlt : i₂ < i₁
⊢ A i₁ c = 0

Tactic:
exact hA.isRowEchelon hlt hlead.1

Goal state after: