mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ closedBall x δ ⊆ cthickening δ {x}

Tactic:
simp only [cthickening_singleton x hδ, Subset.rfl]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
rcases ht with ⟨y, yt⟩

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffDist s t ≤ diam (s ∪ t)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ∞
A :
  Tendsto (fun r ↦ μ (cthickening r s)) (𝓝[>] 0)
    (𝓝 (μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
a✝ : ℝ
hr : a✝ ∈ Iic 0
⊢ μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = μ (cthickening a✝ s)

Tactic:
rw [cthickening_of_nonpos hr]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s → ((s.sup f) a = s.sup fun c ↦ (f c) a) → ((insert a_1 s).sup f) a = (insert a_1 s).sup fun c ↦ (f c) a

Tactic:
intro a s _ ih

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s✝ : Finset γ
a✝¹ : α
a : γ
s : Finset γ
a✝ : a ∉ s
ih : (s.sup f) a✝¹ = s.sup fun c ↦ (f c) a✝¹
⊢ ((insert a s).sup f) a✝¹ = (insert a s).sup fun c ↦ (f c) a✝¹
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : LinearOrder α
a b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
h : a < b
this : a < b + c
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d

Tactic:
tauto

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : LinearOrder α
a b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
h : a < b
this : a ≤ b + c
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k = f a

Tactic:
refine le_antisymm (iSup_le fun i => iSup_le fun hi => hi) (le_of_not_gt ?_)

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ¬⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case inl
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : IsEmpty α
this : ∀ (b : δ), (range fun i ↦ f i b) = ∅
⊢ MeasurableSet {b | BddAbove (range fun i ↦ f i b)}

Tactic:
simp [this]

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

Goal state before:
pp: q : ℚ
⊢ ↑q < ↑q + 1

Tactic:
linarith

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

Goal state before:
pp: q : ℚ
⊢ ↑q < ↑q + 2

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun i ↦ if p i then a else b) L F
i : ι
hi : p i ∧ ¬a = b
⊢ p i ↔ q

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun i ↦ if p i then a else b) L G
i : ι
hi : ¬p i ∧ ¬b = a
⊢ p i ↔ q

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun i ↦ if hi : i ∈ s then mk (f i) ⋯ else fun _b ↦ sSup ∅
this : ∀ i ∈ s, Measurable (g i)
i : ι
hi : i ∈ s
⊢ ∀ᵐ (b : δ) ∂μ, f i b = g i b

Tactic:
by simpa [g, hi] using! (hf i hi).ae_eq_mk

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ b - s ≤ b - r

Tactic:
linarith

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ b + r ≤ b + s

Tactic:
linarith

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

Goal state before:
pp: μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NullSingletonClass μ
b r : ℝ
hr : r < 0
⊢ ¬b - r ≤ b + r

Tactic:
linarith

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 < ε
N : ℕ
hN : edist (e N) x < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Ici ia, (nearestPt e x_1) x ∈ eball x ε

Tactic:
exact ⟨N, trivial, fun n hn => (edist_nearestPt_le e x hn).trans_lt hN⟩

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)
⊢ Tendsto (fun N ↦ (nearestPt e N) x) atTop (𝓝 x)

Tactic:
by
  refine (atTop_basis.tendsto_iff nhds_basis_eball).2 fun ε hε => ?_
  rcases EMetric.mem_closure_iff.1 hx ε hε with ⟨_, ⟨N, rfl⟩, hN⟩
  rw [edist_comm] at hN
  exact ⟨N, trivial, fun n hn => (edist_nearestPt_le e x hn).trans_lt hN⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this✝ : Nonempty ↑s
this : ∀ (n : ℕ), Nat.casesOn n y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
⊢ (approxOn f hf s y₀ h₀ n) x ∈ s

Tactic:
by apply this

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

Goal state before:
pp: case he
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)
hK : IsCompact K
⊢ ∃ g s, MeasurableSet s ∧ ∅ ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε

Tactic:
exact ⟨0, ∅, by simp⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ ∫⁻ (x : α), 1 ∂μ = μ univ

Tactic:
lintegral_const,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ 1 * μ univ = μ univ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
⊢ ∫⁻ (x : α) in s, c ∂μ = c * μ s

Tactic:
lintegral_const,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
⊢ c * (μ.restrict s) univ = c * μ s
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
⊢ AEStronglyMeasurable (fun x ↦ g (f x)) μ ↔ AEStronglyMeasurable f μ

Tactic:
let := pseudoMetrizableSpacePseudoMetric γ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ AEStronglyMeasurable (fun x ↦ g (f x)) μ ↔ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m m0 : MeasurableSpace α
μ : Measure α
hf : StronglyMeasurable f
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ (hf.approxBounded c n) x) atTop (𝓝 (f x))

Tactic:
filter_upwards [hf_bound] with x hfx using tendsto_approxBounded_of_norm_le hf hfx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
x : α
hx : x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
hx_mem : x ∈ sᶜ
⊢ s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
rw [Set.mem_compl_iff] at hx_mem

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
x : α
hx : x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
hx_mem : x ∉ s
⊢ s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ ∫⁻ (x : α) in {x | f x = r}, r ∂μ = r * μ {x | f x = r}

