α : 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
α : 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
revert h
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

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)
α : 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
refine' Succ.rec _ _ hnm
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
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
intro _
no goals
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
exact ReflTransGen.refl
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)
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)
intro m hnm ih h
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)
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)
have : ReflTransGen r n m := ih fun i hi => h i ⟨hi.1, hi.2.trans_le <| le_succ m⟩
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)

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)
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)
cases' (le_succ m).eq_or_lt with hm hm
no goals
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)
exact this.tail (h m ⟨hnm, hm⟩)
no goals
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)
rwa [← hm]