Theorem: Nat.ball_pos_iff (Logic/Vorspiel/Arith.lean)

State before:
p : ℕ → ℕ
n : ℕ
⊢ 0 < n.ball p ↔ ∀ m < n, 0 < p m
Tactic:
induction' n with n ih <;> simp[ball, Nat.lt_succ_iff] at*
State after:
case succ
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m ≤ n, 0 < p m

State before:
case succ
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m ≤ n, 0 < p m
Tactic:
simp[ih]
State after:
case succ
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ (0 < p n ∧ ∀ m < n, 0 < p m) ↔ ∀ m ≤ n, 0 < p m

State before:
case succ
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ (0 < p n ∧ ∀ m < n, 0 < p m) ↔ ∀ m ≤ n, 0 < p m
Tactic:
exact ⟨
by rintro ⟨hn, hp⟩ m hm; rcases lt_or_eq_of_le hm with (hm | rfl); { exact hp _ hm }; { exact hn },
by intro h; exact ⟨h n (Nat.le_refl n), fun m hm => h m (le_of_lt hm)⟩⟩
State after:
no goals

State before:
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ (0 < p n ∧ ∀ m < n, 0 < p m) → ∀ m ≤ n, 0 < p m
Tactic:
rintro ⟨hn, hp⟩ m hm
State after:
case intro
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
hn : 0 < p n
hp : ∀ m < n, 0 < p m
m : ℕ
hm : m ≤ n
⊢ 0 < p m

State before:
case intro
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
hn : 0 < p n
hp : ∀ m < n, 0 < p m
m : ℕ
hm : m ≤ n
⊢ 0 < p m
Tactic:
rcases lt_or_eq_of_le hm with (hm | rfl)
State after:
case intro.inl
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
hn : 0 < p n
hp : ∀ m < n, 0 < p m
m : ℕ
hm✝ : m ≤ n
hm : m < n
⊢ 0 < p m

case intro.inr
p : ℕ → ℕ
m : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) m ↔ ∀ m_1 < m, 0 < p m_1
hn : 0 < p m
hp : ∀ m_1 < m, 0 < p m_1
hm : m ≤ m
⊢ 0 < p m

State before:
case intro.inl
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
hn : 0 < p n
hp : ∀ m < n, 0 < p m
m : ℕ
hm✝ : m ≤ n
hm : m < n
⊢ 0 < p m

case intro.inr
p : ℕ → ℕ
m : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) m ↔ ∀ m_1 < m, 0 < p m_1
hn : 0 < p m
hp : ∀ m_1 < m, 0 < p m_1
hm : m ≤ m
⊢ 0 < p m
Tactic:
{ exact hp _ hm }
State after:
case intro.inr
p : ℕ → ℕ
m : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) m ↔ ∀ m_1 < m, 0 < p m_1
hn : 0 < p m
hp : ∀ m_1 < m, 0 < p m_1
hm : m ≤ m
⊢ 0 < p m

State before:
case intro.inr
p : ℕ → ℕ
m : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) m ↔ ∀ m_1 < m, 0 < p m_1
hn : 0 < p m
hp : ∀ m_1 < m, 0 < p m_1
hm : m ≤ m
⊢ 0 < p m
Tactic:
{ exact hn }
State after:
no goals

State before:
case intro.inl
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
hn : 0 < p n
hp : ∀ m < n, 0 < p m
m : ℕ
hm✝ : m ≤ n
hm : m < n
⊢ 0 < p m
Tactic:
exact hp _ hm
State after:
no goals

State before:
case intro.inr
p : ℕ → ℕ
m : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) m ↔ ∀ m_1 < m, 0 < p m_1
hn : 0 < p m
hp : ∀ m_1 < m, 0 < p m_1
hm : m ≤ m
⊢ 0 < p m
Tactic:
exact hn
State after:
no goals

State before:
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ (∀ m ≤ n, 0 < p m) → 0 < p n ∧ ∀ m < n, 0 < p m
Tactic:
intro h
State after:
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
h : ∀ m ≤ n, 0 < p m
⊢ 0 < p n ∧ ∀ m < n, 0 < p m

State before:
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
h : ∀ m ≤ n, 0 < p m
⊢ 0 < p n ∧ ∀ m < n, 0 < p m
Tactic:
exact ⟨h n (Nat.le_refl n), fun m hm => h m (le_of_lt hm)⟩
State after:
no goals