awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
M : Type u_2
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
inst_2 : IsMulTorsionFree M
x : M
hx : x ≠ 1
hx' : x ≠ 0
⊢ Function.Injective.{1, u_2 + 1} (β := M) fun (n : ℕ) ↦ x ^ n

Tactic:
IsLeftRegular.pow_injective (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hx') hx

Premises used: IsLeftCancelMulZero.mul_left_cancel_of_ne_zero, IsLeftRegular.pow_injective
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
M : Type u_2
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
inst_2 : IsMulTorsionFree M
x : M
hx : x ≠ 1
hx' : x ≠ 0
n m : ℕ
⊢ x ^ n = x ^ m ↔ n = m

Tactic:
(pow_right_injective₀ hx hx').eq_iff

Premises used: Function.Injective.eq_iff, IsMulTorsionFree.pow_right_injective₀
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
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
rwa₁ rwa₂ rwa₃ rwa₄ : Function.Injective (β := R) fun (x : R) ↦ r * x
⊢ IsUnit r

Tactic:
rwa [IsUnit.isUnit_iff_mulLeft_bijective, ← Finite.injective_iff_bijective]

Premises used: Finite.injective_iff_bijective, IsUnit.isUnit_iff_mulLeft_bijective
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
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
rwa₁ rwa₂ rwa₃ rwa₄ : Function.Injective (β := R) fun (x : R) ↦ x * r
⊢ IsUnit r

Tactic:
rwa [IsUnit.isUnit_iff_mulRight_bijective, ← Finite.injective_iff_bijective]

Premises used: Finite.injective_iff_bijective, IsUnit.isUnit_iff_mulRight_bijective
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
r : R
⊢ IsLeftRegular r ↔ Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) r

Tactic:
isLeftRegular_iff_right_eq_zero_of_mul

Premises used: Set.Mem, setOf, isLeftRegular_iff_right_eq_zero_of_mul
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
r : R
⊢ IsRightRegular r ↔ Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r

Tactic:
isRightRegular_iff_left_eq_zero_of_mul

Premises used: Set.Mem, setOf, isRightRegular_iff_left_eq_zero_of_mul
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
r : R
⊢ IsRegular r ↔ Membership.mem (γ := Submonoid R) R⁰ r

Tactic:
isRegular_iff_eq_zero_of_mul

Premises used: isRegular_iff_eq_zero_of_mul, Set.Mem, setOf, Set.inter
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
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)
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)
⊢ S ≤ nonZeroDivisorsLeft R ↔ ∀ (s : ↥S), IsLeftRegular (↑s : R)

Tactic:
simp_rw [SetLike.le_def, isLeftRegular_iff_mem_nonZeroDivisorsLeft, Subtype.forall]

Premises used: SetLike.le_def, Subtype.forall, isLeftRegular_iff_mem_nonZeroDivisorsLeft
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
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)
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)
⊢ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRightRegular (↑s : R)

Tactic:
simp_rw [SetLike.le_def, isRightRegular_iff_mem_nonZeroDivisorsRight, Subtype.forall]

Premises used: isRightRegular_iff_mem_nonZeroDivisorsRight, SetLike.le_def, Subtype.forall
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
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)
simp_rw₄ :
  ((∀ (s : ↥S), IsLeftRegular (↑s : R)) ∧ ∀ (s : ↥S), IsRightRegular (↑s : R)) ↔
    ∀ (s : ↥S), IsLeftRegular (↑s : R) ∧ IsRightRegular (↑s : R)
⊢ 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]

Premises used: isRegular_iff, nonZeroDivisors, le_nonZeroDivisorsLeft_iff_isLeftRegular, le_inf_iff, le_nonZeroDivisorsRight_iff_isRightRegular, forall_and
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
x y r : R
hr : Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) r
⊢ r * x = r * y ↔ x = y

Tactic:
⟨(isLeftRegular_iff_mem_nonZeroDivisorsLeft.mpr hr ·), congr_arg (r * ·)⟩

Premises used: Iff.mpr, HMul.hMul, congr_arg, isLeftRegular_iff_mem_nonZeroDivisorsLeft, Iff.intro
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
x y r : R
hr : Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r
⊢ x * r = y * r ↔ x = y

Tactic:
⟨(isRightRegular_iff_mem_nonZeroDivisorsRight.mpr hr ·), congr_arg (· * r)⟩

Premises used: Iff.mpr, HMul.hMul, isRightRegular_iff_mem_nonZeroDivisorsRight, congr_arg, Iff.intro
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
x y r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
⊢ r * x = r * y ↔ x = y

Tactic:
mul_cancel_left_mem_nonZeroDivisorsLeft hr.1

Premises used: mul_cancel_left_mem_nonZeroDivisorsLeft, And.left
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
x y : R
c : ↥R⁰
⊢ (↑c : R) * x = (↑c : R) * y ↔ x = y

Tactic:
mul_cancel_left_mem_nonZeroDivisors c.prop

Premises used: mul_cancel_left_mem_nonZeroDivisors, Subtype.prop
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
x y r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
⊢ x * r = y * r ↔ x = y

Tactic:
mul_cancel_right_mem_nonZeroDivisorsRight hr.2

Premises used: And.right, mul_cancel_right_mem_nonZeroDivisorsRight
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
x y : R
c : ↥R⁰
⊢ x * (↑c : R) = y * (↑c : R) ↔ x = y

Tactic:
mul_cancel_right_mem_nonZeroDivisors c.prop

Premises used: mul_cancel_right_mem_nonZeroDivisors, Subtype.prop
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
a : R
inst_1 : Finite R
rw : IsUnit a ↔ IsRegular a
rw₁ rw₂ : IsUnit a ↔ IsUnit a
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid R) R⁰ a

Tactic:
rw [← isRegular_iff_mem_nonZeroDivisors, isRegular_iff_isUnit_of_finite]

Premises used: isRegular_iff_isUnit_of_finite, isRegular_iff_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
x y r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
⊢ r * x ∣ r * y ↔ x ∣ y

Tactic:
(isLeftRegular_iff_mem_nonZeroDivisorsLeft.mpr hr.1).dvd_cancel_left

Premises used: Iff.mpr, isLeftRegular_iff_mem_nonZeroDivisorsLeft, And.left, IsLeftRegular.dvd_cancel_left
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Ring R
x y : R
c : ↥R⁰
⊢ (↑c : R) * x ∣ (↑c : R) * y ↔ x ∣ y

Tactic:
dvd_cancel_left_mem_nonZeroDivisors c.prop

Premises used: dvd_cancel_left_mem_nonZeroDivisors, Subtype.prop
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r x y : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
simp_rw : r * x ∣ r * y ↔ x ∣ y
⊢ x * r ∣ y * r ↔ x ∣ y

Tactic:
simp_rw [← mul_comm r, dvd_cancel_left_mem_nonZeroDivisors hr]

Premises used: dvd_cancel_left_mem_nonZeroDivisors, mul_comm
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
x y : R
c : ↥R⁰
⊢ x * (↑c : R) ∣ y * (↑c : R) ↔ x ∣ y

Tactic:
dvd_cancel_right_mem_nonZeroDivisors c.prop

Premises used: dvd_cancel_right_mem_nonZeroDivisors, Subtype.prop
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : NatCast R
n : ℕ
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (↑n : R)) (↑n : Rᵐᵒᵖ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : NatCast R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : IntCast R
n : ℤ
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (↑n : R)) (↑n : Rᵐᵒᵖ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : NatCast R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (unop (↑n : Rᵐᵒᵖ)) (↑n : R)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : NatCast R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) (unop (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : IntCast R
n : ℤ
⊢ Eq.{u_1 + 1} (α := R) (unop (↑n : Rᵐᵒᵖ)) (↑n : R)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : AddMonoidWithOne R
rw : Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op 0) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := Rᵐᵒᵖ) 0 0
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (↑0 : R)) 0

Tactic:
rw [Nat.cast_zero, op_zero]

Premises used: MulOpposite.op_zero, Nat.cast_zero
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ ∀ (n : ℕ), op (↑(n + 1) : R) = HAdd.hAdd (α := Rᵐᵒᵖ) (op (↑n : R)) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : AddGroupWithOne R
n : ℕ
rw rw₁ : Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (↑n : R)) (op (↑n : R))
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (↑(↑n : ℤ) : R)) (op (↑n : R))

Tactic:
rw [Int.cast_natCast]

Premises used: Int.cast_natCast
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : AddGroupWithOne R
n : ℕ
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (op (↑(Int.negSucc n) : R)) (op (-unop (op (↑(n + 1) : R))))

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
⊢ IsDomain.{u_1} Rᵐᵒᵖ

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : AddCommMonoidWithOne R
rw : Eq.{u_1 + 1} (α := Rᵃᵒᵖ) (op 0) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := Rᵃᵒᵖ) 0 0
⊢ Eq.{u_1 + 1} (α := Rᵃᵒᵖ) (op (↑0 : R)) 0

Tactic:
rw [Nat.cast_zero, op_zero]

Premises used: Nat.cast_zero, AddOpposite.op_zero
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : AddCommMonoidWithOne R
⊢ ∀ (n : ℕ), op (↑(n + 1) : R) = HAdd.hAdd (α := Rᵃᵒᵖ) (op (↑n : R)) 1

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Ring.Opposite
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
⊢ IsDomain.{u_1} Rᵃᵒᵖ

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.Algebra.Ring.PUnit
Goal:
a : PUnit
⊢ 0 * a = 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.PUnit
Goal:
a : PUnit
⊢ a * 0 = 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.PUnit
Goal:
a b c : PUnit
⊢ a * (b + c) = a * b + a * c

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.PUnit
Goal:
a b c : PUnit
⊢ (a + b) * c = a * c + b * c

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.PUnit
Goal:
⊢ ∀ {a : PUnit.{u_1 + 1}}, a ≠ 0 → IsLeftRegular a

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.PUnit
Goal:
⊢ ∀ {a : PUnit.{u_1 + 1}}, a ≠ 0 → IsRightRegular a

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
c : ℕ
a : α
simp_rw : (-a) ^ (2 * c) = a ^ (2 * c)
simp_rw₁ : HPow.hPow (β := ℕ) (-a) 2 ^ c = HPow.hPow (β := ℕ) a 2 ^ c
⊢ (-a) ^ (c + c) = a ^ (c + c)

Tactic:
simp_rw [← two_mul, pow_mul, neg_sq]

Premises used: two_mul, neg_sq, pow_mul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
n : ℕ
h : Even n
rw : HPow.hPow (α := α) 1 n = 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := α) 1 1
⊢ HPow.hPow (α := α) (-1) n = 1

Tactic:
rw [h.neg_pow, one_pow]

Premises used: one_pow, Even.neg_pow
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : MulZeroClass α
⊢ IsSquare.{u_2} (α := α) 0

Tactic:
⟨0, (mul_zero _).symm⟩

Premises used: MulZeroClass.mul_zero, IsSquare, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : AddMonoidWithOne α
rw rw₁ : Eq.{u_2 + 1} (α := α) 2 2
⊢ 2 = HAdd.hAdd (α := α) 1 1

Tactic:
rw [one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
a : α
inst_2 : LeftDistribClass α
ha : Even a
b : α
rcases : ∀ (k : α), Even (b * (k + k))
⊢ Even (b * a)

Tactic:
rcases ha with ⟨k, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
inst_2 : LeftDistribClass α
b k : α
h : b * (k + k) = b * k + b * k
⊢ Even (b * (k + k))

Tactic:
use b * k
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
inst_2 : LeftDistribClass α
b k : α
h h₁ : b * k + b * k = b * k + b * k
⊢ b * (k + k) = b * k + b * k

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
a : α
inst_2 : RightDistribClass α
ha : Even a
b : α
rcases : ∀ (k : α), Even ((k + k) * b)
⊢ Even (a * b)

Tactic:
rcases ha with ⟨k, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
inst_2 : RightDistribClass α
b k : α
h : (k + k) * b = k * b + k * b
⊢ Even ((k + k) * b)

Tactic:
use k * b
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Add α
inst_1 : Mul α
inst_2 : RightDistribClass α
b k : α
h h₁ : k * b + k * b = k * b + k * b
⊢ (k + k) * b = k * b + k * b

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
⊢ Even a ↔ ∃ (b : α), a = 2 * b

Tactic:
simp [even_iff_exists_two_nsmul]

Premises used: even_iff_exists_two_nsmul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
⊢ Even a ↔ 2 ∣ a

Tactic:
simp [Even, Dvd.dvd, two_mul]

Premises used: Dvd.dvd, two_mul, Even
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
ha : Even a
hab : a ∣ b
⊢ Even b

Tactic:
even_iff_two_dvd.2 <| ha.two_dvd.trans hab

Premises used: Iff.mpr, Even.two_dvd, even_iff_two_dvd, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
hab : a ∣ b
ha : Even a
⊢ Even b

Tactic:
ha.trans_dvd hab

Premises used: Even.trans_dvd
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_4
inst : NonAssocSemiring α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (Set.range fun (x : α) ↦ 2 * x) x ↔ Membership.mem (γ := Set α) {a : α | Even a} x
⊢ Eq.{u_4 + 1} (α := Set α) (Set.range fun (x : α) ↦ 2 * x) {a : α | Even a}

Tactic:
ext x
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_4
inst : NonAssocSemiring α
x : α
⊢ Membership.mem (γ := Set α) (Set.range fun (x : α) ↦ 2 * x) x ↔ Membership.mem (γ := Set α) {a : α | Even a} x

Tactic:
simp [eq_comm, two_mul, Even]

Premises used: two_mul, eq_comm, Even
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
⊢ Even (2 * a)

Tactic:
⟨a, two_mul _⟩

Premises used: two_mul, Even, Exists.intro
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
ha : Even a
n : ℕ
h : n + 1 ≠ 0
rw : Even (a ^ n * a)
⊢ Even (a ^ (n + 1))

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
ha : Even a
n : ℕ
h : n + 1 ≠ 0
⊢ Even (a ^ n * a)

Tactic:
ha.mul_left _

Premises used: Even.mul_left
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
ha : Even a
n : ℕ
h : n + 1 ≠ 0
⊢ Even (a ^ n * a)

Tactic:
exact ha.mul_left _

Premises used: Even.mul_left
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw rw₁ : a = b + b + 1 ↔ a = b + b + 1
⊢ a = 2 * b + 1 ↔ a = 2 * b + 1

Tactic:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_4
inst : Semiring α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (Set.range fun (x : α) ↦ 2 * x + 1) x ↔ Membership.mem (γ := Set α) {a : α | Odd a} x
⊢ Eq.{u_4 + 1} (α := Set α) (Set.range fun (x : α) ↦ 2 * x + 1) {a : α | Odd a}

Tactic:
ext x
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_4
inst : Semiring α
x : α
⊢ Membership.mem (γ := Set α) (Set.range fun (x : α) ↦ 2 * x + 1) x ↔ Membership.mem (γ := Set α) {a : α | Odd a} x

Tactic:
simp [Odd, eq_comm]

Premises used: Odd, eq_comm
-- Module: Mathlib.Algebra.Ring.Parity
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
rw₂ rw₃ : 2 * a + (2 * b + 1) = 2 * a + (2 * b + 1)
⊢ a + a + (2 * b + 1) = 2 * (a + b) + 1

Tactic:
rw [mul_add, ← two_mul, add_assoc]

Premises used: add_assoc, two_mul, mul_add
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
⊢ Odd (a + a + (2 * b + 1))

Tactic:
exact ⟨a + b, by rw [mul_add, ← two_mul, add_assoc]⟩
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (b + a)

Tactic:
add_comm a b ▸ ha.add_odd hb

Premises used: Eq.rec, Even.add_odd, add_comm
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a + b)

Tactic:
add_comm a b ▸ hb.add_odd ha

Premises used: Eq.rec, Even.add_odd, add_comm, Eq.symm
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
⊢ Even (2 * a + 1 + (2 * b + 1))

Tactic:
⟨a + b + 1, ?_⟩

Premises used: HAdd.hAdd, Even, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
refine : 2 * a + 1 + (2 * b + 1) = a + b + 1 + (a + b + 1)
⊢ Even (2 * a + 1 + (2 * b + 1))

Tactic:
refine ⟨a + b + 1, ?_⟩
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : a + a + 1 + (b + b + 1) = a + b + 1 + (a + b + 1)
⊢ 2 * a + 1 + (2 * b + 1) = a + b + 1 + (a + b + 1)

Tactic:
rw [two_mul, two_mul]

Premises used: two_mul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
⊢ a + a + 1 + (b + b + 1) = a + b + 1 + (a + b + 1)

Tactic:
ac_rfl
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
⊢ Odd.{u_2} (α := α) 1

Tactic:
⟨0, (zero_add _).symm.trans (congr_arg (· + (1 : α)) (mul_zero _).symm)⟩

Premises used: Odd, zero_add, MulZeroClass.mul_zero, congr_arg, HAdd.hAdd, Exists.intro, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
h : Even a
⊢ Odd (a + 1)

Tactic:
h.add_odd odd_one

Premises used: Even.add_odd, odd_one
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
h : Even a
⊢ Odd (1 + a)

Tactic:
h.odd_add odd_one

Premises used: odd_one, Even.odd_add
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
h : Odd a
⊢ Even (a + 1)

Tactic:
h.add_odd odd_one

Premises used: Odd.add_odd, odd_one
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
h : Odd a
⊢ Even (1 + a)

Tactic:
odd_one.add_odd h

Premises used: Odd.add_odd, odd_one
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
⊢ Odd (2 * a + 1)

Tactic:
⟨_, rfl⟩

Premises used: Odd, Exists.intro, rfl
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
⊢ Odd (a + (a + 1))

Tactic:
simp [← add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
⊢ Odd (a + 1 + a)

Tactic:
simp [add_comm _ a]

Premises used: add_comm
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
⊢ Odd (a + (1 + a))

Tactic:
simp [add_comm 1 a]

Premises used: add_comm, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : Semiring β
inst_2 : FunLike F α β
inst_3 : RingHomClass F α β
f : F
a : α
⊢ (f : (a : α) → β) (2 * a + 1) = HMul.hMul (α := β) (β := β) (2 : β) ((f : (a : α) → β) a : β) + 1

Tactic:
simp [two_mul]

Premises used: two_mul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : Semiring β
inst_2 : FunLike F α β
inst_3 : RingHomClass F α β
f : F
a : α
⊢ Odd.{u_3} (α := β) ((f : (a : α) → β) (2 * a + 1) : β)

Tactic:
exact ⟨f a, by simp [two_mul]⟩
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : Semiring R
n : ℕ
hn : Odd n
⊢ Odd.{u_4} (α := R) (↑n : R)

Tactic:
hn.map <| Nat.castRingHom R

Premises used: Odd.map, Nat.castRingHom
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
⊢ Odd ((2 * a + 1) * (2 * b + 1))

Tactic:
⟨2 * a * b + b + a, ?_⟩

Premises used: HMul.hMul, Odd, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
refine : (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
⊢ Odd ((2 * a + 1) * (2 * b + 1))

Tactic:
refine ⟨2 * a * b + b + a, ?_⟩
-- Module: Mathlib.Algebra.Ring.Parity
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
rw₆ : 2 * (a * (2 * b) + b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₇ : 2 * (a * (2 * b) + b + a) + 1 = 2 * (2 * a * b + b + a) + 1
rw₈ : 2 * (a * 2 * b + b + a) + 1 = 2 * (2 * a * b + b + a) + 1
rw₉ : (↑2 : α) * (a * (↑2 : α) * b + b + a) + 1 = (↑2 : α) * ((↑2 : α) * a * b + b + a) + 1
rw₁₀ rw₁₁ : (↑2 : α) * ((↑2 : α) * a * b + b + a) + 1 = (↑2 : α) * ((↑2 : α) * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 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]

Premises used: Nat.cast_comm, add_mul, add_assoc, mul_assoc, mul_add, mul_one, Nat.cast_two, one_mul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
ha : Odd a
⊢ Odd (HPow.hPow (β := ℕ) a 0)

Tactic:
simp [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
ha : Odd a
n : ℕ
hrec : Odd (a ^ n)
succ : Odd (a ^ n * a)
⊢ Odd (a ^ (n + 1))

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
ha : Odd a
n : ℕ
hrec : Odd (a ^ n)
⊢ Odd (a ^ n * a)

Tactic:
hrec.mul ha

Premises used: Odd.mul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
ha : Odd a
n : ℕ
hrec : Odd (a ^ n)
⊢ Odd (a ^ n * a)

Tactic:
exact hrec.mul ha

Premises used: Odd.mul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a : α
n : ℕ
ha : Odd a
zero : Odd (HPow.hPow (β := ℕ) a 0)
succ : ∀ (n : ℕ) (hrec : Odd (a ^ n)), Odd (a ^ (n + 1))
⊢ Odd (a ^ n)

Tactic:
induction n with
  | zero => simp [pow_zero]
  | succ n hrec => rw [pow_succ]; exact hrec.mul ha

Premises used: pow_succ, pow_zero
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
n : ℕ
inst_1 : IsCancelAdd α
hn : Odd n
hab : a + b = 0
obtain : ∀ (k : ℕ), a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a ^ n + b ^ n = 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Premises used: rfl