Theorem: TsumMulIte (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0
Tactic:
have h₀ : (n : ℕ) ≠ 0 := PNat.ne_zero n
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0
Tactic:
let nMul : ℕ → ℕ := (λ (m : ℕ) => (n : ℕ) * m)
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0
Tactic:
have hnMulInj := mul_right_injective₀ h₀
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0
Tactic:
have h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k) := by exact rfl
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0
Tactic:
have h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : Set.range nMul), f ↑a := by
  exact Eq.symm (tsum_range f hnMulInj)
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0
Tactic:
rw [h₁, h₂, _root_.tsum_subtype (Set.range nMul) f]
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
⊢ ∑' (x : ℕ), (Set.range nMul).indicator f x = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
h₃ : ∀ (k : ℕ), (Set.range nMul).indicator f k = if ↑↑n ∣ ↑k then f k else 0
⊢ ∑' (x : ℕ), (Set.range nMul).indicator f x = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0
Tactic:
exact tsum_congr (h₃)
State after:
no goals

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
Tactic:
exact rfl
State after:
no goals

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
⊢ ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
Tactic:
exact Eq.symm (tsum_range f hnMulInj)
State after:
no goals

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
⊢ ∀ (k : ℕ), (Set.range nMul).indicator f k = if ↑↑n ∣ ↑k then f k else 0
Tactic:
intros k
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (Set.range nMul).indicator f k = if ↑↑n ∣ ↑k then f k else 0

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (Set.range nMul).indicator f k = if ↑↑n ∣ ↑k then f k else 0
Tactic:
simp only [Set.indicator, Set.mem_range, eq_comm, Dvd.dvd, nMul]
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (if ∃ c, ↑k = ↑↑n * c then f k else 0) = if ∃ y, k = ↑n * y then f k else 0

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (if ∃ c, ↑k = ↑↑n * c then f k else 0) = if ∃ y, k = ↑n * y then f k else 0
Tactic:
congr 1
State after:
case e_c
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (∃ c, ↑k = ↑↑n * c) = ∃ y, k = ↑n * y

State before:
case e_c
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (∃ c, ↑k = ↑↑n * c) = ∃ y, k = ↑n * y
Tactic:
rw [←iff_eq_eq]
State after:
case e_c
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (∃ c, ↑k = ↑↑n * c) ↔ ∃ y, k = ↑n * y

State before:
case e_c
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (∃ c, ↑k = ↑↑n * c) ↔ ∃ y, k = ↑n * y
Tactic:
constructor
State after:
case e_c.mp
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (∃ c, ↑k = ↑↑n * c) → ∃ y, k = ↑n * y

case e_c.mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (∃ y, k = ↑n * y) → ∃ c, ↑k = ↑↑n * c

State before:
case e_c.mp
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (∃ c, ↑k = ↑↑n * c) → ∃ y, k = ↑n * y
Tactic:
intros h₀
State after:
case e_c.mp
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀✝ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
h₀ : ∃ c, ↑k = ↑↑n * c
⊢ ∃ y, k = ↑n * y

State before:
case e_c.mp
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀✝ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
h₀ : ∃ c, ↑k = ↑↑n * c
⊢ ∃ y, k = ↑n * y
Tactic:
rcases h₀ with ⟨w, hw⟩
State after:
case e_c.mp.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
⊢ ∃ y, k = ↑n * y

State before:
case e_c.mp.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
⊢ ∃ y, k = ↑n * y
Tactic:
have h₁ : ∃ (w₂ : ℕ), w = w₂ := by
  refine Int.eq_ofNat_of_zero_le ?_
  by_contra h₆
  simp only [not_le] at h₆
  have h₃ : (n : ℤ) > 0 := by
    refine Int.ofNat_pos.mpr ?_
    exact PNat.pos n
  have h₄ : ((n : ℤ) * w) < 0 := by
    exact Int.mul_neg_of_pos_of_neg h₃ h₆
  linarith
State after:
case e_c.mp.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁✝ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₁ : ∃ w₂, w = ↑w₂
⊢ ∃ y, k = ↑n * y

State before:
case e_c.mp.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁✝ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₁ : ∃ w₂, w = ↑w₂
⊢ ∃ y, k = ↑n * y
Tactic:
rcases h₁ with ⟨w₂, hw₂⟩
State after:
case e_c.mp.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
w₂ : ℕ
hw₂ : w = ↑w₂
⊢ ∃ y, k = ↑n * y

State before:
case e_c.mp.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
w₂ : ℕ
hw₂ : w = ↑w₂
⊢ ∃ y, k = ↑n * y
Tactic:
use w₂
State after:
case h
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
w₂ : ℕ
hw₂ : w = ↑w₂
⊢ k = ↑n * w₂

State before:
case h
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
w₂ : ℕ
hw₂ : w = ↑w₂
⊢ k = ↑n * w₂
Tactic:
rw [hw₂] at hw
State after:
case h
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
w₂ : ℕ
hw : ↑k = ↑↑n * ↑w₂
hw₂ : w = ↑w₂
⊢ k = ↑n * w₂

State before:
case h
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
w₂ : ℕ
hw : ↑k = ↑↑n * ↑w₂
hw₂ : w = ↑w₂
⊢ k = ↑n * w₂
Tactic:
exact Int.ofNat_inj.mp hw
State after:
no goals

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
⊢ ∃ w₂, w = ↑w₂
Tactic:
refine Int.eq_ofNat_of_zero_le ?_
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
⊢ 0 ≤ w

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
⊢ 0 ≤ w
Tactic:
by_contra h₆
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : ¬0 ≤ w
⊢ False

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : ¬0 ≤ w
⊢ False
Tactic:
simp only [not_le] at h₆
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
⊢ False

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
⊢ False
Tactic:
have h₃ : (n : ℤ) > 0 := by
  refine Int.ofNat_pos.mpr ?_
  exact PNat.pos n
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
h₃ : ↑↑n > 0
⊢ False

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
h₃ : ↑↑n > 0
⊢ False
Tactic:
have h₄ : ((n : ℤ) * w) < 0 := by
  exact Int.mul_neg_of_pos_of_neg h₃ h₆
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
h₃ : ↑↑n > 0
h₄ : ↑↑n * w < 0
⊢ False

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
h₃ : ↑↑n > 0
h₄ : ↑↑n * w < 0
⊢ False
Tactic:
linarith
State after:
no goals

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
⊢ ↑↑n > 0
Tactic:
refine Int.ofNat_pos.mpr ?_
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
⊢ 0 < ↑n

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
⊢ 0 < ↑n
Tactic:
exact PNat.pos n
State after:
no goals

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
h₃ : ↑↑n > 0
⊢ ↑↑n * w < 0
Tactic:
exact Int.mul_neg_of_pos_of_neg h₃ h₆
State after:
no goals

State before:
case e_c.mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
⊢ (∃ y, k = ↑n * y) → ∃ c, ↑k = ↑↑n * c
Tactic:
intros h₄
State after:
case e_c.mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
h₄ : ∃ y, k = ↑n * y
⊢ ∃ c, ↑k = ↑↑n * c

State before:
case e_c.mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k : ℕ
h₄ : ∃ y, k = ↑n * y
⊢ ∃ c, ↑k = ↑↑n * c
Tactic:
rcases h₄ with ⟨w,hw⟩
State after:
case e_c.mpr.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k w : ℕ
hw : k = ↑n * w
⊢ ∃ c, ↑k = ↑↑n * c

State before:
case e_c.mpr.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k w : ℕ
hw : k = ↑n * w
⊢ ∃ c, ↑k = ↑↑n * c
Tactic:
use w
State after:
case h
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k w : ℕ
hw : k = ↑n * w
⊢ ↑k = ↑↑n * ↑w

State before:
case h
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : AddCommMonoid α
f : ℕ → α
n : ℕ+
h₀ : ↑n ≠ 0
nMul : ℕ → ℕ := fun m => ↑n * m
hnMulInj : Function.Injective fun x => ↑n * x
h₁ : ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), f (nMul k)
h₂ : ∑' (k : ℕ), f (nMul k) = ∑' (a : ↑(Set.range nMul)), f ↑a
k w : ℕ
hw : k = ↑n * w
⊢ ↑k = ↑↑n * ↑w
Tactic:
simp only [Nat.cast_mul, hw]
State after:
no goals