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

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

State before:
case succ
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1 ↔ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
Tactic:
constructor
State after:
case succ.mp
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1 → 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n

case succ.mpr
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n → (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1

State before:
case succ.mp
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1 → 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
Tactic:
intro h
State after:
case succ.mp
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
h : (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n

State before:
case succ.mp
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
h : (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
Tactic:
simpa using pos_of_eq_one h
State after:
no goals

State before:
case succ.mpr
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n → (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1
Tactic:
intro h
State after:
case succ.mpr
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
h : 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1

State before:
case succ.mpr
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
h : 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1
Tactic:
simpa[and_eq_one] using h
State after:
no goals