mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
⊢ LowerSemicontinuousOn (fun x ↦ f (M x) x) s

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
⊢ x ∈ s → SemicontinuousWithinAt (fun x1 x2 ↦ (fun x ↦ f (M x) x) x1 > x2) s x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h
⊢ ∀ i < ⊤, ∃ i', Ico ↑i' ⊤ ⊆ Ici i ∩ {⊤}ᶜ

Tactic:
intro x

Goal state after:
case h
x : EReal
⊢ x < ⊤ → ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h
⊢ ∀ (i : EReal), ⊥ < i → ∃ i', Ioc ⊥ ↑i' ⊆ Iic i ∩ {⊥}ᶜ

Tactic:
intro x

Goal state after:
case h
x : EReal
⊢ ⊥ < x → ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
⊢ μ ∅ ≤ 0

Tactic:
exact (iInf_le_of_le fun _ => ∅) <| iInf_le_of_le (empty_subset _) <| by simpa

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ LowerSemicontinuous fun p ↦ p.1 + p.2

Tactic:
intro x

Goal state after:
x : EReal × EReal
⊢ SemicontinuousAt (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.1 * a.2

Tactic:
intro x

Goal state after:
x : ℝ
⊢ ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.1 * a.2
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
h : 0 < a
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 * a.2

Tactic:
intro x

Goal state after:
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 * a.2
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ μ ≤ boundedBy m ↔ ∀ (s : Set α), μ s ≤ m s

Tactic:
boundedBy,

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ μ ≤ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : s.Nonempty), m s) ⋯ ↔ ∀ (s : Set α), μ s ≤ m s
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
k : ℕ
hn : 0 < k.succ
⊢ ∀ i ∈ Finset.range k, 0 ≤ (↑i + 1 + 1) * (↑k + 1)⁻¹

Tactic:
intro x

