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
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:
exact Nat.sub_lt (Finset.card_pos.mpr hJ) zero_lt_one

Premises used: Iff.mpr, Nat.sub_lt, zero_lt_one, Finset.card_pos
-- 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) ≤ ⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2)

Tactic:
have sup_bound {x y : T} (hxy : (x, y) ∈ pairSetSeq J a c l) :
    edist (f x) (f y) ≤ ⨆ p : pairSet J a c, edist (f p.1.1) (f p.1.2) := by
    simp only [iSup_subtype]
    apply le_iSup_of_le (i := (x, y))
    apply le_iSup_of_le
    · exact le_rfl
    refine Finset.mem_biUnion.mpr ⟨l, ?_, hxy⟩
    refine Finset.mem_range.mpr <| lt_of_le_of_lt (Nat.findGreatest_le (#J - 1)) ?_
    exact Nat.sub_lt (Finset.card_pos.mpr hJ) zero_lt_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
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
sup_bound :
  ∀ {x y : T} (hxy : (x, y) ∈ pairSetSeq J a c l),
    edist (f x) (f y) ≤ ⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2)
rw :
  edist (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T))
      (f
        (↑(↑(Subtype.mk (p := fun (t : ↥J) ↦ edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) t ≤ c)
                  (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) hst) :
              ↥J) :
          T)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
      (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
⊢ edist (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T))
      (f
        (↑(↑(Subtype.mk (p := fun (t : ↥J) ↦ edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) t ≤ c)
                  (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) hst) :
              ↥J) :
          T)) ≤
    HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
rw [two_mul]

Premises used: two_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
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
sup_bound :
  ∀ {x y : T} (hxy : (x, y) ∈ pairSetSeq J a c l),
    edist (f x) (f y) ≤ ⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2)
apply :
  edist (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T)) (f (logSizeBallSeq J hJ a c l).point) +
      edist (f (logSizeBallSeq J hJ a c l).point)
        (f
          (↑(↑(Subtype.mk (p := fun (t : ↥J) ↦ edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) t ≤ c)
                    (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) hst) :
                ↥J) :
            T)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
      (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
⊢ edist (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T))
      (f
        (↑(↑(Subtype.mk (p := fun (t : ↥J) ↦ edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) t ≤ c)
                  (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) hst) :
              ↥J) :
          T)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
      (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
apply le_trans (edist_triangle _ (f (logSizeBallSeq J hJ a c l).point) _)

Premises used: PairReduction.logSizeBallStruct.point, PairReduction.logSizeBallSeq, le_trans, PseudoEMetricSpace.edist_triangle
-- 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
sup_bound :
  ∀ {x y : T} (hxy : (x, y) ∈ pairSetSeq J a c l),
    edist (f x) (f y) ≤ ⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2)
rw :
  edist (f (logSizeBallSeq J hJ a c l).point) (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T)) +
      edist (f (logSizeBallSeq J hJ a c l).point)
        (f
          (↑(↑(Subtype.mk (p := fun (t : ↥J) ↦ edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) t ≤ c)
                    (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) hst) :
                ↥J) :
            T)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
      (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
⊢ edist (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T)) (f (logSizeBallSeq J hJ a c l).point) +
      edist (f (logSizeBallSeq J hJ a c l).point)
        (f
          (↑(↑(Subtype.mk (p := fun (t : ↥J) ↦ edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) t ≤ c)
                    (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) hst) :
                ↥J) :
            T)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
      (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- 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
sup_bound :
  ∀ {x y : T} (hxy : (x, y) ∈ pairSetSeq J a c l),
    edist (f x) (f y) ≤ ⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2)
