mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
⊢ UniformContinuousOn Inv.inv s

Tactic:
rw [Metric.uniformContinuousOn_iff_le]
  intro ε hε
  rcases NormedAddGroup.nhds_zero_basis_norm_lt.mem_iff.mp hs with ⟨r, hr₀, hr⟩
  simp only [Set.subset_compl_comm (t := s), Set.compl_ofPred, not_lt] at hr
  have hs₀ : ∀ x ∈ s, x ≠ 0 := fun x hx ↦ norm_pos_iff.mp <| hr₀.trans_le (hr hx)
  refine ⟨ε * r ^ 2, by positivity, fun x hx y hy hxy ↦ ?_⟩
  calc
    dist x⁻¹ y⁻¹ = ‖x‖⁻¹ * dist y x * ‖y‖⁻¹ := by
      simp [dist_eq_norm, inv_sub_inv' (hs₀ x hx) (hs₀ y hy)]
    _ ≤ r⁻¹ * (ε * r ^ 2) * r⁻¹ := by
      rw [dist_comm]
      gcongr <;> exact hr ‹_›
    _ = ε := by field_simp

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

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

Tactic:
exact h n

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
⊢ μ (⋃ i ∈ I, s i) = 0 ↔ ∀ i ∈ I, μ (s i) = 0

Tactic:
refine ⟨fun h i hi ↦ measure_mono_null (subset_biUnion_of_mem hi) h, fun h ↦ ?_⟩
  have _ := hI.to_subtype
  simpa [h] using measure_iUnion_le (μ := μ) fun x : I ↦ s x

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
h0 : Tendsto (fun k ↦ μ ((⋃ n, s n) \ s k)) l (𝓝 0)
⊢ μ (⋃ n, s n) = ⨆ n, μ (s n)

Tactic:
by
  refine le_antisymm ?_ <| iSup_le fun n ↦ measure_mono <| subset_iUnion _ _
  set S := ⋃ n, s n
  set M := ⨆ n, μ (s n)
  have A : ∀ k, μ S ≤ M + μ (S \ s k) := fun k ↦ calc
    μ S ≤ μ (S ∩ s k) + μ (S \ s k) := measure_le_inter_add_sdiff _ _ _
    _ ≤ μ (s k) + μ (S \ s k) := by gcongr; apply inter_subset_right
    _ ≤ M + μ (S \ s k) := by gcongr; exact le_iSup (μ ∘ s) k
  have B : Tendsto (fun k ↦ M + μ (S \ s k)) l (𝓝 M) := by simpa using tendsto_const_nhds.add h0
  exact ge_of_tendsto' B A

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ ⨆ i, MeasurableSpace.comap (fun x ↦ g x i) (inst✝ i) ≤ inst✝¹ ↔
    ∀ (a : δ), MeasurableSpace.comap (fun x ↦ g x a) (inst✝ a) ≤ inst✝¹

Tactic:
iSup_le_iff

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
⊢ Measurable fun x ↦ if hi : i ∈ s then x.2 ⟨i, hi⟩ else x.1 i

Tactic:
by_cases h : i ∈ s

Goal state after:
case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
h : i ∈ s
⊢ Measurable fun x ↦ if hi : i ∈ s then x.2 ⟨i, hi⟩ else x.1 i

case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
h : i ∉ s
⊢ Measurable fun x ↦ if hi : i ∈ s then x.2 ⟨i, hi⟩ else x.1 i
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = zero
⊢ sign (∑ i ∈ s, f i) = zero

Tactic:
simp_rw [zero_eq_zero, sign_eq_zero_iff] at h ⊢
    exact Finset.sum_eq_zero h

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1

pp: case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0

pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1

Tactic:
· cases lt_irrefl 0 (h₁.trans <| h.trans_lt h₃)

Goal state after:
case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1
Module: Mathlib.Data.Sign.Defs

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

Tactic:
if_neg <| asymm ha,

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ (if a < 0 then -1 else 0) = -1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : ℝ
⊢ (-↑x).abs = (↑x).abs

Tactic:
rw [abs_def, ← coe_neg, abs_def, abs_neg]

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

Goal state before:
pp: β : Type u_2
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
b : β
⊢ ↑(g b) ≤ ↑(f b)

Tactic:
exact ENNReal.coe_le_coe.2 (hgf _)

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
⊢ Summable (s.indicator f)

Tactic:
refine NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) ?_) hf
  split_ifs
  · exact le_refl (f a)
  · exact zero_le_coe

Goal state after:
Module: Mathlib.Data.EReal.Inv

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

Tactic:
rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]; exact EReal.coe_nonpos.1 h

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

Goal state before:
pp: case h.refine_2.refine_1
x : ℝ
⊢ IsOpen (Ioi (max (↑x) 0) ×ˢ Ioi 1)

Tactic:
exact IsOpen.prod isOpen_Ioi isOpen_Ioi

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

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m = boundedBy (sInfGen m)

Tactic:
refine le_antisymm ?_ ?_
  · refine le_boundedBy.2 fun s => le_iInf₂ fun μ hμ => ?_
    apply sInf_le hμ
  · refine le_sInf ?_
    intro μ hμ t
    exact le_trans (boundedBy_le t) (iInf₂_le μ hμ)

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

Goal state before:
pp: case h.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2))

Tactic:
exact IsOpen.prod isOpen_Ioi isOpen_Ioi

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

Goal state before:
pp: case inl
a : ℝ
h : a ≠ 0
a_neg : a < 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)

pp: case inr
a : ℝ
h : a ≠ 0
a_pos : 0 < a
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)

Tactic:
· exact neg_neg a ▸ continuousAt_mul_symm2 (continuousAt_mul_top_pos (neg_pos.2 a_neg))

Goal state after:
case inr
a : ℝ
h : a ≠ 0
a_pos : 0 < a
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ x ∈ ⋂ x, ⋂ y, ⋂ (_ : y ≤ x), s y, x ∈ ⋂ x, s x

Tactic:
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
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ x ∈ ⋂ x, s x, x ∈ ⋂ x, ⋂ y, ⋂ (_ : y ≤ x), s y

Tactic:
mem_iInter

Goal state after:
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: R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ Tendsto (fun x ↦ ↑⌊a * x⌋₊ / x) atTop (𝓝 a)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' A tendsto_const_nhds

Goal state after:
case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ ↑⌊a * b⌋₊ / b

case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case singleton
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t : Finset (Set α)
a : Set α
ht : ∀ s ∈ {a}, s ∈ S
h' : (⋂ s ∈ {a}, s).Nonempty
⊢ ⋂ s ∈ {a}, s ∈ S

Tactic:
| singleton a =>

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
n : ℕ
⊢ m (t ∩ ⋃ i, ⋃ (_ : i < n), s i) + m (t \ ⋃ i, s i) ≤ m t

Tactic:
rw [isCaratheodory_iUnion_lt _ (fun i _ => h i) t (n := n)]

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
n : ℕ
⊢ m (t ∩ ⋃ i, ⋃ (_ : i < n), s i) + m (t \ ⋃ i, s i) ≤ m (t ∩ ⋃ i, ⋃ (_ : i < n), s i) + m (t \ ⋃ i, ⋃ (_ : i < n), s i)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case neg
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
h : ∃ i, ¬P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
· obtain ⟨i, hi⟩ := h
    exact le_trans (le_iInf fun h => hi.elim h) (ENNReal.le_tsum i)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ s' ∈ piiUnionInter (fun i ↦ {s i}) S ↔ s' ∈ {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}

Tactic:
piiUnionInter,

Goal state after:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ s' ∈ {s_1 | ∃ t, ∃ (_ : ↑t ⊆ S), ∃ f, ∃ (_ : ∀ x ∈ t, f x ∈ {s x}), s_1 = ⋂ x ∈ t, f x} ↔
    s' ∈ {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}
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
⊢ t1 ∩ t2 ∈ piiUnionInter π S

Tactic:
piiUnionInter,

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
⊢ t1 ∩ t2 ∈ {s | ∃ t, ∃ (_ : ↑t ⊆ S), ∃ f, ∃ (_ : ∀ x ∈ t, f x ∈ π x), s = ⋂ x ∈ t, f x}
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝³ : (x : δ') → MeasurableSpace (π x)
inst✝² : (x : δ') → MeasurableSpace (π' x)
α₁ : Type u_8
β₁ : Type u_9
α₂ : Type u_10
β₂ : Type u_11
inst✝¹ : MeasurableSpace β₁
inst✝ : MeasurableSpace β₂
hα : α₁ ≃ α₂
hβ : β₁ ≃ᵐ β₂
x✝ : Set (α₁ → β₁)
h : MeasurableSet x✝
⊢ MeasurableSet (⇑(hα.arrowCongr' ↑hβ).symm ⁻¹' x✝)

Tactic:
exact MeasurableSet.preimage h <|
      measurable_pi_iff.mpr fun _ ↦ hβ.symm.measurable.comp (measurable_pi_apply _)

Goal state after:
Module: Mathlib.Order.Interval.Set.Monotone

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : k ≤ φ k
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
⊢ succ k ≤ φ (succ k)

Tactic:
ih

Goal state after:
case neg.inl
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : k ≤ φ k
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
⊢ succ (φ k) ≤ φ (succ k)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : g y ∈ iInter X
⊢ False

Tactic:
mem_iInter

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ False
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ y ∈ ⋂ i, f '' F^[i] univ

Tactic:
mem_iInter

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ ∀ (i : ℕ), y ∈ f '' F^[i] univ
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
h : s =ᵐ[μ] t
⊢ NullMeasurableSet t μ

Tactic:
nullMeasurableSet_iff_eventuallyMeasurableSet

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
h : s =ᵐ[μ] t
⊢ EventuallyMeasurableSet m0 (ae μ) t
Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
inst✝¹ : Countable ι
μ : F
inst✝ : Infinite ι
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ∞
⊢ μ (liminf s cofinite) = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← measure_limsup_cofinite_eq_zero h]
  exact measure_mono liminf_le_limsup

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

Goal state before:
pp: α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
⊢ ⨆ s, ∑ a ∈ s, μ (As a) ≤ μ (⋃ i, As i)

Tactic:
iSup_le_iff

Goal state after:
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
⊢ ∀ (i : Finset ι), ∑ a ∈ i, μ (As a) ≤ μ (⋃ i, As i)
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case inr
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
a : X
ha : a ∈ Iio b
⊢ map Subtype.val atTop = 𝓝[<] b

Tactic:
← comap_coe_nhdsLT_of_Ioo_subset hsb (fun _ => hs a ha) hb,

Goal state after:
case inr
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
a : X
ha : a ∈ Iio b
⊢ map Subtype.val (comap Subtype.val (𝓝[<] b)) = 𝓝[<] b
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
ext1 u hu
  rw [restrict_apply hu, restrict_apply hu, restrict_eq_self]
  exact inter_subset_right.trans h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
c : ℝ≥0
⊢ IsLocallyFiniteMeasure (c • μ)

Tactic:
by
  refine ⟨fun x => ?_⟩
  rcases μ.exists_isOpen_measure_lt_top x with ⟨o, xo, o_open, μo⟩
  refine ⟨o, o_open.mem_nhds xo, ?_⟩
  apply ENNReal.mul_lt_top _ μo
  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
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : ℕ → Set (Set α)
D_mem : ∀ (n : ℕ), D n ∈ {D | D ⊆ C ∧ D.Countable}
huD : ∀ (n : ℕ), u n < μ (⋃₀ D n)
hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable}
⊢ μ (⋃₀ ⋃ n, D n) = m

Tactic:
apply le_antisymm (le_biSup (f := fun D ↦ μ (⋃₀ D)) hD)

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

Goal state before:
pp: case basic
α : 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✝ u : Set α
hu : u ∈ S
⊢ μ (u ∩ t) = ν (u ∩ t)

Tactic:
exact ST_eq _ ht _ hu

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
this : x ∈ t ∩ v n
⊢ x ∈ t ∩ w n

Tactic:
exact ⟨hx, subset_toMeasurable μ _ this⟩

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

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ ⋃₀ memPartition f n = univ

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    ext x
    have : x ∈ ⋃₀ memPartition f n := by simp [ih]
    simp only [mem_sUnion, mem_univ,
      iff_true] at this ⊢
    obtain ⟨t, ht, hxt⟩ := this
    by_cases hxf : x ∈ f n
    · exact ⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩
    · exact ⟨t \ f n, ⟨t, ht, Or.inr rfl⟩, hxt, hxf⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ μ t ≠ ∞

Tactic:
· simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at ht
    exact ht.1

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ ν (toMeasurable (μ + ν) t ∩ s) = ν (t ∩ s)

Tactic:
rw [add_comm] at ht ⊢
  exact measure_toMeasurable_add_inter_left hs ht

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

Goal state before:
pp: α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
f g : α → δ
⊢ f =ᵐ[μ.restrict (⋃ i, s i)] g ↔ ∀ (i : ι), f =ᵐ[μ.restrict (s i)] g

Tactic:
by
  simp_rw [EventuallyEq, ae_restrict_iUnion_eq, eventually_iSup]

Goal state after:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l

Tactic:
rcases h.1 with ⟨S, hSc, hSp, hS⟩

Goal state after:
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
h : CountablySeparated α
s : Set α
⊢ CountablySeparated ↑s

Tactic:
rw [CountablySeparated.subtype_iff]
  exact h.countably_separated.mono (fun s ↦ id) <| subset_univ _

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

Goal state before:
pp: case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated α γ

pp: case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated α γ

Tactic:
· have := countable_left_of_prod_of_nonempty h
    infer_instance

Goal state after:
case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated α γ
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✝⁴ : Countable α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
this : ∀ (s : Set α), MeasurableSet s
⊢ BorelSpace α

Tactic:
have : ∀ s, @MeasurableSet α (borel α) s := fun s ↦ measurableSet_generateFrom (isOpen_discrete s)

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✝⁴ : Countable α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
this✝ : ∀ (s : Set α), MeasurableSet s
this : ∀ (s : Set α), MeasurableSet s
⊢ BorelSpace α