awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
ha : 1 < a
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
inr :
  ∀
    (this :
      ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_2 : DecidableEq T]
        (ha : 1 < a) (hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n) {s t : T} (h : (s, t) ∈ pairSet J a c) (i : ℕ) (hiJ : i < #J)
        (h' : (s, t) ∈ pairSetSeq J a c i) (hJ : J.Nonempty) (hn : 1 ≤ n), edist s t ≤ (↑n : ℝ≥0∞) * c)
    (hn : n < 1), edist s t ≤ (↑n : ℝ≥0∞) * c
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c
have wlog! : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_2 : DecidableEq T] (ha : 1 < a)
  (hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n) {s t : T} (h : (s, t) ∈ pairSet J a c) (i : ℕ) (hiJ : i < #J)
  (h' : (s, t) ∈ pairSetSeq J a c i) (hJ : J.Nonempty) (hn : 1 ≤ n), edist s t ≤ (↑n : ℝ≥0∞) * c
Tactic: wlog! hn : 1 ≤ n
Cleared hypotheses: ha, hJ_card, s, t, h, i, hiJ, h', hJ
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
ha : 1 < a
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_2 : DecidableEq T]
    (ha : 1 < a) (hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n) {s t : T} (h : (s, t) ∈ pairSet J a c) (i : ℕ) (hiJ : i < #J)
    (h' : (s, t) ∈ pairSetSeq J a c i) (hJ : J.Nonempty) (hn : 1 ≤ n), edist s t ≤ (↑n : ℝ≥0∞) * c
hn : n < 1
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c
have inr : s = t
Tactic: suffices s = t by simp [this]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (hypothesis)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
ha : 1 < a
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_2 : DecidableEq T]
    (ha : 1 < a) (hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n) {s t : T} (h : (s, t) ∈ pairSet J a c) (i : ℕ) (hiJ : i < #J)
    (h' : (s, t) ∈ pairSetSeq J a c i) (hJ : J.Nonempty) (hn : 1 ≤ n), edist s t ≤ (↑n : ℝ≥0∞) * c
hn : n < 1
⊢ s = t
have hJ_card₁ : #J ≤ 1
Tactic: simp only [Nat.lt_one_iff.mp hn, pow_zero, Nat.cast_le_one] at hJ_card
Cleared hypotheses: hJ_card
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (hypothesis)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
ha : 1 < a
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_2 : DecidableEq T]
    (ha : 1 < a) (hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n) {s t : T} (h : (s, t) ∈ pairSet J a c) (i : ℕ) (hiJ : i < #J)
    (h' : (s, t) ∈ pairSetSeq J a c i) (hJ : J.Nonempty) (hn : 1 ≤ n), edist s t ≤ (↑n : ℝ≥0∞) * c
hn : n < 1
hJ_card : #J ≤ 1
⊢ s = t
have hs : (s, t).1 ∈ J
Tactic: have ⟨hs, ht⟩ := Finset.mem_product.mp (pairSet_subset h)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (hypothesis)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
ha : 1 < a
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_2 : DecidableEq T]
    (ha : 1 < a) (hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n) {s t : T} (h : (s, t) ∈ pairSet J a c) (i : ℕ) (hiJ : i < #J)
    (h' : (s, t) ∈ pairSetSeq J a c i) (hJ : J.Nonempty) (hn : 1 ≤ n), edist s t ≤ (↑n : ℝ≥0∞) * c
hn : n < 1
hJ_card : #J ≤ 1
hs : (s, t).1 ∈ J
⊢ s = t
have ht : (s, t).2 ∈ J
Tactic: have ⟨hs, ht⟩ := Finset.mem_product.mp (pairSet_subset h)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (hypothesis)
Goal:
T_1 : Type u_1
inst : PseudoEMetricSpace T_1
a_1 c_1 : ℝ≥0∞
n_1 : ℕ
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
hn : 1 ≤ n
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c
have h'₁ : (t ∈ (logSizeBallSeq J sorry a c i).finset ∧
    edist (logSizeBallSeq J sorry a c i).point t ≤ (↑(logSizeBallSeq J sorry a c i).radius : ℝ≥0∞) * c) ∧
  (logSizeBallSeq J sorry a c i).point = s
Tactic: simp only [pairSetSeq, hJ, ↓reduceDIte, logSizeBallStruct.ball, Finset.product_eq_sprod,
    Finset.singleton_product, Finset.mem_map, Finset.mem_filter, Function.Embedding.coeFn_mk,
    Prod.mk.injEq, exists_eq_right_right] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T_1 : Type u_1
inst : PseudoEMetricSpace T_1
a_1 c_1 : ℝ≥0∞
n_1 : ℕ
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
hJ : J.Nonempty
hn : 1 ≤ n
h' :
  (t ∈ (logSizeBallSeq J ⋯ a c i).finset ∧
      edist (logSizeBallSeq J ⋯ a c i).point t ≤ (↑(logSizeBallSeq J ⋯ a c i).radius : ℝ≥0∞) * c) ∧
    (logSizeBallSeq J ⋯ a c i).point = s
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c
have obtain : ∀ (ht : t ∈ (logSizeBallSeq J sorry a c i).finset)
  (hdist : edist (logSizeBallSeq J sorry a c i).point t ≤ (↑(logSizeBallSeq J sorry a c i).radius : ℝ≥0∞) * c)
  (h : ((logSizeBallSeq J sorry a c i).point, t) ∈ pairSet J a c),
  edist (logSizeBallSeq J sorry a c i).point t ≤ (↑n : ℝ≥0∞) * c
Tactic: obtain ⟨⟨ht, hdist⟩, rfl⟩ := h'
Cleared hypotheses: s, h, h'
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T_1 : Type u_1
inst : PseudoEMetricSpace T_1
a_1 c_1 : ℝ≥0∞
n_1 : ℕ
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
t : T
i : ℕ
hiJ : i < #J
hJ : J.Nonempty
hn : 1 ≤ n
ht : t ∈ (logSizeBallSeq J ⋯ a c i).finset
hdist : edist (logSizeBallSeq J ⋯ a c i).point t ≤ (↑(logSizeBallSeq J ⋯ a c i).radius : ℝ≥0∞) * c
h : ((logSizeBallSeq J ⋯ a c i).point, t) ∈ pairSet J a c
⊢ edist (logSizeBallSeq J ⋯ a c i).point t ≤ (↑n : ℝ≥0∞) * c
have grw : (↑(logSizeBallSeq J sorry a c i).radius : ℝ≥0∞) * c ≤ (↑n : ℝ≥0∞) * c
Tactic: grw [hdist, radius_logSizeBallSeq_le hJ ha hn hJ_card i]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T_1 : Type u_1
inst : PseudoEMetricSpace T_1
a_1 c_1 : ℝ≥0∞
n_1 : ℕ
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
t : T
i : ℕ
hiJ : i < #J
hJ : J.Nonempty
hn : 1 ≤ n
ht : t ∈ (logSizeBallSeq J ⋯ a c i).finset
hdist : edist (logSizeBallSeq J ⋯ a c i).point t ≤ (↑(logSizeBallSeq J ⋯ a c i).radius : ℝ≥0∞) * c
h : ((logSizeBallSeq J ⋯ a c i).point, t) ∈ pairSet J a c
grw : (↑(logSizeBallSeq J ⋯ a c i).radius : ℝ≥0∞) * c ≤ (↑n : ℝ≥0∞) * c
⊢ edist (logSizeBallSeq J ⋯ a c i).point t ≤ (↑n : ℝ≥0∞) * c
have grw₁ : (↑n : ℝ≥0∞) * c ≤ (↑n : ℝ≥0∞) * c
Tactic: grw [hdist, radius_logSizeBallSeq_le hJ ha hn hJ_card i]
-- 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
⊢ ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
    HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
have rw : ∀ (i : ↥J),
  ⨆ (t : { t : ↥J // edist i t ≤ c }), edist (f (↑i : T)) (f (↑(↑t : ↥J) : T)) ≤
    HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
Tactic: rw [iSup_le_iff]
-- 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
s : T
hs : s ∈ J
⊢ ⨆ (t : { t : ↥J // edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) t ≤ c }),
      edist (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T)) (f (↑(↑t : ↥J) : T)) ≤
    HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
have rw : ∀ (i : { t : ↥J // edist (Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) t ≤ c }),
  edist (f (↑(Subtype.mk (p := fun (x : T) ↦ x ∈ J) s hs) : T)) (f (↑(↑i : ↥J) : T)) ≤
    HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥(pairSet J a c)), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
Tactic: rw [iSup_le_iff]
-- 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
⊢ 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 hJ : J.Nonempty
Tactic: have hJ : J.Nonempty := ⟨s, hs⟩
-- 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
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)
⊢ P l
have apply : P 0
Tactic: apply Nat.findGreatest_spec zero_le
-- 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)
⊢ 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 hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
Tactic: obtain ⟨hsV, htV⟩ : P l := by
    apply Nat.findGreatest_spec zero_le
    simpa [P, finset_logSizeBallSeq_zero] using ⟨hs, ht⟩
-- 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
⊢ 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 htV : t ∈ (logSizeBallSeq J hJ a c l).finset
Tactic: obtain ⟨hsV, htV⟩ : P l := by
    apply Nat.findGreatest_spec zero_le
    simpa [P, finset_logSizeBallSeq_zero] using ⟨hs, ht⟩
-- 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
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
⊢ 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 inr : ∀
  (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),
  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: wlog h : s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset generalizing s t
-- 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
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
⊢ l < #J - 1
have by_contra : ∀ (hl : ¬l < #J - 1), False
Tactic: by_contra hl
-- 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
hl : ¬l < #J - 1
⊢ False
have hl₁ : #J ≤ l + 1
Tactic: simp only [not_lt, tsub_le_iff_right] at hl
Cleared hypotheses: hl
-- 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
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
hl : #J ≤ l + 1
⊢ l + 1 = #J
have refine : l + 1 ≤ #J
Tactic: refine Nat.le_antisymm_iff.mpr ⟨?_, hl⟩
-- 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
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
hl : #J ≤ l + 1
⊢ Nat.findGreatest P (#J - 1) + 1 ≤ #J
have grw : #J - 1 + 1 - 1 + 1 ≤ #J - 1 + 1 - 1 + 1
Tactic: grw [← Nat.sub_add_cancel <| Order.one_le_iff_pos.mpr (Finset.card_pos.mpr hJ),
            Nat.findGreatest_le]
-- 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
hl : #J ≤ l + 1
⊢ False
have hlJ : l + 1 = #J
Tactic: have hlJ : l + 1 = #J := by
          refine Nat.le_antisymm_iff.mpr ⟨?_, hl⟩
          dsimp [l]
          grw [← Nat.sub_add_cancel <| Order.one_le_iff_pos.mpr (Finset.card_pos.mpr hJ),
            Nat.findGreatest_le]
          rfl