Theorem: product_of_two_primes_neq_zero (RSAProject/rsaproject.lean)

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
⊢ p * q ≠ 0
Tactic:
have h1 : p ≠ 0 := by
  apply Nat.Prime.ne_zero hp
State after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
⊢ p * q ≠ 0

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
⊢ p * q ≠ 0
Tactic:
have h2 : q ≠ 0 := by
  apply Nat.Prime.ne_zero hq
State after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
⊢ p * q ≠ 0

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
⊢ p * q ≠ 0
Tactic:
have h3 : p*q ≠ 0 := by
  apply Nat.mul_ne_zero h1 h2
State after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
h3 : p * q ≠ 0
⊢ p * q ≠ 0

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
h3 : p * q ≠ 0
⊢ p * q ≠ 0
Tactic:
apply h3
State after:
no goals

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
⊢ p ≠ 0
Tactic:
apply Nat.Prime.ne_zero hp
State after:
no goals

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
⊢ q ≠ 0
Tactic:
apply Nat.Prime.ne_zero hq
State after:
no goals

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
⊢ p * q ≠ 0
Tactic:
apply Nat.mul_ne_zero h1 h2
State after:
no goals