α : Type u
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain' r (range (succ n)) ↔ ∀ (m : ℕ), m < n → r m (succ m)
rw [range_succ]
case zero
α : Type u
r : ℕ → ℕ → Prop
⊢ Chain' r (range zero ++ [zero]) ↔ ∀ (m : ℕ), m < zero → r m (succ m)

case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range (succ n) ++ [succ n]) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
induction' n with n hn
no goals
case zero
α : Type u
r : ℕ → ℕ → Prop
⊢ Chain' r (range zero ++ [zero]) ↔ ∀ (m : ℕ), m < zero → r m (succ m)
simp
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range n ++ [n] ++ [succ n]) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range (succ n) ++ [succ n]) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
rw [range_succ]
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range n ++ [n]) ∧ r n (succ n) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range n ++ [n] ++ [succ n]) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
simp only [append_assoc, singleton_append, chain'_append_cons_cons, chain'_singleton,
  and_true_iff]
no goals
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range n ++ [n]) ∧ r n (succ n) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
rw [hn, forall_lt_succ]