mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
have : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ (measurableAtom y : Set β) := by
    ext1 ⟨x, y⟩
    simp only [mem_preimage, mem_iUnion, mem_prod]
    refine ⟨fun h ↦ ⟨y, h, mem_measurableAtom_self y⟩, ?_⟩
    rintro ⟨y', hy's, hy'⟩
    rwa [h'f y' y x hy']

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ y, ((fun x ↦ f (x, y)) ⁻¹' s) ×ˢ measurableAtom y
⊢ MeasurableSet (f ⁻¹' s)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⨅ (_ : f ⁻¹' s = ∅), 0 = ⨅ (_ : f '' f ⁻¹' s = ∅), 0

Tactic:
Set.image_eq_empty

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⨅ (_ : f ⁻¹' s = ∅), 0 = ⨅ (_ : f ⁻¹' s = ∅), 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y : EReal
⊢ (x * y).abs = x.abs * y.abs

Tactic:
by
  induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, abs_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
    rw [Ne, abs_eq_zero_iff, coe_eq_zero]
    exact h.ne'
  | neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]

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

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

Tactic:
rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_pos a_pos), coe_ennreal_ofReal,
          max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_inv a]
      congr
      exact abs_of_pos a_pos

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 [ne_self_iff_false, false_or] at h₂

Goal state after:
case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ * b < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: x : EReal
hx : x < ⊤
y : ℚ
hxy : x < ↑↑y
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x

Tactic:
exact ⟨_, trivial, Ioi_subset_Ioi hxy.le⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
⊢ LowerSemicontinuousWithinAt (g ∘ f) s x

Tactic:
intro y

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
⊢ (fun x1 x2 ↦ (g ∘ f) x1 > x2) x y → ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y
Module: Mathlib.Topology.Semicontinuity.Basic

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

Tactic:
intro y

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
⊢ (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x y → ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : |r| < 1
⊢ Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)

Tactic:
simpa only [← abs_pow] using! (tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg r)) h

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

Goal state before:
pp: case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]

Goal state after:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∀ b < ∞, ∃ i, b < ∑ a ∈ Finset.range i, r ^ a
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
this : Nonempty { t // s ⊆ ⋃ i, t i }
⊢ c * ⨅ x, ∑' (n : ℕ), m (↑x n) = ⨅ x, c * ∑' (i : ℕ), m (↑x i)

Tactic:
ENNReal.mul_iInf fun h => (hc h).elim

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
this : Nonempty { t // s ⊆ ⋃ i, t i }
⊢ ⨅ i, c * ∑' (n : ℕ), m (↑i n) = ⨅ x, c * ∑' (i : ℕ), m (↑x i)
Module: Mathlib.Topology.Semicontinuity.Basic

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

Tactic:
intro y

Goal state after:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
⊢ (fun x1 x2 ↦ (fun x' ↦ ⨆ i, f i x') x1 > x2) x y →
    ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun x' ↦ ⨆ i, f i x') x1 > x2) x' y
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
⊢ (restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (restrict s) (m i)

Tactic:
have := hI.to_subtype
  rw [← iInf_subtype'', ← iInf_subtype'']
  exact restrict_iInf _ _

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
s t : Set α
⊢ IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}

Tactic:
by
  rintro _ ⟨l₁, hls₁, u₁, hut₁, _, rfl⟩ _ ⟨l₂, hls₂, u₂, hut₂, _, rfl⟩
  simp only [Hi]
  exact fun H => ⟨l₁ ⊔ l₂, sup_ind l₁ l₂ hls₁ hls₂, u₁ ⊓ u₂, inf_ind u₁ u₂ hut₁ hut₂, Hne H, rfl⟩

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
⊢ m (t ∩ s₁) + m (t ∩ ((s₁ ∪ s₂) \ s₁)) = m (t ∩ s₁) + m (t ∩ s₂)

Tactic:
union_sdiff_cancel_left h

Goal state after:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
⊢ m (t ∩ s₁) + m (t ∩ s₂) = m (t ∩ s₁) + m (t ∩ s₂)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case a
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ generatePiSystem g, MeasurableSet t

pp: case a
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ g, MeasurableSet t

Tactic:
· exact fun t h_t => generateFrom_measurableSet_of_generatePiSystem t h_t

Goal state after:
case a
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ g, MeasurableSet t
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: 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

Tactic:
rw [← iUnion_sdiff]

Goal state after:
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, f i) \ s
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: 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
⊢ ∑' (a : ℕ), (m ((fun i ↦ f i ∩ s) a) + m ((fun i ↦ f i \ s) a)) ≤ ∑' (i : ℕ), m (f i)

Tactic:
exact ENNReal.tsum_le_tsum fun i => hs _

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 α
⊢ sᶜ =ᵐ[μ] t ↔ s =ᵐ[μ] tᶜ

Tactic:
← ae_eq_set_compl_compl,

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ sᶜᶜ =ᵐ[μ] tᶜ ↔ s =ᵐ[μ] tᶜ
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
hg : AEMeasurable g μ
a : δ
⊢ AEMeasurable (fun x ↦ g x a) μ

Tactic:
by
  use fun x ↦ hg.mk g x a, hg.measurable_mk.eval
  exact hg.ae_eq_mk.mono fun _ h ↦ congrFun h _

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (bliminf s atTop p)

Tactic:
simp only [Filter.bliminf_eq_iSup_biInf_of_nat, iInf_eq_iInter, iSup_eq_iUnion]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋃ i, ⋂ j, ⋂ (_ : p j ∧ i ≤ j), s j)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

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

Tactic:
simpa only [symm_preimage_preimage] using e.symm.measurable h

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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
this : (A : Set α) ×' MeasurableSet A ∧ F A = A
⊢ α ≃ᵐ β

Tactic:
by
    classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
h : s =ᵐ[μ] t
⊢ NullMeasurableSet t μ

Tactic:
rw [nullMeasurableSet_iff_eventuallyMeasurableSet]
  exact EventuallyMeasurableSet.congr hs h.symm

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s t : Set α
x✝ : MeasurableSpace α
μ : Measure α
⊢ μ.trim ≤ μ.trim

Tactic:
exact OuterMeasure.trim_anti_measurableSpace _ fun _ ↦ MeasurableSet.nullMeasurableSet

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 μ
s : Set β
hs : NullMeasurableSet s (map f μ)
⊢ (map f μ) s = μ (f ⁻¹' s)

Tactic:
rw [map, dif_pos hf, mapₗ, dif_pos hf.measurable_mk] at hs ⊢
  rw [liftLinear_apply₀ _ hs, measure_congr (hf.ae_eq_mk.preimage s)]
  rfl

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 α
⊢ (c • ν) s = 0 → (c • μ) s = 0

Tactic:
hνs

Goal state after:
α : 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 : (c • ν) s = 0
⊢ (c • μ) s = 0
Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ∞
t : Finset ι
⊢ μ (limsup s cofinite) ≤ μ (⋃ i, s ↑i)

Tactic:
by
      gcongr
      rw [hasBasis_cofinite.limsup_eq_iInf_iSup, iUnion_subtype]
      exact iInter₂_subset _ t.finite_toSet

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
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ c < b

Tactic:
by simpa using hcb

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
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hsne : s.Nonempty
a : X
ha : a < b
c : X
hcb : c < b
hcs : Ioo c b ⊆ s
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
rcases hb.lt_iff_exists_lt.mp (max_lt ha hcb) with ⟨x, hxb, hacx⟩

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hsne : s.Nonempty
a : X
ha : a < b
c : X
hcb : c < b
hcs : Ioo c b ⊆ s
x : X
hxb : x < b
hacx : max a c < x
⊢ (s ∩ Ioo a b).Nonempty
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ |(μ (s \ t)).toReal - (μ (t \ s)).toReal| ≤ (μ (s \ t) + μ (t \ s)).toReal

Tactic:
ENNReal.toReal_add hst hts

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ |(μ (s \ t)).toReal - (μ (t \ s)).toReal| ≤ (μ (s \ t)).toReal + (μ (t \ s)).toReal
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 α
hm : Monotone s
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))

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

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

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

