Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Damiano Testa

! This file was ported from Lean 3 source module algebra.parity
! leanprover-community/mathlib commit 8631e2d5ea77f6c13054d9151d82b83069680cb1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GroupPower.Lemmas
import Mathlib.Data.Nat.Cast.Basic

/-!  # Squares, even and odd elements

This file proves some general facts about squares, even and odd elements of semirings.

In the implementation, we define `IsSquare` and we let `Even` be the notion transported by
`to_additive`.  The definition are therefore as follows:
```lean
IsSquare a ↔ ∃ r, a = r * r
Even a ↔ ∃ r, a = r + r
```

Odd elements are not unified with a multiplicative notion.

## Future work

* TODO: Try to generalize further the typeclass assumptions on `IsSquare/Even`.
For instance, in some cases, there are `Semiring` assumptions that I (DT) am not convinced are
necessary.
* TODO: Consider moving the definition and lemmas about `Odd` to a separate file.
* TODO: The "old" definition of `Even a` asked for the existence of an element `c` such that
`a = 2 * c`.  For this reason, several fixes introduce an extra `two_mul` or `← two_mul`.
It might be the case that by making a careful choice of `simp` lemma, this can be avoided.
-/

open MulOpposite

variable {F: Type ?u.75153F α: Type ?u.5α β: Type ?u.75159β R: Type ?u.75162R : Type _: Type (?u.11+1)Type _}

section Mul

variable [Mul: Type ?u.146 → Type ?u.146Mul α: Type ?u.32α]

/-- An element `a` of a type `α` with multiplication satisfies `IsSquare a` if `a = r * r`,
for some `r : α`. -/
"An element `a` of a type `α` with addition satisfies `Even a` if `a = r + r`,
for some `r : α`."]
def IsSquare: {α : Type u_1} → [inst : Mul α] → α → PropIsSquare (a: αa : α: Type ?u.32α) : Prop: TypeProp :=
∃ r: ?m.51r, a: αa = r: ?m.51r * r: ?m.51r
#align is_square IsSquare: {α : Type u_1} → [inst : Mul α] → α → PropIsSquare
#align even Even: {α : Type u_1} → [inst : Add α] → α → PropEven

@[to_additive: ∀ {α : Type u_1} [inst : Add α] (m : α), Even (m + m)to_additive (attr := simp)]
theorem isSquare_mul_self: ∀ (m : α), IsSquare (m * m)isSquare_mul_self (m: αm : α: Type ?u.137α) : IsSquare: {α : Type ?u.151} → [inst : Mul α] → α → PropIsSquare (m: αm * m: αm) :=
⟨m: αm, rfl: ∀ {α : Sort ?u.249} {a : α}, a = arfl⟩
#align is_square_mul_self isSquare_mul_self: ∀ {α : Type u_1} [inst : Mul α] (m : α), IsSquare (m * m)isSquare_mul_self

theorem isSquare_op_iff: ∀ (a : α), IsSquare (op a) ↔ IsSquare aisSquare_op_iff (a: αa : α: Type ?u.314α) : IsSquare: {α : Type ?u.328} → [inst : Mul α] → α → PropIsSquare (op: {α : Type ?u.331} → α → αᵐᵒᵖop a: αa) ↔ IsSquare: {α : Type ?u.356} → [inst : Mul α] → α → PropIsSquare a: αa :=
⟨fun ⟨c: αᵐᵒᵖc, hc: op a = c * chc⟩ => ⟨unop: {α : Type ?u.419} → αᵐᵒᵖ → αunop c: αᵐᵒᵖc, byGoals accomplished! 🐙 F: Type ?u.311α: Type u_1β: Type ?u.317R: Type ?u.320inst✝: Mul αa: αx✝: IsSquare (op a)c: αᵐᵒᵖhc: op a = c * ca = unop c * unop crw [F: Type ?u.311α: Type u_1β: Type ?u.317R: Type ?u.320inst✝: Mul αa: αx✝: IsSquare (op a)c: αᵐᵒᵖhc: op a = c * ca = unop c * unop c← unop_mul: ∀ {α : Type ?u.593} [inst : Mul α] (x y : αᵐᵒᵖ), unop (x * y) = unop y * unop xunop_mul,F: Type ?u.311α: Type u_1β: Type ?u.317R: Type ?u.320inst✝: Mul αa: αx✝: IsSquare (op a)c: αᵐᵒᵖhc: op a = c * ca = unop (c * c) F: Type ?u.311α: Type u_1β: Type ?u.317R: Type ?u.320inst✝: Mul αa: αx✝: IsSquare (op a)c: αᵐᵒᵖhc: op a = c * ca = unop c * unop c← hc: op a = c * chc,F: Type ?u.311α: Type u_1β: Type ?u.317R: Type ?u.320inst✝: Mul αa: αx✝: IsSquare (op a)c: αᵐᵒᵖhc: op a = c * ca = unop (op a) F: Type ?u.311α: Type u_1β: Type ?u.317R: Type ?u.320inst✝: Mul αa: αx✝: IsSquare (op a)c: αᵐᵒᵖhc: op a = c * ca = unop c * unop cunop_op: ∀ {α : Type ?u.671} (x : α), unop (op x) = xunop_opF: Type ?u.311α: Type u_1β: Type ?u.317R: Type ?u.320inst✝: Mul αa: αx✝: IsSquare (op a)c: αᵐᵒᵖhc: op a = c * ca = a]Goals accomplished! 🐙⟩, fun ⟨c: αc, hc: a = c * chc⟩ => byGoals accomplished! 🐙 F: Type ?u.311α: Type u_1β: Type ?u.317R: Type ?u.320inst✝: Mul αa: αx✝: IsSquare ac: αhc: a = c * cIsSquare (op a)simp [hc: a = c * chc]Goals accomplished! 🐙⟩
#align is_square_op_iff isSquare_op_iff: ∀ {α : Type u_1} [inst : Mul α] (a : α), IsSquare (op a) ↔ IsSquare aisSquare_op_iff
#align even_op_iff even_op_iff: ∀ {α : Type u_1} [inst : Add α] (a : α), Even (AddOpposite.op a) ↔ Even aeven_op_iff

end Mul

theorem isSquare_one: ∀ [inst : MulOneClass α], IsSquare 1isSquare_one [MulOneClass: Type ?u.888 → Type ?u.888MulOneClass α: Type ?u.879α] : IsSquare: {α : Type ?u.891} → [inst : Mul α] → α → PropIsSquare (1: ?m.9191 : α: Type ?u.879α) :=
⟨1: ?m.16621, (mul_one: ∀ {M : Type ?u.2125} [inst : MulOneClass M] (a : M), a * 1 = amul_one _: ?m.2126_).symm: ∀ {α : Sort ?u.2140} {a b : α}, a = b → b = asymm⟩
#align is_square_one isSquare_one: ∀ {α : Type u_1} [inst : MulOneClass α], IsSquare 1isSquare_one
#align even_zero even_zero: ∀ {α : Type u_1} [inst : AddZeroClass α], Even 0even_zero

@[to_additive: ∀ {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
[inst_2 : AddMonoidHomClass F α β] {m : α} (f : F), Even m → Even (↑f m)to_additive]
theorem IsSquare.map: ∀ [inst : MulOneClass α] [inst_1 : MulOneClass β] [inst_2 : MonoidHomClass F α β] {m : α} (f : F),
IsSquare m → IsSquare (↑f m)IsSquare.map [MulOneClass: Type ?u.2221 → Type ?u.2221MulOneClass α: Type ?u.2212α] [MulOneClass: Type ?u.2224 → Type ?u.2224MulOneClass β: Type ?u.2215β] [MonoidHomClass: Type ?u.2229 →
(M : outParam (Type ?u.2228)) →
(N : outParam (Type ?u.2227)) →
[inst : MulOneClass M] → [inst : MulOneClass N] → Type (max(max?u.2229?u.2228)?u.2227)MonoidHomClass F: Type ?u.2209F α: Type ?u.2212α β: Type ?u.2215β] {m: αm : α: Type ?u.2212α} (f: Ff : F: Type ?u.2209F) :
IsSquare: {α : Type ?u.2249} → [inst : Mul α] → α → PropIsSquare m: αm → IsSquare: {α : Type ?u.2588} → [inst : Mul α] → α → PropIsSquare (f: Ff m: αm) := byGoals accomplished! 🐙
F: Type u_3α: Type u_1β: Type u_2R: Type ?u.2218inst✝²: MulOneClass αinst✝¹: MulOneClass βinst✝: MonoidHomClass F α βm: αf: FIsSquare m → IsSquare (↑f m)rintro ⟨m, rfl⟩: IsSquare m⟨m: αm⟨m, rfl⟩: IsSquare m, rfl: m✝ = m * mrfl⟨m, rfl⟩: IsSquare m⟩F: Type u_3α: Type u_1β: Type u_2R: Type ?u.2218inst✝²: MulOneClass αinst✝¹: MulOneClass βinst✝: MonoidHomClass F α βf: Fm: αintroIsSquare (↑f (m * m))
F: Type u_3α: Type u_1β: Type u_2R: Type ?u.2218inst✝²: MulOneClass αinst✝¹: MulOneClass βinst✝: MonoidHomClass F α βm: αf: FIsSquare m → IsSquare (↑f m)exact ⟨f: Ff m: αm, F: Type u_3α: Type u_1β: Type u_2R: Type ?u.2218inst✝²: MulOneClass αinst✝¹: MulOneClass βinst✝: MonoidHomClass F α βf: Fm: αintroIsSquare (↑f (m * m))byGoals accomplished! 🐙 F: Type u_3α: Type u_1β: Type u_2R: Type ?u.2218inst✝²: MulOneClass αinst✝¹: MulOneClass βinst✝: MonoidHomClass F α βf: Fm: α↑f (m * m) = ↑f m * ↑f msimpGoals accomplished! 🐙⟩Goals accomplished! 🐙
#align is_square.map IsSquare.map: ∀ {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulOneClass β]
[inst_2 : MonoidHomClass F α β] {m : α} (f : F), IsSquare m → IsSquare (↑f m)IsSquare.map
#align even.map Even.map: ∀ {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
[inst_2 : AddMonoidHomClass F α β] {m : α} (f : F), Even m → Even (↑f m)Even.map

section Monoid

variable [Monoid: Type ?u.19696 → Type ?u.19696Monoid α: Type ?u.5152α] {n: ℕn : ℕ: Typeℕ} {a: αa : α: Type ?u.5152α}

@[to_additive even_iff_exists_two_nsmul: ∀ {α : Type u_1} [inst : AddMonoid α] (m : α), Even m ↔ ∃ c, m = 2 • ceven_iff_exists_two_nsmul]
theorem isSquare_iff_exists_sq: ∀ {α : Type u_1} [inst : Monoid α] (m : α), IsSquare m ↔ ∃ c, m = c ^ 2isSquare_iff_exists_sq (m: αm : α: Type ?u.5171α) : IsSquare: {α : Type ?u.5189} → [inst : Mul α] → α → PropIsSquare m: αm ↔ ∃ c: ?m.5520c, m: αm = c: ?m.5520c ^ 2: ?m.55272 := byGoals accomplished! 🐙 F: Type ?u.5168α: Type u_1β: Type ?u.5174R: Type ?u.5177inst✝: Monoid αn: ℕa, m: αIsSquare m ↔ ∃ c, m = c ^ 2simp [IsSquare: {α : Type ?u.5667} → [inst : Mul α] → α → PropIsSquare, pow_two: ∀ {M : Type ?u.5678} [inst : Monoid M] (a : M), a ^ 2 = a * apow_two]Goals accomplished! 🐙
#align is_square_iff_exists_sq isSquare_iff_exists_sq: ∀ {α : Type u_1} [inst : Monoid α] (m : α), IsSquare m ↔ ∃ c, m = c ^ 2isSquare_iff_exists_sq
#align even_iff_exists_two_nsmul even_iff_exists_two_nsmul: ∀ {α : Type u_1} [inst : AddMonoid α] (m : α), Even m ↔ ∃ c, m = 2 • ceven_iff_exists_two_nsmul

alias isSquare_iff_exists_sq: ∀ {α : Type u_1} [inst : Monoid α] (m : α), IsSquare m ↔ ∃ c, m = c ^ 2isSquare_iff_exists_sq ↔ IsSquare.exists_sq: ∀ {α : Type u_1} [inst : Monoid α] (m : α), IsSquare m → ∃ c, m = c ^ 2IsSquare.exists_sq isSquare_of_exists_sq: ∀ {α : Type u_1} [inst : Monoid α] (m : α), (∃ c, m = c ^ 2) → IsSquare misSquare_of_exists_sq
#align is_square.exists_sq IsSquare.exists_sq: ∀ {α : Type u_1} [inst : Monoid α] (m : α), IsSquare m → ∃ c, m = c ^ 2IsSquare.exists_sq
#align is_square_of_exists_sq isSquare_of_exists_sq: ∀ {α : Type u_1} [inst : Monoid α] (m : α), (∃ c, m = c ^ 2) → IsSquare misSquare_of_exists_sq

attribute
[to_additive Even.exists_two_nsmul: ∀ {α : Type u_1} [inst : AddMonoid α] (m : α), Even m → ∃ c, m = 2 • cEven.exists_two_nsmul
"Alias of the forwards direction of `even_iff_exists_two_nsmul`."]
IsSquare.exists_sq: ∀ {α : Type u_1} [inst : Monoid α] (m : α), IsSquare m → ∃ c, m = c ^ 2IsSquare.exists_sq
#align even.exists_two_nsmul Even.exists_two_nsmul: ∀ {α : Type u_1} [inst : AddMonoid α] (m : α), Even m → ∃ c, m = 2 • cEven.exists_two_nsmul

@[to_additive: ∀ {α : Type u_1} [inst : AddMonoid α] {a : α} (n : ℕ), Even a → Even (n • a)to_additive]
theorem IsSquare.pow: ∀ {α : Type u_1} [inst : Monoid α] {a : α} (n : ℕ), IsSquare a → IsSquare (a ^ n)IsSquare.pow (n: ℕn : ℕ: Typeℕ) : IsSquare: {α : Type ?u.8168} → [inst : Mul α] → α → PropIsSquare a: αa → IsSquare: {α : Type ?u.8520} → [inst : Mul α] → α → PropIsSquare (a: αa ^ n: ℕn) := byGoals accomplished! 🐙
F: Type ?u.8146α: Type u_1β: Type ?u.8152R: Type ?u.8155inst✝: Monoid αn✝: ℕa: αn: ℕIsSquare a → IsSquare (a ^ n)rintro ⟨a, rfl⟩: IsSquare a⟨a: αa⟨a, rfl⟩: IsSquare a, rfl: a✝ = a * arfl⟨a, rfl⟩: IsSquare a⟩F: Type ?u.8146α: Type u_1β: Type ?u.8152R: Type ?u.8155inst✝: Monoid αn✝, n: ℕa: αintroIsSquare ((a * a) ^ n)
F: Type ?u.8146α: Type u_1β: Type ?u.8152R: Type ?u.8155inst✝: Monoid αn✝: ℕa: αn: ℕIsSquare a → IsSquare (a ^ n)exact ⟨a: αa ^ n: ℕn, (Commute.refl: ∀ {S : Type ?u.13654} [inst : Mul S] (a : S), Commute a aCommute.refl _: ?m.13655_).mul_pow: ∀ {M : Type ?u.13681} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), (a * b) ^ n = a ^ n * b ^ nmul_pow _: ℕ_⟩Goals accomplished! 🐙
#align is_square.pow IsSquare.pow: ∀ {α : Type u_1} [inst : Monoid α] {a : α} (n : ℕ), IsSquare a → IsSquare (a ^ n)IsSquare.pow
#align even.nsmul Even.nsmul: ∀ {α : Type u_1} [inst : AddMonoid α] {a : α} (n : ℕ), Even a → Even (n • a)Even.nsmul

/- Porting note: `simp` attribute removed because linter reports:
simp can prove this:
by simp only [even_two, Even.nsmul']
-/
@[to_additive Even.nsmul': ∀ {α : Type u_1} [inst : AddMonoid α] {n : ℕ}, Even n → ∀ (a : α), Even (n • a)Even.nsmul']
theorem Even.isSquare_pow: ∀ {α : Type u_1} [inst : Monoid α] {n : ℕ}, Even n → ∀ (a : α), IsSquare (a ^ n)Even.isSquare_pow : Even: {α : Type ?u.14092} → [inst : Add α] → α → PropEven n: ℕn → ∀ a: αa : α: Type ?u.14075α, IsSquare: {α : Type ?u.14125} → [inst : Mul α] → α → PropIsSquare (a: αa ^ n: ℕn) := byGoals accomplished! 🐙
F: Type ?u.14072α: Type u_1β: Type ?u.14078R: Type ?u.14081inst✝: Monoid αn: ℕa: αEven n → ∀ (a : α), IsSquare (a ^ n)rintro ⟨n, rfl⟩: Even n⟨n: ℕn⟨n, rfl⟩: Even n, rfl: n✝ = n + nrfl⟨n, rfl⟩: Even n⟩ a: αaF: Type ?u.14072α: Type u_1β: Type ?u.14078R: Type ?u.14081inst✝: Monoid αa✝: αn: ℕa: αintroIsSquare (a ^ (n + n))
F: Type ?u.14072α: Type u_1β: Type ?u.14078R: Type ?u.14081inst✝: Monoid αn: ℕa: αEven n → ∀ (a : α), IsSquare (a ^ n)exact ⟨a: αa ^ n: ℕn, pow_add: ∀ {M : Type ?u.19594} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ npow_add _: ?m.19595_ _: ℕ_ _: ℕ_⟩Goals accomplished! 🐙
#align even.is_square_pow Even.isSquare_pow: ∀ {α : Type u_1} [inst : Monoid α] {n : ℕ}, Even n → ∀ (a : α), IsSquare (a ^ n)Even.isSquare_pow
#align even.nsmul' Even.nsmul': ∀ {α : Type u_1} [inst : AddMonoid α] {n : ℕ}, Even n → ∀ (a : α), Even (n • a)Even.nsmul'

/- Porting note: `simp` attribute removed because linter reports:
simp can prove this:
by simp only [even_two, Even.is_square_pow]
-/
@[to_additive even_two_nsmul: ∀ {α : Type u_1} [inst : AddMonoid α] (a : α), Even (2 • a)even_two_nsmul]
theorem IsSquare_sq: ∀ {α : Type u_1} [inst : Monoid α] (a : α), IsSquare (a ^ 2)IsSquare_sq (a: αa : α: Type ?u.19687α) : IsSquare: {α : Type ?u.19705} → [inst : Mul α] → α → PropIsSquare (a: αa ^ 2: ?m.197352) :=
⟨a: αa, pow_two: ∀ {M : Type ?u.20303} [inst : Monoid M] (a : M), a ^ 2 = a * apow_two _: ?m.20304_⟩
#align is_square_sq IsSquare_sq: ∀ {α : Type u_1} [inst : Monoid α] (a : α), IsSquare (a ^ 2)IsSquare_sq
#align even_two_nsmul even_two_nsmul: ∀ {α : Type u_1} [inst : AddMonoid α] (a : α), Even (2 • a)even_two_nsmul

variable [HasDistribNeg: (α : Type ?u.24643) → [inst : Mul α] → Type ?u.24643HasDistribNeg α: Type ?u.20715α]

theorem Even.neg_pow: Even n → ∀ (a : α), (-a) ^ n = a ^ nEven.neg_pow : Even: {α : Type ?u.21061} → [inst : Add α] → α → PropEven n: ℕn → ∀ a: αa : α: Type ?u.20715α, (-a: αa) ^ n: ℕn = a: αa ^ n: ℕn := byGoals accomplished! 🐙
F: Type ?u.20712α: Type u_1β: Type ?u.20718R: Type ?u.20721inst✝¹: Monoid αn: ℕa: αinst✝: HasDistribNeg αEven n → ∀ (a : α), (-a) ^ n = a ^ nrintro ⟨c, rfl⟩: Even n⟨c: ℕc⟨c, rfl⟩: Even n, rfl: n = c + crfl⟨c, rfl⟩: Even n⟩ a: αaF: Type ?u.20712α: Type u_1β: Type ?u.20718R: Type ?u.20721inst✝¹: Monoid αa✝: αinst✝: HasDistribNeg αc: ℕa: αintro(-a) ^ (c + c) = a ^ (c + c)
F: Type ?u.20712α: Type u_1β: Type ?u.20718R: Type ?u.20721inst✝¹: Monoid αn: ℕa: αinst✝: HasDistribNeg αEven n → ∀ (a : α), (-a) ^ n = a ^ nsimp_rw [F: Type ?u.20712α: Type u_1β: Type ?u.20718R: Type ?u.20721inst✝¹: Monoid αa✝: αinst✝: HasDistribNeg αc: ℕa: αintro(-a) ^ (c + c) = a ^ (c + c)← two_mul: ∀ {α : Type ?u.24274} [inst : NonAssocSemiring α] (n : α), 2 * n = n + ntwo_mul,F: Type ?u.20712α: Type u_1β: Type ?u.20718R: Type ?u.20721inst✝¹: Monoid αa✝: αinst✝: HasDistribNeg αc: ℕa: αintro(-a) ^ (2 * c) = a ^ (2 * c) F: Type ?u.20712α: Type u_1β: Type ?u.20718R: Type ?u.20721inst✝¹: Monoid αa✝: αinst✝: HasDistribNeg αc: ℕa: αintro(-a) ^ (c + c) = a ^ (c + c)pow_mul: ∀ {M : Type ?u.24475} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ m) ^ npow_mul,F: Type ?u.20712α: Type u_1β: Type ?u.20718R: Type ?u.20721inst✝¹: Monoid αa✝: αinst✝: HasDistribNeg αc: ℕa: αintro((-a) ^ 2) ^ c = (a ^ 2) ^ c F: Type ?u.20712α: Type u_1β: Type ?u.20718R: Type ?u.20721inst✝¹: Monoid αa✝: αinst✝: HasDistribNeg αc: ℕa: αintro(-a) ^ (c + c) = a ^ (c + c)neg_sq: ∀ {R : Type ?u.24550} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R), (-a) ^ 2 = a ^ 2neg_sqGoals accomplished! 🐙]Goals accomplished! 🐙
#align even.neg_pow Even.neg_pow: ∀ {α : Type u_1} [inst : Monoid α] {n : ℕ} [inst_1 : HasDistribNeg α], Even n → ∀ (a : α), (-a) ^ n = a ^ nEven.neg_pow

theorem Even.neg_one_pow: ∀ {α : Type u_1} [inst : Monoid α] {n : ℕ} [inst_1 : HasDistribNeg α], Even n → (-1) ^ n = 1Even.neg_one_pow (h: Even nh : Even: {α : Type ?u.24972} → [inst : Add α] → α → PropEven n: ℕn) : (-1: ?m.250101 : α: Type ?u.24627α) ^ n: ℕn = 1: ?m.257641 := byGoals accomplished! 🐙 F: Type ?u.24624α: Type u_1β: Type ?u.24630R: Type ?u.24633inst✝¹: Monoid αn: ℕa: αinst✝: HasDistribNeg αh: Even n(-1) ^ n = 1rw [F: Type ?u.24624α: Type u_1β: Type ?u.24630R: Type ?u.24633inst✝¹: Monoid αn: ℕa: αinst✝: HasDistribNeg αh: Even n(-1) ^ n = 1h: Even nh.neg_pow: ∀ {α : Type ?u.28307} [inst : Monoid α] {n : ℕ} [inst_1 : HasDistribNeg α], Even n → ∀ (a : α), (-a) ^ n = a ^ nneg_pow,F: Type ?u.24624α: Type u_1β: Type ?u.24630R: Type ?u.24633inst✝¹: Monoid αn: ℕa: αinst✝: HasDistribNeg αh: Even n1 ^ n = 1 F: Type ?u.24624α: Type u_1β: Type ?u.24630R: Type ?u.24633inst✝¹: Monoid αn: ℕa: αinst✝: HasDistribNeg αh: Even n(-1) ^ n = 1one_pow: ∀ {M : Type ?u.28406} [inst : Monoid M] (n : ℕ), 1 ^ n = 1one_powF: Type ?u.24624α: Type u_1β: Type ?u.24630R: Type ?u.24633inst✝¹: Monoid αn: ℕa: αinst✝: HasDistribNeg αh: Even n1 = 1]Goals accomplished! 🐙
#align even.neg_one_pow Even.neg_one_pow: ∀ {α : Type u_1} [inst : Monoid α] {n : ℕ} [inst_1 : HasDistribNeg α], Even n → (-1) ^ n = 1Even.neg_one_pow

end Monoid

@[to_additive: ∀ {α : Type u_1} [inst : AddCommSemigroup α] {a b : α}, Even a → Even b → Even (a + b)to_additive]
theorem IsSquare.mul: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, IsSquare a → IsSquare b → IsSquare (a * b)IsSquare.mul [CommSemigroup: Type ?u.28476 → Type ?u.28476CommSemigroup α: Type ?u.28467α] {a: αa b: αb : α: Type ?u.28467α} : IsSquare: {α : Type ?u.28484} → [inst : Mul α] → α → PropIsSquare a: αa → IsSquare: {α : Type ?u.29035} → [inst : Mul α] → α → PropIsSquare b: αb → IsSquare: {α : Type ?u.29062} → [inst : Mul α] → α → PropIsSquare (a: αa * b: αb) := byGoals accomplished! 🐙
F: Type ?u.28464α: Type u_1β: Type ?u.28470R: Type ?u.28473inst✝: CommSemigroup αa, b: αIsSquare a → IsSquare b → IsSquare (a * b)rintro ⟨a, rfl⟩: IsSquare a⟨a: αa⟨a, rfl⟩: IsSquare a, rfl: a✝ = a * arfl⟨a, rfl⟩: IsSquare a⟩ ⟨b, rfl⟩: IsSquare b⟨b: αb⟨b, rfl⟩: IsSquare b, rfl: b✝ = b * brfl⟨b, rfl⟩: IsSquare b⟩F: Type ?u.28464α: Type u_1β: Type ?u.28470R: Type ?u.28473inst✝: CommSemigroup αa, b: αintro.introIsSquare (a * a * (b * b))
F: Type ?u.28464α: Type u_1β: Type ?u.28470R: Type ?u.28473inst✝: CommSemigroup αa, b: αIsSquare a → IsSquare b → IsSquare (a * b)exact ⟨a: αa * b: αb, mul_mul_mul_comm: ∀ {G : Type ?u.30978} [inst : CommSemigroup G] (a b c d : G), a * b * (c * d) = a * c * (b * d)mul_mul_mul_comm _: ?m.30979_ _: ?m.30979_ _: ?m.30979_ _: ?m.30979_⟩Goals accomplished! 🐙
#align is_square.mul IsSquare.mul: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, IsSquare a → IsSquare b → IsSquare (a * b)IsSquare.mul
#align even.add Even.add: ∀ {α : Type u_1} [inst : AddCommSemigroup α] {a b : α}, Even a → Even b → Even (a + b)Even.add

variable (α: ?m.31079α)

@[simp]
theorem isSquare_zero: ∀ (α : Type u_1) [inst : MulZeroClass α], IsSquare 0isSquare_zero [MulZeroClass: Type ?u.31094 → Type ?u.31094MulZeroClass α: Type ?u.31085α] : IsSquare: {α : Type ?u.31097} → [inst : Mul α] → α → PropIsSquare (0: ?m.311250 : α: Type ?u.31085α) :=
⟨0: ?m.316210, (mul_zero: ∀ {M₀ : Type ?u.31915} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0mul_zero _: ?m.31916_).symm: ∀ {α : Sort ?u.31927} {a b : α}, a = b → b = asymm⟩
#align is_square_zero isSquare_zero: ∀ (α : Type u_1) [inst : MulZeroClass α], IsSquare 0isSquare_zero

variable {α: ?m.31985α}

section DivisionMonoid

variable [DivisionMonoid: Type ?u.34445 → Type ?u.34445DivisionMonoid α: Type ?u.32008α] {a: αa : α: Type ?u.31991α}

@[to_additive: ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, Even (-a) ↔ Even ato_additive (attr := simp)]
theorem isSquare_inv: IsSquare a⁻¹ ↔ IsSquare aisSquare_inv : IsSquare: {α : Type ?u.32022} → [inst : Mul α] → α → PropIsSquare a: αa⁻¹ ↔ IsSquare: {α : Type ?u.32447} → [inst : Mul α] → α → PropIsSquare a: αa := byGoals accomplished! 🐙
F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αIsSquare a⁻¹ ↔ IsSquare arefine' ⟨fun h: ?m.32461h => _: ?m.32457_, fun h: ?m.32468h => _: ?m.32456_⟩F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare a⁻¹refine'_1IsSquare aF: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare arefine'_2IsSquare a⁻¹
F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αIsSquare a⁻¹ ↔ IsSquare a·F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare a⁻¹refine'_1IsSquare a F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare a⁻¹refine'_1IsSquare aF: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare arefine'_2IsSquare a⁻¹rw [F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare a⁻¹refine'_1IsSquare a← isSquare_op_iff: ∀ {α : Type ?u.32474} [inst : Mul α] (a : α), IsSquare (op a) ↔ IsSquare aisSquare_op_iff,F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare a⁻¹refine'_1IsSquare (op a) F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare a⁻¹refine'_1IsSquare a← inv_inv: ∀ {G : Type ?u.32890} [inst : InvolutiveInv G] (a : G), a⁻¹⁻¹ = ainv_inv a: αaF: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare a⁻¹refine'_1IsSquare (op a⁻¹⁻¹)]F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare a⁻¹refine'_1IsSquare (op a⁻¹⁻¹)
F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare a⁻¹refine'_1IsSquare aexact h: ?m.32461h.map: ∀ {F : Type ?u.32911} {α : Type ?u.32909} {β : Type ?u.32910} [inst : MulOneClass α] [inst_1 : MulOneClass β]
[inst_2 : MonoidHomClass F α β] {m : α} (f : F), IsSquare m → IsSquare (↑f m)map (MulEquiv.inv': (G : Type ?u.32928) → [inst : DivisionMonoid G] → G ≃* GᵐᵒᵖMulEquiv.inv' α: Type u_1α)Goals accomplished! 🐙
F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αIsSquare a⁻¹ ↔ IsSquare a·F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare arefine'_2IsSquare a⁻¹ F: Type ?u.32005α: Type u_1β: Type ?u.32011R: Type ?u.32014inst✝: DivisionMonoid αa: αh: IsSquare arefine'_2IsSquare a⁻¹exact ((isSquare_op_iff: ∀ {α : Type ?u.33703} [inst : Mul α] (a : α), IsSquare (op a) ↔ IsSquare aisSquare_op_iff a: αa).mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr h: ?m.32468h).map: ∀ {F : Type ?u.33710} {α : Type ?u.33708} {β : Type ?u.33709} [inst : MulOneClass α] [inst_1 : MulOneClass β]
[inst_2 : MonoidHomClass F α β] {m : α} (f : F), IsSquare m → IsSquare (↑f m)map (MulEquiv.inv': (G : Type ?u.33727) → [inst : DivisionMonoid G] → G ≃* GᵐᵒᵖMulEquiv.inv' α: Type u_1α).symm: {M : Type ?u.33730} → {N : Type ?u.33729} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* MsymmGoals accomplished! 🐙
#align is_square_inv isSquare_inv: ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α}, IsSquare a⁻¹ ↔ IsSquare aisSquare_inv
#align even_neg even_neg: ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, Even (-a) ↔ Even aeven_neg

alias isSquare_inv: ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α}, IsSquare a⁻¹ ↔ IsSquare aisSquare_inv ↔ _ IsSquare.inv: ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α}, IsSquare a → IsSquare a⁻¹IsSquare.inv
#align is_square.inv IsSquare.inv: ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α}, IsSquare a → IsSquare a⁻¹IsSquare.inv

attribute [to_additive: ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, Even a → Even (-a)to_additive] IsSquare.inv: ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α}, IsSquare a → IsSquare a⁻¹IsSquare.inv
#align even.neg Even.neg: ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, Even a → Even (-a)Even.neg

@[to_additive: ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (n : ℤ), Even a → Even (n • a)to_additive]
theorem IsSquare.zpow: ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α} (n : ℤ), IsSquare a → IsSquare (a ^ n)IsSquare.zpow (n: ℤn : ℤ: Typeℤ) : IsSquare: {α : Type ?u.34453} → [inst : Mul α] → α → PropIsSquare a: αa → IsSquare: {α : Type ?u.34841} → [inst : Mul α] → α → PropIsSquare (a: αa ^ n: ℤn) := byGoals accomplished! 🐙
F: Type ?u.34433α: Type u_1β: Type ?u.34439R: Type ?u.34442inst✝: DivisionMonoid αa: αn: ℤIsSquare a → IsSquare (a ^ n)rintro ⟨a, rfl⟩: IsSquare a⟨a: αa⟨a, rfl⟩: IsSquare a, rfl: a✝ = a * arfl⟨a, rfl⟩: IsSquare a⟩F: Type ?u.34433α: Type u_1β: Type ?u.34439R: Type ?u.34442inst✝: DivisionMonoid αn: ℤa: αintroIsSquare ((a * a) ^ n)
F: Type ?u.34433α: Type u_1β: Type ?u.34439R: Type ?u.34442inst✝: DivisionMonoid αa: αn: ℤIsSquare a → IsSquare (a ^ n)exact ⟨a: αa ^ n: ℤn, (Commute.refl: ∀ {S : Type ?u.40133} [inst : Mul S] (a : S), Commute a aCommute.refl _: ?m.40134_).mul_zpow: ∀ {α : Type ?u.40160} [inst : DivisionMonoid α] {a b : α}, Commute a b → ∀ (i : ℤ), (a * b) ^ i = a ^ i * b ^ imul_zpow _: ℤ_⟩Goals accomplished! 🐙
#align is_square.zpow IsSquare.zpow: ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α} (n : ℤ), IsSquare a → IsSquare (a ^ n)IsSquare.zpow
#align even.zsmul Even.zsmul: ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (n : ℤ), Even a → Even (n • a)Even.zsmul

variable [HasDistribNeg: (α : Type ?u.44669) → [inst : Mul α] → Type ?u.44669HasDistribNeg α: Type ?u.40569α] {n: ℤn : ℤ: Typeℤ}

theorem Even.neg_zpow: Even n → ∀ (a : α), (-a) ^ n = a ^ nEven.neg_zpow : Even: {α : Type ?u.41335} → [inst : Add α] → α → PropEven n: ℤn → ∀ a: αa : α: Type ?u.40953α, (-a: αa) ^ n: ℤn = a: αa ^ n: ℤn := byGoals accomplished! 🐙
F: Type ?u.40950α: Type u_1β: Type ?u.40956R: Type ?u.40959inst✝¹: DivisionMonoid αa: αinst✝: HasDistribNeg αn: ℤEven n → ∀ (a : α), (-a) ^ n = a ^ nrintro ⟨c, rfl⟩: Even n⟨c: ℤc⟨c, rfl⟩: Even n, rfl: n = c + crfl⟨c, rfl⟩: Even n⟩ a: αaF: Type ?u.40950α: Type u_1β: Type ?u.40956R: Type ?u.40959inst✝¹: DivisionMonoid αa✝: αinst✝: HasDistribNeg αc: ℤa: αintro(-a) ^ (c + c) = a ^ (c + c)
F: Type ?u.40950α: Type u_1β: Type ?u.40956R: Type ?u.40959inst✝¹: DivisionMonoid αa: αinst✝: HasDistribNeg αn: ℤEven n → ∀ (a : α), (-a) ^ n = a ^ nexact zpow_bit0_neg: ∀ {α : Type ?u.44572} [inst : DivisionMonoid α] [inst_1 : HasDistribNeg α] (x : α) (n : ℤ), (-x) ^ bit0 n = x ^ bit0 nzpow_bit0_neg _: ?m.44573_ _: ℤ_Goals accomplished! 🐙
#align even.neg_zpow Even.neg_zpow: ∀ {α : Type u_1} [inst : DivisionMonoid α] [inst_1 : HasDistribNeg α] {n : ℤ}, Even n → ∀ (a : α), (-a) ^ n = a ^ nEven.neg_zpow

theorem Even.neg_one_zpow: ∀ {α : Type u_1} [inst : DivisionMonoid α] [inst_1 : HasDistribNeg α] {n : ℤ}, Even n → (-1) ^ n = 1Even.neg_one_zpow (h: Even nh : Even: {α : Type ?u.45036} → [inst : Add α] → α → PropEven n: ℤn) : (-1: ?m.450741 : α: Type ?u.44655α) ^ n: ℤn = 1: ?m.457741 := byGoals accomplished! 🐙 F: Type ?u.44652α: Type u_1β: Type ?u.44658R: Type ?u.44661inst✝¹: DivisionMonoid αa: αinst✝: HasDistribNeg αn: ℤh: Even n(-1) ^ n = 1rw [F: Type ?u.44652α: Type u_1β: Type ?u.44658R: Type ?u.44661inst✝¹: DivisionMonoid αa: αinst✝: HasDistribNeg αn: ℤh: Even n(-1) ^ n = 1h: Even nh.neg_zpow: ∀ {α : Type ?u.48391} [inst : DivisionMonoid α] [inst_1 : HasDistribNeg α] {n : ℤ}, Even n → ∀ (a : α), (-a) ^ n = a ^ nneg_zpow,F: Type ?u.44652α: Type u_1β: Type ?u.44658R: Type ?u.44661inst✝¹: DivisionMonoid αa: αinst✝: HasDistribNeg αn: ℤh: Even n1 ^ n = 1 F: Type ?u.44652α: Type u_1β: Type ?u.44658R: Type ?u.44661inst✝¹: DivisionMonoid αa: αinst✝: HasDistribNeg αn: ℤh: Even n(-1) ^ n = 1one_zpow: ∀ {α : Type ?u.48473} [inst : DivisionMonoid α] (n : ℤ), 1 ^ n = 1one_zpowF: Type ?u.44652α: Type u_1β: Type ?u.44658R: Type ?u.44661inst✝¹: DivisionMonoid αa: αinst✝: HasDistribNeg αn: ℤh: Even n1 = 1]Goals accomplished! 🐙
#align even.neg_one_zpow Even.neg_one_zpow: ∀ {α : Type u_1} [inst : DivisionMonoid α] [inst_1 : HasDistribNeg α] {n : ℤ}, Even n → (-1) ^ n = 1Even.neg_one_zpow

end DivisionMonoid

theorem even_abs: ∀ [inst : SubtractionMonoid α] [inst_1 : LinearOrder α] {a : α}, Even (abs a) ↔ Even aeven_abs [SubtractionMonoid: Type ?u.48538 → Type ?u.48538SubtractionMonoid α: Type ?u.48529α] [LinearOrder: Type ?u.48541 → Type ?u.48541LinearOrder α: Type ?u.48529α] {a: αa : α: Type ?u.48529α} : Even: {α : Type ?u.48546} → [inst : Add α] → α → PropEven (|a: αa|) ↔ Even: {α : Type ?u.49072} → [inst : Add α] → α → PropEven a: αa := byGoals accomplished! 🐙
F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αEven (abs a) ↔ Even acases abs_choice: ∀ {α : Type ?u.49081} [inst : Neg α] [inst_1 : LinearOrder α] (x : α), abs x = x ∨ abs x = -xabs_choice a: αaF: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = ainlEven (abs a) ↔ Even aF: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = -ainrEven (abs a) ↔ Even a
F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αEven (abs a) ↔ Even a·F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = ainlEven (abs a) ↔ Even a F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = ainlEven (abs a) ↔ Even aF: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = -ainrEven (abs a) ↔ Even ahave h: abs a = ah : abs: {α : Type ?u.49263} → [self : Abs α] → α → αabs a: αa = a: αa := F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = ainlEven (abs a) ↔ Even abyGoals accomplished! 🐙 F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = aabs a = aassumptionGoals accomplished! 🐙
F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = ainlEven (abs a) ↔ Even asimp only [h: abs a = ah, even_neg: ∀ {α : Type ?u.49454} [inst : SubtractionMonoid α] {a : α}, Even (-a) ↔ Even aeven_neg]Goals accomplished! 🐙
F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αEven (abs a) ↔ Even a·F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = -ainrEven (abs a) ↔ Even a F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = -ainrEven (abs a) ↔ Even ahave h: abs a = -ah : abs: {α : Type ?u.49573} → [self : Abs α] → α → αabs a: αa = -a: αa := F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = -ainrEven (abs a) ↔ Even abyGoals accomplished! 🐙 F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = -aabs a = -aassumptionGoals accomplished! 🐙
F: Type ?u.48526α: Type u_1β: Type ?u.48532R: Type ?u.48535inst✝¹: SubtractionMonoid αinst✝: LinearOrder αa: αh✝: abs a = -ainrEven (abs a) ↔ Even asimp only [h: abs a = -ah, even_neg: ∀ {α : Type ?u.49592} [inst : SubtractionMonoid α] {a : α}, Even (-a) ↔ Even aeven_neg]Goals accomplished! 🐙
#align even_abs even_abs: ∀ {α : Type u_1} [inst : SubtractionMonoid α] [inst_1 : LinearOrder α] {a : α}, Even (abs a) ↔ Even aeven_abs

@[to_additive: ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] {a b : α}, Even a → Even b → Even (a - b)to_additive]
theorem IsSquare.div: ∀ {α : Type u_1} [inst : DivisionCommMonoid α] {a b : α}, IsSquare a → IsSquare b → IsSquare (a / b)IsSquare.div [DivisionCommMonoid: Type ?u.49659 → Type ?u.49659DivisionCommMonoid α: Type ?u.49650α] {a: αa b: αb : α: Type ?u.49650α} (ha: IsSquare aha : IsSquare: {α : Type ?u.49666} → [inst : Mul α] → α → PropIsSquare a: αa) (hb: IsSquare bhb : IsSquare: {α : Type ?u.50061} → [inst : Mul α] → α → PropIsSquare b: αb) :
IsSquare: {α : Type ?u.50089} → [inst : Mul α] → α → PropIsSquare (a: αa / b: αb) := byGoals accomplished! 🐙
F: Type ?u.49647α: Type u_1β: Type ?u.49653R: Type ?u.49656inst✝: DivisionCommMonoid αa, b: αha: IsSquare ahb: IsSquare bIsSquare (a / b)rw [F: Type ?u.49647α: Type u_1β: Type ?u.49653R: Type ?u.49656inst✝: DivisionCommMonoid αa, b: αha: IsSquare ahb: IsSquare bIsSquare (a / b)div_eq_mul_inv: ∀ {G : Type ?u.50250} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹div_eq_mul_invF: Type ?u.49647α: Type u_1β: Type ?u.49653R: Type ?u.49656inst✝: DivisionCommMonoid αa, b: αha: IsSquare ahb: IsSquare bIsSquare (a * b⁻¹)]F: Type ?u.49647α: Type u_1β: Type ?u.49653R: Type ?u.49656inst✝: DivisionCommMonoid αa, b: αha: IsSquare ahb: IsSquare bIsSquare (a * b⁻¹)
F: Type ?u.49647α: Type u_1β: Type ?u.49653R: Type ?u.49656inst✝: DivisionCommMonoid αa, b: αha: IsSquare ahb: IsSquare bIsSquare (a / b)exact ha: IsSquare aha.mul: ∀ {α : Type ?u.50347} [inst : CommSemigroup α] {a b : α}, IsSquare a → IsSquare b → IsSquare (a * b)mul hb: IsSquare bhb.inv: ∀ {α : Type ?u.50554} [inst : DivisionMonoid α] {a : α}, IsSquare a → IsSquare a⁻¹invGoals accomplished! 🐙
#align is_square.div IsSquare.div: ∀ {α : Type u_1} [inst : DivisionCommMonoid α] {a b : α}, IsSquare a → IsSquare b → IsSquare (a / b)IsSquare.div
#align even.sub Even.sub: ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] {a b : α}, Even a → Even b → Even (a - b)Even.sub

@[to_additive (attr := simp) Even.zsmul': ∀ {α : Type u_1} [inst : AddGroup α] {n : ℤ}, Even n → ∀ (a : α), Even (n • a)Even.zsmul']
theorem Even.isSquare_zpow: ∀ {α : Type u_1} [inst : Group α] {n : ℤ}, Even n → ∀ (a : α), IsSquare (a ^ n)Even.isSquare_zpow [Group: Type ?u.50627 → Type ?u.50627Group α: Type ?u.50618α] {n: ℤn : ℤ: Typeℤ} : Even: {α : Type ?u.50633} → [inst : Add α] → α → PropEven n: ℤn → ∀ a: αa : α: Type ?u.50618α, IsSquare: {α : Type ?u.50666} → [inst : Mul α] → α → PropIsSquare (a: αa ^ n: ℤn) := byGoals accomplished! 🐙
F: Type ?u.50615α: Type u_1β: Type ?u.50621R: Type ?u.50624inst✝: Group αn: ℤEven n → ∀ (a : α), IsSquare (a ^ n)rintro ⟨n, rfl⟩: Even n⟨n: ℤn⟨n, rfl⟩: Even n, rfl: n✝ = n + nrfl⟨n, rfl⟩: Even n⟩ a: αaF: Type ?u.50615α: Type u_1β: Type ?u.50621R: Type ?u.50624inst✝: Group αn: ℤa: αintroIsSquare (a ^ (n + n))
F: Type ?u.50615α: Type u_1β: Type ?u.50621R: Type ?u.50624inst✝: Group αn: ℤEven n → ∀ (a : α), IsSquare (a ^ n)exact ⟨a: αa ^ n: ℤn, zpow_add: ∀ {G : Type ?u.56286} [inst : Group G] (a : G) (m n : ℤ), a ^ (m + n) = a ^ m * a ^ nzpow_add _: ?m.56287_ _: ℤ_ _: ℤ_⟩Goals accomplished! 🐙
#align even.is_square_zpow Even.isSquare_zpow: ∀ {α : Type u_1} [inst : Group α] {n : ℤ}, Even n → ∀ (a : α), IsSquare (a ^ n)Even.isSquare_zpow
#align even.zsmul' Even.zsmul': ∀ {α : Type u_1} [inst : AddGroup α] {n : ℤ}, Even n → ∀ (a : α), Even (n • a)Even.zsmul'

-- `Odd.tsub` requires `CanonicallyLinearOrderedSemiring`, which we don't have
theorem Even.tsub: ∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {m n : α},
Even m → Even n → Even (m - n)Even.tsub [CanonicallyLinearOrderedAddMonoid: Type ?u.56426 → Type ?u.56426CanonicallyLinearOrderedAddMonoid α: Type ?u.56417α] [Sub: Type ?u.56429 → Type ?u.56429Sub α: Type ?u.56417α] [OrderedSub: (α : Type ?u.56432) → [inst : LE α] → [inst : Add α] → [inst : Sub α] → PropOrderedSub α: Type ?u.56417α]
[ContravariantClass: (M : Type ?u.57051) → (N : Type ?u.57050) → (M → N → N) → (N → N → Prop) → PropContravariantClass α: Type ?u.56417α α: Type ?u.56417α (· + ·): α → α → α(· + ·) (· ≤ ·): α → α → Prop(· ≤ ·)] {m: αm n: αn : α: Type ?u.56417α} (hm: Even mhm : Even: {α : Type ?u.57933} → [inst : Add α] → α → PropEven m: αm) (hn: Even nhn : Even: {α : Type ?u.58295} → [inst : Add α] → α → PropEven n: αn) :
Even: {α : Type ?u.58321} → [inst : Add α] → α → PropEven (m: αm - n: αn) := byGoals accomplished! 🐙
F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1m, n: αhm: Even mhn: Even nEven (m - n)obtain ⟨a, rfl⟩: Even m⟨a: αa⟨a, rfl⟩: Even m, rfl: m = a + arfl⟨a, rfl⟩: Even m⟩ := hm: Even mhmF: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1n: αhn: Even na: αintroEven (a + a - n)
F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1m, n: αhm: Even mhn: Even nEven (m - n)obtain ⟨b, rfl⟩: Even n⟨b: αb⟨b, rfl⟩: Even n, rfl: n = b + brfl⟨b, rfl⟩: Even n⟩ := hn: Even nhnF: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αintro.introEven (a + a - (b + b))
F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1m, n: αhm: Even mhn: Even nEven (m - n)refine' ⟨a: αa - b: αb, _: ?m.58472 (a - b)_⟩F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αintro.introa + a - (b + b) = a - b + (a - b)
F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1m, n: αhm: Even mhn: Even nEven (m - n)obtain h: a ≤ bhh | h: a ≤ b ∨ b ≤ a | h: b ≤ ah := le_total: ∀ {α : Type ?u.58521} [inst : LinearOrder α] (a b : α), a ≤ b ∨ b ≤ ale_total a: αa b: αbF: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: a ≤ bintro.intro.inla + a - (b + b) = a - b + (a - b)F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: b ≤ aintro.intro.inra + a - (b + b) = a - b + (a - b)
F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1m, n: αhm: Even mhn: Even nEven (m - n)·F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: a ≤ bintro.intro.inla + a - (b + b) = a - b + (a - b) F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: a ≤ bintro.intro.inla + a - (b + b) = a - b + (a - b)F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: b ≤ aintro.intro.inra + a - (b + b) = a - b + (a - b)rw [F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: a ≤ bintro.intro.inla + a - (b + b) = a - b + (a - b)tsub_eq_zero_of_le: ∀ {α : Type ?u.58581} [inst : CanonicallyOrderedAddMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α},
a ≤ b → a - b = 0tsub_eq_zero_of_le h: a ≤ bh,F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: a ≤ bintro.intro.inla + a - (b + b) = 0 + 0 F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: a ≤ bintro.intro.inla + a - (b + b) = a - b + (a - b)tsub_eq_zero_of_le: ∀ {α : Type ?u.58622} [inst : CanonicallyOrderedAddMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α},
a ≤ b → a - b = 0tsub_eq_zero_of_le (add_le_add: ∀ {α : Type ?u.58629} [inst : Add α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a ≤ b → c ≤ d → a + c ≤ b + dadd_le_add h: a ≤ bh h: a ≤ bh),F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: a ≤ bintro.intro.inl0 = 0 + 0 F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: a ≤ bintro.intro.inla + a - (b + b) = a - b + (a - b)add_zero: ∀ {M : Type ?u.59576} [inst : AddZeroClass M] (a : M), a + 0 = aadd_zeroF: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: a ≤ bintro.intro.inl0 = 0]Goals accomplished! 🐙
F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1m, n: αhm: Even mhn: Even nEven (m - n)·F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: b ≤ aintro.intro.inra + a - (b + b) = a - b + (a - b) F: Type ?u.56414α: Type u_1β: Type ?u.56420R: Type ?u.56423inst✝³: CanonicallyLinearOrderedAddMonoid αinst✝²: Sub αinst✝¹: OrderedSub αinst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1a, b: αh: b ≤ aintro.intro.inra + a - (b + b) = a - b + (a - b)exact (tsub_add_tsub_comm: ∀ {α : Type ?u.59928} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c d : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
b ≤ a → d ≤ c → a - b + (c - d) = a + c - (b + d)tsub_add_tsub_comm h: b ≤ ah h: b ≤ ah).symm: ∀ {α : Sort ?u.60307} {a b : α}, a = b → b = asymmGoals accomplished! 🐙
#align even.tsub Even.tsub: ∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {m n : α},
Even m → Even n → Even (m - n)Even.tsub

set_option linter.deprecated false in
theorem even_iff_exists_bit0: ∀ [inst : Add α] {a : α}, Even a ↔ ∃ b, a = bit0 beven_iff_exists_bit0 [Add: Type ?u.60365 → Type ?u.60365Add α: Type ?u.60356α] {a: αa : α: Type ?u.60356α} : Even: {α : Type ?u.60370} → [inst : Add α] → α → PropEven a: αa ↔ ∃ b: ?m.60382b, a: αa = bit0: {α : Type ?u.60385} → [inst : Add α] → α → αbit0 b: ?m.60382b :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align even_iff_exists_bit0 even_iff_exists_bit0: ∀ {α : Type u_1} [inst : Add α] {a : α}, Even a ↔ ∃ b, a = bit0 beven_iff_exists_bit0

alias even_iff_exists_bit0: ∀ {α : Type u_1} [inst : Add α] {a : α}, Even a ↔ ∃ b, a = bit0 beven_iff_exists_bit0 ↔ Even.exists_bit0: ∀ {α : Type u_1} [inst : Add α] {a : α}, Even a → ∃ b, a = bit0 bEven.exists_bit0 _
#align even.exists_bit0 Even.exists_bit0: ∀ {α : Type u_1} [inst : Add α] {a : α}, Even a → ∃ b, a = bit0 bEven.exists_bit0

section Semiring

variable [Semiring: Type ?u.66764 → Type ?u.66764Semiring α: Type ?u.73988α] [Semiring: Type ?u.60467 → Type ?u.60467Semiring β: Type ?u.60480β] {m: αm n: αn : α: Type ?u.60455α}

theorem even_iff_exists_two_mul: ∀ {α : Type u_1} [inst : Semiring α] (m : α), Even m ↔ ∃ c, m = 2 * ceven_iff_exists_two_mul (m: αm : α: Type ?u.60477α) : Even: {α : Type ?u.60498} → [inst : Add α] → α → PropEven m: αm ↔ ∃ c: ?m.60616c, m: αm = 2: ?m.606232 * c: ?m.60616c := byGoals accomplished! 🐙
F: Type ?u.60474α: Type u_1β: Type ?u.60480R: Type ?u.60483inst✝¹: Semiring αinst✝: Semiring βm✝, n, m: αEven m ↔ ∃ c, m = 2 * csimp [even_iff_exists_two_nsmul: ∀ {α : Type ?u.60871} [inst : AddMonoid α] (m : α), Even m ↔ ∃ c, m = 2 • ceven_iff_exists_two_nsmul]Goals accomplished! 🐙
#align even_iff_exists_two_mul even_iff_exists_two_mul: ∀ {α : Type u_1} [inst : Semiring α] (m : α), Even m ↔ ∃ c, m = 2 * ceven_iff_exists_two_mul

theorem even_iff_two_dvd: ∀ {α : Type u_1} [inst : Semiring α] {a : α}, Even a ↔ 2 ∣ aeven_iff_two_dvd {a: αa : α: Type ?u.63450α} : Even: {α : Type ?u.63471} → [inst : Add α] → α → PropEven a: αa ↔ 2: ?m.635902 ∣ a: αa := byGoals accomplished! 🐙 F: Type ?u.63447α: Type u_1β: Type ?u.63453R: Type ?u.63456inst✝¹: Semiring αinst✝: Semiring βm, n, a: αEven a ↔ 2 ∣ asimp [Even: {α : Type ?u.63729} → [inst : Add α] → α → PropEven, Dvd.dvd: {α : Type ?u.63740} → [self : Dvd α] → α → α → PropDvd.dvd, two_mul: ∀ {α : Type ?u.63742} [inst : NonAssocSemiring α] (n : α), 2 * n = n + ntwo_mul]Goals accomplished! 🐙
#align even_iff_two_dvd even_iff_two_dvd: ∀ {α : Type u_1} [inst : Semiring α] {a : α}, Even a ↔ 2 ∣ aeven_iff_two_dvd

alias even_iff_two_dvd: ∀ {α : Type u_1} [inst : Semiring α] {a : α}, Even a ↔ 2 ∣ aeven_iff_two_dvd ↔ Even.two_dvd: ∀ {α : Type u_1} [inst : Semiring α] {a : α}, Even a → 2 ∣ aEven.two_dvd _
#align even.two_dvd Even.two_dvd: ∀ {α : Type u_1} [inst : Semiring α] {a : α}, Even a → 2 ∣ aEven.two_dvd

theorem Even.trans_dvd: ∀ {α : Type u_1} [inst : Semiring α] {m n : α}, Even m → m ∣ n → Even nEven.trans_dvd (hm: Even mhm : Even: {α : Type ?u.65976} → [inst : Add α] → α → PropEven m: αm) (hn: m ∣ nhn : m: αm ∣ n: αn) : Even: {α : Type ?u.66218} → [inst : Add α] → α → PropEven n: αn :=
even_iff_two_dvd: ∀ {α : Type ?u.66247} [inst : Semiring α] {a : α}, Even a ↔ 2 ∣ aeven_iff_two_dvd.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 <| hm: Even mhm.two_dvd: ∀ {α : Type ?u.66279} [inst : Semiring α] {a : α}, Even a → 2 ∣ atwo_dvd.trans: ∀ {α : Type ?u.66292} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ ctrans hn: m ∣ nhn
#align even.trans_dvd Even.trans_dvd: ∀ {α : Type u_1} [inst : Semiring α] {m n : α}, Even m → m ∣ n → Even nEven.trans_dvd

theorem Dvd.dvd.even: ∀ {α : Type u_1} [inst : Semiring α] {m n : α}, m ∣ n → Even m → Even nDvd.dvd.even (hn: m ∣ nhn : m: αm ∣ n: αn) (hm: Even mhm : Even: {α : Type ?u.66555} → [inst : Add α] → α → PropEven m: αm) : Even: {α : Type ?u.66682} → [inst : Add α] → α → PropEven n: αn :=
hm: Even mhm.trans_dvd: ∀ {α : Type ?u.66711} [inst : Semiring α] {m n : α}, Even m → m ∣ n → Even ntrans_dvd hn: m ∣ nhn
#align has_dvd.dvd.even Dvd.dvd.even: ∀ {α : Type u_1} [inst : Semiring α] {m n : α}, m ∣ n → Even m → Even nDvd.dvd.even

@[simp]
theorem range_two_mul: ∀ (α : Type u_1) [inst : Semiring α], (Set.range fun x => 2 * x) = { a | Even a }range_two_mul (α: ?m.66774α) [Semiring: Type ?u.66777 → Type ?u.66777Semiring α: ?m.66774α] : (Set.range: {α : Type ?u.66782} → {ι : Sort ?u.66781} → (ι → α) → Set αSet.range fun x: αx : α: ?m.66774α => 2: ?m.667912 * x: αx) = { a: ?m.67069a | Even: {α : Type ?u.67071} → [inst : Add α] → α → PropEven a: ?m.67069a } := byGoals accomplished! 🐙
F: Type ?u.66752α✝: Type ?u.66755β: Type ?u.66758R: Type ?u.66761inst✝²: Semiring α✝inst✝¹: Semiring βm, n: α✝α: Type u_1inst✝: Semiring α(Set.range fun x => 2 * x) = { a | Even a }ext x: ?αxF: Type ?u.66752α✝: Type ?u.66755β: Type ?u.66758R: Type ?u.66761inst✝²: Semiring α✝inst✝¹: Semiring βm, n: α✝α: Type u_1inst✝: Semiring αx: αh(x ∈ Set.range fun x => 2 * x) ↔ x ∈ { a | Even a }
F: Type ?u.66752α✝: Type ?u.66755β: Type ?u.66758R: Type ?u.66761inst✝²: Semiring α✝inst✝¹: Semiring βm, n: α✝α: Type u_1inst✝: Semiring α(Set.range fun x => 2 * x) = { a | Even a }simp [eq_comm: ∀ {α : Sort ?u.67283} {a b : α}, a = b ↔ b = aeq_comm, two_mul: ∀ {α : Type ?u.67301} [inst : NonAssocSemiring α] (n : α), 2 * n = n + ntwo_mul, Even: {α : Type ?u.67318} → [inst : Add α] → α → PropEven]Goals accomplished! 🐙
#align range_two_mul range_two_mul: ∀ (α : Type u_1) [inst : Semiring α], (Set.range fun x => 2 * x) = { a | Even a }range_two_mul

set_option linter.deprecated false in
@[simp] theorem even_bit0: ∀ {α : Type u_1} [inst : Semiring α] (a : α), Even (bit0 a)even_bit0 (a: αa : α: Type ?u.71899α) : Even: {α : Type ?u.71920} → [inst : Add α] → α → PropEven (bit0: {α : Type ?u.71944} → [inst : Add α] → α → αbit0 a: αa) :=
⟨a: αa, rfl: ∀ {α : Sort ?u.72095} {a : α}, a = arfl⟩
#align even_bit0 even_bit0: ∀ {α : Type u_1} [inst : Semiring α] (a : α), Even (bit0 a)even_bit0

@[simp]
theorem even_two: ∀ {α : Type u_1} [inst : Semiring α], Even 2even_two : Even: {α : Type ?u.72144} → [inst : Add α] → α → PropEven (2: ?m.721702 : α: Type ?u.72125α) :=
⟨1: ?m.723291, byGoals accomplished! 🐙 F: Type ?u.72122α: Type u_1β: Type ?u.72128R: Type ?u.72131inst✝¹: Semiring αinst✝: Semiring βm, n: α2 = 1 + 1rw[F: Type ?u.72122α: Type u_1β: Type ?u.72128R: Type ?u.72131inst✝¹: Semiring αinst✝: Semiring βm, n: α2 = 1 + 1one_add_one_eq_two: ∀ {α : Type ?u.72367} [inst : AddMonoidWithOne α], 1 + 1 = 2one_add_one_eq_twoF: Type ?u.72122α: Type u_1β: Type ?u.72128R: Type ?u.72131inst✝¹: Semiring αinst✝: Semiring βm, n: α2 = 2]Goals accomplished! 🐙⟩
#align even_two even_two: ∀ {α : Type u_1} [inst : Semiring α], Even 2even_two

@[simp]
theorem Even.mul_left: ∀ {α : Type u_1} [inst : Semiring α] {m : α}, Even m → ∀ (n : α), Even (n * m)Even.mul_left (hm: Even mhm : Even: {α : Type ?u.72553} → [inst : Add α] → α → PropEven m: αm) (n: ?m.72691n) : Even: {α : Type ?u.72694} → [inst : Add α] → α → PropEven (n: ?m.72691n * m: αm) :=
hm: Even mhm.map: ∀ {F : Type ?u.72925} {α : Type ?u.72923} {β : Type ?u.72924} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
[inst_2 : AddMonoidHomClass F α β] {m : α} (f : F), Even m → Even (↑f m)map (AddMonoidHom.mulLeft: {R : Type ?u.72942} → [inst : NonUnitalNonAssocSemiring R] → R → R →+ RAddMonoidHom.mulLeft n: αn)
#align even.mul_left Even.mul_left: ∀ {α : Type u_1} [inst : Semiring α] {m : α}, Even m → ∀ (n : α), Even (n * m)Even.mul_left

@[simp]
theorem Even.mul_right: Even m → ∀ (n : α), Even (m * n)Even.mul_right (hm: Even mhm : Even: {α : Type ?u.73280} → [inst : Add α] → α → PropEven m: αm) (n: αn) : Even: {α : Type ?u.73421} → [inst : Add α] → α → PropEven (m: αm * n: ?m.73418n) :=
hm: Even mhm.map: ∀ {F : Type ?u.73652} {α : Type ?u.73650} {β : Type ?u.73651} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
[inst_2 : AddMonoidHomClass F α β] {m : α} (f : F), Even m → Even (↑f m)map (AddMonoidHom.mulRight: {R : Type ?u.73669} → [inst : NonUnitalNonAssocSemiring R] → R → R →+ RAddMonoidHom.mulRight n: αn)
#align even.mul_right Even.mul_right: ∀ {α : Type u_1} [inst : Semiring α] {m : α}, Even m → ∀ (n : α), Even (m * n)Even.mul_right

theorem even_two_mul: ∀ {α : Type u_1} [inst : Semiring α] (m : α), Even (2 * m)even_two_mul (m: αm : α: Type ?u.73988α) : Even: {α : Type ?u.74009} → [inst : Add α] → α → PropEven (2: ?m.740372 * m: αm) :=
⟨m: αm, two_mul: ∀ {α : Type ?u.74405} [inst : NonAssocSemiring α] (n : α), 2 * n = n + ntwo_mul _: ?m.74406_⟩
#align even_two_mul even_two_mul: ∀ {α : Type u_1} [inst : Semiring α] (m : α), Even (2 * m)even_two_mul

theorem Even.pow_of_ne_zero: Even m → ∀ {a : ℕ}, a ≠ 0 → Even (m ^ a)Even.pow_of_ne_zero (hm: Even mhm : Even: {α : Type ?u.74486} → [inst : Add α] → α → PropEven m: αm) : ∀ {a: ℕa : ℕ: Typeℕ}, a: ℕa ≠ 0: ?m.746310 → Even: {α : Type ?u.74642} → [inst : Add α] → α → PropEven (m: αm ^ a: ℕa)
| 0: ℕ0, a0: 0 ≠ 0a0 => (a0: 0 ≠ 0a0 rfl: ∀ {α : Sort ?u.74815} {a : α}, a = arfl).elim: ∀ {C : Sort ?u.74821}, False → Celim
| a: ℕa + 1, _ => byGoals accomplished! 🐙
F: Type ?u.74464α: Type u_1β: Type ?u.74470R: Type ?u.74473inst✝¹: Semiring αinst✝: Semiring βm, n: αhm: Even ma: ℕx✝: a + 1 ≠ 0Even (m ^ (a + 1))rw [F: Type ?u.74464α: Type u_1β: Type ?u.74470R: Type ?u.74473inst✝¹: Semiring αinst✝: Semiring βm, n: αhm: Even ma: ℕx✝: a + 1 ≠ 0Even (m ^ (a + 1))pow_succ: ∀ {M : Type ?u.75012} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ npow_succF: Type ?u.74464α: Type u_1β: Type ?u.74470R: Type ?u.74473inst✝¹: Semiring αinst✝: Semiring βm, n: αhm: Even ma: ℕx✝: a + 1 ≠ 0Even (m * m ^ a)]F: Type ?u.74464α: Type u_1β: Type ?u.74470R: Type ?u.74473inst✝¹: Semiring αinst✝: Semiring βm, n: αhm: Even ma: ℕx✝: a + 1 ≠ 0Even (m * m ^ a)
F: Type ?u.74464α: Type u_1β: Type ?u.74470R: Type ?u.74473inst✝¹: Semiring αinst✝: Semiring βm, n: αhm: Even ma: ℕx✝: a + 1 ≠ 0Even (m ^ (a + 1))exact hm: Even mhm.mul_right: ∀ {α : Type ?u.75099} [inst : Semiring α] {m : α}, Even m → ∀ (n : α), Even (m * n)mul_right _: ?m.75105_Goals accomplished! 🐙
#align even.pow_of_ne_zero Even.pow_of_ne_zero: ∀ {α : Type u_1} [inst : Semiring α] {m : α}, Even m → ∀ {a : ℕ}, a ≠ 0 → Even (m ^ a)Even.pow_of_ne_zero

section WithOdd

/-- An element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`. -/
def Odd: {α : Type u_1} → [inst : Semiring α] → α → PropOdd (a: αa : α: Type ?u.75156α) : Prop: TypeProp :=
∃ k: ?m.75182k, a: αa = 2: ?m.751922 * k: ?m.75182k + 1: ?m.752021
#align odd Odd: {α : Type u_1} → [inst : Semiring α] → α → PropOdd

set_option linter.deprecated false in
theorem odd_iff_exists_bit1: ∀ {a : α}, Odd a ↔ ∃ b, a = bit1 bodd_iff_exists_bit1 {a: αa : α: Type ?u.75710α} : Odd: {α : Type ?u.75731} → [inst : Semiring α] → α → PropOdd a: αa ↔ ∃ b: ?m.75745b, a: αa = bit1: {α : Type ?u.75748} → [inst : One α] → [inst : Add α] → α → αbit1 b: ?m.75745b :=
exists_congr: ∀ {α : Sort ?u.75997} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∃ a, p a) ↔ ∃ a, q a)exists_congr fun b: ?m.76013b => byGoals accomplished! 🐙
F: Type ?u.75707α: Type u_1β: Type ?u.75713R: Type ?u.75716inst✝¹: Semiring αinst✝: Semiring βm, n, a, b: αa = 2 * b + 1 ↔ a = bit1 brw [F: Type ?u.75707α: Type u_1β: Type ?u.75713R: Type ?u.75716inst✝¹: Semiring αinst✝: Semiring βm, n, a, b: αa = 2 * b + 1 ↔ a = bit1 btwo_mul: ∀ {α : Type ?u.76020} [inst : NonAssocSemiring α] (n : α), 2 * n = n + ntwo_mulF: Type ?u.75707α: Type u_1β: Type ?u.75713R: Type ?u.75716inst✝¹: Semiring αinst✝: Semiring βm, n, a, b: αa = b + b + 1 ↔ a = bit1 b]F: Type ?u.75707α: Type u_1β: Type ?u.75713R: Type ?u.75716inst✝¹: Semiring αinst✝: Semiring βm, n, a, b: αa = b + b + 1 ↔ a = bit1 b
F: Type ?u.75707α: Type u_1β: Type ?u.75713R: Type ?u.75716inst✝¹: Semiring αinst✝: Semiring βm, n, a, b: αa = 2 * b + 1 ↔ a = bit1 brflGoals accomplished! 🐙
#align odd_iff_exists_bit1 odd_iff_exists_bit1: ∀ {α : Type u_1} [inst : Semiring α] {a : α}, Odd a ↔ ∃ b, a = bit1 bodd_iff_exists_bit1

alias odd_iff_exists_bit1: ∀ {α : Type u_1} [inst : Semiring α] {a : α}, Odd a ↔ ∃ b, a = bit1 bodd_iff_exists_bit1 ↔ Odd.exists_bit1: ∀ {α : Type u_1} [inst : Semiring α] {a : α}, Odd a → ∃ b, a = bit1 bOdd.exists_bit1 _
#align odd.exists_bit1 Odd.exists_bit1: ∀ {α : Type u_1} [inst : Semiring α] {a : α}, Odd a → ∃ b, a = bit1 bOdd.exists_bit1

set_option linter.deprecated false in
@[simp] theorem odd_bit1: ∀ (a : α), Odd (bit1 a)odd_bit1 (a: αa : α: Type ?u.76131α) : Odd: {α : Type ?u.76152} → [inst : Semiring α] → α → PropOdd (bit1: {α : Type ?u.76163} → [inst : One α] → [inst : Add α] → α → αbit1 a: αa) :=
odd_iff_exists_bit1: ∀ {α : Type ?u.76366} [inst : Semiring α] {a : α}, Odd a ↔ ∃ b, a = bit1 bodd_iff_exists_bit1.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ⟨a: αa, rfl: ∀ {α : Sort ?u.76398} {a : α}, a = arfl⟩
#align odd_bit1 odd_bit1: ∀ {α : Type u_1} [inst : Semiring α] (a : α), Odd (bit1 a)odd_bit1

@[simp]
theorem range_two_mul_add_one: ∀ (α : Type u_1) [inst : Semiring α], (Set.range fun x => 2 * x + 1) = { a | Odd a }range_two_mul_add_one (α: Type u_1α : Type _: Type (?u.76455+1)Type _) [Semiring: Type ?u.76458 → Type ?u.76458Semiring α: Type ?u.76455α] :
(Set.range: {α : Type ?u.76463} → {ι : Sort ?u.76462} → (ι → α) → Set αSet.range fun x: αx : α: Type ?u.76455α => 2: ?m.764752 * x: αx + 1: ?m.764851) = { a: ?m.76990a | Odd: {α : Type ?u.76992} → [inst : Semiring α] → α → PropOdd a: ?m.76990a } := byGoals accomplished! 🐙
F: Type ?u.76433α✝: Type ?u.76436β: Type ?u.76439R: Type ?u.76442inst✝²: Semiring α✝inst✝¹: Semiring βm, n: α✝α: Type u_1inst✝: Semiring α(Set.range fun x => 2 * x + 1) = { a | Odd a }ext x: ?αxF: Type ?u.76433α✝: Type ?u.76436β: Type ?u.76439R: Type ?u.76442inst✝²: Semiring α✝inst✝¹: Semiring βm, n: α✝α: Type u_1inst✝: Semiring αx: αh(x ∈ Set.range fun x => 2 * x + 1) ↔ x ∈ { a | Odd a }
F: Type ?u.76433α✝: Type ?u.76436β: Type ?u.76439R: Type ?u.76442inst✝²: Semiring α✝inst✝¹: Semiring βm, n: α✝α: Type u_1inst✝: Semiring α(Set.range fun x => 2 * x + 1) = { a | Odd a }simp [Odd: {α : Type ?u.77088} → [inst : Semiring α] → α → PropOdd, eq_comm: ∀ {α : Sort ?u.77090} {a b : α}, a = b ↔ b = aeq_comm]Goals accomplished! 🐙
#align range_two_mul_add_one range_two_mul_add_one: ∀ (α : Type u_1) [inst : Semiring α], (Set.range fun x => 2 * x + 1) = { a | Odd a }range_two_mul_add_one

theorem Even.add_odd: Even m → Odd n → Odd (m + n)Even.add_odd : Even: {α : Type ?u.81639} → [inst : Add α] → α → PropEven m: αm → Odd: {α : Type ?u.81777} → [inst : Semiring α] → α → PropOdd n: αn → Odd: {α : Type ?u.81795} → [inst : Semiring α] → α → PropOdd (m: αm + n: αn) := byGoals accomplished! 🐙
F: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: αEven m → Odd n → Odd (m + n)rintro ⟨m, rfl⟩: Even m⟨m: αm⟨m, rfl⟩: Even m, rfl: m✝ = m + mrfl⟨m, rfl⟩: Even m⟩ ⟨n, rfl⟩: Odd n⟨n: αn⟨n, rfl⟩: Odd n, rfl: n✝ = 2 * n + 1rfl⟨n, rfl⟩: Odd n⟩F: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.introOdd (m + m + (2 * n + 1))
F: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: αEven m → Odd n → Odd (m + n)exact ⟨m: αm + n: αn, F: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.introOdd (m + m + (2 * n + 1))byGoals accomplished! 🐙 F: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: αm + m + (2 * n + 1) = 2 * (m + n) + 1rw [F: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: αm + m + (2 * n + 1) = 2 * (m + n) + 1mul_add: ∀ {R : Type ?u.82299} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * cmul_add,F: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: αm + m + (2 * n + 1) = 2 * m + 2 * n + 1 F: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: αm + m + (2 * n + 1) = 2 * (m + n) + 1← two_mul: ∀ {α : Type ?u.82739} [inst : NonAssocSemiring α] (n : α), 2 * n = n + ntwo_mul,F: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: α2 * m + (2 * n + 1) = 2 * m + 2 * n + 1 F: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: αm + m + (2 * n + 1) = 2 * (m + n) + 1add_assoc: ∀ {G : Type ?u.82793} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)add_assocF: Type ?u.81616α: Type u_1β: Type ?u.81622R: Type ?u.81625inst✝¹: Semiring αinst✝: Semiring βm, n: α2 * m + (2 * n + 1) = 2 * m + (2 * n + 1)]Goals accomplished! 🐙⟩Goals accomplished! 🐙
#align even.add_odd Even.add_odd: ∀ {α : Type u_1} [inst : Semiring α] {m n : α}, Even m → Odd n → Odd (m + n)Even.add_odd

theorem Odd.add_even: ∀ {α : Type u_1} [inst : Semiring α] {m n : α}, Odd m → Even n → Odd (m + n)Odd.add_even (hm: Odd mhm : Odd: {α : Type ?u.82997} → [inst : Semiring α] → α → PropOdd m: αm) (hn: Even nhn : Even: {α : Type ?u.83018} → [inst : Add α] → α → PropEven n: αn) : Odd: {α : Type ?u.83154} → [inst : Semiring α] → α → PropOdd (m: αm + n: αn) := byGoals accomplished! 🐙
F: Type ?u.82975α: Type u_1β: Type ?u.82981R: Type ?u.82984inst✝¹: Semiring αinst✝: Semiring βm, n: αhm: Odd mhn: Even nOdd (m + n)rw [F: Type ?u.82975α: Type u_1β: Type ?u.82981R: Type ?u.82984inst✝¹: Semiring αinst✝: Semiring βm, n: αhm: Odd mhn: Even nOdd (m + n)add_comm: ∀ {G : Type ?u.83360} [inst : AddCommSemigroup G] (a b : G), a + b = b + aadd_commF: Type ?u.82975α: Type u_1β: Type ?u.82981R: Type ?u.82984inst✝¹: Semiring αinst✝: Semiring βm, n: αhm: Odd mhn: Even nOdd (n + m)]F: Type ?u.82975α: Type u_1β: Type ?u.82981R: Type ?u.82984inst✝¹: Semiring αinst✝: Semiring βm, n: αhm: Odd mhn: Even nOdd (n + m)
F: Type ?u.82975α: Type u_1β: Type ?u.82981R: Type ?u.82984inst✝¹: Semiring αinst✝: Semiring βm, n: αhm: Odd mhn: Even nOdd (m + n)exact hn: Even nhn.add_odd: ∀ {α : Type ?u.83653} [inst : Semiring α] {m n : α}, Even m → Odd n → Odd (m + n)add_odd hm: Odd mhmGoals accomplished! 🐙
#align odd.add_even Odd.add_even: ∀ {α : Type u_1} [inst : Semiring α] {m n : α}, Odd m → Even n → Odd (m + n)Odd.add_even

theorem Odd.add_odd: Odd m → Odd n → Even (m + n)Odd.add_odd : Odd: {α : Type ?u.83729} → [inst : Semiring α] → α → PropOdd m: αm → Odd: {α : Type ?u.83750} → [inst : Semiring α] → α → PropOdd n: αn → Even: {α : Type ?u.83762} → [inst : Add α] → α → PropEven (m: αm + n: αn) := byGoals accomplished! 🐙
F: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αOdd m → Odd n → Even (m + n)rintro ⟨m, rfl⟩: Odd m⟨m: αm⟨m, rfl⟩: Odd m, rfl: m✝ = 2 * m + 1rfl⟨m, rfl⟩: Odd m⟩ ⟨n, rfl⟩: Odd n⟨n: αn⟨n, rfl⟩: Odd n, rfl: n✝ = 2 * n + 1rfl⟨n, rfl⟩: Odd n⟩F: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.introEven (2 * m + 1 + (2 * n + 1))
F: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αOdd m → Odd n → Even (m + n)refine' ⟨n: αn + m: αm + 1: ?m.841751, _: ?m.84162 (n + m + 1)_⟩F: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.intro2 * m + 1 + (2 * n + 1) = n + m + 1 + (n + m + 1)
F: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αOdd m → Odd n → Even (m + n)rw [F: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.intro2 * m + 1 + (2 * n + 1) = n + m + 1 + (n + m + 1)two_mul: ∀ {α : Type ?u.84536} [inst : NonAssocSemiring α] (n : α), 2 * n = n + ntwo_mul,F: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.introm + m + 1 + (2 * n + 1) = n + m + 1 + (n + m + 1) F: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.intro2 * m + 1 + (2 * n + 1) = n + m + 1 + (n + m + 1)two_mul: ∀ {α : Type ?u.84594} [inst : NonAssocSemiring α] (n : α), 2 * n = n + ntwo_mulF: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.introm + m + 1 + (n + n + 1) = n + m + 1 + (n + m + 1)]F: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.introm + m + 1 + (n + n + 1) = n + m + 1 + (n + m + 1)
F: Type ?u.83706α: Type u_1β: Type ?u.83712R: Type ?u.83715inst✝¹: Semiring αinst✝: Semiring βm, n: αOdd m → Odd n → Even (m + n)ac_rflGoals accomplished! 🐙
#align odd.add_odd Odd.add_odd: ∀ {α : Type u_1} [inst : Semiring α] {m n : α}, Odd m → Odd n → Even (m + n)Odd.add_odd

@[simp]
theorem odd_one: ∀ {α : Type u_1} [inst : Semiring α], Odd 1odd_one : Odd: {α : Type ?u.85288} → [inst : Semiring α] → α → PropOdd (1: ?m.853011 : α: Type ?u.85269α) :=
⟨0: ?m.853580, (zero_add: ∀ {M : Type ?u.85490} [inst : AddZeroClass M] (a : M), 0 + a = azero_add _: ?m.85491_).symm: ∀ {α : Sort ?u.85508} {a b : α}, a = b → b = asymm.trans: ∀ {α : Sort ?u.85515} {a b c : α}, a = b → b = c → a = ctrans (congr_arg: ∀ {α : Sort ?u.85530} {β : Sort ?u.85529} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂congr_arg (· + (1 : α: Type ?u.85269α)) (mul_zero: ∀ {M₀ : Type ?u.85885} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0mul_zero _: ?m.85886_).symm: ∀ {α : Sort ?u.85899} {a b : α}, a = b → b = asymm)⟩
#align odd_one odd_one: ∀ {α : Type u_1} [inst : Semiring α], Odd 1odd_one

@[simp]
theorem odd_two_mul_add_one: ∀ {α : Type u_1} [inst : Semiring α] (m : α), Odd (2 * m + 1)odd_two_mul_add_one (m: αm : α: Type ?u.86027α) : Odd: {α : Type ?u.86048} → [inst : Semiring α] → α → PropOdd (2: ?m.860662 * m: αm + 1: ?m.860761) :=
⟨m: αm, rfl: ∀ {α : Sort ?u.86590} {a : α}, a = arfl⟩
#align odd_two_mul_add_one odd_two_mul_add_one: ∀ {α : Type u_1} [inst : Semiring α] (m : α), Odd (2 * m + 1)odd_two_mul_add_one

theorem Odd.map: ∀ [inst : RingHomClass F α β] (f : F), Odd m → Odd (↑f m)Odd.map [RingHomClass: Type ?u.86657 →
(α : outParam (Type ?u.86656)) →
(β : outParam (Type ?u.86655)) →
[inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.86657?u.86656)?u.86655)RingHomClass F: Type ?u.86633F α: Type ?u.86636α β: Type ?u.86639β] (f: Ff : F: Type ?u.86633F) : Odd: {α : Type ?u.86695} → [inst : Semiring α] → α → PropOdd m: αm → Odd: {α : Type ?u.86713} → [inst : Semiring α] → α → PropOdd (f: Ff m: αm) := byGoals accomplished! 🐙
F: Type u_1α: Type u_2β: Type u_3R: Type ?u.86642inst✝²: Semiring αinst✝¹: Semiring βm, n: αinst✝: RingHomClass F α βf: FOdd m → Odd (↑f m)rintro ⟨m, rfl⟩: Odd m⟨m: αm⟨m, rfl⟩: Odd m, rfl: m✝ = 2 * m + 1rfl⟨m, rfl⟩: Odd m⟩F: Type u_1α: Type u_2β: Type u_3R: Type ?u.86642inst✝²: Semiring αinst✝¹: Semiring βn: αinst✝: RingHomClass F α βf: Fm: αintroOdd (↑f (2 * m + 1))
F: Type u_1α: Type u_2β: Type u_3R: Type ?u.86642inst✝²: Semiring αinst✝¹: Semiring βm, n: αinst✝: RingHomClass F α βf: FOdd m → Odd (↑f m)exact ⟨f: Ff m: αm, F: Type u_1α: Type u_2β: Type u_3R: Type ?u.86642inst✝²: Semiring αinst✝¹: Semiring βn: αinst✝: RingHomClass F α βf: Fm: αintroOdd (↑f (2 * m + 1))byGoals accomplished! 🐙 F: Type u_1α: Type u_2β: Type u_3R: Type ?u.86642inst✝²: Semiring αinst✝¹: Semiring βn: αinst✝: RingHomClass F α βf: Fm: α↑f (2 * m + 1) = 2 * ↑f m + 1simp [two_mul: ∀ {α : Type ?u.87430} [inst : NonAssocSemiring α] (n : α), 2 * n = n + ntwo_mul]Goals accomplished! 🐙⟩Goals accomplished! 🐙
#align odd.map Odd.map: ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : Semiring β] {m : α}
[inst_2 : RingHomClass F α β] (f : F), Odd m → Odd (↑f m)Odd.map

@[simp]
theorem Odd.mul: Odd m → Odd n → Odd (m * n)Odd.mul : Odd: {α : Type ?u.88882} → [inst : Semiring α] → α → PropOdd m: αm → Odd: {α : Type ?u.88903} → [inst : Semiring α] → α → PropOdd n: αn → Odd: {α : Type ?u.88915} → [inst : Semiring α] → α → PropOdd (m: αm * n: αn) := byGoals accomplished! 🐙
F: Type ?u.88859α: Type u_1β: Type ?u.88865R: Type ?u.88868inst✝¹: Semiring αinst✝: Semiring βm, n: αOdd m → Odd n → Odd (m * n)rintro ⟨m, rfl⟩: Odd m⟨m: αm⟨m, rfl⟩: Odd m, rfl: m✝ = 2 * m + 1rfl⟨m, rfl⟩: Odd m⟩ ⟨n, rfl⟩: Odd n⟨n: αn⟨n, rfl⟩: Odd n, rfl: n✝ = 2 * n + 1rfl⟨n, rfl⟩: Odd n⟩F: Type ?u.88859α: Type u_1β: Type ?u.88865R: Type ?u.88868inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.introOdd ((2 * m + 1) * (2 * n + 1))
F: Type ?u.88859α: Type u_1β: Type ?u.88865R: Type ?u.88868inst✝¹: Semiring αinst✝: Semiring βm, n: αOdd m → Odd n → Odd (m * n)refine' ⟨2: ?m.892502 * m: αm * n: αn + n: αn + m: αm, _: ?m.89231 (2 * m * n + n + m)_⟩F: Type ?u.88859α: Type u_1β: Type ?u.88865R: Type ?u.88868inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.intro(2 * m + 1) * (2 * n + 1) = 2 * (2 * m * n + n + m) + 1
F: Type ?u.88859α: Type u_1β: Type ?u.88865R: Type ?u.88868inst✝¹: Semiring αinst✝: Semiring βm, n: αOdd m → Odd n → Odd (m * n)rw [F: Type ?u.88859α: Type u_1β: Type ?u.88865R: Type ?u.88868inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.intro(2 * m + 1) * (2 * n + 1) = 2 * (2 * m * n + n + m) + 1mul_add: ∀ {R : Type ?u.89906} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * cmul_add,F: Type ?u.88859α: Type u_1β: Type ?u.88865R: Type ?u.88868inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.intro(2 * m + 1) * (2 * n) + (2 * m + 1) * 1 = 2 * (2 * m * n + n + m) + 1 F: Type ?u.88859α: Type u_1β: Type ?u.88865R: Type ?u.88868inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.intro(2 * m + 1) * (2 * n + 1) = 2 * (2 * m * n + n + m) + 1add_mul: ∀ {R : Type ?u.90340} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
(a + b) * c = a * c + b * cadd_mul,F: Type ?u.88859α: Type u_1β: Type ?u.88865R: Type ?u.88868inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.intro2 * m * (2 * n) + 1 * (2 * n) + (2 * m + 1) * 1 = 2 * (2 * m * n + n + m) + 1 F: Type ?u.88859α: Type u_1β: Type ?u.88865R: Type ?u.88868inst✝¹: Semiring αinst✝: Semiring βm, n: αintro.intro(2 * m + 1) * (2 * n + 1) = 2 * (2 * m * n + n + m) + 1mul_one: ∀ {M : Type ?u.90512} [inst : MulOneClass M] (a : M), a * 1 = amul_one,```