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

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
x : G
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) +
      ↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1))) =ᵐ[μ]
    ↑↑(condExpIndSMul hm hs hμs x) + ↑↑(condExpIndSMul hm ht hμt x)

Tactic:
rfl

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

Goal state before:
pp: α : 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)
⊢ (if h : SigmaFinite (μ.trim hm) ∧ Integrable f μ then
      if StronglyMeasurable f then f
      else
        have this := ⋯;
        AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯
    else 0) =
    if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯ else 0

Tactic:
grind

Goal state after:
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 ∂μ
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
have h_right : Tendsto (fun i => ∫ x in S i ∩ s, f x ∂μ) atTop (𝓝 (∫ x in s, f x ∂μ)) := by
    have h :=
      tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
        (L1.integrable_coeFn f).integrableOn
    rwa [← hs_eq] at h

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 ∂μ))
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᵐ[μ] g
hm : ¬m ≤ m₀
⊢ 0 =ᵐ[μ] 0

Tactic:
rfl

Goal state after:
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'
inst✝ : SigmaFinite (μ.trim hm)
⊢ ∫⁻ (a : α), ↑‖↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊

Tactic:
refine lintegral_le_of_forall_fin_meas_trim_le hm (μ s * ‖x‖₊) fun t ht hμt => ?_

Goal state after:
α : 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'
inst✝ : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ∫⁻ (x_1 : α) in t, ↑‖↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) x_1‖₊ ∂μ ≤ μ s * ↑‖x‖₊
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᵐ[μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : μ Set.univ = ∞
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 = fun x ↦ 0

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
inst✝ : SigmaFinite (μ.trim hm)
⊢ ∫⁻ (a : α), ↑‖↑↑(condExpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊

Tactic:
refine lintegral_le_of_forall_fin_meas_trim_le hm (μ s * ‖x‖₊) fun t ht hμt => ?_

Goal state after:
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
inst✝ : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ∫⁻ (x_1 : α) in t, ↑‖↑↑(condExpIndSMul hm hs hμs x) x_1‖₊ ∂μ ≤ μ s * ↑‖x‖₊
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : ¬m ≤ m0
⊢ 0 =ᵐ[μ.restrict s] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ.restrict s] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
α : 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 ⋯)
⊢ 0 =ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
α : 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 μ
⊢ 0 =ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict sᶜ] 0
hm : ¬m ≤ m0
⊢ 0 =ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
α : 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
⊢ 0 =ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
α : 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 : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ι : Type u_5
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
A : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), μ[f i | m] a = ↑↑(condExpL1 hm μ (f i)) a
B : ∑' (n : ι), ‖condExpL1 hm μ (f n)‖ₑ ≠ ∞
C : ↑↑(∑' (n : ι), condExpL1 hm μ (f n)) =ᵐ[μ] fun x ↦ ∑' (n : ι), ↑↑(condExpL1 hm μ (f n)) x
⊢ ↑↑(condExpL1 hm μ fun a ↦ ∑' (i : ι), f i a) =ᵐ[μ] fun a ↦ ∑' (i : ι), μ[f i | m] a

Tactic:
filter_upwards [A, C] with a ha h'a

Goal state after:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ι : Type u_5
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
A : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), μ[f i | m] a = ↑↑(condExpL1 hm μ (f i)) a
B : ∑' (n : ι), ‖condExpL1 hm μ (f n)‖ₑ ≠ ∞
C : ↑↑(∑' (n : ι), condExpL1 hm μ (f n)) =ᵐ[μ] fun x ↦ ∑' (n : ι), ↑↑(condExpL1 hm μ (f n)) x
a : α
ha : ∀ (i : ι), μ[f i | m] a = ↑↑(condExpL1 hm μ (f i)) a
h'a : ↑↑(∑' (n : ι), condExpL1 hm μ (f n)) a = ∑' (n : ι), ↑↑(condExpL1 hm μ (f n)) a
⊢ ↑↑(condExpL1 hm μ fun a ↦ ∑' (i : ι), f i a) a = ∑' (i : ι), μ[f i | m] a
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : ¬Integrable f μ
⊢ s.indicator 0 =ᵐ[μ] s.indicator 0

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᵐ[μ] μ[gs n | m]
hm : ¬m ≤ m₀
⊢ 0 =ᵐ[μ] 0

Tactic:
rfl

Goal state after:
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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

Tactic:
by
  borelize E
  obtain ⟨t, ht, htt⟩ := hf_int.aestronglyMeasurable.isSeparable_ae_range
  let Y := (Submodule.span ℝ t).topologicalClosure
  have : CompleteSpace Y := (Submodule.isClosed_topologicalClosure _).completeSpace_coe
  have : SecondCountableTopology Y := ht.span.closure.secondCountableTopology
  classical
  let fY : α → Y := fun a => if h : f a ∈ Y then ⟨f a, h⟩ else 0
  let fX : α → E := Y.subtypeL ∘ fY
  have lem0 : ∀ᵐ a ∂μ, f a ∈ Y := by
    filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)
  have lem1 : f =ᵐ[μ] fX := by
    filter_upwards [lem0] with a ha
    simp_all [fX, fY]
  have lem2 : ∀ᵐ a ∂μ, fY a ∈ Y.subtypeL ⁻¹' s := by
    filter_upwards [lem0, hf] with a ha hs
    simpa [fY, ha]
  have hfY_int : Integrable fY μ := by
    refine (hf_int.congr lem1).mono ?_ (by simp [fX])
    obtain ⟨g, hg1, hg2, hg3⟩ := hf_int.1.exists_stronglyMeasurable_range_subset
      ((Submodule.isClosed_topologicalClosure _).measurableSet) Nonempty.of_subtype lem0
    refine ⟨codRestrict g Y hg2, (hg1.measurable.codRestrict hg2).stronglyMeasurable, ?_⟩
    filter_upwards [hg3] with a ha
    have : g a ∈ Y := hg2 a
    simp_all [fY, codRestrict]
  have lem3 : μ[f | m] =ᵐ[μ] Y.subtypeL ∘ μ[fY | m] := calc
    _ =ᵐ[μ] μ[fX | m] := condExp_congr_ae lem1
    _ =ᵐ[μ] _ := (Y.subtypeL.comp_condExp_comm hfY_int).symm
  filter_upwards [(hc.linear_preimage Y.subtype).condExp_mem_of_hereditarilyLindelofSpace
    hm hfY_int (hs.preimage Y.subtypeL.continuous) lem2, lem3] with a ha hb
  simp_all

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᵐ[μ] μ[gs n | m]
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : ¬m ≤ m𝓧
⊢ (fun x ↦ 0) =ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : ¬SigmaFinite (μ.trim hm)
⊢ (fun x ↦ 0) =ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
hm : ¬m ≤ m₀
⊢ 0 ≤ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 ≤ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: case neg
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : ¬m ≤ m𝓧
⊢ 0 =ᵐ[μ] fun x ↦ 0

Tactic:
rfl

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

Goal state before:
pp: case neg
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ] fun x ↦ 0

Tactic:
rfl

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
inst✝ : SigmaFinite (Measure.map g ν)
s : Set ℝ≥0∞
hs : MeasurableSet s
⊢ g ⁻¹' (Measure.map g μ).rnDeriv (Measure.map g ν) ⁻¹' s =
    (fun a ↦ (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)) ⁻¹' s

Tactic:
grind

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

Goal state before:
pp: case hf
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
s : Set ℝ
hs : MeasurableSet s
⊢ (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) a).toReal) ∘ g ⁻¹' s =
    (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) ⁻¹' s

Tactic:
rfl

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

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
hm : m ≤ m𝓧
μ : Measure 𝓧
inst✝ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
h's : μ s ≠ ∞
x : 𝓧
⊢ 0 ≤ if x ∈ s then 1 else 0

Tactic:
grind

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₁
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₃ (g (f n))) (g (f m))

Tactic:
rfl

Goal state after:
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₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
⊢ (∑ σ, domCoprod.summand a b σ) v = 0

Tactic:
rw [_root_.sum_apply]

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₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
⊢ ∑ i, (domCoprod.summand a b i) v = 0
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✝⁵ : PartialOrder k
inst✝⁴ : IsOrderedAddMonoid k
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Module k V
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x < 0 ∨ 1 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hleft : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hright : w i = 1 - x
⊢ False

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
⊢ x⁻¹ * (w i - 1) + 1 = 0 ↔ w i = 1 - x

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_1.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
m₁ m₂ : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ •
      (MultilinearMap.domDomCongr a✝
          (MultilinearMap.domCoprod' (↑m₁ ⊗ₜ[R'] ↑n) + MultilinearMap.domCoprod' (↑m₂ ⊗ₜ[R'] ↑n)))
        x✝ =
    Perm.sign a✝ •
      ((MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m₁ ⊗ₜ[R'] ↑n))) x✝ +
        (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m₂ ⊗ₜ[R'] ↑n))) x✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_2.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (c • MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝ =
    Perm.sign a✝ • c • (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_3.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n₁ n₂ : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ •
      (MultilinearMap.domDomCongr a✝
          (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₁) + MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₂)))
        x✝ =
    Perm.sign a✝ •
      ((MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₁))) x✝ +
        (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₂))) x✝)

Tactic:
rfl

Goal state after:
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
Q : Type u_6
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
f : M →ₗ[R] N
p : P
⊢ ((j.linearMapLeftRightHom β) f) p = ((liftBaseChangeEquiv S) (β ∘ₗ f)) (j.equiv.symm p)

Tactic:
rfl

Goal state after: