awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Odd n₂
neg : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₁ : (¬Odd n₁ ↔ ¬Odd n₂) → Odd n₁
neg₂ neg₃ : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₄ : Odd n₁ → ¬Odd n₁ → ¬Odd n₂
neg₅ : Odd n₁ → ¬Odd n₂ → ¬Odd n₁
neg₆ : ¬Odd n₁ → ¬Odd n₂ → Odd n₁
neg₇ neg₈ neg₉ : ¬¬Odd n₁ → ¬¬Odd n₂ → Odd n₁
neg₁₀ : Odd n₁ → ¬Odd n₁ → ¬Odd n₂
neg₁₁ : Odd n₁ → ¬Odd n₂ → ¬Odd n₁
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
have neg₁₂ : Odd n₁ → Odd n₂ → Odd n₁
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
⊢ (↑(↑(negOnePow (↑n : ℤ)) : ℤ) : R) = HPow.hPow (α := R) (-1) n
have inl : ∀ (k : ℕ), (↑(↑(negOnePow (↑(2 * k) : ℤ)) : ℤ) : R) = HPow.hPow (α := R) (-1) (2 * k)
Tactic: obtain ⟨k, rfl | rfl⟩ := Nat.even_or_odd' n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
inl : ∀ (k : ℕ), (↑(↑(negOnePow (↑(2 * k) : ℤ)) : ℤ) : R) = HPow.hPow (α := R) (-1) (2 * k)
⊢ (↑(↑(negOnePow (↑n : ℤ)) : ℤ) : R) = HPow.hPow (α := R) (-1) n
have inr : ∀ (k : ℕ), (↑(↑(negOnePow (↑(2 * k + 1) : ℤ)) : ℤ) : R) = HPow.hPow (α := R) (-1) (2 * k + 1)
Tactic: obtain ⟨k, rfl | rfl⟩ := Nat.even_or_odd' n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℤ
⊢ (↑(↑n.negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) n.natAbs
have ofNat : ∀ (n : ℕ), (↑(↑(ofNat n).negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) (ofNat n).natAbs
Tactic: cases n with
  | ofNat n => exact cast_negOnePow_natCast R n
  | negSucc n => simp [negOnePow_def, Units.val_pow_eq_pow_val]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℤ
ofNat : ∀ (n : ℕ), (↑(↑(Int.ofNat n).negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) (Int.ofNat n).natAbs
⊢ (↑(↑n.negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) n.natAbs
have negSucc : ∀ (n : ℕ), (↑(↑-[n+1].negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) -[n+1].natAbs
Tactic: cases n with
  | ofNat n => exact cast_negOnePow_natCast R n
  | negSucc n => simp [negOnePow_def, Units.val_pow_eq_pow_val]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n_1 m_1 : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n_1) ((fun (n : ℕ) ↦ r ^ n) m_1)
n m : ℕ
h₁ : n ≤ m
h₂ : r ^ n = r ^ m
⊢ n = m
have obtain : ∀ (l : ℕ) (h₁ : n ≤ n + l) (h₂ : r ^ n = r ^ (n + l)), n = n + l
Tactic: obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le h₁
Cleared hypotheses: m, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n_1 m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n_1) ((fun (n : ℕ) ↦ r ^ n) m)
n l : ℕ
h₁ : n ≤ n + l
h₂ : r ^ n = r ^ (n + l)
⊢ n = n + l
have h₃ : l = 0
Tactic: rw [pow_add, eq_comm, IsLeftRegular.mul_left_eq_self_iff (hx.pow n), pow_eq_one_iff_right hx']
      at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n_1 m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n_1) ((fun (n : ℕ) ↦ r ^ n) m)
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
⊢ n = n + l
have rw : n = n + 0
Tactic: rw [h₂, Nat.add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n_1 m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n_1) ((fun (n : ℕ) ↦ r ^ n) m)
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
rw : n = n + 0
⊢ n = n + l
have rw₁ : n = n
Tactic: rw [h₂, Nat.add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n) ((fun (n : ℕ) ↦ r ^ n) m)
⊢ n = m
have main : ∀ {n m : ℕ} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m), n = m
Tactic: have main {n m} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m) : n = m := by
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le h₁
    rw [pow_add, eq_comm, IsLeftRegular.mul_left_eq_self_iff (hx.pow n), pow_eq_one_iff_right hx']
      at h₂
    rw [h₂, Nat.add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n) ((fun (n : ℕ) ↦ r ^ n) m)
main : ∀ {n m : ℕ} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m), n = m
⊢ n = m
have inl : ∀ (h : n ≤ m), n = m
Tactic: obtain h | h := Nat.le_or_le n m
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n) ((fun (n : ℕ) ↦ r ^ n) m)
main : ∀ {n m : ℕ} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m), n = m
inl : ∀ (h : n ≤ m), n = m
⊢ n = m
have inr : ∀ (h : m ≤ n), n = m
Tactic: obtain h | h := Nat.le_or_le n m
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : Finite R
h : IsLeftRegular r
⊢ IsUnit r
have rwa : Function.Bijective (β := R) fun (x : R) ↦ r * x
Tactic: rwa [IsUnit.isUnit_iff_mulLeft_bijective, ← Finite.injective_iff_bijective]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : Finite R
h : IsLeftRegular r
rwa : Function.Bijective (β := R) fun (x : R) ↦ r * x
⊢ IsUnit r
have rwa₁ : Function.Injective (β := R) fun (x : R) ↦ r * x
Tactic: rwa [IsUnit.isUnit_iff_mulLeft_bijective, ← Finite.injective_iff_bijective]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : Finite R
h : IsRightRegular r
⊢ IsUnit r
have rwa : Function.Bijective (β := R) fun (x : R) ↦ x * r
Tactic: rwa [IsUnit.isUnit_iff_mulRight_bijective, ← Finite.injective_iff_bijective]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : Finite R
h : IsRightRegular r
rwa : Function.Bijective (β := R) fun (x : R) ↦ x * r
⊢ IsUnit r
have rwa₁ : Function.Injective (β := R) fun (x : R) ↦ x * r
Tactic: rwa [IsUnit.isUnit_iff_mulRight_bijective, ← Finite.injective_iff_bijective]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
⊢ S ≤ nonZeroDivisorsLeft R ↔ ∀ (s : ↥S), IsLeftRegular (↑s : R)
have simp_rw : (∀ ⦃x : R⦄, x ∈ S → Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R : Submonoid R) x) ↔
  ∀ (s : ↥S), IsLeftRegular (↑s : R)
Tactic: simp_rw [SetLike.le_def, isLeftRegular_iff_mem_nonZeroDivisorsLeft, Subtype.forall]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
simp_rw :
  (∀ ⦃x : R⦄, x ∈ S → Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R : Submonoid R) x) ↔
    ∀ (s : ↥S), IsLeftRegular (↑s : R)
⊢ S ≤ nonZeroDivisorsLeft R ↔ ∀ (s : ↥S), IsLeftRegular (↑s : R)
have simp_rw₁ : (∀ ⦃x : R⦄, x ∈ S → Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R : Submonoid R) x) ↔
  ∀ (s : ↥S), Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) (↑s : R)
Tactic: simp_rw [SetLike.le_def, isLeftRegular_iff_mem_nonZeroDivisorsLeft, Subtype.forall]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
⊢ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRightRegular (↑s : R)
have simp_rw : (∀ ⦃x : R⦄, x ∈ S → Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R : Submonoid R) x) ↔
  ∀ (s : ↥S), IsRightRegular (↑s : R)
Tactic: simp_rw [SetLike.le_def, isRightRegular_iff_mem_nonZeroDivisorsRight, Subtype.forall]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
simp_rw :
  (∀ ⦃x : R⦄, x ∈ S → Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R : Submonoid R) x) ↔
    ∀ (s : ↥S), IsRightRegular (↑s : R)
⊢ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRightRegular (↑s : R)
have simp_rw₁ : (∀ ⦃x : R⦄, x ∈ S → Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R : Submonoid R) x) ↔
  ∀ (s : ↥S), Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) (↑s : R)
Tactic: simp_rw [SetLike.le_def, isRightRegular_iff_mem_nonZeroDivisorsRight, Subtype.forall]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
⊢ S ≤ R⁰ ↔ ∀ (s : ↥S), IsRegular (↑s : R)
have simp_rw : S ≤ nonZeroDivisorsLeft R ⊓ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
Tactic: simp_rw [nonZeroDivisors, le_inf_iff, le_nonZeroDivisorsLeft_iff_isLeftRegular,
    le_nonZeroDivisorsRight_iff_isRightRegular, isRegular_iff, forall_and]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
simp_rw : S ≤ nonZeroDivisorsLeft R ⊓ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
⊢ S ≤ R⁰ ↔ ∀ (s : ↥S), IsRegular (↑s : R)
have simp_rw₁ : S ≤ nonZeroDivisorsLeft R ∧ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
Tactic: simp_rw [nonZeroDivisors, le_inf_iff, le_nonZeroDivisorsLeft_iff_isLeftRegular,
    le_nonZeroDivisorsRight_iff_isRightRegular, isRegular_iff, forall_and]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
simp_rw : S ≤ nonZeroDivisorsLeft R ⊓ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
simp_rw₁ : S ≤ nonZeroDivisorsLeft R ∧ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
⊢ S ≤ R⁰ ↔ ∀ (s : ↥S), IsRegular (↑s : R)
have simp_rw₂ : (∀ (s : ↥S), IsLeftRegular (↑s : R)) ∧ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
Tactic: simp_rw [nonZeroDivisors, le_inf_iff, le_nonZeroDivisorsLeft_iff_isLeftRegular,
    le_nonZeroDivisorsRight_iff_isRightRegular, isRegular_iff, forall_and]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
simp_rw : S ≤ nonZeroDivisorsLeft R ⊓ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
simp_rw₁ : S ≤ nonZeroDivisorsLeft R ∧ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
simp_rw₂ : (∀ (s : ↥S), IsLeftRegular (↑s : R)) ∧ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
⊢ S ≤ R⁰ ↔ ∀ (s : ↥S), IsRegular (↑s : R)
have simp_rw₃ : ((∀ (s : ↥S), IsLeftRegular (↑s : R)) ∧ ∀ (s : ↥S), IsRightRegular (↑s : R)) ↔ ∀ (s : ↥S), IsRegular (↑s : R)
Tactic: simp_rw [nonZeroDivisors, le_inf_iff, le_nonZeroDivisorsLeft_iff_isLeftRegular,
    le_nonZeroDivisorsRight_iff_isRightRegular, isRegular_iff, forall_and]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
simp_rw : S ≤ nonZeroDivisorsLeft R ⊓ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
simp_rw₁ : S ≤ nonZeroDivisorsLeft R ∧ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
simp_rw₂ : (∀ (s : ↥S), IsLeftRegular (↑s : R)) ∧ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular (↑s : R)
simp_rw₃ : ((∀ (s : ↥S), IsLeftRegular (↑s : R)) ∧ ∀ (s : ↥S), IsRightRegular (↑s : R)) ↔ ∀ (s : ↥S), IsRegular (↑s : R)
⊢ S ≤ R⁰ ↔ ∀ (s : ↥S), IsRegular (↑s : R)
have simp_rw₄ : ((∀ (s : ↥S), IsLeftRegular (↑s : R)) ∧ ∀ (s : ↥S), IsRightRegular (↑s : R)) ↔
  ∀ (s : ↥S), IsLeftRegular (↑s : R) ∧ IsRightRegular (↑s : R)
Tactic: simp_rw [nonZeroDivisors, le_inf_iff, le_nonZeroDivisorsLeft_iff_isLeftRegular,
    le_nonZeroDivisorsRight_iff_isRightRegular, isRegular_iff, forall_and]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
a : R
inst_1 : Finite R
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid R) R⁰ a
have rw : IsUnit a ↔ IsRegular a
Tactic: rw [← isRegular_iff_mem_nonZeroDivisors, isRegular_iff_isUnit_of_finite]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : Ring R
a : R
inst_1 : Finite R
rw : IsUnit a ↔ IsRegular a
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid R) R⁰ a
have rw₁ : IsUnit a ↔ IsUnit a
Tactic: rw [← isRegular_iff_mem_nonZeroDivisors, isRegular_iff_isUnit_of_finite]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
r x y : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
⊢ x * r ∣ y * r ↔ x ∣ y
have simp_rw : r * x ∣ r * y ↔ x ∣ y
Tactic: simp_rw [← mul_comm r, dvd_cancel_left_mem_nonZeroDivisors hr]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Opposite (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (↑0 : R)) 0
have rw : Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op 0) 0
Tactic: rw [Nat.cast_zero, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Opposite (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
rw : Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op 0) 0
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (↑0 : R)) 0
have rw₁ : Eq.{u_1 + 1} (α := Rᵐᵒᵖ) 0 0
Tactic: rw [Nat.cast_zero, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Opposite (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
n : ℕ
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (↑(↑n : ℤ) : R)) (op (↑n : R))
have rw : Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (↑n : R)) (op (↑n : R))
Tactic: rw [Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Opposite (goal)
Goal:
R : Type u_1
inst : AddCommMonoidWithOne R
⊢ Eq.{u_1 + 1} (α := Rᵃᵒᵖ) (op (↑0 : R)) 0
have rw : Eq.{u_1 + 1} (α := Rᵃᵒᵖ) (op 0) 0
Tactic: rw [Nat.cast_zero, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Opposite (goal)
Goal:
R : Type u_1
inst : AddCommMonoidWithOne R
rw : Eq.{u_1 + 1} (α := Rᵃᵒᵖ) (op 0) 0
⊢ Eq.{u_1 + 1} (α := Rᵃᵒᵖ) (op (↑0 : R)) 0
have rw₁ : Eq.{u_1 + 1} (α := Rᵃᵒᵖ) 0 0
Tactic: rw [Nat.cast_zero, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
have simp_rw : (-a) ^ (2 * c) = a ^ (2 * c)
Tactic: simp_rw [← two_mul, pow_mul, neg_sq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
c : ℕ
a : α
simp_rw : (-a) ^ (2 * c) = a ^ (2 * c)
⊢ (-a) ^ (c + c) = a ^ (c + c)
have simp_rw₁ : HPow.hPow (β := ℕ) (-a) 2 ^ c = HPow.hPow (β := ℕ) a 2 ^ c
Tactic: simp_rw [← two_mul, pow_mul, neg_sq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
n : ℕ
h : Even n
⊢ HPow.hPow (α := α) (-1) n = 1
have rw : HPow.hPow (α := α) 1 n = 1
Tactic: rw [h.neg_pow, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
n : ℕ
h : Even n
rw : HPow.hPow (α := α) 1 n = 1
⊢ HPow.hPow (α := α) (-1) n = 1
have rw₁ : Eq.{u_2 + 1} (α := α) 1 1
Tactic: rw [h.neg_pow, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : AddMonoidWithOne α
⊢ 2 = HAdd.hAdd (α := α) 1 1
have rw : Eq.{u_2 + 1} (α := α) 2 2
Tactic: rw [one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
a : α
inst_2 : LeftDistribClass α
ha : Even a
b : α
⊢ Even (b * a)
have rcases : ∀ (k : α), Even (b * (k + k))
Tactic: rcases ha with ⟨k, rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
inst_2 : LeftDistribClass α
b k : α
⊢ Even (b * (k + k))
have h : b * (k + k) = b * k + b * k
Tactic: use b * k
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
inst_2 : LeftDistribClass α
b k : α
⊢ b * (k + k) = b * k + b * k
have h : b * k + b * k = b * k + b * k
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
a : α
inst_2 : RightDistribClass α
ha : Even a
b : α
⊢ Even (a * b)
have rcases : ∀ (k : α), Even ((k + k) * b)
Tactic: rcases ha with ⟨k, rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
inst_2 : RightDistribClass α
b k : α
⊢ Even ((k + k) * b)
have h : (k + k) * b = k * b + k * b
Tactic: use k * b
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
inst_2 : RightDistribClass α
b k : α
⊢ (k + k) * b = k * b + k * b
have h : k * b + k * b = k * b + k * b
Tactic: rw [add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
inst : NonAssocSemiring α
⊢ Eq.{u_4 + 1} (α := Set α) (Set.range fun (x : α) ↦ 2 * x) {a : α | Even a}
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (Set.range fun (x : α) ↦ 2 * x) x ↔ Membership.mem (γ := Set α) {a : α | Even a} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a : α
ha : Even a
n : ℕ
h : n + 1 ≠ 0
⊢ Even (a ^ (n + 1))
have rw : Even (a ^ n * a)
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
⊢ a = 2 * b + 1 ↔ a = 2 * b + 1
have rw : a = b + b + 1 ↔ a = b + b + 1
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
inst : Semiring α
⊢ Eq.{u_4 + 1} (α := Set α) (Set.range fun (x : α) ↦ 2 * x + 1) {a : α | Odd a}
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (Set.range fun (x : α) ↦ 2 * x + 1) x ↔ Membership.mem (γ := Set α) {a : α | Odd a} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
⊢ a + a + (2 * b + 1) = 2 * (a + b) + 1
have rw : a + a + (2 * b + 1) = 2 * a + 2 * b + 1
Tactic: rw [mul_add, ← two_mul, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : a + a + (2 * b + 1) = 2 * a + 2 * b + 1
⊢ a + a + (2 * b + 1) = 2 * (a + b) + 1
have rw₁ : 2 * a + (2 * b + 1) = 2 * a + 2 * b + 1
Tactic: rw [mul_add, ← two_mul, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : a + a + (2 * b + 1) = 2 * a + 2 * b + 1
rw₁ : 2 * a + (2 * b + 1) = 2 * a + 2 * b + 1
⊢ a + a + (2 * b + 1) = 2 * (a + b) + 1
have rw₂ : 2 * a + (2 * b + 1) = 2 * a + (2 * b + 1)
Tactic: rw [mul_add, ← two_mul, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
⊢ Even (2 * a + 1 + (2 * b + 1))
have refine : 2 * a + 1 + (2 * b + 1) = a + b + 1 + (a + b + 1)
Tactic: refine ⟨a + b + 1, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
⊢ 2 * a + 1 + (2 * b + 1) = a + b + 1 + (a + b + 1)
have rw : a + a + 1 + (b + b + 1) = a + b + 1 + (a + b + 1)
Tactic: rw [two_mul, two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
⊢ Odd ((2 * a + 1) * (2 * b + 1))
have refine : (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
Tactic: refine ⟨2 * a * b + b + a, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw₁ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₁ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw₂ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) = 2 * (2 * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₁ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₂ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) = 2 * (2 * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw₃ : 2 * a * (2 * b) + 1 * (2 * b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₁ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₂ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) = 2 * (2 * a * b + b + a) + 1
rw₃ : 2 * a * (2 * b) + 1 * (2 * b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw₄ : 2 * a * (2 * b) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₁ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₂ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) = 2 * (2 * a * b + b + a) + 1
rw₃ : 2 * a * (2 * b) + 1 * (2 * b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₄ : 2 * a * (2 * b) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw₅ : 2 * (a * (2 * b)) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₁ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₂ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) = 2 * (2 * a * b + b + a) + 1
rw₃ : 2 * a * (2 * b) + 1 * (2 * b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₄ : 2 * a * (2 * b) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₅ : 2 * (a * (2 * b)) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw₆ : 2 * (a * (2 * b) + b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]