Theorem: Dvd.dvd.addMultiple (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n m k : ℤ
⊢ n ∣ m ↔ n ∣ m + k * n
Tactic:
have h₁ : n ∣ (k * n) := by
  exact Int.dvd_mul_left k n
State after:
n m k : ℤ
h₁ : n ∣ k * n
⊢ n ∣ m ↔ n ∣ m + k * n

State before:
n m k : ℤ
h₁ : n ∣ k * n
⊢ n ∣ m ↔ n ∣ m + k * n
Tactic:
constructor
State after:
case mp
n m k : ℤ
h₁ : n ∣ k * n
⊢ n ∣ m → n ∣ m + k * n

case mpr
n m k : ℤ
h₁ : n ∣ k * n
⊢ n ∣ m + k * n → n ∣ m

State before:
n m k : ℤ
⊢ n ∣ k * n
Tactic:
exact Int.dvd_mul_left k n
State after:
no goals

State before:
case mp
n m k : ℤ
h₁ : n ∣ k * n
⊢ n ∣ m → n ∣ m + k * n
Tactic:
intros h₀
State after:
case mp
n m k : ℤ
h₁ : n ∣ k * n
h₀ : n ∣ m
⊢ n ∣ m + k * n

State before:
case mp
n m k : ℤ
h₁ : n ∣ k * n
h₀ : n ∣ m
⊢ n ∣ m + k * n
Tactic:
exact Dvd.dvd.add h₀ h₁
State after:
no goals

State before:
case mpr
n m k : ℤ
h₁ : n ∣ k * n
⊢ n ∣ m + k * n → n ∣ m
Tactic:
intros h₂
State after:
case mpr
n m k : ℤ
h₁ : n ∣ k * n
h₂ : n ∣ m + k * n
⊢ n ∣ m

State before:
case mpr
n m k : ℤ
h₁ : n ∣ k * n
h₂ : n ∣ m + k * n
⊢ n ∣ m
Tactic:
exact (Int.dvd_add_left h₁).mp h₂
State after:
no goals