Theorem: SelbergSieve.eq_gcd_mul_of_dvd_of_coprime (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean)

State before:
s : SelbergSieve
k d m : ℕ
hkd : k ∣ d
hmd : m.Coprime d
hk : k ≠ 0
⊢ k = d.gcd (k * m)
Tactic:
cases' hkd with r hr
State after:
case intro
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ k = d.gcd (k * m)

State before:
case intro
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ k = d.gcd (k * m)
Tactic:
have hrdvd : r ∣ d := by use k; rw [mul_comm]; exact hr
State after:
case intro
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ k = d.gcd (k * m)

State before:
case intro
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ k = d.gcd (k * m)
Tactic:
apply symm
State after:
case intro.a
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ d.gcd (k * m) = k

State before:
case intro.a
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ d.gcd (k * m) = k
Tactic:
rw [hr, Nat.gcd_mul_left, mul_eq_left₀ hk, Nat.gcd_comm]
State after:
case intro.a
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ m.gcd r = 1

State before:
case intro.a
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ m.gcd r = 1
Tactic:
apply Coprime.coprime_dvd_right hrdvd hmd
State after:
no goals

State before:
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ r ∣ d
Tactic:
use k
State after:
case h
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ d = r * k

State before:
case h
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ d = r * k
Tactic:
rw [mul_comm]
State after:
case h
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ d = k * r

State before:
case h
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ d = k * r
Tactic:
exact hr
State after:
no goals