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
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
hJ : J.Nonempty
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
this :
  ∀ (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),
    let P : (l : ℕ) → Prop := fun (l : ℕ) ↦
      s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let 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 : s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset),
      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))
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hts : edist t s ≤ c
hP : P = fun (l : ℕ) ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset
⊢ edist
      (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))
      (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T)) ≤
    HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
have htV₁ : t ∈
  (logSizeBallSeq J hJ a c
      (Nat.findGreatest (fun (l : ℕ) ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset)
        (#J - 1))).finset
Tactic: simp only [hP, l] at htV hsV h'
Cleared hypotheses: hsV, htV, h'
-- 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
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
hJ : J.Nonempty
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
this :
  ∀ (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),
    let P : (l : ℕ) → Prop := fun (l : ℕ) ↦
      s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let 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 : s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset),
      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))
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hts : edist t s ≤ c
hP : P = fun (l : ℕ) ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset
htV₁ :
  t ∈
    (logSizeBallSeq J hJ a c
        (Nat.findGreatest
          (fun (l : ℕ) ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset)
          (#J - 1))).finset
⊢ edist
      (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))
      (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T)) ≤
    HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
have hsV₁ : s ∈
  (logSizeBallSeq J hJ a c
      (Nat.findGreatest (fun (l : ℕ) ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset)
        (#J - 1))).finset
Tactic: simp only [hP, l] at htV hsV h'
Cleared hypotheses: hsV, htV, h'
-- 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
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
hJ : J.Nonempty
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
this :
  ∀ (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),
    let P : (l : ℕ) → Prop := fun (l : ℕ) ↦
      s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let 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 : s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset),
      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))
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hts : edist t s ≤ c
hP : P = fun (l : ℕ) ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset
htV₁ :
  t ∈
    (logSizeBallSeq J hJ a c
        (Nat.findGreatest
          (fun (l : ℕ) ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset)
          (#J - 1))).finset
hsV₁ :
  s ∈
    (logSizeBallSeq J hJ a c
        (Nat.findGreatest
          (fun (l : ℕ) ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset)
          (#J - 1))).finset
⊢ edist
      (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))
      (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T)) ≤
    HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
have h'₁ : t ∉
  (logSizeBallSeq J hJ a c
      (Nat.findGreatest (fun (l : ℕ) ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset)
          (#J - 1) +
        1)).finset
Tactic: simp only [hP, l] at htV hsV h'
Cleared hypotheses: hsV, htV, h'
-- 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 : s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
⊢ 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 h₁ : edist (logSizeBallSeq J hJ a c l).point s ≤ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c
Tactic: simp only [finset_logSizeBallSeq_add_one, logSizeBallStruct.smallBall, Finset.mem_sdiff, hsV,
    Finset.mem_filter, true_and, not_le, not_lt] at h
Cleared hypotheses: h
-- 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
⊢ s ∈ (logSizeBallSeq J hJ a c l).ball c
have simp : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
Tactic: simp only [logSizeBallStruct.ball, Finset.mem_filter, hsV, true_and]
-- 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
⊢ edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
have grw : HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c ≤
  (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
Tactic: grw [h, tsub_le_self]
-- 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
grw :
  HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c ≤
    (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
⊢ edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
have grw₁ : (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c ≤ (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
Tactic: grw [h, tsub_le_self]
-- 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
⊢ 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 hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
Tactic: have hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c := by
    simp only [logSizeBallStruct.ball, Finset.mem_filter, hsV, true_and]
    grw [h, tsub_le_self]
-- 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
⊢ t ∈ (logSizeBallSeq J hJ a c l).ball c
have simp : edist (logSizeBallSeq J hJ a c l).point t ≤ (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
Tactic: simp only [logSizeBallStruct.ball, Finset.mem_filter, htV, true_and]
-- 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
⊢ edist (logSizeBallSeq J hJ a c l).point t ≤ (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
have apply : edist (logSizeBallSeq J hJ a c l).point s + edist s t ≤ (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
Tactic: apply le_trans (edist_triangle _ s _)
-- 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
⊢ edist (logSizeBallSeq J hJ a c l).point s + edist s t ≤ (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
have apply : HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c + c =
  (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
Tactic: apply le_of_le_of_eq (add_le_add h hst)
-- 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
⊢ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c + c =
    (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
have nth_rw : 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: nth_rw 3 [← one_mul c]
-- 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
⊢ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 * c + 1 * c =
    (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
have rw : (HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 + 1) * c =
  (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
Tactic: rw [← add_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
⊢ (HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 + 1) * c =
    (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) * c
have e_a : HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 + 1 = (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)
Tactic: congr
-- 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
⊢ HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞) 1 + 1 =
    (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) 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)]
-- 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
⊢ LE.le (α := ℝ≥0∞) 1 (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) (↑1 : ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)
Tactic: rw [← Nat.cast_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
⊢ LE.le (α := ℝ≥0∞) (↑1 : ℝ≥0∞) (↑(logSizeBallSeq J hJ a c l).radius : ℝ≥0∞)
have a₁ : 1 ≤ (logSizeBallSeq J hJ a c l).radius
Tactic: gcongr