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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f g : β × γ → E
F : E → ℝ≥0∞
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
a✝ : β
h2f : Integrable (fun y ↦ f (a✝, y)) (η (a, a✝))
⊢ Integrable (fun y ↦ g (a✝, y)) (η (a, a✝)) →
    F (∫ (y : γ), f (a✝, y) - g (a✝, y) ∂η (a, a✝)) =
      F (∫ (y : γ), f (a✝, y) ∂η (a, a✝) - ∫ (y : γ), g (a✝, y) ∂η (a, a✝))

Tactic:
h2g

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f g : β × γ → E
F : E → ℝ≥0∞
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
a✝ : β
h2f : Integrable (fun y ↦ f (a✝, y)) (η (a, a✝))
h2g : Integrable (fun y ↦ g (a✝, y)) (η (a, a✝))
⊢ F (∫ (y : γ), f (a✝, y) - g (a✝, y) ∂η (a, a✝)) =
    F (∫ (y : γ), f (a✝, y) ∂η (a, a✝) - ∫ (y : γ), g (a✝, y) ∂η (a, a✝))
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1 : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2 : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
⊢ μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν

Tactic:
filter_upwards [h1, h2] with x h1 h2

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1✝ : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2✝ : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
x : 𝓧
h1 : μ'.rnDeriv ν' x = ((ν univ)⁻¹ • μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = ((ν univ)⁻¹⁻¹ • μ.rnDeriv ν) x
⊢ μ'.rnDeriv ν' x = μ.rnDeriv ν x
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ∞
⊢ ((κ ⊗ₖ η) a).real s • c = ∫ (x : β), (η (a, x)).real (Prod.mk x ⁻¹' s) • c ∂κ a

Tactic:
integral_smul_const,

Goal state after:
case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ∞
⊢ ((κ ⊗ₖ η) a).real s • c = (∫ (x : β), (η (a, x)).real (Prod.mk x ⁻¹' s) ∂κ a) • c
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
⊢ Integrable g (η a✝) → F (∫ (y : γ), f y + g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ + ∫ (y : γ), g y ∂η a✝)

Tactic:
h2g

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y + g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ + ∫ (y : γ), g y ∂η a✝)
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
⊢ Integrable g (η a✝) → F (∫ (y : γ), f y - g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ - ∫ (y : γ), g y ∂η a✝)

Tactic:
h2g

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y - g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ - ∫ (y : γ), g y ∂η a✝)
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
⊢ Integrable g (η a✝) → F (∫ (y : γ), f y - g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ - ∫ (y : γ), g y ∂η a✝)

Tactic:
h2g

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y - g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ - ∫ (y : γ), g y ∂η a✝)
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ∞
⊢ ((η ∘ₖ κ) a).real s • c = ∫ (x : β), (η x).real s • c ∂κ a

Tactic:
integral_smul_const,

Goal state after:
case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ∞
⊢ ((η ∘ₖ κ) a).real s • c = (∫ (x : β), (η x).real s ∂κ a) • c
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr.refine_3
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ ∞

Tactic:
refine ae_of_all _ (by simp)

Goal state after:
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:
by
  rw [Measure.compProd, ProbabilityTheory.integral_compProd hf]
  simp

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

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (c • ν).real univ - μ.real univ =
    ↑c * (∫ (a : α), llr (c⁻¹ • μ) ν a ∂c⁻¹ • μ + ν.real univ - (c⁻¹ • μ).real univ)

Tactic:
have h_smul (c : ℝ≥0) (a : ℝ) : c • a = c * a := rfl

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
h_smul : ∀ (c : ℝ≥0) (a : ℝ), c • a = ↑c * a
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (c • ν).real univ - μ.real univ =
    ↑c * (∫ (a : α), llr (c⁻¹ • μ) ν a ∂c⁻¹ • μ + ν.real univ - (c⁻¹ • μ).real univ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: case refine_1
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᵐ[μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ IntegrableOn g s μ

Tactic:
have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg

Goal state after:
case refine_1
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᵐ[μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
hfg_restrict : ↑↑↑f =ᵐ[μ.restrict s] g
⊢ IntegrableOn g s μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: case refine_2
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᵐ[μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, g x ∂μ = 0

Tactic:
have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg

Goal state after:
case refine_2
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᵐ[μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
hfg_restrict : ↑↑↑f =ᵐ[μ.restrict s] g
⊢ ∫ (x : α) in s, g x ∂μ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aestronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᵐ[μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᵐ[μ.restrict s] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_nnnorm_eq : (fun x ↦ ↑‖g x‖₊) =ᵐ[μ.restrict s] fun x ↦ ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊
⊢ Integrable (↑↑↑((condExpL2 ℝ ℝ hm) f)) (μ.restrict s)

Tactic:
exact integrableOn_condExpL2_of_measure_ne_top hm hμs f

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
n : ι
i : ℕ
⊢ μ (s n ∩ spanningSets (μ.restrict (s n)) i) ≠ ∞

Tactic:
rw [Set.inter_comm, ← Measure.restrict_apply' (s_meas n)]

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
n : ι
i : ℕ
⊢ (μ.restrict (s n)) (spanningSets (μ.restrict (s n)) i) ≠ ∞
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯) x ∂μ = ∫ (a : α) in s, ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫ ∂μ

Tactic:
←
      L2.inner_indicatorConstLp_eq_setIntegral_inner 𝕜 (↑(condExpL2 E 𝕜 hm f)) (hm s hs) c hμs.ne,

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯) x ∂μ = ⟪indicatorConstLp 2 ⋯ ⋯ c, ↑((condExpL2 E 𝕜 hm) f)⟫
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) < ∞
h_mono : Monotone fun i ↦ S i ∩ s
h_eq_forall : (fun i ↦ ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) = fun i ↦ ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ
h_right : Tendsto (fun i ↦ ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ) atTop (𝓝 (∫ (x : α) in s, ↑↑f x ∂μ))
⊢ Tendsto (fun i ↦ ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ))

Tactic:
have h := tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
      (L1.integrable_coeFn (condExpL1CLM F' hm μ f)).integrableOn

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) < ∞
h_mono : Monotone fun i ↦ S i ∩ s
h_eq_forall : (fun i ↦ ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) = fun i ↦ ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ
h_right : Tendsto (fun i ↦ ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ) atTop (𝓝 (∫ (x : α) in s, ↑↑f x ∂μ))
h :
  Tendsto (fun i ↦ ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) atTop
    (𝓝 (∫ (x : α) in ⋃ n, S n ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ))
⊢ Tendsto (fun i ↦ ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ))
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 α
s : Set E
inst✝¹ : IsFiniteMeasure μ
inst✝ : HereditarilyLindelofSpace E
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
L : ℕ → E →L[ℝ] ℝ
c : ℕ → ℝ
hLc1 : ∀ (i : ℕ), s.domRestrict ⇑(L i) + const (↑s) (c i) ≤ s.domRestrict φ
hLc2 : ⨆ i, s.domRestrict ⇑(L i) + const (↑s) (c i) = s.domRestrict φ
hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (fun x ↦ (L i) (μ[f | m] x) + c i) a = μ[fun y ↦ (L i) (f y) + c i | m] a
hw : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[⇑(L i) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
⊢ ∀ᵐ (a : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a

Tactic:
filter_upwards [hp, hw, hφ_cvx.1.condExp_mem hm hf_int hs hf] with a hp hw hq

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 α
s : Set E
inst✝¹ : IsFiniteMeasure μ
inst✝ : HereditarilyLindelofSpace E
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
L : ℕ → E →L[ℝ] ℝ
c : ℕ → ℝ
hLc1 : ∀ (i : ℕ), s.domRestrict ⇑(L i) + const (↑s) (c i) ≤ s.domRestrict φ
hLc2 : ⨆ i, s.domRestrict ⇑(L i) + const (↑s) (c i) = s.domRestrict φ
hp✝ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (fun x ↦ (L i) (μ[f | m] x) + c i) a = μ[fun y ↦ (L i) (f y) + c i | m] a
hw✝ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[⇑(L i) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
a : α
hp : ∀ (i : ℕ), (L i) (μ[f | m] a) + c i = μ[fun y ↦ (L i) (f y) + c i | m] a
hw : ∀ (i : ℕ), μ[⇑(L i) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
hq : μ[f | m] a ∈ s
⊢ φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
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₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
n : M₁
⊢ ∀ (m : M₁),
    (B₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun n)) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) =
      (B₁ n) m

Tactic:
m

Goal state after:
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₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
n m : M₁
⊢ (B₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun n)) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) = (B₁ n) m
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 : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ (↑(alternatization a)).domCoprod ↑(alternatization b) =
    ∑ σa, ∑ σb, Perm.sign σa • Perm.sign σb • (domDomCongr σa a).domCoprod (domDomCongr σb b)

Tactic:
simp_rw [← MultilinearMap.domCoprod'_apply, MultilinearMap.alternatization_coe]
  simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, _root_.map_sum,
    ← TensorProduct.smul_tmul', TensorProduct.tmul_smul]
  rfl

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

Goal state before:
pp: case refine_1.right
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 ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ e.fixedReduce = 1

Tactic:
rw [one_eq_refl, fixedReduce_eq_one, he]
      intro x
      apply ker_le_fixedSubmodule_transvection hfv
      rw [transvection.apply]
      simp [hfv]

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

Goal state before:
pp: c : CliffordAlgebra Q
⊢ toComplex (involute c) = (starRingEnd ℂ) (toComplex c)

Tactic:
have : toComplex (involute (ι Q 1)) = conj (toComplex (ι Q 1)) := by
    simp only [involute_ι, toComplex_ι, map_neg, one_smul, Complex.conj_I]
  suffices toComplex.comp involute = Complex.conjAe.toAlgHom.comp toComplex by
    exact AlgHom.congr_fun this c
  ext : 2
  exact this

Goal state after: