awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ edist (f (x', y)) (f (x, y)) ≤ (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞)

Tactic:
exact (hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)

Premises used: PseudoEMetricSpace.edist_comm, LT.lt.le, LipschitzOnWith.edist_le_mul_of_le, Eq.trans_le
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)) + ε / 2 + (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞) =
    (↑δ : ℝ≥0∞) * (3 * (↑K : ℝ≥0∞)) + ε / 2

Tactic:
ring
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) + ε / 2 ≤ ε / 2 + ε / 2

Tactic:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ ε / 2 + ε / 2 = ε

Tactic:
ENNReal.add_halves _

Premises used: ENNReal.add_halves
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : EDist.edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | EDist.edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | EDist.edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
edist :
  EDist.edist (f (a, b)) (f (x', b)) + EDist.edist (f (x', b)) (f (x', y)) + EDist.edist (f (x', y)) (f (x, y)) ≤
    (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)) + ε / 2 + (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞)
edist₁ :
  (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)) + ε / 2 + (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞) =
    (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) + ε / 2
edist₂ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) + ε / 2 ≤ ε / 2 + ε / 2
⊢ f (a, b) ∈ Metric.closedEBall (f (x, y)) ε

Tactic:
calc
    edist (f (a, b)) (f (x, y)) ≤ edist (f (a, b)) (f (x', b)) + edist (f (x', b)) (f (x', y)) +
        edist (f (x', y)) (f (x, y)) := edist_triangle4 _ _ _ _
    _ ≤ K * (δ + δ) + ε / 2 + K * δ := by
      gcongr
      · refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_
        exact (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)
      · exact hby
      · exact (hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)
    _ = δ * ↑(3 * K) + ε / 2 := by push_cast; ring
    _ ≤ ε / 2 + ε / 2 := by gcongr
    _ = ε := ENNReal.add_halves _

Premises used: HMul.hMul, Prod.mk, edist_triangle4, HAdd.hAdd, ENNReal.add_halves, EDist.edist, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s : Set α
t : Set β
K : ℝ≥0
ha : ∀ a ∈ s, ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
⊢ ContinuousOn f (s ×ˢ t)

Tactic:
continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith
    f Subset.rfl subset_closure K ha hb

Premises used: subset_closure, Set.Subset.rfl, continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
s : Set α
hs : Dense s
ha : ∀ a ∈ s, Continuous[inst_1, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun (y : β) ↦ f (a, y)
hb : ∀ (b : β), LipschitzWith.{u, w} (β := γ) K fun (x : α) ↦ f (x, b)
simp :
  ∀ (ha : ∀ a ∈ s, ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) univ)
    (hb : ∀ (b : β), LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) univ),
    ContinuousOn f (SProd.sprod (α := Set α) (β := Set β) univ univ)
⊢ Continuous[instTopologicalSpaceProd, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
simp only [← continuousOn_univ, ← univ_prod_univ, ← lipschitzOnWith_univ] at *

Premises used: Set.univ_prod_univ, lipschitzOnWith_univ, continuousOn_univ
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
s : Set α
hs : Dense s
ha : ∀ a ∈ s, ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) univ
hb : ∀ (b : β), LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) univ
⊢ ContinuousOn f (SProd.sprod (α := Set α) (β := Set β) univ univ)

Tactic:
continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith f (subset_univ _)
    hs.closure_eq.ge K ha fun b _ => hb b

Premises used: Eq.ge, Set.subset_univ, Dense.closure_eq, continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
s : Set α
hs : Dense s
ha : ∀ a ∈ s, ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) univ
hb : ∀ (b : β), LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) univ
⊢ ContinuousOn f (SProd.sprod (α := Set α) (β := Set β) univ univ)

Tactic:
exact continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith f (subset_univ _)
    hs.closure_eq.ge K ha fun b _ => hb b

Premises used: Eq.ge, Set.subset_univ, Dense.closure_eq, continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
ha : ∀ (a : α), Continuous[inst_1, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun (y : β) ↦ f (a, y)
hb : ∀ (b : β), LipschitzWith.{u, w} (β := γ) K fun (x : α) ↦ f (x, b)
⊢ Continuous[instTopologicalSpaceProd, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
continuous_prod_of_dense_continuous_lipschitzWith f K dense_univ (fun _ _ ↦ ha _) hb

Premises used: dense_univ, continuous_prod_of_dense_continuous_lipschitzWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s : Set α
t t' : Set β
ht' : t' ⊆ t
htt' : t ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t'
K : ℝ≥0
ha : ∀ a ∈ s, LipschitzOnWith.{v, w} (β := γ) K (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t', ContinuousOn.{u, w} (Y := γ) (fun (x : α) ↦ f (x, b)) s
⊢ ContinuousOn f (s ×ˢ t)

Tactic:
have : ContinuousOn (f ∘ Prod.swap) (t ×ˢ s) :=
    continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith _ ht' htt' K hb ha
  this.comp continuous_swap.continuousOn (mapsTo_swap_prod _ _)

Premises used: Continuous.continuousOn, Function.comp, continuous_swap, ContinuousOn.comp, Set.mapsTo_swap_prod, Prod.swap, continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s : Set α
t : Set β
K : ℝ≥0
ha : ∀ a ∈ s, LipschitzOnWith.{v, w} (β := γ) K (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, ContinuousOn.{u, w} (Y := γ) (fun (x : α) ↦ f (x, b)) s
⊢ ContinuousOn f (s ×ˢ t)

Tactic:
have : ContinuousOn (f ∘ Prod.swap) (t ×ˢ s) :=
    continuousOn_prod_of_continuousOn_lipschitzOnWith _ K hb ha
  this.comp continuous_swap.continuousOn (mapsTo_swap_prod _ _)

Premises used: Continuous.continuousOn, Function.comp, continuousOn_prod_of_continuousOn_lipschitzOnWith, continuous_swap, ContinuousOn.comp, Set.mapsTo_swap_prod, Prod.swap
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
t : Set β
ht : Dense t
ha : ∀ (a : α), LipschitzWith.{v, w} (β := γ) K fun (y : β) ↦ f (a, y)
hb : ∀ b ∈ t, Continuous[inst, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : α) ↦ f (x, b)
⊢ Continuous[instTopologicalSpaceProd, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
have : Continuous (f ∘ Prod.swap) :=
    continuous_prod_of_dense_continuous_lipschitzWith _ K ht hb ha
  this.comp continuous_swap

Premises used: Continuous.comp, Function.comp, continuous_swap, continuous_prod_of_dense_continuous_lipschitzWith, Prod.swap
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
ha : ∀ (a : α), LipschitzWith.{v, w} (β := γ) K fun (y : β) ↦ f (a, y)
hb : ∀ (b : β), Continuous[inst, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : α) ↦ f (x, b)
⊢ Continuous[instTopologicalSpaceProd, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
have : Continuous (f ∘ Prod.swap) :=
    continuous_prod_of_continuous_lipschitzWith _ K hb ha
  this.comp continuous_swap

Premises used: continuous_prod_of_continuous_lipschitzWith, Continuous.comp, Function.comp, continuous_swap, Prod.swap
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
t : T
V : Finset T
ha : 1 < a
c : ℝ≥0∞
⊢ ∀ᶠ (a_1 : ℕ) in Filter.atTop, LT.lt (α := ℝ≥0∞) (↑(#V) : ℝ≥0∞) (((fun (x : ℝ) ↦ a ^ x) ∘ Nat.cast) a_1)

Tactic:
have := ENNReal.tendsto_nhds_top_iff_nat.1
    ((ENNReal.tendsto_rpow_atTop_of_one_lt_base ha).comp tendsto_natCast_atTop_atTop) #V
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
t : T
V : Finset T
ha : 1 < a
c : ℝ≥0∞
this : ∀ᶠ (a_1 : ℕ) in Filter.atTop, LT.lt (α := ℝ≥0∞) (↑(#V) : ℝ≥0∞) (((fun (x : ℝ) ↦ a ^ x) ∘ Nat.cast) a_1)
⊢ ∃ (a_1 : ℕ), ∀ (b : ℕ), a_1 ≤ b → (↑(#V) : ℝ≥0∞) < a ^ b

Tactic:
simp only [Function.comp_apply, ENNReal.rpow_natCast, Filter.eventually_atTop, ge_iff_le] at this

Premises used: ge_iff_le, ENNReal.rpow_natCast, Function.comp_apply, Filter.eventually_atTop
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
t : T
V : Finset T
ha : 1 < a
c : ℝ≥0∞
this : ∃ (a_1 : ℕ), ∀ (b : ℕ), a_1 ≤ b → (↑(#V) : ℝ≥0∞) < a ^ b
obtain :
  ∀ (r : ℕ) (hr : ∀ (b : ℕ), r ≤ b → (↑(#V) : ℝ≥0∞) < a ^ b),
    ∃ (r : ℕ), 1 ≤ r ∧ (↑(#({x ∈ V | edist t x ≤ (↑r : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ r
⊢ ∃ (r : ℕ), 1 ≤ r ∧ (↑(#({x ∈ V | edist t x ≤ (↑r : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ r

Tactic:
obtain ⟨r, hr⟩ := this
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
t : T
V : Finset T
ha : 1 < a
c : ℝ≥0∞
r : ℕ
hr : ∀ (b : ℕ), r ≤ b → (↑(#V) : ℝ≥0∞) < a ^ b
⊢ ∃ (r : ℕ), 1 ≤ r ∧ (↑(#({x ∈ V | edist t x ≤ (↑r : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ r

Tactic:
⟨max r 1, le_max_right r 1,
    le_trans (mod_cast Finset.card_filter_le V _) (hr (max r 1) (le_max_left r 1)).le⟩

Premises used: le_max_right, LT.lt.le, Max.max, And.intro, Exists.intro, OfNat.ofNat, le_max_left, le_trans
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
t : T
V : Finset T
ha : 1 < a
c : ℝ≥0∞
r : ℕ
hr : ∀ (b : ℕ), r ≤ b → (↑(#V) : ℝ≥0∞) < a ^ b
⊢ ∃ (r : ℕ), 1 ≤ r ∧ (↑(#({x ∈ V | edist t x ≤ (↑r : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ r

Tactic:
exact ⟨max r 1, le_max_right r 1,
    le_trans (mod_cast Finset.card_filter_le V _) (hr (max r 1) (le_max_left r 1)).le⟩
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
rw : 1 ≤ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯
⊢ 1 ≤ logSizeRadius t V a c

Tactic:
rw [logSizeRadius, dif_pos ha]

Premises used: PairReduction.logSizeRadius, dif_pos
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ 1 ≤ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯

Tactic:
(Nat.find_spec (exists_radius_le t V ha c)).1

Premises used: And.left, PairReduction.exists_radius_le, Nat.find_spec
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ 1 ≤ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯

Tactic:
exact (Nat.find_spec (exists_radius_le t V ha c)).1

Premises used: And.left, PairReduction.exists_radius_le, Nat.find_spec
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
rw :
  (↑(#({x ∈ V |
            edist t x ≤
              (↑(Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯) :
                  ℝ≥0∞) *
                c})) :
      ℝ≥0∞) ≤
    a ^ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯
⊢ (↑(#({x ∈ V | edist t x ≤ (↑(logSizeRadius t V a c) : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ logSizeRadius t V a c

Tactic:
rw [logSizeRadius, dif_pos ha]

Premises used: PairReduction.logSizeRadius, dif_pos
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ (↑(#({x ∈ V |
            edist t x ≤
              (↑(Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯) :
                  ℝ≥0∞) *
                c})) :
      ℝ≥0∞) ≤
    a ^ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯

Tactic:
(Nat.find_spec (exists_radius_le t V ha c)).2

Premises used: And.right, PairReduction.exists_radius_le, Nat.find_spec
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ (↑(#({x ∈ V |
            edist t x ≤
              (↑(Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯) :
                  ℝ≥0∞) *
                c})) :
      ℝ≥0∞) ≤
    a ^ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯

Tactic:
exact (Nat.find_spec (exists_radius_le t V ha c)).2

Premises used: And.right, PairReduction.exists_radius_le, Nat.find_spec
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
pos :
  ∀ (h_one : logSizeRadius t V a c = 1),
    a ^ (logSizeRadius t V a c - 1) ≤
      (↑(#({x ∈ V | edist t x ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeRadius t V a c) : ℝ≥0∞) 1 * c})) : ℝ≥0∞)
neg :
  ∀ (h_one : ¬logSizeRadius t V a c = 1),
    a ^ (logSizeRadius t V a c - 1) ≤
      (↑(#({x ∈ V | edist t x ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeRadius t V a c) : ℝ≥0∞) 1 * c})) : ℝ≥0∞)
⊢ a ^ (logSizeRadius t V a c - 1) ≤
    (↑(#({x ∈ V | edist t x ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeRadius t V a c) : ℝ≥0∞) 1 * c})) : ℝ≥0∞)

Tactic:
by_cases h_one : logSizeRadius t V a c = 1

Premises used: PairReduction.logSizeRadius
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : logSizeRadius t V a c = 1
pos : {x ∈ V | edist t x = 0}.Nonempty
⊢ a ^ (logSizeRadius t V a c - 1) ≤
    (↑(#({x ∈ V | edist t x ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeRadius t V a c) : ℝ≥0∞) 1 * c})) : ℝ≥0∞)

Tactic:
simp only [h_one, tsub_self, pow_zero, Nat.cast_one, zero_mul, nonpos_iff_eq_zero,
      Nat.one_le_cast, Finset.one_le_card]

Premises used: MulZeroClass.zero_mul, tsub_self, Nat.one_le_cast, pow_zero, Finset.one_le_card, Nat.cast_one, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : logSizeRadius t V a c = 1
⊢ t ∈ {x ∈ V | edist t x = 0}

Tactic:
simpa
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : logSizeRadius t V a c = 1
⊢ {x ∈ V | edist t x = 0}.Nonempty

Tactic:
exact ⟨t, by simpa⟩
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬logSizeRadius t V a c = 1
neg :
  ∀ (h_one : ¬Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ = 1),
    a ^ (Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1) ≤
      (↑(#({x ∈ V |
              edist t x ≤
                HSub.hSub (α := ℝ≥0∞)
                    (↑(Nat.find (p := fun (n : ℕ) ↦
                          1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯) :
                      ℝ≥0∞)
                    1 *
                  c})) :
        ℝ≥0∞)
⊢ a ^ (logSizeRadius t V a c - 1) ≤
    (↑(#({x ∈ V | edist t x ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeRadius t V a c) : ℝ≥0∞) 1 * c})) : ℝ≥0∞)

Tactic:
rw [logSizeRadius, dif_pos ha] at h_one ⊢

Premises used: PairReduction.logSizeRadius, dif_pos
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ = 1
⊢ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 <
    Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ = 1
⊢ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 <
    Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯

Tactic:
have : Nat.find (exists_radius_le t V ha c) - 1 < Nat.find (exists_radius_le t V ha c) := by
    simp
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ = 1
this :
  Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 <
    Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯
⊢ ¬(1 ≤ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 ∧
      (↑(#({x ∈ V |
                edist t x ≤
                  (↑(Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n)
                            ⋯ -
                          1) :
                      ℝ≥0∞) *
                    c})) :
          ℝ≥0∞) ≤
        a ^ (Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1))

Tactic:
have h := Nat.find_min (exists_radius_le t V ha c) this