mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : s ∈ cobounded α
⊢ s ∈ Filter.atTop

Tactic:
← compl_compl s,

Goal state after:
α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : sᶜᶜ ∈ cobounded α
⊢ s ∈ Filter.atTop
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
⊢ ((∃ i, True ∧ Iic i ⊆ s) ∧ ∃ i, True ∧ Ici i ⊆ s) → s ∈ cobounded α

Tactic:
← compl_compl s,

Goal state after:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
⊢ ((∃ i, True ∧ Iic i ⊆ sᶜᶜ) ∧ ∃ i, True ∧ Ici i ⊆ sᶜᶜ) → sᶜᶜ ∈ cobounded α
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
⊢ (∃ i, True ∧ Ici i ⊆ s) → s ∈ cobounded α

Tactic:
← compl_compl s,

Goal state after:
α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
⊢ (∃ i, True ∧ Ici i ⊆ sᶜᶜ) → sᶜᶜ ∈ cobounded α
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c = x d
this : c = f (x d)
⊢ c = d

Tactic:
hfx _ hd

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c = x d
this : c = d
⊢ c = d
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x / y‖ = ‖y‖

Tactic:
rw [div_eq_mul_inv, norm_mul_eq_norm_right _ h, norm_inv']

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
y : E
ε : ℝ
⊢ {x | ‖x⁻¹ * y‖ < ε} = {x | ‖x / y‖ < ε}

Tactic:
norm_inv_mul

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
⊢ {x | x / a ∈ closedBall 1 r} = closedBall a r

Tactic:
by
  ext x
  rw [mem_closedBall_iff_norm'']
  simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a * b ∈ ball a r ↔ ‖b‖ < r

Tactic:
by
  rw [mem_ball_iff_norm'']
  simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a⁻¹ * b‖ < r
⊢ 0 < ↑n

Tactic:
norm_cast

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ∃ f,
    Monotone f ∧
      ⋃ i, f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)

Tactic:
by
  obtain rfl | ⟨x, -⟩ := U.eq_empty_or_nonempty
  · exact ⟨fun i ↦ ∅, monotone_const, by simp_all⟩
  refine ⟨fun i ↦ U ∩ ball x i, fun i j hij ↦ ?_, ?_, fun i ↦ ⟨?_, hU.inter isOpen_ball⟩⟩
  · exact inter_subset_inter_right _ (ball_subset_ball (Nat.cast_le.2 hij))
  · simp [← inter_iUnion]
  · exact isBounded_ball.subset inter_subset_right

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsDirectedOrder α
k : α
⊢ map (fun a ↦ a - k) atTop = atTop

Tactic:
simp_rw [sub_eq_add_neg]
  apply map_add_atTop_eq

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0 * 1

Tactic:
rw [mul_one]

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
hab : b < a
⊢ f '' Icc a b = Icc (f a) (f b)

Tactic:
· simp [not_le.mpr hab, not_le.mpr (hf hab)]

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: m n : ℤ
⊢ |↑m - ↑n| = ↑|m - n|

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |↑m - ↑n|

Tactic:
norm_cast

Goal state after:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |m - n|
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ (K ∩ s).Finite

Tactic:
refine (IsCompact.finite ?_ ?_).subset (Set.inter_subset_inter_left s subset_closure)
  · exact hK.isCompact_closure.inter_right hs
  · exact hsd.mono Set.inter_subset_right

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
rcases eq_or_ne J ⊥ with rfl | hJ

Goal state after:
case inr.inl
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I : Ideal R
hI : I ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ ⊥) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal ⊥)

case inr.inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ + ↑a✝).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
norm_cast

Goal state after:
case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑(a✝¹ + a✝)).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
H : ∀ {I' : Ideal R}, I' ≠ ⊥ → FiniteMultiplicity p.asIdeal I'
⊢ ↑(min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)) =
    min ↑(multiplicity p.asIdeal I) ↑(multiplicity p.asIdeal J)

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, ⨆ i_1, (⇑f)^[i_1 + i.succ] a =
    (⨅ i, ⨅ (_ : 0 < i), ⨆ i_1, (⇑f)^[i_1 + i] a) ⊓ ⨅ i, ⨅ (_ : ¬0 < i), ⨆ i_1, (⇑f)^[i_1 + i] a

Tactic:
simp only [not_lt, Nat.le_zero, iInf_iInf_eq_left, add_zero, iInf_nat_gt_zero_eq, left_eq_inf]

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ i, ⨆ i_1, (⇑f)^[i_1 + i.succ] a ≤ ⨆ i, (⇑f)^[i] a
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : ∀ (x y : α), edist (f x) (f y) ≤ edist x y
x y : α
⊢ edist (f x) (f y) ≤ ↑1 * edist x y

Tactic:
by simp only [ENNReal.coe_one, one_mul, h]

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

Goal state before:
pp: case bot
b : ℝ
⊢ ⊥ + ↑b - ↑b = ⊥

Tactic:
norm_cast

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

Goal state before:
pp: case coe
b a✝ : ℝ
⊢ ↑a✝ + ↑b - ↑b = ↑a✝

Tactic:
norm_cast

Goal state after:
case coe
b a✝ : ℝ
⊢ a✝ + b - b = a✝
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
b : ℝ
⊢ ⊤ + ↑b - ↑b = ⊤

Tactic:
norm_cast

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

Goal state before:
pp: case bot
b : ℝ
⊢ ↑b - (⊥ + ↑b) = -⊥

Tactic:
norm_cast

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

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

Tactic:
norm_cast

Goal state after:
case coe
b a✝ : ℝ
⊢ b - (a✝ + b) = -a✝
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
b : ℝ
⊢ ↑b - (⊤ + ↑b) = -⊤

Tactic:
norm_cast

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

Goal state before:
pp: case pos
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : y = ⊤
⊢ t - z ≠ ⊥

Tactic:
exact ne_bot_of_le_ne_bot (by simp) (sub_pos.mpr h').le

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

Goal state before:
pp: case neg
x z t : EReal
h' : z < t
hx_top : x ≠ ⊤
y : ℝ
h : x ≤ ↑y
hy_bot : ↑y ≠ ⊥
hy_top : ¬↑y = ⊤
hxy : x = ↑y
htz_top : ¬t - z = ⊤
⊢ ↑y < ↑y + ↑(t - z).toReal

Tactic:
norm_cast

Goal state after:
case neg
x z t : EReal
h' : z < t
hx_top : x ≠ ⊤
y : ℝ
h : x ≤ ↑y
hy_bot : ↑y ≠ ⊥
hy_top : ¬↑y = ⊤
hxy : x = ↑y
htz_top : ¬t - z = ⊤
⊢ y < y + (t - z).toReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe_coe
x✝ y✝ : ℝ
⊢ (↑x✝ * ↑y✝).toReal = (↑x✝).toReal * (↑y✝).toReal

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
inst✝ : Fintype α
⊢ Tendsto Finset.card atTop (pure (Fintype.card α))

Tactic:
by
  rw [Tendsto, map_card_atTop_of_fintype]

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

Goal state before:
pp: case coe_coe
x✝ y✝ : ℝ
⊢ -↑x✝ * ↑y✝ = -(↑x✝ * ↑y✝)

Tactic:
norm_cast

Goal state after:
case coe_coe
x✝ y✝ : ℝ
⊢ -x✝ * y✝ = -(x✝ * y✝)
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case inl
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
b : β
⊢ f b ∈ (L.map f).support ↔ f b ∈ ⇑f '' L.support

pp: case inr
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range ⇑f
⊢ c ∈ (L.map f).support ↔ c ∈ ⇑f '' L.support

Tactic:
· simp [support]

Goal state after:
case inr
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range ⇑f
⊢ c ∈ (L.map f).support ↔ c ∈ ⇑f '' L.support
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
h : ¬Multipliable f L
⊢ ∏'[L] (b : β), f b = 1

Tactic:
by
  simp [tprod_def, h]

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

Goal state before:
pp: f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n ↦ ↑(f n)) (↑a + ∑ i ∈ Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)

Tactic:
norm_cast

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

Goal state before:
pp: case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
exact iSup_pow_of_ne_zero hn _

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

Goal state before:
pp: case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
exact iSup_pow_of_ne_zero hn _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)

Tactic:
norm_cast

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔ ∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))

Tactic:
norm_cast

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.eball x r = Metric.eball (h.symm x) r

Tactic:
by
  rw [← h.isometry.preimage_eball (h.symm x) r, h.apply_symm_apply]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r

Tactic:
by
  rw [← h.isometry.preimage_closedBall (h.symm x) r, h.apply_symm_apply]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
s : Set X
h : IsSeqCompact s
⊢ TotallyBounded s

Tactic:
intro V V_in
  unfold IsSeqCompact at h
  contrapose! h
  obtain ⟨u, u_in, hu⟩ : ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ ∀ n m, m < n → u m ∉ ball (u n) V := by
    simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h
    simpa only [forall_and, forall_mem_image, not_and] using! seq_of_forall_finite_exists h
  refine ⟨u, u_in, fun x _ φ hφ huφ => ?_⟩
  obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V :=
    huφ.cauchySeq.mem_entourage V_in
  exact hu (φ <| N + 1) (φ N) (hφ <| Nat.lt_add_one N) (hN (N + 1) N N.le_succ le_rfl)

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
u : Filter α
a : ℝ≥0
hf : ∀ (x : α), f x ≠ ∞
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 (↑a).toNNReal) ↔ Tendsto f u (𝓝 ↑(↑a).toNNReal)

Tactic:
exact tendsto_toNNReal_iff coe_ne_top hf

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (pkg.coe a)
⊢ pkg.extend f = g

Tactic:
by
  apply pkg.funext pkg.continuous_extend hg.continuous
  simpa only [pkg.extend_coe hf] using h

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous[inst✝².toTopologicalSpace, inst✝¹] f
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
x : α
⊢ (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x

Tactic:
simp only [Function.comp_apply, compare_coe, IsDenseInducing.extend_eq _ cont_f]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Inseparable a b ↔ Inseparable f g

Tactic:
rw [inseparable_iff, (ha.comp tendsto_fst).inseparable_iff_uniformity (hb.comp tendsto_snd)]

Goal state after:
α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Tendsto (fun x ↦ ((id ∘ Prod.fst) x, (id ∘ Prod.snd) x)) (↑f ×ˢ ↑g) (𝓤 α) ↔ ↑f ×ˢ ↑g ≤ 𝓤 α
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : NormedGroup E
a : E
⊢ Tendsto (fun x ↦ ‖x⁻¹ * a‖) (𝓝[≠] a) (𝓝[>] 0)

Tactic:
apply (tendsto_norm_inv_mul_self a).inf

Goal state after:
E : Type u_4
inst✝ : NormedGroup E
a : E
⊢ Tendsto (fun a_1 ↦ ‖a_1⁻¹ * a‖) (𝓟 {a}ᶜ) (𝓟 (Set.Ioi 0))
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs'✝ : (drop (M + 1) L).sum ≤ (take (M + 1) L).sum
hMs' : 2 * (drop (M + 1) L).sum ≤ L.sum
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum

Tactic:
convert! hMs'

Goal state after:
case e'_4
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs'✝ : (drop (M + 1) L).sum ≤ (take (M + 1) L).sum
hMs' : 2 * (drop (M + 1) L).sum ≤ L.sum
⊢ zipWith d (drop M l) (drop (M + 1) l ++ [y]) = drop (M + 1) L
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔ ∀ (x y : α), ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)

Tactic:
norm_cast

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔
    ∀ x ∈ s, ∀ y ∈ s, ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∈ {p | dist p.1 p.2 < ↑(1 / 2) ^ (n + 1)}
⊢ x ∈ U n

Tactic:
mem_ofPred_eq

Goal state after:
case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : dist x.1 x.2 < ↑(1 / 2) ^ (n + 1)
⊢ x ∈ U n
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
⊢ LipschitzWith K (hs.extend f)

Tactic:
have : IsClosed {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by
    have : Continuous (hs.extend f) := (hs.uniformContinuous_extend hf.uniformContinuous).continuous
    apply isClosed_le (by fun_prop)
    exact (ENNReal.continuous_const_mul (by simp)).comp (by fun_prop)
  have : Dense {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by
    apply (hs.prod hs).mono
    rintro ⟨x, y⟩ ⟨hx, hy⟩
    have Ax : hs.extend f x = f ⟨x, hx⟩ := hs.extend_eq hf.continuous ⟨x, hx⟩
    have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩
    simp only [Set.mem_ofPred_eq, Ax, Ay]
    exact hf ⟨x, hx⟩ ⟨y, hy⟩
  simpa only [Dense, IsClosed.closure_eq, Set.mem_ofPred_eq, Prod.forall] using! this

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

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ c⁻¹ • closedEBall x r = closedEBall (c⁻¹ • x) r

Tactic:
smul_closedEBall

Goal state after:
G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ closedEBall (c⁻¹ • x) r = closedEBall (c⁻¹ • x) r
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ ↑(nndist (a₁ * a₂) (b₁ * b₂)) ≤ ↑(nndist a₁ b₁) + ↑(nndist a₂ b₂)

Tactic:
norm_cast

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : ⟨‖x‖, ⋯⟩ < ⟨‖y‖, ⋯⟩
⊢ ∃ a, ⟨‖x‖, ⋯⟩ < a ∧ a < ⟨‖y‖, ⋯⟩

Tactic:
let ⟨z, h⟩ := exists_lt_norm_lt α (norm_nonneg _) hxy

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : ⟨‖x‖, ⋯⟩ < ⟨‖y‖, ⋯⟩
z : α
h : ‖x‖ < ‖z‖ ∧ ‖z‖ < ↑⟨‖y‖, ⋯⟩
⊢ ∃ a, ⟨‖x‖, ⋯⟩ < a ∧ a < ⟨‖y‖, ⋯⟩
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
f g : α →ᵈ α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (f * g) = ratio f * ratio g

Tactic:
exact ratio_comp' h

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ ⇑(e ^ n).toEquiv = (⇑e)^[n]

Tactic:
← toPerm_apply,

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ ⇑(toPerm (e ^ n)) = (⇑e)^[n]