mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(sign a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
_root_.sign_neg a_neg,

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(-1) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
g : α → ℝ≥0
hg : Summable g
i : α
hi : 0 < g i
⊢ 0 < ∑' (b : α), g b

Tactic:
by
  simpa using tsum_lt_tsum (fun a => zero_le) hi hg

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

Goal state before:
pp: case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(sign a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹

Tactic:
_root_.sign_neg a_neg,

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(-1) * ↑(↑a).abs⁻¹ = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
⊢ a * (b⁻¹ * c⁻¹) = a * (b * c)⁻¹

Tactic:
mul_inv

Goal state after:
a b c : EReal
⊢ a * (b⁻¹ * c⁻¹) = a * (b⁻¹ * c⁻¹)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
A : Type u_5
inst✝⁷ : Semifield 𝕜
inst✝⁶ : CharZero 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousSMul ℚ≥0 𝕜
inst✝³ : Semiring A
inst✝² : Algebra 𝕜 A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul 𝕜 A
⊢ Tendsto (⇑(algebraMap 𝕜 A) ∘ fun n ↦ (↑n)⁻¹) atTop (𝓝 0)

Tactic:
convert! (continuous_algebraMap 𝕜 A).continuousAt.tendsto.comp tendsto_inv_atTop_nhds_zero_nat

Goal state after:
𝕜 : Type u_4
A : Type u_5
inst✝⁷ : Semifield 𝕜
inst✝⁶ : CharZero 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousSMul ℚ≥0 𝕜
inst✝³ : Semiring A
inst✝² : Algebra 𝕜 A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul 𝕜 A
⊢ 0 = (algebraMap 𝕜 A) 0
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_4
G : Type u_5
inst✝ : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
⊢ (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x

Tactic:
filter_upwards [hg.le_comap <| preimage_mem_comap (m := g) (mem_principal_self {0}ᶜ)] with x hx

Goal state after:
α : Type u_4
G : Type u_5
inst✝ : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
x : α
hx : x ∈ g ⁻¹' {0}ᶜ
⊢ f x / g x * g x = f x
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
n : ℕ
⊢ m (f ⁻¹' (fun n ↦ (range f)ᶜ ∪ f '' t n) n) = m (t n)

Tactic:
simp [hf.preimage_image]

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ (comap f) (boundedBy m) = boundedBy fun s ↦ m (f '' s)

Tactic:
refine (comap_ofFunction _ ?_).trans ?_
  · refine h.imp (fun H s t hst => iSup_le fun hs => ?_) id
    have ht : t.Nonempty := hs.mono hst
    exact (@H ⟨s, hs⟩ ⟨t, ht⟩ hst).trans (le_iSup (fun _ : t.Nonempty => m t) ht)
  · dsimp only [boundedBy]
    congr with s : 1
    rw [image_nonempty]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S

Tactic:
simp [hs]

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 α
n : ℕ
⊢ ∑ i ∈ Finset.range n.succ, m (t ∩ s i) = m (t ∩ ⋃ i, ⋃ (_ : i < n.succ), s i)

Tactic:
by
    rw [biUnion_lt_succ, Finset.sum_range_succ, Set.union_comm, isCaratheodory_sum h hd,
      m.measure_inter_union _ (h n), add_comm]
    intro a
    simpa using fun (h₁ : a ∈ s n) i (hi : i < n) h₂ => (hd (ne_of_gt hi)).le_bot ⟨h₁, h₂⟩

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
⊢ MeasurableSpace α

Tactic:
apply MeasurableSpace.DynkinSystem.toMeasurableSpace (caratheodoryDynkin m)
  intro s₁ s₂
  apply isCaratheodory_inter

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
rcases h with hs | hs
    · refine ⟨{i}, ?_, fun _ => s, ⟨fun x hx => ?_, ?_⟩⟩
      · rw [Finset.coe_singleton]
      · rw [Finset.mem_singleton] at hx
        rwa [hx]
      · simp only [Finset.mem_singleton, iInter_iInter_eq_left]
    · refine ⟨∅, ?_⟩
      simpa only [Finset.coe_empty, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff,
        imp_true_iff, Finset.notMem_empty, iInter_false, iInter_univ, true_and,
        exists_const] using! hs

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ \ s₂)ᶜ

Tactic:
simp only [sdiff_eq, compl_inter, compl_compl]

Goal state after:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ᶜ ∪ s₂)
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
hf_eq : ∀ (i : ι), ∀ᵐ (x : α) ∂μ, f i x = AEMeasurable.mk (f i) ⋯ x
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n ↦ f n x}ᶜ = 0

Tactic:
← ae_all_iff

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
hf_eq : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) ⋯ a
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n ↦ f n x}ᶜ = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (f '' s)

Tactic:
hf.measurableSet_image

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set β
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (f '' f ⁻¹' s)

Tactic:
hf.measurableSet_image

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set β
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (f ⁻¹' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (f '' s)

Tactic:
hf.measurableSet_image

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
⊢ MeasurableSet (⇑e.symm ⁻¹' s) ↔ MeasurableSet s

Tactic:
measurableSet_preimage

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
⊢ MeasurableSet s ↔ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
⊢ map f μ = map g μ

Tactic:
by
  by_cases hf : AEMeasurable f μ
  · have hg : AEMeasurable g μ := hf.congr h
    simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hg]
    exact
      mapₗ_congr hf.measurable_mk hg.measurable_mk (hf.ae_eq_mk.symm.trans (h.trans hg.ae_eq_mk))
  · have hg : ¬AEMeasurable g μ := by simpa [← aemeasurable_congr h] using hf
    simp [map_of_not_aemeasurable, hf, hg]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : NullMeasurableSet s₂ μ
h_fin : μ s₂ ≠ ∞
⊢ μ (s₁ ∪ s₂) - μ s₂ = μ s₁ - μ s₂

Tactic:
union_eq_self_of_subset_right h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : NullMeasurableSet s₂ μ
h_fin : μ s₂ ≠ ∞
⊢ μ s₁ - μ s₂ = μ s₁ - μ s₂
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
simp [hs]

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) ≠ ∞
h : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))

Tactic:
hm.measure_iInter hs hf

Goal state after:
α : 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) ≠ ∞
h : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (⨅ i, μ (s i)))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ∞
hfem : ⋂ n, f n = ∅
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Tactic:
let F m := μ (⋂ n ≤ m, f n)

Goal state after:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ∞
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m ↦ μ (⋂ n, ⋂ (_ : n ≤ m), f n)
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ᵐ (a : α) ∂μ.restrict s, a ∈ s
p : α → Prop
hp : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∃ x ∈ s, p x

Tactic:
exact (hs.and_eventually hp).exists

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

Goal state before:
pp: case h₁
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
w : ℕ → Set α := ⋯
T : t ⊆ ⋂ n, w n
M : MeasurableSet (⋂ n, w n)
u : Set α
hu : MeasurableSet u
i : ℕ
⊢ ⋂ n, w n ⊆ w i

Tactic:
apply iInter_subset

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

Goal state before:
pp: α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
s : Set α
hs : MeasurableSet s
⊢ (OuterMeasure.toMeasure 0 h) s = 0 s

Tactic:
simp [hs]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (μ.trim ⋯) (f ⁻¹' s) = (Measure.map f μ) s

Tactic:
by
  rw [← map_trim_comap hf, Measure.map_apply (Measurable.of_comap_le le_rfl) hs]

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

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ∞
h_eq : ∀ s ∈ C, μ s = ν s
i : ℕ
⊢ B i ∈ C

Tactic:
apply h2B

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
⊢ (sum μ).restrict s = sum fun i ↦ (μ i).restrict s

Tactic:
by
  ext t ht
  simp_rw [sum_apply _ ht, restrict_apply ht, sum_apply_of_countable]

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

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
⊢ ⋃₀ memPartition f (n + 1) = univ

Tactic:
rw [memPartition_succ]

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
⊢ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} = univ
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ (memPartition f (n + 1)).Finite

Tactic:
rw [memPartition_succ]

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}.Finite
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:
refine (measure_inter_eq_of_measure_eq hs ?_ (subset_toMeasurable _ _) ?_).symm

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

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ μ t ≠ ∞
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
rcases exists_nonempty_countable_separating α hp t with ⟨S, hSne, hSc, hS⟩

Goal state after:
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : Set (Set α)
hSne : S.Nonempty
hSc : S.Countable
hS : (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
by
  rw [OuterMeasure.sInf_eq_boundedBy_sInfGen]
  refine OuterMeasure.boundedBy_caratheodory fun t => ?_
  simp only [OuterMeasure.sInfGen, le_iInf_iff, forall_mem_image, measure_eq_iInf t,
    coe_toOuterMeasure]
  intro μ hμ u htu _hu
  have hm : ∀ {s t}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t := by
    intro s t hst
    rw [OuterMeasure.sInfGen_def, iInf_image]
    exact iInf₂_le_of_le μ hμ <| measure_mono hst
  rw [← measure_inter_add_sdiff u hs]
  exact add_le_add (hm <| inter_subset_inter_left _ htu) (hm <| sdiff_subset_sdiff_left htu)

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

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

Tactic:
← restrict_toMeasurable_of_sFinite s,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ ⨆ i, (μ.restrict (toMeasurable μ s)) (spanningSets μ i) = ⨆ i, μ (toMeasurable μ s ∩ spanningSets μ i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case pos
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : univ = ∅
⊢ μ univ < ∞

Tactic:
rw [h_univ_empty, measure_empty]

Goal state after:
case pos
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : univ = ∅
⊢ 0 < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
⊢ ∀ (i : ℕ), s i = ∅

Tactic:
simpa [h_not_univ] using hs_meas

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

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
rw [mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs]
    exact id

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
s : (y : α) → x ≠ y → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
y : α
⊢ y ∈ {x} ↔ y ∈ ⋂ b, ⋂ (b_1 : x ≠ b), s b b_1

Tactic:
rcases eq_or_ne x y with rfl | h

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
s : (y : α) → x ≠ y → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
⊢ x ∈ {x} ↔ x ∈ ⋂ b, ⋂ (b_1 : x ≠ b), s b b_1

case inr
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
s : (y : α) → x ≠ y → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
y : α
h : x ≠ y
⊢ y ∈ {x} ↔ y ∈ ⋂ b, ⋂ (b_1 : x ≠ b), s b b_1
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν✝ : Measure α
s t : Set α
a : α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ SigmaFinite (μ + ν)

Tactic:
rw [← sum_cond]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν✝ : Measure α
s t : Set α
a : α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ SigmaFinite (sum fun b ↦ bif b then μ else ν)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s \ t n ∈ memPartition t (n + 1)

Tactic:
rw [memPartition_succ]

Goal state after:
case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s \ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n ∈ memPartition t (n + 1)

Tactic:
rw [memPartition_succ]

Goal state after:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ v ∩ t n ∈ memPartition t (n + 1)

Tactic:
rw [memPartition_succ]

Goal state after:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ v ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0

Tactic:
simp [hs]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
μ ν : ι → Measure α
⊢ sum μ + sum ν = sum fun n ↦ μ n + ν n

Tactic:
ext1 s hs
  simp only [add_apply, sum_apply _ hs,
    ENNReal.summable.tsum_add ENNReal.summable]

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
⊢ y ⤳ x

Tactic:
specializes_iff_forall_closed

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
⊢ ∀ (s : Set X), IsClosed[inst✝²] s → y ∈ s → x ∈ s
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul G
inst✝ : MeasurableInv G
c : G
⊢ Measurable fun x ↦ x / c

Tactic:
convert! measurable_id.mul_const c⁻¹ using 1

Goal state after:
α : Type u_1
G : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul G
inst✝ : MeasurableInv G
c : G
⊢ (fun x ↦ x / c) = fun x ↦ id x * c⁻¹
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
⊢ Disjoint (closedEBall x r) s

Tactic:
rw [disjoint_left]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
⊢ ∀ ⦃a : α⦄, a ∈ closedEBall x r → a ∉ s
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
s : Set α
t : Set β
⊢ ⨅ y ∈ s ×ˢ t, edist x y = max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y)

Tactic:
Prod.edist_eq,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
s : Set α
t : Set β
⊢ ⨅ y ∈ s ×ˢ t, max (edist x.1 y.1) (edist x.2 y.2) = max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: case h₂
α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst✝³] t
⊢ MeasurableSet (g ⁻¹' t \ s)

Tactic:
rcases _root_.continuousOn_iff'.1 hg t ht with ⟨u, u_open, hu⟩
    rw [sdiff_eq_compl_inter, inter_comm, hu]
    exact u_open.measurableSet.inter hs.compl

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

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

Tactic:
by
  simp

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

Goal state before:
pp: δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ

Tactic:
have key_iff : ∀ z : X, edist x z < ENNReal.ofReal δ ↔ dist x z < δ := fun z ↦ by
    rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]

Goal state after:
δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x : X
key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ
⊢ x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