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 : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
h₂ : (logSizeBallSeq J hJ a c i).point ∈ (↑(logSizeBallSeq J hJ a c i).finset : Set T)
h₃ : (logSizeBallSeq J hJ a c i).point ∉ (↑(logSizeBallSeq J hJ a c (i + 1)).finset : Set T)
⊢ ¬(logSizeBallSeq J hJ a c i).finset ⊆ (logSizeBallSeq J hJ a c (i + 1)).finset

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

Premises used: Iff.mpr, PairReduction.logSizeBallStruct.point, And.intro, PairReduction.logSizeBallSeq, Set.not_subset, Exists.intro
-- 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 : Set T)

Tactic:
point_mem_finset_logSizeBallSeq hJ i h

Premises used: 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 : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∈ (↑(logSizeBallSeq J hJ a c i).finset : Set T)

Tactic:
exact point_mem_finset_logSizeBallSeq hJ i h

Premises used: 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 : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∉ (↑(logSizeBallSeq J hJ a c (i + 1)).finset : Set T)

Tactic:
point_notMem_finset_logSizeBallSeq_add_one hJ i

Premises used: PairReduction.point_notMem_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).point ∉ (↑(logSizeBallSeq J hJ a c (i + 1)).finset : Set T)

Tactic:
exact point_notMem_finset_logSizeBallSeq_add_one hJ i

Premises used: PairReduction.point_notMem_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 + 1)).finset < #(logSizeBallSeq J hJ a c i).finset

Tactic:
simp [Finset.card_lt_card, finset_logSizeBallSeq_add_one_ssubset hJ i h]

Premises used: Finset.card_lt_card, PairReduction.finset_logSizeBallSeq_add_one_ssubset
-- 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 - 0

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∞
J : Finset T
inst_1 : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
pos : ∀ (h : (logSizeBallSeq J hJ a c i).finset.Nonempty), #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)
neg : ∀ (h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty), #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)
⊢ #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)

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

Premises used: PairReduction.logSizeBallSeq, Finset.Nonempty, PairReduction.logSizeBallStruct.finset
-- 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).finset ≤ #J - 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:
have := card_finset_logSizeBallSeq_add_one_lt hJ i 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 : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
this : #(logSizeBallSeq J hJ a c (i + 1)).finset < #(logSizeBallSeq J hJ a c i).finset
⊢ #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)

Tactic:
lia
-- 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).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
neg : #(logSizeBallSeq J hJ a c i).finset ≤ #J - (i + 1)
⊢ #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)

Tactic:
apply le_trans <| Finset.card_le_card (finset_logSizeBallSeq_add_one_subset hJ i)

Premises used: Finset.card_le_card, PairReduction.finset_logSizeBallSeq_add_one_subset, le_trans
-- 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).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
this : #(logSizeBallSeq J hJ a c i).finset = 0
⊢ #(logSizeBallSeq J hJ a c i).finset ≤ #J - (i + 1)

Tactic:
simp [this]
-- 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).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
neg : #(logSizeBallSeq J hJ a c i).finset = 0
⊢ #(logSizeBallSeq J hJ a c i).finset ≤ #J - (i + 1)

Tactic:
suffices #(logSizeBallSeq J hJ a c i).finset = 0 by simp [this]
-- 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).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
neg : ¬#(logSizeBallSeq J hJ a c i).finset ≠ 0
neg₁ neg₂ neg₃ neg₄ : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ #(logSizeBallSeq J hJ a c i).finset = 0

Tactic:
rwa [← not_ne_iff, Finset.card_ne_zero.not]

Premises used: Iff.not, not_ne_iff, Finset.card_ne_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 : ℕ
zero : #(logSizeBallSeq J hJ a c 0).finset ≤ #J - 0
succ :
  ∀ (i : ℕ) (ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i),
    #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)
⊢ #(logSizeBallSeq J hJ a c i).finset ≤ #J - i

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]

Premises used: PairReduction.finset_logSizeBallSeq_zero, Finset.card_le_card, Iff.not, not_ne_iff, PairReduction.logSizeBallSeq, Finset.Nonempty, PairReduction.finset_logSizeBallSeq_add_one_subset, PairReduction.logSizeBallStruct.finset, Finset.card_ne_zero, le_trans
-- 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
rw : #(logSizeBallSeq J hJ a c #J).finset ≤ #J - #J
⊢ #(logSizeBallSeq J hJ a c #J).finset = 0

Tactic:
rw [← Nat.le_zero, ← tsub_self #J]

Premises used: tsub_self, Nat.le_zero, Finset.card
-- 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 #J).finset ≤ #J - #J

Tactic:
card_finset_logSizeBallSeq_le hJ #J

Premises used: PairReduction.card_finset_logSizeBallSeq_le, Finset.card
-- 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 #J).finset ≤ #J - #J

Tactic:
exact card_finset_logSizeBallSeq_le hJ #J

Premises used: PairReduction.card_finset_logSizeBallSeq_le, Finset.card
-- 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 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)
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)
⊢ 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
-- 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 j : ℕ
hij : i ≠ j
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:
Disjoint.symm <| this hij.symm <| (ne_iff_lt_iff_le.mpr h).mp hij.symm

Premises used: Iff.mpr, Ne.symm, Disjoint.symm, Iff.mp, ne_iff_lt_iff_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
i j : ℕ
hij : i ≠ j
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:
exact Disjoint.symm <| this hij.symm <| (ne_iff_lt_iff_le.mpr h).mp hij.symm

Premises used: Iff.mpr, Ne.symm, Disjoint.symm, Iff.mp, ne_iff_lt_iff_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
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
d : Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((fun (i : ℕ) ↦ (logSizeBallSeq J hJ a c i).finset) i.succ)
u : Finset T
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)

Tactic:
apply Finset.disjoint_of_subset_right

Premises used: Finset.disjoint_of_subset_right
-- 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 j : ℕ
hij : i ≠ j
h : i < j
⊢ (logSizeBallSeq J hJ a c j).smallBall c ⊆ (fun (i : ℕ) ↦ (logSizeBallSeq J hJ a c i).finset) i.succ

Tactic:
(Finset.filter_subset _ _).trans (antitone_logSizeBallSeq_add_one_subset hJ h)

Premises used: Set.Mem, setOf, Finset.filter_subset, HasSubset.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 j : ℕ
hij : i ≠ j
h : i < j
⊢ (logSizeBallSeq J hJ a c j).smallBall c ⊆ (fun (i : ℕ) ↦ (logSizeBallSeq J hJ a c i).finset) i.succ

Tactic:
exact (Finset.filter_subset _ _).trans (antitone_logSizeBallSeq_add_one_subset hJ h)

Premises used: Finset.filter_subset, HasSubset.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 j : ℕ
hij : i ≠ j
h : i < j
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((fun (i : ℕ) ↦ (logSizeBallSeq J hJ a c i).finset) i.succ)

Tactic:
simp [finset_logSizeBallSeq_add_one, Finset.disjoint_sdiff]

Premises used: PairReduction.finset_logSizeBallSeq_add_one, Finset.disjoint_sdiff
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
inst_1 : DecidableEq T
a c : ℝ≥0∞
⊢ Eq.{u_1 + 1} (α := Finset (T × T)) (pairSet ∅ a c) ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, PairReduction.pairSet, List.dedup, Multiset.zero, Finset.empty, Finset.biUnion, Multiset.ofList, List.pwFilter, List.foldr, rfl
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst_1 : DecidableEq T
rw : ∀ x ∈ Finset.range #J, pairSetSeq J a c x ⊆ J ×ˢ J
⊢ (Finset.range #J).biUnion (pairSetSeq J a c) ⊆ J ×ˢ J

Tactic:
rw [Finset.biUnion_subset_iff_forall_subset]

Premises used: Finset.biUnion_subset_iff_forall_subset
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
neg : ∀ (hJ : ¬J.Nonempty), pairSetSeq J a c i ⊆ J ×ˢ J
⊢ pairSetSeq J a c i ⊆ J ×ˢ J

Tactic:
by_cases 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
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
pos : Finset.product {(logSizeBallSeq J ⋯ a c i).point} ((logSizeBallSeq J ⋯ a c i).ball c) ⊆ J ×ˢ J
⊢ pairSetSeq J a c i ⊆ J ×ˢ J

Tactic:
simp only [pairSetSeq, hJ, ↓reduceDIte]

Premises used: reduceDIte, PairReduction.pairSetSeq
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
pos₁ : (logSizeBallSeq J ⋯ a c i).ball c ⊆ J
⊢ Finset.product {(logSizeBallSeq J ⋯ a c i).point} ((logSizeBallSeq J ⋯ a c i).ball c) ⊆ J ×ˢ J

Tactic:
apply Finset.product_subset_product

Premises used: Finset.product_subset_product
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
⊢ {(logSizeBallSeq J ⋯ a c i).point} ⊆ J

Tactic:
Finset.singleton_subset_iff.mpr (point_mem_logSizeBallSeq_init hJ _)

Premises used: Iff.mpr, PairReduction.point_mem_logSizeBallSeq_init, Finset.singleton_subset_iff
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
⊢ {(logSizeBallSeq J ⋯ a c i).point} ⊆ J

Tactic:
exact Finset.singleton_subset_iff.mpr (point_mem_logSizeBallSeq_init hJ _)

Premises used: Iff.mpr, PairReduction.point_mem_logSizeBallSeq_init, Finset.singleton_subset_iff
-- Module: Mathlib.Topology.EMetricSpace.PairReduction
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
⊢ (logSizeBallSeq J ⋯ a c i).ball c ⊆ J

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

Premises used: Set.Mem, setOf, 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∞
J : Finset T
inst_1 : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ (logSizeBallSeq J ⋯ a c i).ball 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∞
J : Finset T
inst_1 : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : ¬J.Nonempty
⊢ pairSetSeq J a c i ⊆ J ×ˢ J

Tactic:
simp [pairSetSeq, hJ]

Premises used: PairReduction.pairSetSeq
-- 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
⊢ (↑(#(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:
simpa [pairSetSeq, hJ, finset_logSizeBallSeq_zero, logSizeBallStruct.ball,
      radius_logSizeBallSeq_zero] using card_le_logSizeRadius_le_pow_logSizeRadius ha

Premises used: PairReduction.finset_logSizeBallSeq_zero, PairReduction.card_le_logSizeRadius_le_pow_logSizeRadius, PairReduction.pairSetSeq, PairReduction.logSizeBallStruct.ball, PairReduction.radius_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
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
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
⊢ (↑(#(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

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
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
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:
simpa [pairSetSeq, logSizeBallStruct.ball, h, hJ]
        using card_le_logSizeRadius_le_pow_logSizeRadius ha

Premises used: PairReduction.card_le_logSizeRadius_le_pow_logSizeRadius, PairReduction.pairSetSeq, PairReduction.logSizeBallStruct.ball
-- 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 : ℕ
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
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:
simp [pairSetSeq, logSizeBallStruct.ball, h, hJ]

Premises used: PairReduction.pairSetSeq, PairReduction.logSizeBallStruct.ball
-- 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
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
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
⊢ (↑(#(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

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]

Premises used: PairReduction.finset_logSizeBallSeq_zero, PairReduction.card_le_logSizeRadius_le_pow_logSizeRadius, PairReduction.pairSetSeq, PairReduction.logSizeBallStruct.ball, HAdd.hAdd, PairReduction.logSizeBallSeq, Finset.Nonempty, PairReduction.logSizeBallStruct.finset, OfNat.ofNat, PairReduction.radius_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 : ℕ
ha : 1 < a
⊢ (if (logSizeBallSeq J hJ a c 0).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c 0).radius - 1) ≤
    (↑(#((logSizeBallSeq J hJ a c 0).smallBall c)) : ℝ≥0∞)

Tactic:
simpa [finset_logSizeBallSeq_zero, hJ, logSizeBallStruct.smallBall, radius_logSizeBallSeq_zero]
      using pow_logSizeRadius_le_card_le_logSizeRadius ha (Exists.choose_spec hJ)

Premises used: Exists.choose_spec, PairReduction.finset_logSizeBallSeq_zero, PairReduction.pow_logSizeRadius_le_card_le_logSizeRadius, PairReduction.logSizeBallStruct.smallBall, PairReduction.radius_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 : ℕ
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∞)
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∞)
⊢ (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

Premises used: HAdd.hAdd, PairReduction.logSizeBallSeq, Finset.Nonempty, PairReduction.logSizeBallStruct.finset, OfNat.ofNat