[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
s : Set α
⊢ mulSupport f = s ↔ (∀ (x : α), x ∈ s → f x ≠ 1) ∧ ∀ (x : α), ¬x ∈ s → f x = 1
[PROOFSTEP]
simp (config := { contextual := true }) only [ext_iff, mem_mulSupport, ne_eq, iff_def, not_imp_comm, and_comm,
  forall_and]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
s : Set α
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s
[PROOFSTEP]
simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', not_mem_compl_iff, EqOn, Pi.one_apply]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
s : Set α
⊢ Disjoint s (mulSupport f) ↔ EqOn f 1 s
[PROOFSTEP]
rw [disjoint_comm, mulSupport_disjoint_iff]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ mulSupport f = ∅ ↔ f = 1
[PROOFSTEP]
simp_rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ (∀ (x : α), ¬x ∈ ∅ → f x = 1) ↔ ∀ (a : α), f a = OfNat.ofNat 1 a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ Set.Nonempty (mulSupport f) ↔ f ≠ 1
[PROOFSTEP]
rw [nonempty_iff_ne_empty, Ne.def, mulSupport_eq_empty_iff]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ range f ⊆ insert 1 (f '' mulSupport f)
[PROOFSTEP]
simpa only [range_subset_iff, mem_insert_iff, or_iff_not_imp_left] using fun x (hx : x ∈ mulSupport f) =>
  mem_image_of_mem f hx
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
c : M
hc : c ≠ 1
⊢ (mulSupport fun x => c) = univ
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
c : M
hc : c ≠ 1
x : α
⊢ (x ∈ mulSupport fun x => c) ↔ x ∈ univ
[PROOFSTEP]
simp [hc]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
op : M → N → P
op1 : op 1 1 = 1
f : α → M
g : α → N
x : α
hx : x ∈ mulSupport fun x => op (f x) (g x)
hf : f x = 1
hg : g x = 1
⊢ (fun x => op (f x) (g x)) x = 1
[PROOFSTEP]
simp only [hf, hg, op1]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ (mulSupport fun x => ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), mulSupport (f i)
[PROOFSTEP]
rw [mulSupport_subset_iff']
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), ¬x ∈ ⋃ (i : ι), mulSupport (f i) → ⨆ (i : ι), f i x = 1
[PROOFSTEP]
simp only [mem_iUnion, not_exists, nmem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), (∀ (x_1 : ι), f x_1 x = 1) → ⨆ (i : ι), f i x = 1
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
x : α
hx : ∀ (x_1 : ι), f x_1 x = 1
⊢ ⨆ (i : ι), f i x = 1
[PROOFSTEP]
simp only [hx, ciSup_const]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : M → N
hg : g 1 = 1
f : α → M
x : α
h : f x = 1
⊢ (g ∘ f) x = 1
[PROOFSTEP]
simp only [(· ∘ ·), *]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : M → N
f : α → M
hg : ∀ {x : M}, x ∈ range f → (g x = 1 ↔ x = 1)
x : α
⊢ (g ∘ f) x = 1 ↔ f x = 1
[PROOFSTEP]
rw [Function.comp, hg (mem_range_self x)]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
g : α → N
x : α
⊢ (x ∈ mulSupport fun x => (f x, g x)) ↔ x ∈ mulSupport f ∪ mulSupport g
[PROOFSTEP]
simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne.def]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M × N
⊢ mulSupport f = (mulSupport fun x => (f x).fst) ∪ mulSupport fun x => (f x).snd
[PROOFSTEP]
simp only [← mulSupport_prod_mk, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α × β → M
a : α
x : β
hx : x ∈ mulSupport fun b => f (a, b)
⊢ (a, x) ∈ mulSupport f ∧ (a, x).snd = x
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : Monoid M
f : α → M
n : ℕ
⊢ (mulSupport fun x => f x ^ n) ⊆ mulSupport f
[PROOFSTEP]
induction' n with n hfn
[GOAL]
case zero
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : Monoid M
f : α → M
⊢ (mulSupport fun x => f x ^ Nat.zero) ⊆ mulSupport f
[PROOFSTEP]
simp [pow_zero, mulSupport_one]
[GOAL]
case succ
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : Monoid M
f : α → M
n : ℕ
hfn : (mulSupport fun x => f x ^ n) ⊆ mulSupport f
⊢ (mulSupport fun x => f x ^ Nat.succ n) ⊆ mulSupport f
[PROOFSTEP]
simpa only [pow_succ] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : DivisionMonoid G
f g : α → G
⊢ (fun a b => a * b⁻¹) 1 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : MulZeroClass R
f g : α → R
x : α
hfg : x ∈ support fun x => f x * g x
hf : f x = 0
⊢ (fun x => f x * g x) x = 0
[PROOFSTEP]
simp only [hf, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : MulZeroClass R
f g : α → R
x : α
hfg : x ∈ support fun x => f x * g x
hg : g x = 0
⊢ (fun x => f x * g x) x = 0
[PROOFSTEP]
simp only [hg, mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : AddMonoid A
inst✝¹ : Monoid B
inst✝ : DistribMulAction B A
b : B
f : α → A
x : α
hbf : x ∈ support (b • f)
hf : f x = 0
⊢ (b • f) x = 0
[PROOFSTEP]
rw [Pi.smul_apply, hf, smul_zero]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : Zero M
inst✝¹ : Zero β
inst✝ : SMulWithZero M β
f : α → M
g : α → β
x : α
hfg : x ∈ support (f • g)
hf : f x = 0
⊢ (f • g) x = 0
[PROOFSTEP]
rw [Pi.smul_apply', hf, zero_smul]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
g : α → M
hc : c ≠ 0
x : α
⊢ x ∈ support (c • g) ↔ x ∈ support g
[PROOFSTEP]
simp only [hc, mem_support, Pi.smul_apply, Ne.def, smul_eq_zero, false_or_iff]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : GroupWithZero G₀
f g : α → G₀
⊢ (support fun x => f x / g x) = support f ∩ support g
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ (mulSupport fun x => ∏ i in s, f i x) ⊆ ⋃ (i : α) (_ : i ∈ s), mulSupport (f i)
[PROOFSTEP]
rw [mulSupport_subset_iff']
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ ∀ (x : β), ¬x ∈ ⋃ (i : α) (_ : i ∈ s), mulSupport (f i) → ∏ i in s, f i x = 1
[PROOFSTEP]
simp only [mem_iUnion, not_exists, nmem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ ∀ (x : β), (∀ (x_1 : α), x_1 ∈ s → f x_1 x = 1) → ∏ i in s, f i x = 1
[PROOFSTEP]
exact fun x => Finset.prod_eq_one
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : CommMonoidWithZero A
inst✝¹ : NoZeroDivisors A
inst✝ : Nontrivial A
s : Finset α
f : α → β → A
x : β
⊢ (x ∈ support fun x => ∏ i in s, f i x) ↔ x ∈ ⋂ (i : α) (_ : i ∈ s), support (f i)
[PROOFSTEP]
simp [support, Ne.def, Finset.prod_eq_zero_iff, mem_setOf_eq, Set.mem_iInter, not_exists]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝¹ : One R
inst✝ : AddGroup R
f : α → R
⊢ mulSupport (1 - f) = support f
[PROOFSTEP]
rw [sub_eq_add_neg, mulSupport_one_add', support_neg']
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
f : α → M
s : Set β
g : β → α
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))
[PROOFSTEP]
rw [mulSupport_comp_eq_preimage f g, image_inter_preimage]
[GOAL]
A : Type u_1
B : Type u_2
inst✝¹ : DecidableEq A
inst✝ : One B
a : A
b : B
⊢ mulSupport (mulSingle a 1) = ∅
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
inst✝¹ : DecidableEq A
inst✝ : One B
a : A
b : B
h : b ≠ 1
x : A
hx : x = a
⊢ x ∈ mulSupport (mulSingle a b)
[PROOFSTEP]
rwa [mem_mulSupport, hx, mulSingle_eq_same]
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : DecidableEq A
inst✝¹ : One B
a : A
b : B
inst✝ : DecidableEq B
⊢ mulSupport (mulSingle a b) = if b = 1 then ∅ else {a}
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
A : Type u_1
B : Type u_2
inst✝² : DecidableEq A
inst✝¹ : One B
a : A
b : B
inst✝ : DecidableEq B
h : b = 1
⊢ mulSupport (mulSingle a b) = ∅
[PROOFSTEP]
simp [h]
[GOAL]
case neg
A : Type u_1
B : Type u_2
inst✝² : DecidableEq A
inst✝¹ : One B
a : A
b : B
inst✝ : DecidableEq B
h : ¬b = 1
⊢ mulSupport (mulSingle a b) = {a}
[PROOFSTEP]
simp [h]
[GOAL]
A : Type u_1
B : Type u_2
inst✝¹ : DecidableEq A
inst✝ : One B
a : A
b b' : B
hb : b ≠ 1
hb' : b' ≠ 1
i j : A
⊢ Disjoint (mulSupport (mulSingle i b)) (mulSupport (mulSingle j b')) ↔ i ≠ j
[PROOFSTEP]
rw [mulSupport_mulSingle_of_ne hb, mulSupport_mulSingle_of_ne hb', disjoint_singleton]


[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ Decidable (TerminatedAt g n)
[PROOFSTEP]
unfold TerminatedAt
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ Decidable (Stream'.Seq.TerminatedAt g.s n)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : One α
a : α
n : ℕ
aₙ : α
h : Stream'.Seq.get? (partialNumerators (GeneralizedContinuedFraction.ofInteger a)) n = some aₙ
⊢ aₙ = 1
[PROOFSTEP]
cases h
[GOAL]
α : Type u_1
inst✝² : One α
inst✝¹ : Zero α
inst✝ : LT α
a : α
n : ℕ
bₙ : α
h : Stream'.Seq.get? (partialDenominators ↑(SimpleContinuedFraction.ofInteger a)) n = some bₙ
⊢ 0 < bₙ
[PROOFSTEP]
cases h


[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