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
ι : Type u_3
inst_7 : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) a : S)
haj : ∀ (j : ι), j ≠ i → LT.lt.{u_2} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
haw : LT.lt.{u_2} (α := S) (1 : S) ((w : (a : R) → S) a : S)
hb : LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) b : S)
hbw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) b : S) (1 : S)
c : ℕ → R := fun (n : ℕ) ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ :
  Tendsto.{0, u_2} (β := S) (fun (n : ℕ) ↦ ((v i : (a : R) → S) (c n) : S)) atTop (𝓝 ((v i : (a : R) → S) b) : Filter S)
hcₙ : Tendsto.{0, u_2} (β := S) (fun (n : ℕ) ↦ ((w : (a : R) → S) (c n) : S)) atTop (𝓝 ((w : (a : R) → S) b) : Filter S)
hcⱼ :
  ∀ (j : ι) (hj : j ≠ i) (s : Set S),
    Membership.mem (γ := Set (Set S)) {s : Set S | ∃ (a : S), s = Set.Ioi a ∨ s = Set.Iio a} s →
      0 ∈ s → ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := S) s ((v j : (a : R) → S) (c b) : S)
r₁ : ℕ
hr₁ : ∀ b ≥ r₁, LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) (c b) : S)
rₙ : (j : ι) → (hj : j ≠ i) → ℕ
hrₙ :
  ∀ (j : ι) (hj : j ≠ i),
    ∀ b ≥ rₙ j hj, Membership.mem.{u_2, u_2} (α := S) (γ := Set S) (Set.Iio 1) ((v j : (a : R) → S) (c b) : S)
rN : ℕ
hrN : ∀ b ≥ rN, LT.lt.{u_2} (α := S) ((w : (a : R) → S) (c b) : S) (1 : S)
this : Fintype ι
r : ℕ := max (Finset.sup Finset.univ fun (j : ι) ↦ if h : j = i then r₁ else rₙ j h) rN
refine_1 : r ≥ r₁
⊢ ∃ (k : R),
    LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) k : S) ∧
      (∀ (j : ι), j ≠ i → LT.lt.{u_2} (α := S) ((v j : (a : R) → S) k : S) (1 : S)) ∧
        LT.lt.{u_2} (α := S) ((w : (a : R) → S) k : S) (1 : S)
have refine_2 : ∀ (j : ι) (hj : j ≠ i), LT.lt.{u_2} (α := S) ((v j : (a : R) → S) (c r) : S) (1 : S)
Tactic: refine ⟨c r, hr₁ r ?_, fun j hj ↦ ?_, ?_⟩
-- 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
ι : Type u_3
inst_7 : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) a : S)
haj : ∀ (j : ι), j ≠ i → LT.lt.{u_2} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
haw : LT.lt.{u_2} (α := S) (1 : S) ((w : (a : R) → S) a : S)
hb : LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) b : S)
hbw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) b : S) (1 : S)
c : ℕ → R := fun (n : ℕ) ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ :
  Tendsto.{0, u_2} (β := S) (fun (n : ℕ) ↦ ((v i : (a : R) → S) (c n) : S)) atTop (𝓝 ((v i : (a : R) → S) b) : Filter S)
hcₙ : Tendsto.{0, u_2} (β := S) (fun (n : ℕ) ↦ ((w : (a : R) → S) (c n) : S)) atTop (𝓝 ((w : (a : R) → S) b) : Filter S)
hcⱼ :
  ∀ (j : ι) (hj : j ≠ i) (s : Set S),
    Membership.mem (γ := Set (Set S)) {s : Set S | ∃ (a : S), s = Set.Ioi a ∨ s = Set.Iio a} s →
      0 ∈ s → ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := S) s ((v j : (a : R) → S) (c b) : S)
r₁ : ℕ
hr₁ : ∀ b ≥ r₁, LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) (c b) : S)
rₙ : (j : ι) → (hj : j ≠ i) → ℕ
hrₙ :
  ∀ (j : ι) (hj : j ≠ i),
    ∀ b ≥ rₙ j hj, Membership.mem.{u_2, u_2} (α := S) (γ := Set S) (Set.Iio 1) ((v j : (a : R) → S) (c b) : S)
rN : ℕ
hrN : ∀ b ≥ rN, LT.lt.{u_2} (α := S) ((w : (a : R) → S) (c b) : S) (1 : S)
this : Fintype ι
r : ℕ := max (Finset.sup Finset.univ fun (j : ι) ↦ if h : j = i then r₁ else rₙ j h) rN
refine_1 : r ≥ r₁
refine_2 : ∀ (j : ι) (hj : j ≠ i), LT.lt.{u_2} (α := S) ((v j : (a : R) → S) (c r) : S) (1 : S)
⊢ ∃ (k : R),
    LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) k : S) ∧
      (∀ (j : ι), j ≠ i → LT.lt.{u_2} (α := S) ((v j : (a : R) → S) k : S) (1 : S)) ∧
        LT.lt.{u_2} (α := S) ((w : (a : R) → S) k : S) (1 : S)
have refine_3 : LT.lt.{u_2} (α := S) ((w : (a : R) → S) (c r) : S) (1 : S)
Tactic: refine ⟨c r, hr₁ r ?_, fun j hj ↦ ?_, ?_⟩
-- 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
ι : Type u_3
inst_7 : Finite ι
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : 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)
have have : ∀ (this : Fintype ι) (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)
Tactic: have := Fintype.ofFinite ι
-- 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
ι : Type u_3
inst_7 : Finite ι
v : ι → AbsoluteValue R S
this : Fintype ι
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)
⊢ ∀ (h : ∀ (i : ι), (v i).IsNontrivial) (hv : 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)
have refine_1 : ∀ (ι : Type u_3) (x : Fintype ι),
  Subsingleton ι →
    ∀ (v : ι → AbsoluteValue R S) (h : ∀ (i : ι), (v i).IsNontrivial)
      (hv : 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)
Tactic: refine induction_subsingleton_or_nontrivial (P := P) ι (fun ι _ _ v h hv i ↦ ?_)
    (fun ι _ _ ih v h hv i ↦ ?_) v
-- 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
ι : Type u_3
inst_7 : Finite ι
v : ι → AbsoluteValue R S
this : Fintype ι
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)
refine_1 :
  ∀ (ι : Type u_3) (x : Fintype ι),
    Subsingleton ι →
      ∀ (v : ι → AbsoluteValue R S) (h : ∀ (i : ι), (v i).IsNontrivial)
        (hv : 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)
⊢ ∀ (h : ∀ (i : ι), (v i).IsNontrivial) (hv : 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)
have refine_2 : ∀ (ι : Type u_3) (x : Fintype ι),
  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 : ι),
      ∃ (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 induction_subsingleton_or_nontrivial (P := P) ι (fun ι _ _ v h hv i ↦ ?_)
    (fun ι _ _ ih v h hv i ↦ ?_) v
-- 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 : Subsingleton ι
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : 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)
have refine_1 : ∀ (a : R) (ha : LT.lt.{u_2} (α := S) (1 : S) ((v i : (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: let ⟨a, ha⟩ := (h i).exists_abv_gt_one
-- 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 : ι
⊢ ∃ (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 : ∀ (hc : card ι = 2),
  ∃ (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 (card ι) 2 with (hc | hc)
-- 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 : ι
refine_2 :
  ∀ (hc : card ι = 2),
    ∃ (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₁ : ∀ (hc : card ι ≠ 2),
  ∃ (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 (card ι) 2 with (hc | hc)
-- 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
⊢ ∃ (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 : ∀ (j : ι) (hj : (fun (y : ι) ↦ y ≠ i) j ∧ ∀ (y : ι), (fun (y : ι) ↦ y ≠ i) y → y = j),
  ∃ (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 ⟨j, hj⟩ := (Nat.card_eq_two_iff' i).1 <| card_eq_nat_card ▸ hc
-- 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
j : ι
hj : (fun (y : ι) ↦ y ≠ i) j ∧ ∀ (y : ι), (fun (y : ι) ↦ y ≠ i) y → y = j
⊢ ∃ (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 : ∀ (a : R)
  (ha :
    LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) a : S) ∧
      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 ⟨a, ha⟩ := (v i).exists_one_lt_lt_one_of_not_isEquiv (h i) (h j) (hv hj.1.symm)
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (hypothesis)
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
⊢ ∃ (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 hlt : 2 < card ι
Tactic: have hlt : 2 < card ι := Nat.lt_of_le_of_ne (one_lt_card_iff_nontrivial.2 ‹_›) hc.symm
-- 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 ι
⊢ ∃ (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 : ∀ (j : ι) (hj : 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)
Tactic: let ⟨j, hj⟩ := exists_ne i
-- 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),
    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 : ∀ (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 sorry) :
              (a : R) → S)
            a :
          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) 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 ⟨a, ha⟩ := ih {k : ι // k ≠ j} (card_subtype_lt fun a ↦ a rfl) (restrict _ v)
      (fun i ↦ h _) (hv.comp_of_injective val_injective) ⟨i, hj.symm⟩
-- 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)
⊢ card.{u_3} { k : ι // k = i ∨ k = j } < card ι
have linarith : card ι ≤ card.{u_3} { k : ι // k = i ∨ k = j } →
  -1 + (HAdd.hAdd (α := ℤ) 2 1 - (↑(card ι) : ℤ)) +
        HSub.hSub (α := ℤ) (↑(card ι) : ℤ) (↑(card.{u_3} { k : ι // k = i ∨ k = j }) : ℤ) +
      HSub.hSub (α := ℤ) (↑(card.{u_3} { c : ι // c = i ∨ c = j }) : ℤ) 2 =
    0
Tactic: linarith [card_subtype_eq_or_eq_of_ne hj.symm]