awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (hypothesis)
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
⊢ 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))
have htB : 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
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (hypothesis)
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
⊢ 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))
have hsP : ((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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (hypothesis)
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
⊢ 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))
have htP : ((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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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)
have simp : edist (f x) (f y) ≤ ⨆ i ∈ pairSet J a c, edist (f i.1) (f i.2)
Tactic: simp only [iSup_subtype]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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) ≤ ⨆ i ∈ pairSet J a c, edist (f i.1) (f i.2)
have apply : 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 (i := (x, y))
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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) ≤ ⨆ (_ : (x, y) ∈ pairSet J a c), edist (f (x, y).1) (f (x, y).2)
have h₁ : edist (f x) (f y) ≤ edist (f (x, y).1) (f (x, y).2)
Tactic: apply le_iSup_of_le
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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)
⊢ edist (f x) (f y) ≤ ⨆ (_ : (x, y) ∈ pairSet J a c), edist (f (x, y).1) (f (x, y).2)
have i : (x, y) ∈ pairSet J a c
Tactic: apply le_iSup_of_le
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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
have i : l ∈ Finset.range #J
Tactic: refine Finset.mem_biUnion.mpr ⟨l, ?_, hxy⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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
have i : #J - 1 < #J
Tactic: refine Finset.mem_range.mpr <| lt_of_le_of_lt (Nat.findGreatest_le (#J - 1)) ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (hypothesis)
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
⊢ 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))
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 : 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
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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 (↑(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))
have 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))
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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 (↑(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))
have 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))
Tactic: apply le_trans (edist_triangle _ (f (logSizeBallSeq J hJ a c l).point) _)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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 (↑(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))
have 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))
Tactic: rw [edist_comm]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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
⊢ ∃ 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))
have 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))
Tactic: rcases le_or_gt a 1 with ha1 | ha1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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))
⊢ ∃ 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))
have 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))
Tactic: rcases le_or_gt a 1 with ha1 | ha1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
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
⊢ ∃ 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))
have 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))
Tactic: rcases isEmpty_or_nonempty J with hJ | hJ