mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ x = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Goal state after:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ x ≤ 0
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ⊢ ∑' (m : ℕ), 2 ^ (-1 - ↑m) = 1

Tactic:
simp_rw [neg_sub_left, ENNReal.zpow_neg, ← Nat.cast_one (R := ℤ), ← Nat.cast_add, zpow_natCast,
    ENNReal.inv_pow, ENNReal.tsum_geometric_add_one, one_sub_inv_two, inv_inv]
  exact ENNReal.inv_mul_cancel (Ne.symm (NeZero.ne' 2)) (Ne.symm top_ne_ofNat)

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

Goal state before:
pp: α : Type u_1
ι : Sort u_2
inst✝ : Nonempty ι
m : ι → OuterMeasure α
s : Set α
⊢ (sInf (range fun i ↦ m i)) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Tactic:
sInf_apply (range_nonempty m)

Goal state after:
α : Type u_1
ι : Sort u_2
inst✝ : Nonempty ι
m : ι → OuterMeasure α
s : Set α
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range m, μ (t n) =
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case bot.coe
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, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₃
    exact continuousAt_mul_symm1 (continuousAt_mul_top_ne_zero h₃)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S s : Set α
⊢ s ∈ {S} → ∀ t ∈ {S}, (s ∩ t).Nonempty → s ∩ t ∈ {S}

Tactic:
h_s

Goal state after:
α : Type u_1
S s : Set α
h_s : s ∈ {S}
⊢ ∀ t ∈ {S}, (s ∩ t).Nonempty → s ∩ t ∈ {S}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case succ
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : (dissipate s n).Nonempty → dissipate s n ∈ C
h' : (dissipate s n ∩ s (n + 1)).Nonempty
⊢ dissipate s n ∩ s (n + 1) ∈ C

Tactic:
exact hC (dissipate s n) (hn h'.left) (s (n + 1)) (h (n + 1)) h'

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case a
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ g, MeasurableSet t

Tactic:
· exact fun t h_t => measurableSet_generateFrom (generatePiSystem.base h_t)

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

Goal state before:
pp: case intro
α : 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)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m (⋃ i, f i) = ∑' (i : β), extend m (f i)

Tactic:
rw [← Encodable.iUnion_decode₂, ← tsum_iUnion_decode₂]

Goal state after:
case intro
α : 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)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m (⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b) = ∑' (i : ℕ), extend m (⋃ b ∈ Encodable.decode₂ β i, f b)

case intro.m0
α : 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)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m ∅ = 0
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case intro.m0
α : 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)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m ∅ = 0

Tactic:
· exact extend_empty P0 m0

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ (⋂ x ∈ p1, f1 x) ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i

Tactic:
ht2_eq

Goal state after:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ (⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x = ⋂ i ∈ p1 ∪ p2, g i
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
⊢ d.Has (⋃ b, bif b then s₁ else s₂)

Tactic:
exact d.has_iUnion (pairwise_disjoint_on_bool.2 h) (Bool.forall_bool.2 ⟨h₂, h₁⟩)

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
s t : Set α
h : t =ᵐ[μ] ∅
⊢ s ∪ t =ᵐ[μ] s ↔ s ∪ t =ᵐ[μ] s ∪ ∅

Tactic:
rw [union_empty]

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

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

Tactic:
exact sdiff_subset_iff.1 (subset_toMeasurable _ _)

Goal state after:
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 : Set α
hs : (comap f μ) s = 0
⊢ μ (f '' s) = 0

Tactic:
rw [← nonpos_iff_eq_zero]

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 : Set α
hs : (comap f μ) s = 0
⊢ μ (f '' s) ≤ 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᵐ[μ] s ↔ t ≤ᵐ[μ] s

Tactic:
rw [ae_le_set]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᵐ[μ] s ↔ μ (t \ s) = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : T1Space β
inst✝¹ : SecondCountableTopology β
inst✝ : Nonempty β
f : α → β
h : ∀ (b : β), ∃ᵐ (x : α) ∂μ, f x ≠ b
⊢ ∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)

Tactic:
set m : OuterMeasure β := OuterMeasure.map f μ.toOuterMeasure
  replace h : ∀ b : β, m {b}ᶜ ≠ 0 := fun b => not_eventually.mpr (h b)
  inhabit β
  have : m univ ≠ 0 := ne_bot_of_le_ne_bot (h default) (measure_mono <| subset_univ _)
  rcases exists_mem_forall_mem_nhdsWithin_pos_measure this with ⟨b, -, hb⟩
  simp only [nhdsWithin_univ] at hb
  rcases exists_mem_forall_mem_nhdsWithin_pos_measure (h b) with ⟨a, hab : a ≠ b, ha⟩
  simp only [isOpen_compl_singleton.nhdsWithin_eq hab] at ha
  exact ⟨a, b, hab, ha, hb⟩

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ

Tactic:
· exact CompactSpace.isFiniteMeasure

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u : Set α
hu : MeasurableSet u
⊢ μ (u ∩ t) = ν (u ∩ t)

Tactic:
induction u, hu using induction_on_inter h_gen h_inter with
  | empty => simp only [Set.empty_inter, measure_empty]
  | basic u hu => exact ST_eq _ ht _ hu
  | compl u hu ihu =>
    have := T_eq t ht
    rw [Set.inter_comm] at ihu ⊢
    rwa [← measure_inter_add_sdiff t hu, ← measure_inter_add_sdiff t hu, ← ihu,
      ENNReal.add_right_inj] at this
    exact ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)
  | iUnion f hfd hfm ihf =>
    simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢
    simp only [measure_iUnion hfd hfm, ihf]

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

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : u ≠ v
hu : u = univ
hv : v = univ
⊢ Disjoint u v

Tactic:
rw [hu, hv] at huv

Goal state after:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : univ ≠ univ
hu : u = univ
hv : v = univ
⊢ Disjoint u v
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hv : v ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
⊢ Disjoint u v

Tactic:
obtain ⟨v', hv', hv'_eq⟩ := hv

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
⊢ Disjoint u v
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑(⋃ i ∈ memPartition f n, {x | x = i ∩ f n ∨ x = i \ f n})

Tactic:
ofPred_or

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑(⋃ i ∈ memPartition f n, {a | a = i ∩ f n} ∪ {a | a = i \ f n})
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
⊢ t ⊆ u → MeasurableSet u → (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ u

Tactic:
htu

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
⊢ MeasurableSet u → (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ u
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
⊢ (sInf (toOuterMeasure '' m)) s ≤ μ s

Tactic:
exact this s

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : ∀ μ' ∈ m, μ ≤ μ'
this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ μ s ≤ (sInf (toOuterMeasure '' m)) s

Tactic:
exact this s

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ ⨆ i, (μ.restrict (spanningSets μ i)) s = μ s

Tactic:
rw [← measure_toMeasurable s,
    ← iSup_restrict_spanningSets_of_measurableSet (measurableSet_toMeasurable _ _)]
  simp_rw [restrict_apply' (measurableSet_spanningSets μ _), Set.inter_comm s,
    ← restrict_apply (measurableSet_spanningSets μ _), ← restrict_toMeasurable_of_sFinite s,
    restrict_apply (measurableSet_spanningSets μ _), Set.inter_comm _ (toMeasurable μ s)]

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

Goal state before:
pp: case refine_3.refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
h : ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i
⊢ ∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i

pp: case refine_3.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
⊢ (∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i) → ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i

Tactic:
· refine ⟨fun n ↦ x ∈ natGeneratingSequence α n, ?_,
        mem_countablyGeneratedAtom_natGeneratingSequence x⟩
      contrapose! h
      refine ⟨fun n ↦ x ∈ natGeneratingSequence α n, h,
        mem_countablyGeneratedAtom_natGeneratingSequence x⟩

Goal state after:
case refine_3.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
⊢ (∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i) → ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_3.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
p : ℕ → Prop
hpq : ¬q p
hpx : x ∈ countablyGeneratedAtom α p
p' : ℕ → Prop
hqp' : q p'
hx_mem : x ∈ countablyGeneratedAtom α p'
hpp' : p ≠ p'
⊢ False

Tactic:
have h_disj : Disjoint (countablyGeneratedAtom α p) (countablyGeneratedAtom α p') :=
        disjoint_countablyGeneratedAtom hpp'

Goal state after:
case refine_3.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
p : ℕ → Prop
hpq : ¬q p
hpx : x ∈ countablyGeneratedAtom α p
p' : ℕ → Prop
hqp' : q p'
hx_mem : x ∈ countablyGeneratedAtom α p'
hpp' : p ≠ p'
h_disj : Disjoint (countablyGeneratedAtom α p) (countablyGeneratedAtom α p')
⊢ False
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_2.mpr
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
t : Set β
ht : MeasurableSet t
x : α
i : ι
hi : x ∉ s i
⊢ mk f ⋯ x ∈ t → ∃ i, mk f ⋯ x ∈ t ∧ x ∉ s i

Tactic:
exact fun h => ⟨i, h, hi⟩

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✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
⊢ Measurable (Function.uncurry fun x1 x2 ↦ x1 • x2)

Tactic:
suffices Measurable fun p : M × ℕ => p.2 • p.1 by apply this.comp measurable_swap
    refine measurable_from_prod_countable_left fun n => ?_
    induction n with
    | zero => simp only [zero_smul, ← Pi.zero_def, measurable_zero]
    | succ n ih =>
      simp only [succ_nsmul]
      exact ih.add measurable_id

Goal state after:
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 α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
s : Set α
h : HasCountableSeparatingOn α IsOpen[inst✝¹²] s
⊢ CountablySeparated ↑s

Tactic:
rw [CountablySeparated.subtype_iff]
  exact .mono (fun _ ↦ IsOpen.measurableSet) Subset.rfl

Goal state after:
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 α
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : MeasurableSpace α
inst✝¹⁴ : OpensMeasurableSpace α
inst✝¹³ : TopologicalSpace β
inst✝¹² : MeasurableSpace β
inst✝¹¹ : OpensMeasurableSpace β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : MeasurableSpace γ
inst✝⁸ : BorelSpace γ
inst✝⁷ : TopologicalSpace γ₂
inst✝⁶ : MeasurableSpace γ₂
inst✝⁵ : BorelSpace γ₂
inst✝⁴ : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
this :
  topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = (↑i).pi s}
⊢ borel ((i : ι) → X i) ≤ MeasurableSpace.pi

Tactic:
borel_eq_generateFrom_of_subbasis this

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι✝ : Sort y
s t u : Set α
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : MeasurableSpace α
inst✝¹⁴ : OpensMeasurableSpace α
inst✝¹³ : TopologicalSpace β
inst✝¹² : MeasurableSpace β
inst✝¹¹ : OpensMeasurableSpace β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : MeasurableSpace γ
inst✝⁸ : BorelSpace γ
inst✝⁷ : TopologicalSpace γ₂
inst✝⁶ : MeasurableSpace γ₂
inst✝⁵ : BorelSpace γ₂
inst✝⁴ : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
this :
  topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = (↑i).pi s}
⊢ MeasurableSpace.generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = (↑i).pi s} ≤ MeasurableSpace.pi
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : ↑ε / 2 ≠ 0
this : infEDist x s < infEDist x s + ↑ε / 2
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + ↑ε

Tactic:
obtain ⟨y : α, ys : y ∈ s, dxy : edist x y < infEDist x s + ↑ε / 2⟩ := infEDist_lt_iff.mp this

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : ↑ε / 2 ≠ 0
this : infEDist x s < infEDist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEDist x s + ↑ε / 2
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + ↑ε
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t) = hausdorffEDist s t

Tactic:
by
  simp [@hausdorffEDist_comm _ _ s _]

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

Goal state before:
pp: X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
⊢ infDist y E + diam E ≤ δ + diam E

Tactic:
grw [(mem_thickening_iff_infDist_lt ⟨x, hx⟩).1 hy]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s t : Set α
⊢ {x | infEDist x s < ENNReal.ofReal δ ∨ infEDist x t < ENNReal.ofReal δ} =
    {x | infEDist x s < ENNReal.ofReal δ} ∪ {x | infEDist x t < ENNReal.ofReal δ}

Tactic:
ofPred_or

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s t : Set α
⊢ {x | infEDist x s ≤ ENNReal.ofReal δ ∨ infEDist x t ≤ ENNReal.ofReal δ} =
    {x | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x | infEDist x t ≤ ENNReal.ofReal δ}

Tactic:
ofPred_or

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : 0 < ε
⊢ (thickening ε s).Nonempty ↔ s.Nonempty

Tactic:
by
  simp [nonempty_iff_ne_empty, thickening_eq_empty_iff_of_pos hε]

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 x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ ↑(r / 2) + ↑(r / 2) = ↑r

Tactic:
rw [← ENNReal.coe_add, add_halves]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
⊢ Tendsto f l (𝓝ˢ s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε

Tactic:
rw [(hasBasis_nhdsSet_thickening hs₁).tendsto_right_iff]

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
⊢ (∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ thickening i s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ f.bind (const α) = f

Tactic:
ext; simp

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n k : ℕ
x✝ : k ∈ Finset.range n
h : ¬i k ≤ f a
⊢ ⊥ ≤ ⨆ k, ⨆ (_ : i k ≤ f a), i k

Tactic:
· exact bot_le

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

Goal state before:
pp: x ε : ℝ
⊢ TotallyBounded (ball x ε)

Tactic:
Real.ball_eq_Ioo

Goal state after:
x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))