[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ { fst := k, snd := c } ∈ sigmaLift (fun x => Icc) { fst := i, snd := a } { fst := j, snd := b } ↔
    { fst := i, snd := a } ≤ { fst := k, snd := c } ∧ { fst := k, snd := c } ≤ { fst := j, snd := b }
[PROOFSTEP]
simp_rw [mem_sigmaLift, le_def, mem_Icc, exists_and_left, ← exists_and_right, ← exists_prop]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ h _h x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h _h h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) →
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b) →
    ∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mp.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a ≤ c
ht : c ≤ (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
⊢ ∃ h, (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
case mpr.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a ≤ c
ht : (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
⊢ ∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ { fst := k, snd := c } ∈ sigmaLift (fun x => Ico) { fst := i, snd := a } { fst := j, snd := b } ↔
    { fst := i, snd := a } ≤ { fst := k, snd := c } ∧ { fst := k, snd := c } < { fst := j, snd := b }
[PROOFSTEP]
simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ico, exists_and_left, ← exists_and_right, ← exists_prop]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ h _h x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h _h h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) →
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a ≤ c
⊢ (∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b) →
    ∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mp.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a ≤ c
ht : c < (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
⊢ ∃ h, (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
case mpr.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a ≤ c
ht : (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
⊢ ∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ { fst := k, snd := c } ∈ sigmaLift (fun x => Ioc) { fst := i, snd := a } { fst := j, snd := b } ↔
    { fst := i, snd := a } < { fst := k, snd := c } ∧ { fst := k, snd := c } ≤ { fst := j, snd := b }
[PROOFSTEP]
simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ioc, exists_and_left, ← exists_and_right, ← exists_prop]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ h _h x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h _h h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) →
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b) →
    ∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mp.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a < c
ht : c ≤ (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
⊢ ∃ h, (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
case mpr.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a < c
ht : (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c ≤ b
⊢ ∃ x, c ≤ (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ { fst := k, snd := c } ∈ sigmaLift (fun x => Ioo) { fst := i, snd := a } { fst := j, snd := b } ↔
    { fst := i, snd := a } < { fst := k, snd := c } ∧ { fst := k, snd := c } < { fst := j, snd := b }
[PROOFSTEP]
simp_rw [mem_sigmaLift, lt_def, mem_Ioo, exists_and_left, ← exists_and_right, ← exists_prop]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ h _h x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h _h h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) ↔
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b) →
    ∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : (_ : i = k) ▸ a < c
⊢ (∃ h, (_ : { fst := k, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b) →
    ∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := k, snd := c }.fst) ▸ b
[PROOFSTEP]
rintro ⟨⟨⟩, ht⟩
[GOAL]
case mp.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a < c
ht : c < (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
⊢ ∃ h, (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
[PROOFSTEP]
exact ⟨rfl, ht⟩
[GOAL]
case mpr.intro.refl
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b c : α j
x✝¹ : i = j
x✝ : (_ : i = j) ▸ a < c
ht : (_ : { fst := j, snd := c }.fst = { fst := j, snd := b }.fst) ▸ c < b
⊢ ∃ x, c < (_ : { fst := j, snd := b }.fst = { fst := j, snd := c }.fst) ▸ b
[PROOFSTEP]
exact ⟨rfl, ht⟩
