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

Goal state before:
pp: case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : ContinuousAt (fun p ↦ p.1 * p.2) (x, l.prod)
⊢ Tendsto (fun p ↦ p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))

Tactic:
ContinuousAt,

Goal state after:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, l.prod)) (𝓝 ((x, l.prod).1 * (x, l.prod).2))
⊢ Tendsto (fun p ↦ p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case inr.refine_1
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
H : (f i) x z ≤ (f i) x y
⊢ ∃ b ∈ s, (f i) x z ≤ (f b) x y

pp: case inr.refine_2
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
H : (f i) x z ≤ (f i) y z
⊢ ∃ b ∈ s, (f i) x z ≤ (f b) y z

Tactic:
<;>

Goal state after:
case inr.refine_1
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
H : (f i) x z ≤ (f i) x y
⊢ ∃ b ∈ s, (f i) x z ≤ (f b) x y

case inr.refine_2
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
H : (f i) x z ≤ (f i) y z
⊢ ∃ b ∈ s, (f i) x z ≤ (f b) y z
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ ContinuousAt (fun p ↦ insertIdx p.1 i p.2) (a, l)

Tactic:
ContinuousAt,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ Tendsto (fun p ↦ insertIdx p.1 i p.2) (𝓝 (a, l)) (𝓝 (insertIdx (a, l).1 i (a, l).2))
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ ContinuousAt (eraseIdx i) ⟨l, hl⟩

Tactic:
ContinuousAt,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (eraseIdx i) (𝓝 ⟨l, hl⟩) (𝓝 (eraseIdx i ⟨l, hl⟩))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mp
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ →
    (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)

pp: case mpr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂) →
    (Homotopic.setoid N x) a₁ a₂

Tactic:
<;>

Goal state after:
case mp
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ →
    (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)

case mpr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂) →
    (Homotopic.setoid N x) a₁ a₂
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
i : N
iH : y i = 0
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x

pp: case inr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
i : N
iH : y i = 1
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x

Tactic:
<;>

Goal state after:
case inl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
i : N
iH : y i = 0
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x

case inr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
i : N
iH : y i = 1
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inl.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 0
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x

pp: case inr.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 1
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x

Tactic:
<;>

Goal state after:
case inl.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 0
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x

case inr.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 1
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mp
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ →
    (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂)

pp: case mpr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂) →
    (Homotopic.setoid N x) a₁ a₂

Tactic:
<;>

Goal state after:
case mp
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ →
    (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂)

case mpr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂) →
    (Homotopic.setoid N x) a₁ a₂
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ↑t ≤ 2⁻¹
⊢ Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default))) = fun x ↦
    Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t)

pp: case refine_2
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ¬↑t ≤ 2⁻¹
⊢ Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default) - 1)) = fun x ↦
    Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t - 1)

Tactic:
<;>

Goal state after:
case refine_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ↑t ≤ 2⁻¹
⊢ Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default))) = fun x ↦
    Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t)

case refine_2
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ¬↑t ≤ 2⁻¹
⊢ Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default) - 1)) = fun x ↦
    Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t - 1)
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: case h₁
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ edist x y ≤ edist (x, s) (y, t)

pp: case h₂
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ hausdorffEDist ↑s ↑t ≤ edist (x, s) (y, t)

Tactic:
<;>

Goal state after:
case h₁
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ edist x y ≤ edist (x, s) (y, t)

case h₂
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ hausdorffEDist ↑s ↑t ≤ edist (x, s) (y, t)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
⊢ 0 ≤ diam univ

pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
⊢ 0 ≤ diam univ

Tactic:
<;>

Goal state after:
case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
⊢ 0 ≤ diam univ

case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
⊢ 0 ≤ diam univ
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
⊢ externalCoveringNumber δ A ≤ externalCoveringNumber ε A

Tactic:
simp_rw [externalCoveringNumber]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
⊢ ⨅ C, ⨅ (_ : IsCover δ A C), C.encard ≤ ⨅ C, ⨅ (_ : IsCover ε A C), C.encard
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ 1 ≤ 2

pp: case hbc
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ 1 ≤ 2

Tactic:
<;>

Goal state after:
case hbc
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ 1 ≤ 2

case hbc
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ 1 ≤ 2
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := ⋯
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋯
t : Closeds α := ⋯
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ n + l ≤ n + l

pp: case a
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := ⋯
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋯
t : Closeds α := ⋯
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ n + l ≤ n + l + 1

Tactic:
<;>

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := ⋯
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋯
t : Closeds α := ⋯
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ n + l ≤ n + l

case a
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := ⋯
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋯
t : Closeds α := ⋯
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ n + l ≤ n + l + 1
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case h₁
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, z) ≤ ↑(maxVar X Y) * dist x z

pp: case h₂
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (t, y) ≤ ↑(maxVar X Y) * dist t y

Tactic:
<;>

Goal state after:
case h₁
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, z) ≤ ↑(maxVar X Y) * dist x z

case h₂
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (t, y) ≤ ↑(maxVar X Y) * dist t y
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ y ∈ maximalSeparatedSet ε A, (x, y) ∉ {x | edist x.1 x.2 ≤ ↑ε}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
⊢ ∀ y ∈ maximalSeparatedSet ε A, ↑ε < edist x y

Tactic:
simpa using h_dist

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

Goal state before:
pp: case h₂
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
f : ↑D → ↑C := ⋯
hf' : ∀ (x : ↑D), edist ↑x ↑(f x) ≤ ↑ε
x y : ↑D
hxy : f x = f y
⊢ edist ↑(f x) ↑y ≤ ↑ε

Tactic:
· simpa [edist_comm, hxy] using hf' y

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f < ∞ ↔ MemHolder r f

Tactic:
refine ⟨fun h => ?_,
    fun hf => let ⟨C, hC⟩ := hf; iInf_lt_top.2 ⟨C, iInf_lt_top.2 ⟨hC, coe_lt_top⟩⟩⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f < ∞
⊢ MemHolder r f
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case none
α : Type u_1
inst✝ : EDist α
ι : Type u_3
s : ι → Set α
⊢ (⋃ i ∈ none, s i).einfsep = ⨅ i ∈ none, (s i).einfsep

pp: case some
α : Type u_1
inst✝ : EDist α
ι : Type u_3
s : ι → Set α
val✝ : ι
⊢ (⋃ i ∈ some val✝, s i).einfsep = ⨅ i ∈ some val✝, (s i).einfsep

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : EDist α
ι : Type u_3
s : ι → Set α
⊢ (⋃ i ∈ none, s i).einfsep = ⨅ i ∈ none, (s i).einfsep

case some
α : Type u_1
inst✝ : EDist α
ι : Type u_3
s : ι → Set α
val✝ : ι
⊢ (⋃ i ∈ some val✝, s i).einfsep = ⨅ i ∈ some val✝, (s i).einfsep
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b

pp: case inl.inr
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist a b ≤ edist a b ∨ edist b a ≤ edist a b

pp: case inr.inl
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b

pp: case inr.inr
α : Type u_1
inst✝ : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝ : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b

case inl.inr
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist a b ≤ edist a b ∨ edist b a ≤ edist a b

case inr.inl
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b

case inr.inr
α : Type u_1
inst✝ : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b

pp: case inr.inr
α : Type u_1
inst✝ : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝ : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b

case inr.inr
α : Type u_1
inst✝ : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r f) * edist x₁ x₂ ^ ↑r

pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r f) * edist x₁ x₂ ^ ↑r

Tactic:
· simp only [hx, edist_self, zero_le]

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r f) * edist x₁ x₂ ^ ↑r
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z y ∨ s.einfsep ≤ edist z y

Tactic:
exact Or.inl (iInf_le_of_le _ (iInf₂_le hy hyz.symm))

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ∞
⊢ s.Subsingleton

Tactic:
rw [einfsep_top] at hs
  exact fun _ hx _ hy => of_not_not fun hxy => edist_ne_top _ _ (hs _ hx _ hy hxy)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < s.einfsep

Tactic:
by
  cases nonempty_fintype s
  by_cases hs : s.Nontrivial
  · rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩
    exact hxy'.symm ▸ edist_pos.2 hxy
  · rw [not_nontrivial_iff] at hs
    exact hs.einfsep.symm ▸ WithTop.top_pos

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
⊢ s.infsep = if s.Nontrivial then ⨅ d, uncurry dist ↑d else 0

Tactic:
split_ifs with hs

Goal state after:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ s.infsep = ⨅ d, uncurry dist ↑d

case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : ¬s.Nontrivial
⊢ s.infsep = 0
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
⊢ s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (uncurry dist) else 0

Tactic:
split_ifs with hs

Goal state after:
case pos
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

case neg
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ s.infsep = 0
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
⊢ s.infsep = if hs : s.Nontrivial then ⋯.toFinset.inf' ⋯ (uncurry dist) else 0

Tactic:
split_ifs with hs

Goal state after:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
⊢ s.infsep = ⋯.toFinset.inf' ⋯ (uncurry dist)

case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : ¬s.Nontrivial
⊢ s.infsep = 0
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
⊢ (↑s).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0

Tactic:
split_ifs with hs

Goal state after:
case pos
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : s.offDiag.Nonempty
⊢ (↑s).infsep = s.offDiag.inf' hs (uncurry dist)

case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : ¬s.offDiag.Nonempty
⊢ (↑s).infsep = 0
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)

Tactic:
have IΦ' : Isometry Φ' := fun x y => ha x y

Goal state after:
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case toSnowflaking.toSnowflaking.hx_nonneg
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ 0 ≤ dist x✝¹ x✝

pp: case toSnowflaking.toSnowflaking.hp_nonneg
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ 0 ≤ α

Tactic:
<;>

Goal state after:
case toSnowflaking.toSnowflaking.hx_nonneg
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ 0 ≤ dist x✝¹ x✝

case toSnowflaking.toSnowflaking.hp_nonneg
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ 0 ≤ α
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case pos
a : Prop
h✝ : a
⊢ (Iic a)ᶜ ∈ {∅, {True}}

pp: case neg
a : Prop
h✝ : ¬a
⊢ (Iic a)ᶜ ∈ {∅, {True}}

Tactic:
<;>

Goal state after:
case pos
a : Prop
h✝ : a
⊢ (Iic a)ᶜ ∈ {∅, {True}}

case neg
a : Prop
h✝ : ¬a
⊢ (Iic a)ᶜ ∈ {∅, {True}}