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

Goal state before:
pp: case top.top
h : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ ⊥
h' : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
exact continuousAt_add_top_top

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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : f z > z₁
H : f x < f z
⊢ min (f z) (f x) ∈ u

Tactic:
simpa [H.le]

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

Goal state before:
pp: case h.refine_1
x : ℝ
p : EReal × EReal
p_in_prod : (↑x < p.1 ∧ 0 < p.1) ∧ 1 < p.2
⊢ ↑x < p.1 * p.2

Tactic:
rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩

Goal state after:
case h.refine_1
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
⊢ ↑x < p.1 * p.2
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
⊢ LowerSemicontinuousWithinAt (fun z ↦ f z + g z) s x

Tactic:
by
  intro y hy
  obtain ⟨u, v, u_open, xu, v_open, xv, h⟩ :
    ∃ u v : Set γ,
      IsOpen u ∧ f x ∈ u ∧ IsOpen v ∧ g x ∈ v ∧ u ×ˢ v ⊆ { p : γ × γ | y < p.fst + p.snd } :=
    mem_nhds_prod_iff'.1 (hcont (isOpen_Ioi.mem_nhds hy))
  by_cases hx₁ : ∃ l, l < f x
  · obtain ⟨z₁, z₁lt, h₁⟩ : ∃ z₁ < f x, Ioc z₁ (f x) ⊆ u :=
      exists_Ioc_subset_of_mem_nhds (u_open.mem_nhds xu) hx₁
    by_cases hx₂ : ∃ l, l < g x
    · obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v :=
        exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂
      filter_upwards [hf z₁ z₁lt, hg z₂ z₂lt] with z h₁z h₂z
      have A1 : min (f z) (f x) ∈ u := by
        by_cases! H : f z ≤ f x
        · simpa [H] using h₁ ⟨h₁z, H⟩
        · simpa [H.le]
      have A2 : min (g z) (g x) ∈ v := by
        by_cases! H : g z ≤ g x
        · simpa [H] using h₂ ⟨h₂z, H⟩
        · simpa [H.le]
      have : (min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v := ⟨A1, A2⟩
      calc
        y < min (f z) (f x) + min (g z) (g x) := h this
        _ ≤ f z + g z := add_le_add (min_le_left _ _) (min_le_left _ _)
    · simp only [not_exists, not_lt] at hx₂
      filter_upwards [hf z₁ z₁lt] with z h₁z
      have A1 : min (f z) (f x) ∈ u := by
        by_cases! H : f z ≤ f x
        · simpa [H] using h₁ ⟨h₁z, H⟩
        · simpa [H.le]
      have : (min (f z) (f x), g x) ∈ u ×ˢ v := ⟨A1, xv⟩
      calc
        y < min (f z) (f x) + g x := h this
        _ ≤ f z + g z := add_le_add (min_le_left _ _) (hx₂ (g z))
  · simp only [not_exists, not_lt] at hx₁
    by_cases hx₂ : ∃ l, l < g x
    · obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v :=
        exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂
      filter_upwards [hg z₂ z₂lt] with z h₂z
      have A2 : min (g z) (g x) ∈ v := by
        by_cases! H : g z ≤ g x
        · simpa [H] using h₂ ⟨h₂z, H⟩
        · simpa [H.le] using h₂ ⟨z₂lt, le_rfl⟩
      have : (f x, min (g z) (g x)) ∈ u ×ˢ v := ⟨xu, A2⟩
      calc
        y < f x + min (g z) (g x) := h this
        _ ≤ f z + g z := add_le_add (hx₁ (f z)) (min_le_left _ _)
    · simp only [not_exists, not_lt] at hx₁ hx₂
      apply Filter.Eventually.of_forall
      intro z
      have : (f x, g x) ∈ u ×ˢ v := ⟨xu, xv⟩
      calc
        y < f x + g x := h this
        _ ≤ f z + g z := add_le_add (hx₁ (f z)) (hx₂ (g z))

Goal state after:
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) < ε

Tactic:
refine lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i ↦ ?_) Hsum

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 * ↑((fun i ↦ δ' i / max 1 (w i)) i) ≤ ↑(δ' i)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ LowerSemicontinuousWithinAt f⁻¹ s a ↔ UpperSemicontinuousWithinAt f s a

Tactic:
rw [lowerSemicontinuousWithinAt_iff, inv_surjective.forall, upperSemicontinuousWithinAt_iff]

Goal state after:
α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ (∀ (x : β), x⁻¹ < f⁻¹ a → ∀ᶠ (x' : α) in 𝓝[s] a, x⁻¹ < f⁻¹ x') ↔ ∀ (y : β), f a < y → ∀ᶠ (x' : α) in 𝓝[s] a, f x' < y
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case coe.bot
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✝, ⊥)

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

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✝, ⊤)

pp: case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

pp: case top.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✝)

pp: case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
· simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₁
    exact continuousAt_mul_symm2 (continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₁))

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

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✝, ⊤)

case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

case top.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✝)

case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)
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
⊢ Tendsto (fun x ↦ ↑⌊x⌋₊ / x) atTop (𝓝 1)

Tactic:
simpa using tendsto_nat_floor_mul_div_atTop (zero_le_one' R)

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ Filter.map (fun x ↦ x / n) atTop ≤ atTop

Tactic:
map_div_atTop_eq_nat n hn.bot_lt

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ atTop ≤ atTop
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

Tactic:
by_cases h : P s <;> simp [extend, *]

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
⊢ MeasurableSet {x | Tendsto (fun n ↦ f n x) l l'}

Tactic:
by
  rcases l.exists_antitone_basis with ⟨u, hu⟩
  rcases (Filter.hasBasis_self.mpr hl'.exists_measurable_subset).exists_antitone_subbasis with
    ⟨v, v_meas, hv⟩
  simp only [hu.tendsto_iff hv.toHasBasis, true_imp_iff, true_and, ofPred_forall, ofPred_exists]
  exact .iInter fun n ↦ .iUnion fun _ ↦ .biInter (to_countable _) fun i _ ↦
    (v_meas n).2.preimage (hf i)

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

Goal state before:
pp: α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
⊢ m.trim ≤ m.trim

Tactic:
simp only [le_trim_iff]

Goal state after:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
⊢ ∀ (s : Set α), MeasurableSet s → m.trim s ≤ m s
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ (∀ᵐ (a : α) ∂ν, a ∉ s) → μ s = 0

Tactic:
measure_eq_zero_iff_ae_notMem

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ (∀ᵐ (a : α) ∂ν, a ∉ s) → ∀ᵐ (a : α) ∂μ, a ∉ s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Tactic:
rw [union_comm, inter_comm, measure_union_add_inter t hs, add_comm]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)

Tactic:
set T : ℕ → Set α := fun n => toMeasurable μ (t n)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
T : ℕ → Set α := fun n ↦ toMeasurable μ (t n)
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)
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 α
μ : Measure α
hs : Fact (μ s < ∞)
⊢ (μ.restrict s) univ < ∞

Tactic:
simpa using hs.elim

Goal state after:
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)}
n : ℕ
⊢ fairmeas n = (fun i ↦ μ (As i)) ⁻¹' Ici (as n)

Tactic:
simp only [fairmeas]

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)}
n : ℕ
⊢ {i | as n ≤ μ (As i)} = (fun i ↦ μ (As i)) ⁻¹' Ici (as 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)}
countable_union : posmeas = ⋃ n, fairmeas n
⊢ posmeas.Countable

Tactic:
rw [countable_union]

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
⊢ (⋃ n, fairmeas n).Countable
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ s ≠ ∞
ht : MeasurableSet t
hst : s ⊆ t
⊢ μ.restrict (t ∩ toMeasurable μ s) = μ.restrict s

Tactic:
ext u hu

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ s ≠ ∞
ht : MeasurableSet t
hst : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict (t ∩ toMeasurable μ s)) u = (μ.restrict s) u
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

Tactic:
constructor <;> intros

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

case mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case pos.hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
ha : Order.IsPredPrelimit a
this : atBot.IsCountablyGenerated
⊢ ∃ i, μ (s ↑i) ≠ ∞

Tactic:
· simpa only [Subtype.exists, exists_prop]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᵐ[μ.restrict sᶜ] fun x ↦ b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = (μ.restrict s) (f ⁻¹' t)

Tactic:
rw [Measure.restrict_apply₀ (f_mble t_mble)]
  rw [EventuallyEq, ae_iff, Measure.restrict_apply₀] at hs
  · apply le_antisymm _ (measure_mono inter_subset_left)
    apply (measure_mono (Eq.symm (inter_union_compl (f ⁻¹' t) s)).le).trans
    apply (measure_union_le _ _).trans
    suffices μ ((f ⁻¹' t) ∩ sᶜ) = 0 by simp [this]
    rw [← nonpos_iff_eq_zero, ← hs]
    gcongr
    exact fun x hx hfx ↦ ht (hfx ▸ hx)
  · exact NullMeasurableSet.of_null hs

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

Goal state before:
pp: case refine_1
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ ⋃ n, memPartition t n
⊢ MeasurableSet u

pp: case refine_2
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ range t
⊢ MeasurableSet u

Tactic:
· simp only [mem_iUnion] at hu
    obtain ⟨n, hun⟩ := hu
    induction n generalizing u with
    | zero =>
      simp only [memPartition_zero, mem_singleton_iff] at hun
      rw [hun]
      exact MeasurableSet.univ
    | succ n ih =>
      simp only [memPartition_succ, mem_ofPred_eq] at hun
      obtain ⟨v, hv, huv⟩ := hun
      rcases huv with rfl | rfl
      · exact (ih v hv).inter (measurableSet_generateFrom ⟨n, rfl⟩)
      · exact (ih v hv).diff (measurableSet_generateFrom ⟨n, rfl⟩)

Goal state after:
case refine_2
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ range t
⊢ MeasurableSet u
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ generateFrom (⋃ n, countablePartition α n) = m

Tactic:
rw [countablePartition, generateFrom_iUnion_memPartition,
    range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
    generateFrom_countableGeneratingSet]

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

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n) + ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n) ≤
    ∑' (x : ↑{k | μ (t' k) ≤ ν (t' k)}), min (μ (t' ↑x)) (ν (t' ↑x)) +
      ∑' (x : ↑{k | ν (t' k) < μ (t' k)}), min (μ (t' ↑x)) (ν (t' ↑x))

Tactic:
refine add_le_add (tsum_congr ?_).le (tsum_congr ?_).le
      · rw [Subtype.forall]
        intro n hn; simpa
      · rw [Subtype.forall]
        intro n hn
        rw [mem_ofPred_eq] at hn
        simp [le_of_lt hn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (range fun a ↦ (g (f a)) a) ⊆ ⋃ i ∈ range ⇑f, range ⇑(g i)

Tactic:
rintro _ ⟨a, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : α
⊢ (fun a ↦ (g (f a)) a) a ∈ ⋃ i ∈ range ⇑f, range ⇑(g i)
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
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB (range fun i ↦ f i b) (g b)
⊢ ∀ t ∈ range Ioi, MeasurableSet (g ⁻¹' t)

Tactic:
rintro _ ⟨a, rfl⟩

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB (range fun i ↦ f i b) (g b)
a : α
⊢ MeasurableSet (g ⁻¹' Ioi a)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case hnhds
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U

Tactic:
let V := f ⁻¹' (thickening (δ / 2) {f x})

Goal state after:
case hnhds
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
⊢ ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∑' (n : ℕ), ↑((eapproxDiff f n) a) = f a

Tactic:
by
  simp_rw [ENNReal.tsum_eq_iSup_nat' (tendsto_add_atTop_nat 1), sum_eapproxDiff,
    iSup_eapprox_apply hf a]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ (const α c).lintegral (μ.restrict s) = c * μ s

Tactic:
const_lintegral,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ c * (μ.restrict s) univ = c * μ s
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (support ⇑f)

Tactic:
rw [f.support_eq]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y})
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ ∀ t ∈ range Iio, MeasurableSet t

Tactic:
rintro _ ⟨a, rfl⟩

Goal state after:
a : ℝ
⊢ MeasurableSet (Iio a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ ∀ t ∈ range Ioi, MeasurableSet t

Tactic:
rintro _ ⟨a, rfl⟩

Goal state after:
a : ℝ
⊢ MeasurableSet (Ioi a)