Goal state after:
case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
⊢ x ∈ Finset.range k → 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
k : ℕ
hn : 0 < k.succ
⊢ ∀ i ∈ Finset.range k, (↑i + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
intro x

Goal state after:
case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
⊢ x ∈ Finset.range k → (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable α
p : α → Prop
⊢ μ {a | ¬p a} = 0 ↔ ∀ (x : α), μ {x} ≠ 0 → p x

Tactic:
measure_null_iff_singleton

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable α
p : α → Prop
⊢ (∀ x ∈ {a | ¬p a}, μ {x} = 0) ↔ ∀ (x : α), μ {x} ≠ 0 → p x

α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable α
p : α → Prop
⊢ {a | ¬p a}.Countable
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π S

Tactic:
refine Subset.trans ?_ (piiUnionInter_mono_right h_ss)

Goal state after:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π {i}
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ MeasurableSet (⋂ i, U i)

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ⊆ ⋂ i, V i

Tactic:
· have := ht.countable.toEncodable.countable
    exact MeasurableSet.iInter fun i => (hU i).1

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ⊆ ⋂ i, V i
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋂ i, ⋃ j, ⋃ (_ : p j ∧ i ≤ j), s j)

Tactic:
exact .iInter fun _ => .iUnion fun m => .iUnion fun hm => h m hm.1

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: ι : Type u_8
ι' : Type u_9
e : ι ≃ ι'
β : ι' → Type u_10
inst✝ : (i' : ι') → MeasurableSpace (β i')
x : (i : ι) → β (e i)
i : ι
⊢ (piCongrLeft (fun i' ↦ β i') e) x (e i) = x i

Tactic:
by
  rw [piCongrLeft, coe_mk, Equiv.piCongrLeft_apply_apply]

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

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u : Set α
⊢ AEDisjoint μ (s ∪ t) u ↔ AEDisjoint μ s u ∧ AEDisjoint μ t u

Tactic:
by
  simp [union_eq_iUnion, and_comm]

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

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u : Set α
⊢ AEDisjoint μ s (t ∪ u) ↔ AEDisjoint μ s t ∧ AEDisjoint μ s u

Tactic:
by
  simp [union_eq_iUnion, and_comm]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Nonempty α
hf : MeasurableEmbedding f
⊢ LeftInverse hf.invFun f

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Nonempty α
hf : MeasurableEmbedding f
x : α
⊢ hf.invFun (f x) = x
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s

Tactic:
· have : toMeasurable μ (s \ t) =ᵐ[μ] (∅ : Set α) := by simp [ae_le_set.1 hst.le]
    simpa only [union_empty] using hst.symm.union this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ (map f μ) univ = 0 ↔ μ univ = 0

Tactic:
map_apply_of_aemeasurable hf .univ,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ μ (f ⁻¹' univ) = 0 ↔ μ univ = 0
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ 2 • ν ≪ ν

Tactic:
exact AbsolutelyContinuous.rfl.smul_left 2

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑e ⁻¹' s =ᵐ[μ] s

Tactic:
convert! he.preimage_ae_eq hs.symm

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑e ⁻¹' s =ᵐ[μ] s ↔ ⇑e ⁻¹' s =ᵐ[μ] ⇑e ⁻¹' ⇑e '' s
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
⊢ False

Tactic:
rcases not_subset_iff_exists_mem_notMem.mp hsub with ⟨a, has, ha⟩

Goal state after:
case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
⊢ False
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
⊢ LocallyFinite fun n ↦ Icc (f n) (g n)

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
⊢ ∃ t ∈ 𝓝 x, {i | ((fun n ↦ Icc (f n) (g n)) i ∩ t).Nonempty}.Finite
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ∞
this : ∀ {s : Set α}, (sum fun n ↦ c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0
⊢ ∃ ν, IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ

Tactic:
refine ⟨.sum fun n ↦ c n • sfiniteSeq μ n, ⟨?_⟩, fun _ ↦ this.1, fun _ ↦ this.2⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ∞
this : ∀ {s : Set α}, (sum fun n ↦ c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0
⊢ (sum fun n ↦ c n • sfiniteSeq μ n) univ < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
decr : Antitone fun n ↦ ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i ⊆ ∅

Tactic:
intro x

Goal state after:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
decr : Antitone fun n ↦ ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
⊢ x ∈ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i → x ∈ ∅
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ∞
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
by
  refine le_antisymm (le_iInf fun i ↦ measure_mono <| iInter_subset _ _) ?_
  have := hfin.nonempty
  rcases exists_seq_antitone_tendsto_atTop_atBot ι with ⟨x, hxm, hx⟩
  calc
    ⨅ i, μ (s i) ≤ ⨅ n, μ (s (x n)) := le_iInf_comp (μ ∘ s) x
    _ = μ (⋂ n, s (x n)) := by
      refine .symm <| (hs.comp_antitone hxm).directed_ge.measure_iInter (fun n ↦ hsm _) ?_
      rcases hfin with ⟨k, hk⟩
      rcases (hx.eventually_le_atBot k).exists with ⟨n, hn⟩
      exact ⟨n, ne_top_of_le_ne_top hk <| measure_mono <| hs hn⟩
    _ ≤ μ (⋂ i, s i) := by
      refine measure_mono <| iInter_mono' fun i ↦ ?_
      rcases (hx.eventually_le_atBot i).exists with ⟨n, hn⟩
      exact ⟨n, hs hn⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
hMono : Monotone t
⊢ μ (t i) ≠ ∞

Tactic:
rwa [← measure_congr (hst i)]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
hMono : Monotone t
⊢ μ (⋂ i, s i) = μ (⋂ i, t i)

Tactic:
refine measure_congr ?_

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
hMono : Monotone t
⊢ ⋂ i, s i =ᵐ[μ] ⋂ i, t i
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen[inst✝¹] u → ∃ v ∈ {s | IsOpen[inst✝¹] s ∧ μ s < ∞}, a ∈ v ∧ v ⊆ u

Tactic:
intro x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
⊢ ∀ (u : Set α), x ∈ u → IsOpen[inst✝¹] u → ∃ v ∈ {s | IsOpen[inst✝¹] s ∧ μ s < ∞}, x ∈ v ∧ v ⊆ u
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
⊢ μ.restrict (⋃ i ∈ S, i) = ν.restrict (⋃ i ∈ S, i) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s

Tactic:
restrict_biUnion_congr hc

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
⊢ (∀ i ∈ S, μ.restrict i = ν.restrict i) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
⊢ map f (μ.restrict s) ≪ ν.restrict t

Tactic:
by
    refine AbsolutelyContinuous.mk fun u hum ↦ ?_
    suffices ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0 by simpa [hum, hf.measurable, hf.measurable hum]
    refine fun hu ↦ measure_mono_null ?_ (hf.preimage_null hu)
    rw [preimage_inter]
    gcongr
    assumption

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
intro x

Goal state after:
case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
⊢ x ∈ s → ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
⊢ t ⊆ ⋃ i, t ∩ w i

Tactic:
intro x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
x : α
⊢ x ∈ t → x ∈ ⋃ i, t ∩ w i
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case e_f
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ (fun n ↦ μ (toMeasurable μ (t ∩ disjointed w n) ∩ u)) = fun n ↦ μ (t ∩ disjointed w n ∩ u)

Tactic:
ext1 n

Goal state after:
case e_f
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ μ (toMeasurable μ (t ∩ disjointed w n) ∩ u) = μ (t ∩ disjointed w n ∩ u)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case e_f
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ (fun n ↦ μ (t ∩ disjointed w n ∩ u)) = fun n ↦ (μ.restrict (t ∩ u)) (disjointed w n)

Tactic:
ext1 n

Goal state after:
case e_f
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ μ (t ∩ disjointed w n ∩ u) = (μ.restrict (t ∩ u)) (disjointed w n)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case refine_2
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ (s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ).Subsingleton

Tactic:
intro x

Goal state after:
case refine_2
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x : α
⊢ x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ →
    ∀ ⦃y : α⦄, y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ → x = y
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ t ∈ ae (μ.restrict s) ↔ t ∈ ae μ ⊓ 𝓟 s

Tactic:
simp only [mem_inf_principal, mem_ae_iff, restrict_apply_eq_zero' hs, compl_ofPred,
    Classical.not_imp, fun a => and_comm (a := a ∈ s) (b := a ∉ t)]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ (tᶜ ∩ s) = 0 ↔ μ {a | a ∉ t ∧ a ∈ s} = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ s ⊆ ⋃ y ∈ s, measurableAtom y

Tactic:
intro x

Goal state after:
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
x : α
⊢ x ∈ s → x ∈ ⋃ y ∈ s, measurableAtom y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ ∀ i ∈ s, measurableAtom i ⊆ s

Tactic:
intro x

Goal state after:
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
x : α
⊢ x ∈ s → measurableAtom x ⊆ s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case iUnion
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
f : ℕ → Set ↑s
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n) μ
⊢ NullMeasurableSet (Subtype.val '' ⋃ i, f i) μ

Tactic:
rw [image_iUnion]

Goal state after:
case iUnion
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
f : ℕ → Set ↑s
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n) μ
⊢ NullMeasurableSet (⋃ i, Subtype.val '' f i) μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
⊢ SigmaFinite μ

Tactic:
cases isEmpty_or_nonempty α
    · rw [Subsingleton.elim μ 0]
      infer_instance
    · obtain ⟨f, hf⟩ := exists_surjective_nat α
      exact ⟨⟨⟨fun n ↦ {f n}, by simp, by simpa [hf.forall] using hμ, by simp [hf.range_eq]⟩⟩⟩

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
⊢ ∀ (x y : α), (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
intro x

Goal state after:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x : α
⊢ ∀ (y : α), (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t' n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

Tactic:
· simp only [iInf_image, coe_toOuterMeasure, iInf_pair]
      rw [tsum_eq_add_tsum_ite 0, tsum_eq_add_tsum_ite 1, if_neg zero_ne_one.symm,
        ENNReal.summable.tsum_eq_zero_iff.2 _, add_zero]
      · exact add_le_add (inf_le_left.trans <| by simp [ht']) (inf_le_right.trans <| by simp [ht'])
      · simp only [ite_eq_left_iff]
        intro n hn₁ hn₀
        simp only [ht', if_neg hn₀, if_neg hn₁, measure_empty, le_refl, inf_of_le_left]

Goal state after: