case mp
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x x_1 => x < x_1) ⇒ r) f f → ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))

case mpr
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))) → ((fun x x_1 => x < x_1) ⇒ r) f f
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x x_1 => x < x_1) ⇒ r) f f ↔ ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
constructor
case mp
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ((fun x x_1 => x < x_1) ⇒ r) f f
i : Fin n
⊢ r (f (↑castSucc i)) (f (succ i))
case mp
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x x_1 => x < x_1) ⇒ r) f f → ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
intro H i
no goals
case mp
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ((fun x x_1 => x < x_1) ⇒ r) f f
i : Fin n
⊢ r (f (↑castSucc i)) (f (succ i))
exact H i.castSucc_lt_succ
case mpr.refine'_1
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
i : Fin (n + 1)
⊢ (fun x x_1 => x < x_1) i 0 → r (f i) (f 0)

case mpr.refine'_2
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin n),
    ((fun x x_1 => x < x_1) i (↑castSucc i_1) → r (f i) (f (↑castSucc i_1))) →
      (fun x x_1 => x < x_1) i (succ i_1) → r (f i) (f (succ i_1))
case mpr
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))) → ((fun x x_1 => x < x_1) ⇒ r) f f
refine' fun H i => Fin.induction _ _
no goals
case mpr.refine'_1
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
i : Fin (n + 1)
⊢ (fun x x_1 => x < x_1) i 0 → r (f i) (f 0)
exact fun h => (h.not_le (zero_le i)).elim
case mpr.refine'_2
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
i : Fin (n + 1)
j : Fin n
ihj : (fun x x_1 => x < x_1) i (↑castSucc j) → r (f i) (f (↑castSucc j))
hij : i < succ j
⊢ r (f i) (f (succ j))
case mpr.refine'_2
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin n),
    ((fun x x_1 => x < x_1) i (↑castSucc i_1) → r (f i) (f (↑castSucc i_1))) →
      (fun x x_1 => x < x_1) i (succ i_1) → r (f i) (f (succ i_1))
intro j ihj hij
case mpr.refine'_2
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
i : Fin (n + 1)
j : Fin n
ihj : (fun x x_1 => x < x_1) i (↑castSucc j) → r (f i) (f (↑castSucc j))
hij : i ≤ ↑castSucc j
⊢ r (f i) (f (succ j))
case mpr.refine'_2
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
i : Fin (n + 1)
j : Fin n
ihj : (fun x x_1 => x < x_1) i (↑castSucc j) → r (f i) (f (↑castSucc j))
hij : i < succ j
⊢ r (f i) (f (succ j))
rw [← le_castSucc_iff] at hij
case mpr.refine'_2.inl
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
j : Fin n
ihj : (fun x x_1 => x < x_1) (↑castSucc j) (↑castSucc j) → r (f (↑castSucc j)) (f (↑castSucc j))
hij : ↑castSucc j ≤ ↑castSucc j
⊢ r (f (↑castSucc j)) (f (succ j))

case mpr.refine'_2.inr
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
i : Fin (n + 1)
j : Fin n
ihj : (fun x x_1 => x < x_1) i (↑castSucc j) → r (f i) (f (↑castSucc j))
hij : i ≤ ↑castSucc j
hlt : i < ↑castSucc j
⊢ r (f i) (f (succ j))
case mpr.refine'_2
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
i : Fin (n + 1)
j : Fin n
ihj : (fun x x_1 => x < x_1) i (↑castSucc j) → r (f i) (f (↑castSucc j))
hij : i ≤ ↑castSucc j
⊢ r (f i) (f (succ j))
rcases hij.eq_or_lt with (rfl | hlt)
no goals
case mpr.refine'_2.inl
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
j : Fin n
ihj : (fun x x_1 => x < x_1) (↑castSucc j) (↑castSucc j) → r (f (↑castSucc j)) (f (↑castSucc j))
hij : ↑castSucc j ≤ ↑castSucc j
⊢ r (f (↑castSucc j)) (f (succ j))

case mpr.refine'_2.inr
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (↑castSucc i)) (f (succ i))
i : Fin (n + 1)
j : Fin n
ihj : (fun x x_1 => x < x_1) i (↑castSucc j) → r (f i) (f (↑castSucc j))
hij : i ≤ ↑castSucc j
hlt : i < ↑castSucc j
⊢ r (f i) (f (succ j))
exacts [H j, _root_.trans (ihj hlt) (H j)]