[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g✝ : α → β
c c₁ c₂ x : α
inst✝ : Add α
h : Periodic f c
g : β → γ
⊢ Periodic (g ∘ f) c
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g✝ : α → β
c c₁ c₂ x✝ : α
inst✝¹ : Add α
inst✝ : Add γ
h : Periodic f c
g : AddHom γ α
g_inv : α → γ
hg : RightInverse g_inv ↑g
x : γ
⊢ (f ∘ ↑g) (x + g_inv c) = (f ∘ ↑g) x
[PROOFSTEP]
simp only [hg c, h (g x), map_add, comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Mul β
hf : Periodic f c
hg : Periodic g c
⊢ Periodic (f * g) c
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Div β
hf : Periodic f c
hg : Periodic g c
⊢ Periodic (f / g) c
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l : List (α → β)
hl : ∀ (f : α → β), f ∈ l → Periodic f c
⊢ Periodic (List.prod l) c
[PROOFSTEP]
induction' l with g l ih hl
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l : List (α → β)
hl✝ : ∀ (f : α → β), f ∈ l → Periodic f c
hl : ∀ (f : α → β), f ∈ [] → Periodic f c
⊢ Periodic (List.prod []) c
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f g✝ : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l✝ : List (α → β)
hl✝ : ∀ (f : α → β), f ∈ l✝ → Periodic f c
g : α → β
l : List (α → β)
ih : (∀ (f : α → β), f ∈ l → Periodic f c) → Periodic (List.prod l) c
hl : ∀ (f : α → β), f ∈ g :: l → Periodic f c
⊢ Periodic (List.prod (g :: l)) c
[PROOFSTEP]
rw [List.forall_mem_cons] at hl 
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f g✝ : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l✝ : List (α → β)
hl✝ : ∀ (f : α → β), f ∈ l✝ → Periodic f c
g : α → β
l : List (α → β)
ih : (∀ (f : α → β), f ∈ l → Periodic f c) → Periodic (List.prod l) c
hl : Periodic g c ∧ ∀ (x : α → β), x ∈ l → Periodic x c
⊢ Periodic (List.prod (g :: l)) c
[PROOFSTEP]
simpa only [List.prod_cons] using hl.1.mul (ih hl.2)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ g : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : CommMonoid β
ι : Type u_4
f : ι → α → β
s : Finset ι
hs : ∀ (i : ι), i ∈ s → Periodic (f i) c
⊢ ∀ (f_1 : α → β), f_1 ∈ List.map f (Finset.toList s) → Periodic f_1 c
[PROOFSTEP]
simpa [-Periodic]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : SMul γ β
h : Periodic f c
a : γ
⊢ Periodic (a • f) c
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝² : AddMonoid α
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Periodic f c
a : γ
x : α
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x
[PROOFSTEP]
simpa only [smul_add, smul_inv_smul] using h (a • x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
ha : a = 0
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x
[PROOFSTEP]
simp only [ha, zero_smul]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
ha : ¬a = 0
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x
[PROOFSTEP]
simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝² : AddMonoid α
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Periodic f c
a : γ
⊢ Periodic (fun x => f (a⁻¹ • x)) (a • c)
[PROOFSTEP]
simpa only [inv_inv] using h.const_smul a⁻¹
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
⊢ Periodic (fun x => f (a⁻¹ • x)) (a • c)
[PROOFSTEP]
simpa only [inv_inv] using h.const_smul₀ a⁻¹
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic (fun x => f (x * a)) (c / a)
[PROOFSTEP]
simpa only [div_eq_mul_inv] using h.mul_const a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic (fun x => f (x / a)) (c * a)
[PROOFSTEP]
simpa only [div_eq_mul_inv] using h.mul_const_inv a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddSemigroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
⊢ Periodic f (c₁ + c₂)
[PROOFSTEP]
simp_all [← add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h : Periodic f c
x : α
⊢ f (x - c) = f x
[PROOFSTEP]
simpa only [sub_add_cancel] using (h (x - c)).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddCommGroup α
h : Periodic f c
⊢ f (c - x) = f (-x)
[PROOFSTEP]
simpa only [sub_eq_neg_add] using h (-x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddGroup α
h : Periodic f c
⊢ Periodic f (-c)
[PROOFSTEP]
simpa only [sub_eq_add_neg, Periodic] using h.sub_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + (c₁ - c₂)) = f x
[PROOFSTEP]
rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddSemigroup α
h : Periodic f c
a x : α
⊢ (fun x => f (a + x)) (x + c) = (fun x => f (a + x)) x
[PROOFSTEP]
simpa [add_assoc] using h (a + x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddCommSemigroup α
h : Periodic f c
a x : α
⊢ (fun x => f (x + a)) (x + c) = (fun x => f (x + a)) x
[PROOFSTEP]
simpa only [add_right_comm] using h (x + a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddCommGroup α
h : Periodic f c
a x : α
⊢ (fun x => f (a - x)) (x + c) = (fun x => f (a - x)) x
[PROOFSTEP]
simp only [← sub_sub, h.sub_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddCommGroup α
h : Periodic f c
a : α
⊢ Periodic (fun x => f (x - a)) c
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h.add_const (-a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddMonoid α
h : Periodic f c
n : ℕ
⊢ Periodic f (n • c)
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddMonoid α
h : Periodic f c
⊢ Periodic f (Nat.zero • c)
[PROOFSTEP]
simp_all [Nat.succ_eq_add_one, add_nsmul, ← add_assoc, zero_nsmul]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddMonoid α
h : Periodic f c
n✝ : ℕ
n_ih✝ : Periodic f (n✝ • c)
⊢ Periodic f (Nat.succ n✝ • c)
[PROOFSTEP]
simp_all [Nat.succ_eq_add_one, add_nsmul, ← add_assoc, zero_nsmul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : Semiring α
h : Periodic f c
n : ℕ
⊢ Periodic f (↑n * c)
[PROOFSTEP]
simpa only [nsmul_eq_mul] using h.nsmul n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ f (x - n • c) = f x
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h.neg_nsmul n x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : Ring α
h : Periodic f c
n : ℕ
⊢ f (x - ↑n * c) = f x
[PROOFSTEP]
simpa only [nsmul_eq_mul] using h.sub_nsmul_eq n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : Ring α
h : Periodic f c
n : ℕ
⊢ f (↑n * c - x) = f (-x)
[PROOFSTEP]
simpa only [sub_eq_neg_add] using h.nat_mul n (-x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℤ
⊢ Periodic f (n • c)
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.ofNat n • c)
[PROOFSTEP]
simpa only [Int.ofNat_eq_coe, coe_nat_zsmul] using h.nsmul n
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)
[PROOFSTEP]
simpa only [negSucc_zsmul] using (h.nsmul (n + 1)).neg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : Ring α
h : Periodic f c
n : ℤ
⊢ Periodic f (↑n * c)
[PROOFSTEP]
simpa only [zsmul_eq_mul] using h.zsmul n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝ : AddZeroClass α
h : Periodic f c
⊢ f c = f 0
[PROOFSTEP]
simpa only [zero_add] using h 0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc : c ≠ 0
a : α
⊢ f '' uIcc a (a + c) = range f
[PROOFSTEP]
cases hc.lt_or_lt with
| inl hc =>
  rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c), add_neg_cancel_right]
| inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc : c ≠ 0
a : α
x✝ : c < 0 ∨ 0 < c
⊢ f '' uIcc a (a + c) = range f
[PROOFSTEP]
cases hc.lt_or_lt with
| inl hc =>
  rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c), add_neg_cancel_right]
| inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' uIcc a (a + c) = range f
[PROOFSTEP]

| inl hc =>
  rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c), add_neg_cancel_right]
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' uIcc a (a + c) = range f
[PROOFSTEP]
rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c), add_neg_cancel_right]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : 0 < c
⊢ f '' uIcc a (a + c) = range f
[PROOFSTEP]

| inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : 0 < c
⊢ f '' uIcc a (a + c) = range f
[PROOFSTEP]
rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddZeroClass α
f : α → β
x : α
⊢ f (x + 0) = f x
[PROOFSTEP]
rw [add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddCommGroup α
hf : Periodic f c
a : { x // x ∈ AddSubgroup.zmultiples c }
x : α
⊢ f (a +ᵥ x) = f x
[PROOFSTEP]
rcases a with ⟨_, m, rfl⟩
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddCommGroup α
hf : Periodic f c
x : α
m : ℤ
⊢ f ({ val := (fun x => x • c) m, property := (_ : ∃ y, (fun x => x • c) y = (fun x => x • c) m) } +ᵥ x) = f x
[PROOFSTEP]
simp [AddSubgroup.vadd_def, add_comm _ x, hf.zsmul m x]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddCommMonoid α
hf : Periodic f c
a : { x // x ∈ AddSubmonoid.multiples c }
x : α
⊢ f (a +ᵥ x) = f x
[PROOFSTEP]
rcases a with ⟨_, m, rfl⟩
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddCommMonoid α
hf : Periodic f c
x : α
m : ℕ
⊢ f ({ val := (fun i => i • c) m, property := (_ : ∃ y, (fun i => i • c) y = (fun i => i • c) m) } +ᵥ x) = f x
[PROOFSTEP]
simp [AddSubmonoid.vadd_def, add_comm _ x, hf.nsmul m x]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h : Periodic f c
x : α ⧸ AddSubgroup.zmultiples c
a b : α
h' : Setoid.r a b
⊢ f a = f b
[PROOFSTEP]
rw [QuotientAddGroup.leftRel_apply] at h' 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h : Periodic f c
x : α ⧸ AddSubgroup.zmultiples c
a b : α
h' : -a + b ∈ AddSubgroup.zmultiples c
⊢ f a = f b
[PROOFSTEP]
obtain ⟨k, hk⟩ := h'
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h : Periodic f c
x : α ⧸ AddSubgroup.zmultiples c
a b : α
k : ℤ
hk : (fun x => x • c) k = -a + b
⊢ f a = f b
[PROOFSTEP]
exact (h.zsmul k _).symm.trans (congr_arg f (add_eq_of_eq_neg_add hk))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Semiring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ Periodic f (2 * c)
[PROOFSTEP]
simp [two_mul, ← add_assoc, h _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddZeroClass α
inst✝ : Neg β
h : Antiperiodic f c
⊢ f c = -f 0
[PROOFSTEP]
simpa only [zero_add] using h 0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝¹ : Semiring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x
[PROOFSTEP]
rw [← add_assoc, h, h.periodic.nat_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝¹ : Ring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x
[PROOFSTEP]
rw [← add_assoc, h, h.periodic.int_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
x : α
⊢ f (x - c) = -f x
[PROOFSTEP]
simp only [← neg_eq_iff_eq_neg, ← h (x - c), sub_add_cancel]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddCommGroup α
inst✝ : Neg β
h : Antiperiodic f c
⊢ f (c - x) = -f (-x)
[PROOFSTEP]
simpa only [sub_eq_neg_add] using h (-x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ Antiperiodic f (-c)
[PROOFSTEP]
simpa only [sub_eq_add_neg, Antiperiodic] using h.sub_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ f (-c) = -f 0
[PROOFSTEP]
simpa only [zero_add] using h.neg 0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Semiring α
inst✝ : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
⊢ f (↑0 * c) = 0
[PROOFSTEP]
rwa [Nat.cast_zero, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Semiring α
inst✝ : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑(n + 1) * c) = 0
[PROOFSTEP]
simp [add_mul, h _, Antiperiodic.nat_mul_eq_of_eq_zero h hi n]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Ring α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑↑n * c) = 0
[PROOFSTEP]
rw [Int.cast_ofNat, h.nat_mul_eq_of_eq_zero hi n]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Ring α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑(Int.negSucc n) * c) = 0
[PROOFSTEP]
rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝¹ : AddSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ (fun x => f (a + x)) (x + c) = -(fun x => f (a + x)) x
[PROOFSTEP]
simpa [add_assoc] using h (a + x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝¹ : AddCommSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ (fun x => f (x + a)) (x + c) = -(fun x => f (x + a)) x
[PROOFSTEP]
simpa only [add_right_comm] using h (x + a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝¹ : AddCommGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
a x : α
⊢ (fun x => f (a - x)) (x + c) = -(fun x => f (a - x)) x
[PROOFSTEP]
simp only [← sub_sub, h.sub_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddCommGroup α
inst✝ : Neg β
h : Antiperiodic f c
a : α
⊢ Antiperiodic (fun x => f (x - a)) c
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h.add_const (-a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝³ : Add α
inst✝² : Monoid γ
inst✝¹ : AddGroup β
inst✝ : DistribMulAction γ β
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (a • f) c
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
x : α
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = -(fun x => f (a • x)) x
[PROOFSTEP]
simpa only [smul_add, smul_inv_smul] using h (a • x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝³ : AddCommMonoid α
inst✝² : Neg β
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Antiperiodic f c
a : γ
ha : a ≠ 0
x : α
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = -(fun x => f (a • x)) x
[PROOFSTEP]
simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)
[PROOFSTEP]
simpa only [inv_inv] using h.const_smul a⁻¹
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝³ : AddCommMonoid α
inst✝² : Neg β
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Antiperiodic f c
a : γ
ha : a ≠ 0
⊢ Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)
[PROOFSTEP]
simpa only [inv_inv] using h.const_smul₀ (inv_ne_zero ha)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : DivisionSemiring α
inst✝ : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic (fun x => f (x * a)) (c / a)
[PROOFSTEP]
simpa only [div_eq_mul_inv] using h.mul_const ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : DivisionSemiring α
inst✝ : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic (fun x => f (x / a)) (c * a)
[PROOFSTEP]
simpa only [div_eq_mul_inv] using h.mul_const_inv ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic f c₂
⊢ Periodic f (c₁ + c₂)
[PROOFSTEP]
simp_all [← add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic f c₂
⊢ Periodic f (c₁ - c₂)
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h1.add h2.neg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddGroup α
inst✝ : Neg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ + c₂)
[PROOFSTEP]
simp_all [← add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ - c₂)
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h1.add_antiperiod h2.neg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝² : Add α
inst✝¹ : Mul β
inst✝ : HasDistribNeg β
hf : Antiperiodic f c
hg : Antiperiodic g c
⊢ Periodic (f * g) c
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x : α
inst✝² : Add α
inst✝¹ : DivisionMonoid β
inst✝ : HasDistribNeg β
hf : Antiperiodic f c
hg : Antiperiodic g c
⊢ Periodic (f / g) c
[PROOFSTEP]
simp_all [neg_div_neg_eq]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
f g : α✝ → β
c c₁ c₂ x : α✝
α : Type u_4
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ fract (a + 1) = fract a
[PROOFSTEP]
exact_mod_cast Int.fract_add_int a 1