Tactic:
lintegral_const,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ r * (μ.restrict {x | f x = r}) univ = r * μ {x | f x = r}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ Monotone fun n ↦ (eapprox f n).lintegral μ

Tactic:
· intro i j h
          exact SimpleFunc.lintegral_mono (monotone_eapprox _ h) le_rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ Monotone fun n ↦ (eapprox g n).lintegral μ

Tactic:
· intro i j h
          exact SimpleFunc.lintegral_mono (monotone_eapprox _ h) le_rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
⊢ (StronglyMeasurable fun x ↦ g (f x)) ↔ StronglyMeasurable f

Tactic:
let := pseudoMetrizableSpacePseudoMetric γ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ (StronglyMeasurable fun x ↦ g (f x)) ↔ StronglyMeasurable f
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ

Tactic:
refine lintegral_mono fun x => ENNReal.ofReal_le_ofReal ?_

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ f x ≤ ‖f x‖
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace (E × E) := borel (E × E)
this✝ : BorelSpace (E × E)
⊢ MeasurableSet {a | f a = g a}

Tactic:
exact (hf.prodMk hg).measurable isClosed_diagonal.measurableSet

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

Tactic:
hνs,

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * 0
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PerfectSpace α
U : Set α
hU : IsOpen[inst✝¹] U
⊢ Preperfect U

Tactic:
simpa using PerfectSpace.univ_preperfect.open_inter hU

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

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
this : (fun p ↦ u (↑p.1) p.2) = (fun p ↦ u (↑p.2) p.1) ∘ Prod.swap
⊢ Measurable ((fun p ↦ u (↑p.2) p.1) ∘ Prod.swap)

Tactic:
@measurable_swap_iff α (↥(t_sf n).range) β m

Goal state after:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
this : (fun p ↦ u (↑p.1) p.2) = (fun p ↦ u (↑p.2) p.1) ∘ Prod.swap
⊢ Measurable fun p ↦ u (↑p.2) p.1
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
this : (fun p ↦ u (↑p.1) p.2) = (fun p ↦ u (↑p.2) p.1) ∘ Prod.swap
⊢ Measurable fun p ↦ u (↑p.2) p.1

Tactic:
exact measurable_from_prod_countable_left fun j => h j

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mp.left
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ 1 / 2 ≤ t

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mp.right
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ t ≤ 1

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mpr.left
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 0 ≤ 2 * t - 1

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mpr.right
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 2 * t - 1 ≤ 1

Tactic:
linarith

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ ⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) ≤ 0

Tactic:
have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ ⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) ≤ 0
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ Subtype.val ⁻¹' Iic ↑x = Icc 0 x

Tactic:
rw [preimage_subtype_val_Iic]

Goal state after:
x : ↑I
⊢ Iic x = Icc 0 x
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace Y := upgradeIsCompletelyPseudoMetrizable Y
this : PseudoMetricSpace X := ⋯.comapPseudoMetricSpace
⊢ CompleteSpace X

Tactic:
completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace Y := upgradeIsCompletelyPseudoMetrizable Y
this : PseudoMetricSpace X := ⋯.comapPseudoMetricSpace
⊢ IsComplete (range f)
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝ : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
⊢ CompleteSpace X

Tactic:
completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝ : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
⊢ IsComplete (range f)
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case pos
a b : ℝ
x y z : ↑(Icc a b)
h : ↑z - ↑x = 0
hxy : ↑x ≤ ↑y
hyz : ↑y ≤ ↑z
⊢ ↑y = ↑x

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝¹ : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this✝ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ CompleteSpace α

Tactic:
completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝¹ : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this✝ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ IsComplete (range f)
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ι : Sort u_1
a b : ℝ
h : a ≤ b
c : ι → Set ↑(Icc a b)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
⊢ ∃ t, ↑(t 0) = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, ↑(t n) = b) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i

Tactic:
by
  obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
  have hδ := half_pos δ_pos
  refine ⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n ↦ ?_⟩
  obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n) trivial
  exact ⟨i, fun t ht ↦ hsub ((abs_sub_addNSMul_le h hδ.le n ht).trans_lt <| half_lt_self δ_pos)⟩

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

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
this : (∀ i < n, y i = x i) ↔ n ≤ firstDiff y x
⊢ y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n

Tactic:
simpa [dist_eq_of_ne hne]

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 j : ι
h : i ≠ j
x : E i
y : E j
⊢ 1 ≤ dist ⟨i, x⟩ ⟨j, y⟩

Tactic:
rw [Sigma.dist_ne h x y]
  linarith [@dist_nonneg _ _ x (Nonempty.some ⟨x⟩), @dist_nonneg _ _ (Nonempty.some ⟨y⟩) y]

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

Goal state before:
pp: case mpr.inr
E : ℕ → Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ y ∈ cylinder x (firstDiff x y)

Tactic:
firstDiff_comm

Goal state after:
case mpr.inr
E : ℕ → Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ y ∈ cylinder x (firstDiff y x)
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
⊢ 0 < ε / 2

Tactic:
linarith

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

Goal state before:
pp: case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ ε / 2 < ε

Tactic:
linarith

Goal state after: