awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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)
⊢ f a = f b
have obtain : ∀ (k : ℤ) (hk : (fun (x : ℤ) ↦ x • c) k = -a + b), f a = f b
Tactic: obtain ⟨k, hk⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddMonoid α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + (2 * n + 1) • c) = -f x
have rw : f (x + ((2 * n) • c + HSMul.hSMul (α := ℕ) 1 c)) = -f x
Tactic: rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + (2 * n + 1) • c) = -f x
have rw₁ : f (x + ((2 * n) • c + c)) = -f x
Tactic: rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + (2 * n + 1) • c) = -f x
have rw₂ : f (x + (2 * n) • c + c) = -f x
Tactic: rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + (2 * n + 1) • c) = -f x
have rw₃ : -f (x + (2 * n) • c) = -f x
Tactic: rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + (2 * n + 1) • c) = -f x
have rw₄ : -f x = -f x
Tactic: rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocSemiring α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + ((↑n : α) * (2 * c) + c)) = -f x
have rw : f (x + (↑n : α) * (2 * c) + c) = -f x
Tactic: rw [← add_assoc, h, h.nat_even_mul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + ((↑n : α) * (2 * c) + c)) = -f x
have rw₁ : -f (x + (↑n : α) * (2 * c)) = -f x
Tactic: rw [← add_assoc, h, h.nat_even_mul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + ((↑n : α) * (2 * c) + c)) = -f x
have rw₂ : -f x = -f x
Tactic: rw [← add_assoc, h, h.nat_even_mul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f ((2 * n) • c)
have rw : Periodic f (n • HSMul.hSMul (α := ℕ) 2 c)
Tactic: rw [mul_comm, mul_zsmul, two_zsmul, ← two_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + (2 * n + 1) • c) = -f x
have rw : f (x + ((2 * n) • c + HSMul.hSMul (α := ℤ) 1 c)) = -f x
Tactic: rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + (2 * n + 1) • c) = -f x
have rw₁ : f (x + ((2 * n) • c + c)) = -f x
Tactic: rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + (2 * n + 1) • c) = -f x
have rw₂ : f (x + (2 * n) • c + c) = -f x
Tactic: rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + (2 * n + 1) • c) = -f x
have rw₃ : -f (x + (2 * n) • c) = -f x
Tactic: rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + (2 * n + 1) • c) = -f x
have rw₄ : -f x = -f x
Tactic: rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocRing α
inst_1 : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + ((↑n : α) * (2 * c) + c)) = -f x
have rw : f (x + (↑n : α) * (2 * c) + c) = -f x
Tactic: rw [← add_assoc, h, h.int_even_mul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + ((↑n : α) * (2 * c) + c)) = -f x
have rw₁ : -f (x + (↑n : α) * (2 * c)) = -f x
Tactic: rw [← add_assoc, h, h.int_even_mul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + ((↑n : α) * (2 * c) + c)) = -f x
have rw₂ : -f x = -f x
Tactic: rw [← add_assoc, h, h.int_even_mul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocSemiring α
inst_1 : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
⊢ f ((↑0 : α) * c) = 0
have rwa : f (0 * c) = 0
Tactic: rwa [Nat.cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocRing α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f ((↑(↑n : ℤ) : α) * c) = 0
have rw : f ((↑n : α) * c) = 0
Tactic: rw [Int.cast_natCast, h.nat_mul_eq_of_eq_zero hi n]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f ((↑(↑n : ℤ) : α) * c) = 0
have rw₁ : Eq.{u_2 + 1} (α := β) 0 0
Tactic: rw [Int.cast_natCast, h.nat_mul_eq_of_eq_zero hi n]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : NonAssocRing α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f ((↑(Int.negSucc n) : α) * c) = 0
have rw : f (-(↑(n + 1) : α) * c) = 0
Tactic: rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f ((↑(Int.negSucc n) : α) * c) = 0
have rw₁ : f (-((↑(n + 1) : α) * c)) = 0
Tactic: rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f ((↑(Int.negSucc n) : α) * c) = 0
have rw₂ : f ((↑(n + 1) : α) * -c) = 0
Tactic: rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f ((↑(Int.negSucc n) : α) * c) = 0
have rw₃ : Eq.{u_2 + 1} (α := β) 0 0
Tactic: rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
have inl : ∀ (k : ℤ), f (x + (2 * k) • c) = (↑(2 * k).negOnePow : ℤ) • f x
Tactic: rcases Int.even_or_odd' n with ⟨k, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + n • c) = (↑n.negOnePow : ℤ) • f x
have inr : ∀ (k : ℤ), f (x + (2 * k + 1) • c) = (↑(2 * k + 1).negOnePow : ℤ) • f x
Tactic: rcases Int.even_or_odd' n with ⟨k, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k) • c) = (↑(2 * k).negOnePow : ℤ) • f x
have inl : f x = (↑(2 * k).negOnePow : ℤ) • f x
Tactic: rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + (2 * k) • c) = (↑(2 * k).negOnePow : ℤ) • f x
have inl₁ : f x = HSMul.hSMul (α := ℤ) (↑1 : ℤ) (f x)
Tactic: rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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)
⊢ f (x + (2 * k) • c) = (↑(2 * k).negOnePow : ℤ) • f x
have inl₂ : f x = HSMul.hSMul (α := ℤ) 1 (f x)
Tactic: rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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)
⊢ f (x + (2 * k) • c) = (↑(2 * k).negOnePow : ℤ) • f x
have inl₃ : f x = f x
Tactic: rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k + 1) • c) = (↑(2 * k + 1).negOnePow : ℤ) • f x
have inr : -f x = (↑(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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + (2 * k + 1) • c) = (↑(2 * k + 1).negOnePow : ℤ) • f x
have inr₁ : -f x = HSMul.hSMul (α := ℤ) (↑(-1) : ℤ) (f x)
Tactic: rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg,
      Units.val_one, neg_zsmul, one_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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)
⊢ f (x + (2 * k + 1) • c) = (↑(2 * k + 1).negOnePow : ℤ) • f x
have inr₂ : -f x = HSMul.hSMul (α := ℤ) (-(↑1 : ℤ)) (f x)
Tactic: rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg,
      Units.val_one, neg_zsmul, one_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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)
⊢ f (x + (2 * k + 1) • c) = (↑(2 * k + 1).negOnePow : ℤ) • f x
have inr₃ : -f x = HSMul.hSMul (α := ℤ) (-1) (f x)
Tactic: rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg,
      Units.val_one, neg_zsmul, one_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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)
⊢ f (x + (2 * k + 1) • c) = (↑(2 * k + 1).negOnePow : ℤ) • f x
have inr₄ : -f x = -HSMul.hSMul (α := ℤ) 1 (f x)
Tactic: rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg,
      Units.val_one, neg_zsmul, one_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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)
⊢ f (x + (2 * k + 1) • c) = (↑(2 * k + 1).negOnePow : ℤ) • f x
have inr₅ : -f x = -f x
Tactic: rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg,
      Units.val_one, neg_zsmul, one_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddCommGroup α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (n • c - x) = (↑n.negOnePow : ℤ) • f (-x)
have rw : f (-x + n • c) = (↑n.negOnePow : ℤ) • f (-x)
Tactic: rw [sub_eq_add_neg, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddMonoid α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
n : ℕ
⊢ f (x + n • c) = HPow.hPow (α := ℤ) (-1) n • f x
have inl : ∀ (k : ℕ), f (x + (2 * k) • c) = HPow.hPow (α := ℤ) (-1) (2 * k) • f x
Tactic: rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
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
⊢ f (x + n • c) = HPow.hPow (α := ℤ) (-1) n • f x
have inr : ∀ (k : ℕ), f (x + (2 * k + 1) • c) = HPow.hPow (α := ℤ) (-1) (2 * k + 1) • f x
Tactic: rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddMonoid α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k) • c) = HPow.hPow (α := ℤ) (-1) (2 * k) • f x
have inl : f x = HPow.hPow (α := ℤ) (-1) (2 * k) • f x
Tactic: rw [h.even_nsmul_periodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : AddMonoid α
inst_1 : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k + 1) • c) = HPow.hPow (α := ℤ) (-1) (2 * k + 1) • f x
have inr : -f x = HPow.hPow (α := ℤ) (-1) (2 * k + 1) • f x
Tactic: rw [h.odd_nsmul_antiperiodic]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Pi (goal)
Goal:
I : Type u
f : I → Type v
i : I
inst : (i : I) → Distrib (f i)
a b c : (i : I) → f i
⊢ a * (b + c) = a * b + a * c
have h : ∀ (x : I), (a * (b + c)) x = (a * b + a * c) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Pi (goal)
Goal:
I : Type u
f : I → Type v
i : I
inst : (i : I) → Distrib (f i)
a b c : (i : I) → f i
⊢ (a + b) * c = a * c + b * c
have h : ∀ (x : I), ((a + b) * c) x = (a * c + b * c) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : HasDistribNeg α
x x_1 : Set α
⊢ -x * x_1 = -(x * x_1)
have simp_rw : (fun (x : α) ↦ -x) '' x * x_1 = (fun (x : α) ↦ -x) '' (x * x_1)
Tactic: simp_rw [← image_neg_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : HasDistribNeg α
x x_1 : Set α
⊢ x * -x_1 = -(x * x_1)
have simp_rw : x * (fun (x : α) ↦ -x) '' x_1 = (fun (x : α) ↦ -x) '' (x * x_1)
Tactic: simp_rw [← image_neg_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Prod (goal)
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
⊢ x * (x_1 + x_2) = x * x_1 + x * x_2
have fst : (x * (x_1 + x_2)).1 = (x * x_1 + x * x_2).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Prod (goal)
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
fst : (x * (x_1 + x_2)).1 = (x * x_1 + x * x_2).1
⊢ x * (x_1 + x_2) = x * x_1 + x * x_2
have snd : (x * (x_1 + x_2)).2 = (x * x_1 + x * x_2).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Prod (goal)
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
⊢ (x + x_1) * x_2 = x * x_2 + x_1 * x_2
have fst : ((x + x_1) * x_2).1 = (x * x_2 + x_1 * x_2).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Prod (goal)
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
fst : ((x + x_1) * x_2).1 = (x * x_2 + x_1 * x_2).1
⊢ (x + x_1) * x_2 = x * x_2 + x_1 * x_2
have snd : ((x + x_1) * x_2).2 = (x * x_2 + x_1 * x_2).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Prod (goal)
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : Subsingleton S
x : R × S
⊢ (fun (x : R) ↦ ((x, 0) : R × S)) x.1 = x
have mk : ∀ (fst : R) (snd : S), (fun (x : R) ↦ ((x, 0) : R × S)) (fst, snd).1 = (fst, snd)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Ring.Prod (goal)
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : Subsingleton S
x : S × R
⊢ (fun (x : R) ↦ ((0, x) : S × R)) x.2 = x
have mk : ∀ (fst : S) (snd : R), (fun (x : R) ↦ ((0, x) : S × R)) (fst, snd).2 = (fst, snd)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Ring.Prod (hypothesis)
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
⊢ False
have this : Eq (α := R × S) (0, 1) 0 ∨ Eq (α := R × S) (1, 0) 0
Tactic: have :=
    NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Prod (hypothesis)
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
this : Eq (α := R × S) (0, 1) 0 ∨ Eq (α := R × S) (1, 0) 0
⊢ False
have this₁ : Eq.{u_6 + 1} (α := R) 0 0 ∧ Eq.{u_7 + 1} (α := S) 1 0 ∨ Eq.{u_6 + 1} (α := R) 1 0 ∧ Eq.{u_7 + 1} (α := S) 0 0
Tactic: rw [Prod.mk_eq_zero, Prod.mk_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Prod (goal)
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
this : Eq.{u_6 + 1} (α := R) 0 0 ∧ Eq.{u_7 + 1} (α := S) 1 0 ∨ Eq.{u_6 + 1} (α := R) 1 0 ∧ Eq.{u_7 + 1} (α := S) 0 0
⊢ False
have inl : Eq.{u_6 + 1} (α := R) 0 0 → ∀ (h : Eq.{u_7 + 1} (α := S) 1 0), False
Tactic: rcases this with (⟨_, h⟩ | ⟨h, _⟩)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Prod (goal)
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
this : Eq.{u_6 + 1} (α := R) 0 0 ∧ Eq.{u_7 + 1} (α := S) 1 0 ∨ Eq.{u_6 + 1} (α := R) 1 0 ∧ Eq.{u_7 + 1} (α := S) 0 0
inl : Eq.{u_6 + 1} (α := R) 0 0 → ∀ (h : Eq.{u_7 + 1} (α := S) 1 0), False
⊢ False
have inr : ∀ (h : Eq.{u_6 + 1} (α := R) 1 0), Eq.{u_7 + 1} (α := S) 0 0 → False
Tactic: rcases this with (⟨_, h⟩ | ⟨h, _⟩)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
x : ℕ
x_1 : ℚ
⊢ HPow.hPow (β := ℤ) x_1 (↑x.succ : ℤ) = HPow.hPow (β := ℤ) x_1 (↑x : ℤ) * x_1
have rw : x_1 ^ x.succ = HPow.hPow (β := ℤ) x_1 (↑x : ℤ) * x_1
Tactic: rw [Rat.zpow_natCast, Rat.zpow_natCast, Rat.pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
x : ℕ
x_1 : ℚ
rw : x_1 ^ x.succ = HPow.hPow (β := ℤ) x_1 (↑x : ℤ) * x_1
⊢ HPow.hPow (β := ℤ) x_1 (↑x.succ : ℤ) = HPow.hPow (β := ℤ) x_1 (↑x : ℤ) * x_1
have rw₁ : x_1 ^ x.succ = x_1 ^ x * x_1
Tactic: rw [Rat.zpow_natCast, Rat.zpow_natCast, Rat.pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
x : ℕ
x_1 : ℚ
rw : x_1 ^ x.succ = HPow.hPow (β := ℤ) x_1 (↑x : ℤ) * x_1
rw₁ : x_1 ^ x.succ = x_1 ^ x * x_1
⊢ HPow.hPow (β := ℤ) x_1 (↑x.succ : ℤ) = HPow.hPow (β := ℤ) x_1 (↑x : ℤ) * x_1
have rw₂ : x_1 ^ x * x_1 = x_1 ^ x * x_1
Tactic: rw [Rat.zpow_natCast, Rat.zpow_natCast, Rat.pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x / (d /. x) = n /. d
have rw : n /. x * (d /. x)⁻¹ = n /. d
Tactic: rw [div_eq_mul_inv, inv_divInt, divInt_mul_divInt_cancel hx]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
rw : n /. x * (d /. x)⁻¹ = n /. d
⊢ n /. x / (d /. x) = n /. d
have rw₁ : n /. x * (x /. d) = n /. d
Tactic: rw [div_eq_mul_inv, inv_divInt, divInt_mul_divInt_cancel hx]