Theorem: HTPI.all_prime_cons (HTPILib/Chap7.lean)

State before:
n : ℕ
L : List ℕ
⊢ all_prime (n :: L) ↔ prime n ∧ all_prime L
Tactic:
apply Iff.intro
State after:
case mp
n : ℕ
L : List ℕ
⊢ all_prime (n :: L) → prime n ∧ all_prime L

case mpr
n : ℕ
L : List ℕ
⊢ prime n ∧ all_prime L → all_prime (n :: L)

State before:
case mp
n : ℕ
L : List ℕ
⊢ all_prime (n :: L) → prime n ∧ all_prime L
Tactic:
assume h1 : all_prime (n :: L)
State after:
case mp
n : ℕ
L : List ℕ
h1 : all_prime (n :: L)
⊢ prime n ∧ all_prime L

State before:
case mp
n : ℕ
L : List ℕ
h1 : all_prime (n :: L)
⊢ prime n ∧ all_prime L
Tactic:
define at h1
State after:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ prime n ∧ all_prime L

State before:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ prime n ∧ all_prime L
Tactic:
apply And.intro (h1 n (List.mem_cons_self n L))
State after:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ all_prime L

State before:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ all_prime L
Tactic:
define
State after:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ ∀ p ∈ L, prime p

State before:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ ∀ p ∈ L, prime p
Tactic:
fix p : Nat
State after:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
p : ℕ
⊢ p ∈ L → prime p

State before:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
p : ℕ
⊢ p ∈ L → prime p
Tactic:
assume h2 : p ∈ L
State after:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
p : ℕ
h2 : p ∈ L
⊢ prime p

State before:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
p : ℕ
h2 : p ∈ L
⊢ prime p
Tactic:
show prime p from h1 p (List.mem_cons_of_mem n h2)
State after:
no goals

State before:
case mpr
n : ℕ
L : List ℕ
⊢ prime n ∧ all_prime L → all_prime (n :: L)
Tactic:
assume h1 : prime n ∧ all_prime L
State after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ all_prime L
⊢ all_prime (n :: L)

State before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ all_prime L
⊢ all_prime (n :: L)
Tactic:
define : all_prime L at h1
State after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
⊢ all_prime (n :: L)

State before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
⊢ all_prime (n :: L)
Tactic:
define
State after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
⊢ ∀ p ∈ n :: L, prime p

State before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
⊢ ∀ p ∈ n :: L, prime p
Tactic:
fix p : Nat
State after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
⊢ p ∈ n :: L → prime p

State before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
⊢ p ∈ n :: L → prime p
Tactic:
assume h2 : p ∈ n :: L
State after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p ∈ n :: L
⊢ prime p

State before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p ∈ n :: L
⊢ prime p
Tactic:
rewrite [List.mem_cons] at h2
State after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n ∨ p ∈ L
⊢ prime p

State before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n ∨ p ∈ L
⊢ prime p
Tactic:
by_cases on h2
State after:
case mpr.Case_1
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n
⊢ prime p

case mpr.Case_2
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p ∈ L
⊢ prime p

State before:
case mpr.Case_1
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n
⊢ prime p
Tactic:
rewrite [h2]
State after:
case mpr.Case_1
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n
⊢ prime n

State before:
case mpr.Case_1
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n
⊢ prime n
Tactic:
show prime n from h1.left
State after:
no goals

State before:
case mpr.Case_2
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p ∈ L
⊢ prime p
Tactic:
show prime p from h1.right p h2
State after:
no goals