-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
inst_6 : OrderTopology S
ι_1 : Type u_3
inst_7 : Finite ι_1
v_1 : ι_1 → AbsoluteValue R S
this : Fintype ι_1
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun (ι : Type u_3) [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun (i j : ι) ↦ ¬(v i).IsEquiv (v j)) →
          ∀ (i : ι),
            ∃ (a : R),
              LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) a : S) ∧
                ∀ (j : ι), j ≠ i → LT.lt.{u_2} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
ι : Type u_3
x : Fintype ι
h_1 : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun (i j : ι) ↦ ¬(v i).IsEquiv (v j)
i : ι
hc_1 : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  LT.lt.{u_2} (α := S) (1 : S)
      ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k ≠ j) v
              (Subtype.mk (p := fun (k : ι) ↦ k ≠ j) i ⋯) :
            (a : R) → S)
          a :
        S) ∧
    ∀ (j_1 : { k : ι // k ≠ j }),
      j_1 ≠ Subtype.mk (p := fun (k : ι) ↦ k ≠ j) i ⋯ →
        LT.lt.{u_2} (α := S)
          ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k ≠ j) v j_1 : (a : R) → S) a : S) (1 : S)
b : R
hb :
  LT.lt.{u_2} (α := S) (1 : S)
      ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k = i ∨ k = j) v
              (Subtype.mk (p := fun (k : ι) ↦ k = i ∨ k = j) i ⋯) :
            (a : R) → S)
          b :
        S) ∧
    ∀ (j_1 : { k : ι // k = i ∨ k = j }),
      j_1 ≠ Subtype.mk (p := fun (k : ι) ↦ k = i ∨ k = j) i ⋯ →
        LT.lt.{u_2} (α := S)
          ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k = i ∨ k = j) v j_1 : (a : R) → S) b : S)
          (1 : S)
ha₁ : Eq.{u_2 + 1} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
c : R
hc :
  LT.lt.{u_2} (α := S) (1 : S)
      ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k ≠ j) v
              (Subtype.mk (p := fun (k : ι) ↦ k ≠ j) i ⋯) :
            (a : R) → S)
          c :
        S) ∧
    (∀ (j_1 : { k : ι // k ≠ j }),
        j_1 ≠ Subtype.mk (p := fun (k : ι) ↦ k ≠ j) i ⋯ →
          LT.lt.{u_2} (α := S)
            ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k ≠ j) v j_1 : (a : R) → S) c : S)
            (1 : S)) ∧
      LT.lt.{u_2} (α := S) ((v j : (a : R) → S) c : S) (1 : S)
k : ι
hk : k ≠ i
⊢ LT.lt.{u_2} (α := S) ((v k : (a : R) → S) c : S) (1 : S)
have refine_2 : ∀ (hj : k ≠ i)
  (ha :
    LT.lt.{u_2} (α := S) (1 : S)
        ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 ≠ k) v
                (Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i sorry) :
              (a : R) → S)
            a :
          S) ∧
      ∀ (j : { k_1 : ι // k_1 ≠ k }),
        j ≠ Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i sorry →
          LT.lt.{u_2} (α := S)
            ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 ≠ k) v j : (a : R) → S) a : S)
            (1 : S))
  (hb :
    LT.lt.{u_2} (α := S) (1 : S)
        ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 = i ∨ k_1 = k) v
                (Subtype.mk (p := fun (k_1 : ι) ↦ k_1 = i ∨ k_1 = k) i sorry) :
              (a : R) → S)
            b :
          S) ∧
      ∀ (j : { k_1 : ι // k_1 = i ∨ k_1 = k }),
        j ≠ Subtype.mk (p := fun (k_1 : ι) ↦ k_1 = i ∨ k_1 = k) i sorry →
          LT.lt.{u_2} (α := S)
            ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 = i ∨ k_1 = k) v j : (a : R) → S) b :
              S)
            (1 : S))
  (ha₁ : Eq.{u_2 + 1} (α := S) ((v k : (a : R) → S) a : S) (1 : S))
  (hc :
    LT.lt.{u_2} (α := S) (1 : S)
        ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 ≠ k) v
                (Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i sorry) :
              (a : R) → S)
            c :
          S) ∧
      (∀ (j : { k_1 : ι // k_1 ≠ k }),
          j ≠ Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i sorry →
            LT.lt.{u_2} (α := S)
              ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 ≠ k) v j : (a : R) → S) c : S)
              (1 : S)) ∧
        LT.lt.{u_2} (α := S) ((v k : (a : R) → S) c : S) (1 : S)),
  LT.lt.{u_2} (α := S) ((v k : (a : R) → S) c : S) (1 : S)
Tactic: rcases eq_or_ne k j with (rfl | h)
Cleared hypotheses: j, hj, ha, hb, ha₁, hc