mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ (𝓝 ⊥).HasBasis (fun x ↦ True) fun x ↦ Iio ↑x

Tactic:
refine (_root_.nhds_bot_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩
  rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩
  exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩

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

Goal state before:
pp: case h
x : EReal
hx : ⊥ < x
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

Tactic:
by_cases hx_top : x = ⊤

Goal state after:
case pos
x : EReal
hx : ⊥ < x
hx_top : x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

case neg
x : EReal
hx : ⊥ < x
hx_top : ¬x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case neg
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ¬∀ (i : ℕ), P (t i)
⊢ ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) ≤ ∑' (n : ℕ), m (t n)

Tactic:
simp only [ht, not_false_eq_true, iInf_neg, top_le_iff]
      push Not at ht
      obtain ⟨i, hti_notMem⟩ := ht
      have hfi_top : m (t i) = ∞ := m_top _ hti_notMem
      exact ENNReal.tsum_eq_top_of_eq_top ⟨i, hfi_top⟩

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

Goal state before:
pp: ⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
simp only [ContinuousAt, EReal.top_mul_top, EReal.tendsto_nhds_top_iff_real]
  intro x
  rw [_root_.eventually_nhds_iff]
  use (Set.Ioi ((max x 0) : EReal)) ×ˢ (Set.Ioi 1)
  split_ands
  · intro p p_in_prod
    simp only [Set.mem_prod, Set.mem_Ioi, max_lt_iff] at p_in_prod
    rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩
    have := mul_le_mul_of_nonneg_left (le_of_lt p2_gt_1) (le_of_lt p1_pos)
    rw [mul_one p.1] at this
    exact lt_of_lt_of_le p1_gt_x this
  · exact IsOpen.prod isOpen_Ioi isOpen_Ioi
  · simp
  · rw [Set.mem_Ioi, ← EReal.coe_one]; exact EReal.coe_lt_top 1

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

Goal state before:
pp: α : Type u_1
⊢ boundedBy 0 = 0

Tactic:
rw [← coe_bot, eq_bot_iff]
  apply boundedBy_le

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
n : ℕ
x : α
⊢ x ∈ dissipate s (n + 1) ↔ x ∈ dissipate s n ∩ s (n + 1)

Tactic:
simp_all only [dissipate_def, mem_iInter, mem_inter_iff]

Goal state after:
α : Type u_1
s : ℕ → Set α
n : ℕ
x : α
⊢ (∀ i ≤ n + 1, x ∈ s i) ↔ (∀ i ≤ n, x ∈ s i) ∧ x ∈ s (n + 1)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_4
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorSemiring α
x : ℕ
⊢ x ≤ ⌊max 0 (↑x + 1)⌋₊

Tactic:
simp [Nat.le_floor_iff]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
t1 t2 : Set α
h : (t1 ∩ t2).Nonempty
n : ι
ht1 : t1 ∈ p n
m : ι
ht2 : t2 ∈ p m
⊢ ∃ i, t1 ∩ t2 ∈ p i

Tactic:
obtain ⟨k, hpnk, hpmk⟩ : ∃ k, p n ≤ p k ∧ p m ≤ p k := hp_directed n m

Goal state after:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
t1 t2 : Set α
h : (t1 ∩ t2).Nonempty
n : ι
ht1 : t1 ∈ p n
m : ι
ht2 : t2 ∈ p m
k : ι
hpnk : p n ⊆ p k
hpmk : p m ⊆ p k
⊢ ∃ i, t1 ∩ t2 ∈ p i
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₂ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊤
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)

Tactic:
simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₂

Goal state after:
case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
h₂ : ¬a✝ = 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ generateFrom (piiUnionInter (fun k ↦ {s k}) S) = generateFrom {t | ∃ k ∈ S, s k = t}

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_mono ?_)

Goal state after:
case refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ ∀ t ∈ piiUnionInter (fun k ↦ {s k}) S, MeasurableSet t

case refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ {t | ∃ k ∈ S, s k = t} ⊆ piiUnionInter (fun k ↦ {s k}) 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 s : Set α
hs : P s
⊢ ⨅ (_ : ⇑f ⁻¹' A ⊆ ⇑f ⁻¹' s), m (⇑f ⁻¹' s) ⋯ = ⨅ (_ : A ⊆ s), m s hs

Tactic:
refine iInf_congr_Prop f.surjective.preimage_subset_preimage_iff ?_

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 α
hs : P s
⊢ A ⊆ s → m (⇑f ⁻¹' s) ⋯ = m s hs
Module: Mathlib.MeasureTheory.PiSystem

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

Tactic:
have h_ss : {i} ⊆ S := by
    intro j hj
    rw [mem_singleton_iff] at hj
    rwa [hj]
  refine Subset.trans ?_ (piiUnionInter_mono_right h_ss)
  rw [piiUnionInter_singleton]
  exact subset_union_left

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) ≤ ⨆ i ∈ S, m i

Tactic:
← @generateFrom_measurableSet α (⨆ i ∈ S, m i)

Goal state after:
case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) ≤ generateFrom {s | MeasurableSet s}
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
n : ℕ
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (↑n)⁻¹

Tactic:
refine this _ (ENNReal.lt_add_right hs ?_)

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
n : ℕ
⊢ (↑n)⁻¹ ≠ 0
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this✝ : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
this : ∀ (n : ℕ), ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (↑n)⁻¹
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Tactic:
choose t hsub hm hm' using this

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), m (t n) < ms + (↑n)⁻¹
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
⊢ (⨆ i, μ i).trim = ⨆ i, (μ i).trim

Tactic:
simp_rw [← @iSup_plift_down _ ι]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
⊢ (⨆ i, μ i.down).trim = ⨆ i, (μ i.down).trim
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
m : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hg : Measurable g
hf : NullMeasurable f μ
⊢ EventuallyMeasurable m (ae μ) (g ∘ f)

Tactic:
exact hg.comp_eventuallyMeasurable hf

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
⊢ comap f (c • μ) = c • comap f μ

Tactic:
· have h' : ¬ (Function.Injective f ∧
        ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)) := by
      simpa [nullMeasurableSet_smul_measure_iff hc] using h
    simp [comap_undef, h, h']

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
hb : IsSuccPrelimit b
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f (𝓝[<] b) l

Tactic:
← map_coe_Ioo_atTop h hb,

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
hb : IsSuccPrelimit b
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f (map Subtype.val atTop) l
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
x : α
n : ℕ
⊢ spanningSetsIndex μ x = n ↔ x ∈ disjointed (spanningSets μ) n

Tactic:
by
  convert! Set.ext_iff.1 (preimage_spanningSetsIndex_singleton μ n) x

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
⊢ μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i)

Tactic:
ext1 t ht

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t = (ν.restrict (⋃ i, s i)) t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
U : ι → Set α
hU : ⋃ i, U i = univ
H : ∀ (i : ι), μ (U i) ≤ 0
⊢ μ = 0

Tactic:
rw [← measure_univ_eq_zero, ← hU]

Goal state after:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
U : ι → Set α
hU : ⋃ i, U i = univ
H : ∀ (i : ι), μ (U i) ≤ 0
⊢ μ (⋃ i, U i) = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
← restrict_biUnion_congr hc,

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : ⋃ i ∈ S, s i = univ
⊢ μ = ν ↔ μ.restrict (⋃ i ∈ S, s i) = ν.restrict (⋃ i ∈ S, s i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
w : ℕ → Set α := fun n ↦ toMeasurable (m n) t
T : t ⊆ ⋂ n, w n
M : MeasurableSet (⋂ n, w n)
u : Set α
hu : MeasurableSet u
⊢ μ ((⋂ n, w n) ∩ u) = μ (t ∩ u)

Tactic:
refine le_antisymm ?_ (by gcongr)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
w : ℕ → Set α := fun n ↦ toMeasurable (m n) t
T : t ⊆ ⋂ n, w n
M : MeasurableSet (⋂ n, w n)
u : Set α
hu : MeasurableSet u
⊢ μ ((⋂ n, w n) ∩ u) ≤ μ (t ∩ u)
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
h_univ : (μ.trim ⋯) Set.univ < ∞
⊢ μ Set.univ < ∞

pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : μ Set.univ < ∞
⊢ (μ.trim ⋯) Set.univ < ∞

Tactic:
· rwa [trim_measurableSet_eq bot_le MeasurableSet.univ] at h_univ

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : μ Set.univ < ∞
⊢ (μ.trim ⋯) Set.univ < ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b

Tactic:
by
    refine ⟨⋃ y, {measurableAtom y}, countable_iUnion (fun i ↦ countable_singleton _), ?_⟩
    refine le_antisymm ?_ (generateFrom_le (by simp [MeasurableSet.measurableAtom_of_countable]))
    intro s hs
    have : s = ⋃ y ∈ s, measurableAtom y := by
      apply Subset.antisymm
      · intro x hx
        simpa using ⟨x, hx, by simp⟩
      · simp only [iUnion_subset_iff]
        intro x hx
        exact measurableAtom_subset hs hx
    rw [this]
    apply MeasurableSet.biUnion (to_countable s) (fun x _hx ↦ ?_)
    apply measurableSet_generateFrom
    simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
⊢ Measure.map f (Measure.comap f μ) = μ.restrict (range f)

Tactic:
ext1 t ht

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

Goal state before:
pp: case refine_1
α : 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
⊢ s.indicator f =ᵐ[μ] s.indicator g

Tactic:
filter_upwards [h] with x hx

Goal state after:
α : 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
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
filter_upwards [h] with x hx

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : s.indicator f =ᵐ[μ] s.indicator g
x : α
hx : s.indicator f x = s.indicator g x
⊢ x ∈ s → f x = g x
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ν s < ∞ → ∀ᵐ (x : α) ∂μ.restrict s, P x
⊢ ∀ᵐ (x : α) ∂μ, P x

Tactic:
by
  have : ∀ n, ∀ᵐ x ∂μ, x ∈ spanningSets (μ + ν) n → P x := by
    intro n
    have := h
      (spanningSets (μ + ν) n) (measurableSet_spanningSets _ _)
      ((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
      ((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
    exact (ae_restrict_iff' (measurableSet_spanningSets _ _)).mp this
  filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
⊢ AEMeasurable f (sum μ)

Tactic:
nontriviality β

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
⊢ AEMeasurable f (sum μ)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
s : Set γ
hs : MeasurableSet s
⊢ (Measure.map g (Measure.map f μ)) s = (Measure.map (g ∘ f) μ) s

Tactic:
rw [map_apply_of_aemeasurable hg hs, map_apply₀ hf (hg.nullMeasurable hs),
    map_apply_of_aemeasurable (hg.comp_aemeasurable hf) hs, preimage_comp]

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

Goal state before:
pp: α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ μ.restrict (AEMeasurable.mk f hf ⁻¹' s) = μ.restrict (f ⁻¹' s)

Tactic:
ext1 t ht

Goal state after:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (AEMeasurable.mk f hf ⁻¹' s)) t = (μ.restrict (f ⁻¹' s)) t
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
nontriviality β

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
a✝ : Nontrivial β
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
⊢ ((sum fun i ↦ μ ↑i) + sum fun i ↦ μ ↑i) = sum μ

Tactic:
ext1 t ht

Goal state after:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ ((sum fun i ↦ μ ↑i) + sum fun i ↦ μ ↑i) t = (sum μ) t
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
hs : s ∈ μ.cofinite
⊢ (toMeasurable μ sᶜ)ᶜ ∈ μ.cofinite

Tactic:
compl_mem_cofinite,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
hs : s ∈ μ.cofinite
⊢ μ (toMeasurable μ sᶜ) < ∞
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]

Goal state after:
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 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : atBot.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x ↦ μ (Ioc x a)) atBot (𝓝 (μ (⋃ b, Ioc b a)))

Tactic:
exact tendsto_measure_iUnion_atBot (monotone_id.Ioc antitone_const)

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
⊢ y ⤳ x

Tactic:
by
    rw [specializes_iff_forall_closed]
    intro K hK hyK
    apply IsClosed.isGδ at hK
    obtain ⟨Ts, hoTs, -, rfl⟩ := hK
    rw [mem_sInter] at hyK ⊢
    intros
    solve_by_elim [hxy.mem_open]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : infEDist x s ≤ ↑ε
y : α
hy : infEDist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
hε : ↑ε < ↑ε + ↑δ
⊢ edist x y ≤ ediam s + 2 * ↑ε + ↑δ

Tactic:
replace hx := hx.trans_lt hε

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
hε : ↑ε < ↑ε + ↑δ
hx : infEDist x s < ↑ε + ↑δ
⊢ edist x y ≤ ediam s + 2 * ↑ε + ↑δ
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s₁ t₁ : Set α
s₂ t₂ : Set β
⊢ hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂)

Tactic:
by
  refine le_of_forall_ge fun _ _ => ?_
  simp_all only [hausdorffEDist, infEDist_prod, max_le_iff, iSup_le_iff, mem_prod, true_and,
    implies_true]

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

Goal state before:
pp: ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
by_cases hs : IsBounded s

Goal state after:
case pos
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

case neg
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : ¬Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
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✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
⊢ AEMeasurable g μ

Tactic:
by
  classical
  nontriviality α
  have hα : Nonempty α := inferInstance
  rcases isEmpty_or_nonempty ι with hι | hι
  · simp only [IsEmpty.exists_iff, ofPred_false, isLUB_empty_iff] at hg
    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))
  let p : δ → (ι → α) → Prop := fun x f' => IsLUB { a | ∃ i, f' i = a } (g x)
  let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
  have hg_seq : ∀ b, IsLUB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) := by
    intro b
    simp only [g_seq, aeSeq, Set.piecewise]
    split_ifs with h
    · have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_ofPred_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
      rw [h_set_eq]
      exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
    · exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
  refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
  exact
    (ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm

Goal state after: