Theorem: Imo1989P5.lemma1 (Compfiles/Imo1989P5.lean)

State before:
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
⊢ (p1 * p2).Coprime q
Tactic:
have h1 : Nat.Coprime p1 q := Iff.mpr (Nat.coprime_primes hp1 hq) hp1q
State after:
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
h1 : p1.Coprime q
⊢ (p1 * p2).Coprime q

State before:
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
h1 : p1.Coprime q
⊢ (p1 * p2).Coprime q
Tactic:
have h2 : Nat.Coprime p2 q := Iff.mpr (Nat.coprime_primes hp2 hq) hp2q
State after:
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
h1 : p1.Coprime q
h2 : p2.Coprime q
⊢ (p1 * p2).Coprime q

State before:
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
h1 : p1.Coprime q
h2 : p2.Coprime q
⊢ (p1 * p2).Coprime q
Tactic:
exact Nat.Coprime.mul h1 h2
State after:
no goals