case intro.intro
ι : Type u_2
α : ι → Type u_1
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
ι : Type u_2
α : ι → Type u_1
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
obtain ⟨hle, j, hlt⟩ := Pi.lt_def.1 hlt
no goals
case intro.intro
ι : Type u_2
α : ι → Type u_1
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
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
case intro.intro
ι : Type u_2
α : ι → Type u_1
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
case intro.intro
ι : Type u_2
α : ι → Type u_1
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
have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
case intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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
case intro.intro
ι : Type u_2
α : ι → Type u_1
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
obtain ⟨i, hi, hl⟩ := this.has_min { i | x i < y i } ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
case intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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
case intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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
refine' ⟨i, fun k hk ↦ ⟨hle k, _⟩, hi⟩
no goals
case intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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
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