mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ c ∉ Set.range Encodable.encode, 0 ≤ f c

Tactic:
intro i _

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
i : ℕ
a✝ : i ∉ Set.range Encodable.encode
⊢ 0 ≤ f i
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x) ↔
    LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s

Tactic:
exact
    ⟨fun H => ⟨fun x hx => (H x hx).1, fun x hx => (H x hx).2⟩, fun H x hx => ⟨H.1 x hx, H.2 x hx⟩⟩

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

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

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

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ b, g b)
⊢ ∃ T f, t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
induction h_t with
  | @base s h_s =>
    rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
    refine ⟨{b}, fun _ => s, ?_⟩
    simpa using h_s_in_t'
  | inter h_gen_s h_gen_t' h_nonempty h_s h_t' =>
    rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
    rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
    use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)
    constructor
    · ext a
      simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
      grind
    intro b h_b
    split_ifs with hbs hbt hbt
    · refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)
      exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)
    · exact h_s b hbs
    · exact h_t' b hbt
    · rw [Finset.mem_union] at h_b
      apply False.elim (h_b.elim hbs hbt)

Goal state after:
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
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

pp: case neg
α : 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 ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Tactic:
· have ht_eq_i : t = {i} := by
        ext1 x
        rw [Finset.mem_singleton]
        exact ⟨fun h => hti x h, fun h => h.symm ▸ hi⟩
      simp only [ht_eq_i, Finset.mem_singleton, iInter_iInter_eq_left]
      exact Or.inl (hfπ i hi)

Goal state after:
case neg
α : 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 ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}
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 α
h : s =ᵐ[μ] ∅
⊢ s ∪ t =ᵐ[μ] t

Tactic:
convert! ae_eq_set_union h (ae_eq_refl t)

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᵐ[μ] ∅
⊢ s ∪ t =ᵐ[μ] t ↔ s ∪ t =ᵐ[μ] ∅ ∪ t
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 α
h : s =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] t

Tactic:
convert! ae_eq_set_inter h (ae_eq_refl t)

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] t ↔ s ∩ t =ᵐ[μ] univ ∩ t
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 α
h : s =ᵐ[μ] ∅
⊢ s ∩ t =ᵐ[μ] ∅

Tactic:
convert! ae_eq_set_inter h (ae_eq_refl t)

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n ↦ AEMeasurable.mk (f n) ⋯ x

Tactic:
rw [funext fun n => mk_eq_fun_of_mem_aeSeqSet hf hx n]

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n ↦ f n x
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
⊢ MeasurableSet {x | Tendsto (fun n ↦ f n x) l l'}

Tactic:
rcases l.exists_antitone_basis with ⟨u, hu⟩

Goal state after:
β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
⊢ MeasurableSet {x | Tendsto (fun n ↦ f n x) l l'}
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: ι : Type u_8
ι' : Type u_9
e : ι ≃ ι'
β : ι' → Type u_10
inst✝ : (i' : ι') → MeasurableSpace (β i')
x : (i : ι) → β (e i)
i : ι
⊢ (piCongrLeft (fun i' ↦ β i') e) x (e i) = x i

Tactic:
piCongrLeft,

Goal state after:
ι : Type u_8
ι' : Type u_9
e : ι ≃ ι'
β : ι' → Type u_10
inst✝ : (i' : ι') → MeasurableSpace (β i')
x : (i : ι) → β (e i)
i : ι
⊢ { toEquiv := Equiv.piCongrLeft (fun i' ↦ β i') e, measurable_toFun := ⋯, measurable_invFun := ⋯ } x (e i) = x i
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ((restrict s) μ).trim t ≤ ((restrict s) μ.trim) t

Tactic:
restrict_apply

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ((restrict s) μ).trim t ≤ μ.trim (t ∩ s)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ s) ≤ ((restrict s) μ) t

Tactic:
restrict_apply

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ s) ≤ μ (t ∩ s)
Module: Mathlib.Order.Interval.Set.Monotone

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
⊢ StrictMonoOn φ (Iic n) → ∀ m ≤ n, m ≤ φ m

Tactic:
refine
    Succ.rec_bot (fun n => StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ m)
      (fun _ _ hm => hm.trans bot_le) ?_ _

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
⊢ ∀ (a : α), (StrictMonoOn φ (Iic a) → ∀ m ≤ a, m ≤ φ m) → StrictMonoOn φ (Iic (succ a)) → ∀ m ≤ succ a, m ≤ φ m
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ μ (s ∪ t) = μ s + μ t

Tactic:
← measure_union_add_inter₀ s ht,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ μ (s ∪ t) = μ (s ∪ t) + μ (s ∩ t)
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : ¬AEMeasurable f μ
⊢ map f (c • μ) = c • map f μ

Tactic:
have hfc : ¬AEMeasurable f (c • μ) := by
      intro hfc
      exact hf ⟨hfc.mk f, hfc.measurable_mk, (ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : ¬AEMeasurable f μ
hfc : ¬AEMeasurable f (c • μ)
⊢ map f (c • μ) = c • map f μ
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ ν + ν ≪ ν

Tactic:
· rw [← two_smul ℝ≥0]
    exact AbsolutelyContinuous.rfl.smul_left 2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : QuasiMeasurePreserving f μa μb
f' : α → β
hf' : Measurable f'
h : f =ᵐ[μa] f'
⊢ map f' μa ≪ μb

Tactic:
rw [Measure.map_congr h.symm]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : QuasiMeasurePreserving f μa μb
f' : α → β
hf' : Measurable f'
h : f =ᵐ[μa] f'
⊢ map f μa ≪ μb
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ((OuterMeasure.comap f) μ.toOuterMeasure) t =
    ((OuterMeasure.comap f) μ.toOuterMeasure) (t ∩ s) + ((OuterMeasure.comap f) μ.toOuterMeasure) (t \ s)

Tactic:
simp only [OuterMeasure.comap_apply, image_inter hf.1, image_sdiff hf.1]
      apply le_toOuterMeasure_caratheodory
      exact hf.2 s hs

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∃ i, μ (t i) = ∞
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Tactic:
rcases htop with ⟨i, hi⟩
    calc
      μ (⋃ i, t i) ≤ ∞ := le_top
      _ ≤ μ (s i) := hi ▸ h_le i
      _ ≤ μ (⋃ i, s i) := measure_mono <| subset_iUnion _ _

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ s ≠ ∞
ht : MeasurableSet t
hst : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict (t ∩ toMeasurable μ s)) u = (μ.restrict s) u

Tactic:
rw [restrict_apply hu, restrict_apply hu, inter_comm t, inter_comm, inter_assoc,
    measure_toMeasurable_inter (ht.inter hu) h]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ s ≠ ∞
ht : MeasurableSet t
hst : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ μ (s ∩ (t ∩ u)) = μ (u ∩ s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s✝ t : Set α
s : Finset ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), IsFiniteMeasure (μ i)
⊢ (∑ i ∈ s, μ i) univ < ∞

Tactic:
simp [measure_lt_top]

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

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), IsFiniteMeasure (μ i)
val✝ : Fintype ι
⊢ (sum μ) univ < ∞

Tactic:
simp [measure_lt_top]

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

Goal state before:
pp: case intro
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ∞
hne : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
⊢ Tendsto (fun i ↦ μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (μ (⋂ i, f i)))

Tactic:
measure_iInter_eq_iInf_measure_iInter_le hm hf

Goal state after:
case intro
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ∞
hne : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
⊢ Tendsto (fun i ↦ μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁✝ μ₂✝ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
x✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ μ₁ (⋃ i, s i) + μ₂ (⋃ i, s i) = ∑' (a : ℕ), μ₁ (s a) + ∑' (a : ℕ), μ₂ (s a)

Tactic:
measure_iUnion hd hs,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁✝ μ₂✝ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
x✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ ∑' (i : ℕ), μ₁ (s i) + μ₂ (⋃ i, s i) = ∑' (a : ℕ), μ₁ (s a) + ∑' (a : ℕ), μ₂ (s a)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ t ∈ range (natGeneratingSequence α), MeasurableSet t → ∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
simp only [mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (a : ℕ),
    MeasurableSet (natGeneratingSequence α a) →
      ∃ q, natGeneratingSequence α a = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
⊢ ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂

Tactic:
add_comm _ μ,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
⊢ μ + ν₁ = ν₂ + μ ↔ ν₁ = ν₂
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
⊢ μ + ν₁ = ν₂ + μ ↔ ν₁ = ν₂

Tactic:
add_comm _ μ,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
⊢ μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_1
α : 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)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ {x_1 ∈ F | x ∈ s x_1} ∈ G i

pp: case refine_2
α : 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)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ x ∈ P ({x_1 ∈ F | x ∈ s x_1})

Tactic:
· exact ⟨Finset.mem_powerset.mpr (filter_subset _ F), mem_filter.mpr ⟨hi, hx⟩⟩

Goal state after:
case refine_2
α : 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)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ x ∈ P ({x_1 ∈ F | x ∈ s x_1})
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₂
⊢ ∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun C ↦ (μ.restrict (P C)) t) C =
    ∑' (x : Finset ι), (↑Cs).indicator (fun C ↦ ∑ i ∈ F, (↑C).indicator (fun x ↦ (μ.restrict (P C)) t) i) x

Tactic:
congr with C

Goal state after:
case e_f
α : 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₂
C : Finset ι
⊢ ∑ i ∈ F, (G i).indicator (fun C ↦ (μ.restrict (P C)) t) C =
    (↑Cs).indicator (fun C ↦ ∑ i ∈ F, (↑C).indicator (fun x ↦ (μ.restrict (P C)) t) i) C
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
refine le_antisymm ?_ ?_
  · calc
      _ ≤ hausdorffEDist (closure s) s + hausdorffEDist s t := hausdorffEDist_triangle
      _ = hausdorffEDist s t := by simp [hausdorffEDist_comm]
  · calc
      _ ≤ hausdorffEDist s (closure s) + hausdorffEDist (closure s) t := hausdorffEDist_triangle
      _ = hausdorffEDist (closure s) t := by simp

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

Goal state before:
pp: case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
← univ_prod,

Goal state after:
case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (univ ×ˢ s)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ ((const α (i k)).restrict {a | i k ≤ f a}) a = if i k ≤ f a then i k else 0

Tactic:
restrict_apply

Goal state after:
case e_f
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ {a | i k ≤ f a}.indicator (⇑(const α (i k))) a = if i k ≤ f a then i k else 0

case e_f.hs
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ MeasurableSet {a | i k ≤ f a}
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n k : ℕ
x✝ : k ∈ Finset.range n
h : ¬i k ≤ f a
⊢ ⊥ ≤ ⨆ k, ⨆ (_ : i k ≤ f a), i k

Tactic:
exact bot_le

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (∀ a ≤ b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)

Tactic:
le_add_iff_lt_right_or_exists_le

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (∀ (a : α), (a < c ∨ ∃ d ≤ b, a = d + c) → P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (∃ a ≤ b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)

Tactic:
le_add_iff_lt_right_or_exists_le

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (∃ a, (a < c ∨ ∃ d ≤ b, a = d + c) ∧ P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this✝ : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
this : V ∈ 𝓝 x
⊢ thickening (δ / 2 + δ / 2) {f x} ⊆ U

Tactic:
by simp [hthick]

Goal state after: