awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
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)
⊢ ∃ (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₁)

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
⊢ Ne (α := { k : ι // k = i ∨ k = j }) (Subtype.mk (p := fun (k : ι) ↦ k = i ∨ k = j) j ⋯)
    (Subtype.mk (p := fun (k : ι) ↦ k = i ∨ k = j) i ⋯)

Tactic:
grind
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
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 ⋯) :
                (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)
⊢ ∃ (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))
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)

Tactic:
⟨c, hc.1, fun k hk ↦ ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
refine_2 : ∀ (k : ι) (hk : k ≠ i), LT.lt.{u_2} (α := S) ((v k : (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:
refine ⟨c, hc.1, fun k hk ↦ ?_⟩
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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 ι
a b c : R
k : ι
hk 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 ⋯) :
            (a : R) → S)
          a :
        S) ∧
    ∀ (j : { k_1 : ι // k_1 ≠ k }),
      j ≠ Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i ⋯ →
        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 ⋯) :
            (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 ⋯ →
        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 ⋯) :
            (a : R) → S)
          c :
        S) ∧
    (∀ (j : { k_1 : ι // k_1 ≠ k }),
        j ≠ Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i ⋯ →
          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:
hc.2.2

Premises used: And.right
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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 ι
a b c : R
k : ι
hk 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 ⋯) :
            (a : R) → S)
          a :
        S) ∧
    ∀ (j : { k_1 : ι // k_1 ≠ k }),
      j ≠ Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i ⋯ →
        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 ⋯) :
            (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 ⋯ →
        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 ⋯) :
            (a : R) → S)
          c :
        S) ∧
    (∀ (j : { k_1 : ι // k_1 ≠ k }),
        j ≠ Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i ⋯ →
          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:
exact hc.2.2

Premises used: And.right
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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_2 : ∀ (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
h : k ≠ j
⊢ Ne (α := { k : ι // k ≠ j }) (Subtype.mk (p := fun (k : ι) ↦ k ≠ j) k h) (Subtype.mk (p := fun (k : ι) ↦ k ≠ j) i ⋯)

Tactic:
grind