mathlib-initiative/mathlib-tactics huggingface dataset:
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:
rw [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.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
⊢ ∀ (a : ℕ) (b : a ∈ {k | ν (t' k) < μ (t' k)}), ν (t' ↑⟨a, b⟩) = min (μ (t' ↑⟨a, b⟩)) (ν (t' ↑⟨a, b⟩))

Tactic:
intro n hn

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
n : ℕ
hn : n ∈ {k | ν (t' k) < μ (t' k)}
⊢ ν (t' ↑⟨n, hn⟩) = min (μ (t' ↑⟨n, hn⟩)) (ν (t' ↑⟨n, hn⟩))
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
⊢ ∀ (s : Set X), IsClosed[inst✝²] s → y ∈ s → x ∈ s

Tactic:
intro K

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
K : Set X
⊢ IsClosed[inst✝²] K → y ∈ K → x ∈ K
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst✝³] t
⊢ MeasurableSet (s.ite (f ⁻¹' t) (g ⁻¹' t))

Tactic:
Set.ite

Goal state after:
α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst✝³] t
⊢ MeasurableSet (f ⁻¹' t ∩ s ∪ g ⁻¹' t \ s)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : s.Nonempty
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ infDist x s = 0

Tactic:
by
  simp [mem_closure_iff_infEDist_zero, infDist, ENNReal.toReal_eq_zero_iff, infEDist_ne_top h]

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

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ (MeasurableSpace.comap g mδ).prod (MeasurableSpace.comap f mβ) = mγ.prod mα

Tactic:
hg.comap_eq,

Goal state after:
case refine_1
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ mγ.prod (MeasurableSpace.comap f mβ) = mγ.prod mα
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case refine_2
α : 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 = ⊥
k : ℕ
hk : i k ≤ f a
this : k ∈ Finset.range (k + 1)
⊢ i k = if i k ≤ f a then i k else 0

Tactic:
rw [if_pos hk]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ g (f a) * ∑ y ∈ f.range with g y = g (f a), μ (⇑f ⁻¹' {y}) = ∑ j ∈ f.range with g j = g (f a), g j * μ (⇑f ⁻¹' {j})

Tactic:
Finset.mul_sum

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ ∑ i ∈ f.range with g i = g (f a), g (f a) * μ (⇑f ⁻¹' {i}) = ∑ j ∈ f.range with g j = g (f a), g j * μ (⇑f ⁻¹' {j})
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: a : ℝ
x✝ : Set ℝ
hav : a ∈ x✝
hv : IsOpen x✝
w✝¹ w✝ : ℝ
hl : w✝¹ < a
hu : a < w✝
h : Ioo w✝¹ w✝ ⊆ x✝
q : ℚ
hlq : w✝¹ < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < w✝
⊢ Ioo ↑q ↑p ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}

Tactic:
simp only [mem_iUnion]
      exact ⟨q, p, Rat.cast_lt.1 <| hqa.trans hap, rfl⟩

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

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (⨆ x, f (x + k)))

Tactic:
exact tendsto_atTop_ciSup h_mon h_bdd

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Ici ia, (nearestPt e x_1) x ∈ eball x ε

Tactic:
rcases EMetric.mem_closure_iff.1 hx ε hε with ⟨_, ⟨N, rfl⟩, hN⟩

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist x (e N) < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Ici ia, (nearestPt e x_1) x ∈ eball x ε
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
⊢ ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε

Tactic:
intro K

Goal state after:
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
⊢ IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: X : Type u_3
Y : Type u_4
α : Type u_5
inst✝¹⁰ : Zero α
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : OpensMeasurableSpace Y
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetrizableSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : ℕ → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n) x) < u n
x : X × Y
n : ℕ
⊢ dist (f x) ((g n) x) ≤ u n

Tactic:
exact (hg n x).le

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f_sf : α →ₛ β := { toFun := f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

pp: case refine_1
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
x : β
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
· exact ⟨fun _ => f_sf, fun x => tendsto_const_nhds⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
x : β
⊢ MeasurableSet (f ⁻¹' {x})
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f μ
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
g : α → β
g_meas : Measurable g
gt : range g ⊆ t
fg : f =ᵐ[μ] g
⊢ StronglyMeasurable g

Tactic:
exact stronglyMeasurable_iff_measurable_separable.2 ⟨g_meas, t_sep.mono gt⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
⊢ (φ x + if x ∈ {x | φ x + ε ≤ g x} then ε else 0) ≤ g x

Tactic:
split_ifs with hx₂

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
hx₂ : x ∈ {x | φ x + ε ≤ g x}
⊢ φ x + ε ≤ g x

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
hx₂ : x ∉ {x | φ x + ε ≤ g x}
⊢ φ x + 0 ≤ g x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), (⨆ n, (eapprox f n) a) + ⨆ n, (eapprox g n) a ∂μ

Tactic:
simp only [iSup_eapprox_apply, hf, hg]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ n, r * (eapprox f n).lintegral μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
← ENNReal.mul_iSup,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ r * ⨆ i, (eapprox f i).lintegral μ = r * ∫⁻ (a : α), f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case inr
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone fun i ↦ f i a
h_tendsto : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)

Tactic:
exact h_tendsto

Goal state after:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
⊢ CauchySeq (f ∘ u)

Tactic:
rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ CauchySeq (f ∘ u)
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
⊢ CauchySeq (f ∘ u)

Tactic:
rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ CauchySeq (f ∘ u)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : Y
y : X
⊢ ε ≤ glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y)

Tactic:
rw [glueDist_comm]; apply le_glueDist_inl_inr

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

Goal state before:
pp: case mp.inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ ⦃a b : X⦄, dist a b < δX → Prod.map Sum.inl Sum.inl (a, b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < δY → Prod.map Sum.inr Sum.inr (a, b) ∈ s
a : X
b : Y
h :
  (glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < δX ∧ glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < δY) ∧
    glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < ε
⊢ (Sum.inl a, Sum.inr b) ∈ s

Tactic:
exact absurd h.2 (le_glueDist_inl_inr _ _ _ _ _).not_gt

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

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x y + dist y ⋯.some + 1 + dist ⋯.some z

Tactic:
apply_rules [add_le_add, le_rfl, dist_triangle]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(⇑(affineHomeomorph (b - a) a ⋯) '' Icc 0 1) := (affineHomeomorph (b - a) a ⋯).image (Icc 0 1)
⊢ ↑(Icc a b) ≃ₜ ↑(Icc 0 1)

Tactic:
refine (e.trans ?_).symm

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(⇑(affineHomeomorph (b - a) a ⋯) '' Icc 0 1) := (affineHomeomorph (b - a) a ⋯).image (Icc 0 1)
⊢ ↑(⇑(affineHomeomorph (b - a) a ⋯) '' Icc 0 1) ≃ₜ ↑(Icc a b)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + (dist ⋯.some y + dist y z)

Tactic:
apply_rules [add_le_add, le_rfl, dist_triangle]

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

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist ⟨i, x⟩ ⟨j, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨j, z⟩

Tactic:
simp only [Sigma.dist_ne hij, Sigma.dist_same]
        calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
              dist x (Nonempty.some ⟨x⟩) + 1 + (dist (Nonempty.some ⟨z⟩) y + dist y z) := by
            apply_rules [add_le_add, le_rfl, dist_triangle]
          _ = _ := by abel

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

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist ⟨i, x⟩ ⟨j, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨j, z⟩

pp: case inr.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist ⟨i, x⟩ ⟨k, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨k, z⟩

Tactic:
· simp only [Sigma.dist_ne hij, Sigma.dist_same]
        calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
              dist x (Nonempty.some ⟨x⟩) + 1 + (dist (Nonempty.some ⟨z⟩) y + dist y z) := by
            apply_rules [add_le_add, le_rfl, dist_triangle]
          _ = _ := by abel

Goal state after:
case inr.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist ⟨i, x⟩ ⟨k, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨k, z⟩
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∈ s
⊢ ∃ x, Tendsto u atTop (𝓝 x)

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
⊢ ∃ x, Tendsto u atTop (𝓝 x)

Tactic:
· exact ⟨⟨x, xs⟩, tendsto_subtype_rng.2 xlim⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
⊢ ∃ x, Tendsto u atTop (𝓝 x)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ (∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s) → IsOpen[Pi.topologicalSpace] s

Tactic:
· intro h
    refine (isTopologicalBasis_cylinders E).isOpen_iff.2 fun x hx => ?_
    rcases h x hx with ⟨ε, εpos, hε⟩
    obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2 : ℝ) ^ n < ε := exists_pow_lt_of_lt_one εpos one_half_lt_one
    refine ⟨cylinder x n, ⟨x, n, rfl⟩, self_mem_cylinder x n, fun y hy => hε y ?_⟩
    rw [PiNat.dist_comm]
    exact (mem_cylinder_iff_dist_le.1 hy).trans_lt hn

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

Goal state before:
pp: α : Type u_1
t : TopologicalSpace α
inst✝ : PolishSpace α
s : ℕ → Set α
m : ℕ → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h✝ : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
⊢ IsOpen[t'] (⋃ n, s n)

Tactic:
apply isOpen_iUnion

Goal state after:
α : Type u_1
t : TopologicalSpace α
inst✝ : PolishSpace α
s : ℕ → Set α
m : ℕ → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h✝ : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
⊢ ∀ (i : ℕ), IsOpen[t'] (s i)
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol : μ univ < ↑n * μ s
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), μ (f^[m] ⁻¹' s) = μ s
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
have : μ (univ : Set α) < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s) := by simpa [B]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol : μ univ < ↑n * μ s
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), μ (f^[m] ⁻¹' s) = μ s
this : μ univ < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s)
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ SigmaFinite count

Tactic:
simp [sigmaFinite_iff_measure_singleton_lt_top]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
· simp only [x_in_A, h A A_mble x_in_A]

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
⊢ (μ.prod ν) (s ×ˢ t) = μ s * ν t

Tactic:
apply (prod_prod_le s t).antisymm

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
⊢ hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩)

Tactic:
rw [← Equiv.eq_symm_apply]

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
⊢ 1 = hST.equiv.symm (⟨1, hs1⟩, ⟨1, ht1⟩)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
⊢ hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩)

Tactic:
rw [← Equiv.eq_symm_apply]; simp [equiv]

Goal state after: