awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ = 1
this :
  Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 <
    Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯
h :
  ¬(1 ≤ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 ∧
      (↑(#({x ∈ V |
                edist t x ≤
                  (↑(Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n)
                            ⋯ -
                          1) :
                      ℝ≥0∞) *
                    c})) :
          ℝ≥0∞) ≤
        a ^ (Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1))
⊢ 1 ≤ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 →
    a ^ (Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1) <
      (↑(#({x ∈ V |
              edist t x ≤
                HSub.hSub (α := ℝ≥0∞)
                    (↑(Nat.find (p := fun (n : ℕ) ↦
                          1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯) :
                      ℝ≥0∞)
                    1 *
                  c})) :
        ℝ≥0∞)

Tactic:
simp only [ENNReal.natCast_sub, Nat.cast_one, not_and, not_le] at h

Premises used: not_le, ENNReal.natCast_sub, not_and, Nat.cast_one
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ = 1
this :
  Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 <
    Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯
h :
  1 ≤ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 →
    a ^ (Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1) <
      (↑(#({x ∈ V |
              edist t x ≤
                HSub.hSub (α := ℝ≥0∞)
                    (↑(Nat.find (p := fun (n : ℕ) ↦
                          1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯) :
                      ℝ≥0∞)
                    1 *
                  c})) :
        ℝ≥0∞)
⊢ 1 ≤ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1

Tactic:
lia
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ = 1
this :
  Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 <
    Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯
h :
  1 ≤ Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1 →
    a ^ (Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1) <
      (↑(#({x ∈ V |
              edist t x ≤
                HSub.hSub (α := ℝ≥0∞)
                    (↑(Nat.find (p := fun (n : ℕ) ↦
                          1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯) :
                      ℝ≥0∞)
                    1 *
                  c})) :
        ℝ≥0∞)
⊢ a ^ (Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ - 1) ≤
    (↑(#({x ∈ V |
            edist t x ≤
              HSub.hSub (α := ℝ≥0∞)
                  (↑(Nat.find (p := fun (n : ℕ) ↦ 1 ≤ n ∧ (↑(#({x ∈ V | edist t x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n)
                        ⋯) :
                    ℝ≥0∞)
                  1 *
                c})) :
      ℝ≥0∞)

Tactic:
exact (h (by lia)).le

Premises used: LT.lt.le
-- 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
⊢ (logSizeBallSeq J hJ a c 0).finset = J

Tactic:
rfl

Premises used: rfl
-- 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
⊢ (logSizeBallSeq J hJ a c 0).point = Exists.choose (p := Membership.mem J) hJ

Tactic:
rfl

Premises used: Classical.choose, rfl
-- 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
⊢ (logSizeBallSeq J hJ a c 0).radius = logSizeRadius (Exists.choose (p := Membership.mem J) hJ) J a c

Tactic:
rfl

Premises used: PairReduction.logSizeRadius, dite, rfl
-- 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 : ℕ
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset =
    (logSizeBallSeq J hJ a c i).finset \ (logSizeBallSeq J hJ a c i).smallBall c

Tactic:
rfl

Premises used: rfl
-- 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 : ℕ
⊢ (logSizeBallSeq J hJ a c (i + 1)).point =
    if hV' : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then
      Exists.choose (p := Membership.mem (logSizeBallSeq J hJ a c (i + 1)).finset) hV'
    else (logSizeBallSeq J hJ a c i).point

Tactic:
rfl

Premises used: Set.Mem, setOf, dite, Multiset.pmap, Multiset.sub, Multiset.attach, rfl
-- 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 : ℕ
⊢ (logSizeBallSeq J hJ a c (i + 1)).radius =
    logSizeRadius (logSizeBallSeq J hJ a c (i + 1)).point (logSizeBallSeq J hJ a c (i + 1)).finset a c

Tactic:
rfl

Premises used: PairReduction.logSizeRadius, dite, Multiset.pmap, Multiset.sub, Multiset.attach, rfl
-- 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 : ℕ
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset

Tactic:
simp [finset_logSizeBallSeq_add_one]

Premises used: PairReduction.finset_logSizeBallSeq_add_one
-- 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
⊢ Antitone.{0, u_1} (β := Finset T) fun (i : ℕ) ↦ (logSizeBallSeq J hJ a c i).finset

Tactic:
antitone_nat_of_succ_le (finset_logSizeBallSeq_add_one_subset hJ)

Premises used: antitone_nat_of_succ_le, PairReduction.finset_logSizeBallSeq_add_one_subset
-- 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 : ℕ
apply : (fun (i : ℕ) ↦ (logSizeBallSeq J hJ a c i).finset) 0 ⊆ J
⊢ (logSizeBallSeq J hJ a c i).finset ⊆ J

Tactic:
apply subset_trans <| antitone_logSizeBallSeq_add_one_subset hJ zero_le

Premises used: zero_le, subset_trans, PairReduction.antitone_logSizeBallSeq_add_one_subset
-- 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 : ℕ
⊢ (fun (i : ℕ) ↦ (logSizeBallSeq J hJ a c i).finset) 0 ⊆ J

Tactic:
simp [finset_logSizeBallSeq_zero]

Premises used: PairReduction.finset_logSizeBallSeq_zero
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i : ℕ
simp :
  Nat.find (p := fun (n : ℕ) ↦
      1 ≤ n ∧ (↑(#({x ∈ J | edist (Exists.choose (p := Membership.mem J) hJ) x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ ≤
    n
⊢ (logSizeBallSeq J hJ a c 0).radius ≤ n

Tactic:
simp only [radius_logSizeBallSeq_zero, logSizeRadius, ha, ↓reduceDIte]

Premises used: PairReduction.logSizeRadius, reduceDIte, PairReduction.radius_logSizeBallSeq_zero
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i : ℕ
a₁ : {x ∈ J | edist (Exists.choose (p := Membership.mem J) hJ) x ≤ (↑n : ℝ≥0∞) * c} ⊆ J
⊢ LE.le (α := ℝ≥0∞) (↑(#({x ∈ J | edist (Exists.choose (p := Membership.mem J) hJ) x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞)
    (↑(#J) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i : ℕ
⊢ {x ∈ J | edist (Exists.choose (p := Membership.mem J) hJ) x ≤ (↑n : ℝ≥0∞) * c} ⊆ J

Tactic:
apply Finset.filter_subset

Premises used: Finset.filter_subset
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i : ℕ
⊢ Nat.find (p := fun (n : ℕ) ↦
      1 ≤ n ∧ (↑(#({x ∈ J | edist (Exists.choose (p := Membership.mem J) hJ) x ≤ (↑n : ℝ≥0∞) * c})) : ℝ≥0∞) ≤ a ^ n) ⋯ ≤
    n

Tactic:
exact Nat.find_min' _ ⟨hn, le_trans (by gcongr; apply Finset.filter_subset) hJ_card⟩

Premises used: Nat.find_min'
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i_1 i : ℕ
simp :
  Nat.find (p := fun (n : ℕ) ↦
      1 ≤ n ∧
        (↑(#({x ∈ (logSizeBallSeq J hJ a c (i + 1)).finset |
                  edist (logSizeBallSeq J hJ a c (i + 1)).point x ≤ (↑n : ℝ≥0∞) * c})) :
            ℝ≥0∞) ≤
          a ^ n)
      ⋯ ≤
    n
⊢ (logSizeBallSeq J hJ a c (i + 1)).radius ≤ n

Tactic:
simp only [radius_logSizeBallSeq_add_one, logSizeRadius, ha, ↓reduceDIte]

Premises used: PairReduction.logSizeRadius, reduceDIte, PairReduction.radius_logSizeBallSeq_add_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
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i_1 i : ℕ
⊢ Nat.find (p := fun (n : ℕ) ↦
      1 ≤ n ∧
        (↑(#({x ∈ (logSizeBallSeq J hJ a c (i + 1)).finset |
                  edist (logSizeBallSeq J hJ a c (i + 1)).point x ≤ (↑n : ℝ≥0∞) * c})) :
            ℝ≥0∞) ≤
          a ^ n)
      ⋯ ≤
    n

Tactic:
Nat.find_min' _ ⟨hn, le_trans ?_ hJ_card⟩

Premises used: Nat.find_min', And.intro, le_trans
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i_1 i : ℕ
refine :
  LE.le (α := ℝ≥0∞)
    (↑(#({x ∈ (logSizeBallSeq J hJ a c (i + 1)).finset |
            edist (logSizeBallSeq J hJ a c (i + 1)).point x ≤ (↑n : ℝ≥0∞) * c})) :
      ℝ≥0∞)
    (↑(#J) : ℝ≥0∞)
⊢ Nat.find (p := fun (n : ℕ) ↦
      1 ≤ n ∧
        (↑(#({x ∈ (logSizeBallSeq J hJ a c (i + 1)).finset |
                  edist (logSizeBallSeq J hJ a c (i + 1)).point x ≤ (↑n : ℝ≥0∞) * c})) :
            ℝ≥0∞) ≤
          a ^ n)
      ⋯ ≤
    n

Tactic:
refine Nat.find_min' _ ⟨hn, le_trans ?_ hJ_card⟩

Premises used: Nat.find_min'
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i_1 i : ℕ
a₁ :
  {x ∈ (logSizeBallSeq J hJ a c (i + 1)).finset | edist (logSizeBallSeq J hJ a c (i + 1)).point x ≤ (↑n : ℝ≥0∞) * c} ⊆ J
⊢ LE.le (α := ℝ≥0∞)
    (↑(#({x ∈ (logSizeBallSeq J hJ a c (i + 1)).finset |
            edist (logSizeBallSeq J hJ a c (i + 1)).point x ≤ (↑n : ℝ≥0∞) * c})) :
      ℝ≥0∞)
    (↑(#J) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i_1 i : ℕ
⊢ {x ∈ (logSizeBallSeq J hJ a c (i + 1)).finset | edist (logSizeBallSeq J hJ a c (i + 1)).point x ≤ (↑n : ℝ≥0∞) * 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 : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i_1 i : ℕ
⊢ {x ∈ (logSizeBallSeq J hJ a c (i + 1)).finset | edist (logSizeBallSeq J hJ a c (i + 1)).point x ≤ (↑n : ℝ≥0∞) * 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
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
i : ℕ
⊢ (logSizeBallSeq J hJ a c i).radius ≤ n

Tactic:
match i with
  | 0 =>
    simp only [radius_logSizeBallSeq_zero, logSizeRadius, ha, ↓reduceDIte]
    exact Nat.find_min' _ ⟨hn, le_trans (by gcongr; apply Finset.filter_subset) hJ_card⟩
  | i + 1 =>
    simp only [radius_logSizeBallSeq_add_one, logSizeRadius, ha, ↓reduceDIte]
    refine Nat.find_min' _ ⟨hn, le_trans ?_ hJ_card⟩
    gcongr
    exact (Finset.filter_subset _ _).trans (finset_logSizeBallSeq_subset_logSizeBallSeq_init _ _)
-- 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
ha : 1 < a
i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c 0).radius

Tactic:
one_le_logSizeRadius ha

Premises used: PairReduction.one_le_logSizeRadius, PairReduction.logSizeRadius, dite
-- 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
ha : 1 < a
i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c 0).radius

Tactic:
exact one_le_logSizeRadius ha

Premises used: PairReduction.one_le_logSizeRadius
-- 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
ha : 1 < a
i_1 i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c (i + 1)).radius

Tactic:
one_le_logSizeRadius ha

Premises used: PairReduction.one_le_logSizeRadius, PairReduction.logSizeRadius, dite
-- 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
ha : 1 < a
i_1 i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c (i + 1)).radius

Tactic:
exact one_le_logSizeRadius ha

Premises used: PairReduction.one_le_logSizeRadius
-- 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
ha : 1 < a
i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c i).radius

Tactic:
match i with
  | 0 => exact one_le_logSizeRadius ha
  | i + 1 => exact one_le_logSizeRadius ha
-- 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 : ℕ
h : (logSizeBallSeq J hJ a c 0).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c 0).point ∈ (logSizeBallSeq J hJ a c 0).finset

Tactic:
simp [point_logSizeBallSeq_zero, finset_logSizeBallSeq_zero, Exists.choose_spec]

Premises used: Exists.choose_spec, PairReduction.finset_logSizeBallSeq_zero, PairReduction.point_logSizeBallSeq_zero
-- 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 i : ℕ
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ (logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
simp [point_logSizeBallSeq_add_one, h, Exists.choose_spec]

Premises used: Exists.choose_spec, PairReduction.point_logSizeBallSeq_add_one
-- 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 : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∈ (logSizeBallSeq J hJ a c i).finset

Tactic:
match i with
  | 0 => simp [point_logSizeBallSeq_zero, finset_logSizeBallSeq_zero, Exists.choose_spec]
  | i + 1 => simp [point_logSizeBallSeq_add_one, h, Exists.choose_spec]
-- 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
⊢ (logSizeBallSeq J hJ a c 0).point ∈ J

Tactic:
point_mem_finset_logSizeBallSeq hJ 0 hJ

Premises used: Set.Mem, setOf, PairReduction.point_mem_finset_logSizeBallSeq, OfNat.ofNat
-- 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
⊢ (logSizeBallSeq J hJ a c 0).point ∈ J

Tactic:
exact point_mem_finset_logSizeBallSeq hJ 0 hJ

Premises used: PairReduction.point_mem_finset_logSizeBallSeq, OfNat.ofNat
-- 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 : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
pos : ∀ (h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty), (logSizeBallSeq J hJ a c (i + 1)).point ∈ J
neg : ∀ (h : ¬(logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty), (logSizeBallSeq J hJ a c (i + 1)).point ∈ J
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

Tactic:
by_cases h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty

Premises used: HAdd.hAdd, PairReduction.logSizeBallSeq, Finset.Nonempty, PairReduction.logSizeBallStruct.finset, OfNat.ofNat
-- 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 : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

Tactic:
Finset.mem_of_subset ?_ (point_mem_finset_logSizeBallSeq hJ (i + 1) h)

Premises used: HAdd.hAdd, PairReduction.point_mem_finset_logSizeBallSeq, OfNat.ofNat, Finset.mem_of_subset
-- 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 : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
pos : (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ J
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

Tactic:
refine Finset.mem_of_subset ?_ (point_mem_finset_logSizeBallSeq hJ (i + 1) h)

Premises used: HAdd.hAdd, PairReduction.point_mem_finset_logSizeBallSeq, OfNat.ofNat, Finset.mem_of_subset
-- 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 : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ J

Tactic:
apply finset_logSizeBallSeq_subset_logSizeBallSeq_init

Premises used: PairReduction.finset_logSizeBallSeq_subset_logSizeBallSeq_init
-- 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 : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
h : ¬(logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

Tactic:
simp [point_logSizeBallSeq_add_one, ih, h]

Premises used: PairReduction.point_logSizeBallSeq_add_one
-- 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 : ℕ
zero : (logSizeBallSeq J hJ a c 0).point ∈ J
succ : ∀ (i : ℕ) (ih : (logSizeBallSeq J hJ a c i).point ∈ J), (logSizeBallSeq J hJ a c (i + 1)).point ∈ J
⊢ (logSizeBallSeq J hJ a c i).point ∈ J

Tactic:
induction i with
  | zero => exact point_mem_finset_logSizeBallSeq hJ 0 hJ
  | succ i ih =>
    by_cases h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
    · refine Finset.mem_of_subset ?_ (point_mem_finset_logSizeBallSeq hJ (i + 1) h)
      apply finset_logSizeBallSeq_subset_logSizeBallSeq_init
    simp [point_logSizeBallSeq_add_one, ih, h]

Premises used: HAdd.hAdd, PairReduction.logSizeBallSeq, Finset.Nonempty, PairReduction.finset_logSizeBallSeq_subset_logSizeBallSeq_init, PairReduction.point_mem_finset_logSizeBallSeq, PairReduction.logSizeBallStruct.finset, PairReduction.point_logSizeBallSeq_add_one, OfNat.ofNat
-- 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 : ℕ
⊢ (logSizeBallSeq J hJ a c i).point ∉ (logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
simp [finset_logSizeBallSeq_add_one, logSizeBallStruct.smallBall]

Premises used: PairReduction.logSizeBallStruct.smallBall, PairReduction.finset_logSizeBallSeq_add_one
-- 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 : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
h₁ : (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset
h₂ : ¬(logSizeBallSeq J hJ a c i).finset ⊆ (logSizeBallSeq J hJ a c (i + 1)).finset
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊂ (logSizeBallSeq J hJ a c i).finset

Tactic:
apply ssubset_of_subset_not_subset

Premises used: ssubset_of_subset_not_subset
-- 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 : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset

Tactic:
simp [finset_logSizeBallSeq_add_one]

Premises used: PairReduction.finset_logSizeBallSeq_add_one
-- 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 : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ ¬(logSizeBallSeq J hJ a c i).finset ⊆ (logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
Set.not_subset.mpr ⟨(logSizeBallSeq J hJ a c i).point, ?_, ?_⟩

Premises used: Iff.mpr, Set.Subset, PairReduction.logSizeBallStruct.point, And.intro, PairReduction.logSizeBallSeq, Set.not_subset, Exists.intro