mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
m : ℕ
hm : m ≥ N + 1
⊢ u m / v m = 1

Tactic:
simp [huv m (le_of_lt hm)]

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ
w : α
hw : 1 < ‖w‖
n : ℕ
hn : r < ‖w‖ ^ n
⊢ r < ‖w ^ n‖

Tactic:
by rwa [norm_pow]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ nndist (f x) (f y) = ratio f * nndist x y

Tactic:
simp only [← ENNReal.coe_inj, ← edist_nndist, ENNReal.coe_mul, edist_eq]

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)

Tactic:
apply generateFrom_induction

Goal state after:
case hC
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ t ∈ S, MeasurableSet t → (x ∈ t ↔ y ∈ t)

case empty
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ x ∈ ∅ ↔ y ∈ ∅

case compl
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ (t : Set α), MeasurableSet t → (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)

case iUnion
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n : ℕ), x ∈ s n ↔ y ∈ s n) → (x ∈ ⋃ i, s i ↔ y ∈ ⋃ i, s i)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
ht : ∀ i ∈ s, MeasurableSet (t i)
⊢ MeasurableSet (s.pi t)

Tactic:
pi_def

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
ht : ∀ i ∈ s, MeasurableSet (t i)
⊢ MeasurableSet (⋂ a ∈ s, eval a ⁻¹' t a)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi t
hst : MeasurableSet (s.pi t)
i : δ
hi : i ∈ s
⊢ t i = update f i ⁻¹' s.pi t

Tactic:
update_preimage_pi hi

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi t
hst : MeasurableSet (s.pi t)
i : δ
hi : i ∈ s
⊢ t i = t i

δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi t
hst : MeasurableSet (s.pi t)
i : δ
hi : i ∈ s
⊢ ∀ j ∈ s, j ≠ i → f j ∈ t j
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
⊢ 0 < 1 / (↑n + 1)

Tactic:
rw [one_div]
  exact inv_pos_of_nat

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (x : ↑univ) (x_1 : ↑(t ↑x)), f ↑x_1

Tactic:
rw [← ENNReal.tsum_biUnion' h, Set.biUnion_univ]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
⊢ ∑' (a : α), ↑(f a) ≠ ∞ ↔ Summable f

Tactic:
exact tsum_coe_ne_top_iff_summable

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

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (-↑a✝)⁻¹ = -↑a✝⁻¹

Tactic:
← coe_neg _⁻¹,

Goal state after:
case coe
a✝ : ℝ
⊢ (-↑a✝)⁻¹ = ↑(-a✝⁻¹)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ a⁻¹⁻¹ = a

Tactic:
rw [← coe_toReal h' h, ← coe_inv a.toReal, ← coe_inv a.toReal⁻¹, _root_.inv_inv a.toReal]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i ↦ ∑' (k : ℕ), (fun i ↦ ↑(f i)) (k + i)) atTop (𝓝 0)

Tactic:
simp only [← ENNReal.coe_tsum, NNReal.summable_nat_add _ hf, ← ENNReal.coe_zero]

Goal state after:
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i ↦ ↑(∑' (a : ℕ), f (a + i))) atTop (𝓝 ↑0)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inr.inl
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : a * ⊤ < c
b0 : 0 < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
rcases lt_trichotomy a 0 with a0 | rfl | a0

Goal state after:
case inr.inr.inl.inl
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : a * ⊤ < c
b0 : 0 < ⊤
a0 : a < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

case inr.inr.inl.inr.inl
c : EReal
b0 : 0 < ⊤
a_top : 0 < ⊤
h₁ : 0 ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : 0 ≠ ⊤ ∨ 0 < ⊤
hc : 0 * ⊤ < c
⊢ ∃ a' ∈ Ioo 0 ⊤, a' * ⊤ < c

case inr.inr.inl.inr.inr
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : a * ⊤ < c
b0 : 0 < ⊤
a0 : 0 < a
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : 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, HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε

Tactic:
rcases hf.summable.comp_injective (@Encodable.encode_injective ι _) with ⟨c, hg⟩

Goal state after:
α : 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, HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
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, LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun z ↦ ∑ i ∈ a, f i z) univ x

Tactic:
exact lowerSemicontinuousWithinAt_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
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 (a + 0))
⊢ Tendsto (fun x ↦ ↑⌈a * x⌉₊ / x) atTop (𝓝 a)

Tactic:
rw [add_zero] at A

Goal state after:
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
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
⊢ Tendsto (fun x ↦ ↑⌈a * x⌉₊ / x) atTop (𝓝 a)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

Tactic:
exact continuousAt_mul_symm2 continuousAt_mul_top_top

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inter
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ s ∈ S, MeasurableSet s
t s✝ t✝ : Set α
h_s✝ : generatePiSystem S s✝
h_t✝ : generatePiSystem S t✝
h_nonempty✝ : (s✝ ∩ t✝).Nonempty
h_s : MeasurableSet s✝
h_u : MeasurableSet t✝
⊢ MeasurableSet (s✝ ∩ t✝)

Tactic:
| inter _ _ _ h_s h_u =>

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}

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

Tactic:
· rintro ⟨t, hti, f, hfπ, rfl⟩
    simp only [subset_singleton_iff, Finset.mem_coe] at hti
    by_cases hi : i ∈ t
    · 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)
    · have ht_empty : t = ∅ := by
        ext1 x
        simp only [Finset.notMem_empty, iff_false]
        exact fun hx => hi (hti x hx ▸ hx)
      simp [ht_empty, iInter_univ, Set.mem_singleton univ]

Goal state after:
case refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) = ⨆ i ∈ S, m i

Tactic:
refine le_antisymm ?_ ?_
  · rw [← @generateFrom_measurableSet α (⨆ i ∈ S, m i)]
    exact generateFrom_mono (measurableSet_iSup_of_mem_piiUnionInter m S)
  · refine iSup₂_le fun i hi => ?_
    rw [← @generateFrom_measurableSet α (m i)]
    exact generateFrom_mono (mem_piiUnionInter_of_measurableSet m hi)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
t : ι → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᵐ[μ] s i
⊢ ∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᵐ[μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)

Tactic:
rcases exists_null_pairwise_disjoint_sdiff hd with ⟨u, hum, hu₀, hud⟩

Goal state after:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
t : ι → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᵐ[μ] s i
u : ι → Set α
hum : ∀ (i : ι), MeasurableSet (u i)
hu₀ : ∀ (i : ι), μ (u i) = 0
hud : Pairwise (Disjoint on fun i ↦ s i \ u i)
⊢ ∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᵐ[μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ (mapₗ (AEMeasurable.mk f hf)) μ = (mapₗ (AEMeasurable.mk g hg)) μ

Tactic:
exact
      mapₗ_congr hf.measurable_mk hg.measurable_mk (hf.ae_eq_mk.symm.trans (h.trans hg.ae_eq_mk))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

Tactic:
by
  by_cases h : AEMeasurable f μ
  · change range f ∈ ae (μ.map f)
    rw [mem_ae_map_iff h hf]
    filter_upwards using mem_range_self
  · simp [map_of_not_aemeasurable h]

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

Goal state before:
pp: case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
· intro x hx
    rcases (hμ x hx).exists_mem_basis (nhds_basis_opens _) with ⟨U, ⟨hx, hUo⟩, hU⟩
    exact ⟨U, nhdsWithin_le_nhds (hUo.mem_nhds hx), U, Subset.rfl, hUo, hU⟩

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

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ x ∈ ⋃ y ∈ s, measurableAtom y

Tactic:
simpa using ⟨x, hx, by simp⟩

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

Goal state before:
pp: case intro
α : 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 ι
⊢ SigmaFinite (sum μ)

Tactic:
have : ∀ n, MeasurableSet (⋂ i : ι, spanningSets (μ i) n) := fun n =>
    MeasurableSet.iInter fun i => measurableSet_spanningSets (μ i) n

Goal state after:
case intro
α : 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)
⊢ SigmaFinite (sum μ)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
⊢ f =ᵐ[μ.restrict s] g ↔ s.indicator f =ᵐ[μ] s.indicator g

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs]
  refine ⟨fun h => ?_, fun h => ?_⟩ <;> filter_upwards [h] with x hx
  · by_cases hxs : x ∈ s
    · simp [hxs, hx hxs]
    · simp [hxs]
  · intro hxs
    simpa [hxs] using hx

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

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

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

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

pp: 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

Tactic:
· simp only [coe_toFinset, iUnion_subset_iff]
        exact hS_subset

Goal state after:
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
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
⊢ ((sum fun i ↦ μ ↑i) + sum fun i ↦ μ ↑i) = sum μ

Tactic:
by
  ext1 t ht
  simp only [add_apply, sum_apply _ ht]
  exact ENNReal.summable.tsum_add_tsum_compl (f := fun i => μ i t) ENNReal.summable

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
μ ν : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum μ + sum ν) s = (sum fun n ↦ μ n + ν n) s

Tactic:
simp only [add_apply, sum_apply _ hs,
    ENNReal.summable.tsum_add ENNReal.summable]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι✝ : Sort y
s t u : Set α
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : MeasurableSpace α
inst✝¹⁴ : OpensMeasurableSpace α
inst✝¹³ : TopologicalSpace β
inst✝¹² : MeasurableSpace β
inst✝¹¹ : OpensMeasurableSpace β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : MeasurableSpace γ
inst✝⁸ : BorelSpace γ
inst✝⁷ : TopologicalSpace γ₂
inst✝⁶ : MeasurableSpace γ₂
inst✝⁵ : BorelSpace γ₂
inst✝⁴ : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
this :
  topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = (↑i).pi s}
⊢ ∀ t ∈ {t | ∃ s i, (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = (↑i).pi s}, MeasurableSet t

Tactic:
rintro _ ⟨s, i, hi, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι✝ : Sort y
s✝ t u : Set α
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : MeasurableSpace α
inst✝¹⁴ : OpensMeasurableSpace α
inst✝¹³ : TopologicalSpace β
inst✝¹² : MeasurableSpace β
inst✝¹¹ : OpensMeasurableSpace β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : MeasurableSpace γ
inst✝⁸ : BorelSpace γ
inst✝⁷ : TopologicalSpace γ₂
inst✝⁶ : MeasurableSpace γ₂
inst✝⁵ : BorelSpace γ₂
inst✝⁴ : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
this :
  topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = (↑i).pi s}
s : (a : ι) → Set (X a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ countableBasis (X a)
⊢ MeasurableSet ((↑i).pi s)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case pos
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
⊢ MeasurableSet (Iio a)

pp: case neg
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∃ b < a, Ioo b a = ∅
⊢ MeasurableSet (Iio a)

Tactic:
· convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u < a), Icc l u)
    · ext y
      push _ ∈ _
      constructor
      · intro hy
        rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) y with ⟨l, hlt, hly⟩
        rcases htd.exists_mem_open isOpen_Ioo (ha y hy) with ⟨u, hut, hyu, hua⟩
        exact ⟨l, hlt, u, hut, hly.trans_lt hyu, hua, hly, hyu.le⟩
      · rintro ⟨l, -, u, -, -, hua, -, hyu⟩
        exact hyu.trans_lt hua
    · refine MeasurableSet.biUnion hc fun a ha => MeasurableSet.biUnion hc fun b hb => ?_
      refine MeasurableSet.iUnion fun hab => MeasurableSet.iUnion fun _ => ?_
      exact .basic _ ⟨a, hts ha, b, hts hb, hab.le, mem_singleton _⟩

Goal state after:
case neg
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∃ b < a, Ioo b a = ∅
⊢ MeasurableSet (Iio a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
⊢ MeasurableSpace.comap e (borel β) = inst✝³

Tactic:
simpa [hβ.measurable_eq] using h'e.comap_eq

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContinuousAt (fun x ↦ (infDist x s)⁻¹) x

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)
  · simp only [infDist_empty, continuousAt_const]
  · refine (continuous_infDist_pt s).continuousAt.inv₀ ?_
    rwa [Ne, ← mem_closure_iff_infDist_zero hs]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
⊢ ∃ y ∈ t, dist x y < r

Tactic:
by
  have r0 : 0 < r := lt_of_le_of_lt hausdorffDist_nonneg H
  have : hausdorffEDist s t < ENNReal.ofReal r := by
    rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
      ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H
  rcases exists_edist_lt_of_hausdorffEDist_lt h this with ⟨y, hy, yr⟩
  rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff r0] at yr
  exact ⟨y, hy, yr⟩

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_2
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
x l : α
hls : l ∈ s
hlx : l ≤ x
u : α
hus : u ∈ s
hxu : x ≤ u
⊢ ∃ b ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}, x ∈ b

Tactic:
exact ⟨_, ⟨l, hls, u, hus, hlx.trans hxu, rfl⟩, hlx, hxu⟩

Goal state after:
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:
simp [hthick]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
s : Set α
μ : Measure α
⊢ f.lintegral (μ.restrict s) = ∑ y ∈ f.range, y * μ (⇑f ⁻¹' {y} ∩ s)

Tactic:
simp only [lintegral, Measure.restrict_apply, f.measurableSet_preimage]

Goal state after: