mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ UpperHemicontinuousWithinAt f s x ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
rw [UpperHemicontinuousWithinAt, semicontinuousWithinAt_iff_frequently, compl_surjective.forall]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (x_1 : Set β), (∃ᶠ (x' : α) in 𝓝[s] x, x_1ᶜ ∉ 𝓝ˢ (f x')) → x_1ᶜ ∉ 𝓝ˢ (f x)) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
β : Type u_4
f : α → ℝ
hf : Summable f
hn : ∀ (a : α), 0 ≤ f a
i : β → α
hi : Injective i
⊢ tsum (f ∘ i) ≤ tsum f

Tactic:
lift f to α → ℝ≥0 using hn
  rw [NNReal.summable_coe] at hf
  simpa only [Function.comp_def, ← NNReal.coe_tsum] using! NNReal.tsum_comp_le_tsum_of_inj hf hi

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
x : α
hx : x ∈ s
⊢ {x_1 | (fun y ↦ f y ≤ f x) x_1} ∈ φ (f ↑⟨x, hx⟩)

Tactic:
by apply inter_subset_right

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
⊢ ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x

pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
x✝ : ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
u : Finset ↑I
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅

Tactic:
· suffices ∀ i ∈ I, IsClosed (s ↓∩ (fun i ↦ f i ⁻¹' Iic c) i) by
      simpa [Set.eq_empty_iff_forall_notMem] using
        ks.elim_finite_subfamily_isClosed_subtype _ this H
    exact fun i hi ↦ lowerSemicontinuous_restrict_iff.mpr (hfi i hi) |>.isClosed_preimage c

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
x✝ : ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
u : Finset ↑I
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (liminf_le_iff).2 fun c c_ab ↦ ?_

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > liminf v f
c : EReal
c_ab : c > a * b
⊢ ∃ᶠ (a : α) in f, (u * v) a < c
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
H : Monotone fun s ↦ m ↑s
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
⊢ m s ≤ (fun s ↦ ⨆ (_ : s.Nonempty), m s) t

Tactic:
have ht : t.Nonempty := hs.mono hst

Goal state after:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
H : Monotone fun s ↦ m ↑s
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
ht : t.Nonempty
⊢ m s ≤ (fun s ↦ ⨆ (_ : s.Nonempty), m s) t
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

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

Tactic:
· refine le_sInf ?_
    intro μ hμ t
    exact le_trans (boundedBy_le t) (iInf₂_le μ hμ)

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 : ι
⊢ ↑(δ' i) / ↑(max 1 (w i)) ≤ ↑(δ' i) / (fun i ↦ ↑(w i)) i

Tactic:
grw [← le_max_right]

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case succ
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
n : ℕ
hn : ∃ m, s m ⊆ dissipate s n
⊢ ∃ m, s m ⊆ dissipate s (n + 1)

Tactic:
obtain ⟨m, hm⟩ := hn
    obtain ⟨k, hk⟩ := hd m (n + 1)
    exact ⟨k, by simp; grind⟩

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

Goal state before:
pp: α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
x✝ : MeasurableSet s
t : Set α
hs₁ : s ∈ (fun m ↦ {t | MeasurableSet t}) m₁.caratheodory
hs₂ : s ∈ (fun m ↦ {t | MeasurableSet t}) m₂.caratheodory
⊢ (m₁ + m₂) t = (m₁ + m₂) (t ∩ s) + (m₁ + m₂) (t \ s)

Tactic:
simp [hs₁ t, hs₂ t, add_left_comm, add_assoc]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mp
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ f ⟨a_1, b⟩
b : β
h_b : b ∈ s
⊢ ⟨b, h_b⟩ ∈ T → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨b, h_b⟩

Tactic:
h_b_in_T

Goal state after:
case refine_1.mp
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ f ⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨b, h_b⟩
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨a_1, b⟩
b : β
h_b : b ∈ s
⊢ ⟨b, h_b⟩ ∈ T → a ∈ f ⟨b, h_b⟩

Tactic:
h_b_in_T

Goal state after:
case refine_1.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ f ⟨b, h_b⟩
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ f i ∈ π i ∨ f i ∈ {univ}

Tactic:
exact Or.inl (hfπ i hi)

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → x ∈ t) ↔ μ (s \ t) = 0

Tactic:
simp [ae_iff]; rfl

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

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

Tactic:
obtain rfl | h := le_succ_iff_eq_or_le.1 hm

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap (compl ∘ f) inferInstance = MeasurableSpace.comap f inferInstance

Tactic:
← MeasurableSpace.comap_comp

Goal state after:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap f (MeasurableSpace.comap compl inferInstance) = MeasurableSpace.comap f inferInstance
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
h : μ s = μ t
hfin : μ (s ∩ t) ≠ ∞
⊢ μ (s \ t) = μ (t \ s)

Tactic:
by
  rw [← ENNReal.add_right_inj hfin, measure_inter_add_sdiff₀ _ ht, inter_comm,
    measure_inter_add_sdiff₀ _ hs, h]

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

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

Tactic:
by
  simp_rw [← measure_univ_eq_zero, map_apply_of_aemeasurable hf .univ, preimage_univ]

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

Goal state before:
pp: α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : ν s = 0
⊢ (c • μ) s = 0

Tactic:
simp only [h hνs, smul_apply, smul_zero, ← smul_one_smul ℝ≥0∞ c (0 : ℝ≥0∞)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
hs : s.Countable
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ ∑' (b : ↑s), μ (f ⁻¹' {↑b}) = μ (⋃ y ∈ s, f ⁻¹' {y})

Tactic:
measure_biUnion hs (pairwiseDisjoint_fiber f s) hf

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
hs : s.Countable
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ ∑' (b : ↑s), μ (f ⁻¹' {↑b}) = ∑' (p : ↑s), μ (f ⁻¹' {↑p})
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ (fun x ↦ if x ∈ s then f x else g x) =ᵐ[μ] g

Tactic:
refine measure_mono_null ?_ hs_zero

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ {x | (fun x ↦ (fun x ↦ if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ s
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 = ∅
F : ι → ℝ≥0∞ := fun m ↦ μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : Tendsto F atTop (𝓝 0)
x✝ : Nonempty ι := Exists.nonempty hfin
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Tactic:
rw [ENNReal.tendsto_atTop_zero_iff_lt_of_antitone hFAnti] at this

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)
hFAnti : Antitone F
this : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, F n < ε
x✝ : Nonempty ι := Exists.nonempty hfin
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
simp [union_eq_iUnion, iSup_bool_eq]

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

Goal state before:
pp: case inr
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : {x}.Subsingleton
htl : {x} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
· exact ⟨x, hts rfl, htl⟩

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) ≠ ∞
⊢ μ (toMeasurable μ t ∩ s) = μ (t ∩ s)

Tactic:
have A : ∃ t', t' ⊇ t ∧ MeasurableSet t' ∧ ∀ u, MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u) := by
    let w n := toMeasurable μ (t ∩ v n)
    have hw : ∀ n, μ (w n) < ∞ := by
      intro n
      simp_rw [w, measure_toMeasurable]
      exact (h'v n).lt_top
    set t' := ⋃ n, toMeasurable μ (t ∩ disjointed w n) with ht'
    have tt' : t ⊆ t' :=
      calc
        t ⊆ ⋃ n, t ∩ disjointed w n := by
          rw [← inter_iUnion, iUnion_disjointed, inter_iUnion]
          intro x hx
          rcases mem_iUnion.1 (hv hx) with ⟨n, hn⟩
          refine mem_iUnion.2 ⟨n, ?_⟩
          have : x ∈ t ∩ v n := ⟨hx, hn⟩
          exact ⟨hx, subset_toMeasurable μ _ this⟩
        _ ⊆ ⋃ n, toMeasurable μ (t ∩ disjointed w n) :=
          iUnion_mono fun n => subset_toMeasurable _ _
    refine ⟨t', tt', MeasurableSet.iUnion fun n => measurableSet_toMeasurable μ _, fun u hu => ?_⟩
    apply le_antisymm _ (by gcongr)
    calc
      μ (t' ∩ u) ≤ ∑' n, μ (toMeasurable μ (t ∩ disjointed w n) ∩ u) := by
        rw [ht', iUnion_inter]
        exact measure_iUnion_le _
      _ = ∑' n, μ (t ∩ disjointed w n ∩ u) := by
        congr 1
        ext1 n
        apply measure_toMeasurable_inter hu
        apply ne_of_lt
        calc
          μ (t ∩ disjointed w n) ≤ μ (t ∩ w n) := by
            gcongr
            exact disjointed_le w n
          _ ≤ μ (w n) := measure_mono inter_subset_right
          _ < ∞ := hw n
      _ = ∑' n, μ.restrict (t ∩ u) (disjointed w n) := by
        congr 1
        ext1 n
        rw [restrict_apply, inter_comm t _, inter_assoc]
        refine MeasurableSet.disjointed (fun n => ?_) n
        exact measurableSet_toMeasurable _ _
      _ = μ.restrict (t ∩ u) (⋃ n, disjointed w n) := by
        rw [measure_iUnion]
        · exact disjoint_disjointed _
        · intro i
          refine MeasurableSet.disjointed (fun n => ?_) i
          exact measurableSet_toMeasurable _ _
      _ ≤ μ.restrict (t ∩ u) univ := measure_mono (subset_univ _)
      _ = μ (t ∩ u) := by rw [restrict_apply MeasurableSet.univ, univ_inter]
  -- thanks to the definition of `toMeasurable`, the previous property will also be shared
  -- by `toMeasurable μ t`, which is enough to conclude the proof.
  rw [toMeasurable]
  split_ifs with ht
  · apply measure_congr
    exact ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)
  · exact A.choose_spec.2.2 s hs

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 (spanningSets μ i)) s = μ s

Tactic:
rw [← measure_toMeasurable s,
    ← iSup_restrict_spanningSets_of_measurableSet (measurableSet_toMeasurable _ _)]

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

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
p : ℕ → Prop
hpn : p n
hpx : x ∈ countablyGeneratedAtom α p
⊢ x ∈ natGeneratingSequence α n

Tactic:
simp only [countablyGeneratedAtom, mem_iInter] at hpx

Goal state after:
case refine_1.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
p : ℕ → Prop
hpn : p n
hpx : ∀ (i : ℕ), x ∈ if p i then natGeneratingSequence α i else (natGeneratingSequence α i)ᶜ
⊢ x ∈ natGeneratingSequence α n
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : Nonempty α
f : ℕ → α
hf : Surjective f
⊢ ∀ (i : ℕ), μ {f i} < ∞

Tactic:
by simpa [hf.forall] using hμ

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

pp: case neg
α : 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]
    exact ENNReal.zero_ne_top.lt_top

Goal state after:
case neg
α : 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 < ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ x = y

Tactic:
exact separatesPoints_def <| fun _ hs ↦ (hxy _ hs).mp

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

Goal state before:
pp: case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ MeasurableSet s

Tactic:
hS_eq,

Goal state after:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ MeasurableSet (⋃₀ ↑S)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (range t)

Tactic:
conv_rhs => rw [← generateFrom_iUnion_memPartition t]

Goal state after:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (⋃ n, memPartition t n)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g

Tactic:
by
  classical
  let s : Set α := toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ
  let g : α → β := piecewise s (fun _ => h₀.some) (H.mk f)
  refine ⟨g, ?_, ?_, ?_⟩
  · exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk
  · rintro _ ⟨x, rfl⟩
    by_cases hx : x ∈ s
    · simpa [g, hx] using h₀.some_mem
    · simp only [g, hx, piecewise_eq_of_notMem, not_false_iff]
      contrapose hx
      apply subset_toMeasurable
      simp +contextual only [hx, mem_compl_iff, mem_ofPred_eq, not_and,
        not_false_iff, imp_true_iff]
  · have A : μ (toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ) = 0 := by
      rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
      exact H.ae_eq_mk.and ht
    filter_upwards [compl_mem_ae_iff.2 A] with x hx
    rw [mem_compl_iff] at hx
    simp only [s, g, hx, piecewise_eq_of_notMem, not_false_iff]
    contrapose! hx
    apply subset_toMeasurable
    simp only [hx, mem_compl_iff, mem_ofPred_eq, false_and, not_false_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α : Type u_1
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℤ
⊢ Measurable fun x ↦ (x, n).1 ^ (x, n).2

Tactic:
by
      rcases n with n | n
      · simp_rw [Int.ofNat_eq_natCast, zpow_natCast]
        exact measurable_id.pow_const _
      · simp_rw [zpow_negSucc]
        exact (measurable_id.pow_const (n + 1)).inv

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
M : Type u_2
α : Type u_3
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : SMul M α
inst✝² : SMul Mᵐᵒᵖ α
inst✝¹ : IsCentralScalar M α
inst✝ : MeasurableSMul₂ M α
⊢ Measurable fun x ↦ MulOpposite.op (unop x.1) • x.2

Tactic:
simp_rw [op_smul_eq_smul]
      exact (measurable_mul_unop.comp measurable_fst).smul measurable_snd

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ thickening δ E

Tactic:
rw [← cthickening_zero]
  exact cthickening_subset_thickening' δ_pos δ_pos E

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

Goal state before:
pp: ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
by_cases hs : IsBounded s
  · exact (diam_mono (thickening_subset_cthickening _ _) hs.cthickening).trans
      (diam_cthickening_le _ hε)
  obtain rfl | hε := hε.eq_or_lt
  · simp [thickening_of_nonpos, diam_nonneg]
  · rw [diam_eq_zero_of_unbounded (mt (IsBounded.subset · <| self_subset_thickening hε _) hs)]
    positivity

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
⊢ cthickening ε (cthickening δ s) ⊆ cthickening (ε + δ) s

Tactic:
intro x
  simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]
  exact fun hx => infEDist_le_infEDist_cthickening_add.trans (by grw [hx])

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : ¬f b = 0
⊢ f b * μ (⇑(f.restrict s) ⁻¹' {f b}) = f b * μ (⇑f ⁻¹' {f b} ∩ s)

Tactic:
rw [restrict_preimage_singleton _ hs hb, inter_comm]

Goal state after: