-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this_1 : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (h.card ε ^ n).succ → Fin n → R),
    ∃ (i₀ : Fin (h.card ε ^ n).succ) (i₁ : Fin (h.card ε ^ n).succ),
      i₀ ≠ i₁ ∧
        ∀ (k : Fin n),
          (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht :
  ∀ (i₀ i₁ : Fin (M ^ n.succ).succ),
    t i₀ = t i₁ →
      (↑((abv : (a : R) → ℤ) (A i₁ 0 % b - A i₀ 0 % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
s : Fin M
hs : M ^ n < Finset.card (α := Fin (M ^ n.succ).succ) {x : Fin (M ^ n.succ).succ | t x = s}
this : (M ^ n).succ ≤ List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s})
refine_1 :
  ∀ (i j : Fin (M ^ n).succ)
    (h :
      Eq (α := Fin (M ^ n.succ).succ)
        ((fun (i : Fin (M ^ n).succ) ↦
            getElem (valid :=
              fun (xs : List (Fin (M ^ n.succ).succ))
                (i :
                  Fin
                    (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
              (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) ⋯)
          i)
        ((fun (i : Fin (M ^ n).succ) ↦
            getElem (valid :=
              fun (xs : List (Fin (M ^ n.succ).succ))
                (i :
                  Fin
                    (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
              (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) ⋯)
          j)),
    i = j
refine_2 :
  ∀ (i₀ i₁ : Fin (M ^ n).succ),
    t
        ((fun (i : Fin (M ^ n).succ) ↦
            getElem (valid :=
              fun (xs : List (Fin (M ^ n.succ).succ))
                (i :
                  Fin
                    (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
              (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) ⋯)
          i₀) =
      t
        ((fun (i : Fin (M ^ n).succ) ↦
            getElem (valid :=
              fun (xs : List (Fin (M ^ n.succ).succ))
                (i :
                  Fin
                    (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
              (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) ⋯)
          i₁)
⊢ ∃ (s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ),
    Function.Injective s ∧
      ∀ (i₀ i₁ : Fin (M ^ n).succ),
        (↑((abv : (a : R) → ℤ) (A (s i₁) 0 % b - A (s i₀) 0 % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε

Tactic:
refine ⟨fun i ↦ (Finset.toList {x | t x = s})[i.castLE this], fun i j h ↦ ?_,
      fun i₀ i₁ ↦ ht _ _ ?_⟩