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

Proof state:
case pos
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : y ≤ x
⊢ TransGen (fun x1 x2 => x1 ⩿ x2) x y

Tactic:
exact .single <| wcovBy_of_le_of_le hxy hxy'

Result:
no goals

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

Tactic:
exact .tail h₁ h₂

Result:
no goals

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

Tactic:
have h₂ : z ⩿ y := by
  refine ⟨(mem_Ico.mp z_mem).2.le, fun c hzc hcy ↦ hz c ?_ hzc⟩
  exact mem_Ico.mpr <| ⟨(mem_Ico.mp z_mem).1.trans hzc.le, hcy⟩

Result:
case neg.intro.intro
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Icc x z) < #(Icc x y)
h₁ : TransGen (fun x1 x2 => x1 ⩿ x2) x z
h₂ : z ⩿ y
⊢ TransGen (fun x1 x2 => x1 ⩿ x2) x y

Proof state:
case neg.intro.intro
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
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 := calc
  #(Icc x z) ≤ #(Ico x y) := card_le_card <| Icc_subset_Ico_right (mem_Ico.mp z_mem).2
  _          < #(Icc x y) := this

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

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

Tactic:
have h₁ := transGen_wcovBy_of_le (mem_Ico.mp z_mem).1

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

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
⊢ TransGen (fun x1 x2 => x1 ⩿ x2) x y

Tactic:
by_cases hxy' : y ≤ x

Result:
case pos
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : y ≤ x
⊢ TransGen (fun x1 x2 => x1 ⩿ x2) x y

case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
⊢ TransGen (fun x1 x2 => x1 ⩿ x2) x y

Proof state:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
⊢ TransGen (fun x1 x2 => x1 ⩿ x2) x y

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

Result:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
h_non : (Ico x y).Nonempty
⊢ TransGen (fun x1 x2 => x1 ⩿ x2) 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 : #(Ico x y) < #(Icc x y) := card_lt_card <|
  ⟨Ico_subset_Icc_self, not_subset.mpr ⟨y, ⟨right_mem_Icc.mpr hxy, right_not_mem_Ico⟩⟩⟩

Result:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
⊢ TransGen (fun x1 x2 => x1 ⩿ x2) x y

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Icc x z) < #(Icc x y)
h₁ : TransGen (fun x1 x2 => x1 ⩿ x2) x z
c : α
hzc : z < c
hcy : c < y
⊢ c ∈ Ico x y

Tactic:
exact mem_Ico.mpr <| ⟨(mem_Ico.mp z_mem).1.trans hzc.le, hcy⟩

Result:
no goals

Proof state:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
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 neg.intro.intro
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
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:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Icc x z) < #(Icc x y)
h₁ : TransGen (fun x1 x2 => x1 ⩿ x2) x z
⊢ z ⩿ y

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

Result:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
h_non : (Ico x y).Nonempty
z : α
z_mem : z ∈ Ico x y
hz : ∀ x_1 ∈ Ico x y, ¬z < x_1
z_card : #(Icc x z) < #(Icc x y)
h₁ : TransGen (fun x1 x2 => x1 ⩿ x2) x z
c : α
hzc : z < c
hcy : c < y
⊢ c ∈ Ico x y