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

State before:
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
⊢ (p1 * p2).Coprime (q1 * q2)
Tactic:
have h1 := lemma1 hp1 hp2 hq1 hp1q1 hp2q1
State after:
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
h1 : (p1 * p2).Coprime q1
⊢ (p1 * p2).Coprime (q1 * q2)

State before:
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
h1 : (p1 * p2).Coprime q1
⊢ (p1 * p2).Coprime (q1 * q2)
Tactic:
have h2 := lemma1 hp1 hp2 hq2 hp1q2 hp2q2
State after:
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
h1 : (p1 * p2).Coprime q1
h2 : (p1 * p2).Coprime q2
⊢ (p1 * p2).Coprime (q1 * q2)

State before:
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
h1 : (p1 * p2).Coprime q1
h2 : (p1 * p2).Coprime q2
⊢ (p1 * p2).Coprime (q1 * q2)
Tactic:
exact Nat.Coprime.mul_right h1 h2
State after:
no goals