awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
rw :
  (HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 + 1) * c =
    (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
⊢ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c + 1 * c =
    (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c

Tactic:
rw [← add_mul]

Premises used: add_mul
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
e_a :
  HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 + 1 =
    (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)
⊢ (HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 + 1) * c =
    (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c

Tactic:
congr
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
rw : LE.le (α := ℝ≥0∞) 1 (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)
⊢ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 + 1 =
    (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)

Tactic:
rw [ENNReal.sub_add_eq_add_sub _ (ENNReal.one_ne_top),
      ENNReal.add_sub_cancel_right (ENNReal.one_ne_top)]

Premises used: ENNReal.sub_add_eq_add_sub, ENNReal.add_sub_cancel_right, ENNReal.one_ne_top
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
rw : LE.le (α := ℝ≥0∞) (↑1 : ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) 1 (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)

Tactic:
rw [← Nat.cast_one]

Premises used: Nat.cast_one
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
a₁ : 1 ≤ (logSizeBallSeq J hJ a c l).radius
⊢ LE.le (α := ℝ≥0∞) (↑1 : ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ 1 ≤ (logSizeBallSeq J hJ a c l).radius

Tactic:
one_le_radius_logSizeBallSeq hJ ha l

Premises used: PairReduction.one_le_radius_logSizeBallSeq
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ 1 ≤ (logSizeBallSeq J hJ a c l).radius

Tactic:
exact one_le_radius_logSizeBallSeq hJ ha l

Premises used: PairReduction.one_le_radius_logSizeBallSeq
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ t ∈ (logSizeBallSeq J hJ a c l).ball c

Tactic:
have htB : t ∈ (logSizeBallSeq J hJ a c l).ball c := by
    simp only [logSizeBallStruct.ball, Finset.mem_filter, htV, true_and]
    apply le_trans (edist_triangle _ s _)
    apply le_of_le_of_eq (add_le_add h hst)
    nth_rw 3 [← one_mul c]
    rw [← add_mul]
    congr
    rw [ENNReal.sub_add_eq_add_sub _ (ENNReal.one_ne_top),
      ENNReal.add_sub_cancel_right (ENNReal.one_ne_top)]
    rw [← Nat.cast_one]
    gcongr
    exact one_le_radius_logSizeBallSeq hJ ha l
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l

Tactic:
simp [pairSetSeq, hJ, hsB]

Premises used: PairReduction.pairSetSeq
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l

Tactic:
have hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l := by
    simp [pairSetSeq, hJ, hsB]
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
⊢ ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l

Tactic:
simp [pairSetSeq, hJ, htB]

Premises used: PairReduction.pairSetSeq
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
⊢ ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l

Tactic:
have htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l := by
    simp [pairSetSeq, hJ, htB]
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
simp : edist (f x) (f y) ≤ ⨆ i ∈ pairSet J a c, edist (f i.1) (f i.2)
⊢ edist (f x) (f y) ≤ ⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2)

Tactic:
simp only [iSup_subtype]

Premises used: iSup_subtype
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
apply : edist (f x) (f y) ≤ ⨆ (_ : (x, y) ∈ pairSet J a c), edist (f (x, y).1) (f (x, y).2)
⊢ edist (f x) (f y) ≤ ⨆ i ∈ pairSet J a c, edist (f i.1) (f i.2)

Tactic:
apply le_iSup_of_le (i := (x, y))

Premises used: Prod.mk, le_iSup_of_le
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
h₁ : edist (f x) (f y) ≤ edist (f (x, y).1) (f (x, y).2)
i : (x, y) ∈ pairSet J a c
⊢ edist (f x) (f y) ≤ ⨆ (_ : (x, y) ∈ pairSet J a c), edist (f (x, y).1) (f (x, y).2)

Tactic:
apply le_iSup_of_le

Premises used: le_iSup_of_le
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
⊢ edist (f x) (f y) ≤ edist (f (x, y).1) (f (x, y).2)

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
⊢ edist (f x) (f y) ≤ edist (f (x, y).1) (f (x, y).2)

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
⊢ (x, y) ∈ pairSet J a c

Tactic:
Finset.mem_biUnion.mpr ⟨l, ?_, hxy⟩

Premises used: Iff.mpr, Set.Mem, setOf, And.intro, Exists.intro, Finset.mem_biUnion
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
i : l ∈ Finset.range #J
⊢ (x, y) ∈ pairSet J a c

Tactic:
refine Finset.mem_biUnion.mpr ⟨l, ?_, hxy⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.mem_biUnion
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
⊢ l ∈ Finset.range #J

Tactic:
Finset.mem_range.mpr <| lt_of_le_of_lt (Nat.findGreatest_le (#J - 1)) ?_

Premises used: Iff.mpr, lt_of_le_of_lt, HSub.hSub, Finset.mem_range, Finset.card, OfNat.ofNat, Nat.findGreatest_le
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
i : #J - 1 < #J
⊢ l ∈ Finset.range #J

Tactic:
refine Finset.mem_range.mpr <| lt_of_le_of_lt (Nat.findGreatest_le (#J - 1)) ?_

Premises used: Iff.mpr, lt_of_le_of_lt, HSub.hSub, Finset.mem_range, Finset.card, OfNat.ofNat, Nat.findGreatest_le
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) ≤ c
P : (l : ℕ) → Prop := fun (l : ℕ) ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
⊢ #J - 1 < #J

Tactic:
Nat.sub_lt (Finset.card_pos.mpr hJ) zero_lt_one

Premises used: Iff.mpr, Nat.sub_lt, zero_lt_one, Finset.card_pos