-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem forall_lt_succ_right' {p : (m : Nat) → (m < n + 1) → Prop} :
    (∀ m (h : m < n + 1), p m h) ↔ (∀ m (h : m < n), p m (by omega)) ∧ p n (by omega)

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯) ↔ (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯

Tactic:
constructor

Result:
case mp
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯) → (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯

case mpr
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯ → ∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯

Proof state:
case mp
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯) → (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯

Tactic:
intro w

Result:
case mp
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : ∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯
⊢ (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯

Proof state:
case mp.right
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : ∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯
⊢ p n ⋯

Tactic:
exact w _ (.inr rfl)

Result:
no goals

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
⊢ m < n + 1

Tactic:
omega

Result:
no goals

Proof state:
case mpr.inl
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯
m : Nat
h : m < n
⊢ p m ⋯

Tactic:
exact w.1 _ h

Result:
no goals

Proof state:
case mp
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : ∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯
⊢ (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯

Tactic:
constructor

Result:
case mp.left
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : ∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯
⊢ ∀ (m : Nat) (h : m < n), p m ⋯

case mp.right
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : ∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯
⊢ p n ⋯

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ n < n + 1

Tactic:
omega

Result:
no goals

Proof state:
case mp.left
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : ∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯
m : Nat
h : m < n
⊢ p m ⋯

Tactic:
exact w _ (.inl h)

Result:
no goals

Proof state:
case mpr
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯ → ∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯

Tactic:
rintro w m (h|rfl)

Result:
case mpr.inl
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯
m : Nat
h : m < n
⊢ p m ⋯

case mpr.inr
m : Nat
p : (m_1 : Nat) → m_1 < m + 1 → Prop
w : (∀ (m_1 : Nat) (h : m_1 < m), p m_1 ⋯) ∧ p m ⋯
⊢ p m ⋯

Proof state:
case mp.left
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : ∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯
⊢ ∀ (m : Nat) (h : m < n), p m ⋯

Tactic:
intro m h

Result:
case mp.left
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : ∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯
m : Nat
h : m < n
⊢ p m ⋯

Proof state:
case mpr.inr
m : Nat
p : (m_1 : Nat) → m_1 < m + 1 → Prop
w : (∀ (m_1 : Nat) (h : m_1 < m), p m_1 ⋯) ∧ p m ⋯
⊢ p m ⋯

Tactic:
exact w.2

Result:
no goals

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∀ (m : Nat) (h : m < n + 1), p m h) ↔ (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯

Tactic:
simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]

Result:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∀ (m : Nat) (h : m < n ∨ m = n), p m ⋯) ↔ (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