awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n : ℤ
obtain : ∀ (n_1 : ℕ), n = (↑n_1 : ℤ) ∨ n = -(↑n_1 : ℤ) → HPow.hPow (α := α) (-1) n = if Even n then 1 else -1
⊢ HPow.hPow (α := α) (-1) n = if Even n then 1 else -1

Tactic:
obtain ⟨n, _⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n_1 : ℤ
n : ℕ
h : n_1 = (↑n : ℤ) ∨ n_1 = -(↑n : ℤ)
⊢ HPow.hPow (α := α) (-1) n_1 = if Even n_1 then 1 else -1

Tactic:
aesop (add safe (by rw [neg_one_pow_eq_ite]))
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
h : Eq.{u_4 + 1} (α := R) 2 0
⊢ (Even (α := ℕ) 0 → Eq.{u_4 + 1} (α := R) (↑0 : R) 0) ∧ (Odd (α := ℕ) 0 → Eq.{u_4 + 1} (α := R) (↑0 : R) 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
h : Eq.{u_4 + 1} (α := R) 2 0
⊢ (Even (α := ℕ) 1 → Eq.{u_4 + 1} (α := R) (↑1 : R) 0) ∧ (Odd (α := ℕ) 1 → Eq.{u_4 + 1} (α := R) (↑1 : R) 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
h : Eq.{u_4 + 1} (α := R) 2 0
n : ℕ
h_1 : (Even n → Eq.{u_4 + 1} (α := R) (↑n : R) 0) ∧ (Odd n → Eq.{u_4 + 1} (α := R) (↑n : R) 1)
h_2 : (Even (n + 1) → Eq.{u_4 + 1} (α := R) (↑(n + 1) : R) 0) ∧ (Odd (n + 1) → Eq.{u_4 + 1} (α := R) (↑(n + 1) : R) 1)
⊢ (Even (n + 2) → Eq.{u_4 + 1} (α := R) (↑(n + 2) : R) 0) ∧ (Odd (n + 2) → Eq.{u_4 + 1} (α := R) (↑(n + 2) : R) 1)

Tactic:
simpa [add_assoc, Nat.even_add_one, Nat.odd_add_one, h]

Premises used: Nat.even_add_one, Nat.odd_add_one, add_assoc
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
zero : (Even (α := ℕ) 0 → Eq.{u_4 + 1} (α := R) (↑0 : R) 0) ∧ (Odd (α := ℕ) 0 → Eq.{u_4 + 1} (α := R) (↑0 : R) 1)
one : (Even (α := ℕ) 1 → Eq.{u_4 + 1} (α := R) (↑1 : R) 0) ∧ (Odd (α := ℕ) 1 → Eq.{u_4 + 1} (α := R) (↑1 : R) 1)
more :
  ∀ (n : ℕ),
    (Even n → Eq.{u_4 + 1} (α := R) (↑n : R) 0) ∧ (Odd n → Eq.{u_4 + 1} (α := R) (↑n : R) 1) →
      (Even (n + 1) → Eq.{u_4 + 1} (α := R) (↑(n + 1) : R) 0) ∧ (Odd (n + 1) → Eq.{u_4 + 1} (α := R) (↑(n + 1) : R) 1) →
        (Even (n + 2) → Eq.{u_4 + 1} (α := R) (↑(n + 2) : R) 0) ∧ (Odd (n + 2) → Eq.{u_4 + 1} (α := R) (↑(n + 2) : R) 1)
⊢ (Even n → Eq.{u_4 + 1} (α := R) (↑n : R) 0) ∧ (Odd n → Eq.{u_4 + 1} (α := R) (↑n : R) 1)

Tactic:
induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp
  | more n _ _ => simpa [add_assoc, Nat.even_add_one, Nat.odd_add_one, h]

Premises used: Nat.even_add_one, Nat.odd_add_one, add_assoc, Nat.zero
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
hn : Even n
h : Eq.{u_4 + 1} (α := R) 2 0
⊢ Eq.{u_4 + 1} (α := R) (↑n : R) 0

Tactic:
(natCast_eq_zero_or_one_of_two_eq_zero' n h).1 hn

Premises used: _private.0.natCast_eq_zero_or_one_of_two_eq_zero', And.left
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
hn : Odd n
h : Eq.{u_4 + 1} (α := R) 2 0
⊢ Eq.{u_4 + 1} (α := R) (↑n : R) 1

Tactic:
(natCast_eq_zero_or_one_of_two_eq_zero' n h).2 hn

Premises used: _private.0.natCast_eq_zero_or_one_of_two_eq_zero', And.right
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
inl : ∀ (hn : Even n), Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1
inr : ∀ (hn : Odd n), Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1
⊢ Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1

Tactic:
obtain hn | hn := Nat.even_or_odd n

Premises used: Nat.even_or_odd
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
hn : Even n
⊢ Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1

Tactic:
Or.inl <| natCast_eq_zero_of_even_of_two_eq_zero hn h

Premises used: natCast_eq_zero_of_even_of_two_eq_zero, Or.inl
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
hn : Even n
⊢ Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1

Tactic:
exact Or.inl <| natCast_eq_zero_of_even_of_two_eq_zero hn h

Premises used: natCast_eq_zero_of_even_of_two_eq_zero, Or.inl
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
hn : Odd n
⊢ Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1

Tactic:
Or.inr <| natCast_eq_one_of_odd_of_two_eq_zero hn h

Premises used: natCast_eq_one_of_odd_of_two_eq_zero, Or.inr
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
hn : Odd n
⊢ Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1

Tactic:
exact Or.inr <| natCast_eq_one_of_odd_of_two_eq_zero hn h

Premises used: natCast_eq_one_of_odd_of_two_eq_zero, Or.inr
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : Add α
h : Periodic f c
⊢ (fun (x : α) ↦ f (x + c)) = f

Tactic:
funext h

Premises used: funext
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : Add α
h : Periodic f c
g : β → γ
⊢ Periodic (g ∘ f) c

Tactic:
simp_all
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : Add α
inst_1 : Add γ
h : Periodic f c
g : γ →ₙ+ α
g_inv : α → γ
hg : RightInverse g_inv (⇑g : (a : γ) → α)
x : γ
⊢ (f ∘ (⇑g : (a : γ) → α)) (x + g_inv c) = (f ∘ (⇑g : (a : γ) → α)) x

Tactic:
simp only [hg c, h (g x), map_add, comp_apply]

Premises used: map_add, Function.comp_apply, DFunLike.coe
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
c : α
inst : Add α
inst_1 : Mul β
hf : Periodic f c
hg : Periodic g c
⊢ Periodic (f * g) c

Tactic:
simp_all
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
c : α
inst : Add α
inst_1 : Div β
hf : Periodic f c
hg : Periodic g c
⊢ Periodic (f / g) c

Tactic:
simp_all
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
c : α
inst : Add α
inst_1 : MulOneClass β
hl : ∀ (f : α → β), Membership.mem (γ := List (α → β)) [] f → Periodic f c
⊢ Periodic.{u_1, u_2} (β := β) (List.prod []) c

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
c : α
inst : Add α
inst_1 : MulOneClass β
g : α → β
l : List (α → β)
ih : ∀ (hl : ∀ f ∈ l, Periodic f c), Periodic l.prod c
hl : ∀ f ∈ g :: l, Periodic f c
⊢ Periodic g c ∧ ∀ x ∈ l, Periodic x c

Tactic:
rw [List.forall_mem_cons] at hl

Premises used: List.forall_mem_cons
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
c : α
inst : Add α
inst_1 : MulOneClass β
g : α → β
l : List (α → β)
ih : ∀ (hl : ∀ f ∈ l, Periodic f c), Periodic l.prod c
hl : Periodic g c ∧ ∀ x ∈ l, Periodic x c
⊢ Periodic (g :: l).prod c

Tactic:
simpa only [List.prod_cons] using hl.1.mul (ih hl.2)

Premises used: And.right, And.left, List.prod_cons, Function.Periodic.mul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
c : α
inst : Add α
inst_1 : MulOneClass β
l : List (α → β)
hl : ∀ f ∈ l, Periodic f c
nil :
  ∀ (hl : ∀ (f : α → β), Membership.mem (γ := List (α → β)) [] f → Periodic f c),
    Periodic.{u_1, u_2} (β := β) (List.prod []) c
cons :
  ∀ (g : α → β) (l : List (α → β)) (ih : ∀ (hl : ∀ f ∈ l, Periodic f c), Periodic l.prod c)
    (hl : ∀ f ∈ g :: l, Periodic f c), Periodic (g :: l).prod c
⊢ Periodic l.prod c

Tactic:
induction l with
  | nil => simp
  | cons g l ih =>
    rw [List.forall_mem_cons] at hl
    simpa only [List.prod_cons] using hl.1.mul (ih hl.2)

Premises used: List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
c : α
inst : Add α
inst_1 : CommMonoid β
ι : Type u_4
f : ι → α → β
s : Finset ι
hs : ∀ i ∈ s, Periodic (f i) c
⊢ ∀ f_1 ∈ List.map f s.toList, Periodic f_1 c

Tactic:
simpa [-Periodic]

Premises used: Function.Periodic
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : Add α
inst_1 : SMul γ β
h : Periodic f c
a : γ
⊢ Periodic (a • f) c

Tactic:
simp_all
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : AddMonoid α
inst_1 : Group γ
inst_2 : DistribMulAction γ α
h : Periodic f c
a : γ
x : α
⊢ Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) ((fun (x : α) ↦ f (a • x)) x)

Tactic:
simpa only [smul_add, smul_inv_smul] using h (a • x)

Premises used: smul_inv_smul, HSMul.hSMul, smul_add
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : AddMonoid α
inst_1 : Group γ
inst_2 : DistribMulAction γ α
h : Periodic f c
a : γ
⊢ Periodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (a⁻¹ • x)) (a • c)

Tactic:
simpa only [inv_inv] using h.const_smul a⁻¹

Premises used: Inv.inv, inv_inv, Function.Periodic.const_smul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst : AddSemigroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
⊢ Periodic f (c₁ + c₂)

Tactic:
simp_all [← add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
x : α
⊢ f (x - c) = f x

Tactic:
simpa only [sub_add_cancel] using (h (x - c)).symm

Premises used: HSub.hSub, Eq.symm, sub_add_cancel
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : SubtractionCommMonoid α
h : Periodic f c
⊢ f (c - x) = f (-x)

Tactic:
simpa only [sub_eq_neg_add] using h (-x)

Premises used: sub_eq_neg_add, Neg.neg
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
⊢ Periodic f (-c)

Tactic:
simpa only [sub_eq_add_neg, Periodic] using h.sub_eq

Premises used: sub_eq_add_neg, Function.Periodic, Function.Periodic.sub_eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
rw : f (x + (c₁ + -c₂)) = f x
rw₁ : f (x + c₁ + -c₂) = f x
rw₂ : f (x + c₁) = f x
rw₃ rw₄ : f x = f x
⊢ f (x + (c₁ - c₂)) = f x

Tactic:
rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]

Premises used: add_assoc, sub_eq_add_neg, Function.Periodic.neg
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddSemigroup α
h : Periodic f c
a x : α
⊢ Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a + x)) (x + c)) ((fun (x : α) ↦ f (a + x)) x)

