internlm/Lean-Github huggingface dataset:
Theorem: RuesRealToReal
Proof state before:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = ∑' (z : ℕ), 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0
Tactic:
rw [tsum_zero] at h₁
Proof state after:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0
Theorem: RuesRealToReal
Proof state before:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0
Tactic:
rw [←h₁]
Proof state after:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial
Theorem: RuesRealToReal
Proof state before:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial
Tactic:
simp only [div_natCast_im]
Proof state after:
no goals
Theorem: RuesRotationallySymmetric
Proof state before:
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
⊢ Rues n z = Rues n (z * rou)
Tactic:
simp_rw [Rues]
Proof state after:
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
⊢ ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial = ∑' (k : ℕ), (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Theorem: RuesRotationallySymmetric
Proof state before:
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
⊢ ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial = ∑' (k : ℕ), (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
congr
Proof state after:
case e_f
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
⊢ (fun k => z ^ (↑n * k) / ↑(↑n * k).factorial) = fun k => (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Theorem: RuesRotationallySymmetric
Proof state before:
case e_f
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
⊢ (fun k => z ^ (↑n * k) / ↑(↑n * k).factorial) = fun k => (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
ext1 k
Proof state after:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Theorem: RuesRotationallySymmetric
Proof state before:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
have h₀ : (z * rou) ^ (n * k) = z ^ (n * k) * rou ^ (n * k) := by
  exact mul_pow z rou (↑n * k)
Proof state after:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Theorem: RuesRotationallySymmetric
Proof state before:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
have h₁ : rou ^ (n * k) = (rou ^ (n : ℕ)) ^ k := by
  exact pow_mul rou (↑n) k
Proof state after:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
h₁ : rou ^ (↑n * k) = (rou ^ ↑n) ^ k
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Theorem: RuesRotationallySymmetric
Proof state before:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
h₁ : rou ^ (↑n * k) = (rou ^ ↑n) ^ k
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
simp only [h₀, h₁, h, one_pow, mul_one]
Proof state after:
no goals
Theorem: RuesRotationallySymmetric
Proof state before:
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
Tactic:
exact mul_pow z rou (↑n * k)
Proof state after:
no goals
Theorem: RuesRotationallySymmetric
Proof state before:
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
⊢ rou ^ (↑n * k) = (rou ^ ↑n) ^ k
Tactic:
exact pow_mul rou (↑n) k
Proof state after:
no goals
Theorem: RouNot0
Proof state before:
n : ℕ+
rou : ℂ
h : rou ^ ↑n = 1
⊢ rou ≠ 0
Tactic:
by_contra h₁
Proof state after:
n : ℕ+
rou : ℂ
h : rou ^ ↑n = 1
h₁ : rou = 0
⊢ False
Theorem: RouNot0
Proof state before:
n : ℕ+
rou : ℂ
h : rou ^ ↑n = 1
h₁ : rou = 0
⊢ False
Tactic:
rw [h₁] at h
Proof state after:
n : ℕ+
rou : ℂ
h : 0 ^ ↑n = 1
h₁ : rou = 0
⊢ False
Theorem: RouNot0
Proof state before:
n : ℕ+
rou : ℂ
h : 0 ^ ↑n = 1
h₁ : rou = 0
⊢ False
Tactic:
simp only [ne_eq, PNat.ne_zero, not_false_eq_true, zero_pow, zero_ne_one] at h
Proof state after:
no goals
Theorem: RuesDiffSummable
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ Summable fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0
Tactic:
sorry
Proof state after:
no goals
Theorem: RuesDiffHasDeriv
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ HasDerivAt (RuesDiff n m) (RuesDiff n (m + 1) z) z
Tactic:
sorry
Proof state after:
no goals
Theorem: RuesDiffDeriv
Proof state before:
n : ℕ+
m : ℤ
⊢ deriv (RuesDiff n m) = RuesDiff n (m + 1)
Tactic:
sorry
Proof state after:
no goals
Theorem: RuesDiffIteratedDeriv
Proof state before:
k : ℕ
n : ℕ+
m : ℤ
⊢ iteratedDeriv k (RuesDiff n m) = RuesDiff n (↑k + m)
Tactic:
induction' k with K Kih
Proof state after:
case zero
n : ℕ+
m : ℤ
⊢ iteratedDeriv 0 (RuesDiff n m) = RuesDiff n (↑0 + m)

case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
⊢ iteratedDeriv (K + 1) (RuesDiff n m) = RuesDiff n (↑(K + 1) + m)
Theorem: RuesDiffIteratedDeriv
Proof state before:
case zero
n : ℕ+
m : ℤ
⊢ iteratedDeriv 0 (RuesDiff n m) = RuesDiff n (↑0 + m)
Tactic:
simp only [Nat.zero_eq, iteratedDeriv_zero, CharP.cast_eq_zero, zero_add]
Proof state after:
no goals
Theorem: RuesDiffIteratedDeriv
Proof state before:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
⊢ iteratedDeriv (K + 1) (RuesDiff n m) = RuesDiff n (↑(K + 1) + m)
Tactic:
have h₀ := congrArg deriv Kih
Proof state after:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ iteratedDeriv (K + 1) (RuesDiff n m) = RuesDiff n (↑(K + 1) + m)
Theorem: RuesDiffIteratedDeriv
Proof state before:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ iteratedDeriv (K + 1) (RuesDiff n m) = RuesDiff n (↑(K + 1) + m)
Tactic:
rw [iteratedDeriv_succ, h₀, RuesDiffDeriv]
Proof state after:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ RuesDiff n (↑K + m + 1) = RuesDiff n (↑(K + 1) + m)
Theorem: RuesDiffIteratedDeriv
Proof state before:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ RuesDiff n (↑K + m + 1) = RuesDiff n (↑(K + 1) + m)
Tactic:
have h₁ : ↑K + m + 1 = ↑(Nat.succ K) + m := by
  simp only [Nat.cast_succ]
  ring
Proof state after:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
h₁ : ↑K + m + 1 = ↑K.succ + m
⊢ RuesDiff n (↑K + m + 1) = RuesDiff n (↑(K + 1) + m)
Theorem: RuesDiffIteratedDeriv
Proof state before:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
h₁ : ↑K + m + 1 = ↑K.succ + m
⊢ RuesDiff n (↑K + m + 1) = RuesDiff n (↑(K + 1) + m)
Tactic:
rw [h₁]
Proof state after:
no goals
Theorem: RuesDiffIteratedDeriv
Proof state before:
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ ↑K + m + 1 = ↑K.succ + m
Tactic:
simp only [Nat.cast_succ]
Proof state after:
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ ↑K + m + 1 = ↑K + 1 + m
Theorem: RuesDiffIteratedDeriv
Proof state before:
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ ↑K + m + 1 = ↑K + 1 + m
Tactic:
ring
Proof state after:
no goals
Theorem: TsumMulIte
Proof 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
Proof 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
Theorem: TsumMulIte
Proof 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)
Proof 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
Theorem: TsumMulIte
Proof 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₀
Proof 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
Theorem: TsumMulIte
Proof 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
Proof 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
Theorem: TsumMulIte
Proof 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)
Proof 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
Theorem: TsumMulIte
Proof 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]
Proof 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
Theorem: TsumMulIte
Proof 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₃)
Proof state after:
no goals
Theorem: TsumMulIte
Proof 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
Proof state after:
no goals
Theorem: TsumMulIte
Proof 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)
Proof state after:
no goals
Theorem: TsumMulIte
Proof 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
Proof 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
Theorem: TsumMulIte
Proof 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]
Proof 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
Theorem: TsumMulIte
Proof 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
Proof 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
Theorem: TsumMulIte
Proof 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]
Proof 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
Theorem: TsumMulIte
Proof 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
Proof 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
Theorem: TsumMulIte
Proof 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₀
Proof 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
Theorem: TsumMulIte
Proof 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⟩
Proof 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
Theorem: TsumMulIte
Proof 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
Proof 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
Theorem: TsumMulIte
Proof 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₂⟩
Proof 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
Theorem: TsumMulIte
Proof 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₂
Proof 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₂