awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocSemiring α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
⊢ Periodic f (2 * c)

Tactic:
nsmul_eq_mul 2 c ▸ h.periodic

Premises used: Function.Antiperiodic.periodic, Eq.rec, nsmul_eq_mul, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddZeroClass α
inst_1 : Neg β
h : Antiperiodic 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 : AddMonoid α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
⊢ Periodic f ((2 * n) • c)

Tactic:
mul_nsmul c 2 n ▸ h.periodic.nsmul n

Premises used: Function.Periodic.nsmul, Function.Antiperiodic.periodic, Eq.rec, mul_nsmul, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocSemiring α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
⊢ Periodic f ((↑n : α) * (2 * c))

Tactic:
h.periodic_two_mul.nat_mul n

Premises used: Function.Antiperiodic.periodic_two_mul, Function.Periodic.nat_mul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddMonoid α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
rw : f (x + ((2 * n) • c + HSMul.hSMul (α := ℕ) 1 c)) = -f x
rw₁ : f (x + ((2 * n) • c + c)) = -f x
rw₂ : f (x + (2 * n) • c + c) = -f x
rw₃ : -f (x + (2 * n) • c) = -f x
rw₄ rw₅ : -f x = -f x
⊢ f (x + (2 * n + 1) • c) = -f x

Tactic:
rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]

Premises used: add_assoc, Function.Antiperiodic.even_nsmul_periodic, one_nsmul, add_nsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocSemiring α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
rw : f (x + (↑n : α) * (2 * c) + c) = -f x
rw₁ : -f (x + (↑n : α) * (2 * c)) = -f x
rw₂ rw₃ : -f x = -f x
⊢ f (x + ((↑n : α) * (2 * c) + c)) = -f x

Tactic:
rw [← add_assoc, h, h.nat_even_mul_periodic]

Premises used: add_assoc, Function.Antiperiodic.nat_even_mul_periodic
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
rw : Periodic f (n • HSMul.hSMul (α := ℕ) 2 c)
⊢ Periodic f ((2 * n) • c)

Tactic:
rw [mul_comm, mul_zsmul, two_zsmul, ← two_nsmul]

Premises used: mul_zsmul, mul_comm, two_zsmul, two_nsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f (n • HSMul.hSMul (α := ℕ) 2 c)

Tactic:
h.periodic.zsmul n

Premises used: Function.Antiperiodic.periodic, Function.Periodic.zsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f (n • HSMul.hSMul (α := ℕ) 2 c)

Tactic:
exact h.periodic.zsmul n

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

Tactic:
h.periodic_two_mul.int_mul n

Premises used: Function.Periodic.int_mul, Function.Antiperiodic.periodic_two_mul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
rw : f (x + ((2 * n) • c + HSMul.hSMul (α := ℤ) 1 c)) = -f x
rw₁ : f (x + ((2 * n) • c + c)) = -f x
rw₂ : f (x + (2 * n) • c + c) = -f x
rw₃ : -f (x + (2 * n) • c) = -f x
rw₄ rw₅ : -f x = -f x
⊢ f (x + (2 * n + 1) • c) = -f x

Tactic:
rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]

Premises used: add_assoc, add_zsmul, one_zsmul, Function.Antiperiodic.even_zsmul_periodic
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocRing α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
rw : f (x + (↑n : α) * (2 * c) + c) = -f x
rw₁ : -f (x + (↑n : α) * (2 * c)) = -f x
rw₂ rw₃ : -f x = -f x
⊢ f (x + ((↑n : α) * (2 * c) + c)) = -f x

Tactic:
rw [← add_assoc, h, h.int_even_mul_periodic]

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

Tactic:
simp only [← neg_eq_iff_eq_neg, ← h (x - c), sub_add_cancel]

Premises used: HSub.hSub, neg_eq_iff_eq_neg, sub_add_cancel
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : SubtractionCommMonoid α
inst_1 : Neg β
h : Antiperiodic 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 α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
⊢ Antiperiodic f (-c)

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

Premises used: Function.Antiperiodic.sub_eq, sub_eq_add_neg, Function.Antiperiodic
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
⊢ f (-c) = -f 0

Tactic:
simpa only [zero_add] using h.neg 0

Premises used: Function.Antiperiodic.neg, zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocSemiring α
inst_1 : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
rwa : f (0 * c) = 0
rwa₁ rwa₂ rwa₃ rwa₄ : f 0 = 0
⊢ f ((↑0 : α) * c) = 0

Tactic:
rwa [Nat.cast_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, Nat.cast_zero
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocSemiring α
inst_1 : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f ((↑(n + 1) : α) * c) = 0

Tactic:
simp [add_mul, h _, Antiperiodic.nat_mul_eq_of_eq_zero h hi n]

Premises used: add_mul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocRing α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
rw : f ((↑n : α) * c) = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := β) 0 0
⊢ f ((↑(↑n : ℤ) : α) * c) = 0

Tactic:
rw [Int.cast_natCast, h.nat_mul_eq_of_eq_zero hi n]

Premises used: Int.cast_natCast, Function.Antiperiodic.nat_mul_eq_of_eq_zero
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocRing α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
rw : f (-(↑(n + 1) : α) * c) = 0
rw₁ : f (-((↑(n + 1) : α) * c)) = 0
rw₂ : f ((↑(n + 1) : α) * -c) = 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := β) 0 0
⊢ f ((↑(Int.negSucc n) : α) * c) = 0

Tactic:
rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]

Premises used: Function.Antiperiodic.neg, Int.cast_negSucc, Function.Antiperiodic.nat_mul_eq_of_eq_zero, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
inl : ∀ (k : ℤ), f (x + (2 * k) • c) = (↑(2 * k).negOnePow : ℤ) • f x
inr : ∀ (k : ℤ), f (x + (2 * k + 1) • c) = (↑(2 * k + 1).negOnePow : ℤ) • f x
⊢ f (x + n • c) = (↑n.negOnePow : ℤ) • f x

Tactic:
rcases Int.even_or_odd' n with ⟨k, rfl | rfl⟩

Premises used: Int.even_or_odd', rfl
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
inl : f x = (↑(2 * k).negOnePow : ℤ) • f x
inl₁ : f x = HSMul.hSMul (α := ℤ) (↑1 : ℤ) (f x)
inl₂ : f x = HSMul.hSMul (α := ℤ) 1 (f x)
inl₃ inl₄ : f x = f x
⊢ f (x + (2 * k) • c) = (↑(2 * k).negOnePow : ℤ) • f x

Tactic:
rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]

Premises used: Int.negOnePow_two_mul, one_zsmul, Function.Antiperiodic.even_zsmul_periodic, Units.val_one
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
inr : -f x = (↑(2 * k + 1).negOnePow : ℤ) • f x
inr₁ : -f x = HSMul.hSMul (α := ℤ) (↑(-1) : ℤ) (f x)
inr₂ : -f x = HSMul.hSMul (α := ℤ) (-(↑1 : ℤ)) (f x)
inr₃ : -f x = HSMul.hSMul (α := ℤ) (-1) (f x)
inr₄ : -f x = -HSMul.hSMul (α := ℤ) 1 (f x)
inr₅ inr₆ : -f x = -f x
⊢ f (x + (2 * k + 1) • c) = (↑(2 * k + 1).negOnePow : ℤ) • f x

Tactic:
rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg,
      Units.val_one, neg_zsmul, one_zsmul]

Premises used: neg_zsmul, Units.val_neg, Int.negOnePow_two_mul_add_one, Function.Antiperiodic.odd_zsmul_antiperiodic, one_zsmul, Units.val_one
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (x - n • c) = (↑n.negOnePow : ℤ) • f x

Tactic:
simpa only [sub_eq_add_neg, neg_zsmul, Int.negOnePow_neg] using h.add_zsmul_eq (-n)

Premises used: neg_zsmul, sub_eq_add_neg, Int.negOnePow_neg, Function.Antiperiodic.add_zsmul_eq, Neg.neg
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddCommGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
rw : f (-x + n • c) = (↑n.negOnePow : ℤ) • f (-x)
⊢ f (n • c - x) = (↑n.negOnePow : ℤ) • f (-x)

Tactic:
rw [sub_eq_add_neg, add_comm]

Premises used: sub_eq_add_neg, add_comm
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddCommGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (-x + n • c) = (↑n.negOnePow : ℤ) • f (-x)

Tactic:
h.add_zsmul_eq n

Premises used: Function.Antiperiodic.add_zsmul_eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddCommGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (-x + n • c) = (↑n.negOnePow : ℤ) • f (-x)

Tactic:
exact h.add_zsmul_eq n

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

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

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

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

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

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

Premises used: zsmul_eq_mul, Function.Antiperiodic.zsmul_sub_eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddMonoid α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
n : ℕ
inl : ∀ (k : ℕ), f (x + (2 * k) • c) = HPow.hPow (α := ℤ) (-1) (2 * k) • f x
inr : ∀ (k : ℕ), f (x + (2 * k + 1) • c) = HPow.hPow (α := ℤ) (-1) (2 * k + 1) • f x
⊢ f (x + n • c) = HPow.hPow (α := ℤ) (-1) n • f x

Tactic:
rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩

Premises used: Nat.even_or_odd', rfl
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddMonoid α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
inl : f x = HPow.hPow (α := ℤ) (-1) (2 * k) • f x
⊢ f (x + (2 * k) • c) = HPow.hPow (α := ℤ) (-1) (2 * k) • f x

Tactic:
rw [h.even_nsmul_periodic]

Premises used: Function.Antiperiodic.even_nsmul_periodic
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddMonoid α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ f x = HPow.hPow (α := ℤ) (-1) (2 * k) • f x

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddMonoid α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
inr : -f x = HPow.hPow (α := ℤ) (-1) (2 * k + 1) • f x
⊢ f (x + (2 * k + 1) • c) = HPow.hPow (α := ℤ) (-1) (2 * k + 1) • f x

Tactic:
rw [h.odd_nsmul_antiperiodic]

Premises used: Function.Antiperiodic.odd_nsmul_antiperiodic
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddMonoid α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ -f x = HPow.hPow (α := ℤ) (-1) (2 * k + 1) • f x

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
n : ℕ
⊢ f (x - n • c) = HPow.hPow (α := ℤ) (-1) n • f x

Tactic:
simpa only [Int.reduceNeg, natCast_zsmul] using h.sub_zsmul_eq n

Premises used: Int.reduceNeg, Nat.cast, natCast_zsmul, Function.Antiperiodic.sub_zsmul_eq
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddCommGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
n : ℕ
⊢ f (n • c - x) = HPow.hPow (α := ℤ) (-1) n • f (-x)

Tactic:
simpa only [Int.reduceNeg, natCast_zsmul] using h.zsmul_sub_eq n

Premises used: Int.reduceNeg, Nat.cast, Function.Antiperiodic.zsmul_sub_eq, natCast_zsmul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddSemigroup α
inst_1 : Neg β
h : Antiperiodic 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 α
inst_1 : Neg β
h : Antiperiodic 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 α
inst_1 : InvolutiveNeg β
h : Antiperiodic 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: Function.Antiperiodic.sub_eq, sub_sub
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : SubtractionCommMonoid α
inst_1 : Neg β
h : Antiperiodic f c
a : α
⊢ Antiperiodic.{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.Antiperiodic.add_const, Neg.neg
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : Add α
inst_1 : Monoid γ
inst_2 : AddGroup β
inst_3 : DistribMulAction γ β
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (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 : Neg β
inst_2 : Group γ
inst_3 : DistribMulAction γ α
h : Antiperiodic 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 : Neg β
inst_2 : Group γ
inst_3 : DistribMulAction γ α
h : Antiperiodic f c
a : γ
⊢ Antiperiodic.{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.Antiperiodic.const_smul
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst : AddSemigroup α
inst_1 : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic 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₁ c₂ : α
inst : AddGroup α
inst_1 : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic f c₂
⊢ Periodic f (c₁ - c₂)

Tactic:
simpa only [sub_eq_add_neg] using h1.add h2.neg

Premises used: Function.Antiperiodic.neg, sub_eq_add_neg, Function.Antiperiodic.add
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst : AddSemigroup α
inst_1 : Neg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic 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₁ c₂ : α
inst : AddGroup α
inst_1 : InvolutiveNeg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ - c₂)

Tactic:
simpa only [sub_eq_add_neg] using h1.add_antiperiod h2.neg

Premises used: Function.Antiperiodic.neg, sub_eq_add_neg, Function.Periodic.add_antiperiod
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst : AddMonoid α
inst_1 : Neg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ f (c₁ + c₂) = -f 0

Tactic:
(h1.add_antiperiod h2).eq

Premises used: Function.Antiperiodic.eq, Function.Periodic.add_antiperiod
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst : AddGroup α
inst_1 : InvolutiveNeg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ f (c₁ - c₂) = -f 0

Tactic:
(h1.sub_antiperiod h2).eq

Premises used: Function.Antiperiodic.eq, Function.Periodic.sub_antiperiod
-- Module: Mathlib.Algebra.Ring.Periodic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
c : α
inst : Add α
inst_1 : Mul β
inst_2 : HasDistribNeg β
hf : Antiperiodic f c
hg : Antiperiodic 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 : DivisionMonoid β
inst_2 : HasDistribNeg β
hf : Antiperiodic f c
hg : Antiperiodic g c
⊢ Periodic (f / g) c

Tactic:
simp_all [neg_div_neg_eq]

Premises used: neg_div_neg_eq
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type v
i : I
inst : (i : I) → Distrib (f i)
a b c : (i : I) → f i
h : ∀ (x : I), (a * (b + c)) x = (a * b + a * c) x
⊢ a * (b + c) = a * b + a * c

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type v
i : I
inst : (i : I) → Distrib (f i)
a b c : (i : I) → f i
x : I
⊢ (a * (b + c)) x = (a * b + a * c) x

Tactic:
mul_add _ _ _

Premises used: mul_add
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type v
i : I
inst : (i : I) → Distrib (f i)
a b c : (i : I) → f i
x : I
⊢ (a * (b + c)) x = (a * b + a * c) x

Tactic:
exact mul_add _ _ _

Premises used: mul_add
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type v
i : I
inst : (i : I) → Distrib (f i)
a b c : (i : I) → f i
h : ∀ (x : I), ((a + b) * c) x = (a * c + b * c) x
⊢ (a + b) * c = a * c + b * c

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type v
i : I
inst : (i : I) → Distrib (f i)
a b c : (i : I) → f i
x : I
⊢ ((a + b) * c) x = (a * c + b * c) x

Tactic:
add_mul _ _ _

Premises used: add_mul
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type v
i : I
inst : (i : I) → Distrib (f i)
a b c : (i : I) → f i
x : I
⊢ ((a + b) * c) x = (a * c + b * c) x

Tactic:
exact add_mul _ _ _

Premises used: add_mul
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type v
γ : Type w
inst : Nonempty I
inst_1 : (i : I) → NonUnitalNonAssocSemiring (f i)
inst_2 : NonUnitalNonAssocSemiring γ
g : (i : I) → NonUnitalRingHom.{w, v} γ (f i)
hg : ∀ (i : I), Function.Injective.{w + 1, v + 1} (α := γ) (β := f i) (⇑(g i) : (a : γ) → f i)
⊢ Function.Injective (α := γ) (β := (i : I) → f i) (⇑(Pi.nonUnitalRingHom (f := f) g) : (a : γ) → (i : I) → f i)

Tactic:
mulHom_injective (fun i => (g i).toMulHom) hg

Premises used: NonUnitalRingHom.toMulHom, Pi.mulHom_injective
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type v
γ : Type w
inst : Nonempty I
inst_1 : (i : I) → NonAssocSemiring (f i)
inst_2 : NonAssocSemiring γ
g : (i : I) → RingHom.{w, v} γ (f i)
hg : ∀ (i : I), Function.Injective.{w + 1, v + 1} (α := γ) (β := f i) (⇑(g i) : (a : γ) → f i)
⊢ Function.Injective (α := γ) (β := (i : I) → f i) (⇑(Pi.ringHom (f := f) g) : (a : γ) → (i : I) → f i)

Tactic:
monoidHom_injective (fun i => (g i).toMonoidHom) hg

Premises used: RingHom.toMonoidHom, Pi.monoidHom_injective
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type u_1
inst : (i : I) → Semiring (f i)
i : I
x : f i
⊢ (i : I) → f i

Tactic:
exact (if h : · = i then h ▸ x else 0)

Premises used: dite, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type u_1
inst : (i : I) → Semiring (f i)
i : I
x : f i
⊢ (i : I) → f i

Tactic:
classical exact (if h : · = i then h ▸ x else 0)
-- Module: Mathlib.Algebra.Ring.Pi
Goal:
I : Type u
f : I → Type u_1
inst : (i : I) → Semiring (f i)
i : I
x : f i
⊢ (((Pi.evalRingHom f i : ((i : I) → f i) →+* f i) : (a : (i : I) → f i) → f i) fun (x_1 : I) ↦
      if h : x_1 = i then Eq.rec (motive := fun (x : I) (h : i = x) ↦ f x) x ⋯ else 0) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Pointwise.Finset
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Distrib α
s t u : Finset α
⊢ s * (t + u) ⊆ s * t + s * u

Tactic:
image₂_distrib_subset_left mul_add

Premises used: Set.Mem, setOf, Finset.image₂_distrib_subset_left, mul_add
-- Module: Mathlib.Algebra.Ring.Pointwise.Finset
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Distrib α
s t u : Finset α
⊢ (s + t) * u ⊆ s * u + t * u

Tactic:
image₂_distrib_subset_right add_mul

Premises used: add_mul, Set.Mem, setOf, Finset.image₂_distrib_subset_right
-- Module: Mathlib.Algebra.Ring.Pointwise.Set
Goal:
α : Type u_1
inst : Mul α
inst_1 : HasDistribNeg α
x x_1 : Set α
simp_rw : (fun (x : α) ↦ -x) '' x * x_1 = (fun (x : α) ↦ -x) '' (x * x_1)
⊢ -x * x_1 = -(x * x_1)

Tactic:
simp_rw [← image_neg_eq_neg]

Premises used: Set.image_neg_eq_neg
-- Module: Mathlib.Algebra.Ring.Pointwise.Set
Goal:
α : Type u_1
inst : Mul α
inst_1 : HasDistribNeg α
x x_1 : Set α
⊢ (fun (x : α) ↦ -x) '' x * x_1 = (fun (x : α) ↦ -x) '' (x * x_1)

Tactic:
image2_image_left_comm neg_mul

Premises used: Set.image2_image_left_comm, neg_mul
-- Module: Mathlib.Algebra.Ring.Pointwise.Set
Goal:
α : Type u_1
inst : Mul α
inst_1 : HasDistribNeg α
x x_1 : Set α
⊢ (fun (x : α) ↦ -x) '' x * x_1 = (fun (x : α) ↦ -x) '' (x * x_1)

Tactic:
exact image2_image_left_comm neg_mul

Premises used: Set.image2_image_left_comm, neg_mul
-- Module: Mathlib.Algebra.Ring.Pointwise.Set
Goal:
α : Type u_1
inst : Mul α
inst_1 : HasDistribNeg α
x x_1 : Set α
simp_rw : x * (fun (x : α) ↦ -x) '' x_1 = (fun (x : α) ↦ -x) '' (x * x_1)
⊢ x * -x_1 = -(x * x_1)

Tactic:
simp_rw [← image_neg_eq_neg]

Premises used: Set.image_neg_eq_neg
-- Module: Mathlib.Algebra.Ring.Pointwise.Set
Goal:
α : Type u_1
inst : Mul α
inst_1 : HasDistribNeg α
x x_1 : Set α
⊢ x * (fun (x : α) ↦ -x) '' x_1 = (fun (x : α) ↦ -x) '' (x * x_1)

Tactic:
image_image2_right_comm mul_neg

Premises used: Set.image_image2_right_comm, mul_neg
-- Module: Mathlib.Algebra.Ring.Pointwise.Set
Goal:
α : Type u_1
inst : Mul α
inst_1 : HasDistribNeg α
x x_1 : Set α
⊢ x * (fun (x : α) ↦ -x) '' x_1 = (fun (x : α) ↦ -x) '' (x * x_1)

Tactic:
exact image_image2_right_comm mul_neg

Premises used: Set.image_image2_right_comm, mul_neg
-- Module: Mathlib.Algebra.Ring.Pointwise.Set
Goal:
α : Type u_1
inst : Distrib α
s t u : Set α
⊢ s * (t + u) ⊆ s * t + s * u

Tactic:
image2_distrib_subset_left mul_add

Premises used: Set.image2_distrib_subset_left, mul_add