-- Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
theorem le_multiplicity_of_δ_of_fin {n : ℕ} (f : Fin n → E) (h : ∀ i, ‖f i‖ ≤ 2)
    (h' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖) : n ≤ multiplicity E

Proof state:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
⊢ n ≤ multiplicity E

Tactic:
let s := Finset.image f Finset.univ

Result:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ n ≤ multiplicity E

Proof state:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
hs : ∀ c ∈ s, ‖c‖ ≤ 2
⊢ n ≤ multiplicity E

Tactic:
have h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - goodδ E ≤ ‖c - d‖ := by
  simp only [s, forall_apply_eq_imp_iff, forall_exists_index, Finset.mem_univ, Finset.mem_image,
    Ne, 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' this

Result:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - goodδ E ≤ ‖c - d‖
⊢ n ≤ multiplicity E

Proof state:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ s.card = n

Tactic:
rw [Finset.card_image_of_injective _ finj]

Result:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ Finset.univ.card = n

Proof state:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
hs : ∀ c ∈ s, ‖c‖ ≤ 2
i j : Fin n
hij : ¬f i = f j
this : i ≠ j
⊢ 1 - goodδ E ≤ ‖f i - f j‖

Tactic:
exact h' this

Result:
no goals

Proof state:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
hs : ∀ c ∈ s, ‖c‖ ≤ 2
⊢ ∀ (a a_1 : Fin n), ¬f a = f a_1 → 1 - goodδ E ≤ ‖f a - f a_1‖

Tactic:
intro i j hij

Result:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
hs : ∀ c ∈ s, ‖c‖ ≤ 2
i j : Fin n
hij : ¬f i = f j
⊢ 1 - goodδ E ≤ ‖f i - f j‖

Proof state:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
⊢ n ≤ multiplicity E

Tactic:
have finj : Function.Injective f := by
  intro i j hij
  by_contra h
  have : 1 - goodδ E ≤ ‖f i - f j‖ := h' h
  simp only [hij, norm_zero, sub_self] at this
  linarith [goodδ_lt_one E]

Result:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
⊢ n ≤ multiplicity E

Proof state:
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' : Pairwise fun 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

Tactic:
simp only [hij, norm_zero, sub_self] at this

Result:
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' : Pairwise fun 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

Proof state:
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' : Pairwise fun 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

Tactic:
linarith [goodδ_lt_one E]

Result:
no goals

Proof state:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ n ≤ multiplicity E

Tactic:
have s_card : s.card = n := by rw [Finset.card_image_of_injective _ finj]; exact Finset.card_fin n

Result:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
⊢ n ≤ multiplicity E

Proof state:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
⊢ i = j

Tactic:
by_contra h

Result:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
⊢ False

Proof state:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
⊢ ∀ c ∈ s, ‖c‖ ≤ 2

Tactic:
simp only [s, h, forall_apply_eq_imp_iff, forall_const, forall_exists_index, Finset.mem_univ,
  Finset.mem_image, imp_true_iff, true_and]

Result:
no goals

Proof state:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
⊢ Function.Injective f

Tactic:
intro i j hij

Result:
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' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
⊢ i = j