awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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)
⊢ ∃ (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)
have refine_2 : ∀ (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 sorry) :
              (a : R) → S)
            b :
          S) ∧
      ∀ (j_1 : { k : ι // k = i ∨ k = j }),
        j_1 ≠ Subtype.mk (p := fun (k : ι) ↦ k = i ∨ k = j) i sorry →
          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)),
  ∃ (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)
Tactic: let ⟨b, hb⟩ := ih {k : ι // k = i ∨ k = j} (by linarith [card_subtype_eq_or_eq_of_ne hj.symm])
      (restrict _ v) (fun _ ↦ h _) (hv.comp_of_injective val_injective) ⟨i, .inl rfl⟩
-- 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 : 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)
⊢ ∃ (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)
have refine_2 : ∀ (ha₁ : Eq.{u_2 + 1} (α := S) ((v j : (a : R) → S) a : S) (1 : S)),
  ∃ (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)
Tactic: rcases eq_or_ne (v j a) 1 with (ha₁ | ha₁)
-- 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 : 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)
refine_2 :
  ∀ (ha₁ : Eq.{u_2 + 1} (α := S) ((v j : (a : R) → S) a : S) (1 : S)),
    ∃ (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)
⊢ ∃ (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)
have refine_2₁ : ∀ (ha₁ : Ne.{u_2 + 1} (α := S) ((v j : (a : R) → S) a : S) (1 : S)),
  ∃ (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)
Tactic: rcases eq_or_ne (v j a) 1 with (ha₁ | ha₁)
-- 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 : 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)
⊢ ∃ (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)
have refine_2 : ∀ (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 sorry) :
              (a : R) → S)
            c :
          S) ∧
      (∀ (j_1 : { k : ι // k ≠ j }),
          j_1 ≠ Subtype.mk (p := fun (k : ι) ↦ k ≠ j) i sorry →
            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)),
  ∃ (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)
Tactic: let ⟨c, hc⟩ := exists_one_lt_lt_one_pi_of_eq_one ha.1 ha.2 ha₁ hb.1 (hb.2 ⟨j, .inr rfl⟩
        (by grind))
-- 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)
⊢ ∃ (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)
have refine_2 : ∀ (k : ι) (hk : k ≠ i), LT.lt.{u_2} (α := S) ((v k : (a : R) → S) c : S) (1 : S)
Tactic: refine ⟨c, hc.1, fun k hk ↦ ?_⟩
-- 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 : 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₁ : Ne.{u_2 + 1} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
⊢ ∃ (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)
have refine_2 : ∀ (ha_lt : LT.lt.{u_2} (α := S) ((v j : (a : R) → S) a : S) (1 : S)),
  ∃ (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)
Tactic: rcases ha₁.lt_or_gt with (ha_lt | ha_gt)
-- 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 : 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₁ : Ne.{u_2 + 1} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
refine_2 :
  ∀ (ha_lt : LT.lt.{u_2} (α := S) ((v j : (a : R) → S) a : S) (1 : S)),
    ∃ (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)
⊢ ∃ (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)
have refine_2₁ : ∀ (ha_gt : LT.lt.{u_2} (α := S) (1 : S) ((v j : (a : R) → S) a : S)),
  ∃ (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)
Tactic: rcases ha₁.lt_or_gt with (ha_lt | ha_gt)
-- 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 : 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₁ : Ne.{u_2 + 1} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
ha_lt : LT.lt.{u_2} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
⊢ ∃ (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)
have refine_2 : ∀ (k : ι) (hk : k ≠ i), LT.lt.{u_2} (α := S) ((v k : (a : R) → S) a : S) (1 : S)
Tactic: refine ⟨a, ha.1, fun k hk ↦ ?_⟩