mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
⊢ (↑(transvection hfv * e)).fixedSubmodule = (↑e).fixedSubmodule ⊔ K ∙ v

Tactic:
by
  symm
  suffices e.fixedSubmodule ⊔ K ∙ v ≤ (transvection hfv * e).fixedSubmodule by
    apply Submodule.eq_of_le_of_finrank_le this
    rw [finrank_sup_span_singleton hv, add_comm]
    apply finrank_fixedSubmodule_dilatransvection_mul_le
    exact transvection_mem_dilatransvections hfv
  simp only [sup_le_iff, Submodule.span_singleton_le_iff_mem]
  have ht : e.fixedSubmodule ≤ (transvection hfv).fixedSubmodule := fun x hx ↦ by
    rw [mem_fixedSubmodule_transvection_iff, smul_eq_zero]
    left
    rw [← Submodule.mem_bot K, ← hf]
    exact mem_map_of_mem hx
  constructor
  · -- e.fixedSubmodule ≤ e'.fixedSubmodule
    intro x hx
    simp only [mem_fixedSubmodule_iff, LinearEquiv.coe_toLinearMap, LinearEquiv.mul_apply]
    suffices transvection hfv x = x by
      simp only [mem_fixedSubmodule_iff, LinearEquiv.coe_toLinearMap] at hx
      simp only [hx, this]
    rw [← LinearEquiv.coe_toLinearMap, ← mem_fixedSubmodule_iff]
    exact ht hx
  · -- u ∈ e.fixedSubmodule
    simp only [mem_fixedSubmodule_iff, LinearEquiv.coe_toLinearMap,
      LinearEquiv.mul_apply, transvection.apply]
    simp [hfv']

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case pos
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
hi₁ : i ∈ s₁
⊢ f i ∈ t₁' i

Tactic:
exact hf.1 i hi₁

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: case left
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : ↥(I ∪ J)) → α ↑i) := ⋯
⊢ (P (I ∪ J)) U = (P I) S

Tactic:
have h_eq_union : cylinder I S = cylinder (I ∪ J) U := by
      rw [← inter_cylinder, h_eq, inter_self]
    exact hP.congr_cylinder_of_subset hS h_eq_union.symm Finset.subset_union_left

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ : Measure ((i : ι) → α i)
hμ : IsProjectiveLimit μ P
I : Finset ι
⊢ μ univ = (P I) univ

Tactic:
rw [← cylinder_univ I, hμ.measure_cylinder _ MeasurableSet.univ]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : Nonempty ((i : ι) → α i)
s t : Finset ι
S : Set ((i : ↥s) → α ↑i)
T : Set ((i : ↥t) → α ↑i)
inst✝ : DecidableEq ι
⊢ cylinder s S ∩ cylinder t T ⊆ ∅ ↔ Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T ⊆ ∅

Tactic:
subset_empty_iff,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Nonempty ((i : ι) → α i)
s t : Finset ι
S : Set ((i : ↥s) → α ↑i)
T : Set ((i : ↥t) → α ↑i)
inst✝ : DecidableEq ι
⊢ cylinder s S ∩ cylinder t T = ∅ ↔ Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T = ∅
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

Tactic:
rw [pairwiseDisjoint_union]
  refine ⟨h_dis, hC.pairwiseDisjoint_disjointOfDiffUnion hs hI, fun u hu v hv _ ↦ ?_⟩
  simp_rw [id]
  exact disjoint_of_subset (subset_sUnion_of_mem hu) (subset_sUnion_of_mem hv)
    (hC.disjoint_sUnion_disjointOfDiffUnion hs hI)

Goal state after:
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ (⋃ a ∈ Au, ⋂ t ∈ a, t) ∪ ⋃ a ∈ Av, ⋂ t ∈ a, t = ⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t

Tactic:
← biUnion_union

Goal state after:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ ⋃ x ∈ Au ∪ Av, ⋂ t ∈ x, t = ⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t
Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct

Goal state before:
pp: M : Type u_3
N : Type u_1
α : Type u_4
β : Type u_2
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableConstSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : SMul N β
inst✝ : ContinuousConstSMul N β
⊢ ∀ (m : Mᵈᵐᵃ) (n : N) (a : α →ₘ[μ] β), m • n • a = n • m • a

Tactic:
rintro _ _ ⟨_⟩

Goal state after:
case mk
M : Type u_3
N : Type u_1
α : Type u_4
β : Type u_2
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableConstSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : SMul N β
inst✝ : ContinuousConstSMul N β
m✝ : Mᵈᵐᵃ
n✝ : N
a✝¹ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ m✝ • n✝ • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝ = n✝ • m✝ • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ (eLpNormEssSup f μ).toReal < (eLpNormEssSup f μ + 1).toReal

Tactic:
ENNReal.toReal_lt_toReal hbdd.ne

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ eLpNormEssSup f μ < eLpNormEssSup f μ + 1

α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ eLpNormEssSup f μ + 1 ≠ ∞
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ v x✝ = 0

Tactic:
v.not_measurable hi

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Measure.Complex

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ re c ≪ᵥ μ ∧ im c ≪ᵥ μ

pp: case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
⊢ c ≪ᵥ μ

Tactic:
· constructor <;> · intro i hi; simp [h hi]

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
⊢ c ≪ᵥ μ
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
hij : j ⊆ i
⊢ (v.restrict i) j = v j

Tactic:
rw [restrict_apply v hi hj, Set.inter_eq_left.2 hij]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

Tactic:
have hk₂ : s ≤[i \ ⋃ l < k, restrictNonposSeq s i l] 0 := Nat.find_spec hn

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
i : Set α
hi : MeasurableSet i
⊢ (toSignedMeasure 0) i = 0 i

Tactic:
rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
    FunLike.coe_zero, Pi.zero_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ f x = ({x | M ≤ ↑‖f x‖₊}.indicator f + {x | ‖f x‖ < M}.indicator f) x

Tactic:
rw [Pi.add_apply, Set.indicator_of_mem, Set.indicator_of_notMem, add_zero]

Goal state after:
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ x ∉ {x | ‖f x‖ < M}

case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁ = j₂

Tactic:
ext1
  · exact hj
  · rw [← toSignedMeasure_eq_toSignedMeasure_iff]
    unfold toSignedMeasure at hj'
    simp_rw [hj, sub_right_inj] at hj'
    exact hj'

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : Fin (n + 1)) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
let g : Fin n → α → β := fun k => f k.castSucc

Goal state after:
case succ
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : Fin (n + 1)) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ (v.trim hle) (j ∩ i) = (v.restrict i) j

pp: case hi
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

pp: case hj
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j

Tactic:
restrict_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ (v.trim hle) (j ∩ i) = v (j ∩ i)

case hi
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

case hj
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j

case hi
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

case hj
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (f • g) x ∂μ = ((μ.withDensity fun x ↦ ↑(f x)).withDensityᵥ g) s

Tactic:
withDensityᵥ_apply ((integrable_withDensity_iff_integrable_smul₀ hf).mpr hfg) hs,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (f • g) x ∂μ = ∫ (x : α) in s, g x ∂μ.withDensity fun x ↦ ↑(f x)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
⊢ (s.toMeasureOfLEZero i hi₁ hi) univ < ∞

Tactic:
toMeasureOfLEZero_apply s hi hi₁ MeasurableSet.univ

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
⊢ ↑(NNReal.mk (-s (i ∩ univ)) ⋯) < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℚ≥0 E
inst✝ : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ lpNorm (𝔼 i ∈ s, f i) p μ ≤ 𝔼 i ∈ s, lpNorm (f i) p μ

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℚ≥0 E
inst✝ : NormedSpace ℝ E
ι : Type u_3
f : ι → α → E
hp : 1 ≤ p
hf : ∀ i ∈ ∅, MemLp (f i) p μ
⊢ lpNorm (𝔼 i ∈ ∅, f i) p μ ≤ 𝔼 i ∈ ∅, lpNorm (f i) p μ

case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℚ≥0 E
inst✝ : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ lpNorm (𝔼 i ∈ s, f i) p μ ≤ 𝔼 i ∈ s, lpNorm (f i) p μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : ¬m ≤ m0
a : α
⊢ μ[f | m] a ≤ c

Tactic:
by simpa [condExp_of_not_le hm]

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : HasOuterApproxClosed Ω
inst✝¹ : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝ : IsFiniteMeasure μ
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν
F : Set Ω
F_closed : IsClosed[inst✝³] F
ν_finite : IsFiniteMeasure ν
obs_μ : Tendsto (fun n ↦ ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂μ) atTop (𝓝 (μ F))
obs_ν : Tendsto (fun n ↦ ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂ν) atTop (𝓝 (ν F))
⊢ μ F = ν F

Tactic:
simp_rw [h] at obs_μ

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : HasOuterApproxClosed Ω
inst✝¹ : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝ : IsFiniteMeasure μ
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν
F : Set Ω
F_closed : IsClosed[inst✝³] F
ν_finite : IsFiniteMeasure ν
obs_ν : Tendsto (fun n ↦ ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂ν) atTop (𝓝 (ν F))
obs_μ : Tendsto (fun n ↦ ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂ν) atTop (𝓝 (μ F))
⊢ μ F = ν F
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
R : E
f : α → E
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ R
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ R

Tactic:
by_cases! hn : {x | |f x| ≤ R} = ∅
  · exact measure_mono_null (by simp) <| ae_eq_empty.1 (hn ▸ (ae_eq_univ.2 hbdd).symm)
  have hR : 0 ≤ R := (abs_nonneg _).trans hn.some_mem
  exact (abs_condExp_ae_le_condExp_abs f).trans (condExp_le_nonneg_const (m := m) hR hbdd)

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑μ.mass⁻¹ * ↑μ s = (μ.mass⁻¹ • ↑μ) s

Tactic:
exact Measure.coe_nnreal_smul_apply _ _ _

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : ↑C ^ ENNReal.toReal 1 * μ {x | ↑C ≤ ↑‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ ENNReal.toReal 1
⊢ μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ

Tactic:
rw [ENNReal.toReal_one, ENNReal.rpow_one, mul_comm, ←
      ENNReal.le_div_iff_mul_le (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne'))
        (Or.inl ENNReal.coe_lt_top.ne)] at this

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | ↑C ≤ ↑‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ UniformIntegrable f p μ

Tactic:
set g : ι → α → β := fun i => (hf i).choose
  have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hf i).1
  have hgeq : ∀ i, g i =ᵐ[μ] f i := fun i => (Exists.choose_spec <| hf i).2.symm
  refine (uniformIntegrable_of' hp hp' hgmeas fun ε hε => ?_).ae_eq hgeq
  obtain ⟨C, hC⟩ := h ε hε
  refine ⟨C, fun i => le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)⟩
  filter_upwards [(Exists.choose_spec <| hf i).2] with x hx
  by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
  · rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
    rwa [Set.mem_ofPred, hx] at hfx
  · rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]
    rwa [Set.mem_ofPred, hx] at hfx

Goal state after: