[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ (i : α), i ∈ Ico n m → r i (succ i)
hnm : n ≤ m
⊢ ReflTransGen r n m
[PROOFSTEP]
revert h
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ (∀ (i : α), i ∈ Ico n m → r i (succ i)) → ReflTransGen r n m
[PROOFSTEP]
refine' Succ.rec _ _ hnm
[GOAL]
case refine'_1
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ (∀ (i : α), i ∈ Ico n n → r i (succ i)) → ReflTransGen r n n
[PROOFSTEP]
intro _
[GOAL]
case refine'_1
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
h✝ : ∀ (i : α), i ∈ Ico n n → r i (succ i)
⊢ ReflTransGen r n n
[PROOFSTEP]
exact ReflTransGen.refl
[GOAL]
case refine'_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ ∀ (n_1 : α),
    n ≤ n_1 →
      ((∀ (i : α), i ∈ Ico n n_1 → r i (succ i)) → ReflTransGen r n n_1) →
        (∀ (i : α), i ∈ Ico n (succ n_1) → r i (succ i)) → ReflTransGen r n (succ n_1)
[PROOFSTEP]
intro m hnm ih h
[GOAL]
case refine'_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ (i : α), i ∈ Ico n m → r i (succ i)) → ReflTransGen r n m
h : ∀ (i : α), i ∈ Ico n (succ m) → r i (succ i)
⊢ ReflTransGen r n (succ m)
[PROOFSTEP]
have : ReflTransGen r n m := ih fun i hi => h i ⟨hi.1, hi.2.trans_le <| le_succ m⟩
[GOAL]
case refine'_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ (i : α), i ∈ Ico n m → r i (succ i)) → ReflTransGen r n m
h : ∀ (i : α), i ∈ Ico n (succ m) → r i (succ i)
this : ReflTransGen r n m
⊢ ReflTransGen r n (succ m)
[PROOFSTEP]
cases' (le_succ m).eq_or_lt with hm hm
[GOAL]
case refine'_2.inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ (i : α), i ∈ Ico n m → r i (succ i)) → ReflTransGen r n m
h : ∀ (i : α), i ∈ Ico n (succ m) → r i (succ i)
this : ReflTransGen r n m
hm : m = succ m
⊢ ReflTransGen r n (succ m)
[PROOFSTEP]
rwa [← hm]
[GOAL]
case refine'_2.inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ (i : α), i ∈ Ico n m → r i (succ i)) → ReflTransGen r n m
h : ∀ (i : α), i ∈ Ico n (succ m) → r i (succ i)
this : ReflTransGen r n m
hm : m < succ m
⊢ ReflTransGen r n (succ m)
[PROOFSTEP]
exact this.tail (h m ⟨hnm, hm⟩)
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ (i : α), i ∈ Ico m n → r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen r n m
[PROOFSTEP]
rw [← reflTransGen_swap]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ (i : α), i ∈ Ico m n → r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen (swap r) m n
[PROOFSTEP]
exact reflTransGen_of_succ_of_le (swap r) h hmn
[GOAL]
α : 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
[PROOFSTEP]
rcases eq_or_ne m n with (rfl | hmn)
[GOAL]
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
[PROOFSTEP]
exact TransGen.single (hr m)
[GOAL]
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
[PROOFSTEP]
exact transGen_of_succ_of_ne r h1 h2 hmn.symm
