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

Goal state before:
pp: case coe
a : ℝ
h : ↑a ≤ 0
⊢ (↑a)⁻¹ ≤ 0

Tactic:
| coe a =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
h : HasOpenCGraph f
⊢ HasOpenLowerSections f

Tactic:
intro x b hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
h : HasOpenCGraph f
x : α
b : β
hb : b ∈ f x
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x b ↦ b ∈ f x) x' b
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c d : EReal
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
by
  rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]

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

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun x ↦ c * u x) f = c * limsup u f

Tactic:
simp_rw [EReal.mul_comm (x := c)]

Goal state after:
case inr
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun x ↦ u x * c) f = limsup u f * c
Module: Mathlib.Topology.Instances.EReal.Lemmas

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

Tactic:
refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds
    (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_

Goal state after:
r : ℝ
x✝ : EReal × EReal
h : ↑0 < x✝.1 ∧ ↑r < x✝.2
⊢ ↑r < x✝.1 + x✝.2
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
this : (fun s ↦ ⨆ (_ : s.Nonempty), m s) = m
⊢ (boundedBy m) s = (OuterMeasure.ofFunction m m_empty) s

Tactic:
simp [boundedBy, this]

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

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
⊢ ⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t

Tactic:
rcases t.eq_empty_or_nonempty with (rfl | ht)
  · simp [biInf_const h]
  · simp [ht, sInfGen_def]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
simp only [one_mul, Nat.cast_add, zero_add, Nat.cast_one]

Goal state after:
k : ℕ
hn : 0 < k.succ
⊢ (∏ x ∈ Finset.range k, (↑x + 1 + 1) * (↑k + 1)⁻¹) * (↑k + 1)⁻¹ ≤ (↑k + 1)⁻¹
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : (s ∩ t).Nonempty
⊢ s ∩ t ∈ {S}

Tactic:
rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self,
    Set.mem_singleton_iff]

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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
⊢ f ⁻¹' v ∈ 𝓝[s] x

pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
· rcases exists_Ioc_subset_of_mem_nhds hv Hl with ⟨l, lfx, hl⟩
    by_cases! Hu : ∃ u, f x < u
    · rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
      filter_upwards [h₁ l lfx, h₂ u fxu] with a lfa fau
      rcases le_or_gt (f a) (f x) with h | h
      · exact hl ⟨lfa, h⟩
      · exact hu ⟨le_of_lt h, fau⟩
    · filter_upwards [h₁ l lfx] with a lfa using hl ⟨lfa, Hu (f a)⟩

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
⊢ f ⁻¹' v ∈ 𝓝[s] x
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s

Tactic:
simp only [ContinuousOn, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
  exact
    ⟨fun H => ⟨fun x hx => (H x hx).1, fun x hx => (H x hx).2⟩, fun H x hx => ⟨H.1 x hx, H.2 x hx⟩⟩

Goal state after:
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
h : ∀ (s : Set α), μ sᶜ = 0 ↔ s = univ
a : α
ha : μ {a} = 0
⊢ False

Tactic:
simpa [ha] using (h {a}ᶜ).1

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
s₁ : Set α → Prop
has_empty✝¹ : s₁ ∅
has_compl✝¹ : ∀ {a : Set α}, s₁ a → s₁ aᶜ
has_iUnion_nat✝¹ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₁ (f i)) → s₁ (⋃ i, f i)
s₂ : Set α → Prop
has_empty✝ : s₂ ∅
has_compl✝ : ∀ {a : Set α}, s₂ a → s₂ aᶜ
has_iUnion_nat✝ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₂ (f i)) → s₂ (⋃ i, f i)
h :
  ∀ (s : Set α),
    { Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ }.Has s ↔
      { Has := s₂, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ }.Has s
⊢ { Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ } =
    { Has := s₂, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ }

Tactic:
by
    have : s₁ = s₂ := funext fun x => propext <| h x
    subst this
    rfl

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
⊢ d.Has (⋃ i, f i ∩ s)

Tactic:
refine d.has_iUnion_nat ?_ hf

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
⊢ Pairwise (Disjoint on fun i ↦ f i ∩ s)
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ (s ∩ t) + (μ t + μ (s \ t)) = μ (s ∩ t) + μ (s \ t) + μ t

Tactic:
← add_assoc,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ (s ∩ t) + μ t + μ (s \ t) = μ (s ∩ t) + μ (s \ t) + μ t
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
s : Set β
⊢ μ (⇑f ⁻¹' s)ᶜ = 0 ↔ (map (⇑f) μ) sᶜ = 0

Tactic:
← preimage_compl,

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
s : Set β
⊢ μ (⇑f ⁻¹' sᶜ) = 0 ↔ (map (⇑f) μ) sᶜ = 0
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : (comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ μ (f '' (s \ t ∪ t \ s)) = 0

Tactic:
rw [h_eq_α] at hst

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : (comap f μ) (s \ t ∪ t \ s) = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ μ (f '' (s \ t ∪ t \ s)) = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : NullMeasurableSet s μ
h₂ : μ t = μ s
ht : μ s ≠ ∞
⊢ μ s - μ s = 0

Tactic:
tsub_self

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : NullMeasurableSet s μ
h₂ : μ t = μ s
ht : μ s ≠ ∞
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict s) t = μ (t ∩ s)

Tactic:
by
  rw [← toOuterMeasure_apply,
    Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,
    OuterMeasure.restrict_apply s t _, toOuterMeasure_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝ : SigmaFinite μ
⊢ SFinite μ

Tactic:
by
  have : ∀ n, Fact (μ (disjointed (spanningSets μ) n) < ∞) :=
    fun n ↦ ⟨(measure_mono (disjointed_subset _ _)).trans_lt (measure_spanningSets_lt_top μ n)⟩
  exact ⟨⟨fun n ↦ μ.restrict (disjointed (spanningSets μ) n), fun n ↦ by infer_instance,
    (sum_restrict_disjointed_spanningSets μ μ).symm⟩⟩

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∩ t) + (μ.restrict t + μ.restrict (s \ t)) = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t

Tactic:
← add_assoc,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∩ t) + μ.restrict t + μ.restrict (s \ t) = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
⊢ ((μ + ν).trim hm) s = (μ.trim hm + ν.trim hm) s

Tactic:
by simp [trim_measurableSet_eq hm hs]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : ν (t ∩ s) = 0
⊢ μ (t ∩ s) = 0

Tactic:
exact h htν

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

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ memPartitionSet f (n + 1) a ∈ memPartition f (n + 1)

Tactic:
memPartitionSet_succ,

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) ∈ memPartition f (n + 1)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ x ∈ countablyGeneratedAtom α fun x_1 ↦ x ∈ natGeneratingSequence α x_1

Tactic:
simp [countablyGeneratedAtom]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ ∀ (i : ℕ), x ∈ if x ∈ natGeneratingSequence α i then natGeneratingSequence α i else (natGeneratingSequence α i)ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
hx : x ∈ natGeneratingSequence α n
⊢ (fun x_1 ↦ x ∈ natGeneratingSequence α x_1) n ∧ x ∈ countablyGeneratedAtom α fun x_1 ↦ x ∈ natGeneratingSequence α x_1

Tactic:
simp [countablyGeneratedAtom]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
hx : x ∈ natGeneratingSequence α n
⊢ x ∈ natGeneratingSequence α n ∧
    ∀ (i : ℕ), x ∈ if x ∈ natGeneratingSequence α i then natGeneratingSequence α i else (natGeneratingSequence α i)ᶜ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), MeasurableSet (s i)
⊢ μ univ < ∞

Tactic:
MeasurableSpace.measurableSet_bot_iff

Goal state after:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
⊢ μ univ < ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
⊢ s.indicator f x = f x

Tactic:
by_cases hxs : x ∈ s

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
hxs : x ∈ s
⊢ s.indicator f x = f x

case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
hxs : x ∉ s
⊢ s.indicator f x = f x
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
⊢ s.indicator f x = 0 x

Tactic:
by_cases hxs : x ∈ s

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
hxs : x ∈ s
⊢ s.indicator f x = 0 x

case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
hxs : x ∉ s
⊢ s.indicator f x = 0 x
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
⊢ s.indicator f x = s.indicator g x

Tactic:
by_cases hxs : x ∈ s

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : x ∈ s
⊢ s.indicator f x = s.indicator g x

case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : x ∉ s
⊢ s.indicator f x = s.indicator g x
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
s : Set α
hxs : x ∈ s
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
⊢ (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1) ⊆ s

Tactic:
suffices q (x ∈ A ·) by
    rw [hq]
    refine subset_trans (le_of_eq ?_) (subset_iUnion _ (x ∈ A ·))
    simp [this]

Goal state after:
case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
s : Set α
hxs : x ∈ s
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
⊢ q fun x_1 ↦ x ∈ A x_1
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
s : (y : α) → x ≠ y → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
y : α
h : x ≠ y
⊢ y ∈ {x} ↔ y ∈ ⋂ b, ⋂ (b_1 : x ≠ b), s b b_1

Tactic:
· simp only [mem_singleton_iff, h.symm, false_iff, mem_iInter, not_forall]
      exact ⟨y, h, hys y h⟩

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ✝ ν μ : Measure α
f : α → β
inst✝ : SFinite μ
H : ¬AEMeasurable f μ
⊢ SFinite (map f μ)

Tactic:
· rw [map_of_not_aemeasurable H]
    infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁵ : MeasurableSpace M✝
inst✝⁴ : MeasurableSMul M✝ X
M : Type u_6
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
n : ℤ
⊢ Measurable fun x ↦ (x, n).2 • (x, n).1

Tactic:
cases n with

Goal state after:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ cthickening δ E

Tactic:
rw [← cthickening_of_nonpos (min_le_right δ 0)]
  exact cthickening_mono (min_le_left δ 0) E

Goal state after:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal (↑r / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal (↑r / 2)
⊢ z ∈ ⊥

Tactic:
rw [← NNReal.coe_two, ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal] at hzs hzt

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ↑(r / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ↑(r / 2)
⊢ z ∈ ⊥
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)

Tactic:
by
  obtain ⟨r, hr, h⟩ := exists_pos_forall_lt_edist hs ht hst
  refine ⟨r / 2, half_pos (NNReal.coe_pos.2 hr), ?_⟩
  rw [disjoint_iff_inf_le]
  rintro z ⟨hzs, hzt⟩
  rw [mem_thickening_iff_exists_edist_lt] at hzs hzt
  rw [← NNReal.coe_two, ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal] at hzs hzt
  obtain ⟨x, hx, hzx⟩ := hzs
  obtain ⟨y, hy, hzy⟩ := hzt
  refine (h x hx y hy).not_ge ?_
  calc
    edist x y ≤ edist z x + edist z y := edist_triangle_left _ _ _
    _ ≤ ↑(r / 2) + ↑(r / 2) := add_le_add hzx.le hzy.le
    _ = r := by rw [← ENNReal.coe_add, add_halves]

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

Goal state before:
pp: β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), MeasurableSet (⇑f ⁻¹' {x})
⊢ ∃ c, ∀ (x : α), f x = c

Tactic:
MeasurableSpace.measurableSet_bot_iff

Goal state after:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ⇑f ⁻¹' {x} = ∅ ∨ ⇑f ⁻¹' {x} = univ
⊢ ∃ c, ∀ (x : α), f x = c
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
this : Measurable fun _b ↦ sSup ∅
⊢ EqOn (fun b ↦ ⨆ i, f i b) (fun _b ↦ sSup ∅) {b | BddAbove (range fun i ↦ f i b)}ᶜ

Tactic:
· intro b hb
    apply csSup_of_not_bddAbove
    simpa

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : PseudoMetricSpace β
inst✝ : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : ℕ → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
x : α
hx : ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
⊢ Tendsto (fun b ↦ dist (f b x) (g x)) atTop (𝓝 0)

Tactic:
exact squeeze_zero (fun n => dist_nonneg) hx u_lim

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

Goal state before:
pp: μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NullSingletonClass μ
b : ℝ
⊢ Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝 0) (𝓝 0)

Tactic:
rw [← nhdsLT_sup_nhdsGE, tendsto_sup]

Goal state after:
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NullSingletonClass μ
b : ℝ
⊢ Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0) ∧ Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun n ↦ (approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f x))

Tactic:
have : Nonempty s := ⟨⟨y₀, h₀⟩⟩
  rw [← @Subtype.range_coe _ s, ← image_univ, ← (denseRange_denseSeq s).closure_eq] at hx
  simp -iota only [approxOn, coe_comp]
  refine tendsto_nearestPt (closure_minimal ?_ isClosed_closure hx)
  simp -iota only [Nat.range_casesOn, closure_union, range_comp]
  exact
    Subset.trans (image_closure_subset_closure_image continuous_subtype_val)
      subset_union_right

Goal state after: