mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
rcases eq_top_or_lt_top a with rfl | a_top
  · rw [ne_self_iff_false, false_or] at h₂; rw [top_mul_of_pos h₂] at hc; exact (not_top_lt hc).rec
  rcases le_or_gt b 0 with b0 | b0
  · obtain ⟨a', aa', a_top'⟩ := exists_between a_top
    exact ⟨a', mem_Ioo.2 ⟨aa', a_top'⟩, lt_of_le_of_lt (mul_le_mul_of_nonpos_right aa'.le b0) hc⟩
  rcases eq_top_or_lt_top b with rfl | b_top
  · rcases lt_trichotomy a 0 with a0 | rfl | a0
    · obtain ⟨a', aa', a0'⟩ := exists_between a0
      rw [mul_top_of_neg a0] at hc
      refine ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt a0'⟩, mul_top_of_neg a0' ▸ hc⟩
    · rw [ne_self_iff_false, ne_self_iff_false, false_or] at h₁; exact h₁.rec
    · rw [mul_top_of_pos a0] at hc; exact (not_top_lt hc).rec
  · obtain ⟨a', aa', hc'⟩ := exists_between ((lt_div_iff b0 b_top.ne).2 hc)
    exact ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt hc'⟩, (lt_div_iff b0 b_top.ne).1 hc'⟩

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) ↔
    IsOpen[instTopologicalSpaceProd] {p | p.1 ∈ s ∧ f p.1 ≤ p.2}ᶜ

Tactic:
compl_ofPred,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) ↔
    IsOpen[instTopologicalSpaceProd] {a | ¬(a.1 ∈ s ∧ f a.1 ≤ a.2)}
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : (fun n ↦ C / ↑n) = fun n ↦ ↑(C.toReal / ↑n)
⊢ Tendsto (fun n ↦ C.toReal / ↑n) atTop (𝓝 0)

Tactic:
exact _root_.tendsto_const_div_atTop_nhds_zero_nat C.toReal

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y

pp: case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∀ (l : γ), f x ≤ l
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y

Tactic:
· obtain ⟨z, zlt, hz⟩ : ∃ z < f x, Ioc z (f x) ⊆ g ⁻¹' Ioi y :=
      exists_Ioc_subset_of_mem_nhds (hg (Ioi_mem_nhds hy)) h
    filter_upwards [hf z zlt] with a ha
    calc
      y < g (min (f x) (f a)) := hz (by simp [zlt, ha])
      _ ≤ g (f a) := gmon (min_le_right _ _)

Goal state after:
case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∀ (l : γ), f x ≤ l
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ioo 0 (limsup u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
x✝ : a < u x ∧ b < v x ∧ 0 x ≤ v x
xa : a < u x
xb : b < v x
vx : 0 x ≤ v x
⊢ c < (u * v) x

Tactic:
exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ioo 0 (liminf u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
xa : a < u x
xb : b < v x
⊢ c < u x * v x

Tactic:
exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
s : Set β
⊢ ((map f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f ⁻¹' s)

Tactic:
rw [map_apply]
    apply ofFunction_le

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

Goal state before:
pp: a b : EReal
h : ContinuousAt (fun p ↦ p.1 * p.2) (a, b)
this : (fun p ↦ p.1 * p.2) = (fun x ↦ -x) ∘ (fun p ↦ p.1 * p.2) ∘ fun p ↦ (-p.1, p.2)
⊢ ContinuousAt ((fun x ↦ -x) ∘ (fun p ↦ p.1 * p.2) ∘ fun p ↦ (-p.1, p.2)) (-a, b)

Tactic:
apply ContinuousAt.comp (Continuous.continuousAt continuous_neg)
    <| ContinuousAt.comp _ (ContinuousAt.prodMap (Continuous.continuousAt continuous_neg)
      (Continuous.continuousAt continuous_id))

Goal state after:
a b : EReal
h : ContinuousAt (fun p ↦ p.1 * p.2) (a, b)
this : (fun p ↦ p.1 * p.2) = (fun x ↦ -x) ∘ (fun p ↦ p.1 * p.2) ∘ fun p ↦ (-p.1, p.2)
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (Prod.map (fun a ↦ -a) id (-a, b))
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
H : Monotone fun s ↦ m ↑s
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
ht : t.Nonempty
⊢ m s ≤ (fun s ↦ ⨆ (_ : s.Nonempty), m s) t

Tactic:
exact (@H ⟨s, hs⟩ ⟨t, ht⟩ hst).trans (le_iSup (fun _ : t.Nonempty => m t) ht)

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
b : Finset ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ∑ i ∈ b, f i x') s x

Tactic:
exact lowerSemicontinuousWithinAt_sum fun i _hi => h i

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
n : ℕ
⊢ ∃ m, s m ⊆ dissipate s n

Tactic:
induction n with
  | zero => use 0; simp [dissipate_def]
  | succ n hn =>
    obtain ⟨m, hm⟩ := hn
    obtain ⟨k, hk⟩ := hd m (n + 1)
    exact ⟨k, by simp; grind⟩

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S

pp: case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
· simp [hs]

Goal state after:
case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A : Set α
⊢ ⨅ t, ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht = ⨅ t, ⨅ (ht : P t), ⨅ (_ : ⇑f ⁻¹' A ⊆ t), m t ht

Tactic:
refine f.injective.preimage_surjective.iInf_congr (preimage f) fun s => ?_

Goal state after:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A s : Set α
⊢ ⨅ (ht : P (⇑f ⁻¹' s)), ⨅ (_ : ⇑f ⁻¹' A ⊆ ⇑f ⁻¹' s), m (⇑f ⁻¹' s) ht = ⨅ (ht : P s), ⨅ (_ : A ⊆ s), m s ht
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
⊢ μ hs.choose = μ s

Tactic:
exact measure_congr hs.choose_spec.2.2

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ ofMeasurableSpace ((generate s).toMeasurableSpace ⋯) ≤ ofMeasurableSpace (generateFrom s)

Tactic:
rw [ofMeasurableSpace_toMeasurableSpace]

Goal state after:
α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ generate s ≤ ofMeasurableSpace (generateFrom s)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ∞

Tactic:
simp only [iInf_eq_top, ms] at hs

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ∀ (i : Set α), s ⊆ i → MeasurableSet i → m i = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ∞
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
⊢ ((restrict s) μ).trim = (restrict s) μ.trim

Tactic:
by
  refine le_antisymm (fun t => ?_) (le_trim_iff.2 fun t ht => ?_)
  · rw [restrict_apply]
    rcases μ.exists_measurable_superset_eq_trim (t ∩ s) with ⟨t', htt', ht', hμt'⟩
    rw [← hμt']
    rw [inter_subset] at htt'
    refine (measure_mono htt').trans ?_
    rw [trim_eq _ (hs.compl.union ht'), restrict_apply, union_inter_distrib_right, compl_inter_self,
      Set.empty_union]
    exact measure_mono inter_subset_left
  · rw [restrict_apply, trim_eq _ (ht.inter hs), restrict_apply]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : ¬AEMeasurable f μ
hg : ¬AEMeasurable g μ
⊢ map f μ = map g μ

Tactic:
simp [map_of_not_aemeasurable, hf, hg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
⊢ f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) = toMeasurable μ (f ⁻¹' s)

Tactic:
hf.injective.preimage_image

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
⊢ toMeasurable μ (f ⁻¹' s) = toMeasurable μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
s : Set α
hs : ν s = 0
t : Set α
h1t : s ⊆ t
h2t : MeasurableSet t
h3t : ν t = 0
⊢ μ s = 0

Tactic:
exact measure_mono_null h1t (h h2t h3t)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
μ : Measure α
hs : Fact (μ s < ∞)
⊢ (μ.restrict s) univ < ∞

Tactic:
by simpa using hs.elim

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : μ (⋃ i, As i) ≠ ∞
posmeas : Set ι := {i | 0 < μ (As i)}
posmeas_def : posmeas = {i | 0 < μ (As i)}
as : ℕ → ℝ≥0∞
left✝ : StrictAnti as
as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : ℕ → Set ι := fun n ↦ {i | as n ≤ μ (As i)}
countable_union : posmeas = ⋃ n, fairmeas n
⊢ posmeas.Countable

Tactic:
countable_union

Goal state after:
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : μ (⋃ i, As i) ≠ ∞
posmeas : Set ι := {i | 0 < μ (As i)}
posmeas_def : posmeas = {i | 0 < μ (As i)}
as : ℕ → ℝ≥0∞
left✝ : StrictAnti as
as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : ℕ → Set ι := fun n ↦ {i | as n ≤ μ (As i)}
countable_union : posmeas = ⋃ n, fairmeas n
⊢ (⋃ n, fairmeas n).Countable
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case hs
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ Antitone fun i ↦ ⋂ j, ⋂ (_ : j ≤ i), f j

Tactic:
exact fun i j h ↦ biInter_mono (Iic_subset_Iic.2 h) fun _ _ ↦ Set.Subset.rfl

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
this : x ∈ ⋃₀ memPartition f n
⊢ x ∈ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} ↔ x ∈ univ

Tactic:
simp only [mem_sUnion, mem_univ,
      iff_true] at this ⊢

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
this : ∃ t ∈ memPartition f n, x ∈ t
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
a : α
⊢ memPartitionSet f 0 a = univ

Tactic:
by
  simp [memPartitionSet]

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
inst✝ : Decidable (a ∈ f n)
⊢ memPartitionSet f (n + 1) a = if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

Tactic:
by
  simp [memPartitionSet]

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

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ generateFrom (countableGeneratingSet α) = m

Tactic:
generateFrom_countableGeneratingSet

Goal state after:
α : Type u_3
m : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ m = m
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
⊢ CountablyGenerated α

Tactic:
comap_generateFrom

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
⊢ CountablyGenerated α
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
⊢ (Measure.comap f μ) s = (Measure.comap f μ) (f ⁻¹' f '' s)

Tactic:
hf.injective.preimage_image

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
⊢ (Measure.comap f μ) s = (Measure.comap f μ) s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
inst✝ : MeasureSpace α
s : Set α
hs : MeasurableSet s
⊢ Measure.map Subtype.val (Measure.comap Subtype.val volume) = volume.restrict s

Tactic:
(MeasurableEmbedding.subtype_coe hs).map_comap volume,

Goal state after:
α : Type u_2
inst✝ : MeasureSpace α
s : Set α
hs : MeasurableSet s
⊢ volume.restrict (range Subtype.val) = volume.restrict s
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ ∀ (a : ℕ), Measurable fun x ↦ mapNatBool α x a

Tactic:
refine fun n ↦ measurable_to_bool ?_

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
n : ℕ
⊢ MeasurableSet ((fun x ↦ mapNatBool α x n) ⁻¹' {true})
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.iUnion
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ⋃ i, f i = ⋃₀ ↑S

Tactic:
have : Fintype (⋃ n, (S n : Set (Set α))) := by
        refine (Finite.subset (finite_memPartition t n) ?_).fintype
        simp only [iUnion_subset_iff]
        exact hS_subset

Goal state after:
case refine_1.iUnion
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ⋃ i, f i = ⋃₀ ↑S
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝¹ : Preorder β
inst✝ : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
⊢ ∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᵐ[μ] g

Tactic:
obtain ⟨G, hG_meas, hG_mem, hG_ae_eq⟩ := hf.exists_ae_eq_range_subset f_nn ⟨0, le_rfl⟩

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝¹ : Preorder β
inst✝ : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
G : α → β
hG_meas : Measurable G
hG_mem : range G ⊆ inst✝¹.toLE.1 0
hG_ae_eq : f =ᵐ[μ] G
⊢ ∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᵐ[μ] g
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case inl
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
n : ℕ
h : x < u n
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))

pp: case inr
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))

Tactic:
· exact g_meas (u n) h

Goal state after:
case inr
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
choose! T hTf hTm hTeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_subset_ae_eq

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
⊢ AEMeasurable f μ
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
n : ?m.90
⊢ ?m.93 n

Tactic:
by
    apply normal_exists_closure_subset t_cl (T_open (g n).1 (g n).2)
    rw [T_int]
    exact sInter_subset_of_mem (g n).2

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : u ∈ s
⊢ TopologicalSpace.IsOpen u

Tactic:
rw [hs]

Goal state after:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : u ∈ s
⊢ TopologicalSpace.IsOpen u
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
α : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
inst✝ : SecondCountableTopology α
⊢ CountablyGenerated α

Tactic:
obtain ⟨b, bct, -, hb⟩ := exists_countable_basis α

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
α : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
bct : b.Countable
hb : IsTopologicalBasis b
⊢ CountablyGenerated α
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod
hl : Measurable f ∧ ∀ x ∈ l, Measurable x
⊢ Measurable (f :: l).prod

Tactic:
List.prod_cons

Goal state after:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod
hl : Measurable f ∧ ∀ x ∈ l, Measurable x
⊢ Measurable (f * l.prod)
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ
hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
⊢ AEMeasurable (f :: l).prod μ

Tactic:
List.prod_cons

Goal state after:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ
hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
⊢ AEMeasurable (f * l.prod) μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
⊢ Measurable f

Tactic:
apply measurable_of_isClosed

Goal state after:
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
⊢ ∀ (s : Set γ), IsClosed[inst✝³] s → MeasurableSet (f ⁻¹' s)