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
ι : 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)
choose :
  ∀ (rN : ℕ) (hrN : ∀ b ≥ rN, LT.lt.{u_2} (α := S) ((w : (a : R) → S) (c b) : 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)
⊢ ∃ (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)

Tactic:
choose rN hrN using Filter.eventually_atTop.1 <| Filter.Tendsto.eventually_lt_const hbw hcₙ

Premises used: Filter.Tendsto.eventually_lt_const, Iff.mp, Filter.eventually_atTop
-- 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
ι : 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)
have :
  ∀ (this : Fintype ι),
    ∃ (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)
⊢ ∃ (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)

Tactic:
have := Fintype.ofFinite ι
-- 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
ι : 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
⊢ ∃ (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)

Tactic:
⟨c r, hr₁ r ?_, fun j hj ↦ ?_, ?_⟩

Premises used: 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
ι : 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)
refine_3 : LT.lt.{u_2} (α := S) ((w : (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)

Tactic:
refine ⟨c r, hr₁ r ?_, fun j hj ↦ ?_, ?_⟩
-- 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
ι : 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
⊢ r ≥ r₁

Tactic:
le_max_iff.2 <| .inl <|
      Finset.le_sup_dite_pos (p := fun j ↦ j = i) (f := fun _ _ ↦ r₁) (Finset.mem_univ _) rfl

Premises used: Iff.mpr, Finset.mem_univ, Finset.le_sup_dite_pos, Or.inl, le_max_iff, Eq, rfl
-- 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
ι : 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
⊢ r ≥ r₁

Tactic:
exact le_max_iff.2 <| .inl <|
      Finset.le_sup_dite_pos (p := fun j ↦ j = i) (f := fun _ _ ↦ r₁) (Finset.mem_univ _) rfl

Premises used: Iff.mpr, Finset.mem_univ, Finset.le_sup_dite_pos, le_max_iff, Eq, rfl
-- 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
ι : 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
j : ι
hj : j ≠ i
⊢ LT.lt.{u_2} (α := S) ((v j : (a : R) → S) (c r) : S) (1 : S)

Tactic:
hrₙ j hj _ <| le_max_iff.2 <| .inl <|
      Finset.le_sup_dite_neg (fun j ↦ j = i) (Finset.mem_univ j) _

Premises used: Iff.mpr, Finset.mem_univ, Set.Mem, setOf, Finset.le_sup_dite_neg, Or.inl, le_max_iff, Set.Iio, Eq
-- 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
ι : 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
j : ι
hj : j ≠ i
⊢ LT.lt.{u_2} (α := S) ((v j : (a : R) → S) (c r) : S) (1 : S)

Tactic:
exact hrₙ j hj _ <| le_max_iff.2 <| .inl <|
      Finset.le_sup_dite_neg (fun j ↦ j = i) (Finset.mem_univ j) _

Premises used: Iff.mpr, Finset.mem_univ, Finset.le_sup_dite_neg, le_max_iff, Eq
-- 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
ι : 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
⊢ LT.lt.{u_2} (α := S) ((w : (a : R) → S) (c r) : S) (1 : S)

Tactic:
hrN _ <| le_max_iff.2 (.inr le_rfl)

Premises used: Iff.mpr, le_rfl, le_max_iff, Or.inr
-- 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
ι : 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
⊢ LT.lt.{u_2} (α := S) ((w : (a : R) → S) (c r) : S) (1 : S)

Tactic:
exact hrN _ <| le_max_iff.2 (.inr le_rfl)

Premises used: Iff.mpr, le_rfl, le_max_iff, Or.inr
-- 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
ι : 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)
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)
⊢ ∀ (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 ι
-- 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
ι : 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)
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)
revert :
  ∀ (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)
⊢ ∀ (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:
revert hv h
-- 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
ι : 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)

Tactic:
induction_subsingleton_or_nontrivial (P := P) ι (fun ι _ _ v h hv i ↦ ?_)
    (fun ι _ _ ih v h hv i ↦ ?_) v

Premises used: Fintype.induction_subsingleton_or_nontrivial