-- Mathlib/Order/Interval/Finset/Basic.lean
lemma transGen_covBy_of_lt [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x < y) :
    TransGen (· ⋖ ·) x y

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
have h_non : (Ico x y).Nonempty := ⟨x, mem_Ico.mpr ⟨le_rfl, hxy⟩⟩

Result:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Proof state:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x ≤ z → z ≤ x
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
exact .single (hzy.of_le_of_lt (hxz (mem_Ico.mp z_mem).1) hxy)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
⊢ z ⋖ y

Tactic:
refine ⟨(mem_Ico.mp z_mem).2, fun c hc hcy ↦ ?_⟩

Result:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
c : α
hc : z < c
hcy : c < y
⊢ False

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
obtain ⟨z, z_mem, hz⟩ := (Ico x y).exists_maximal h_non

Result:
case intro.intro
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
by_cases hxz : x < z

Result:
case pos
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x < z
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : ¬x < z
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
c : α
hc : z < c
hcy : c < y
⊢ False

Tactic:
exact hz _ (mem_Ico.mpr ⟨((mem_Ico.mp z_mem).1.trans_lt hc).le, hcy⟩) hc

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
have z_card : #(Ico x z) < #(Ico x y) := card_lt_card <| ssubset_iff_of_subset
  (Ico_subset_Ico le_rfl (mem_Ico.mp z_mem).2.le) |>.mpr ⟨z, z_mem, right_not_mem_Ico⟩

Result:
case intro.intro
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Proof state:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : ¬x < z
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
simp only [lt_iff_le_not_le, not_and, not_not] at hxz

Result:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x ≤ z → z ≤ x
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Proof state:
case pos
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x < z
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
exact .tail (transGen_covBy_of_lt hxz) hzy

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
have hzy : z ⋖ y := by
  refine ⟨(mem_Ico.mp z_mem).2, fun c hc hcy ↦ ?_⟩
  exact hz _ (mem_Ico.mpr ⟨((mem_Ico.mp z_mem).1.trans_lt hc).le, hcy⟩) hc

Result:
case intro.intro
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
⊢ TransGen (fun x1 x2 => x1 ⋖ x2) x y