-- Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean
theorem exists_approx {ι : Type*} [Fintype ι] {ε : ℝ} (hε : 0 < ε) {b : R} (hb : b ≠ 0)
    (h : abv.IsAdmissible) (A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R) :
    ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ k, (abv (A i₁ k % b - A i₀ k % b) : ℝ) < abv b • ε

Proof state:
case intro.intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : abv.IsAdmissible
A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
refine ⟨i₀, i₁, ne, fun k ↦ ?_⟩

Result:
case intro.intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : abv.IsAdmissible
A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε
k : ι
⊢ ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Proof state:
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h : abv.IsAdmissible
A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
obtain ⟨i₀, i₁, ne, h⟩ := h.exists_approx_aux (Fintype.card ι) hε hb fun x y ↦ A x (e.symm y)

Result:
case intro.intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : abv.IsAdmissible
A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Proof state:
case intro.intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : abv.IsAdmissible
A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε
k : ι
⊢ ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
convert h (e k) <;> simp only [e.symm_apply_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h : abv.IsAdmissible
A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
let e := Fintype.equivFin ι

Result:
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h : abv.IsAdmissible
A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε