awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
i_1 : ℕ
ha : 1 < a
i : ℕ
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:
simpa [h, logSizeBallStruct.smallBall, radius_logSizeBallSeq_add_one]
        using pow_logSizeRadius_le_card_le_logSizeRadius ha (point_mem_finset_logSizeBallSeq hJ _ h)

Premises used: PairReduction.pow_logSizeRadius_le_card_le_logSizeRadius, PairReduction.logSizeBallStruct.smallBall, PairReduction.radius_logSizeBallSeq_add_one, PairReduction.point_mem_finset_logSizeBallSeq
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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 : ℕ
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:
simp [h]
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
⊢ (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1) ≤
    (↑(#((logSizeBallSeq J hJ a c i).smallBall c)) : ℝ≥0∞)

Tactic:
match i with
  | 0 =>
    simpa [finset_logSizeBallSeq_zero, hJ, logSizeBallStruct.smallBall, radius_logSizeBallSeq_zero]
      using pow_logSizeRadius_le_card_le_logSizeRadius ha (Exists.choose_spec hJ)
  | i + 1 =>
    by_cases! h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
    · simpa [h, logSizeBallStruct.smallBall, radius_logSizeBallSeq_add_one]
        using pow_logSizeRadius_le_card_le_logSizeRadius ha (point_mem_finset_logSizeBallSeq hJ _ h)
    simp [h]
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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∞)
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∞)
⊢ (↑(#(pairSet J a c)) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞)

Tactic:
wlog hJ : J.Nonempty

Premises used: Finset.Nonempty
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
ha : 1 < a
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:
simp [Finset.not_nonempty_iff_eq_empty.mp hJ]

Premises used: Finset.not_nonempty_iff_eq_empty, Iff.mp
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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∞)
grw₁ : ℕ → ℕ
⊢ (↑(#((Finset.range #J).biUnion (pairSetSeq J a c))) : ℝ≥0∞) ≤ 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) _]

Premises used: PairReduction.card_pairSetSeq_le_logSizeRadius_mul, mul_le_mul_right, LT.lt.le, pow_le_pow_right₀, Nat.cast_sum, Finset.card_biUnion_le, Finset.sum_le_sum, le_tsub_add
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
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)
| ∑ 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)

Tactic:
enter [2]
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
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)
| 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:
ext _
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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 : ℕ
h : a * ((if (logSizeBallSeq J hJ a c x).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c x).radius - 1))
| (if (logSizeBallSeq J hJ a c x).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c x).radius - 1 + 1)

Tactic:
rw [pow_add, pow_one, ← mul_assoc, mul_comm]

Premises used: mul_assoc, pow_add, pow_one, mul_comm
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
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))
| ∑ 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)

Tactic:
enter [2]; ext _; rw [pow_add, pow_one, ← mul_assoc, mul_comm]

Premises used: mul_assoc, pow_add, pow_one, mul_comm
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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 :
  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∞)
⊢ ∑ 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∞)

Tactic:
grw [← Finset.mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
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∞)
⊢ 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:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
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∞)
⊢ 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:
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]

Premises used: PairReduction.disjoint_smallBall_logSizeBallSeq, Finset.card_biUnion, Nat.cast_sum, Finset.sum_le_sum, PairReduction.logSizeRadius_le_card_smallBall
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
bc : ((Finset.range #J).biUnion fun (x : ℕ) ↦ (logSizeBallSeq J hJ a c x).smallBall c) ⊆ J
⊢ 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:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
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
⊢ ((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

Tactic:
rw [Finset.biUnion_subset_iff_forall_subset]

Premises used: Finset.biUnion_subset_iff_forall_subset
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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 : ℕ
bc :
  i ∈ Finset.range #J →
    {x ∈ (logSizeBallSeq J hJ a c i).finset |
        edist (logSizeBallSeq J hJ a c i).point x ≤
          HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c i).radius : ℝ≥0∞) 1 * c} ⊆
      J
⊢ i ∈ Finset.range #J →
    {x ∈ (logSizeBallSeq J hJ a c i).finset |
        edist (logSizeBallSeq J hJ a c i).point x ≤
          HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c i).radius : ℝ≥0∞) 1 * c} ⊆
      J

Tactic:
_
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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 : ℕ
h : i ∈ Finset.range #J
⊢ {x ∈ (logSizeBallSeq J hJ a c i).finset |
      edist (logSizeBallSeq J hJ a c i).point x ≤
        HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c i).radius : ℝ≥0∞) 1 * c} ⊆
    J

Tactic:
(Finset.filter_subset _ _).trans (finset_logSizeBallSeq_subset_logSizeBallSeq_init _ _)

Premises used: Finset.filter_subset, HasSubset.Subset.trans, PairReduction.finset_logSizeBallSeq_subset_logSizeBallSeq_init
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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 : ℕ
h : i ∈ Finset.range #J
⊢ {x ∈ (logSizeBallSeq J hJ a c i).finset |
      edist (logSizeBallSeq J hJ a c i).point x ≤
        HSub.hSub (α := ℝ≥0∞) (↑(logSizeBallSeq J hJ a c i).radius : ℝ≥0∞) 1 * c} ⊆
    J

Tactic:
exact (Finset.filter_subset _ _).trans (finset_logSizeBallSeq_subset_logSizeBallSeq_init _ _)

Premises used: Finset.filter_subset, HasSubset.Subset.trans, PairReduction.finset_logSizeBallSeq_subset_logSizeBallSeq_init
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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 < #J, (s, t) ∈ pairSetSeq J a c i

Tactic:
simpa [pairSet] using h

Premises used: PairReduction.pairSet
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
obtain : ∀ (i : ℕ) (hiJ : i < #J) (h' : (s, t) ∈ pairSetSeq J a c i), edist s t ≤ (↑n : ℝ≥0∞) * c
⊢ 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

Premises used: Prod.mk
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
⊢ J.Nonempty

Tactic:
have hJ : J.Nonempty := Finset.card_pos.mp (Nat.zero_lt_of_lt hiJ)
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
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
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c

Tactic:
wlog! hn : 1 ≤ n
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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_1 :
  ∀ {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
this : s = t
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c

Tactic:
simp [this]
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
inr : s = t
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c

Tactic:
suffices s = t by simp [this]
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
⊢ #J ≤ 1

Tactic:
simp only [Nat.lt_one_iff.mp hn, pow_zero, Nat.cast_le_one] at hJ_card

Premises used: pow_zero, Nat.lt_one_iff, Iff.mp, Nat.cast_le_one
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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).1 ∈ J

Tactic:
have ⟨hs, ht⟩ := Finset.mem_product.mp (pairSet_subset h)
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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).2 ∈ J

Tactic:
have ⟨hs, ht⟩ := Finset.mem_product.mp (pairSet_subset h)
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
ht : (s, t).2 ∈ J
⊢ s = t

Tactic:
Finset.card_le_one_iff.mp hJ_card hs ht

Premises used: Finset.card_le_one_iff, Iff.mp
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
ht : (s, t).2 ∈ J
⊢ s = t

Tactic:
exact Finset.card_le_one_iff.mp hJ_card hs ht

Premises used: Finset.card_le_one_iff, Iff.mp
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
⊢ (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

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'

Premises used: exists_eq_right_right, Finset.product_eq_sprod, reduceDIte, PairReduction.pairSetSeq, PairReduction.logSizeBallStruct.ball, Prod.mk.injEq, Function.Embedding.coeFn_mk, Finset.mem_filter, Finset.singleton_product, Finset.mem_map
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
obtain :
  ∀ (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
⊢ edist s t ≤ (↑n : ℝ≥0∞) * c

Tactic:
obtain ⟨⟨ht, hdist⟩, rfl⟩ := h'

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
grw₁ grw₂ : (↑n : ℝ≥0∞) * c ≤ (↑n : ℝ≥0∞) * c
⊢ edist (logSizeBallSeq J ⋯ a c i).point t ≤ (↑n : ℝ≥0∞) * c

Tactic:
grw [hdist, radius_logSizeBallSeq_le hJ ha hn hJ_card i]

Premises used: PairReduction.radius_logSizeBallSeq_le
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
E : Type u_2
inst_2 : PseudoEMetricSpace E
ha : 1 < a
f : T → E
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))
⊢ ⨆ (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))

Tactic:
rw [iSup_le_iff]

Premises used: iSup_le_iff