⊢ edist (f (logSizeBallSeq J hJ a c l).point) (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T)) +
      edist (f (logSizeBallSeq J hJ a c l).point)
        (f
          (↑(↑(Subtype.mk (p := fun (t : ↥J) ↦ edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) t ≤ c)
                    (Subtype.mk (p := fun (x : T) ↦ x ∈ J) t ht) hst) :
                ↥J) :
            T)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
      (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
apply add_le_add (sup_bound hsP) (sup_bound htP)

Premises used: add_le_add
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
inl :
  ∀ (ha1 : a ≤ 1),
    ∃ K ⊆ J ×ˢ J,
      (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
        (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
          ∀ (f : T → E),
            ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
              HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
inr :
  ∀ (ha1 : 1 < a),
    ∃ K ⊆ J ×ˢ J,
      (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
        (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
          ∀ (f : T → E),
            ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
              HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
rcases le_or_gt a 1 with ha1 | ha1

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
inl :
  ∀ (hJ : IsEmpty.{u_1 + 1} ↥J),
    ∃ K ⊆ J ×ˢ J,
      (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
        (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
          ∀ (f : T → E),
            ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
              HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
inl₁ :
  ∀ (hJ : Nonempty.{u_1 + 1} ↥J),
    ∃ K ⊆ J ×ˢ J,
      (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
        (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
          ∀ (f : T → E),
            ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
              HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
rcases isEmpty_or_nonempty J with hJ | hJ

Premises used: Membership.mem, isEmpty_or_nonempty, Subtype
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : IsEmpty.{u_1 + 1} ↥J
⊢ J = ∅

Tactic:
simp only [Finset.isEmpty_coe_sort] at hJ

Premises used: Finset.isEmpty_coe_sort
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : J = ∅
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
simp [hJ]
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
rw : #J = 1
⊢ ∃ (x₀ : T), J = {x₀}

Tactic:
rw [← Finset.card_eq_one]

Premises used: Finset.card_eq_one
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ #J = 1

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
refine_1 : #J ≤ 1
refine_2 : 1 ≤ #J
⊢ #J = 1

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
this : LE.le (α := ℝ≥0∞) (↑(#J) : ℝ≥0∞) 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ∀ (this : #J ≤ 1), #J ≤ 1
⊢ #J ≤ 1

Tactic:
norm_cast at this
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
refine_1 : LE.le (α := ℝ≥0∞) (↑(#J) : ℝ≥0∞) 1
⊢ #J ≤ 1

Tactic:
suffices (#J : ENNReal) ≤ 1 by norm_cast at this
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ LE.le (α := ℝ≥0∞) (↑(#J) : ℝ≥0∞) 1

Tactic:
hJ_card.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
refine_1 : a ^ n ≤ 1
⊢ LE.le (α := ℝ≥0∞) (↑(#J) : ℝ≥0∞) 1

Tactic:
refine hJ_card.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
rw : HPow.hPow (α := ℝ≥0∞) 1 n
| 1

Tactic:
rw [← one_pow n]

Premises used: one_pow
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
refine_1 : a ^ n ≤ HPow.hPow (α := ℝ≥0∞) 1 n
⊢ a ^ n ≤ 1

Tactic:
conv_rhs => rw [← one_pow n]

Premises used: one_pow
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ a ^ n ≤ HPow.hPow (α := ℝ≥0∞) 1 n

Tactic:
ENNReal.pow_le_pow_left ha1

Premises used: ENNReal.pow_le_pow_left
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ a ^ n ≤ HPow.hPow (α := ℝ≥0∞) 1 n

Tactic:
exact ENNReal.pow_le_pow_left ha1

Premises used: ENNReal.pow_le_pow_left
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
refine_2 : J.Nonempty
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : Nonempty.{u_1 + 1} ↥J
⊢ 1 ≤ #J

Tactic:
rwa [Finset.one_le_card, ← Finset.nonempty_coe_sort]

Premises used: Finset.nonempty_coe_sort, Finset.one_le_card
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
inl :
  ∀ (x₀ : T) (hJ_card : (↑(Finset.card (α := T) {x₀}) : ℝ≥0∞) ≤ a ^ n) (hJ : Nonempty.{u_1 + 1} ↥{x₀}),
    ∃ K ⊆ SProd.sprod (α := Finset T) (β := Finset T) {x₀} {x₀},
      (↑(#K) : ℝ≥0∞) ≤ a * (↑(Finset.card (α := T) {x₀}) : ℝ≥0∞) ∧
        (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
          ∀ (f : T → E),
            ⨆ (s : ↥{x₀}), ⨆ (t : { t : ↥{x₀} // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥{x₀}) : T)) ≤
              HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
obtain ⟨x₀, rfl⟩ : ∃ x₀, J = {x₀} := by
      rw [← Finset.card_eq_one]
      refine le_antisymm ?_ ?_
      · suffices (#J : ENNReal) ≤ 1 by norm_cast at this
        refine hJ_card.trans ?_
        conv_rhs => rw [← one_pow n]
        exact ENNReal.pow_le_pow_left ha1
      · rwa [Finset.one_le_card, ← Finset.nonempty_coe_sort]

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
x₀ : T
hJ_card : (↑(Finset.card (α := T) {x₀}) : ℝ≥0∞) ≤ a ^ n
hJ : Nonempty.{u_1 + 1} ↥{x₀}
⊢ ∃ K ⊆ SProd.sprod (α := Finset T) (β := Finset T) {x₀} {x₀},
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(Finset.card (α := T) {x₀}) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥{x₀}), ⨆ (t : { t : ↥{x₀} // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥{x₀}) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
simp_all
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : 1 < a
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
⟨pairSet J a c, pairSet_subset, card_pairSet_le ha1,
      fun _ _ ↦ edist_le_of_mem_pairSet ha1 hJ_card, iSup_edist_pairSet ha1⟩

Premises used: PairReduction.pairSet, PairReduction.edist_le_of_mem_pairSet, And.intro, Exists.intro, PairReduction.card_pairSet_le, PairReduction.pairSet_subset, PairReduction.iSup_edist_pairSet
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : 1 < a
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))

Tactic:
exact ⟨pairSet J a c, pairSet_subset, card_pairSet_le ha1,
      fun _ _ ↦ edist_le_of_mem_pairSet ha1 hJ_card, iSup_edist_pairSet ha1⟩