case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
m : α
hr : Reflexive r
h1 : ∀ (i : α), i ∈ Ico m m → r i (succ i)
h2 : ∀ (i : α), i ∈ Ico m m → r (succ i) i
⊢ TransGen r m m

case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hr : Reflexive r
h1 : ∀ (i : α), i ∈ Ico n m → r i (succ i)
h2 : ∀ (i : α), i ∈ Ico m n → r (succ i) i
hmn : m ≠ n
⊢ TransGen r n m
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hr : Reflexive r
h1 : ∀ (i : α), i ∈ Ico n m → r i (succ i)
h2 : ∀ (i : α), i ∈ Ico m n → r (succ i) i
⊢ TransGen r n m
rcases eq_or_ne m n with (rfl | hmn)
no goals
case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hr : Reflexive r
h1 : ∀ (i : α), i ∈ Ico n m → r i (succ i)
h2 : ∀ (i : α), i ∈ Ico m n → r (succ i) i
hmn : m ≠ n
⊢ TransGen r n m
exact transGen_of_succ_of_ne r h1 h2 hmn.symm
no goals
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
m : α
hr : Reflexive r
h1 : ∀ (i : α), i ∈ Ico m m → r i (succ i)
h2 : ∀ (i : α), i ∈ Ico m m → r (succ i) i
⊢ TransGen r m m
exact TransGen.single (hr m)