mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case top
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
⊢ MeasurableSet (⋃ i, f ⁻¹' {some i})ᶜ

Tactic:
exact .compl <| .iUnion h

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
a : α
ha : a ∈ s
⊢ (∑ i,
      if Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) i = a then ↑(Sum.elim sgn 0 i) else 0) =
    f a

Tactic:
simp [hf _ ha]

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
⊢ Continuous[inst✝², inst✝¹] ⇑(algebraMap R A) ↔ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1 • p.2

Tactic:
by
  refine ⟨fun h => ?_, fun h => have : ContinuousSMul R A := ⟨h⟩; continuous_algebraMap _ _⟩
  simp only [Algebra.smul_def]
  exact (h.comp continuous_fst).mul continuous_snd

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
⊢ (if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0

Tactic:
split_ifs with h h'

Goal state after:
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ (if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0

Tactic:
split_ifs with h h'

Goal state after:
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf_nonneg : ∀ (n : α), 0 ≤ f n
hf : Summable f
⊢ ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)

Tactic:
by
  simp_rw [ENNReal.ofReal, ENNReal.tsum_coe_eq (NNReal.hasSum_real_toNNReal_of_nonneg hf_nonneg hf)]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
hd : Summable d
⊢ CauchySeq f

Tactic:
refine EMetric.cauchySeq_iff_NNReal.2 fun ε εpos ↦ ?_
  -- Actually we need partial sums of `d` to be a Cauchy sequence.
  replace hd : CauchySeq fun n : ℕ ↦ ∑ x ∈ Finset.range n, d x :=
    let ⟨_, H⟩ := hd
    H.tendsto_sum_nat.cauchySeq
  -- Now we take the same `N` as in one of the definitions of a Cauchy sequence.
  refine (Metric.cauchySeq_iff'.1 hd ε (NNReal.coe_pos.2 εpos)).imp fun N hN n hn ↦ ?_
  specialize hN n hn
  -- We simplify the known inequality.
  rw [dist_nndist, NNReal.nndist_eq, ← Finset.sum_range_add_sum_Ico _ hn, add_tsub_cancel_left,
    NNReal.coe_lt_coe, max_lt_iff] at hN
  rw [edist_comm]
  -- Then use `hf` to simplify the goal to the same form.
  refine lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ ↦ hf _) ?_
  exact mod_cast hN.1

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

Goal state before:
pp: C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
⊢ ↑C.toReal / ↑↑n = ↑(C.toReal / ↑n)

Tactic:
← coe_div C.toReal n

Goal state after:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
⊢ ↑(C.toReal / ↑n) = ↑(C.toReal / ↑n)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
⊢ limsup (u + v) f ≤ a + b

Tactic:
rcases eq_top_or_lt_top b with rfl | h
  · rw [add_top_of_ne_bot ha.ne_bot]; exact le_top
  · exact (limsup_add_le (.inr (hb.trans_lt h).ne) (.inl ha.ne_top)).trans (add_le_add ha.le hb)

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i ↦ Nat.casesOn i s fun x ↦ ∅
⊢ ∀ (b' : ℕ), b' ≠ 0 → m (f b') = 0

Tactic:
by
        rintro (_ | i)
        · simp
        · simp [f, m_empty]

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

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

Tactic:
intro x y

Goal state after:
x : EReal × EReal
y : EReal
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
s : Set β
⊢ ⨆ (_ : (f '' s).Nonempty), m (f '' s) = ⨆ (_ : s.Nonempty), m (f '' s)

Tactic:
rw [image_nonempty]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ ((comap f) (⨅ i, m i)) s = (⨅ i, (comap f) (m i)) s

Tactic:
refine ((comap_mono f).map_iInf_le s).antisymm ?_

Goal state after:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ (⨅ i, (comap f) (m i)) s ≤ ((comap f) (⨅ i, m i)) s
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ∩ range f ⊆ f '' ⋃ i, t i

Tactic:
←
      image_preimage_eq_inter_range

Goal state after:
case refine_1
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ f '' f ⁻¹' s ⊆ f '' ⋃ i, t i
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i ↦ ↑(w i)) i * ↑((fun i ↦ δ' i / max 1 (w i)) i) ≤ ↑(δ' i)

Tactic:
rw [coe_div (this i).ne']

Goal state after:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i ↦ ↑(w i)) i * (↑(δ' i) / ↑(max 1 (w i))) ≤ ↑(δ' i)
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋂ x, dissipate s x = ⋂ x, s x

Tactic:
apply Subset.antisymm <;> simp_rw [subset_def, dissipate_def, mem_iInter]

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β), (∀ (i i_1 : α), i_1 ≤ i → x ∈ s i_1) → ∀ (i : α), x ∈ s i

case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β), (∀ (i : α), x ∈ s i) → ∀ (i i_1 : α), i_1 ≤ i → x ∈ s i_1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ Tendsto (fun x ↦ x / n) atTop atTop

Tactic:
rw [Tendsto, map_div_atTop_eq_nat n hn.bot_lt]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ GenerateHas C s

Tactic:
convert! GenerateHas.compl h

Goal state after:
α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ s = sᶜᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
s : Set α
hs : s ∈ ⨅ i, f i
⊢ ∃ t ∈ ⨅ i, f i, MeasurableSet t ∧ t ⊆ s

Tactic:
← Equiv.plift.surjective.iInf_comp,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
s : Set α
hs : s ∈ ⨅ x, f (Equiv.plift x)
⊢ ∃ t ∈ ⨅ i, f i, MeasurableSet t ∧ t ⊆ s
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

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

Tactic:
← Equiv.plift.surjective.iInf_comp,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
⊢ s = ⇑e.toEquiv '' t ↔ ⇑e.symm '' s = t

Tactic:
Equiv.eq_image_iff_symm_image_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
⊢ ⇑e.symm '' s = t ↔ ⇑e.symm '' s = t
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

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

Tactic:
by
  rw [← measure_inter_add_sdiff₀ (s ∪ t) ht, union_inter_cancel_right, union_sdiff_right, ←
    measure_inter_add_sdiff₀ s ht, add_comm, ← add_assoc, add_right_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ (mapₗ (AEMeasurable.mk f hf)) μ = map f μ

Tactic:
simp [map, hf]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f 0
⊢ map f 0 = 0

Tactic:
simp [map, hf]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : ¬AEMeasurable f 0
⊢ map f 0 = 0

Tactic:
simp [map, hf]

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

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

Tactic:
simp [map, hf]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ᵐ (x : α) ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ (x : α) ∂μ, x ∈ Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Ioc b a → P x

Tactic:
by
  simp only [uIoc_eq_union, mem_union, or_imp, eventually_and]

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
⊢ SFinite (sum m)

Tactic:
by
  obtain ⟨f, hf⟩ : ∃ f : ι → ℕ, Function.Injective f := Countable.exists_injective_nat ι
  refine ⟨_, fun n ↦ ?_, (sum_extend_zero hf m).symm⟩
  rcases em (n ∈ range f) with ⟨i, rfl⟩ | hn
  · rw [hf.extend_apply]
    infer_instance
  · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply]
    infer_instance

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
⊢ μ (⋃ n, t n) = ⨆ n, μ (t n)

Tactic:
clear! ι

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
⊢ μ (⋃ n, t n) = ⨆ n, μ (t n)
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)}
⊢ posmeas.Countable

Tactic:
have countable_union : posmeas = ⋃ n, fairmeas n := by
    have fairmeas_eq : ∀ n, fairmeas n = (fun i => μ (As i)) ⁻¹' Ici (as n) := fun n => by
      simp only [fairmeas]
      rfl
    simpa only [fairmeas_eq, posmeas_def, ← preimage_iUnion,
      iUnion_Ici_eq_Ioi_of_lt_of_tendsto (fun n => (as_mem n).1) as_lim]

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
⊢ posmeas.Countable
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ |(μ (s \ t)).toReal - (μ (t \ s)).toReal| ≤ (μ (s \ t)).toReal + (μ (t \ s)).toReal

Tactic:
convert! abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal <;> simp

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : ⊥ < m
⊢ ∃ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D) = m

Tactic:
obtain ⟨u, -, u_mem, u_lim⟩ :
        ∃ u : ℕ → ℝ≥0∞, StrictMono u ∧ (∀ n, u n ∈ Ioo 0 m) ∧ Tendsto u atTop (𝓝 m) :=
      exists_seq_strictMono_tendsto' hm

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
⊢ ∃ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D) = m
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : 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 : Set α
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
x✝ : MeasurableSpace α
c : R
μ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ (c • μ.toOuterMeasure) (⋃ i, s i) = ∑' (i : ℕ), (c • μ.toOuterMeasure) (s i)

