Theorem: RuesDiffSumOfRuesDiff (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n k : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z = ∑ k₀ ∈ range ↑k, RuesDiff (n * k) (↑↑n * ↑k₀ + m) z
Tactic:
simp_rw [RuesDiff]
State after:
n k : ℕ+
m : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑ x ∈ range ↑k, ∑' (k_1 : ℕ), if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0

State before:
n k : ℕ+
m : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑ x ∈ range ↑k, ∑' (k_1 : ℕ), if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
have h₀ : ∀ x ∈ range k, Summable (λ (k_1 : ℕ) => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0) := by
  intros x _
  exact RuesDiffSummable (n * k) _ z
State after:
n k : ℕ+
m : ℤ
z : ℂ
h₀ : ∀ x ∈ range ↑k, Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑ x ∈ range ↑k, ∑' (k_1 : ℕ), if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0

State before:
n k : ℕ+
m : ℤ
z : ℂ
h₀ : ∀ x ∈ range ↑k, Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑ x ∈ range ↑k, ∑' (k_1 : ℕ), if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
rw [← tsum_sum h₀]
State after:
n k : ℕ+
m : ℤ
z : ℂ
h₀ : ∀ x ∈ range ↑k, Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (b : ℕ), ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0

State before:
n k : ℕ+
m : ℤ
z : ℂ
h₀ : ∀ x ∈ range ↑k, Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (b : ℕ), ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0
Tactic:
clear h₀
State after:
n k : ℕ+
m : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (b : ℕ), ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0

State before:
n k : ℕ+
m : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (b : ℕ), ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0
Tactic:
congr
State after:
case e_f
n k : ℕ+
m : ℤ
z : ℂ
⊢ (fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = fun b =>
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0

State before:
case e_f
n k : ℕ+
m : ℤ
z : ℂ
⊢ (fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = fun b =>
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0
Tactic:
ext1 x
State after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0

State before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
let f₀ : ℕ → Prop := (λ (i : ℕ) => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m))
State after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0

State before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
have h₁ : ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j := by
  intros i hir j hjr hi hj
  simp [f₀] at hi hj
  simp only [mem_range] at hir hjr
  clear f₀ z
  rw [←Int.modEq_zero_iff_dvd] at hi hj
  have h₀ := Int.ModEq.sub hi hj
  simp only [add_sub_add_left_eq_sub, add_sub_add_right_eq_sub, sub_self] at h₀
  clear hi hj
  rw [Int.modEq_zero_iff_dvd, (show (↑↑n * ↑i - ↑↑n * ↑j : ℤ) = ↑↑n * (↑i - ↑j) by ring)] at h₀
  have h₁ : (n : ℤ) ≠ 0 := by
    exact Ne.symm (NeZero.ne' (n : ℤ))
  have h₂ : (k : ℤ) ∣ ↑i - ↑j := by exact (mul_dvd_mul_iff_left h₁).mp h₀
  obtain ⟨y, h₃⟩ := h₂
  have h₄ : k * y < k := by
    linarith
  have h₅ : -k < k * y := by
    linarith
  have h₆ : (k : ℤ) > 0 := by
    linarith
  have h₇ : y < 1 := by
    exact (mul_lt_iff_lt_one_right h₆).mp h₄
  nth_rw 1 [(show -(k : ℤ) = ↑↑k * -1 by ring)] at h₅
  have h₈ : -1 < y := by
    exact (mul_lt_mul_left h₆).mp h₅
  have h₉ : y = 0 := by
    linarith
  rw [h₉] at h₃
  simp only [mul_zero] at h₃
  clear n hir hjr m h₀ h₁ h₄ h₅ h₆ h₇ h₈ h₉ y x k
  refine Int.ofNat_inj.mp ?intro.a
  have h₀ := congrArg (λ (k : ℤ) => k + j) h₃
  simp only [sub_add_cancel, zero_add] at h₀
  exact h₀
State after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₁ : ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0

State before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₁ : ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
have h₂ := Finset.sum_ite_zero (range ↑k) f₀ h₁ (z ^ x / ↑x.factorial)
State after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₁ : ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j
h₂ :
  (∑ i ∈ range ↑k, if f₀ i then z ^ x / ↑x.factorial else 0) = if ∃ i ∈ range ↑k, f₀ i then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0

State before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₁ : ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j
h₂ :
  (∑ i ∈ range ↑k, if f₀ i then z ^ x / ↑x.factorial else 0) = if ∃ i ∈ range ↑k, f₀ i then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
clear h₁
State after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ i ∈ range ↑k, if f₀ i then z ^ x / ↑x.factorial else 0) = if ∃ i ∈ range ↑k, f₀ i then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0

State before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ i ∈ range ↑k, if f₀ i then z ^ x / ↑x.factorial else 0) = if ∃ i ∈ range ↑k, f₀ i then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
simp only [PNat.mul_coe, Nat.cast_mul, mem_range, f₀] at h₂ ⊢
State after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0

State before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0
Tactic:
rw [h₂]
State after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0

State before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
clear h₂ f₀
State after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0

State before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
congr
State after:
case e_f.h.e_c
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (↑↑n ∣ ↑x + m) = ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)

