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

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
h₀ : p 0 ⋯
h₁ : ∀ (m : Nat) (h : m < n), p (m + 1) ⋯
m : Nat
h : m + 1 < n + 1
⊢ m < n

Tactic:
omega

Result:
no goals

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

Tactic:
intro w

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
rintro ⟨h₀, h₁⟩ m h

Result:
case mpr.intro
n : Nat
p : (m : Nat) → m < n + 1 → Prop
h₀ : p 0 ⋯
h₁ : ∀ (m : Nat) (h : m < n), p (m + 1) ⋯
m : Nat
h : m < n + 1
⊢ p m h

Proof state:
case mpr.intro.zero
n : Nat
p : (m : Nat) → m < n + 1 → Prop
h₀ : p 0 ⋯
h₁ : ∀ (m : Nat) (h : m < n), p (m + 1) ⋯
h : 0 < n + 1
⊢ p 0 h

Tactic:
exact h₀

Result:
no goals

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

Tactic:
intro m h

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

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

Tactic:
exact w 0 (by omega)

Result:
no goals

Proof state:
case mpr.intro
n : Nat
p : (m : Nat) → m < n + 1 → Prop
h₀ : p 0 ⋯
h₁ : ∀ (m : Nat) (h : m < n), p (m + 1) ⋯
m : Nat
h : m < n + 1
⊢ p m h

Tactic:
cases m with
| zero => exact h₀
| succ m => exact h₁ m (by omega)

Result:
no goals

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

Tactic:
constructor

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

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
exact w (m + 1) (by omega)

Result:
no goals

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

Tactic:
constructor

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

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

Proof state:
case mpr.intro.succ
n : Nat
p : (m : Nat) → m < n + 1 → Prop
h₀ : p 0 ⋯
h₁ : ∀ (m : Nat) (h : m < n), p (m + 1) ⋯
m : Nat
h : m + 1 < n + 1
⊢ p (m + 1) h

Tactic:
exact h₁ m (by omega)

Result:
no goals

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

Tactic:
omega

Result:
no goals

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

Tactic:
omega

Result:
no goals