Tactic:
simpa [add_assoc] using h (a + x)

Premises used: add_assoc, HAdd.hAdd
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommSemigroup α
h : Periodic f c
a x : α
⊢ Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (x + a)) (x + c)) ((fun (x : α) ↦ f (x + a)) x)

Tactic:
simpa only [add_right_comm] using h (x + a)

Premises used: add_right_comm, HAdd.hAdd
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
h : Periodic f c
a x : α
⊢ Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a - x)) (x + c)) ((fun (x : α) ↦ f (a - x)) x)

Tactic:
simp only [← sub_sub, h.sub_eq]

Premises used: sub_sub, Function.Periodic.sub_eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : SubtractionCommMonoid α
h : Periodic f c
a : α
⊢ Periodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (x - a)) c

Tactic:
simpa only [sub_eq_add_neg] using h.add_const (-a)

Premises used: sub_eq_add_neg, Function.Periodic.add_const, Neg.neg
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddMonoid α
h : Periodic f c
n : ℕ
zero : Periodic f (HSMul.hSMul (α := ℕ) 0 c)
succ : ∀ (n : ℕ), Periodic f (n • c) → Periodic f ((n + 1) • c)
⊢ Periodic f (n • c)

Tactic:
induction n
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddMonoid α
h : Periodic f c
⊢ Periodic f (HSMul.hSMul (α := ℕ) 0 c)

Tactic:
simp_all [add_nsmul, ← add_assoc]

Premises used: add_assoc, add_nsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddMonoid α
h : Periodic f c
n : ℕ
h_1 : Periodic f (n • c)
⊢ Periodic f ((n + 1) • c)

Tactic:
simp_all [add_nsmul, ← add_assoc]

Premises used: add_assoc, add_nsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocSemiring α
h : Periodic f c
n : ℕ
⊢ Periodic f ((↑n : α) * c)

Tactic:
simpa only [nsmul_eq_mul] using h.nsmul n

Premises used: Function.Periodic.nsmul, nsmul_eq_mul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (-(n • c))

Tactic:
(h.nsmul n).neg

Premises used: Function.Periodic.nsmul, Function.Periodic.neg
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ Periodic f (-((↑n : α) * c))

Tactic:
(h.nat_mul n).neg

Premises used: Function.Periodic.nat_mul, Function.Periodic.neg
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddGroup α
h : Periodic f c
n : ℕ
⊢ f (x - n • c) = f x

Tactic:
simpa only [sub_eq_add_neg] using h.neg_nsmul n x

Premises used: sub_eq_add_neg, Function.Periodic.neg_nsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ f (x - (↑n : α) * c) = f x

Tactic:
simpa only [nsmul_eq_mul] using h.sub_nsmul_eq n

Premises used: nsmul_eq_mul, Function.Periodic.sub_nsmul_eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : SubtractionCommMonoid α
h : Periodic f c
n : ℕ
⊢ f (n • c - x) = f (-x)

Tactic:
(h.nsmul n).sub_eq'

Premises used: Function.Periodic.nsmul, Function.Periodic.sub_eq'
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ f ((↑n : α) * c - x) = f (-x)

Tactic:
simpa only [sub_eq_neg_add] using h.nat_mul n (-x)

Premises used: sub_eq_neg_add, Function.Periodic.nat_mul, Neg.neg
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
n : ℤ
ofNat : ∀ (n : ℕ), Periodic f (Int.ofNat n • c)
negSucc : ∀ (n : ℕ), Periodic f (Int.negSucc n • c)
⊢ Periodic f (n • c)

Tactic:
rcases n with n | n
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.ofNat n • c)

Tactic:
simpa only [Int.ofNat_eq_natCast, natCast_zsmul] using h.nsmul n

Premises used: Function.Periodic.nsmul, Int.ofNat_eq_natCast, natCast_zsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)

Tactic:
simpa only [negSucc_zsmul] using (h.nsmul (n + 1)).neg

Premises used: Function.Periodic.nsmul, Function.Periodic.neg, negSucc_zsmul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocRing α
h : Periodic f c
n : ℤ
⊢ Periodic f ((↑n : α) * c)

Tactic:
simpa only [zsmul_eq_mul] using h.zsmul n

Premises used: zsmul_eq_mul, Function.Periodic.zsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddGroup α
h : Periodic f c
n : ℤ
⊢ f (x - n • c) = f x

Tactic:
(h.zsmul n).sub_eq x

Premises used: Function.Periodic.zsmul, Function.Periodic.sub_eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : NonAssocRing α
h : Periodic f c
n : ℤ
⊢ f (x - (↑n : α) * c) = f x

Tactic:
(h.int_mul n).sub_eq x

Premises used: Function.Periodic.int_mul, Function.Periodic.sub_eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddCommGroup α
h : Periodic f c
n : ℤ
⊢ f (n • c - x) = f (-x)

Tactic:
(h.zsmul _).sub_eq'

Premises used: Function.Periodic.sub_eq', Function.Periodic.zsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : NonAssocRing α
h : Periodic f c
n : ℤ
⊢ f ((↑n : α) * c - x) = f (-x)

Tactic:
(h.int_mul _).sub_eq'

Premises used: Function.Periodic.int_mul, Function.Periodic.sub_eq'
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddZeroClass α
h : Periodic f c
⊢ f c = f 0

Tactic:
simpa only [zero_add] using h 0

Premises used: zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
⊢ f (-c) = f 0

Tactic:
h.neg.eq

Premises used: Function.Periodic.neg, Function.Periodic.eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddMonoid α
h : Periodic f c
n : ℕ
⊢ f (n • c) = f 0

Tactic:
(h.nsmul n).eq

Premises used: Function.Periodic.nsmul, Function.Periodic.eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocSemiring α
h : Periodic f c
n : ℕ
⊢ f ((↑n : α) * c) = f 0

Tactic:
(h.nat_mul n).eq

Premises used: Function.Periodic.nat_mul, Function.Periodic.eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
n : ℤ
⊢ f (n • c) = f 0

Tactic:
(h.zsmul n).eq

Premises used: Function.Periodic.zsmul, Function.Periodic.eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocRing α
h : Periodic f c
n : ℤ
⊢ f ((↑n : α) * c) = f 0

Tactic:
(h.int_mul n).eq

Premises used: Function.Periodic.int_mul, Function.Periodic.eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
inst : AddZeroClass α
f : α → β
x : α
rw rw₁ : f x = f x
⊢ f (x + 0) = f x

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
f : α → α
n : ℕ
a : α
⊢ Periodic.{0, u_1} (β := α) (fun (x : ℕ) ↦ f^[x] a) n ↔ IsPeriodicPt f n a

Tactic:
⟨fun h ↦ h.eq, fun h k ↦ ?_⟩

Premises used: Iff.intro, Function.Periodic.eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
f : α → α
n : ℕ
a : α
refine :
  ∀ (h : IsPeriodicPt f n a) (k : ℕ),
    Eq.{u_1 + 1} (α := α) ((fun (x : ℕ) ↦ f^[x] a) (k + n)) ((fun (x : ℕ) ↦ f^[x] a) k)
⊢ Periodic.{0, u_1} (β := α) (fun (x : ℕ) ↦ f^[x] a) n ↔ IsPeriodicPt f n a

Tactic:
refine ⟨fun h ↦ h.eq, fun h k ↦ ?_⟩
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
f : α → α
n : ℕ
a : α
h : IsPeriodicPt f n a
k : ℕ
⊢ Eq.{u_1 + 1} (α := α) ((fun (x : ℕ) ↦ f^[x] a) (k + n)) ((fun (x : ℕ) ↦ f^[x] a) k)

Tactic:
simp only [Function.iterate_add_apply, h.eq]

Premises used: Function.iterate_add_apply, Function.IsFixedPt.eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
hf : Periodic f c
a : ↥(AddSubgroup.zmultiples c)
x : α
rcases :
  ∀ (m : ℤ),
    f
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (AddSubgroup.zmultiples c) x)
            ((fun (x : ℤ) ↦ x • c) m) ⋯ +ᵥ
          x) =
      f x
⊢ f (a +ᵥ x) = f x

Tactic:
rcases a with ⟨_, m, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
hf : Periodic f c
x : α
m : ℤ
⊢ f
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (AddSubgroup.zmultiples c) x)
          ((fun (x : ℤ) ↦ x • c) m) ⋯ +ᵥ
        x) =
    f x

Tactic:
simp [AddSubgroup.vadd_def, add_comm _ x, hf.zsmul m x]

Premises used: add_comm, AddSubgroup.vadd_def, Function.Periodic.zsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommMonoid α
hf : Periodic f c
a : ↥(AddSubmonoid.multiples c)
x : α
rcases :
  ∀ (m : ℕ),
    f
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubmonoid α) (AddSubmonoid.multiples c) x)
            ((fun (i : ℕ) ↦ i • c) m) ⋯ +ᵥ
          x) =
      f x
⊢ f (a +ᵥ x) = f x

Tactic:
rcases a with ⟨_, m, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommMonoid α
hf : Periodic f c
x : α
m : ℕ
⊢ f
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubmonoid α) (AddSubmonoid.multiples c) x)
          ((fun (i : ℕ) ↦ i • c) m) ⋯ +ᵥ
        x) =
    f x

Tactic:
simp [AddSubmonoid.vadd_def, add_comm _ x, hf.nsmul m x]

Premises used: Function.Periodic.nsmul, add_comm, AddSubmonoid.vadd_def
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x_1 : α
inst : AddGroup α
h : Periodic f c
x : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples c)
a b : α
h' : (QuotientAddGroup.leftRel (AddSubgroup.zmultiples c) : α → α → Prop) a b
⊢ Membership.mem (γ := AddSubgroup α) (AddSubgroup.zmultiples c) (-a + b)

Tactic:
rw [QuotientAddGroup.leftRel_apply] at h'

Premises used: QuotientAddGroup.leftRel_apply
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x_1 : α
inst : AddGroup α
h : Periodic f c
x : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples c)
a b : α
h' : Membership.mem (γ := AddSubgroup α) (AddSubgroup.zmultiples c) (-a + b)
obtain : ∀ (k : ℤ) (hk : (fun (x : ℤ) ↦ x • c) k = -a + b), f a = f b
⊢ f a = f b

Tactic:
obtain ⟨k, hk⟩ := h'
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x_1 : α
inst : AddGroup α
h : Periodic f c
x : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples c)
a b : α
k : ℤ
hk : (fun (x : ℤ) ↦ x • c) k = -a + b
⊢ f a = f b

Tactic:
(h.zsmul k _).symm.trans (congr_arg f (add_eq_of_eq_neg_add hk))

Premises used: add_eq_of_eq_neg_add, congr_arg, Function.Periodic.zsmul, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x_1 : α
inst : AddGroup α
h : Periodic f c
x : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples c)
a b : α
k : ℤ
hk : (fun (x : ℤ) ↦ x • c) k = -a + b
⊢ f a = f b

Tactic:
exact (h.zsmul k _).symm.trans (congr_arg f (add_eq_of_eq_neg_add hk))

Premises used: add_eq_of_eq_neg_add, congr_arg, Function.Periodic.zsmul, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
a : α
⊢ h.lift (↑a : α ⧸ AddSubgroup.zmultiples c) = f a

Tactic:
rfl

Premises used: Quotient.liftOn', Function.Periodic.lift, rfl
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
R : Type u_4
X : Type u_5
inst : AddZeroClass R
f : R → X
c : R
hf : Periodic f c
hc : c ≠ 0
⊢ ¬Injective f

Tactic:
fun h ↦ hc <| h hf.eq

Premises used: Function.Periodic.eq, Not
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : Add α
inst_1 : Neg β
h : Antiperiodic f c
⊢ (fun (x : α) ↦ f (x + c)) = -f

Tactic:
funext h

Premises used: funext
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : Add α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
⊢ (fun (x : α) ↦ -f (x + c)) = f

Tactic:
neg_eq_iff_eq_neg.mpr h.funext

Premises used: Iff.mpr, neg_eq_iff_eq_neg, Function.Antiperiodic.funext
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddMonoid α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
⊢ Periodic f (HSMul.hSMul (α := ℕ) 2 c)

Tactic:
simp [two_nsmul, ← add_assoc, h _]

Premises used: add_assoc, two_nsmul