-- Mathlib/Data/DFinsupp/Lex.lean
theorem lex_lt_of_lt_of_preorder [∀ i, Preorder (α i)] (r) [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

Proof state:
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 : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
this : (↑(x.neLocus y)).WellFoundedOn r
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
obtain ⟨i, hi, hl⟩ := this.has_min { i | x i < y i } ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩

Result:
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 : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
this : (↑(x.neLocus y)).WellFoundedOn r
i : ↑↑(x.neLocus y)
hi : i ∈ {i | x ↑i < y ↑i}
hl : ∀ 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

Proof state:
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 : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
this : (↑(x.neLocus y)).WellFoundedOn r
i : ↑↑(x.neLocus y)
hi : i ∈ {i | x ↑i < y ↑i}
hl : ∀ x_1 ∈ {i | x ↑i < y ↑i}, ¬r ↑x_1 ↑i
k : ι
hk : r k ↑i
⊢ y k ≤ x k

Tactic:
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

Result:
no goals

Proof state:
ι : 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

Tactic:
obtain ⟨hle, j, hlt⟩ := Pi.lt_def.1 hlt

Result:
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 : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Proof state:
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 : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn

Result:
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 : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
this : (↑(x.neLocus y)).WellFoundedOn r
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Proof state:
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 : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
this : (↑(x.neLocus y)).WellFoundedOn r
i : ↑↑(x.neLocus y)
hi : i ∈ {i | x ↑i < y ↑i}
hl : ∀ 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

Tactic:
refine ⟨i, fun k hk ↦ ⟨hle k, ?_⟩, hi⟩

Result:
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 : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
this : (↑(x.neLocus y)).WellFoundedOn r
i : ↑↑(x.neLocus y)
hi : i ∈ {i | x ↑i < y ↑i}
hl : ∀ x_1 ∈ {i | x ↑i < y ↑i}, ¬r ↑x_1 ↑i
k : ι
hk : r k ↑i
⊢ y k ≤ x k

Proof state:
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 : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
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

Result:
no goals