Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2019 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes
! This file was ported from Lean 3 source module data.pi.lex
! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.Basic
import Mathlib.Order.WellFounded
import Mathlib.Algebra.Group.Pi
import Mathlib.Algebra.Order.Group.Defs
import Mathlib.Mathport.Notation
/-!
# Lexicographic order on Pi types
This file defines the lexicographic order for Pi types. `a` is less than `b` if `a i = b i` for all
`i` up to some point `k`, and `a k < b k`.
## Notation
* `Πₗ i, α i`: Pi type equipped with the lexicographic order. Type synonym of `Π i, α i`.
## See also
Related files are:
* `Data.Finset.Colex`: Colexicographic order on finite sets.
* `Data.List.Lex`: Lexicographic order on lists.
* `Data.Oigma.Order`: Lexicographic order on `Σₗ i, α i`.
* `Data.PSigma.Order`: Lexicographic order on `Σₗ' i, α i`.
* `Data.Prod.Lex`: Lexicographic order on `α × β`.
-/
variable { ι : Type _ } { β : ι → Type _ : Type (?u.11934+1)} ( r : ι → ι → Prop ) ( s : {i : ι } → β i β i Prop s : ∀ { i }, β i → β i → Prop )
namespace Pi
instance { α : Type _ } : ∀ [ Inhabited : Sort ?u.54 → Sort (max1?u.54) α ], Inhabited : Sort ?u.57 → Sort (max1?u.57) ( Lex α ) :=
@ fun x => x
/-- The lexicographic relation on `Π i : ι, β i`, where `ι` is ordered by `r`,
and each `β i` is ordered by `s`. -/
protected def Lex : ((i : ι ) → β i ) → ((i : ι ) → β i ) → Prop Lex ( x y : ∀ i , β i ) : Prop :=
∃ i , (∀ j , r j i → x j = y j ) ∧ s : {i : ι } → β i β i Prop s ( x i ) ( y i )
#align pi.lex Pi.Lex : {ι : Type u_1} →
{β : ι → Type u_2(ι → ι → Prop ({i : ι } → β i β i Prop ) → ((i : ι ) → β i ) → ((i : ι ) → β i ) → Prop
/- This unfortunately results in a type that isn't delta-reduced, so we keep the notation out of the
basic API, just in case -/
/-- The notation `Πₗ i, α i` refers to a pi type equipped with the lexicographic order. -/
notation3 "Πₗ "(...)", " r :( scoped p => Lex (∀ i, p i)) => r
@[ simp ]
theorem toLex_apply : ∀ (x : (i : ι ) → β i ) (i : ι ), ↑toLex x i = x i toLex_apply ( x : ∀ i , β i ) ( i : ι ) : toLex x i = x i :=
rfl : ∀ {α : Sort ?u.3560} {a : α }, a = a
#align pi.to_lex_apply Pi.toLex_apply : ∀ {ι : Type u_2} {β : ι → Type u_1x : (i : ι ) → β i ) (i : ι ), ↑toLex x i = x i
@[ simp ]
theorem ofLex_apply : ∀ {ι : Type u_1} {β : ι → Type u_2x : Lex ((i : ι ) → β i )i : ι ), ↑ofLex x i = x i ofLex_apply ( x : Lex (∀ i , β i )) ( i : ι ) : ofLex x i = x i :=
rfl : ∀ {α : Sort ?u.3716} {a : α }, a = a
#align pi.of_lex_apply Pi.ofLex_apply : ∀ {ι : Type u_1} {β : ι → Type u_2x : Lex ((i : ι ) → β i )i : ι ), ↑ofLex x i = x i
theorem lex_lt_of_lt_of_preorder : ∀ [inst : (i : ι ) → Preorder (β i ] {r : ι → ι → Prop WellFounded r ∀ {x y : (i : ι ) → β i }, x < y ∃ i , (∀ (j : ι ), r j i x j ≤ y j ∧ y j ≤ x j ) ∧ x i < y i lex_lt_of_lt_of_preorder [∀ i , Preorder ( β i )] { r } ( hwf : WellFounded r ) { x y : ∀ i , β i }
( hlt : x < y ) : ∃ i , (∀ j , r j i → x j ≤ y j ∧ y j ≤ x j ) ∧ x i < y i :=
let h' := Pi.lt_def : ∀ {ι : Type ?u.3912} {α : ι → Type ?u.3911inst : (i : ι ) → Preorder (α i ] {x y : (i : ι ) → α i },
x < y ↔ x ≤ y ∧ ∃ i , x i < y i . 1 : ∀ {a b : Prop }, (a ↔ b a → b hlt
let ⟨ i , hi : i ∈ fun x_1 => Preorder.toLT .1x x_1 y x_1 hi , hl : ∀ (x_1 : ι ), (x_1 ∈ fun x_2 => Preorder.toLT .1x x_2 y x_2 ¬ r x_1 i hl ⟩ := hwf . has_min _ h' . 2 : ∀ {a b : Prop }, a ∧ b b
⟨ i , fun j hj => ⟨ h' . 1 : ∀ {a b : Prop }, a ∧ b a j , not_not . 1 : ∀ {a b : Prop }, (a ↔ b a → b fun h => hl : ∀ (x_1 : ι ), (x_1 ∈ fun x_2 => Preorder.toLT .1x x_2 y x_2 ¬ r x_1 i hl j ( lt_of_le_not_le : ∀ {α : Type ?u.4108} [inst : Preorder α a b : α }, a ≤ b ¬ b ≤ a a < b ( h' . 1 : ∀ {a b : Prop }, a ∧ b a j ) h ) hj ⟩, hi : i ∈ fun x_1 => Preorder.toLT .1x x_1 y x_1 hi ⟩
#align pi.lex_lt_of_lt_of_preorder Pi.lex_lt_of_lt_of_preorder : ∀ {ι : Type u_2} {β : ι → Type u_1inst : (i : ι ) → Preorder (β i ] {r : ι → ι → Prop WellFounded r ∀ {x y : (i : ι ) → β i }, x < y ∃ i , (∀ (j : ι ), r j i x j ≤ y j ∧ y j ≤ x j ) ∧ x i < y i
theorem lex_lt_of_lt [∀ i , PartialOrder : Type ?u.4380 → Type ?u.4380 ( β i )] { r } ( hwf : WellFounded r ) { x y : ∀ i , β i }
( hlt : x < y ) : Pi.Lex : {ι : Type ?u.4478} →
{β : ι → Type ?u.4477(ι → ι → Prop ({i : ι } → β i β i Prop ) → ((i : ι ) → β i ) → ((i : ι ) → β i ) → Prop r (@ fun i => (· < ·) : β i β i Prop ) x y := by
Pi.Lex r (fun i x x_1 => x < x_1 ) x y simp_rw [ Pi.Lex r (fun i x x_1 => x < x_1 ) x y Pi.Lex : {ι : Type ?u.4678} →
{β : ι → Type ?u.4677(ι → ι → Prop ({i : ι } → β i β i Prop ) → ((i : ι ) → β i ) → ((i : ι ) → β i ) → Prop , ∃ i , (∀ (j : ι ), r j i x j = y j ) ∧ x i < y i Pi.Lex r (fun i x x_1 => x < x_1 ) x y le_antisymm_iff ∃ i , (∀ (j : ι ), r j i x j ≤ y j ∧ y j ≤ x j ) ∧ x i < y i ] ∃ i , (∀ (j : ι ), r j i x j ≤ y j ∧ y j ≤ x j ) ∧ x i < y i
Pi.Lex r (fun i x x_1 => x < x_1 ) x y exact lex_lt_of_lt_of_preorder : ∀ {ι : Type ?u.5005} {β : ι → Type ?u.5004inst : (i : ι ) → Preorder (β i ] {r : ι → ι → Prop WellFounded r ∀ {x y : (i : ι ) → β i }, x < y ∃ i , (∀ (j : ι ), r j i x j ≤ y j ∧ y j ≤ x j ) ∧ x i < y i hwf hlt
#align pi.lex_lt_of_lt Pi.lex_lt_of_lt
theorem isTrichotomous_lex [∀ i , IsTrichotomous ( β i ) s : {i : ι } → β i β i Prop s ] ( wf : WellFounded r ) :
IsTrichotomous (∀ i , β i ) ( Pi.Lex : {ι : Type ?u.5207} →
{β : ι → Type ?u.5206(ι → ι → Prop ({i : ι } → β i β i Prop ) → ((i : ι ) → β i ) → ((i : ι ) → β i ) → Prop r @ s : {i : ι } → β i β i Prop s ) :=
{ trichotomous := fun a b => by
cases' eq_or_ne : ∀ {α : Sort ?u.5274} (x y : α ), x = y ∨ x ≠ y a b with hab hab
· exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inl : ∀ {a b : Prop }, a → a ∨ b hab )
· rw [ Function.ne_iff : ∀ {α : Sort ?u.5355} {β : α → Sort ?u.5354f₁ f₂ : (a : α ) → β a }, f₁ ≠ f₂ ↔ ∃ a , f₁ a ≠ f₂ a ] at hab
let i := wf . min _ hab : ∃ a_1 , a a_1 ≠ b a_1 hab
have hri : ∀ (j : ι ), r j i a j = b j hri : ∀ j , r j i → a j = b j := by
∀ (j : ι ), r j i a j = b j intro j
∀ (j : ι ), r j i a j = b j rw [ ← not_imp_not : ∀ {a b : Prop }, ¬ a ¬ b ↔ b → a ]
∀ (j : ι ), r j i a j = b j exact fun h' => wf . not_lt_min _ _ h'
have hne : a i ≠ b i := wf . min_mem _ hab : ∃ a_1 , a a_1 ≠ b a_1 hab
cases' trichotomous_of s : {i : ι } → β i β i Prop s ( a i ) ( b i ) with hi hi
exacts [ Or.inl : ∀ {a b : Prop }, a → a ∨ b ⟨ i , hri : ∀ (j : ι ), r j i a j = b j hri , hi ⟩,
Or.inr : ∀ {a b : Prop }, b → a ∨ b <| Or.inr : ∀ {a b : Prop }, b → a ∨ b <| ⟨ i , fun j hj => ( hri : ∀ (j : ι ), r j i a j = b j hri j hj ). symm : ∀ {α : Sort ?u.5654} {a b : α }, a = b b = a symm , hi . resolve_left : ∀ {a b : Prop }, a ∨ b ¬ a b hne ⟩] }
#align pi.is_trichotomous_lex Pi.isTrichotomous_lex
instance : {ι : Type u_1} → {β : ι → Type u_2[inst : LT ι [inst : (a : ι ) → LT (β a ] → LT (Lex ((i : ι ) → β i ) instance [ LT ι ] [∀ a , LT ( β a )] : LT ( Lex (∀ i , β i )) :=
⟨ Pi.Lex : {ι : Type ?u.5786} →
{β : ι → Type ?u.5785(ι → ι → Prop ({i : ι } → β i β i Prop ) → ((i : ι ) → β i ) → ((i : ι ) → β i ) → Prop (· < ·) @ fun _ => (· < ·) : β x✝ β x✝ Prop ⟩
instance Lex.isStrictOrder [ LinearOrder : Type ?u.5968 → Type ?u.5968 ι ] [∀ a , PartialOrder : Type ?u.5975 → Type ?u.5975 ( β a )] :
IsStrictOrder ( Lex (∀ i , β i )) (· < ·) : Lex ((i : ι ) → β i )Lex ((i : ι ) → β i )Prop where
irrefl := fun a ⟨ k , _, hk₂ : (fun x x_1 x_2 => x_1 < x_2 ) k (a k a k hk₂ ⟩ => lt_irrefl ( a k ) hk₂ : (fun x x_1 x_2 => x_1 < x_2 ) k (a k a k hk₂
trans := by
∀ (a b c : Lex ((i : ι ) → β i )a < b b < c a < c rintro a b c ⟨N₁, lt_N₁, a_lt_b⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) N₁ (a N₁ b N₁ N₁ ⟨N₁, lt_N₁, a_lt_b⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) N₁ (a N₁ b N₁ lt_N₁ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j lt_N₁ ⟨N₁, lt_N₁, a_lt_b⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) N₁ (a N₁ b N₁ a_lt_b ⟨N₁, lt_N₁, a_lt_b⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) N₁ (a N₁ b N₁ ⟨N₂, lt_N₂, b_lt_c⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) N₂ (b N₂ c N₂ N₂ ⟨N₂, lt_N₂, b_lt_c⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) N₂ (b N₂ c N₂ lt_N₂ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j lt_N₂ ⟨N₂, lt_N₂, b_lt_c⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) N₂ (b N₂ c N₂ b_lt_c ⟨N₂, lt_N₂, b_lt_c⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) N₂ (b N₂ c N₂ ι : Type ?u.5944β : ι → Type ?u.5949r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝¹ : LinearOrder ι inst✝ : (a : ι ) → PartialOrder (β a a, b, c : Lex ((i : ι ) → β i )N₁ : ι lt_N₁ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j a_lt_b : a N₁ < b N₁ N₂ : ι lt_N₂ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j b_lt_c : b N₂ < c N₂ intro.intro.intro.intro
∀ (a b c : Lex ((i : ι ) → β i )a < b b < c a < c rcases lt_trichotomy N₁ N₂ with (H | rfl | H) : N₁ < N₂ ∨ N₁ = N₂ ∨ N₂ < N₁ H H | rfl | H : N₁ < N₂ ∨ N₁ = N₂ ∨ N₂ < N₁ rfl H | rfl | H : N₁ < N₂ ∨ N₁ = N₂ ∨ N₂ < N₁ H (H | rfl | H) : N₁ < N₂ ∨ N₁ = N₂ ∨ N₂ < N₁ ι : Type ?u.5944β : ι → Type ?u.5949r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝¹ : LinearOrder ι inst✝ : (a : ι ) → PartialOrder (β a a, b, c : Lex ((i : ι ) → β i )N₁ : ι lt_N₁ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j a_lt_b : a N₁ < b N₁ N₂ : ι lt_N₂ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j b_lt_c : b N₂ < c N₂ H : N₁ < N₂ intro.intro.intro.intro.inl ι : Type ?u.5944β : ι → Type ?u.5949r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝¹ : LinearOrder ι inst✝ : (a : ι ) → PartialOrder (β a a, b, c : Lex ((i : ι ) → β i )N₁ : ι lt_N₁ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j a_lt_b : a N₁ < b N₁ lt_N₂ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → b j = c j b_lt_c : b N₁ < c N₁ intro.intro.intro.intro.inr.inl ι : Type ?u.5944β : ι → Type ?u.5949r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝¹ : LinearOrder ι inst✝ : (a : ι ) → PartialOrder (β a a, b, c : Lex ((i : ι ) → β i )N₁ : ι lt_N₁ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j a_lt_b : a N₁ < b N₁ N₂ : ι lt_N₂ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j b_lt_c : b N₂ < c N₂ H : N₂ < N₁ intro.intro.intro.intro.inr.inr
∀ (a b c : Lex ((i : ι ) → β i )a < b b < c a < c exacts [⟨ N₁ , fun j hj => ( lt_N₁ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j lt_N₁ _ hj ). trans : ∀ {α : Sort ?u.7116} {a b c : α }, a = b b = c a = c trans ( lt_N₂ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j lt_N₂ _ <| hj . trans : ∀ {α : Type ?u.7136} [inst : Preorder α a b c : α }, a < b b < c a < c H ), lt_N₂ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j lt_N₂ _ H ▸ a_lt_b ⟩,
⟨ N₁ , fun j hj => ( lt_N₁ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j lt_N₁ _ hj ). trans : ∀ {α : Sort ?u.7400} {a b c : α }, a = b b = c a = c trans ( lt_N₂ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → b j = c j lt_N₂ _ hj ), a_lt_b . trans : ∀ {α : Type ?u.7418} [inst : Preorder α a b c : α }, a < b b < c a < c b_lt_c ⟩,
⟨ N₂ , fun j hj => ( lt_N₁ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j lt_N₁ _ ( hj . trans : ∀ {α : Type ?u.7500} [inst : Preorder α a b c : α }, a < b b < c a < c H )). trans : ∀ {α : Sort ?u.7513} {a b c : α }, a = b b = c a = c trans ( lt_N₂ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₂ → b j = c j lt_N₂ _ hj ), ( lt_N₁ : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j N₁ → a j = b j lt_N₁ _ H ). symm : ∀ {α : Sort ?u.7532} {a b : α }, a = b b = a symm ▸ b_lt_c ⟩]
#align pi.lex.is_strict_order Pi.Lex.isStrictOrder
instance [ LinearOrder : Type ?u.7711 → Type ?u.7711 ι ] [∀ a , PartialOrder : Type ?u.7718 → Type ?u.7718 ( β a )] : PartialOrder : Type ?u.7722 → Type ?u.7722 ( Lex (∀ i , β i )) :=
partialOrderOfSO (· < ·) : Lex ((i : ι ) → β i )Lex ((i : ι ) → β i )Prop
/-- `Πₗ i, α i` is a linear order if the original order is well-founded. -/
noncomputable instance [ LinearOrder : Type ?u.8198 → Type ?u.8198 ι ] [ IsWellOrder ι (· < ·) ] [∀ a , LinearOrder : Type ?u.8402 → Type ?u.8402 ( β a )] :
LinearOrder : Type ?u.8406 → Type ?u.8406 ( Lex (∀ i , β i )) :=
@ linearOrderOfSTO (Πₗ i , β i ) (· < ·) : Lex ((i : ι ) → (fun i => β i ) i )Lex ((i : ι ) → (fun i => β i ) i )Prop
{ trichotomous := ( isTrichotomous_lex _ : ?m.9131 → ?m.9131 → Prop _ : {i : ?m.9131 } → ?m.9132 i ?m.9132 i Prop IsWellFounded.wf ). 1 } ( Classical.decRel _ : ?m.9868 → ?m.9868 → Prop )
section PartialOrder
variable [ LinearOrder : Type ?u.13680 → Type ?u.13680 ι ] [ IsWellOrder ι (· < ·) ] [∀ i , PartialOrder : Type ?u.16039 → Type ?u.16039 ( β i )] { x y : ∀ i , β i } { i : ι }
{ a : β i }
open Function
theorem toLex_monotone : Monotone (@ toLex (∀ i , β i )) := fun a b h =>
or_iff_not_imp_left : ∀ {a b : Prop }, a ∨ b ↔ ¬ a b . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun hne =>
let ⟨ i , hi : i ∈ { i | a i ≠ b i hi , hl : ∀ (x : ι ), x ∈ { i | a i ≠ b i ¬ x < i hl ⟩ := IsWellFounded.wf . has_min (r := (· < · ) ) { i | a i ≠ b i }
( Function.ne_iff : ∀ {α : Sort ?u.10839} {β : α → Sort ?u.10838f₁ f₂ : (a : α ) → β a }, f₁ ≠ f₂ ↔ ∃ a , f₁ a ≠ f₂ a . 1 : ∀ {a b : Prop }, (a ↔ b a → b hne )
⟨ i , fun j hj => by
ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i✝ : ι a✝ : β i✝ a, b : (i : ι ) → β i h : a ≤ b hne : ¬ ↑toLex a = ↑toLex b i : ι hi : i ∈ { i | a i ≠ b i hl : ∀ (x : ι ), x ∈ { i | a i ≠ b i ¬ x < i j : ι hj : (fun x x_1 => x < x_1 ) j i contrapose! hl : ↑toLex a j ≠ ↑toLex b j hl ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i✝ : ι a✝ : β i✝ a, b : (i : ι ) → β i h : a ≤ b hne : ¬ ↑toLex a = ↑toLex b i : ι hi : i ∈ { i | a i ≠ b i j : ι hj : (fun x x_1 => x < x_1 ) j i hl : ↑toLex a j ≠ ↑toLex b j ∃ x , x ∈ { i | a i ≠ b i ∧ x < i
ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i✝ : ι a✝ : β i✝ a, b : (i : ι ) → β i h : a ≤ b hne : ¬ ↑toLex a = ↑toLex b i : ι hi : i ∈ { i | a i ≠ b i hl : ∀ (x : ι ), x ∈ { i | a i ≠ b i ¬ x < i j : ι hj : (fun x x_1 => x < x_1 ) j i exact ⟨ j , hl : ↑toLex a j ≠ ↑toLex b j hl , hj : (fun x x_1 => x < x_1 ) j i hj ⟩ , ( h i ). lt_of_ne hi : i ∈ { i | a i ≠ b i hi ⟩
#align pi.to_lex_monotone Pi.toLex_monotone
theorem toLex_strictMono : StrictMono (@ toLex (∀ i , β i )) := fun a b h =>
let ⟨ i , hi : i ∈ { i | a i ≠ b i hi , hl : ∀ (x : ι ), x ∈ { i | a i ≠ b i ¬ x < i hl ⟩ := IsWellFounded.wf . has_min (r := (· < · ) ) { i | a i ≠ b i }
( Function.ne_iff : ∀ {α : Sort ?u.12552} {β : α → Sort ?u.12551f₁ f₂ : (a : α ) → β a }, f₁ ≠ f₂ ↔ ∃ a , f₁ a ≠ f₂ a . 1 : ∀ {a b : Prop }, (a ↔ b a → b h . ne : ∀ {α : Type ?u.12575} [inst : Preorder α a b : α }, a < b a ≠ b )
⟨ i , fun j hj => by
ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i✝ : ι a✝ : β i✝ a, b : (i : ι ) → β i h : a < b i : ι hi : i ∈ { i | a i ≠ b i hl : ∀ (x : ι ), x ∈ { i | a i ≠ b i ¬ x < i j : ι hj : (fun x x_1 => x < x_1 ) j i contrapose! hl : ↑toLex a j ≠ ↑toLex b j hl ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i✝ : ι a✝ : β i✝ a, b : (i : ι ) → β i h : a < b i : ι hi : i ∈ { i | a i ≠ b i j : ι hj : (fun x x_1 => x < x_1 ) j i hl : ↑toLex a j ≠ ↑toLex b j ∃ x , x ∈ { i | a i ≠ b i ∧ x < i
ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i✝ : ι a✝ : β i✝ a, b : (i : ι ) → β i h : a < b i : ι hi : i ∈ { i | a i ≠ b i hl : ∀ (x : ι ), x ∈ { i | a i ≠ b i ¬ x < i j : ι hj : (fun x x_1 => x < x_1 ) j i exact ⟨ j , hl : ↑toLex a j ≠ ↑toLex b j hl , hj : (fun x x_1 => x < x_1 ) j i hj ⟩ , ( h . le : ∀ {α : Type ?u.12793} [inst : Preorder α a b : α }, a < b a ≤ b i ). lt_of_ne hi : i ∈ { i | a i ≠ b i hi ⟩
#align pi.to_lex_strict_mono Pi.toLex_strictMono
@[ simp ]
theorem lt_toLex_update_self_iff : toLex x < toLex ( update : {α : Sort ?u.14065} →
{β : α → Sort ?u.14064[inst : DecidableEq α ((a : α ) → β a ) → (a' : α ) → β a' (a : α ) → β a x i a ) ↔ x i < a := by
refine' ⟨ _ , fun h => toLex_strictMono <| lt_update_self_iff : ∀ {ι : Type ?u.14630} {π : ι → Type ?u.14631inst : DecidableEq ι inst_1 : (i : ι ) → Preorder (π i ]
{x : (i : ι ) → π i } {i : ι } {a : π i x < update x i a ↔ x i < a . 2 : ∀ {a b : Prop }, (a ↔ b b → a h ⟩ ↑toLex x < ↑toLex (update x i a x i < a
rintro ⟨j, hj, h⟩ : (∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a j_1 ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) j (↑toLex x j ) (↑toLex (update x i a j ) j ⟨j, hj, h⟩ : (∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a j_1 ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) j (↑toLex x j ) (↑toLex (update x i a j ) hj : ∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a j_1 hj ⟨j, hj, h⟩ : (∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a j_1 ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) j (↑toLex x j ) (↑toLex (update x i a j ) h : ↑toLex x j < ↑toLex (update x i a j h ⟨j, hj, h⟩ : (∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a j_1 ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) j (↑toLex x j ) (↑toLex (update x i a j )
dsimp at h : ↑toLex x j < ↑toLex (update x i a j h
obtain rfl : j = i := by
by_contra H
rw [ update_noteq : ∀ {α : Sort ?u.15643} {β : α → Sort ?u.15642inst : DecidableEq α a a' : α },
a ≠ a' ∀ (v : β a' f : (a : α ) → β a ), update f a' v a = f a H ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i : ι a : β i j : ι hj : ∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a j_1 h : x j < x j H : ¬ j = i ] ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i : ι a : β i j : ι hj : ∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a j_1 h : x j < x j H : ¬ j = i at h ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i : ι a : β i j : ι hj : ∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a j_1 h : x j < x j H : ¬ j = i
exact h . false
rwa [ update_same : ∀ {α : Sort ?u.15003} {β : α → Sort ?u.15002inst : DecidableEq α a : α ) (v : β a f : (a : α ) → β a ),
update f a v a = v ] at h
#align pi.lt_to_lex_update_self_iff Pi.lt_toLex_update_self_iff
@[ simp ]
theorem toLex_update_lt_self_iff : toLex ( update : {α : Sort ?u.16139} →
{β : α → Sort ?u.16138[inst : DecidableEq α ((a : α ) → β a ) → (a' : α ) → β a' (a : α ) → β a x i a ) < toLex x ↔ a < x i := by
refine' ⟨ _ , fun h => toLex_strictMono <| update_lt_self_iff : ∀ {ι : Type ?u.16785} {π : ι → Type ?u.16786inst : DecidableEq ι inst_1 : (i : ι ) → Preorder (π i ]
{x : (i : ι ) → π i } {i : ι } {a : π i update x i a < x ↔ a < x i . 2 : ∀ {a b : Prop }, (a ↔ b b → a h ⟩ ↑toLex (update x i a < ↑toLex x a < x i
rintro ⟨ j , hj : ∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex (update x i a j_1 = ↑toLex x j_1 hj , h : ↑toLex (update x i a j < ↑toLex x j h ⟩
dsimp at h : ↑toLex (update x i a j < ↑toLex x j h
obtain rfl : j = i := by
by_contra H
rw [ update_noteq : ∀ {α : Sort ?u.17798} {β : α → Sort ?u.17797inst : DecidableEq α a a' : α },
a ≠ a' ∀ (v : β a' f : (a : α ) → β a ), update f a' v a = f a H ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i : ι a : β i j : ι hj : ∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex (update x i a j_1 = ↑toLex x j_1 h : x j < x j H : ¬ j = i ] ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i : ι a : β i j : ι hj : ∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex (update x i a j_1 = ↑toLex x j_1 h : x j < x j H : ¬ j = i at h ι : Type u_1β : ι → Type u_2r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : LinearOrder ι inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1 inst✝ : (i : ι ) → PartialOrder (β i x, y : (i : ι ) → β i i : ι a : β i j : ι hj : ∀ (j_1 : ι ), (fun x x_1 => x < x_1 ) j_1 j → ↑toLex (update x i a j_1 = ↑toLex x j_1 h : x j < x j H : ¬ j = i
exact h . false
rwa [ update_same : ∀ {α : Sort ?u.17159} {β : α → Sort ?u.17158inst : DecidableEq α a : α ) (v : β a f : (a : α ) → β a ),
update f a v a = v ] at h
#align pi.to_lex_update_lt_self_iff Pi.toLex_update_lt_self_iff
@[ simp ]
theorem le_toLex_update_self_iff : toLex x ≤ toLex ( update : {α : Sort ?u.18374} →
{β : α → Sort ?u.18373[inst : DecidableEq α ((a : α ) → β a ) → (a' : α ) → β a' (a : α ) → β a x i a ) ↔ x i ≤ a := by
simp_rw [ le_iff_lt_or_eq , lt_toLex_update_self_iff : ∀ {ι : Type ?u.19425} {β : ι → Type ?u.19426inst : LinearOrder ι inst_1 : IsWellOrder ι fun x x_1 => x < x_1 inst_2 : (i : ι ) → PartialOrder (β i ] {x : (i : ι ) → β i } {i : ι } {a : β i ↑toLex x < ↑toLex (update x i a ↔ x i < a , toLex_inj : ∀ {α : Type ?u.19713} {a b : α }, ↑toLex a = ↑toLex b ↔ a = b , eq_update_self_iff ]
#align pi.le_to_lex_update_self_iff Pi.le_toLex_update_self_iff
@[ simp ]
theorem toLex_update_le_self_iff : toLex ( update : {α : Sort ?u.20861} →
{β : α → Sort ?u.20860[inst : DecidableEq α ((a : α ) → β a ) → (a' : α ) → β a' (a : α ) → β a x i a ) ≤ toLex x ↔ a ≤ x i := by
simp_rw [ le_iff_lt_or_eq , toLex_update_lt_self_iff : ∀ {ι : Type ?u.21837} {β : ι → Type ?u.21838inst : LinearOrder ι inst_1 : IsWellOrder ι fun x x_1 => x < x_1 inst_2 : (i : ι ) → PartialOrder (β i ] {x : (i : ι ) → β i } {i : ι } {a : β i ↑toLex (update x i a < ↑toLex x ↔ a < x i , toLex_inj : ∀ {α : Type ?u.22125} {a b : α }, ↑toLex a = ↑toLex b ↔ a = b , update_eq_self_iff : ∀ {α : Sort ?u.22334} {β : α → Sort ?u.22333inst : DecidableEq α f : (a : α ) → β a } {a : α } {b : β a update f a b = f ↔ b = f a ]
#align pi.to_lex_update_le_self_iff Pi.toLex_update_le_self_iff
end PartialOrder
instance [ LinearOrder : Type ?u.22827 → Type ?u.22827 ι ] [ IsWellOrder ι (· < ·) ] [∀ a , PartialOrder : Type ?u.23031 → Type ?u.23031 ( β a )] [∀ a , OrderBot : (α : Type ?u.23039) → [inst : LE α Type ?u.23039 ( β a )] :
OrderBot : (α : Type ?u.23070) → [inst : LE α Type ?u.23070 ( Lex (∀ a , β a )) where
bot := toLex ⊥
bot_le _ := toLex_monotone bot_le : ∀ {α : Type ?u.23434} [inst : LE α inst_1 : OrderBot α a : α }, ⊥ ≤ a
instance [ LinearOrder : Type ?u.24164 → Type ?u.24164 ι ] [ IsWellOrder ι (· < ·) ] [∀ a , PartialOrder : Type ?u.24368 → Type ?u.24368 ( β a )] [∀ a , OrderTop : (α : Type ?u.24376) → [inst : LE α Type ?u.24376 ( β a )] :
OrderTop : (α : Type ?u.24407) → [inst : LE α Type ?u.24407 ( Lex (∀ a , β a )) where
top := toLex ⊤
le_top _ := toLex_monotone le_top : ∀ {α : Type ?u.24759} [inst : LE α inst_1 : OrderTop α a : α }, a ≤ ⊤
instance [ LinearOrder : Type ?u.25433 → Type ?u.25433 ι ] [ IsWellOrder ι (· < ·) ] [∀ a , PartialOrder : Type ?u.25637 → Type ?u.25637 ( β a )]
[∀ a , BoundedOrder : (α : Type ?u.25645) → [inst : LE α Type ?u.25645 ( β a )] : BoundedOrder : (α : Type ?u.25676) → [inst : LE α Type ?u.25676 ( Lex (∀ a , β a )) :=
{ }
instance [ Preorder ι ] [∀ i , LT ( β i )] [∀ i , DenselyOrdered : (α : Type ?u.26237) → [inst : LT α Prop ( β i )] :
DenselyOrdered : (α : Type ?u.26249) → [inst : LT α Prop ( Lex (∀ i , β i )) :=
⟨ by
∀ (a₁ a₂ : Lex ((i : ι ) → β i )a₁ < a₂ ∃ a , a₁ < a ∧ a < a₂ rintro _ a₂ ⟨i, h, hi⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) i (a₁✝ i a₂ i i ⟨i, h, hi⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) i (a₁✝ i a₂ i h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j h ⟨i, h, hi⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) i (a₁✝ i a₂ i hi ⟨i, h, hi⟩ : (∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j ) ∧ (fun x x_1 x_2 => x_1 < x_2 ) i (a₁✝ i a₂ i ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i intro.intro
∀ (a₁ a₂ : Lex ((i : ι ) → β i )a₁ < a₂ ∃ a , a₁ < a ∧ a < a₂ obtain ⟨a, ha₁, ha₂⟩ : ∃ a , a₁✝ i < a ∧ a < a₂ i a ⟨a, ha₁, ha₂⟩ : ∃ a , a₁✝ i < a ∧ a < a₂ i ha₁ ⟨a, ha₁, ha₂⟩ : ∃ a , a₁✝ i < a ∧ a < a₂ i ha₂ ⟨a, ha₁, ha₂⟩ : ∃ a , a₁✝ i < a ∧ a < a₂ i := exists_between : ∀ {α : Type ?u.26416} [inst : LT α inst_1 : DenselyOrdered α a₁ a₂ : α }, a₁ < a₂ ∃ a , a₁ < a ∧ a < a₂ hi ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i intro.intro.intro.intro
∀ (a₁ a₂ : Lex ((i : ι ) → β i )a₁ < a₂ ∃ a , a₁ < a ∧ a < a₂ classical
ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i intro.intro.intro.intro refine' ⟨ Function.update : {α : Sort ?u.26516} →
{β : α → Sort ?u.26515[inst : DecidableEq α ((a : α ) → β a ) → (a' : α ) → β a' (a : α ) → β a a₂ _ a , ⟨ i , fun j hj => _ , _ ⟩, i , fun j hj => _ , _ ⟩ ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i j : ι hj : (fun x x_1 => x < x_1 ) j i intro.intro.intro.intro.refine'_1 ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i intro.intro.intro.intro.refine'_2 ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i j : ι hj : (fun x x_1 => x < x_1 ) j i intro.intro.intro.intro.refine'_3 ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i intro.intro.intro.intro.refine'_4
ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i intro.intro.intro.intro rw [ ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i j : ι hj : (fun x x_1 => x < x_1 ) j i intro.intro.intro.intro.refine'_1 ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i intro.intro.intro.intro.refine'_2 ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i j : ι hj : (fun x x_1 => x < x_1 ) j i intro.intro.intro.intro.refine'_3 ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i intro.intro.intro.intro.refine'_4 h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j h j hj ι : Type ?u.26198β : ι → Type ?u.26203r : ι → ι → Prop s : {i : ι } → β i β i Prop inst✝² : Preorder ι inst✝¹ : (i : ι ) → LT (β i inst✝ : ∀ (i : ι ), DenselyOrdered (β i a₁✝, a₂ : Lex ((i : ι ) → β i )i : ι h : ∀ (j : ι ), (fun x x_1 => x < x_1 ) j i → a₁✝ j = a₂ j hi : a₁✝ i < a₂ i a : β i ha₁ : a₁✝ i < a ha₂ : a < a₂ i j : ι