internlm/Lean-Github huggingface dataset:
Theorem: TsumMulIte
Proof 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
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 : ℤ
w₂ : ℕ
hw : ↑k = ↑↑n * ↑w₂
hw₂ : w = ↑w₂
⊢ k = ↑n * w₂
Theorem: TsumMulIte
Proof 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
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
⊢ ∃ w₂, w = ↑w₂
Tactic:
refine Int.eq_ofNat_of_zero_le ?_
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
⊢ 0 ≤ w
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
⊢ 0 ≤ w
Tactic:
by_contra 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
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
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : ¬0 ≤ w
⊢ False
Tactic:
simp only [not_le] at 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
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
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
⊢ False
Tactic:
have h₃ : (n : ℤ) > 0 := by
  refine Int.ofNat_pos.mpr ?_
  exact PNat.pos n
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
h₃ : ↑↑n > 0
⊢ False
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 : ℕ
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₆
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
h₃ : ↑↑n > 0
h₄ : ↑↑n * w < 0
⊢ False
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
h₃ : ↑↑n > 0
h₄ : ↑↑n * w < 0
⊢ False
Tactic:
linarith
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
⊢ ↑↑n > 0
Tactic:
refine Int.ofNat_pos.mpr ?_
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
⊢ 0 < ↑n
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 : ℕ
w : ℤ
hw : ↑k = ↑↑n * w
h₆ : w < 0
⊢ 0 < ↑n
Tactic:
exact PNat.pos n
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 : ℕ
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₆
Proof state after:
no goals
Theorem: TsumMulIte
Proof 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₄
Proof 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
Theorem: TsumMulIte
Proof 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⟩
Proof 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
Theorem: TsumMulIte
Proof 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
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
⊢ ↑k = ↑↑n * ↑w
Theorem: TsumMulIte
Proof 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]
Proof state after:
no goals
Theorem: NeedZeroCoeff
Proof state before:
f : ℕ → ℂ
n : ℕ+
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0
Tactic:
exact TsumMulIte _
Proof state after:
no goals
Theorem: RuesDiffM0EqualsRues
Proof state before:
n : ℕ+
⊢ RuesDiff n 0 = Rues n
Tactic:
ext1 z
Proof state after:
case h
n : ℕ+
z : ℂ
⊢ RuesDiff n 0 z = Rues n z
Theorem: RuesDiffM0EqualsRues
Proof state before:
case h
n : ℕ+
z : ℂ
⊢ RuesDiff n 0 z = Rues n z
Tactic:
rw [Rues, RuesDiff]
Proof state after:
case h
n : ℕ+
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + 0 then z ^ k / ↑k.factorial else 0) = ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial
Theorem: RuesDiffM0EqualsRues
Proof state before:
case h
n : ℕ+
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + 0 then z ^ k / ↑k.factorial else 0) = ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
simp only [add_zero]
Proof state after:
case h
n : ℕ+
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k then z ^ k / ↑k.factorial else 0) = ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial
Theorem: RuesDiffM0EqualsRues
Proof state before:
case h
n : ℕ+
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k then z ^ k / ↑k.factorial else 0) = ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
rw [NeedZeroCoeff (λ (k : ℕ) => z ^ k / (Nat.factorial k)) n]
Proof state after:
no goals
Theorem: RuesDiffRotationallySymmetric
Proof state before:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
⊢ RuesDiff n m (z * rou) = rou ^ (-m) * RuesDiff n m z
Tactic:
simp_rw [RuesDiff, ←tsum_mul_left]
Proof state after:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    ∑' (x : ℕ), rou ^ (-m) * if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0
Theorem: RuesDiffRotationallySymmetric
Proof state before:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    ∑' (x : ℕ), rou ^ (-m) * if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0
Tactic:
congr
Proof state after:
case e_f
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
⊢ (fun k => if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) = fun x =>
    rou ^ (-m) * if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case e_f
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
⊢ (fun k => if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) = fun x =>
    rou ^ (-m) * if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0
Tactic:
ext1 k
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    rou ^ (-m) * if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    rou ^ (-m) * if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0
Tactic:
simp only [zpow_neg, mul_ite, mul_zero]
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Tactic:
have h₀ := Classical.em (↑↑n ∣ ↑k + m)
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : ↑↑n ∣ ↑k + m ∨ ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : ↑↑n ∣ ↑k + m ∨ ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Tactic:
rcases h₀ with h₀a | h₀b
Proof state after:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0

case e_f.h.inr
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀b : ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Tactic:
simp_rw [if_pos h₀a]
Proof state after:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ (z * rou) ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ (z * rou) ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Tactic:
rw [mul_pow z rou k]
Proof state after:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ z ^ k * rou ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ z ^ k * rou ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Tactic:
have h₁ : rou ^ k = (rou ^ m)⁻¹ := by
  obtain ⟨k₂, kmDiv⟩ := h₀a
  have h₂ : rou ^ (↑k + m) = 1 := by
    rw [kmDiv, zpow_mul]
    simp only [zpow_natCast, h, one_zpow]
  have h₃ := congrArg (λ (z₀ : ℂ) => z₀ * (rou ^ m)⁻¹) h₂
  simp only [one_mul, ne_eq, inv_eq_zero] at h₃
  have h₄ := RouNot0 n rou h
  rw [zpow_add₀ h₄ ↑k m] at h₃
  rw [←h₃]
  have h₅ : rou ^ m ≠ 0 := by
    exact zpow_ne_zero m h₄
  field_simp
Proof state after:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
h₁ : rou ^ k = (rou ^ m)⁻¹
⊢ z ^ k * rou ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
h₁ : rou ^ k = (rou ^ m)⁻¹
⊢ z ^ k * rou ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Tactic:
rw [h₁]
Proof state after:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
h₁ : rou ^ k = (rou ^ m)⁻¹
⊢ z ^ k * (rou ^ m)⁻¹ / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
h₁ : rou ^ k = (rou ^ m)⁻¹
⊢ z ^ k * (rou ^ m)⁻¹ / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Tactic:
ring
Proof state after:
no goals
Theorem: RuesDiffRotationallySymmetric
Proof state before:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
obtain ⟨k₂, kmDiv⟩ := h₀a
Proof state after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
⊢ rou ^ k = (rou ^ m)⁻¹
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
have h₂ : rou ^ (↑k + m) = 1 := by
  rw [kmDiv, zpow_mul]
  simp only [zpow_natCast, h, one_zpow]
Proof state after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
⊢ rou ^ k = (rou ^ m)⁻¹
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
have h₃ := congrArg (λ (z₀ : ℂ) => z₀ * (rou ^ m)⁻¹) h₂
Proof state after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : (fun z₀ => z₀ * (rou ^ m)⁻¹) (rou ^ (↑k + m)) = (fun z₀ => z₀ * (rou ^ m)⁻¹) 1
⊢ rou ^ k = (rou ^ m)⁻¹
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : (fun z₀ => z₀ * (rou ^ m)⁻¹) (rou ^ (↑k + m)) = (fun z₀ => z₀ * (rou ^ m)⁻¹) 1
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
simp only [one_mul, ne_eq, inv_eq_zero] at h₃
Proof state after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ (↑k + m) * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
⊢ rou ^ k = (rou ^ m)⁻¹
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ (↑k + m) * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
have h₄ := RouNot0 n rou h
Proof state after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ (↑k + m) * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = (rou ^ m)⁻¹
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ (↑k + m) * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
rw [zpow_add₀ h₄ ↑k m] at h₃
Proof state after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = (rou ^ m)⁻¹
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
rw [←h₃]
Proof state after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹
Tactic:
have h₅ : rou ^ m ≠ 0 := by
  exact zpow_ne_zero m h₄
Proof state after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
h₅ : rou ^ m ≠ 0
⊢ rou ^ k = rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
h₅ : rou ^ m ≠ 0
⊢ rou ^ k = rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹
Tactic:
field_simp
Proof state after:
no goals
Theorem: RuesDiffRotationallySymmetric
Proof state before:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
⊢ rou ^ (↑k + m) = 1
Tactic:
rw [kmDiv, zpow_mul]
Proof state after:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
⊢ (rou ^ ↑↑n) ^ k₂ = 1
Theorem: RuesDiffRotationallySymmetric
Proof state before:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
⊢ (rou ^ ↑↑n) ^ k₂ = 1
Tactic:
simp only [zpow_natCast, h, one_zpow]
Proof state after:
no goals
Theorem: RuesDiffRotationallySymmetric
Proof state before:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ m ≠ 0
Tactic:
exact zpow_ne_zero m h₄
Proof state after:
no goals
Theorem: RuesDiffRotationallySymmetric
Proof state before:
case e_f.h.inr
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀b : ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Tactic:
simp_rw [if_neg h₀b]
Proof state after:
no goals
Theorem: Dvd.dvd.addMultiple
Proof 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
Proof state after:
n m k : ℤ
h₁ : n ∣ k * n
⊢ n ∣ m ↔ n ∣ m + k * n
Theorem: Dvd.dvd.addMultiple
Proof state before:
n m k : ℤ
h₁ : n ∣ k * n
⊢ n ∣ m ↔ n ∣ m + k * n
Tactic:
constructor
Proof 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
Theorem: Dvd.dvd.addMultiple
Proof state before:
n m k : ℤ
⊢ n ∣ k * n
Tactic:
exact Int.dvd_mul_left k n
Proof state after:
no goals
Theorem: Dvd.dvd.addMultiple
Proof state before:
case mp
n m k : ℤ
h₁ : n ∣ k * n
⊢ n ∣ m → n ∣ m + k * n
Tactic:
intros h₀
Proof state after:
case mp
n m k : ℤ
h₁ : n ∣ k * n
h₀ : n ∣ m
⊢ n ∣ m + k * n
Theorem: Dvd.dvd.addMultiple
Proof 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₁
Proof state after:
no goals
Theorem: Dvd.dvd.addMultiple
Proof state before:
case mpr
n m k : ℤ
h₁ : n ∣ k * n
⊢ n ∣ m + k * n → n ∣ m
Tactic:
intros h₂
Proof state after:
case mpr
n m k : ℤ
h₁ : n ∣ k * n
h₂ : n ∣ m + k * n
⊢ n ∣ m
Theorem: Dvd.dvd.addMultiple
Proof 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₂
Proof state after:
no goals