State before:
case e_f.h.e_c
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (↑↑n ∣ ↑x + m) = ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
rw [←iff_eq_eq]
State after:
case e_f.h.e_c
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ ↑↑n ∣ ↑x + m ↔ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)

State before:
case e_f.h.e_c
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ ↑↑n ∣ ↑x + m ↔ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
constructor
State after:
case e_f.h.e_c.mp
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ ↑↑n ∣ ↑x + m → ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)

case e_f.h.e_c.mpr
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)) → ↑↑n ∣ ↑x + m

State before:
n k : ℕ+
m : ℤ
z : ℂ
⊢ ∀ x ∈ range ↑k, Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
intros x _
State after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
a✝ : x ∈ range ↑k
⊢ Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0

State before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
a✝ : x ∈ range ↑k
⊢ Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
exact RuesDiffSummable (n * k) _ z
State after:
no goals

State before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
⊢ ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j
Tactic:
intros i hir j hjr hi hj
State after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i : ℕ
hir : i ∈ range ↑k
j : ℕ
hjr : j ∈ range ↑k
hi : f₀ i
hj : f₀ j
⊢ i = j

State before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i : ℕ
hir : i ∈ range ↑k
j : ℕ
hjr : j ∈ range ↑k
hi : f₀ i
hj : f₀ j
⊢ i = j
Tactic:
simp [f₀] at hi hj
State after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i : ℕ
hir : i ∈ range ↑k
j : ℕ
hjr : j ∈ range ↑k
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
⊢ i = j

State before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i : ℕ
hir : i ∈ range ↑k
j : ℕ
hjr : j ∈ range ↑k
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
⊢ i = j
Tactic:
simp only [mem_range] at hir hjr
State after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i j : ℕ
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
hir : i < ↑k
hjr : j < ↑k
⊢ i = j

State before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i j : ℕ
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
hir : i < ↑k
hjr : j < ↑k
⊢ i = j
Tactic:
clear f₀ z
State after:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
hir : i < ↑k
hjr : j < ↑k
⊢ i = j

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
hir : i < ↑k
hjr : j < ↑k
⊢ i = j
Tactic:
rw [←Int.modEq_zero_iff_dvd] at hi hj
State after:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
⊢ i = j

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
⊢ i = j
Tactic:
have h₀ := Int.ModEq.sub hi hj
State after:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑x + (↑↑n * ↑i + m) - (↑x + (↑↑n * ↑j + m)) ≡ 0 - 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑x + (↑↑n * ↑i + m) - (↑x + (↑↑n * ↑j + m)) ≡ 0 - 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j
Tactic:
simp only [add_sub_add_left_eq_sub, add_sub_add_right_eq_sub, sub_self] at h₀
State after:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑i - ↑↑n * ↑j ≡ 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑i - ↑↑n * ↑j ≡ 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j
Tactic:
clear hi hj
State after:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑i - ↑↑n * ↑j ≡ 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑i - ↑↑n * ↑j ≡ 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j
Tactic:
rw [Int.modEq_zero_iff_dvd, (show (↑↑n * ↑i - ↑↑n * ↑j : ℤ) = ↑↑n * (↑i - ↑j) by ring)] at h₀
State after:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
⊢ i = j

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
⊢ i = j
Tactic:
have h₁ : (n : ℤ) ≠ 0 := by
  exact Ne.symm (NeZero.ne' (n : ℤ))
State after:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
⊢ i = j

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
⊢ i = j
Tactic:
have h₂ : (k : ℤ) ∣ ↑i - ↑j := by exact (mul_dvd_mul_iff_left h₁).mp h₀
State after:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
h₂ : ↑↑k ∣ ↑i - ↑j
⊢ i = j

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
h₂ : ↑↑k ∣ ↑i - ↑j
⊢ i = j
Tactic:
obtain ⟨y, h₃⟩ := h₂
State after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
⊢ i = j

State before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
⊢ i = j
Tactic:
have h₄ : k * y < k := by
  linarith
State after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
⊢ i = j

State before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
⊢ i = j
Tactic:
have h₅ : -k < k * y := by
  linarith
State after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
⊢ i = j

State before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
⊢ i = j
Tactic:
have h₆ : (k : ℤ) > 0 := by
  linarith
State after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
⊢ i = j

State before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
⊢ i = j
Tactic:
have h₇ : y < 1 := by
  exact (mul_lt_iff_lt_one_right h₆).mp h₄
State after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ i = j

State before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ i = j
Tactic:
nth_rw 1 [(show -(k : ℤ) = ↑↑k * -1 by ring)] at h₅
State after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ i = j

State before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ i = j
Tactic:
have h₈ : -1 < y := by
  exact (mul_lt_mul_left h₆).mp h₅
State after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
⊢ i = j

State before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
⊢ i = j
Tactic:
have h₉ : y = 0 := by
  linarith
State after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
⊢ i = j

State before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
⊢ i = j
Tactic:
rw [h₉] at h₃
State after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * 0
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
⊢ i = j

State before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * 0
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
⊢ i = j
Tactic:
simp only [mul_zero] at h₃
State after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
h₃ : ↑i - ↑j = 0
⊢ i = j

State before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
h₃ : ↑i - ↑j = 0
⊢ i = j
Tactic:
clear n hir hjr m h₀ h₁ h₄ h₅ h₆ h₇ h₈ h₉ y x k
State after:
case intro
i j : ℕ
h₃ : ↑i - ↑j = 0
⊢ i = j

State before:
case intro
i j : ℕ
h₃ : ↑i - ↑j = 0
⊢ i = j
Tactic:
refine Int.ofNat_inj.mp ?intro.a
State after:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
⊢ ↑i = ↑j

State before:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
⊢ ↑i = ↑j
Tactic:
have h₀ := congrArg (λ (k : ℤ) => k + j) h₃
State after:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
h₀ : (fun k => k + ↑j) (↑i - ↑j) = (fun k => k + ↑j) 0
⊢ ↑i = ↑j

State before:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
h₀ : (fun k => k + ↑j) (↑i - ↑j) = (fun k => k + ↑j) 0
⊢ ↑i = ↑j
Tactic:
simp only [sub_add_cancel, zero_add] at h₀
State after:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
h₀ : ↑i = ↑j
⊢ ↑i = ↑j

State before:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
h₀ : ↑i = ↑j
⊢ ↑i = ↑j
Tactic:
exact h₀
State after:
no goals

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * ↑i - ↑↑n * ↑j
⊢ ↑↑n * ↑i - ↑↑n * ↑j = ↑↑n * (↑i - ↑j)
Tactic:
ring
State after:
no goals

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
⊢ ↑↑n ≠ 0
Tactic:
exact Ne.symm (NeZero.ne' (n : ℤ))
State after:
no goals

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
⊢ ↑↑k ∣ ↑i - ↑j
Tactic:
exact (mul_dvd_mul_iff_left h₁).mp h₀
State after:
no goals

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
⊢ ↑↑k * y < ↑↑k
Tactic:
linarith
State after:
no goals

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
⊢ -↑↑k < ↑↑k * y
Tactic:
linarith
State after:
no goals

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
⊢ ↑↑k > 0
Tactic:
linarith
State after:
no goals

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
⊢ y < 1
Tactic:
exact (mul_lt_iff_lt_one_right h₆).mp h₄
State after:
no goals

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ -↑↑k = ↑↑k * -1
Tactic:
ring
State after:
no goals

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ -1 < y
Tactic:
exact (mul_lt_mul_left h₆).mp h₅
State after:
no goals

State before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
⊢ y = 0
Tactic:
linarith
State after:
no goals

State before:
case e_f.h.e_c.mp
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ ↑↑n ∣ ↑x + m → ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
intros h₀
State after:
case e_f.h.e_c.mp
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
h₀ : ↑↑n ∣ ↑x + m
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)

State before:
case e_f.h.e_c.mp
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
h₀ : ↑↑n ∣ ↑x + m
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
obtain ⟨w, h₁⟩ := h₀
State after:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)

State before:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
have h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + (↑↑n * ↑i) := by
  intros i
  ring_nf
State after:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)

State before:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
simp_rw [h₂, h₁]
State after:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑i

State before:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑i
Tactic:
use ((-w) % k).toNat
State after:
case h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ (-w % ↑↑k).toNat < ↑k ∧ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat

State before:
case h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ (-w % ↑↑k).toNat < ↑k ∧ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat
Tactic:
constructor
State after:
case h.left
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ (-w % ↑↑k).toNat < ↑k

case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat

State before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
⊢ ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
Tactic:
intros i
State after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
i : ℕ
⊢ ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i

State before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
i : ℕ
⊢ ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
Tactic:
ring_nf
State after:
no goals

State before:
case h.left
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ (-w % ↑↑k).toNat < ↑k
Tactic:
refine (Int.toNat_lt' ?h.left.hn).mpr ?h.left.a
State after:
case h.left.hn
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑k ≠ 0

case h.left.a
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ -w % ↑↑k < ↑↑k

State before:
case h.left.hn
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑k ≠ 0
Tactic:
exact PNat.ne_zero k
State after:
no goals

State before:
case h.left.a
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ -w % ↑↑k < ↑↑k
Tactic:
refine Int.emod_lt_of_pos (-w) ?h.left.a.H
State after:
case h.left.a.H
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 < ↑↑k

State before:
case h.left.a.H
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 < ↑↑k
Tactic:
refine Int.ofNat_pos.mpr ?h.left.a.H.a
State after:
case h.left.a.H.a
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 < ↑k

State before:
case h.left.a.H.a
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 < ↑k
Tactic:
exact PNat.pos k
State after:
no goals

State before:
case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat
Tactic:
have h₃ : ↑(-w % ↑↑k).toNat = (-w % ↑↑k) := by
  refine Int.toNat_of_nonneg ?_
  refine Int.emod_nonneg (-w) ?_
  exact Ne.symm (NeZero.ne' (k : ℤ))
State after:
case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
h₃ : ↑(-w % ↑↑k).toNat = -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat

State before:
case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
h₃ : ↑(-w % ↑↑k).toNat = -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat
Tactic:
rw [h₃]
State after:
case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
h₃ : ↑(-w % ↑↑k).toNat = -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)

State before:
case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
h₃ : ↑(-w % ↑↑k).toNat = -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Tactic:
clear h₁ h₂ h₃ m z x
State after:
case h.right
n k : ℕ+
w : ℤ
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)

State before:
case h.right
n k : ℕ+
w : ℤ
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Tactic:
suffices h₀ : ↑↑k ∣ w + (-w % ↑↑k)
State after:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)

case h₀
n k : ℕ+
w : ℤ
⊢ ↑↑k ∣ w + -w % ↑↑k

State before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑(-w % ↑↑k).toNat = -w % ↑↑k
Tactic:
refine Int.toNat_of_nonneg ?_
State after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 ≤ -w % ↑↑k

State before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 ≤ -w % ↑↑k
Tactic:
refine Int.emod_nonneg (-w) ?_
State after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑↑k ≠ 0

State before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑↑k ≠ 0
Tactic:
exact Ne.symm (NeZero.ne' (k : ℤ))
State after:
no goals

State before:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Tactic:
have h₁ := mul_dvd_mul_left (n : ℤ) h₀
State after:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
h₁ : ↑↑n * ↑↑k ∣ ↑↑n * (w + -w % ↑↑k)
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)

State before:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
h₁ : ↑↑n * ↑↑k ∣ ↑↑n * (w + -w % ↑↑k)
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Tactic:
ring_nf at *
State after:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
h₁ : ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)

State before:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
h₁ : ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Tactic:
exact h₁
State after:
no goals

State before:
case h₀
n k : ℕ+
w : ℤ
⊢ ↑↑k ∣ w + -w % ↑↑k
Tactic:
refine Int.dvd_of_emod_eq_zero ?h₀.H
State after:
case h₀.H
n k : ℕ+
w : ℤ
⊢ (w + -w % ↑↑k) % ↑↑k = 0

State before:
case h₀.H
n k : ℕ+
w : ℤ
⊢ (w + -w % ↑↑k) % ↑↑k = 0
Tactic:
have h₀ : (0 : ℤ) = 0 % k := by
  exact rfl
State after:
case h₀.H
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ (w + -w % ↑↑k) % ↑↑k = 0

State before:
case h₀.H
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ (w + -w % ↑↑k) % ↑↑k = 0
Tactic:
rw [h₀]
State after:
case h₀.H
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ (w + -w % ↑↑k) % ↑↑k = 0 % ↑↑k

State before:
case h₀.H
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ (w + -w % ↑↑k) % ↑↑k = 0 % ↑↑k
Tactic:
refine Eq.symm (Int.ModEq.eq ?h₀.H.a)
State after:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]

State before:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Tactic:
have h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k] := by
  exact Int.mod_modEq (-w) ↑↑k
State after:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]

State before:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Tactic:
have h₂ : w ≡ w [ZMOD ↑↑k] := by exact rfl
State after:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]

State before:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Tactic:
have h₃ := Int.ModEq.add h₂ h₁
State after:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
h₃ : w + -w % ↑↑k ≡ w + -w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]

State before:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
h₃ : w + -w % ↑↑k ≡ w + -w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Tactic:
simp only [add_right_neg] at h₃
State after:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
h₃ : w + -w % ↑↑k ≡ 0 [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]

State before:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
h₃ : w + -w % ↑↑k ≡ 0 [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Tactic:
exact h₃.symm
State after:
no goals

State before:
n k : ℕ+
w : ℤ
⊢ 0 = 0 % ↑↑k
Tactic:
exact rfl
State after:
no goals

State before:
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ -w % ↑↑k ≡ -w [ZMOD ↑↑k]
Tactic:
exact Int.mod_modEq (-w) ↑↑k
State after:
no goals

State before:
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
⊢ w ≡ w [ZMOD ↑↑k]
Tactic:
exact rfl
State after:
no goals

State before:
case e_f.h.e_c.mpr
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)) → ↑↑n ∣ ↑x + m
Tactic:
intros h₀
State after:
case e_f.h.e_c.mpr
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
h₀ : ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
⊢ ↑↑n ∣ ↑x + m

State before:
case e_f.h.e_c.mpr
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
h₀ : ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
⊢ ↑↑n ∣ ↑x + m
Tactic:
obtain ⟨w, _, h₂⟩ := h₀
State after:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
⊢ ↑↑n ∣ ↑x + m

State before:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
⊢ ↑↑n ∣ ↑x + m
Tactic:
have h₃ := dvd_of_mul_right_dvd h₂
State after:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
⊢ ↑↑n ∣ ↑x + m

State before:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
⊢ ↑↑n ∣ ↑x + m
Tactic:
have h₄ : (n : ℤ) ∣ ↑↑n * ↑w := by exact Int.dvd_mul_right (↑n) w
State after:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
h₄ : ↑↑n ∣ ↑↑n * ↑w
⊢ ↑↑n ∣ ↑x + m

State before:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
h₄ : ↑↑n ∣ ↑↑n * ↑w
⊢ ↑↑n ∣ ↑x + m
Tactic:
rw [(show ↑x + (↑↑n * ↑w + m) = ↑↑n * ↑w + ↑(x + m) by ring_nf)] at h₃
State after:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑↑n * ↑w + (↑x + m)
h₄ : ↑↑n ∣ ↑↑n * ↑w
⊢ ↑↑n ∣ ↑x + m

State before:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑↑n * ↑w + (↑x + m)
h₄ : ↑↑n ∣ ↑↑n * ↑w
⊢ ↑↑n ∣ ↑x + m
Tactic:
exact (Int.dvd_iff_dvd_of_dvd_add h₃).mp h₄
State after:
no goals

State before:
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
⊢ ↑↑n ∣ ↑↑n * ↑w
Tactic:
exact Int.dvd_mul_right (↑n) w
State after:
no goals

State before:
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
h₄ : ↑↑n ∣ ↑↑n * ↑w
⊢ ↑x + (↑↑n * ↑w + m) = ↑↑n * ↑w + (↑x + m)
Tactic:
ring_nf
State after:
no goals