Tactic:
Subtype.forall

Goal state after:
case pos.hs
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
ha : Order.IsPredPrelimit a
this : atBot.IsCountablyGenerated
⊢ ∀ (a_1 : ι) (b : a_1 ∈ Ioi a), NullMeasurableSet (s ↑⟨a_1, b⟩) μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : 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 α := fun n ↦ toMeasurable (m n) t
T : t ⊆ ⋂ n, w n
M : MeasurableSet (⋂ n, w n)
u : Set α
hu : MeasurableSet u
i : ℕ
⊢ (m i) ((⋂ n, w n) ∩ u) ≤ (m i) (t ∩ u)

Tactic:
calc
    m i ((⋂ n, w n) ∩ u) ≤ m i (w i ∩ u) := by gcongr; apply iInter_subset
    _ = m i (t ∩ u) := measure_toMeasurable_inter hu (hv i)

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

Goal state before:
pp: case refine_2
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x : α
hx : x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
y : α
hy : y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
⊢ x = y

Tactic:
simp only [mem_sInter, mem_inter_iff, mem_iInter, mem_compl_iff] at hx hy

Goal state after:
case refine_2
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : α
hx : (x ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ i ∈ S, iᶜ ∈ l → x ∉ i
hy : (y ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ i ∈ S, iᶜ ∈ l → y ∉ i
⊢ x = y
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 (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t') = (x ∈ t)
⊢ t' ∩ s =ᵐ[μ] t ∩ s

Tactic:
filter_upwards [this] with y hy

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t') = (x ∈ t)
y : α
hy : y ∈ s → (y ∈ t') = (y ∈ t)
⊢ (t' ∩ s) y = (t ∩ s) y
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 : α
hx : t' x = t x
⊢ x ∈ t' ↔ x ∈ t

Tactic:
simpa using! hx

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
p q : ℕ → Prop
hpq : p ≠ q
s : Set α
hsp : s ⊆ countablyGeneratedAtom α p
hsq : s ⊆ countablyGeneratedAtom α q
x : α
hxs : x ∈ s
n : ℕ
hn : p n ≠ q n
⊢ False

Tactic:
specialize hsp hxs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
p q : ℕ → Prop
hpq : p ≠ q
s : Set α
hsq : s ⊆ countablyGeneratedAtom α q
x : α
hsp : x ∈ countablyGeneratedAtom α p
hxs : x ∈ s
n : ℕ
hn : p n ≠ q n
⊢ False
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

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

Tactic:
Subtype.forall

Goal state after:
case refine_2.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∀ (a : ℕ) (b : a ∈ {k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑⟨a, b⟩) = min (μ (t' ↑⟨a, b⟩)) (ν (t' ↑⟨a, b⟩))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

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

Tactic:
Subtype.forall

Goal state after:
case refine_2.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∀ (a : ℕ) (b : a ∈ {k | ν (t' k) < μ (t' k)}), ν (t' ↑⟨a, b⟩) = min (μ (t' ↑⟨a, b⟩)) (ν (t' ↑⟨a, b⟩))
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
⊢ AEMeasurable f μ

Tactic:
rcases eq_or_ne μ 0 with (rfl | hμ)
  · exact aemeasurable_zero_measure
  · have := ae_neBot.2 hμ
    rcases h.exists with ⟨x, hx⟩
    exact ⟨const α (f x), measurable_const, EventuallyEq.symm hx⟩

Goal state after: