mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set ↑s
htc : (Subtype.val '' t).Countable
hst : s ⊆ closure[inst✝¹] (Subtype.val '' t)
⊢ Dense t

Tactic:
IsInducing.subtypeVal.dense_iff,

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set ↑s
htc : (Subtype.val '' t).Countable
hst : s ⊆ closure[inst✝¹] (Subtype.val '' t)
⊢ ∀ (x : { x // x ∈ s }), ↑x ∈ closure[inst✝¹] (Subtype.val '' t)
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Tactic:
refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu x hx => ?_⟩

Goal state after:
α : Type u
β : Type v
ι : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ CauchySeq u ↔ Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
rw [cauchySeq_iff_tendsto, Metric.uniformity_eq_comap_nhds_zero, tendsto_comap_iff,
    Function.comp_def]

Goal state after:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun x ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun y ↦ dist y x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a b : α
s : Set α
x : α
inst✝ : Nontrivial α
⊢ (𝓝[≠] x).NeBot

Tactic:
refine forall_mem_nonempty_iff_neBot.1 fun s hs => ?_
  obtain ⟨u, u_open, xu, us⟩ : ∃ u : Set α, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ s := mem_nhdsWithin.1 hs
  obtain ⟨a, b, a_lt_b, hab⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ u := u_open.exists_Ioo_subset ⟨x, xu⟩
  obtain ⟨y, hy⟩ : ∃ y, a < y ∧ y < b := exists_between a_lt_b
  rcases ne_or_eq x y with (xy | rfl)
  · exact ⟨y, us ⟨hab hy, xy.symm⟩⟩
  obtain ⟨z, hz⟩ : ∃ z, a < z ∧ z < x := exists_between hy.1
  exact ⟨z, us ⟨hab ⟨hz.1, hz.2.trans hy.2⟩, hz.2.ne⟩⟩

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
β : Type u_3
inst✝² : LinearOrder β
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
rcases Dense.exists_seq_strictMono_tendsto_of_lt hf hlt with ⟨u, hu, huyxf, hlim⟩
  have huyx (n : ℕ) : u n ∈ Ioo y x := (huyxf n).1
  have huf (n : ℕ) : u n ∈ range f := (huyxf n).2
  choose v hv using huf
  obtain rfl : f ∘ v = u := funext hv
  exact ⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, huyx, hlim⟩

Goal state after:
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
⊢ ∃ a ∈ Ioo y x, l < f a

Tactic:
by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h_nonempty.image _) hl

Goal state after:
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Tactic:
obtain ⟨u, hu⟩ := mem_atTop_sets.mp hs.2

Goal state after:
case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ (b : α), u ≤ b → b ∈ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
hs : IsPreconnected ∅
⊢ ∅ ∈
    {Icc (sInf ∅) (sSup ∅), Ico (sInf ∅) (sSup ∅), Ioc (sInf ∅) (sSup ∅), Ioo (sInf ∅) (sSup ∅), Ici (sInf ∅),
      Ioi (sInf ∅), Iic (sSup ∅), Iio (sSup ∅), univ, ∅}

pp: case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

Tactic:
· apply_rules [Or.inr, mem_singleton]

Goal state after:
case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
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 δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
h : Nontrivial α
⊢ StrictMono f ∨ StrictAnti f

Tactic:
| inr h =>

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

Goal state before:
pp: x : ℤ
r : ℝ
⊢ IsCompact (Icc ⌈↑x - r⌉ ⌊↑x + r⌋)

Tactic:
exact (Set.finite_Icc _ _).isCompact

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
t : Set α
h : (s ∩ t).Nonempty
⊢ diam (s ∪ t) ≤ diam s + diam t

Tactic:
rcases h with ⟨x, ⟨xs, xt⟩⟩

Goal state after:
α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
t : Set α
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f

Tactic:
fun_prop

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: case refine_1
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ g / a ^ k ∈ H

Tactic:
exact Subgroup.div_mem H g_in (Subgroup.zpow_mem H a_in k)

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] fun a ↦ f x₀

Tactic:
fun_prop

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

Goal state before:
pp: x : ℕ
r : ℝ
⊢ IsCompact (Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊)

Tactic:
exact (Set.finite_Icc _ _).isCompact

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

Goal state before:
pp: ⊢ Continuous fun p ↦ max (↑p.1 - ↑p.2) 0

Tactic:
fun_prop

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : MulAction ℚ R
inst✝² : MulAction ℚ≥0 R
inst✝¹ : IsScalarTower ℚ≥0 ℚ R
inst✝ : ContinuousSMul ℚ R
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ ↑p.1 • p.2

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Continuous fun p ↦ p.1 • ↑p.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : (∀ k ∈ s, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s, u k)
h : IsBoundedUnder r f (u k₀) ∧ ∀ x ∈ s, IsBoundedUnder r f (u x)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons k₀ s k₀_notin_s, u k)

Tactic:
simpa only [Finset.sum_cons] using hr _ _ h.1 (ih h.2)

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

Goal state before:
pp: x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
cases x <;> simp_all only [ne_eq, not_false_eq_true, top_add_of_ne_bot, not_true_eq_false,
    IsEmpty.forall_iff]

Goal state after:
case coe
y : EReal
a✝ : ℝ
hy : ¬y = ⊥
hx : ¬↑a✝ = ⊥
⊢ ¬↑a✝ + y = ⊤ → ¬↑a✝ = ⊤ ∧ ¬y = ⊤
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
⊢ ∃ r, ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'

Tactic:
by simpa using! this

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

Goal state before:
pp: case inl
α : Type u_3
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h✝ : IsEmpty α
⊢ Tendsto Finset.Iic atTop atTop

Tactic:
exact tendsto_of_isEmpty

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto f (pure (Fintype.card α)) l

Tactic:
rw [← map_card_atTop_of_fintype, tendsto_map'_iff]
  rfl

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ (∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e) →
    ∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s

Tactic:
· rintro h e he
    rcases exists_nhds_split_inv he with ⟨d, hd, hde⟩
    rcases h d hd with ⟨s, h⟩
    use (s, s)
    rintro ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩
    have : ((∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b) = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b := by
      rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]
    simp only [this]
    exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hgf : Multipliable (⇑g ∘ f) L
a : α
ha : g a = ∏'[L] (i : β), g (f i)
⊢ HasProd f a L

Tactic:
have := hgf.hasProd

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hgf : Multipliable (⇑g ∘ f) L
a : α
ha : g a = ∏'[L] (i : β), g (f i)
this : HasProd (⇑g ∘ f) (∏'[L] (b : β), (⇑g ∘ f) b) L
⊢ HasProd f a L
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
hf : (mulSupport f).Finite
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
simpa [tprod_bot hL, finprod_eq_prod _ hf] using h _

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
⊢ tprod (f ∘ g) = ∏' (b : β), f b

Tactic:
have hf_fin' : ¬ Set.Finite (mulSupport (f ∘ g)) := by
      rwa [this, Set.finite_image_iff hg.injOn] at hf_fin

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ tprod (f ∘ g) = ∏' (b : β), f b
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: 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
x y : X
l : List X
⊢ (zipWith d (y :: l.reverse).reverse (l.reverse ++ [x]).reverse).sum = (zipWith d (x :: l) (l ++ [y])).sum

pp: 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
x y : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length

Tactic:
reverse_append,

Goal state after:
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
x y : X
l : List X
⊢ (zipWith d (y :: l.reverse).reverse ([x].reverse ++ l.reverse.reverse)).sum = (zipWith d (x :: l) (l ++ [y])).sum

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
x y : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ (Finset.univ.sup fun b ↦ edist (Pi.single i x b) (Pi.single i y b)) = edist x y

Tactic:
refine le_antisymm (Finset.sup_le fun j ↦ ?_) (Finset.le_sup_of_le (Finset.mem_univ i) (by simp))

Goal state after:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
j : ι
⊢ j ∈ Finset.univ → edist (Pi.single i x j) (Pi.single i y j) ≤ edist x y
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_7
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousENorm E
X : Type u_8
inst✝ : TopologicalSpace X
f : X → E
a : X
h : ContinuousAt f a
⊢ ContinuousAt (fun x ↦ ‖f x‖ₑ) a

Tactic:
fun_prop

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

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedGroup E
x : E
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {1} ↔ ‖x‖ = 0

Tactic:
← closedBall_zero',

Goal state after:
E : Type u_4
inst✝ : SeminormedGroup E
x : E
⊢ x ∈ closedBall 1 0 ↔ ‖x‖ = 0
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: case refine_1
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.1 p.2 < ε} → (a, b) ∈ u
x : (ι × ι) × κ
hx : (f x.1.1 x.2, f x.1.2 x.2) ∈ {p | dist p.1 p.2 < ε}
⊢ (1, (f x.1.1 x.2)⁻¹ * f x.1.2 x.2) ∈ {p | dist p.1 p.2 < ε}

Tactic:
simpa [dist_eq_norm_inv_mul, norm_div_rev] using hx

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

Goal state before:
pp: case refine_2
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.1 p.2 < ε} → (a, b) ∈ u
x : (ι × ι) × κ
hx : (1 x.2, (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) x.1 x.2) ∈ {p | dist p.1 p.2 < ε}
⊢ (f x.1.1 x.2, f x.1.2 x.2) ∈ {p | dist p.1 p.2 < ε}

Tactic:
simpa [dist_eq_norm_inv_mul, norm_div_rev] using hx

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a - ε ≤ f n
⊢ a - f n ≤ ε

Tactic:
rw [tsub_le_iff_right] at hN_left ⊢

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a ≤ f n + ε
⊢ a ≤ ε + f n
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_2
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : β
hn : f n ≤ ε
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
exact ⟨n, fun m hm ↦ (hf hm).trans hn⟩

Goal state after:
Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : ContinuousConstSMul R M
inst✝³ : Semiring S
inst✝² : AddCommMonoid N
inst✝¹ : Module S N
inst✝ : TopologicalSpace N
σ : R →+* S
f : M →SL[σ] N
hf : ∀ (x y : M), Inseparable x y → f x = f y
⊢ Continuous[_, inst✝] (lift (⇑f) hf)

Tactic:
fun_prop

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

Goal state before:
pp: b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (∞, ↑b)) (𝓝 (∞ - ↑b))

Tactic:
by
    rw [top_sub_coe, tendsto_nhds_top_iff_nnreal]
    refine fun x => ((lt_mem_nhds <| @coe_lt_top (b + 1 + x)).prod_nhds
      (ge_mem_nhds <| coe_lt_coe.2 <| lt_add_one b)).mono fun y hy => ?_
    grw [lt_tsub_iff_left, hy.2]
    exact hy.1

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

Goal state before:
pp: α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous₂ (pkg.extend₂ pkg' f)

Tactic:
by
  rw [uniformContinuous₂_def, AbstractCompletion.extend₂, uncurry_curry]
  apply uniformContinuous_extend

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
⊢ ((𝓤 α).lift fun s ↦ (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ (𝓤 α).lift' gen

Tactic:
have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val

Goal state after:
α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.2 ×ˢ ↑p.1 = map Prod.swap (↑p.1 ×ˢ ↑p.2)
⊢ ((𝓤 α).lift fun s ↦ (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ (𝓤 α).lift' gen
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
⊢ ContinuousOn (fun x ↦ (a, x)) {x | x ≠ ∞}

Tactic:
fun_prop

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

Goal state before:
pp: a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous fun x ↦ (x, a)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
a : α
r : ℝ≥0∞
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun y ↦ edist y a

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous fun x ↦ ↑K * x
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ s
⊢ ContinuousOn (fun x ↦ edist (f x) (f y)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
fun_prop

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous fun x ↦ ↑K * x
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ s
⊢ ContinuousOn (fun x ↦ ↑K * edist x y) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
fun_prop

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous fun x ↦ ↑K * x
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContinuousOn (fun y ↦ edist (f x) (f y)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
fun_prop

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

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous fun x ↦ ↑K * x
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContinuousOn (fun y ↦ ↑K * edist x y) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
fun_prop

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

Goal state before:
pp: t : ℝ≥0∞
t_ne_top : t ≠ ∞
⊢ Continuous (min t)

Tactic:
fun_prop

Goal state after: