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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
⊢ FrechetUrysohnSpace X

Tactic:
refine ⟨fun s x hx ↦ ?_⟩
  rw [hf.closure_eq_preimage_closure_image, mem_preimage, mem_closure_iff_seq_limit] at hx
  rcases hx with ⟨u, hus, hu⟩
  choose v hv hvu using hus
  refine ⟨v, hv, ?_⟩
  simpa only [hf.tendsto_nhds_iff, Function.comp_def, hvu]

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

Goal state before:
pp: α : Type u_4
l : Filter α
x : ℝ≥0
f : ℝ≥0∞ → α
⊢ Tendsto f (𝓝 ↑x) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l

Tactic:
rw [nhds_coe, tendsto_map'_iff]

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

Goal state before:
pp: a : ℝ≥0
⊢ Tendsto ENNReal.toNNReal (𝓝 ↑a) (𝓝 (↑a).toNNReal)

Tactic:
rw [nhds_coe, tendsto_map'_iff]

Goal state after:
a : ℝ≥0
⊢ Tendsto (ENNReal.toNNReal ∘ ofNNReal) (𝓝 a) (𝓝 (↑a).toNNReal)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y y')

Tactic:
by rw [edist_comm y y']; abel

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

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ liminf (f + g) u ≤ liminf f u

Tactic:
refine liminf_le_of_le (by isBoundedDefault) fun b hb ↦ ?_

Goal state after:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
⊢ b ≤ liminf f u
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
⊢ liminf (g + f) u = liminf g u

Tactic:
liminf_add_of_right_tendsto_zero hf

Goal state after:
ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
⊢ liminf g u = liminf g u
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
⊢ limsup (f + g) u ≤ b

Tactic:
Filter.limsup_le_iff'

Goal state after:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
⊢ ∀ y > b, ∀ᶠ (a : ι) in u, (f + g) a ≤ y
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: a : ℝ≥0
b : ℝ≥0∞
⊢ (a • b).toNNReal = a * b.toNNReal

Tactic:
by
  change ((a : ℝ≥0∞) * b).toNNReal = a * b.toNNReal
  simp only [ENNReal.toNNReal_mul, ENNReal.toNNReal_coe]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ ¬BoundedSpace E

Tactic:
← isBounded_univ

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ ¬Bornology.IsBounded univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
⊢ measurableAtom x ⊆ measurableAtom y

Tactic:
by
  intro z hz
  simp only [measurableAtom, mem_iInter] at hz hx ⊢
  exact fun s hys hs ↦ hz s (hx s hys hs) hs

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

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y z : β
hx : x ∉ measurableAtom x
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
⊢ False

Tactic:
exact hx (mem_measurableAtom_self x)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
⊢ MeasurableSet (Sum.inl '' s) ↔ MeasurableSet s

Tactic:
by
  simp [measurableSet_sum_iff, Sum.inl_injective.preimage_image]

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

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

Tactic:
cases h₂ (h₁.trans_le h)

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

Goal state before:
pp: case mp
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ x = y

Tactic:
rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]

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

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

Tactic:
by
  simp +contextual [SemicontinuousWithinAt]

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

Goal state before:
pp: a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
⊢ a / (b * c) * c = a / b

Tactic:
← div_div a b c,

Goal state after:
a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
⊢ a / b / c * c = a / b
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
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
x✝ : (𝓝 a ⊓ ℱ).NeBot := h
this : ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
⊢ False

Tactic:
rwa [eventually_const] at this

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

Goal state before:
pp: a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto toReal (𝓝 ↑a) (𝓝 (↑a).toReal)

Tactic:
rw [nhds_coe, tendsto_map'_iff]

Goal state after:
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a).toReal)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ 0 ≤ 2 * max (x + 1) 0

Tactic:
simp only [Nat.ofNat_pos, mul_nonneg_iff_of_pos_left, le_max_iff, le_refl, or_true]

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
n : ℕ
i : ι
⊢ f '' f ⁻¹' (fun n ↦ f '' t n ∪ (range f)ᶜ) n ⊆ f '' t n

Tactic:
simpa only [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      image_subset_iff] using subset_rfl

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
ι : Type u_4
γ : Type u_5
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : LinearOrder γ
inst✝³ : IsOrderedAddMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) univ x
⊢ UpperSemicontinuousWithinAt (fun z ↦ ∑ i ∈ a, f i z) univ x

Tactic:
exact upperSemicontinuousWithinAt_sum ha

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

Goal state before:
pp: R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ Tendsto (fun x ↦ ↑⌈a * x⌉₊ / x) atTop (𝓝 a)

Tactic:
have A : Tendsto (fun x : R ↦ a + x⁻¹) atTop (𝓝 (a + 0)) :=
    tendsto_const_nhds.add tendsto_inv_atTop_zero
  rw [add_zero] at A
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds A
  · refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    rw [le_div_iff₀ (zero_lt_one.trans_le hx)]
    exact Nat.le_ceil _
  · refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    simp [div_le_iff₀ (zero_lt_one.trans_le hx), inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne',
      (Nat.ceil_lt_add_one (mul_nonneg ha (zero_le_one.trans hx))).le, add_mul]

Goal state after:
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:
← isCaratheodory_compl_iff,

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_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ ∀ (t : Set α),
    (OuterMeasure.ofFunction m h₀) (t ∩ s) + (OuterMeasure.ofFunction m h₀) (t \ s) ≤ (OuterMeasure.ofFunction m h₀) t

Tactic:
refine fun t => le_iInf fun f => le_iInf fun hf => ?_

Goal state after:
α : 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)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ {t | ∃ k ∈ S, s k = t} ⊆ piiUnionInter (fun k ↦ {s k}) S

Tactic:
rintro _ ⟨k, hk, rfl⟩

Goal state after:
case refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k ∈ piiUnionInter (fun k ↦ {s k}) S
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
inst✝ : Countable α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), μ {x} ≠ 0 → p x

Tactic:
by
  rw [ae_iff, measure_null_iff_singleton]
  exacts [forall_congr' fun _ ↦ not_imp_comm, Set.to_countable _]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
⊢ d.Has (tᶜ ∩ s)

Tactic:
by
    have : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ := Set.ext fun x => by by_cases h : x ∈ s <;> simp [h]
    simp_rw [this]
    exact
      d.has_sdiff (d.has_compl hts) (d.has_compl h)
        (compl_subset_compl.mpr inter_subset_right)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ ofMeasurableSpace ((generate s).toMeasurableSpace ⋯) ≤ ofMeasurableSpace (generateFrom s)

Tactic:
rw [ofMeasurableSpace_toMeasurableSpace]
      exact generate_le _ fun t ht => measurableSet_generateFrom ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : f.IsMeasurablyGenerated
inst✝ : g.IsMeasurablyGenerated
⊢ (f ⊓ g).IsMeasurablyGenerated

Tactic:
by
  constructor
  rintro t ⟨sf, hsf, sg, hsg, rfl⟩
  rcases IsMeasurablyGenerated.exists_measurable_subset hsf with ⟨s'f, hs'f, hmf, hs'sf⟩
  rcases IsMeasurablyGenerated.exists_measurable_subset hsg with ⟨s'g, hs'g, hmg, hs'sg⟩
  refine ⟨s'f ∩ s'g, inter_mem_inf hs'f hs'g, hmf.inter hmg, ?_⟩
  exact inter_subset_inter hs'sf hs'sg

Goal state after:
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 (g '' f '' s)

Tactic:
hg.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 (f '' s)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt :
  ∀ (i : Option (PLift ι)),
    (Option.elim' (⨆ i, μ i.down) (μ ∘ PLift.down) i) t = (Option.elim' (⨆ i, μ i.down) (μ ∘ PLift.down) i).trim s
⊢ (⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s

Tactic:
simp only [Option.forall, Option.elim'] at hμt

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt : (⨆ i, μ i.down) t = (⨆ i, μ i.down).trim s ∧ ∀ (x : PLift ι), ((μ ∘ PLift.down) x) t = ((μ ∘ PLift.down) x).trim s
⊢ (⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s
Module: Mathlib.Order.Interval.Set.Monotone

Goal state before:
pp: case pos
α : 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:
rw [succ_eq_iff_isMax.2 hk] at hm

Goal state after:
case pos
α : 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 ≤ k
hk : IsMax k
⊢ m ≤ φ m
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
⊢ map f 0 = 0

Tactic:
by_cases hf : AEMeasurable f (0 : Measure α) <;> simp [map, hf]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ ν s = 0 → μ s = 0

Tactic:
rw [measure_eq_zero_iff_ae_notMem, 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.Comap

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : ¬Injective f
⊢ comap f (comap g μ) = comap (g ∘ f) μ

Tactic:
· rw [comap, dif_neg <| mt And.left hf, comap, dif_neg fun h ↦ hf h.1.of_comp]

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

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
i : ι
⊢ IsFiniteMeasure (Function.extend f m 0 (f i))

Tactic:
rw [hf.extend_apply]

Goal state after:
case inl
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
i : ι
⊢ IsFiniteMeasure (m i)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun x1 x2 ↦ x1 ⊆ x2) on s) t
⊢ μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)

Tactic:
have := ht.to_subtype

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun x1 x2 ↦ x1 ⊆ x2) on s) t
this : Countable ↑t
⊢ μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ∞
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
refine le_antisymm (le_iInf fun i ↦ measure_mono <| iInter_subset _ _) ?_
  have := hfin.nonempty
  rcases exists_seq_antitone_tendsto_atTop_atBot ι with ⟨x, hxm, hx⟩
  calc
    ⨅ i, μ (s i) ≤ ⨅ n, μ (s (x n)) := le_iInf_comp (μ ∘ s) x
    _ = μ (⋂ n, s (x n)) := by
      refine .symm <| (hs.comp_antitone hxm).directed_ge.measure_iInter (fun n ↦ hsm _) ?_
      rcases hfin with ⟨k, hk⟩
      rcases (hx.eventually_le_atBot k).exists with ⟨n, hn⟩
      exact ⟨n, ne_top_of_le_ne_top hk <| measure_mono <| hs hn⟩
    _ ≤ μ (⋂ i, s i) := by
      refine measure_mono <| iInter_mono' fun i ↦ ?_
      rcases (hx.eventually_le_atBot i).exists with ⟨n, hn⟩
      exact ⟨n, hs hn⟩

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

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

Tactic:
by
  refine ⟨fun h ↦ ⟨restrict_congr_mono subset_union_left h,
    restrict_congr_mono subset_union_right h⟩, ?_⟩
  rintro ⟨hs, ht⟩
  ext1 u hu
  simp only [restrict_apply hu, inter_union_distrib_left]
  rcases exists_measurable_superset₂ μ ν (u ∩ s) with ⟨US, hsub, hm, hμ, hν⟩
  calc
    μ (u ∩ s ∪ u ∩ t) = μ (US ∪ u ∩ t) :=
      measure_union_congr_of_subset hsub hμ.le Subset.rfl le_rfl
    _ = μ US + μ ((u ∩ t) \ US) := (measure_add_sdiff hm.nullMeasurableSet _).symm
    _ = restrict μ s u + restrict μ t (u \ US) := by
      simp only [restrict_apply, hu, hu.diff hm, hμ, ← inter_comm t, inter_sdiff_assoc]
    _ = restrict ν s u + restrict ν t (u \ US) := by rw [hs, ht]
    _ = ν US + ν ((u ∩ t) \ US) := by
      simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_sdiff_assoc]
    _ = ν (US ∪ u ∩ t) := measure_add_sdiff hm.nullMeasurableSet _
    _ = ν (u ∩ s ∪ u ∩ t) := .symm <| measure_union_congr_of_subset hsub hν.le Subset.rfl le_rfl

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

Goal state before:
pp: α : 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
t : Set α
ht : t ∈ measurableAtom '' s
⊢ MeasurableSet t

Tactic:
obtain ⟨x, hxs, hx⟩ := ht

Goal state after:
α : 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
t : Set α
x : α
hxs : x ∈ s
hx : measurableAtom x = t
⊢ MeasurableSet t
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Tactic:
have := ht.to_subtype

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable ↑t
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))
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 : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)

Tactic:
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)

Goal state after:
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 μ
s : Set α
⊢ SigmaFinite (μ.restrict s)

Tactic:
refine ⟨⟨⟨spanningSets μ, fun _ => trivial, fun i => ?_, iUnion_spanningSets μ⟩⟩⟩
  rw [Measure.restrict_apply (measurableSet_spanningSets μ i)]
  exact (measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ i)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : SeparatesPoints α
x y : α
h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s
⊢ x = y

Tactic:
exact separatesPoints_def h

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

Goal state before:
pp: α : 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)
x : α
x✝ : x ∈ (⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ) ∩ s
hx₁ : x ∈ ⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ
hx₂ : x ∈ s
i : ℕ
hi : x ∈ t' i
h : i ∉ {k | ν (t' k) < μ (t' k)}
⊢ False

Tactic:
simp only [mem_ofPred_eq, not_lt] at h

Goal state after:
α : 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)
x : α
x✝ : x ∈ (⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ) ∩ s
hx₁ : x ∈ ⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ
hx₂ : x ∈ s
i : ℕ
hi : x ∈ t' i
h : μ (t' i) ≤ ν (t' i)
⊢ False
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
n : ℕ
⊢ (Measure.map f μ) (f '' spanningSets μ n ∪ (range f)ᶜ) < ∞

Tactic:
rw [hf.map_apply, Set.preimage_union]
    simp only [Set.preimage_compl, Set.preimage_range, Set.compl_univ, Set.union_empty,
      Set.preimage_image_eq _ hf.injective]
    exact measure_spanningSets_lt_top μ n

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ SigmaFinite (Measure.map f μ)

Tactic:
refine ⟨fun n ↦ f '' (spanningSets μ n) ∪ (Set.range f)ᶜ, by simp, fun n ↦ ?_, ?_⟩
  · rw [hf.map_apply, Set.preimage_union]
    simp only [Set.preimage_compl, Set.preimage_range, Set.compl_univ, Set.union_empty,
      Set.preimage_image_eq _ hf.injective]
    exact measure_spanningSets_lt_top μ n
  · rw [← Set.iUnion_union, ← Set.image_iUnion, iUnion_spanningSets,
      Set.image_univ, Set.union_compl_self]

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

Goal state before:
pp: case refine_1.iUnion
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ⋃ i, f i = ⋃₀ ↑S

Tactic:
refine ⟨(⋃ n, (S n : Set (Set α))).toFinset, ?_, ?_⟩

Goal state after:
case refine_1.iUnion.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ↑(⋃ n, ↑(S n)).toFinset ⊆ memPartition t n

case refine_1.iUnion.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ⋃ i, f i = ⋃₀ ↑(⋃ n, ↑(S n)).toFinset