mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s : Finset ι
y : (i : ↥s) → π ↑i
i : ι
z : π i
hi : i ∉ s
⊢ updateFinset (updateFinset x s y) {i} (uniqueElim z) =
    updateFinset x (s ∪ {i}) ((piFinsetUnion π ⋯) (y, uniqueElim z))

Tactic:
updateFinset_updateFinset

Goal state after:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s : Finset ι
y : (i : ↥s) → π ↑i
i : ι
z : π i
hi : i ∉ s
⊢ updateFinset x (s ∪ {i}) ((piFinsetUnion π ?m.54) (y, uniqueElim z)) =
    updateFinset x (s ∪ {i}) ((piFinsetUnion π ⋯) (y, uniqueElim z))

ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s : Finset ι
y : (i : ↥s) → π ↑i
i : ι
z : π i
hi : i ∉ s
⊢ Disjoint s {i}
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ dist x⁻¹ y⁻¹ ≤ ε

Tactic:
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.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
⊢ MeasurableSet {x | p x ↔ q x}

Tactic:
by
  have h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x} := by ext; simp; grind
  rw [h_eq]
  exact (hs.imp ht).inter (ht.imp hs)

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯
s : Set α
hs : MeasurableSet s
⊢ p s hs

Tactic:
induction hs
  exacts [hC _ ‹_› _, empty, compl _ ‹_› ‹_›, iUnion ‹_› ‹_› ‹_›]

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

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
h : y ∈ measurableAtom x
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
⊢ y ∈ s

Tactic:
by
  simp only [measurableAtom, mem_iInter] at h
  exact h s hxs hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ MeasurableSpace.comap Prod.fst mβ ≤ MeasurableSpace.map f m

Tactic:
rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ MeasurableSpace.comap Prod.snd mγ ≤ MeasurableSpace.map f m

Tactic:
rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable α
f : α × β → γ
hf : ∀ (x : α), Measurable fun y ↦ f (x, y)
h'f : ∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)
⊢ Measurable f

Tactic:
change Measurable ((fun p ↦ f (p.2, p.1)) ∘ Prod.swap)
  exact (measurable_from_prod_countable_left' hf h'f).comp measurable_swap

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
⊢ Measurable fun v ↦ v.elim hj

Tactic:
by_cases hji : j = i

Goal state after:
case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : j = i
⊢ Measurable fun v ↦ v.elim hj

case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v ↦ v.elim hj
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : EReal
⊢ x.abs = 0 ↔ x = 0

Tactic:
induction x

Goal state after:
case bot
⊢ ⊥.abs = 0 ↔ ⊥ = 0

case coe
a✝ : ℝ
⊢ (↑a✝).abs = 0 ↔ ↑a✝ = 0

case top
⊢ ⊤.abs = 0 ↔ ⊤ = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
by_cases hf : ∀ i, f i = 0
  · simp [hf]
  · rw [← ENNReal.tsum_eq_zero] at hf
    have : Tendsto (fun s : Finset α => ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' i, f i)) := by
      simp only [← Finset.mul_sum]
      exact ENNReal.Tendsto.const_mul ENNReal.summable.hasSum (Or.inl hf)
    exact HasSum.tsum_eq this

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

Goal state before:
pp: case inl.inl
c : EReal
hc : 0 ≤ c
ha : 0 ≤ 0
h : c < 0
⊢ ∃ a' ∈ Ioo 0 0, c < a' * ⊤

Tactic:
exact (not_le_of_gt h hc).rec

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

Goal state before:
pp: case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ * b < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c

Tactic:
rw [top_mul_of_pos h₂] at hc

Goal state after:
case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c
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) ≤ (fun i ↦ ↑(d i)) n
hd : ∑' (i : ℕ), ↑(d i) ≠ ∞
⊢ CauchySeq f

Tactic:
rw [ENNReal.tsum_coe_ne_top_iff_summable] at hd

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable d
⊢ CauchySeq f
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
refine Filter.Eventually.of_forall fun x' => ?_

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
refine Filter.Eventually.of_forall fun x' => ?_

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
by
  rcases eq_top_or_lt_top a with rfl | a_top
  · rw [ne_self_iff_false, false_or] at h₂; rw [top_mul_of_pos h₂] at hc; exact (not_top_lt hc).rec
  rcases le_or_gt b 0 with b0 | b0
  · obtain ⟨a', aa', a_top'⟩ := exists_between a_top
    exact ⟨a', mem_Ioo.2 ⟨aa', a_top'⟩, lt_of_le_of_lt (mul_le_mul_of_nonpos_right aa'.le b0) hc⟩
  rcases eq_top_or_lt_top b with rfl | b_top
  · rcases lt_trichotomy a 0 with a0 | rfl | a0
    · obtain ⟨a', aa', a0'⟩ := exists_between a0
      rw [mul_top_of_neg a0] at hc
      refine ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt a0'⟩, mul_top_of_neg a0' ▸ hc⟩
    · rw [ne_self_iff_false, ne_self_iff_false, false_or] at h₁; exact h₁.rec
    · rw [mul_top_of_pos a0] at hc; exact (not_top_lt hc).rec
  · obtain ⟨a', aa', hc'⟩ := exists_between ((lt_div_iff b0 b_top.ne).2 hc)
    exact ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt hc'⟩, (lt_div_iff b0 b_top.ne).1 hc'⟩

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

Goal state before:
pp: ⊢ Tendsto toReal (𝓝[≠] ⊥) atBot

Tactic:
by
  rw [nhdsWithin_bot, tendsto_map'_iff]
  exact tendsto_id

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ (OuterMeasure.ofFunction m m_empty) s = ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i)

Tactic:
rw [OuterMeasure.ofFunction_apply]

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n) =
    ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i)
Module: Mathlib.Topology.Instances.EReal.Lemmas

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

Tactic:
induction x

Goal state after:
case bot
y : EReal
h : (⊥, y).1 ≠ ⊤ ∨ (⊥, y).2 ≠ ⊥
h' : (⊥, y).1 ≠ ⊥ ∨ (⊥, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, y)

case coe
y : EReal
a✝ : ℝ
h : (↑a✝, y).1 ≠ ⊤ ∨ (↑a✝, y).2 ≠ ⊥
h' : (↑a✝, y).1 ≠ ⊥ ∨ (↑a✝, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, y)

case top
y : EReal
h : (⊤, y).1 ≠ ⊤ ∨ (⊤, y).2 ≠ ⊥
h' : (⊤, y).1 ≠ ⊥ ∨ (⊤, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, y)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: x y : EReal
h₁ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊥
h₂ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊤
h₃ : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ 0
h₄ : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (x, y)

Tactic:
induction x

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

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

case top
y : EReal
h₁ : (⊤, y).1 ≠ 0 ∨ (⊤, y).2 ≠ ⊥
h₂ : (⊤, y).1 ≠ 0 ∨ (⊤, y).2 ≠ ⊤
h₃ : (⊤, y).1 ≠ ⊥ ∨ (⊤, y).2 ≠ 0
h₄ : (⊤, y).1 ≠ ⊤ ∨ (⊤, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, y)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun x' ↦ ⨆ i, f i x') x

Tactic:
by
  simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  rw [← nhdsWithin_univ] at bdd
  exact lowerSemicontinuousWithinAt_ciSup bdd h

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

Goal state before:
pp: α : Type u_1
ι : Sort u_2
s : Set α
m : ι → OuterMeasure α
⊢ (restrict s) (⨅ i, (restrict s) (m i)) = (restrict (range Subtype.val)) (⨅ i, (restrict s) (m i))

Tactic:
Subtype.range_coe

Goal state after:
α : Type u_1
ι : Sort u_2
s : Set α
m : ι → OuterMeasure α
⊢ (restrict s) (⨅ i, (restrict s) (m i)) = (restrict s) (⨅ i, (restrict s) (m i))
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ ∩ s₂)ᶜ

Tactic:
Set.compl_inter

Goal state after:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ᶜ ∪ s₂ᶜ)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ ∩ s₂)

Tactic:
rw [← isCaratheodory_compl_iff, Set.compl_inter]
  exact isCaratheodory_union _ (isCaratheodory_compl _ h₁) (isCaratheodory_compl _ h₂)

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

Goal state before:
pp: case pos
α : 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:
rw [extend_eq _ (PU h), congr_arg tsum _]

Goal state after:
case pos
α : 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)
⊢ m (⋃ i, s i) ⋯ ≤ tsum ?m.89

α : 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)
⊢ ℕ → ℝ≥0∞

α : 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)
⊢ (fun i ↦ extend m (s i)) = ?m.89
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ i, f i
⊢ (OuterMeasure.ofFunction m h₀) (t ∩ s) + (OuterMeasure.ofFunction m h₀) (t \ s) ≤ ∑' (i : ℕ), m (f i)

Tactic:
refine
    le_trans
      (add_le_add ((iInf_le_of_le fun i => f i ∩ s) <| iInf_le _ ?_)
        ((iInf_le_of_le fun i => f i \ s) <| iInf_le _ ?_))
      ?_

Goal state after:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ i, f i
⊢ t ∩ s ⊆ ⋃ i, (fun i ↦ f i ∩ s) i

case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ i, f i
⊢ t \ s ⊆ ⋃ i, (fun i ↦ f i \ s) i

case refine_3
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ i, f i
⊢ ∑' (i : ℕ), m ((fun i ↦ f i ∩ s) i) + ∑' (i : ℕ), m ((fun i ↦ f i \ s) i) ≤ ∑' (i : ℕ), m (f i)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ b, g b)
⊢ ∃ T f, t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
induction h_t with

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m = k
⊢ m ∈ S

Tactic:
rwa [hm]

Goal state after:
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)
f : δ ≃ δ'
⊢ ∀ (a : δ), Measurable fun x ↦ (Equiv.piCongrLeft π f).symm x a

Tactic:
exact fun i => measurable_pi_apply (f i)

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
⊢ comap Subtype.val (𝓝[>] a) = atBot

Tactic:
refine comap_coe_nhdsLT_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from hsa) ?_ ha.dual
  simpa only [OrderDual.exists, Ioo_toDual]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ∞
M : Set α → Set α := toMeasurable μ
H : ∀ (b : ι), M (t b) ∩ M (⋃ b, s b) =ᵐ[μ] M (t b)
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Tactic:
calc
    μ (⋃ b, t b) ≤ μ (⋃ b, M (t b)) := measure_mono (iUnion_mono fun b => subset_toMeasurable _ _)
    _ = μ (⋃ b, M (t b) ∩ M (⋃ b, s b)) :=
      measure_congr (Filter.EventuallyEq.countable_iUnion H).symm
    _ ≤ μ (M (⋃ b, s b)) := measure_mono (iUnion_subset fun b => inter_subset_right)
    _ = μ (⋃ b, s b) := measure_toMeasurable _

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
⊢ (sum fun n ↦ μ.restrict (disjointed (spanningSets ν) n)) = μ

Tactic:
by
  rw [← restrict_iUnion (disjoint_disjointed _)
      (MeasurableSet.disjointed (measurableSet_spanningSets _)),
    iUnion_disjointed, iUnion_spanningSets, restrict_univ]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ∞
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))

Tactic:
by
  refine .of_neBot_imp fun h ↦ ?_
  have := (atTop_neBot_iff.1 h).2
  rw [hm.measure_iInter hs hf]
  exact tendsto_atTop_iInf fun n m hnm => measure_mono <| hm hnm

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

Goal state before:
pp: case e_f
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ t ∈ measurableAtom '' s, MeasurableSet t
s' : ↑(measurableAtom '' s)
⊢ μ ↑s' = ν ↑s'

Tactic:
have hs' := s'.2

Goal state after:
case e_f
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ t ∈ measurableAtom '' s, MeasurableSet t
s' : ↑(measurableAtom '' s)
hs' : ↑s' ∈ measurableAtom '' s
⊢ μ ↑s' = ν ↑s'
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
⊢ μ = ν

Tactic:
by
  refine ext_of_generateFrom_of_cover h_gen hc h_inter hU htop ?_ fun t ht => h_eq t (h_sub ht)
  intro t ht s hs; rcases (s ∩ t).eq_empty_or_nonempty with H | H
  · simp only [H, measure_empty]
  · exact h_eq _ (h_inter _ hs _ (h_sub ht) H)

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

Goal state before:
pp: α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
⊢ c • μ {a | ¬p a} = 0

Tactic:
ae_iff.1 h,

Goal state after:
α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
⊢ c • 0 = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ NullMeasurableSet (t \ s) (μ.restrict s)

Tactic:
apply NullMeasurableSet.of_null

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ (μ.restrict s) (t \ s) = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)

Tactic:
apply ae_imp_of_ae_restrict

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
⊢ ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t' ↔ x ∈ t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ (ν₁.restrict (spanningSets μ i)) s = (ν₂.restrict (spanningSets μ i)) s

Tactic:
← ENNReal.add_right_inj (measure_mono s.inter_subset_right |>.trans_lt <|
    measure_spanningSets_lt_top μ i).ne

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ μ (s ∩ spanningSets μ i) + (ν₁.restrict (spanningSets μ i)) s =
    μ (s ∩ spanningSets μ i) + (ν₂.restrict (spanningSets μ i)) s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
s : Set α
hs : MeasurableSet s
μ : Measure α
⊢ μ.restrict (range Subtype.val) = μ.restrict s

Tactic:
Subtype.range_coe

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
s : Set α
hs : MeasurableSet s
μ : Measure α
⊢ μ.restrict s = μ.restrict s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
inst✝ : MeasureSpace α
s : Set α
hs : MeasurableSet s
⊢ volume.restrict (range Subtype.val) = volume.restrict s

Tactic:
Subtype.range_coe

Goal state after:
α : Type u_2
inst✝ : MeasureSpace α
s : Set α
hs : MeasurableSet s
⊢ volume.restrict s = volume.restrict s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
inst✝ : MeasureSpace α
s t : Set α
hs : NullMeasurableSet s volume
ht : MeasurableSet t
⊢ volume (t ∩ range fun a ↦ ↑a) = volume (t ∩ s)

Tactic:
Subtype.range_coe

Goal state after:
α : Type u_2
inst✝ : MeasureSpace α
s t : Set α
hs : NullMeasurableSet s volume
ht : MeasurableSet t
⊢ volume (t ∩ s) = volume (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ μ ((f ⁻¹' t ∩ s)ᶜ ∩ (0 ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0

Tactic:
Set.compl_inter

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ (0 ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0