Tactic:
by
        simp only [smul_apply, coe_toOuterMeasure, ENNReal.tsum_const_smul,
          measure_iUnion hd hs]

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

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
⊢ a ∈ memPartitionSet f n a

Tactic:
by
  induction n with
  | zero => simp [memPartitionSet]
  | succ n ih =>
    classical
    rw [memPartitionSet_succ]
    split_ifs with h <;> exact ⟨ih, h⟩

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

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

Tactic:
exact measurableAtom_subset hs hx

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ ⋃ i, f '' spanningSets μ i ∪ (range f)ᶜ = univ

Tactic:
rw [← Set.iUnion_union, ← Set.image_iUnion, iUnion_spanningSets,
      Set.image_univ, Set.union_compl_self]

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
i : ι
hi : i ∈ F
C : Finset ι
x : α
hx : x ∈ ⋂ i ∈ C, s i ∧ x ∈ ⋂ i ∈ F \ C, (s i)ᶜ
hxs : x ∈ s i
⊢ i ∈ C

Tactic:
mem_iInter₂,

Goal state after:
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
i : ι
hi : i ∈ F
C : Finset ι
x : α
hx : (∀ i ∈ C, x ∈ s i) ∧ x ∈ ⋂ i ∈ F \ C, (s i)ᶜ
hxs : x ∈ s i
⊢ i ∈ C
Module: Mathlib.MeasureTheory.Order.Lattice

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ ∀ n_1 ∈ range (n + 1), Measurable (f n_1)

Tactic:
simpa [Finset.mem_range]

Goal state after:
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_gd : IsGδ t
⊢ HasSeparatingCover s t

Tactic:
obtain ⟨T, T_open, T_count, T_int⟩ := t_gd

Goal state after:
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
⊢ HasSeparatingCover s t
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 δ
h : SecondCountableTopologyEither α β
⊢ OpensMeasurableSpace (α × β)

Tactic:
apply opensMeasurableSpace_iff_forall_measurableSet.2 (fun s hs ↦ ?_)

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 δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
⊢ MeasurableSet s
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
⊢ infEDist x s < r ↔ ∃ y ∈ s, edist x y < r

Tactic:
by
  simp_rw [infEDist, iInf_lt_iff, exists_prop]

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

Goal state before:
pp: case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
ht : t.Nonempty
⊢ ∅ = ∅ ∧ t = ∅ ∨ ∅.Nonempty ∧ t.Nonempty

Tactic:
rw [hausdorffEDist_comm] at fin
      exact Or.inr ⟨nonempty_of_hausdorffEDist_ne_top ht fin, ht⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ cthickening 0 E ⊆ thickening δ E

Tactic:
exact cthickening_subset_thickening' δ_pos δ_pos E

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s₁ s₂ t₁ t₂ : Set α
⊢ hausdorffEDist (s₁ ∪ s₂) (t₁ ∪ t₂) ≤ max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂)

Tactic:
simp_rw [union_eq_iUnion, sup_eq_iSup]
  convert! hausdorffEDist_iUnion_le with (_ | _)

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

Goal state before:
pp: case neg.h₂
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ ⋂ δ ∈ s, cthickening δ E ⊆ cthickening δ E

Tactic:
exact biInter_subset_of_mem hδs

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : (hausdorffEDist s t).toReal < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ hausdorffEDist s t < ENNReal.ofReal r

Tactic:
← ENNReal.toReal_ofReal (le_of_lt r0),

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : (hausdorffEDist s t).toReal < (ENNReal.ofReal r).toReal
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ hausdorffEDist s t < ENNReal.ofReal r
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Preorder β
s : Set α
f g : α →ₛ β
H : f ≤ g
hs : MeasurableSet s
x : α
⊢ (f.restrict s) x ≤ (g.restrict s) x

Tactic:
by
    simp only [coe_restrict _ hs, indicator_le_indicator (H x)]

Goal state after: