/-
Copyright (c) 2021 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen

! This file was ported from Lean 3 source module number_theory.class_number.admissible_absolute_value
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Real.Basic
import Mathlib.Combinatorics.Pigeonhole
import Mathlib.Algebra.Order.EuclideanAbsoluteValue

/-!
# Admissible absolute values
This file defines a structure `AbsoluteValue.IsAdmissible` which we use to show the class number
of the ring of integers of a global field is finite.

## Main definitions

 * `AbsoluteValue.IsAdmissible abv` states the absolute value `abv : R → ℤ`
   respects the Euclidean domain structure on `R`, and that a large enough set
   of elements of `R^n` contains a pair of elements whose remainders are
   pointwise close together.

## Main results

 * `AbsoluteValue.absIsAdmissible` shows the "standard" absolute value on `ℤ`,
   mapping negative `x` to `-x`, is admissible.
 * `Polynomial.cardPowDegreeIsAdmissible` shows `cardPowDegree`,
   mapping `p : Polynomial 𝔽_q` to `q ^ degree p`, is admissible
-/

local infixl:50 " ≺ " => 
EuclideanDomain.r: {R : Type u} → [self : EuclideanDomain R] → R → R → Prop
EuclideanDomain.r

namespace AbsoluteValue

variable {
R: Type ?u.8588
R : 
Type _: Type (?u.20781+1)
Type _} [
EuclideanDomain: Type ?u.8812 → Type ?u.8812
EuclideanDomain 
R: Type ?u.8582
R]

variable (
abv: AbsoluteValue R ℤ
abv : 
AbsoluteValue: (R : Type ?u.8595) → (S : Type ?u.8594) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.8595?u.8594)
AbsoluteValue 
R: Type ?u.8588
R 
ℤ: Type
ℤ)

/-- An absolute value `R → ℤ` is admissible if it respects the Euclidean domain
structure and a large enough set of elements in `R^n` will contain a pair of
elements whose remainders are pointwise close together. -/
structure 
IsAdmissible: {R : Type u_1} → [inst : EuclideanDomain R] → AbsoluteValue R ℤ → Type
IsAdmissible extends 
IsEuclidean: {R : Type ?u.9033} →
  {S : Type ?u.9032} → [inst : EuclideanDomain R] → [inst_1 : OrderedSemiring S] → AbsoluteValue R S → Prop
IsEuclidean 
abv: AbsoluteValue R ℤ
abv where
  protected 
card: {R : Type u_1} → [inst : EuclideanDomain R] → {abv : AbsoluteValue R ℤ} → IsAdmissible abv → ℝ → ℕ
card : 
ℝ: Type
ℝ → 
ℕ: Type
ℕ
  /-- For all `ε > 0` and finite families `A`, we can partition the remainders of `A` mod `b`
  into `abv.card ε` sets, such that all elements in each part of remainders are close together. -/
  
exists_partition': ∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} (self : IsAdmissible abv) (n : ℕ) {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 → ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
exists_partition' :
    ∀ (
n: ℕ
n : 
ℕ: Type
ℕ) {
ε: ℝ
ε : 
ℝ: Type
ℝ} (
_: 0 < ε
_ : 
0: ?m.9117
0 < 
ε: ℝ
ε) {
b: R
b : 
R: Type ?u.8809
R} (
_: b ≠ 0
_ : 
b: R
b ≠ 
0: ?m.9172
0) (
A: Fin n → R
A : 
Fin: ℕ → Type
Fin 
n: ℕ
n → 
R: Type ?u.8809
R),
      ∃ 
t: Fin n → Fin (card ε)
t : 
Fin: ℕ → Type
Fin 
n: ℕ
n → 
Fin: ℕ → Type
Fin (
card: ℝ → ℕ
card 
ε: ℝ
ε), ∀ 
i₀: ?m.9396
i₀ 
i₁: ?m.9399
i₁, 
t: Fin n → Fin (card ε)
t 
i₀: ?m.9396
i₀ = 
t: Fin n → Fin (card ε)
t 
i₁: ?m.9399
i₁ → (
abv: AbsoluteValue R ℤ
abv (
A: Fin n → R
A 
i₁: ?m.9399
i₁ % 
b: R
b - 
A: Fin n → R
A 
i₀: ?m.9396
i₀ % 
b: R
b) : 
ℝ: Type
ℝ) < 
abv: AbsoluteValue R ℤ
abv 
b: R
b • 
ε: ℝ
ε
#align absolute_value.is_admissible 
AbsoluteValue.IsAdmissible: {R : Type u_1} → [inst : EuclideanDomain R] → AbsoluteValue R ℤ → Type
AbsoluteValue.IsAdmissible

-- Porting note: no docstrings for IsAdmissible
attribute [nolint 
docBlame: Std.Tactic.Lint.Linter
docBlame] 
IsAdmissible.card: {R : Type u_1} → [inst : EuclideanDomain R] → {abv : AbsoluteValue R ℤ} → IsAdmissible abv → ℝ → ℕ
IsAdmissible.card


namespace IsAdmissible

variable {
abv: ?m.21002
abv}

/-- For all `ε > 0` and finite families `A`, we can partition the remainders of `A` mod `b`
into `abv.card ε` sets, such that all elements in each part of remainders are close together. -/
theorem 
exists_partition: ∀ {ι : Type u_1} [inst : Fintype ι] {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : ι → R) (h : IsAdmissible abv),
          ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
exists_partition {
ι: Type ?u.21226
ι : 
Type _: Type (?u.21226+1)
Type _} [
Fintype: Type ?u.21229 → Type ?u.21229
Fintype 
ι: Type ?u.21226
ι] {
ε: ℝ
ε : 
ℝ: Type
ℝ} (
hε: 0 < ε
hε : 
0: ?m.21236
0 < 
ε: ℝ
ε) {
b: R
b : 
R: Type ?u.21005
R} (
hb: b ≠ 0
hb : 
b: R
b ≠ 
0: ?m.21291
0)
    (
A: ι → R
A : 
ι: Type ?u.21226
ι → 
R: Type ?u.21005
R) (
h: IsAdmissible abv
h : 
abv: AbsoluteValue R ℤ
abv.
IsAdmissible: {R : Type ?u.21511} → [inst : EuclideanDomain R] → AbsoluteValue R ℤ → Type
IsAdmissible) : ∃ 
t: ι → Fin (IsAdmissible.card h ε)
t : 
ι: Type ?u.21226
ι → 
Fin: ℕ → Type
Fin (
h: IsAdmissible abv
h.
card: {R : Type ?u.21534} → [inst : EuclideanDomain R] → {abv : AbsoluteValue R ℤ} → IsAdmissible abv → ℝ → ℕ
card 
ε: ℝ
ε),
      ∀ 
i₀: ?m.21544
i₀ 
i₁: ?m.21547
i₁, 
t: ι → Fin (IsAdmissible.card h ε)
t 
i₀: ?m.21544
i₀ = 
t: ι → Fin (IsAdmissible.card h ε)
t 
i₁: ?m.21547
i₁ → (
abv: AbsoluteValue R ℤ
abv (
A: ι → R
A 
i₁: ?m.21547
i₁ % 
b: R
b - 
A: ι → R
A 
i₀: ?m.21544
i₀ % 
b: R
b) : 
ℝ: Type
ℝ) < 
abv: AbsoluteValue R ℤ
abv 
b: R
b • 
ε: ℝ
ε := by
Goals accomplished! 🐙
  
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h: IsAdmissible abv

∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • εlet 
e: ?m.32299
e := 
Fintype.equivFin: (α : Type ?u.32300) → [inst : Fintype α] → α ≃ Fin (Fintype.card α)
Fintype.equivFin 
ι: Type u_1
ι
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h: IsAdmissible abv

e:= Fintype.equivFin ι: ι ≃ Fin (Fintype.card ι)

∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
  
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h: IsAdmissible abv

∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • εobtain 
⟨t, ht⟩: ∃ t, ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε
⟨
t: Fin (Fintype.card ι) → Fin (IsAdmissible.card h ε)
t
⟨t, ht⟩: ∃ t, ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε
, 
ht: ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε
ht
⟨t, ht⟩: ∃ t, ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε
⟩ := 
h: IsAdmissible abv
h.
exists_partition': ∀ {R : Type ?u.32312} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} (self : IsAdmissible abv) (n : ℕ) {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 → ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
exists_partition' (
Fintype.card: (α : Type ?u.32324) → [inst : Fintype α] → ℕ
Fintype.card 
ι: Type u_1
ι) 
hε: 0 < ε
hε 
hb: b ≠ 0
hb (
A: ι → R
A ∘ 
e: ?m.32299
e.
symm: {α : Sort ?u.32348} → {β : Sort ?u.32347} → α ≃ β → β ≃ α
symm)
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h: IsAdmissible abv

e:= Fintype.equivFin ι: ι ≃ Fin (Fintype.card ι)

t: Fin (Fintype.card ι) → Fin (IsAdmissible.card h ε)

ht: ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε

intro
∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
  
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h: IsAdmissible abv

∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • εrefine' ⟨
t: Fin (Fintype.card ι) → Fin (IsAdmissible.card h ε)
t ∘ 
e: ?m.32299
e, fun 
i₀: ?m.32668
i₀ 
i₁: ?m.32671
i₁ 
h: ?m.32674
h ↦ 
_: ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
_⟩
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h✝: IsAdmissible abv

e:= Fintype.equivFin ι: ι ≃ Fin (Fintype.card ι)

t: Fin (Fintype.card ι) → Fin (IsAdmissible.card h✝ ε)

ht: ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε

i₀, i₁: ι

h: (t ∘ ↑e) i₀ = (t ∘ ↑e) i₁

intro
↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
  
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h: IsAdmissible abv

∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • εconvert (config := {transparency := 
.default: Lean.Meta.TransparencyMode
.default})
    
ht: ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε
ht (
e: ?m.32299
e 
i₀: ?m.32668
i₀) (
e: ?m.32299
e 
i₁: ?m.32671
i₁) 
h: ?m.32674
h
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h✝: IsAdmissible abv

e:= Fintype.equivFin ι: ι ≃ Fin (Fintype.card ι)

t: Fin (Fintype.card ι) → Fin (IsAdmissible.card h✝ ε)

ht: ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε

i₀, i₁: ι

h: (t ∘ ↑e) i₀ = (t ∘ ↑e) i₁

h.e'_3.h.e'_3.h.e'_6.h.e'_5.h.e'_5.h.e'_1
i₁ = ↑e.symm (↑e i₁)
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h✝: IsAdmissible abv

e:= Fintype.equivFin ι: ι ≃ Fin (Fintype.card ι)

t: Fin (Fintype.card ι) → Fin (IsAdmissible.card h✝ ε)

ht: ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε

i₀, i₁: ι

h: (t ∘ ↑e) i₀ = (t ∘ ↑e) i₁

h.e'_3.h.e'_3.h.e'_6.h.e'_6.h.e'_5.h.e'_1
i₀ = ↑e.symm (↑e i₀) 
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h✝: IsAdmissible abv

e:= Fintype.equivFin ι: ι ≃ Fin (Fintype.card ι)

t: Fin (Fintype.card ι) → Fin (IsAdmissible.card h✝ ε)

ht: ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε

i₀, i₁: ι

h: (t ∘ ↑e) i₀ = (t ∘ ↑e) i₁

intro
↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε<;>
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h✝: IsAdmissible abv

e:= Fintype.equivFin ι: ι ≃ Fin (Fintype.card ι)

t: Fin (Fintype.card ι) → Fin (IsAdmissible.card h✝ ε)

ht: ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε

i₀, i₁: ι

h: (t ∘ ↑e) i₀ = (t ∘ ↑e) i₁

h.e'_3.h.e'_3.h.e'_6.h.e'_5.h.e'_5.h.e'_1
i₁ = ↑e.symm (↑e i₁)
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h✝: IsAdmissible abv

e:= Fintype.equivFin ι: ι ≃ Fin (Fintype.card ι)

t: Fin (Fintype.card ι) → Fin (IsAdmissible.card h✝ ε)

ht: ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε

i₀, i₁: ι

h: (t ∘ ↑e) i₀ = (t ∘ ↑e) i₁

h.e'_3.h.e'_3.h.e'_6.h.e'_6.h.e'_5.h.e'_1
i₀ = ↑e.symm (↑e i₀) 
R: Type u_2

inst✝¹: EuclideanDomain R

abv: AbsoluteValue R ℤ

ι: Type u_1

inst✝: Fintype ι

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: ι → R

h✝: IsAdmissible abv

e:= Fintype.equivFin ι: ι ≃ Fin (Fintype.card ι)

t: Fin (Fintype.card ι) → Fin (IsAdmissible.card h✝ ε)

ht: ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε

i₀, i₁: ι

h: (t ∘ ↑e) i₀ = (t ∘ ↑e) i₁

intro
↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • εsimp only [
e: ?m.32299
e.
symm_apply_apply: ∀ {α : Sort ?u.39275} {β : Sort ?u.39274} (e : α ≃ β) (x : α), ↑e.symm (↑e x) = x
symm_apply_apply]
Goals accomplished! 🐙
#align absolute_value.is_admissible.exists_partition 
AbsoluteValue.IsAdmissible.exists_partition: ∀ {R : Type u_2} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} {ι : Type u_1} [inst_1 : Fintype ι] {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : ι → R) (h : IsAdmissible abv),
          ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
AbsoluteValue.IsAdmissible.exists_partition

/-- Any large enough family of vectors in `R^n` has a pair of elements
whose remainders are close together, pointwise. -/
theorem 
exists_approx_aux: ∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} (n : ℕ) (h : IsAdmissible abv) {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
exists_approx_aux (
n: ℕ
n : 
ℕ: Type
ℕ) (
h: IsAdmissible abv
h : 
abv: AbsoluteValue R ℤ
abv.
IsAdmissible: {R : Type ?u.39720} → [inst : EuclideanDomain R] → AbsoluteValue R ℤ → Type
IsAdmissible) :
    ∀ {
ε: ℝ
ε : 
ℝ: Type
ℝ} (
_hε: 0 < ε
_hε : 
0: ?m.39747
0 < 
ε: ℝ
ε) {
b: R
b : 
R: Type ?u.39497
R} (
_hb: b ≠ 0
_hb : 
b: R
b ≠ 
0: ?m.39802
0) (
A: Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R
A : 
Fin: ℕ → Type
Fin (
h: IsAdmissible abv
h.
card: {R : Type ?u.40018} → [inst : EuclideanDomain R] → {abv : AbsoluteValue R ℤ} → IsAdmissible abv → ℝ → ℕ
card 
ε: ℝ
ε ^ 
n: ℕ
n).
succ: ℕ → ℕ
succ → 
Fin: ℕ → Type
Fin 
n: ℕ
n → 
R: Type ?u.39497
R),
      ∃ 
i₀: ?m.40073
i₀ 
i₁: ?m.40078
i₁, 
i₀: ?m.40073
i₀ ≠ 
i₁: ?m.40078
i₁ ∧ ∀ 
k: ?m.40084
k, (
abv: AbsoluteValue R ℤ
abv (
A: Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R
A 
i₁: ?m.40078
i₁ 
k: ?m.40084
k % 
b: R
b - 
A: Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R
A 
i₀: ?m.40073
i₀ 
k: ?m.40084
k % 
b: R
b) : 
ℝ: Type
ℝ) < 
abv: AbsoluteValue R ℤ
abv 
b: R
b • 
ε: ℝ
ε := by
Goals accomplished! 🐙
  
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • εhaveI := 
Classical.decEq: (α : Sort ?u.50823) → DecidableEq α
Classical.decEq 
R: Type u_1
R
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

this: DecidableEq R

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
  
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • εinduction' 
n: ℕ
n with 
n: ℕ
n 
ih: ?m.50843 n
ih
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

zero
∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin Nat.zero), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

succ
∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
  
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε·
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

zero
∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin Nat.zero), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε 
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

zero
∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin Nat.zero), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

succ
∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • εintro 
ε: ℝ
ε 
_hε: 0 < ε
_hε 
b: R
b 
_hb: b ≠ 0
_hb 
A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R
A
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

ε: ℝ

_hε: 0 < ε

b: R

_hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R

zero
∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin Nat.zero), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

zero
∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin Nat.zero), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • εrefine' ⟨
0: ?m.50889
0, 
1: ?m.50924
1, 
_: ?m.50939
_, 
_: ?m.50940
_⟩
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

ε: ℝ

_hε: 0 < ε

b: R

_hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R

zero.refine'_1
0 ≠ 1
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

ε: ℝ

_hε: 0 < ε

b: R

_hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R

zero.refine'_2
∀ (k : Fin Nat.zero), ↑(↑abv (A 1 k % b - A 0 k % b)) < ↑abv b • ε
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

zero
∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin Nat.zero), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε·
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

ε: ℝ

_hε: 0 < ε

b: R

_hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R

zero.refine'_1
0 ≠ 1 
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

ε: ℝ

_hε: 0 < ε

b: R

_hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R

zero.refine'_1
0 ≠ 1
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

ε: ℝ

_hε: 0 < ε

b: R

_hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R

zero.refine'_2
∀ (k : Fin Nat.zero), ↑(↑abv (A 1 k % b - A 0 k % b)) < ↑abv b • εsimp
Goals accomplished! 🐙
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

zero
∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin Nat.zero), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • εrintro 
⟨i, ⟨⟩⟩: Fin Nat.zero
⟨
i: ℕ
i
⟨i, ⟨⟩⟩: Fin Nat.zero
, 
⟨⟩: i < Nat.zero
⟨⟩
⟨i, ⟨⟩⟩: Fin Nat.zero
⟩
Goals accomplished! 🐙
  
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • εintro 
ε: ℝ
ε 
hε: 0 < ε
hε 
b: R
b 
hb: b ≠ 0
hb 
A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
A
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

succ
∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
  
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • εlet 
M: ?m.51893
M := 
h: IsAdmissible abv
h.
card: {R : Type ?u.51894} → [inst : EuclideanDomain R] → {abv : AbsoluteValue R ℤ} → IsAdmissible abv → ℝ → ℕ
card 
ε: ℝ
ε
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

succ
∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
  -- By the "nicer" pigeonhole principle, we can find a collection `s`
  -- of more than `M^n` remainders where the first components lie close together:
  
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
obtain: ∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
obtain 
⟨s, s_inj, hs⟩: ?m✝
⟨
s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s
⟨s, s_inj, hs⟩: ?m✝
, 
s_inj: Function.Injective s
s_inj
⟨s, s_inj, hs⟩: ?m✝
, 
hs: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
hs
⟨s, s_inj, hs⟩: ?m✝
⟩ :
    ∃ 
s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s : 
Fin: ℕ → Type
Fin (
M: ?m.51893
M ^ 
n: ℕ
n).
succ: ℕ → ℕ
succ → 
Fin: ℕ → Type
Fin (
M: ?m.51893
M ^ 
n: ℕ
n.
succ: ℕ → ℕ
succ).
succ: ℕ → ℕ
succ,
      
Function.Injective: {α : Sort ?u.51980} → {β : Sort ?u.51979} → (α → β) → Prop
Function.Injective 
s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s ∧ ∀ 
i₀: ?m.51987
i₀ 
i₁: ?m.51990
i₁, (
abv: AbsoluteValue R ℤ
abv (
A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
A (
s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s 
i₁: ?m.51990
i₁) 
0: ?m.57202
0 % 
b: R
b - 
A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
A (
s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s 
i₀: ?m.51987
i₀) 
0: ?m.57217
0 % 
b: R
b) : 
ℝ: Type
ℝ) < 
abv: AbsoluteValue R ℤ
abv 
b: R
b • 
ε: ℝ
ε := 
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

succ
∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • εby
Goals accomplished! 🐙
    -- We can partition the `A`s into `M` subsets where
    -- the first components lie close together:
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
obtain: ∃ t,
  ∀ (i₀ i₁ : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n))),
    t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
obtain 
⟨t, ht⟩: ?m✝
⟨
t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
t
⟨t, ht⟩: ?m✝
, 
ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
ht
⟨t, ht⟩: ?m✝
⟩ :
      ∃ 
t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
t : 
Fin: ℕ → Type
Fin (
M: ℕ
M ^ 
n: ℕ
n.
succ: ℕ → ℕ
succ).
succ: ℕ → ℕ
succ → 
Fin: ℕ → Type
Fin 
M: ℕ
M,
        ∀ 
i₀: ?m.63000
i₀ 
i₁: ?m.63003
i₁, 
t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
t 
i₀: ?m.63000
i₀ = 
t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
t 
i₁: ?m.63003
i₁ → (
abv: AbsoluteValue R ℤ
abv (
A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
A 
i₁: ?m.63003
i₁ 
0: ?m.68205
0 % 
b: R
b - 
A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
A 
i₀: ?m.63000
i₀ 
0: ?m.68211
0 % 
b: R
b) : 
ℝ: Type
ℝ) < 
abv: AbsoluteValue R ℤ
abv 
b: R
b • 
ε: ℝ
ε :=
      
h: IsAdmissible abv
h.
exists_partition: ∀ {R : Type ?u.73603} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} {ι : Type ?u.73602} [inst_1 : Fintype ι]
  {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : ι → R) (h : IsAdmissible abv),
          ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
exists_partition 
hε: 0 < ε
hε 
hb: b ≠ 0
hb fun 
x: ?m.73640
x ↦ 
A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
A 
x: ?m.73640
x 
0: ?m.73643
0
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

intro
∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
    -- Since the `M` subsets contain more than `M * M^n` elements total,
    -- there must be a subset that contains more than `M^n` elements.
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • εobtain 
⟨s, hs⟩: ∃ y, M ^ n < Finset.card (Finset.filter (fun x => t x = y) Finset.univ)
⟨
s: Fin M
s
⟨s, hs⟩: ∃ y, M ^ n < Finset.card (Finset.filter (fun x => t x = y) Finset.univ)
, 
hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
hs
⟨s, hs⟩: ∃ y, M ^ n < Finset.card (Finset.filter (fun x => t x = y) Finset.univ)
⟩ :=
      @
Fintype.exists_lt_card_fiber_of_mul_lt_card: ∀ {α : Type ?u.73719} {β : Type ?u.73718} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β)
  {n : ℕ}, Fintype.card β * n < Fintype.card α → ∃ y, n < Finset.card (Finset.filter (fun x => f x = y) Finset.univ)
Fintype.exists_lt_card_fiber_of_mul_lt_card 
_: Type ?u.73719
_ 
_: Type ?u.73718
_ _ _ _ 
t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
t (
M: ℕ
M ^ 
n: ℕ
n)
        (
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

intro
∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • εby
Goals accomplished! 🐙 
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

Fintype.card (Fin M) * M ^ n < Fintype.card (Fin (Nat.succ (M ^ Nat.succ n)))simpa only [
Fintype.card_fin: ∀ (n : ℕ), Fintype.card (Fin n) = n
Fintype.card_fin, 
pow_succ: ∀ {M : Type ?u.74169} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
pow_succ] using 
Nat.lt_succ_self: ∀ (n : ℕ), n < Nat.succ n
Nat.lt_succ_self (
M: ℕ
M ^ 
n: ℕ
n.
succ: ℕ → ℕ
succ)
Goals accomplished! 🐙)
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

intro.intro
∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • εrefine'
      ⟨fun 
i: ?m.73846
i ↦ (
Finset.univ: {α : Type ?u.73848} → [inst : Fintype α] → Finset α
Finset.univ.
filter: {α : Type ?u.73928} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter fun 
x: ?m.73936
x ↦ 
t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
t 
x: ?m.73936
x = 
s: Fin M
s).
toList: {α : Type ?u.73971} → Finset α → List α
toList.
nthLe: {α : Type ?u.73974} → (l : List α) → (n : ℕ) → n < List.length l → α
nthLe 
i: ?m.73846
i 
_: ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
_, 
_: ?m.74106
_, fun 
i₀: ?m.74112
i₀ 
i₁: ?m.74115
i₁ ↦ 
ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
ht 
_: Fin (Nat.succ (M ^ Nat.succ n))
_ 
_: Fin (Nat.succ (M ^ Nat.succ n))
_ 
_: t ?m.74117 = t ?m.74118
_⟩
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i: Fin (Nat.succ (M ^ n))

intro.intro.refine'_1
↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

intro.intro.refine'_2
Function.Injective fun i =>
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
    (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)))
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i₀, i₁: Fin (Nat.succ (M ^ n))

intro.intro.refine'_3
t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₀) =   t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₁)
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε·
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i: Fin (Nat.succ (M ^ n))

intro.intro.refine'_1
↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) 
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i: Fin (Nat.succ (M ^ n))

intro.intro.refine'_1
↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

intro.intro.refine'_2
Function.Injective fun i =>
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
    (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)))
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i₀, i₁: Fin (Nat.succ (M ^ n))

intro.intro.refine'_3
t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₀) =   t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₁)refine' 
i: ?m.73846
i.
2: ∀ {n : ℕ} (self : Fin n), ↑self < n
2.
trans_le: ∀ {α : Type ?u.74473} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c
trans_le 
_: ?m.74484 ≤ ?m.74485
_
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i: Fin (Nat.succ (M ^ n))

intro.intro.refine'_1
Nat.succ (M ^ n) ≤ List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
      
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i: Fin (Nat.succ (M ^ n))

intro.intro.refine'_1
↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))rwa [
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i: Fin (Nat.succ (M ^ n))

intro.intro.refine'_1
Nat.succ (M ^ n) ≤ List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
Finset.length_toList: ∀ {α : Type ?u.74533} (s : Finset α), List.length (Finset.toList s) = Finset.card s
Finset.length_toList
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i: Fin (Nat.succ (M ^ n))

intro.intro.refine'_1
Nat.succ (M ^ n) ≤ Finset.card (Finset.filter (fun x => t x = s) Finset.univ)]
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i: Fin (Nat.succ (M ^ n))

intro.intro.refine'_1
Nat.succ (M ^ n) ≤ Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε·
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

intro.intro.refine'_2
Function.Injective fun i =>
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
    (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))) 
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

intro.intro.refine'_2
Function.Injective fun i =>
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
    (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)))
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i₀, i₁: Fin (Nat.succ (M ^ n))

intro.intro.refine'_3
t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₀) =   t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₁)intro 
i: Fin (Nat.succ (M ^ n))
i 
j: Fin (Nat.succ (M ^ n))
j 
h: (fun i =>
      List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
        (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
    i =   (fun i =>
      List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
        (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
    j
h
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h✝: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h✝ ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i, j: Fin (Nat.succ (M ^ n))

h: (fun i =>
      List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
        (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
    i =   (fun i =>
      List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
        (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
    j

intro.intro.refine'_2
i = j
      
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

intro.intro.refine'_2
Function.Injective fun i =>
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
    (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)))ext
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h✝: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h✝ ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i, j: Fin (Nat.succ (M ^ n))

h: (fun i =>
      List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
        (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
    i =   (fun i =>
      List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
        (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
    j

intro.intro.refine'_2.h
↑i = ↑j
      
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

intro.intro.refine'_2
Function.Injective fun i =>
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
    (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)))exact 
Fin.mk.inj_iff: ∀ {n a b : ℕ} {ha : a < n} {hb : b < n}, { val := a, isLt := ha } = { val := b, isLt := hb } ↔ a = b
Fin.mk.inj_iff.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (
List.nodup_iff_injective_get: ∀ {α : Type ?u.74645} {l : List α}, List.Nodup l ↔ Function.Injective (List.get l)
List.nodup_iff_injective_get.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (
Finset.nodup_toList: ∀ {α : Type ?u.74650} (s : Finset α), List.Nodup (Finset.toList s)
Finset.nodup_toList 
_: Finset ?m.74651
_) 
h: (fun i =>
      List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
        (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
    i =   (fun i =>
      List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
        (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
    j
h)
Goals accomplished! 🐙
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • εhave : ∀ 
i: ?m.74683
i 
h: ?m.74686
h, (
Finset.univ: {α : Type ?u.74709} → [inst : Fintype α] → Finset α
Finset.univ.
filter: {α : Type ?u.74789} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter fun 
x: ?m.74797
x ↦ 
t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
t 
x: ?m.74797
x = 
s: Fin M
s).
toList: {α : Type ?u.74808} → Finset α → List α
toList.
nthLe: {α : Type ?u.74810} → (l : List α) → (n : ℕ) → n < List.length l → α
nthLe 
i: ?m.74683
i 
h: ?m.74686
h ∈
        
Finset.univ: {α : Type ?u.74817} → [inst : Fintype α] → Finset α
Finset.univ.
filter: {α : Type ?u.74897} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter fun 
x: ?m.74905
x ↦ 
t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
t 
x: ?m.74905
x = 
s: Fin M
s := 
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i₀, i₁: Fin (Nat.succ (M ^ n))

intro.intro.refine'_3
t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₀) =   t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₁)by
Goals accomplished! 🐙
      
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i₀, i₁: Fin (Nat.succ (M ^ n))

∀ (i : ℕ) (h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))),
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈     Finset.filter (fun x => t x = s) Finset.univintro 
i: ℕ
i 
h: i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
h
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h✝: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h✝ ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i₀, i₁: Fin (Nat.succ (M ^ n))

i: ℕ

h: i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))

List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈   Finset.filter (fun x => t x = s) Finset.univ
      
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i₀, i₁: Fin (Nat.succ (M ^ n))

∀ (i : ℕ) (h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))),
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈     Finset.filter (fun x => t x = s) Finset.univexact 
Finset.mem_toList: ∀ {α : Type ?u.74947} {a : α} {s : Finset α}, a ∈ Finset.toList s ↔ a ∈ s
Finset.mem_toList.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (
List.get_mem: ∀ {α : Type ?u.74959} (l : List α) (n : ℕ) (h : n < List.length l), List.get l { val := n, isLt := h } ∈ l
List.get_mem 
_: List ?m.74960
_ 
i: ℕ
i 
h: i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
h)
Goals accomplished! 🐙
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • εobtain 
⟨_, h₀⟩: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293 ∈ Finset.univ ∧   t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293) = s
⟨
_: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293 ∈ Finset.univ
_
⟨_, h₀⟩: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293 ∈ Finset.univ ∧   t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293) = s
, 
h₀: t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293) = s
h₀
⟨_, h₀⟩: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293 ∈ Finset.univ ∧   t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293) = s
⟩ := 
Finset.mem_filter: ∀ {α : Type ?u.74976} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : α},
  a ∈ Finset.filter p s ↔ a ∈ s ∧ p a
Finset.mem_filter.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (
this: ∀ (i : ℕ) (h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))),
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈     Finset.filter (fun x => t x = s) Finset.univ
this 
i₀: ?m.74112
i₀ 
_: ↑i₀ < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
_)
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this✝: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i₀, i₁: Fin (Nat.succ (M ^ n))

this: ∀ (i : ℕ) (h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))),
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈     Finset.filter (fun x => t x = s) Finset.univ

left✝: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293 ∈ Finset.univ

h₀: t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293) = s

intro.intro.refine'_3.intro
t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₀) =   t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₁)
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • εobtain 
⟨_, h₁⟩: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655 ∈ Finset.univ ∧   t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655) = s
⟨
_: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655 ∈ Finset.univ
_
⟨_, h₁⟩: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655 ∈ Finset.univ ∧   t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655) = s
, 
h₁: t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655) = s
h₁
⟨_, h₁⟩: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655 ∈ Finset.univ ∧   t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655) = s
⟩ := 
Finset.mem_filter: ∀ {α : Type ?u.75338} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : α},
  a ∈ Finset.filter p s ↔ a ∈ s ∧ p a
Finset.mem_filter.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (
this: ∀ (i : ℕ) (h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))),
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈     Finset.filter (fun x => t x = s) Finset.univ
this 
i₁: ?m.74115
i₁ 
_: ↑i₁ < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
_)
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this✝: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

t: Fin (Nat.succ (M ^ Nat.succ n)) → Fin M

ht: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε

s: Fin M

hs: M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)

i₀, i₁: Fin (Nat.succ (M ^ n))

this: ∀ (i : ℕ) (h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))),
  List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈     Finset.filter (fun x => t x = s) Finset.univ

left✝¹: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293 ∈ Finset.univ

h₀: t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293) = s

left✝: List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655 ∈ Finset.univ

h₁: t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655) = s

intro.intro.refine'_3.intro.intro
t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₀) =   t
    ((fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i₁)
    
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h ε: ℕ

∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • εexact 
h₀: t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.75293) = s
h₀.
trans: ∀ {α : Sort ?u.75692} {a b c : α}, a = b → b = c → a = c
trans 
h₁: t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.75655) = s
h₁.
symm: ∀ {α : Sort ?u.75708} {a b : α}, a = b → b = a
symm
Goals accomplished! 🐙
  -- Since `s` is large enough, there are two elements of `A ∘ s`
  -- where the second components lie close together.
  
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • εobtain 
⟨k₀, k₁, hk, h⟩: ∃ i₁, k₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s i₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε
⟨
k₀: Fin (Nat.succ (IsAdmissible.card h ε ^ n))
k₀
⟨k₀, k₁, hk, h⟩: ∃ i₁, k₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s i₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε
, 
k₁: Fin (Nat.succ (IsAdmissible.card h ε ^ n))
k₁
⟨k₀, k₁, hk, h⟩: ∃ i₁, k₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s i₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε
, 
hk: k₀ ≠ k₁
hk
⟨k₀, k₁, hk, h⟩: ∃ i₁, k₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s i₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε
, 
h: ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε
h
⟨k₀, k₁, hk, h⟩: ∃ i₁, k₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s i₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε
⟩ := 
ih: ?m.50843 n
ih 
hε: 0 < ε
hε 
hb: b ≠ 0
hb fun 
x: ?m.62801
x ↦ 
Fin.tail: {n : ℕ} → {α : Fin (n + 1) → Type ?u.62803} → ((i : Fin (n + 1)) → α i) → (i : Fin n) → α (Fin.succ i)
Fin.tail (
A: Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
A (
s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s 
x: ?m.62801
x))
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h✝: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h✝ ε: ℕ

s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))

s_inj: Function.Injective s

hs: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε

k₀, k₁: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))

hk: k₀ ≠ k₁

h: ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε

succ.intro.intro.intro.intro.intro
∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
  
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • εrefine' ⟨
s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s 
k₀: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))
k₀, 
s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s 
k₁: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))
k₁, fun 
h: ?m.62923
h ↦ 
hk: k₀ ≠ k₁
hk (
s_inj: Function.Injective s
s_inj 
h: ?m.62923
h), fun 
i: ?m.62929
i ↦ 
Fin.cases: ∀ {n : ℕ} {C : Fin (n + 1) → Sort ?u.62931}, C 0 → (∀ (i : Fin n), C (Fin.succ i)) → ∀ (i : Fin (n + 1)), C i
Fin.cases 
_: ↑(↑abv (A (s k₁) 0 % b - A (s k₀) 0 % b)) < ↑abv b • ε
_ (fun 
i: ?m.62960
i ↦ 
_: ↑(↑abv (A (s k₁) (Fin.succ i) % b - A (s k₀) (Fin.succ i) % b)) < ↑abv b • ε
_) 
i: ?m.62929
i⟩
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h✝: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h✝ ε: ℕ

s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))

s_inj: Function.Injective s

hs: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε

k₀, k₁: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))

hk: k₀ ≠ k₁

h: ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε

i: Fin (Nat.succ n)

succ.intro.intro.intro.intro.intro.refine'_1
↑(↑abv (A (s k₁) 0 % b - A (s k₀) 0 % b)) < ↑abv b • ε
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h✝: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h✝ ε: ℕ

s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))

s_inj: Function.Injective s

hs: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε

k₀, k₁: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))

hk: k₀ ≠ k₁

h: ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε

i✝: Fin (Nat.succ n)

i: Fin n

succ.intro.intro.intro.intro.intro.refine'_2
↑(↑abv (A (s k₁) (Fin.succ i) % b - A (s k₀) (Fin.succ i) % b)) < ↑abv b • ε
  
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε·
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h✝: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h✝ ε: ℕ

s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))

s_inj: Function.Injective s

hs: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε

k₀, k₁: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))

hk: k₀ ≠ k₁

h: ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε

i: Fin (Nat.succ n)

succ.intro.intro.intro.intro.intro.refine'_1
↑(↑abv (A (s k₁) 0 % b - A (s k₀) 0 % b)) < ↑abv b • ε 
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h✝: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h✝ ε: ℕ

s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))

s_inj: Function.Injective s

hs: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε

k₀, k₁: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))

hk: k₀ ≠ k₁

h: ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε

i: Fin (Nat.succ n)

succ.intro.intro.intro.intro.intro.refine'_1
↑(↑abv (A (s k₁) 0 % b - A (s k₀) 0 % b)) < ↑abv b • ε
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

h✝: IsAdmissible abv

this: DecidableEq R

n: ℕ

ih: ∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε

ε: ℝ

hε: 0 < ε

b: R

hb: b ≠ 0

A: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R

M:= IsAdmissible.card h✝ ε: ℕ

s: Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))

s_inj: Function.Injective s

hs: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε

k₀, k₁: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))

hk: k₀ ≠ k₁

h: ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε

i✝: Fin (Nat.succ n)

i: Fin n

succ.intro.intro.intro.intro.intro.refine'_2
↑(↑abv (A (s k₁) (Fin.succ i) % b - A (s k₀) (Fin.succ i) % b)) < ↑abv b • εexact 
hs: ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
hs 
k₀: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))
k₀ 
k₁: Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))
k₁
Goals accomplished! 🐙
  
R: Type u_1

inst✝: EuclideanDomain R

abv: AbsoluteValue R ℤ

n: ℕ

h: IsAdmissible abv

∀ {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε·
R: Type u_1

inst✝: