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∞
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ #(logSizeBallSeq J hJ a c i).finset = 0
have neg : ¬#(logSizeBallSeq J hJ a c i).finset ≠ 0
Tactic: rwa [← not_ne_iff, Finset.card_ne_zero.not]
-- 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
hJ : J.Nonempty
i : ℕ
⊢ #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
have zero : #(logSizeBallSeq J hJ a c 0).finset ≤ #J - 0
Tactic: induction i with
  | zero => simp [finset_logSizeBallSeq_zero]
  | succ i ih =>
    by_cases h : (logSizeBallSeq J hJ a c i).finset.Nonempty
    · have := card_finset_logSizeBallSeq_add_one_lt hJ i h
      lia
    apply le_trans <| Finset.card_le_card (finset_logSizeBallSeq_add_one_subset hJ i)
    suffices #(logSizeBallSeq J hJ a c i).finset = 0 by simp [this]
    rwa [← not_ne_iff, Finset.card_ne_zero.not]
Cleared hypotheses: 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
hJ : J.Nonempty
i : ℕ
zero : #(logSizeBallSeq J hJ a c 0).finset ≤ #J - 0
⊢ #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
have succ : ∀ (i : ℕ) (ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i), #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)
Tactic: induction i with
  | zero => simp [finset_logSizeBallSeq_zero]
  | succ i ih =>
    by_cases h : (logSizeBallSeq J hJ a c i).finset.Nonempty
    · have := card_finset_logSizeBallSeq_add_one_lt hJ i h
      lia
    apply le_trans <| Finset.card_le_card (finset_logSizeBallSeq_add_one_subset hJ i)
    suffices #(logSizeBallSeq J hJ a c i).finset = 0 by simp [this]
    rwa [← not_ne_iff, Finset.card_ne_zero.not]
Cleared hypotheses: 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
hJ : J.Nonempty
⊢ #(logSizeBallSeq J hJ a c #J).finset = 0
have rw : #(logSizeBallSeq J hJ a c #J).finset ≤ #J - #J
Tactic: rw [← Nat.le_zero, ← tsub_self #J]
-- 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
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
have inr : ∀
  (this :
    ∀ {i j : ℕ} (hij : i ≠ j) (h : i < j),
      Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c))
  (h : j ≤ i), Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
Tactic: wlog! h : i < j generalizing i j
-- 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
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
inr :
  ∀
    (this :
      ∀ {i j : ℕ} (hij : i ≠ j) (h : i < j),
        Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c))
    (h : j ≤ i), Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
have wlog! : ∀ {i j : ℕ} (hij : i ≠ j) (h : i < j),
  Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
Tactic: wlog! h : i < j generalizing i j
Cleared hypotheses: i, j, hij
-- 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
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
h : i < j
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
have h₁ : (logSizeBallSeq J hJ a c j).smallBall c ⊆ (fun (i : ℕ) ↦ (logSizeBallSeq J hJ a c i).finset) i.succ
Tactic: apply Finset.disjoint_of_subset_right
-- 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
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
h : i < j
h₁ : (logSizeBallSeq J hJ a c j).smallBall c ⊆ (fun (i : ℕ) ↦ (logSizeBallSeq J hJ a c i).finset) i.succ
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
have d : Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((fun (i : ℕ) ↦ (logSizeBallSeq J hJ a c i).finset) i.succ)
Tactic: apply Finset.disjoint_of_subset_right
-- 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
⊢ (Finset.range #J).biUnion (pairSetSeq J a c) ⊆ J ×ˢ J
have rw : ∀ x ∈ Finset.range #J, pairSetSeq J a c x ⊆ J ×ˢ J
Tactic: rw [Finset.biUnion_subset_iff_forall_subset]
-- 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
i : ℕ
hi : i ∈ Finset.range #J
⊢ pairSetSeq J a c i ⊆ J ×ˢ J
have pos : ∀ (hJ : J.Nonempty), pairSetSeq J a c i ⊆ J ×ˢ J
Tactic: by_cases hJ : J.Nonempty
-- 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
i : ℕ
hi : i ∈ Finset.range #J
pos : ∀ (hJ : J.Nonempty), pairSetSeq J a c i ⊆ J ×ˢ J
⊢ pairSetSeq J a c i ⊆ J ×ˢ J
have neg : ∀ (hJ : ¬J.Nonempty), pairSetSeq J a c i ⊆ J ×ˢ J
Tactic: by_cases hJ : J.Nonempty
-- 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
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ pairSetSeq J a c i ⊆ J ×ˢ J
have pos : Finset.product {(logSizeBallSeq J sorry a c i).point} ((logSizeBallSeq J sorry a c i).ball c) ⊆ J ×ˢ J
Tactic: simp only [pairSetSeq, hJ, ↓reduceDIte]
-- 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
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ Finset.product {(logSizeBallSeq J ⋯ a c i).point} ((logSizeBallSeq J ⋯ a c i).ball c) ⊆ J ×ˢ J
have pos : {(logSizeBallSeq J sorry a c i).point} ⊆ J
Tactic: apply Finset.product_subset_product
-- 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
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
pos : {(logSizeBallSeq J ⋯ a c i).point} ⊆ J
⊢ Finset.product {(logSizeBallSeq J ⋯ a c i).point} ((logSizeBallSeq J ⋯ a c i).ball c) ⊆ J ×ˢ J
have pos₁ : (logSizeBallSeq J sorry a c i).ball c ⊆ J
Tactic: apply Finset.product_subset_product
-- 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
hJ : J.Nonempty
ha : 1 < a
i : ℕ
ih :
  (↑(#(pairSetSeq J a c i)) : ℝ≥0∞) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
⊢ (↑(#(pairSetSeq J a c (i + 1))) : ℝ≥0∞) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius
have pos : ∀ (h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty),
  (↑(#(pairSetSeq J a c (i + 1))) : ℝ≥0∞) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius
Tactic: by_cases! h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
-- 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
hJ : J.Nonempty
ha : 1 < a
i : ℕ
ih :
  (↑(#(pairSetSeq J a c i)) : ℝ≥0∞) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
pos :
  ∀ (h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty),
    (↑(#(pairSetSeq J a c (i + 1))) : ℝ≥0∞) ≤
      (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
        a ^ (logSizeBallSeq J hJ a c (i + 1)).radius
⊢ (↑(#(pairSetSeq J a c (i + 1))) : ℝ≥0∞) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius
have neg : ∀ (h : (logSizeBallSeq J hJ a c (i + 1)).finset = ∅),
  (↑(#(pairSetSeq J a c (i + 1))) : ℝ≥0∞) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius
Tactic: by_cases! h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
-- 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
hJ : J.Nonempty
i : ℕ
ha : 1 < a
⊢ (↑(#(pairSetSeq J a c i)) : ℝ≥0∞) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
have zero : (↑(#(pairSetSeq J a c 0)) : ℝ≥0∞) ≤
  (if (logSizeBallSeq J hJ a c 0).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c 0).radius
Tactic: induction i with
  | zero =>
    simpa [pairSetSeq, hJ, finset_logSizeBallSeq_zero, logSizeBallStruct.ball,
      radius_logSizeBallSeq_zero] using card_le_logSizeRadius_le_pow_logSizeRadius ha
  | succ i ih =>
    by_cases! h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
    · simpa [pairSetSeq, logSizeBallStruct.ball, h, hJ]
        using card_le_logSizeRadius_le_pow_logSizeRadius ha
    simp [pairSetSeq, logSizeBallStruct.ball, h, hJ]
Cleared hypotheses: 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
hJ : J.Nonempty
i : ℕ
ha : 1 < a
zero :
  (↑(#(pairSetSeq J a c 0)) : ℝ≥0∞) ≤
    (if (logSizeBallSeq J hJ a c 0).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c 0).radius
⊢ (↑(#(pairSetSeq J a c i)) : ℝ≥0∞) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
have succ : ∀ (i : ℕ)
  (ih :
    (↑(#(pairSetSeq J a c i)) : ℝ≥0∞) ≤
      (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius),
  (↑(#(pairSetSeq J a c (i + 1))) : ℝ≥0∞) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius
Tactic: induction i with
  | zero =>
    simpa [pairSetSeq, hJ, finset_logSizeBallSeq_zero, logSizeBallStruct.ball,
      radius_logSizeBallSeq_zero] using card_le_logSizeRadius_le_pow_logSizeRadius ha
  | succ i ih =>
    by_cases! h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
    · simpa [pairSetSeq, logSizeBallStruct.ball, h, hJ]
        using card_le_logSizeRadius_le_pow_logSizeRadius ha
    simp [pairSetSeq, logSizeBallStruct.ball, h, hJ]
Cleared hypotheses: 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
hJ : J.Nonempty
i_1 : ℕ
ha : 1 < a
i : ℕ
⊢ (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    (↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c)) : ℝ≥0∞)
have pos : ∀ (h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty),
  (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    (↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c)) : ℝ≥0∞)
Tactic: by_cases! h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
-- 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
hJ : J.Nonempty
i_1 : ℕ
ha : 1 < a
i : ℕ
pos :
  ∀ (h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty),
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
        a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
      (↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c)) : ℝ≥0∞)
⊢ (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    (↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c)) : ℝ≥0∞)
have neg : ∀ (h : (logSizeBallSeq J hJ a c (i + 1)).finset = ∅),
  (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    (↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c)) : ℝ≥0∞)
Tactic: by_cases! h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
-- 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
ha : 1 < a
⊢ (↑(#(pairSet J a c)) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞)
have inr : ∀
  (this :
    ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {J : Finset T} [inst_2 : DecidableEq T] (ha : 1 < a)
      (hJ : J.Nonempty), (↑(#(pairSet J a c)) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞))
  (hJ : ¬J.Nonempty), (↑(#(pairSet J a c)) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞)
Tactic: wlog hJ : J.Nonempty
-- 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
ha : 1 < a
inr :
  ∀
    (this :
      ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {J : Finset T} [inst_2 : DecidableEq T] (ha : 1 < a)
        (hJ : J.Nonempty), (↑(#(pairSet J a c)) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞))
    (hJ : ¬J.Nonempty), (↑(#(pairSet J a c)) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞)
⊢ (↑(#(pairSet J a c)) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞)
have wlog : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {J : Finset T} [inst_2 : DecidableEq T] (ha : 1 < a)
  (hJ : J.Nonempty), (↑(#(pairSet J a c)) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞)
Tactic: wlog hJ : J.Nonempty
Cleared hypotheses: ha
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ (↑(#((Finset.range #J).biUnion (pairSetSeq J a c))) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞)
have grw : ∑ i ∈ Finset.range #J,
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1 + 1) ≤
  a * (↑(#J) : ℝ≥0∞)
Tactic: grw [Finset.card_biUnion_le, Nat.cast_sum,
    Finset.sum_le_sum fun i _ ↦ card_pairSetSeq_le_logSizeRadius_mul hJ i ha,
    Finset.sum_le_sum fun _ _ ↦ mul_le_mul_right (pow_le_pow_right₀ ha.le le_tsub_add) _]
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
grw :
  ∑ i ∈ Finset.range #J,
      (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) *
        a ^ ((logSizeBallSeq J hJ a c i).radius - 1 + 1) ≤
    a * (↑(#J) : ℝ≥0∞)
⊢ (↑(#((Finset.range #J).biUnion (pairSetSeq J a c))) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞)
have grw₁ : ℕ → ℕ
Tactic: grw [Finset.card_biUnion_le, Nat.cast_sum,
    Finset.sum_le_sum fun i _ ↦ card_pairSetSeq_le_logSizeRadius_mul hJ i ha,
    Finset.sum_le_sum fun _ _ ↦ mul_le_mul_right (pow_le_pow_right₀ ha.le le_tsub_add) _]
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
| ∑ i ∈ Finset.range #J,
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1 + 1)
have enter : fun (i : ℕ) ↦
  (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1 + 1)
Tactic: enter [2]
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
| fun (i : ℕ) ↦
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1 + 1)
have h : ∀ (x : ℕ),
  (if (logSizeBallSeq J hJ a c x).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c x).radius - 1 + 1)
Tactic: ext _
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
x : ℕ
| (if (logSizeBallSeq J hJ a c x).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c x).radius - 1 + 1)
have h : a * ((if (logSizeBallSeq J hJ a c x).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c x).radius - 1))
Tactic: rw [pow_add, pow_one, ← mul_assoc, mul_comm]
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
| ∑ i ∈ Finset.range #J,
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1 + 1)
have h : ∀ (x : ℕ),
  a * ((if (logSizeBallSeq J hJ a c x).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c x).radius - 1))
Tactic: enter [2]; ext _; rw [pow_add, pow_one, ← mul_assoc, mul_comm]
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ∑ x ∈ Finset.range #J,
      a *
        ((if (logSizeBallSeq J hJ a c x).finset.Nonempty then 1 else 0) *
          a ^ ((logSizeBallSeq J hJ a c x).radius - 1)) ≤
    a * (↑(#J) : ℝ≥0∞)
have grw : a *
    ∑ i ∈ Finset.range #J,
      (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1) ≤
  a * (↑(#J) : ℝ≥0∞)
Tactic: grw [← Finset.mul_sum]
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ a *
      ∑ i ∈ Finset.range #J,
        (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1) ≤
    a * (↑(#J) : ℝ≥0∞)
have bc : LE.le (α := ℝ≥0∞)
  (∑ i ∈ Finset.range #J,
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1))
  (↑(#J) : ℝ≥0∞)
Tactic: gcongr
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ LE.le (α := ℝ≥0∞)
    (∑ i ∈ Finset.range #J,
      (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1))
    (↑(#J) : ℝ≥0∞)
have bc : LE.le (α := ℝ≥0∞)
  (↑(Finset.card.{u_1} (α := T) ((Finset.range #J).biUnion fun (x : ℕ) ↦ (logSizeBallSeq J hJ a c x).smallBall c)) :
    ℝ≥0∞)
  (↑(#J) : ℝ≥0∞)
Tactic: grw [Finset.sum_le_sum fun i _ ↦ logSizeRadius_le_card_smallBall hJ i ha, ← Nat.cast_sum,
    ← Finset.card_biUnion fun _ _ _ _ ↦ disjoint_smallBall_logSizeBallSeq hJ]
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ LE.le (α := ℝ≥0∞)
    (↑(Finset.card.{u_1} (α := T) ((Finset.range #J).biUnion fun (x : ℕ) ↦ (logSizeBallSeq J hJ a c x).smallBall c)) :
      ℝ≥0∞)
    (↑(#J) : ℝ≥0∞)
have bc : ((Finset.range #J).biUnion fun (x : ℕ) ↦ (logSizeBallSeq J hJ a c x).smallBall c) ⊆ J
Tactic: gcongr
-- 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∞
J_1 : Finset T_1
inst_1 : DecidableEq T_1
T : Type u_1
inst_2 : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_3 : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ((Finset.range #J).biUnion fun (x : ℕ) ↦
      {x_1 ∈ (logSizeBallSeq J hJ a c x).finset |
        edist (logSizeBallSeq J hJ a c x).point x_1 ≤
          HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c x).radius : ℝ≥0∞) 1 * c}) ⊆
    J
have bc : ∀ x ∈ Finset.range #J,
  {x_1 ∈ (logSizeBallSeq J hJ a c x).finset |
      edist (logSizeBallSeq J hJ a c x).point x_1 ≤
        HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c x).radius : ℝ≥0∞) 1 * c} ⊆
    J
Tactic: rw [Finset.biUnion_subset_iff_forall_subset]
-- 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
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c
have obtain : ∀ (i : ℕ) (hiJ : i < #J) (h' : (s, t) ∈ pairSetSeq J a c i), edist s t ≤ (↑n : ℝ≥0∞) * c
Tactic: obtain ⟨i, hiJ, h'⟩ : ∃ i < #J, (s, t) ∈ pairSetSeq J a c i := by simpa [pairSet] using 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
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
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c
have hJ : J.Nonempty
Tactic: have hJ : J.Nonempty := Finset.card_pos.mp (Nat.zero_lt_of_lt hiJ)
-- 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
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c
have 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
Tactic: wlog! hn : 1 ≤ n