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

Goal state before:
pp: a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
by
  refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_
  obtain ⟨a', aa', hd⟩ := exists_mul_left_lt (h₁.imp_left ne_of_gt) h₂ hd
  replace h₁ : 0 < a' ∨ b ≠ ⊤ := h₁.imp_left fun a0 ↦ a0.trans (mem_Ioo.1 aa').1
  replace h₂ : a' ≠ ⊤ ∨ b ≠ 0 := Or.inl (mem_Ioo.1 aa').2.ne
  obtain ⟨b', bb', hd⟩ := exists_mul_right_lt h₁ h₂ hd
  exact (h a' (mem_Ioo.1 aa').1 b' (mem_Ioo.1 bb').1).trans hd.le

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto (fun n ↦ ↑n / (↑n + x)) atTop (𝓝 1)

Tactic:
by
  convert! Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn ↦ _)) _
  · exact fun n : ℕ ↦ 1 / (1 + x / n)
  · simp [Nat.cast_ne_zero.mpr hn, add_div']
  · have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * (0 : 𝕜))) := by
      rw [mul_zero, add_zero, div_one]
    rw [this]
    refine tendsto_const_nhds.div (tendsto_const_nhds.add ?_) (by simp)
    simp_rw [div_eq_mul_inv]
    exact tendsto_const_nhds.mul tendsto_inv_atTop_nhds_zero_nat

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

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

Tactic:
simp_rw [le_iInf_iff]

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

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

Tactic:
by_cases ht : ∀ i, P (t i)

Goal state after:
case pos
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ∀ (i : ℕ), P (t i)
⊢ ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) ≤ ∑' (n : ℕ), m (t n)

case neg
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ¬∀ (i : ℕ), P (t i)
⊢ ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) ≤ ∑' (n : ℕ), m (t n)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case succ
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i ↦ Nat.casesOn i s fun x ↦ ∅
i : ℕ
⊢ i + 1 ≠ 0 → m (f (i + 1)) = 0

Tactic:
· simp [f, m_empty]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
m : ι → OuterMeasure α
s : Set α
⊢ (⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)

Tactic:
have := hI.to_subtype

Goal state after:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
m : ι → OuterMeasure α
s : Set α
this : Nonempty ↑I
⊢ (⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
⊢ (map f) (⨅ i ∈ I, (comap f) (m i)) = ⨅ i ∈ I, (map f) ((comap f) (m i))

Tactic:
have := hI.to_subtype

Goal state after:
α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ (map f) (⨅ i ∈ I, (comap f) (m i)) = ⨅ i ∈ I, (map f) ((comap f) (m i))
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

Goal state after:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
this : Nonempty ↑I
⊢ (restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (restrict s) (m i)
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋂ x, dissipate s x ⊆ ⋂ x, s x

Tactic:
subset_def,

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ x ∈ ⋂ x, dissipate s x, x ∈ ⋂ x, s x
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋂ x, s x ⊆ ⋂ x, dissipate s x

Tactic:
subset_def,

Goal state after:
case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ x ∈ ⋂ x, s x, x ∈ ⋂ x, dissipate s x
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:
| succ n hn =>

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case succ
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : (dissipate s n).Nonempty → dissipate s n ∈ C
h' : (dissipate s (n + 1)).Nonempty
⊢ dissipate s (n + 1) ∈ C

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
⊢ IsPiSystem (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
rintro _ ⟨s₁, hs₁, t₁, ht₁, rfl⟩ _ ⟨s₂, hs₂, t₂, ht₂, rfl⟩ hst
  rw [prod_inter_prod] at hst ⊢; rw [prod_nonempty_iff] at hst
  exact mem_image2_of_mem (hC _ hs₁ _ hs₂ hst.1) (hD _ ht₁ _ ht₂ hst.2)

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₂
t : Set α
⊢ m t = m (t ∩ (s₁ ∪ s₂)) + m (t \ (s₁ ∪ s₂))

Tactic:
by
  rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁), h₁ (t ∩ (s₁ ∪ s₂)), inter_sdiff_assoc _ _ s₁,
    Set.inter_assoc _ _ s₁, inter_eq_self_of_subset_right Set.subset_union_left,
    union_sdiff_left, h₂ (t ∩ s₁)]
  simp [sdiff_eq, add_assoc]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

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

Tactic:
rintro ⟨t, hti, f, hfπ, rfl⟩

Goal state after:
case refine_1
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
hti : ↑t ⊆ {i}
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : 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
x : ι
⊢ x ∈ t ↔ x ∈ {i}

Tactic:
rw [Finset.mem_singleton]

Goal state after:
α : 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
x : ι
⊢ x ∈ t ↔ x = i
Module: Mathlib.MeasureTheory.PiSystem

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

Tactic:
· 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.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ MeasurableSet s ↔
    ∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

Tactic:
isCaratheodory_iff_le

Goal state after:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t) ↔
    ∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ∈ ⨅ i, f i

Tactic:
rw [← Equiv.plift.surjective.iInf_comp, mem_iInf]
    exact ⟨t, ht, U, hUf, rfl⟩

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

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

Tactic:
rw [toMeasurable_def, dif_pos]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ Exists.choose ?hc =ᵐ[μ] s

case hc
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
⊢ f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ f ⁻¹' (range f)ᶜ = toMeasurable μ (f ⁻¹' s)

Tactic:
preimage_compl,

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
⊢ f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ (f ⁻¹' range f)ᶜ = toMeasurable μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ ((comapₗ f) μ) s = μ (f '' s)

Tactic:
rw [comapₗ, dif_pos, liftLinear_apply _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure]

Goal state after:
case hc
α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ tᶜ = 0
⊢ μ (s ∩ t) = μ s

Tactic:
rw [← sdiff_compl, measure_sdiff_null ht]

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 : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
⊢ map Subtype.val atTop = 𝓝[<] b

Tactic:
rcases eq_empty_or_nonempty (Iio b) with (hb' | ⟨a, ha⟩)
  · have : IsEmpty s := ⟨fun x => hb'.subset (hsb x.2)⟩
    rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]
  · rw [← comap_coe_nhdsLT_of_Ioo_subset hsb (fun _ => hs a ha) hb, map_comap_of_mem]
    rw [Subtype.range_val]
    exact (mem_nhdsLT_iff_exists_Ioo_subset' ha).2 (hs a ha)

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
⊢ SFinite (sum m)

Tactic:
obtain ⟨f, hf⟩ : ∃ f : ι → ℕ, Function.Injective f := Countable.exists_injective_nat ι
  refine ⟨_, fun n ↦ ?_, (sum_extend_zero hf m).symm⟩
  rcases em (n ∈ range f) with ⟨i, rfl⟩ | hn
  · rw [hf.extend_apply]
    infer_instance
  · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply]
    infer_instance

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

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

Tactic:
Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ ((OuterMeasure.restrict s) μ.toOuterMeasure) t = μ (t ∩ s)
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) ≠ ∞
⊢ (μ s).toReal - (μ t).toReal = (μ (s ∪ t)).toReal - (μ t).toReal - ((μ (s ∪ t)).toReal - (μ s).toReal)

Tactic:
abel

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : μ.restrict s = ν.restrict s
t : Set α
hts : t ⊆ s
ht : MeasurableSet t
⊢ μ (t ∩ s) = ν (t ∩ s)

Tactic:
← restrict_apply ht,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : μ.restrict s = ν.restrict s
t : Set α
hts : t ⊆ s
ht : MeasurableSet t
⊢ (μ.restrict s) t = ν (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
D : ℕ → Set (Set α)
DC : ∀ (n : ℕ), D n ⊆ C
D_count : ∀ (n : ℕ), (D n).Countable
hD : ∀ (n : ℕ), ∀ s ∈ C, s ≤ᵐ[sfiniteSeq μ n] ⋃₀ D n
⊢ ⋃ n, D n ⊆ C

Tactic:
simp [DC]

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
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

Tactic:
by_cases hxf : x ∈ f n

Goal state after:
case pos
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∈ f n
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

case neg
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∉ f n
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
⊢ (μ.restrict s) (f ⁻¹' t)ᶜ = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0

Tactic:
Measure.restrict_apply' hs

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
⊢ μ ((f ⁻¹' t)ᶜ ∩ s) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case hn
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Pairwise (Disjoint on disjointed w)

pp: case h
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∀ (i : ℕ), MeasurableSet (disjointed w i)

Tactic:
· exact disjoint_disjointed _

Goal state after:
case h
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∀ (i : ℕ), MeasurableSet (disjointed w i)
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
mem_ae_iff

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ μ (s.indicator f ⁻¹' t)ᶜ = 0 ↔ (μ.restrict s) (f ⁻¹' t)ᶜ = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
⊢ (sum fun i ↦ μ.restrict (s i)) ≤ M • μ.restrict (⋃ i, s i)

Tactic:
refine le_iff.mpr (fun t ht ↦ le_of_eq_of_le (sum_apply _ ht) ?_)

Goal state after:
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
⊢ ∑' (i : ι), (μ.restrict (s i)) t ≤ (M • μ.restrict (⋃ i, s i)) t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case intro.refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
⊢ ⋃ i, ⋂ i_1, spanningSets (μ i_1) i = univ

Tactic:
· rw [iUnion_iInter_of_monotone]
    · simp_rw [iUnion_spanningSets, iInter_univ]
    exact fun i => monotone_spanningSets (μ i)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ Measurable (mapNatBool α)

Tactic:
rw [measurable_pi_iff]
  refine fun n ↦ measurable_to_bool ?_
  simp only [preimage, mem_singleton_iff, mapNatBool,
    Bool.decide_iff, ofPred_mem_eq]
  apply measurableSet_natGeneratingSequence

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
i : ι
x : α
hx : x ∉ s i
⊢ f x = mk f ⋯ x

Tactic:
contrapose! hx

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
i : ι
x : α
hx : f x ≠ mk f ⋯ x
⊢ x ∈ s i
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
⊢ ∑ i ∈ F, ∑' (C : ↑(G i)), (μ.restrict (P ↑C)) t =
    ∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun C ↦ (μ.restrict (P C)) t) C

Tactic:
rw [Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)]
      congr with i
      rw [tsum_subtype (G i) (fun C ↦ (μ.restrict (P C)) t)]

Goal state after:
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
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
⊢ {x | f x = mk f H x ∧ f x ∈ t} ∈ ae μ

Tactic:
exact H.ae_eq_mk.and ht

Goal state after:
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
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
A : μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : x ∉ toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ f x = mk f H x

Tactic:
contrapose! hx

Goal state after:
α : 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
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
A : μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : f x ≠ mk f H x
⊢ x ∈ toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t✝ : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t✝
t_cl : IsClosed[inst✝¹] t✝
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t✝ = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t✝ ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
t : Set X
tinT : t ∈ T
n : ℕ
gn : g n = ⟨t, tinT⟩
⊢ ↑(g n) ⊆ t

Tactic:
rw [gn]

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

Goal state before:
pp: G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableMul G
g : G
⊢ Measurable fun h ↦ h * g⁻¹

Tactic:
measurable_mul_const

Goal state after: