no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
⊢ n ≤ multiplicity E
classical
have finj : Function.Injective f := by
  intro i j hij
  by_contra h
  have : 1 - goodδ E ≤ ‖f i - f j‖ := h' i j h
  simp only [hij, norm_zero, sub_self] at this
  linarith [goodδ_lt_one E]
let s := Finset.image f Finset.univ
have s_card : s.card = n := by rw [Finset.card_image_of_injective _ finj]; exact Finset.card_fin n
have hs : ∀ c ∈ s, ‖c‖ ≤ 2 := by
  simp only [h, forall_apply_eq_imp_iff', forall_const, forall_exists_index, Finset.mem_univ,
    Finset.mem_image, imp_true_iff, true_and]
have h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - goodδ E ≤ ‖c - d‖ := by
  simp only [forall_apply_eq_imp_iff', forall_exists_index, Finset.mem_univ, Finset.mem_image,
    Ne.def, exists_true_left, forall_apply_eq_imp_iff', forall_true_left, true_and]
  intro i j hij
  have : i ≠ j := fun h => by rw [h] at hij ; exact hij rfl
  exact h' i j this
have : s.card ≤ multiplicity E := card_le_multiplicity_of_δ hs h's
rwa [s_card] at this
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
⊢ n ≤ multiplicity E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
⊢ n ≤ multiplicity E
have finj : Function.Injective f := by
  intro i j hij
  by_contra h
  have : 1 - goodδ E ≤ ‖f i - f j‖ := h' i j h
  simp only [hij, norm_zero, sub_self] at this
  linarith [goodδ_lt_one E]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ n ≤ multiplicity E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
⊢ n ≤ multiplicity E
let s := Finset.image f Finset.univ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
⊢ n ≤ multiplicity E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ n ≤ multiplicity E
have s_card : s.card = n := by rw [Finset.card_image_of_injective _ finj]; exact Finset.card_fin n
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
⊢ n ≤ multiplicity E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
⊢ n ≤ multiplicity E
have hs : ∀ c ∈ s, ‖c‖ ≤ 2 := by
  simp only [h, forall_apply_eq_imp_iff', forall_const, forall_exists_index, Finset.mem_univ,
    Finset.mem_image, imp_true_iff, true_and]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 - goodδ E ≤ ‖c - d‖
⊢ n ≤ multiplicity E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
⊢ n ≤ multiplicity E
have h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - goodδ E ≤ ‖c - d‖ := by
  simp only [forall_apply_eq_imp_iff', forall_exists_index, Finset.mem_univ, Finset.mem_image,
    Ne.def, exists_true_left, forall_apply_eq_imp_iff', forall_true_left, true_and]
  intro i j hij
  have : i ≠ j := fun h => by rw [h] at hij ; exact hij rfl
  exact h' i j this
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 - goodδ E ≤ ‖c - d‖
this : Finset.card s ≤ multiplicity E
⊢ n ≤ multiplicity E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 - goodδ E ≤ ‖c - d‖
⊢ n ≤ multiplicity E
have : s.card ≤ multiplicity E := card_le_multiplicity_of_δ hs h's
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 - goodδ E ≤ ‖c - d‖
this : Finset.card s ≤ multiplicity E
⊢ n ≤ multiplicity E
rwa [s_card] at this
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
⊢ i = j
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
⊢ Function.Injective f
intro i j hij
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
⊢ False
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
⊢ i = j
by_contra h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
this : 1 - goodδ E ≤ ‖f i - f j‖
⊢ False
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
⊢ False
have : 1 - goodδ E ≤ ‖f i - f j‖ := h' i j h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
this : 1 - goodδ E ≤ 0
⊢ False
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
this : 1 - goodδ E ≤ ‖f i - f j‖
⊢ False
simp only [hij, norm_zero, sub_self] at this
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
this : 1 - goodδ E ≤ 0
⊢ False
linarith [goodδ_lt_one E]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ Finset.card Finset.univ = n
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ Finset.card s = n
rw [Finset.card_image_of_injective _ finj]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ Finset.card Finset.univ = n
exact Finset.card_fin n
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
⊢ ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
simp only [h, forall_apply_eq_imp_iff', forall_const, forall_exists_index, Finset.mem_univ,
  Finset.mem_image, imp_true_iff, true_and]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
⊢ ∀ (a a_1 : Fin n), ¬f a = f a_1 → 1 - goodδ E ≤ ‖f a - f a_1‖
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
⊢ ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 - goodδ E ≤ ‖c - d‖
simp only [forall_apply_eq_imp_iff', forall_exists_index, Finset.mem_univ, Finset.mem_image,
  Ne.def, exists_true_left, forall_apply_eq_imp_iff', forall_true_left, true_and]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
i j : Fin n
hij : ¬f i = f j
⊢ 1 - goodδ E ≤ ‖f i - f j‖
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
⊢ ∀ (a a_1 : Fin n), ¬f a = f a_1 → 1 - goodδ E ≤ ‖f a - f a_1‖
intro i j hij
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
i j : Fin n
hij : ¬f i = f j
this : i ≠ j
⊢ 1 - goodδ E ≤ ‖f i - f j‖
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
i j : Fin n
hij : ¬f i = f j
⊢ 1 - goodδ E ≤ ‖f i - f j‖
have : i ≠ j := fun h => by rw [h] at hij ; exact hij rfl
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
i j : Fin n
hij : ¬f i = f j
this : i ≠ j
⊢ 1 - goodδ E ≤ ‖f i - f j‖
exact h' i j this
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
i j : Fin n
hij : ¬f j = f j
h : i = j
⊢ False
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
i j : Fin n
hij : ¬f i = f j
h : i = j
⊢ False
rw [h] at hij
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : ∀ (i j : Fin n), i ≠ j → 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : Finset.card s = n
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
i j : Fin n
hij : ¬f j = f j
h : i = j
⊢ False
exact hij rfl