[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι 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
[PROOFSTEP]
obtain ⟨hle, j, hlt⟩ := Pi.lt_def.1 hlt
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : (fun i => ↑x i) ≤ fun i => ↑y i
j : ι
hlt : ↑x j < ↑y j
⊢ ∃ i, (∀ (j : ι), r j i → ↑x j ≤ ↑y j ∧ ↑y j ≤ ↑x j) ∧ ↑x i < ↑y i
[PROOFSTEP]
classical
have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
obtain ⟨i, hi, hl⟩ := this.has_min {i | x i < y i} ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
refine' ⟨i, fun k hk ↦ ⟨hle k, _⟩, hi⟩
exact of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_le h) hk
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : (fun i => ↑x i) ≤ fun i => ↑y i
j : ι
hlt : ↑x j < ↑y j
⊢ ∃ i, (∀ (j : ι), r j i → ↑x j ≤ ↑y j ∧ ↑y j ≤ ↑x j) ∧ ↑x i < ↑y i
[PROOFSTEP]
have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : (fun i => ↑x i) ≤ fun i => ↑y i
j : ι
hlt : ↑x j < ↑y j
this : Set.WellFoundedOn (↑(neLocus x y)) r
⊢ ∃ i, (∀ (j : ι), r j i → ↑x j ≤ ↑y j ∧ ↑y j ≤ ↑x j) ∧ ↑x i < ↑y i
[PROOFSTEP]
obtain ⟨i, hi, hl⟩ := this.has_min {i | x i < y i} ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : (fun i => ↑x i) ≤ fun i => ↑y i
j : ι
hlt : ↑x j < ↑y j
this : Set.WellFoundedOn (↑(neLocus x y)) r
i : ↑↑(neLocus x y)
hi : i ∈ {i | ↑x ↑i < ↑y ↑i}
hl : ∀ (x_1 : ↑↑(neLocus x y)), x_1 ∈ {i | ↑x ↑i < ↑y ↑i} → ¬r ↑x_1 ↑i
⊢ ∃ i, (∀ (j : ι), r j i → ↑x j ≤ ↑y j ∧ ↑y j ≤ ↑x j) ∧ ↑x i < ↑y i
[PROOFSTEP]
refine' ⟨i, fun k hk ↦ ⟨hle k, _⟩, hi⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : (fun i => ↑x i) ≤ fun i => ↑y i
j : ι
hlt : ↑x j < ↑y j
this : Set.WellFoundedOn (↑(neLocus x y)) r
i : ↑↑(neLocus x y)
hi : i ∈ {i | ↑x ↑i < ↑y ↑i}
hl : ∀ (x_1 : ↑↑(neLocus x y)), x_1 ∈ {i | ↑x ↑i < ↑y ↑i} → ¬r ↑x_1 ↑i
k : ι
hk : r k ↑i
⊢ ↑y k ≤ ↑x k
[PROOFSTEP]
exact of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_le h) hk
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ Pi.Lex r (fun {i} x x_1 => x < x_1) ↑x ↑y
[PROOFSTEP]
simp_rw [Pi.Lex, le_antisymm_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι 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
[PROOFSTEP]
exact lex_lt_of_lt_of_preorder r hlt
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
⊢ P (↑toLex f) (↑toLex g)
[PROOFSTEP]
apply (mem_neLocus.mp <| Finset.mem_of_min h).lt_or_lt.by_cases
[GOAL]
case h₁
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
⊢ ↑f wit < ↑g wit → P (↑toLex f) (↑toLex g)
[PROOFSTEP]
intro hwit
[GOAL]
case h₂
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
⊢ ↑g wit < ↑f wit → P (↑toLex f) (↑toLex g)
[PROOFSTEP]
intro hwit
[GOAL]
case h₁
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
hwit : ↑f wit < ↑g wit
⊢ P (↑toLex f) (↑toLex g)
[PROOFSTEP]
exact h_lt ⟨wit, fun j hj ↦ not_mem_neLocus.mp (Finset.not_mem_of_lt_min hj h), hwit⟩
[GOAL]
case h₂
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
hwit : ↑g wit < ↑f wit
⊢ P (↑toLex f) (↑toLex g)
[PROOFSTEP]
exact h_gt ⟨wit, fun j hj ↦ not_mem_neLocus.mp (Finset.not_mem_of_lt_min hj <| by rwa [neLocus_comm]), hwit⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → ↑toLex f < ↑toLex g → P (↑toLex f) (↑toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → ↑toLex f = ↑toLex g → P (↑toLex f) (↑toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → ↑toLex g < ↑toLex f → P (↑toLex f) (↑toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : Finset.min (neLocus f g) = ↑wit
hwit : ↑g wit < ↑f wit
j : ι
hj : (fun x x_1 => x < x_1) j wit
⊢ Finset.min (neLocus (↑ofLex (↑toLex g)) (↑ofLex (↑toLex f))) = ↑wit
[PROOFSTEP]
rwa [neLocus_comm]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
⊢ Monotone ↑toLex
[PROOFSTEP]
intro a b h
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
⊢ ↑toLex a ≤ ↑toLex b
[PROOFSTEP]
refine' le_of_lt_or_eq (or_iff_not_imp_right.2 fun hne ↦ _)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬↑toLex a = ↑toLex b
⊢ ↑toLex a < ↑toLex b
[PROOFSTEP]
classical exact
  ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne), fun j hj ↦ not_mem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_lt hj,
    (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬↑toLex a = ↑toLex b
⊢ ↑toLex a < ↑toLex b
[PROOFSTEP]
exact
  ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne), fun j hj ↦ not_mem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_lt hj,
    (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩
