[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s t : Set α
a : α
⊢ a⁻¹ ∈ s⁻¹ ↔ a ∈ s
[PROOFSTEP]
simp only [mem_inv, inv_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s✝ t : Set α
a : α
s : Set α
⊢ s⁻¹⁻¹ = s
[PROOFSTEP]
simp only [← inv_preimage, preimage_preimage, inv_inv, preimage_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s t : Set α
a : α
⊢ s⁻¹ ⊆ t ↔ s ⊆ t⁻¹
[PROOFSTEP]
rw [← inv_subset_inv, inv_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s t : Set α
a✝ a : α
⊢ {a}⁻¹ = {a⁻¹}
[PROOFSTEP]
rw [← image_inv, image_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s✝ t : Set α
a✝ a : α
s : Set α
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹
[PROOFSTEP]
rw [insert_eq, union_inv, inv_singleton, insert_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s t : Set α
a : α
ι : Sort u_5
f : ι → α
⊢ (range f)⁻¹ = range fun i => (f i)⁻¹
[PROOFSTEP]
rw [← image_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s t : Set α
a : α
ι : Sort u_5
f : ι → α
⊢ Inv.inv '' range f = range fun i => (f i)⁻¹
[PROOFSTEP]
exact (range_comp _ _).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s t : Set α
a : α
⊢ op '' s⁻¹ = (op '' s)⁻¹
[PROOFSTEP]
simp_rw [← image_inv, Function.Semiconj.set_image op_inv s]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
ha : a ∈ s
⊢ a ^ 0 ∈ s ^ 0
[PROOFSTEP]
rw [pow_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
ha : a ∈ s
⊢ 1 ∈ s ^ 0
[PROOFSTEP]
exact one_mem_one
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n✝ : ℕ
ha : a ∈ s
n : ℕ
⊢ a ^ (n + 1) ∈ s ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n✝ : ℕ
ha : a ∈ s
n : ℕ
⊢ a * a ^ n ∈ s ^ (n + 1)
[PROOFSTEP]
exact mul_mem_mul ha (pow_mem_pow ha _)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hst : s ⊆ t
⊢ s ^ 0 ⊆ t ^ 0
[PROOFSTEP]
rw [pow_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hst : s ⊆ t
⊢ 1 ⊆ t ^ 0
[PROOFSTEP]
exact Subset.rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s ^ (n + 1) ⊆ t ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s * s ^ n ⊆ t ^ (n + 1)
[PROOFSTEP]
exact mul_subset_mul hst (pow_subset_pow hst _)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
hn : m ≤ n
⊢ s ^ m ⊆ s ^ n
[PROOFSTEP]
induction' n, hn using Nat.le_induction with _ _ ih
[GOAL]
case base
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ s ^ m ⊆ s ^ m
[PROOFSTEP]
exact Subset.rfl
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
n✝ : ℕ
hn✝ : m ≤ n✝
ih : s ^ m ⊆ s ^ n✝
⊢ s ^ m ⊆ s ^ (n✝ + 1)
[PROOFSTEP]
dsimp only
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
n✝ : ℕ
hn✝ : m ≤ n✝
ih : s ^ m ⊆ s ^ n✝
⊢ s ^ m ⊆ s ^ (n✝ + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n : ℕ
hs : 1 ∈ s
n✝ : ℕ
hn✝ : m ≤ n✝
ih : s ^ m ⊆ s ^ n✝
⊢ s ^ m ⊆ s * s ^ n✝
[PROOFSTEP]
exact ih.trans (subset_mul_right _ hs)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n✝ n : ℕ
hn : n ≠ 0
⊢ ∅ ^ n = ∅
[PROOFSTEP]
rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn), pow_succ, empty_mul]
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α✝
s t : Set α✝
a : α✝
m n✝ : ℕ
α : Type u_5
inst✝ : AddMonoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (n + 2) • univ = univ
[PROOFSTEP]
rw [succ_nsmul, nsmul_univ n.succ_ne_zero, univ_add_univ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n✝ n : ℕ
x✝ : n + 2 ≠ 0
⊢ univ ^ (n + 2) = univ
[PROOFSTEP]
rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
⊢ s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
[PROOFSTEP]
have hst : (s * t).Nonempty := h.symm.subst one_nonempty
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
[PROOFSTEP]
obtain ⟨a, ha⟩ := hst.of_image2_left
[GOAL]
case refine'_1.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
[PROOFSTEP]
obtain ⟨b, hb⟩ := hst.of_image2_right
[GOAL]
case refine'_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
[PROOFSTEP]
have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb => h.subset <| mem_image2_of_mem ha hb
[GOAL]
case refine'_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
[PROOFSTEP]
refine' ⟨a, b, _, _, H ha hb⟩
[GOAL]
case refine'_1.intro.intro.refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ s = {a}
[PROOFSTEP]
refine' eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => _⟩
[GOAL]
case refine'_1.intro.intro.refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ t = {b}
[PROOFSTEP]
refine' eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => _⟩
[GOAL]
case refine'_1.intro.intro.refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a
[PROOFSTEP]
exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)
[GOAL]
case refine'_1.intro.intro.refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : Set.Nonempty (s * t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b
[PROOFSTEP]
exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1
[PROOFSTEP]
rintro ⟨b, c, rfl, rfl, h⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
b c : α
h : b * c = 1
⊢ {b} * {c} = 1
[PROOFSTEP]
rw [singleton_mul_singleton, h, singleton_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
src✝³ : Monoid (Set α) := Set.monoid
src✝² : InvolutiveInv (Set α) := involutiveInv
src✝¹ : Div (Set α) := Set.div
src✝ : Pow (Set α) ℤ := Set.ZPow
s t : Set α
⊢ s / t = s * t⁻¹
[PROOFSTEP]
rw [← image_id (s / t), ← image_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
src✝³ : Monoid (Set α) := Set.monoid
src✝² : InvolutiveInv (Set α) := involutiveInv
src✝¹ : Div (Set α) := Set.div
src✝ : Pow (Set α) ℤ := Set.ZPow
s t : Set α
⊢ id '' (s / t) = s * Inv.inv '' t
[PROOFSTEP]
exact image_image2_distrib_right div_eq_mul_inv
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
src✝³ : Monoid (Set α) := Set.monoid
src✝² : InvolutiveInv (Set α) := involutiveInv
src✝¹ : Div (Set α) := Set.div
src✝ : Pow (Set α) ℤ := Set.ZPow
s t : Set α
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹
[PROOFSTEP]
simp_rw [← image_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
src✝³ : Monoid (Set α) := Set.monoid
src✝² : InvolutiveInv (Set α) := involutiveInv
src✝¹ : Div (Set α) := Set.div
src✝ : Pow (Set α) ℤ := Set.ZPow
s t : Set α
⊢ Inv.inv '' (s * t) = Inv.inv '' t * Inv.inv '' s
[PROOFSTEP]
exact image_image2_antidistrib mul_inv_rev
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
src✝³ : Monoid (Set α) := Set.monoid
src✝² : InvolutiveInv (Set α) := involutiveInv
src✝¹ : Div (Set α) := Set.div
src✝ : Pow (Set α) ℤ := Set.ZPow
s t : Set α
h : s * t = 1
⊢ s⁻¹ = t
[PROOFSTEP]
obtain ⟨a, b, rfl, rfl, hab⟩ := Set.mul_eq_one_iff.1 h
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
src✝³ : Monoid (Set α) := Set.monoid
src✝² : InvolutiveInv (Set α) := involutiveInv
src✝¹ : Div (Set α) := Set.div
src✝ : Pow (Set α) ℤ := Set.ZPow
a b : α
hab : a * b = 1
h : {a} * {b} = 1
⊢ {a}⁻¹ = {b}
[PROOFSTEP]
rw [inv_singleton, inv_eq_of_mul_eq_one_right hab]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case mp.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
t : Set α
u : (Set α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
[PROOFSTEP]
obtain ⟨a, b, ha, hb, h⟩ := Set.mul_eq_one_iff.1 u.mul_inv
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
t : Set α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
[PROOFSTEP]
refine' ⟨a, ha, ⟨a, b, h, singleton_injective _⟩, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
t : Set α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b * a} = {1}
[PROOFSTEP]
rw [← singleton_mul_singleton, ← ha, ← hb]
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
t : Set α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}
[PROOFSTEP]
exact u.inv_mul
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s
[PROOFSTEP]
rintro ⟨a, rfl, ha⟩
[GOAL]
case mpr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
t : Set α
a : α
ha : IsUnit a
⊢ IsUnit {a}
[PROOFSTEP]
exact ha.set
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
src✝ : InvolutiveNeg (Set α) := involutiveNeg
x✝¹ x✝ : Set α
⊢ -x✝¹ * x✝ = -(x✝¹ * x✝)
[PROOFSTEP]
simp_rw [← image_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
src✝ : InvolutiveNeg (Set α) := involutiveNeg
x✝¹ x✝ : Set α
⊢ Neg.neg '' x✝¹ * x✝ = Neg.neg '' (x✝¹ * x✝)
[PROOFSTEP]
exact image2_image_left_comm neg_mul
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
src✝ : InvolutiveNeg (Set α) := involutiveNeg
x✝¹ x✝ : Set α
⊢ x✝¹ * -x✝ = -(x✝¹ * x✝)
[PROOFSTEP]
simp_rw [← image_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
src✝ : InvolutiveNeg (Set α) := involutiveNeg
x✝¹ x✝ : Set α
⊢ x✝¹ * Neg.neg '' x✝ = Neg.neg '' (x✝¹ * x✝)
[PROOFSTEP]
exact image_image2_right_comm mul_neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : MulZeroClass α
s✝ t s : Set α
⊢ s * 0 ⊆ 0
[PROOFSTEP]
simp [subset_def, mem_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : MulZeroClass α
s✝ t s : Set α
⊢ 0 * s ⊆ 0
[PROOFSTEP]
simp [subset_def, mem_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : MulZeroClass α
s t : Set α
hs : Set.Nonempty s
⊢ 0 ⊆ s * 0
[PROOFSTEP]
simpa [mem_mul] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : MulZeroClass α
s t : Set α
hs : Set.Nonempty s
⊢ 0 ⊆ 0 * s
[PROOFSTEP]
simpa [mem_mul] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ 1 ∈ s / t ↔ ¬Disjoint s t
[PROOFSTEP]
simp [not_disjoint_iff_nonempty_inter, mem_div, div_eq_one, Set.Nonempty]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ IsUnit s ↔ ∃ a, s = {a}
[PROOFSTEP]
simp only [isUnit_iff, Group.isUnit, and_true_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ (fun x x_1 => x * x_1) a '' t = (fun x x_1 => x * x_1) a⁻¹ ⁻¹' t
[PROOFSTEP]
rw [image_eq_preimage_of_inverse]
[GOAL]
case h₁
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ LeftInverse ((fun x x_1 => x * x_1) a⁻¹) ((fun x x_1 => x * x_1) a)
[PROOFSTEP]
intro c
[GOAL]
case h₂
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ Function.RightInverse ((fun x x_1 => x * x_1) a⁻¹) ((fun x x_1 => x * x_1) a)
[PROOFSTEP]
intro c
[GOAL]
case h₁
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b c : α
⊢ (fun x x_1 => x * x_1) a⁻¹ ((fun x x_1 => x * x_1) a c) = c
[PROOFSTEP]
simp
[GOAL]
case h₂
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b c : α
⊢ (fun x x_1 => x * x_1) a ((fun x x_1 => x * x_1) a⁻¹ c) = c
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ (fun x => x * b) '' t = (fun x => x * b⁻¹) ⁻¹' t
[PROOFSTEP]
rw [image_eq_preimage_of_inverse]
[GOAL]
case h₁
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ LeftInverse (fun x => x * b⁻¹) fun x => x * b
[PROOFSTEP]
intro c
[GOAL]
case h₂
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ Function.RightInverse (fun x => x * b⁻¹) fun x => x * b
[PROOFSTEP]
intro c
[GOAL]
case h₁
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b c : α
⊢ (fun x => x * b⁻¹) ((fun x => x * b) c) = c
[PROOFSTEP]
simp
[GOAL]
case h₂
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b c : α
⊢ (fun x => x * b) ((fun x => x * b⁻¹) c) = c
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ (fun b => a⁻¹ * b) '' t = (fun b => a * b) ⁻¹' t
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ (fun x => x * b⁻¹) '' t = (fun x => x * b) ⁻¹' t
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ (fun x x_1 => x * x_1) a ⁻¹' {b} = {a⁻¹ * b}
[PROOFSTEP]
rw [← image_mul_left', image_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ (fun x => x * a) ⁻¹' {b} = {b * a⁻¹}
[PROOFSTEP]
rw [← image_mul_right', image_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ (fun x x_1 => x * x_1) a ⁻¹' 1 = {a⁻¹}
[PROOFSTEP]
rw [← image_mul_left', image_one, mul_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ (fun x => x * b) ⁻¹' 1 = {b⁻¹}
[PROOFSTEP]
rw [← image_mul_right', image_one, one_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ (fun b => a⁻¹ * b) ⁻¹' 1 = {a}
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Set α
a b : α
⊢ (fun x => x * b⁻¹) ⁻¹' 1 = {b}
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : GroupWithZero α
s✝ t s : Set α
⊢ s / 0 ⊆ 0
[PROOFSTEP]
simp [subset_def, mem_div]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : GroupWithZero α
s✝ t s : Set α
⊢ 0 / s ⊆ 0
[PROOFSTEP]
simp [subset_def, mem_div]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : GroupWithZero α
s t : Set α
hs : Set.Nonempty s
⊢ 0 ⊆ s / 0
[PROOFSTEP]
simpa [mem_div] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : GroupWithZero α
s t : Set α
hs : Set.Nonempty s
⊢ 0 ⊆ 0 / s
[PROOFSTEP]
simpa [mem_div] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : MulHomClass F α β
m : F
s✝ t✝ : Set α
s t : Set β
⊢ ↑m ⁻¹' s * ↑m ⁻¹' t ⊆ ↑m ⁻¹' (s * t)
[PROOFSTEP]
rintro _ ⟨_, _, _, _, rfl⟩
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : MulHomClass F α β
m : F
s✝ t✝ : Set α
s t : Set β
w✝¹ w✝ : α
left✝¹ : w✝¹ ∈ ↑m ⁻¹' s
left✝ : w✝ ∈ ↑m ⁻¹' t
⊢ (fun x x_1 => x * x_1) w✝¹ w✝ ∈ ↑m ⁻¹' (s * t)
[PROOFSTEP]
exact ⟨_, _, ‹_›, ‹_›, (map_mul m _ _).symm⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
s✝ t✝ : Set α
s t : Set β
⊢ ↑m ⁻¹' s / ↑m ⁻¹' t ⊆ ↑m ⁻¹' (s / t)
[PROOFSTEP]
rintro _ ⟨_, _, _, _, rfl⟩
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
s✝ t✝ : Set α
s t : Set β
w✝¹ w✝ : α
left✝¹ : w✝¹ ∈ ↑m ⁻¹' s
left✝ : w✝ ∈ ↑m ⁻¹' t
⊢ (fun x x_1 => x / x_1) w✝¹ w✝ ∈ ↑m ⁻¹' (s / t)
[PROOFSTEP]
exact ⟨_, _, ‹_›, ‹_›, (map_div m _ _).symm⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
A B : Set α
⊢ BddAbove A → BddAbove B → BddAbove (A * B)
[PROOFSTEP]
rintro ⟨bA, hbA⟩ ⟨bB, hbB⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
A B : Set α
bA : α
hbA : bA ∈ upperBounds A
bB : α
hbB : bB ∈ upperBounds B
⊢ BddAbove (A * B)
[PROOFSTEP]
use bA * bB
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
A B : Set α
bA : α
hbA : bA ∈ upperBounds A
bB : α
hbB : bB ∈ upperBounds B
⊢ bA * bB ∈ upperBounds (A * B)
[PROOFSTEP]
rintro x ⟨xa, xb, hxa, hxb, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
A B : Set α
bA : α
hbA : bA ∈ upperBounds A
bB : α
hbB : bB ∈ upperBounds B
xa xb : α
hxa : xa ∈ A
hxb : xb ∈ B
⊢ (fun x x_1 => x * x_1) xa xb ≤ bA * bB
[PROOFSTEP]
exact mul_le_mul' (hbA hxa) (hbB hxb)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
[PROOFSTEP]
have key : ∃ n : ℕ, n ≤ B ∧ f n = f (n + 1) := by
  contrapose! h2
  suffices ∀ n : ℕ, n ≤ B + 1 → n ≤ f n by exact ⟨B + 1, this (B + 1) (le_refl (B + 1))⟩
  exact fun n =>
    Nat.rec (fun _ => Nat.zero_le (f 0))
      (fun n ih h =>
        lt_of_le_of_lt (ih (n.le_succ.trans h)) (lt_of_le_of_ne (h1 n.le_succ) (h2 n (Nat.succ_le_succ_iff.mp h))))
      n
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
⊢ ∃ n, n ≤ B ∧ f n = f (n + 1)
[PROOFSTEP]
contrapose! h2
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
h2 : ∀ (n : ℕ), n ≤ B → f n ≠ f (n + 1)
⊢ ∃ n, B < f n
[PROOFSTEP]
suffices ∀ n : ℕ, n ≤ B + 1 → n ≤ f n by exact ⟨B + 1, this (B + 1) (le_refl (B + 1))⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
h2 : ∀ (n : ℕ), n ≤ B → f n ≠ f (n + 1)
this : ∀ (n : ℕ), n ≤ B + 1 → n ≤ f n
⊢ ∃ n, B < f n
[PROOFSTEP]
exact ⟨B + 1, this (B + 1) (le_refl (B + 1))⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
h2 : ∀ (n : ℕ), n ≤ B → f n ≠ f (n + 1)
⊢ ∀ (n : ℕ), n ≤ B + 1 → n ≤ f n
[PROOFSTEP]
exact fun n =>
  Nat.rec (fun _ => Nat.zero_le (f 0))
    (fun n ih h =>
      lt_of_le_of_lt (ih (n.le_succ.trans h)) (lt_of_le_of_ne (h1 n.le_succ) (h2 n (Nat.succ_le_succ_iff.mp h))))
    n
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
key : ∃ n, n ≤ B ∧ f n = f (n + 1)
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
[PROOFSTEP]
obtain ⟨n, hn1, hn2⟩ := key
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
n : ℕ
hn1 : n ≤ B
hn2 : f n = f (n + 1)
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
[PROOFSTEP]
replace key : ∀ k : ℕ, f (n + k) = f (n + k + 1) ∧ f (n + k) = f n := fun k =>
  Nat.rec ⟨hn2, rfl⟩ (fun k ih => ⟨h3 _ ih.1, ih.1.symm.trans ih.2⟩) k
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
n : ℕ
hn1 : n ≤ B
hn2 : f n = f (n + 1)
key : ∀ (k : ℕ), f (n + k) = f (n + k + 1) ∧ f (n + k) = f n
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
[PROOFSTEP]
replace key : ∀ k : ℕ, n ≤ k → f k = f n := fun k hk =>
  (congr_arg f (add_tsub_cancel_of_le hk)).symm.trans (key (k - n)).2
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
n : ℕ
hn1 : n ≤ B
hn2 : f n = f (n + 1)
key : ∀ (k : ℕ), n ≤ k → f k = f n
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
[PROOFSTEP]
exact fun k hk => (key k (hn1.trans hk)).trans (key B hn1).symm


[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
⊢ ∀ (s : Set ℤ) (a : ℤ), BddAbove s → a ∈ s → a ≤ sSup s
[PROOFSTEP]
intro s n hs hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddAbove s
hns : n ∈ s
⊢ n ≤ sSup s
[PROOFSTEP]
have : s.Nonempty ∧ BddAbove s :=
  ⟨⟨n, hns⟩, hs⟩
    -- Porting note: this was `rw [dif_pos this]`
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddAbove s
hns : n ∈ s
this : Set.Nonempty s ∧ BddAbove s
⊢ n ≤ sSup s
[PROOFSTEP]
simp only [this, and_self, dite_true, ge_iff_le]
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddAbove s
hns : n ∈ s
this : Set.Nonempty s ∧ BddAbove s
⊢ n ≤ ↑(greatestOfBdd (choose (_ : BddAbove s)) (_ : choose (_ : BddAbove s) ∈ upperBounds s) (_ : Set.Nonempty s))
[PROOFSTEP]
exact (greatestOfBdd _ _ _).2.2 n hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
⊢ ∀ (s : Set ℤ) (a : ℤ), Set.Nonempty s → a ∈ upperBounds s → sSup s ≤ a
[PROOFSTEP]
intro s n hs hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ upperBounds s
⊢ sSup s ≤ n
[PROOFSTEP]
have : s.Nonempty ∧ BddAbove s :=
  ⟨hs, ⟨n, hns⟩⟩
    -- Porting note: this was `rw [dif_pos this]`
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ upperBounds s
this : Set.Nonempty s ∧ BddAbove s
⊢ sSup s ≤ n
[PROOFSTEP]
simp only [this, and_self, dite_true, ge_iff_le]
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ upperBounds s
this : Set.Nonempty s ∧ BddAbove s
⊢ ↑(greatestOfBdd (choose (_ : BddAbove s)) (_ : choose (_ : BddAbove s) ∈ upperBounds s) (_ : Set.Nonempty s)) ≤ n
[PROOFSTEP]
exact hns (greatestOfBdd _ (Classical.choose_spec this.2) _).2.1
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
⊢ ∀ (s : Set ℤ) (a : ℤ), BddBelow s → a ∈ s → sInf s ≤ a
[PROOFSTEP]
intro s n hs hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddBelow s
hns : n ∈ s
⊢ sInf s ≤ n
[PROOFSTEP]
have : s.Nonempty ∧ BddBelow s :=
  ⟨⟨n, hns⟩, hs⟩
    -- Porting note: this was `rw [dif_pos this]`
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddBelow s
hns : n ∈ s
this : Set.Nonempty s ∧ BddBelow s
⊢ sInf s ≤ n
[PROOFSTEP]
simp only [this, and_self, dite_true, ge_iff_le]
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddBelow s
hns : n ∈ s
this : Set.Nonempty s ∧ BddBelow s
⊢ ↑(leastOfBdd (choose (_ : BddBelow s)) (_ : choose (_ : BddBelow s) ∈ lowerBounds s) (_ : Set.Nonempty s)) ≤ n
[PROOFSTEP]
exact (leastOfBdd _ _ _).2.2 n hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
⊢ ∀ (s : Set ℤ) (a : ℤ), Set.Nonempty s → a ∈ lowerBounds s → a ≤ sInf s
[PROOFSTEP]
intro s n hs hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ lowerBounds s
⊢ n ≤ sInf s
[PROOFSTEP]
have : s.Nonempty ∧ BddBelow s :=
  ⟨hs, ⟨n, hns⟩⟩
    -- Porting note: this was `rw [dif_pos this]`
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ lowerBounds s
this : Set.Nonempty s ∧ BddBelow s
⊢ n ≤ sInf s
[PROOFSTEP]
simp only [this, and_self, dite_true, ge_iff_le]
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ lowerBounds s
this : Set.Nonempty s ∧ BddBelow s
⊢ n ≤ ↑(leastOfBdd (choose (_ : BddBelow s)) (_ : choose (_ : BddBelow s) ∈ lowerBounds s) (_ : Set.Nonempty s))
[PROOFSTEP]
exact hns (leastOfBdd _ (Classical.choose_spec this.2) _).2.1
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
hs : ¬BddAbove s
⊢ sSup s = sSup Set.univ
[PROOFSTEP]
simp [hs]
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
hs : ¬BddBelow s
⊢ sInf s = sInf Set.univ
[PROOFSTEP]
simp [hs]
[GOAL]
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → z ≤ b
Hinh : ∃ z, z ∈ s
⊢ sSup s = ↑(greatestOfBdd b Hb Hinh)
[PROOFSTEP]
have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩
[GOAL]
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → z ≤ b
Hinh : ∃ z, z ∈ s
this : Set.Nonempty s ∧ BddAbove s
⊢ sSup s = ↑(greatestOfBdd b Hb Hinh)
[PROOFSTEP]
simp only [sSup, this, and_self, dite_true]
[GOAL]
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → z ≤ b
Hinh : ∃ z, z ∈ s
this : Set.Nonempty s ∧ BddAbove s
⊢ ↑(greatestOfBdd (choose (_ : BddAbove s)) (_ : choose (_ : BddAbove s) ∈ upperBounds s) (_ : Set.Nonempty s)) =
    ↑(greatestOfBdd b Hb Hinh)
[PROOFSTEP]
convert (coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm
[GOAL]
⊢ ¬(Set.Nonempty ∅ ∧ BddAbove ∅)
[PROOFSTEP]
simp
[GOAL]
s : Set ℤ
h : ¬BddAbove s
⊢ ¬(Set.Nonempty s ∧ BddAbove s)
[PROOFSTEP]
simp [h]
[GOAL]
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → b ≤ z
Hinh : ∃ z, z ∈ s
⊢ sInf s = ↑(leastOfBdd b Hb Hinh)
[PROOFSTEP]
have : s.Nonempty ∧ BddBelow s := ⟨Hinh, b, Hb⟩
[GOAL]
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → b ≤ z
Hinh : ∃ z, z ∈ s
this : Set.Nonempty s ∧ BddBelow s
⊢ sInf s = ↑(leastOfBdd b Hb Hinh)
[PROOFSTEP]
simp only [sInf, this, and_self, dite_true]
[GOAL]
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → b ≤ z
Hinh : ∃ z, z ∈ s
this : Set.Nonempty s ∧ BddBelow s
⊢ ↑(leastOfBdd (choose (_ : BddBelow s)) (_ : choose (_ : BddBelow s) ∈ lowerBounds s) (_ : Set.Nonempty s)) =
    ↑(leastOfBdd b Hb Hinh)
[PROOFSTEP]
convert (coe_leastOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) Hinh).symm
[GOAL]
⊢ ¬(Set.Nonempty ∅ ∧ BddBelow ∅)
[PROOFSTEP]
simp
[GOAL]
s : Set ℤ
h : ¬BddBelow s
⊢ ¬(Set.Nonempty s ∧ BddBelow s)
[PROOFSTEP]
simp [h]
[GOAL]
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddAbove s
⊢ sSup s ∈ s
[PROOFSTEP]
convert (greatestOfBdd _ (Classical.choose_spec h2) h1).2.1
[GOAL]
case h.e'_4
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddAbove s
⊢ sSup s = ↑(greatestOfBdd (choose h2) (_ : choose h2 ∈ upperBounds s) h1)
[PROOFSTEP]
exact dif_pos ⟨h1, h2⟩
[GOAL]
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddBelow s
⊢ sInf s ∈ s
[PROOFSTEP]
convert (leastOfBdd _ (Classical.choose_spec h2) h1).2.1
[GOAL]
case h.e'_4
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddBelow s
⊢ sInf s = ↑(leastOfBdd (choose h2) (_ : choose h2 ∈ lowerBounds s) h1)
[PROOFSTEP]
exact dif_pos ⟨h1, h2⟩


[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue ℤ S
x : ℤˣ
⊢ ↑abv ↑x = 1
[PROOFSTEP]
rcases Int.units_eq_one_or x with (rfl | rfl)
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue ℤ S
⊢ ↑abv ↑1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue ℤ S
⊢ ↑abv ↑(-1) = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
x : ℤˣ
⊢ ↑abv ↑↑x = 1
[PROOFSTEP]
rcases Int.units_eq_one_or x with (rfl | rfl)
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ ↑abv ↑↑1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ ↑abv ↑↑(-1) = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
x : ℤˣ
y : R
⊢ ↑abv (x • y) = ↑abv y
[PROOFSTEP]
rcases Int.units_eq_one_or x with (rfl | rfl)
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
y : R
⊢ ↑abv (1 • y) = ↑abv y
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
y : R
⊢ ↑abv (-1 • y) = ↑abv y
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
h : ↑n = 0
⊢ n = 0
[PROOFSTEP]
cases n
[GOAL]
case ofNat
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑(ofNat a✝) = 0
⊢ ofNat a✝ = 0
[PROOFSTEP]
erw [Int.cast_ofNat] at h
[GOAL]
case ofNat
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑a✝ = 0
⊢ ofNat a✝ = 0
[PROOFSTEP]
exact congr_arg _ (Nat.cast_eq_zero.1 h)
[GOAL]
case negSucc
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑-[a✝+1] = 0
⊢ -[a✝+1] = 0
[PROOFSTEP]
rw [cast_negSucc, neg_eq_zero, Nat.cast_eq_zero] at h
[GOAL]
case negSucc
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : a✝ + 1 = 0
⊢ -[a✝+1] = 0
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
h : n = 0
⊢ ↑n = 0
[PROOFSTEP]
rw [h, cast_zero]
[GOAL]
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
m n : ℤ
⊢ ↑m = ↑n ↔ m = n
[PROOFSTEP]
rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]
[GOAL]
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
⊢ ↑n = 1 ↔ n = 1
[PROOFSTEP]
rw [← cast_one, cast_inj]
[GOAL]
α : Type u_1
k : Type u_2
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
α : Type u_1
k : Type u_2
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m : ℤ
n_dvd : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0
[PROOFSTEP]
simp [Int.ediv_zero]
[GOAL]
case inr
α : Type u_1
k : Type u_2
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
exact cast_div n_dvd (cast_ne_zero.mpr hn)


[GOAL]
n : ℕ
x : ℤ
⊢ (↑n + 1) * x = x + ↑n * x
[PROOFSTEP]
rw [Int.add_mul, Int.add_comm, Int.one_mul]
[GOAL]
x✝¹ : ℕ
x✝ : ℤ
⊢ (fun n x => x ^ n) (x✝¹ + 1) x✝ = x✝ * (fun n x => x ^ n) x✝¹ x✝
[PROOFSTEP]
rw [Int.mul_comm]
[GOAL]
x✝¹ : ℕ
x✝ : ℤ
⊢ (fun n x => x ^ n) (x✝¹ + 1) x✝ = (fun n x => x ^ n) x✝¹ x✝ * x✝
[PROOFSTEP]
rfl
[GOAL]
m : ℕ
n : ℤ
⊢ (fun x x_1 => x * x_1) (ofNat (succ m)) n = n + (fun x x_1 => x * x_1) (ofNat m) n
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_succ, Int.add_mul, Int.add_comm, Int.one_mul]
[GOAL]
m : ℕ
n : ℤ
⊢ (fun x x_1 => x * x_1) -[m+1] n = -(fun x x_1 => x * x_1) (↑(succ m)) n
[PROOFSTEP]
simp only [negSucc_coe, ofNat_succ, Int.neg_mul]
[GOAL]
⊢ AddCommMonoid ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ AddMonoid ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Monoid ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CommMonoid ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CommSemigroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Semigroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ AddCommGroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ AddGroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ AddCommSemigroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ AddSemigroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CommSemiring ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Semiring ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Ring ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Distrib ℤ
[PROOFSTEP]
infer_instance
[GOAL]
a : ℤ
⊢ succ (-succ a) = -a
[PROOFSTEP]
rw [neg_succ, succ_pred]
[GOAL]
a : ℤ
⊢ -pred a = succ (-a)
[PROOFSTEP]
rw [neg_eq_iff_eq_neg.mp (neg_succ (-a)), neg_neg]
[GOAL]
a : ℤ
⊢ pred (-pred a) = -a
[PROOFSTEP]
rw [neg_pred, pred_succ]
[GOAL]
n : ℕ
h : 0 < n
⊢ ↑(n - 1) = ↑n - 1
[PROOFSTEP]
cases n
[GOAL]
case zero
h : 0 < zero
⊢ ↑(zero - 1) = ↑zero - 1
case succ n✝ : ℕ h : 0 < Nat.succ n✝ ⊢ ↑(Nat.succ n✝ - 1) = ↑(Nat.succ n✝) - 1
[PROOFSTEP]
cases h
[GOAL]
case succ
n✝ : ℕ
h : 0 < Nat.succ n✝
⊢ ↑(Nat.succ n✝ - 1) = ↑(Nat.succ n✝) - 1
[PROOFSTEP]
simp
[GOAL]
p : ℤ → Prop
i : ℤ
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
⊢ p i
[PROOFSTEP]
induction i with
| ofNat i =>
  induction i with
  | zero => exact hz
  | succ i ih => exact hp _ ih
| negSucc i =>
  suffices ∀ n : ℕ, p (-n) from this (i + 1)
  intro n;
  induction n with
  | zero => simp [hz, Nat.cast_zero]
  | succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
p : ℤ → Prop
i : ℤ
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
⊢ p i
[PROOFSTEP]
induction i with
| ofNat i =>
  induction i with
  | zero => exact hz
  | succ i ih => exact hp _ ih
| negSucc i =>
  suffices ∀ n : ℕ, p (-n) from this (i + 1)
  intro n;
  induction n with
  | zero => simp [hz, Nat.cast_zero]
  | succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
case ofNat
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (ofNat i)
[PROOFSTEP]

| ofNat i =>
  induction i with
  | zero => exact hz
  | succ i ih => exact hp _ ih
[GOAL]
case ofNat
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (ofNat i)
[PROOFSTEP]
induction i with
| zero => exact hz
| succ i ih => exact hp _ ih
[GOAL]
case ofNat
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (ofNat i)
[PROOFSTEP]
induction i with
| zero => exact hz
| succ i ih => exact hp _ ih
[GOAL]
case ofNat.zero
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
⊢ p (ofNat zero)
[PROOFSTEP]

| zero => exact hz
[GOAL]
case ofNat.zero
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
⊢ p (ofNat zero)
[PROOFSTEP]
exact hz
[GOAL]
case ofNat.succ
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
ih : p (ofNat i)
⊢ p (ofNat (Nat.succ i))
[PROOFSTEP]

| succ i ih => exact hp _ ih
[GOAL]
case ofNat.succ
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
ih : p (ofNat i)
⊢ p (ofNat (Nat.succ i))
[PROOFSTEP]
exact hp _ ih
[GOAL]
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p -[i+1]
[PROOFSTEP]

| negSucc i =>
  suffices ∀ n : ℕ, p (-n) from this (i + 1)
  intro n;
  induction n with
  | zero => simp [hz, Nat.cast_zero]
  | succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p -[i+1]
[PROOFSTEP]
suffices ∀ n : ℕ, p (-n) from this (i + 1)
[GOAL]
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ ∀ (n : ℕ), p (-↑n)
[PROOFSTEP]
intro n
[GOAL]
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
⊢ p (-↑n)
[PROOFSTEP]
induction n with
| zero => simp [hz, Nat.cast_zero]
| succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
⊢ p (-↑n)
[PROOFSTEP]
induction n with
| zero => simp [hz, Nat.cast_zero]
| succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
case negSucc.zero
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (-↑zero)
[PROOFSTEP]

| zero => simp [hz, Nat.cast_zero]
[GOAL]
case negSucc.zero
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (-↑zero)
[PROOFSTEP]
simp [hz, Nat.cast_zero]
[GOAL]
case negSucc.succ
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
ih : p (-↑n)
⊢ p (-↑(Nat.succ n))
[PROOFSTEP]

| succ n ih => convert hn _ ih using 1; simp [sub_eq_neg_add]
[GOAL]
case negSucc.succ
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
ih : p (-↑n)
⊢ p (-↑(Nat.succ n))
[PROOFSTEP]
convert hn _ ih using 1
[GOAL]
case h.e'_1
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
ih : p (-↑n)
⊢ -↑(Nat.succ n) = -↑n - 1
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -((- -[m+1] - 1) / ↑(Nat.succ n) + 1)
[PROOFSTEP]
rw [show (- -[m+1] : ℤ) = (m + 1 : ℤ) by rfl]
[GOAL]
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ - -[m+1] = ↑m + 1
[PROOFSTEP]
rfl
[GOAL]
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -((↑m + 1 - 1) / ↑(Nat.succ n) + 1)
[PROOFSTEP]
rw [add_sub_cancel]
[GOAL]
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -(↑m / ↑(Nat.succ n) + 1)
[PROOFSTEP]
rfl


[GOAL]
m n : ℤ
⊢ ¬n % 2 = 1 ↔ n % 2 = 0
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h h
[GOAL]
case inl
m n : ℤ
h : n % 2 = 0
⊢ ¬n % 2 = 1 ↔ n % 2 = 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr
m n : ℤ
h : n % 2 = 1
⊢ ¬n % 2 = 1 ↔ n % 2 = 0
[PROOFSTEP]
simp [h]
[GOAL]
m n : ℤ
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h h
[GOAL]
case inl
m n : ℤ
h : n % 2 = 0
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
[PROOFSTEP]
simp [h]
[GOAL]
case inr
m n : ℤ
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
[PROOFSTEP]
simp [h]
[GOAL]
m✝ n : ℤ
x✝ : Even n
m : ℤ
hm : n = m + m
⊢ n % 2 = 0
[PROOFSTEP]
simp [← two_mul, hm]
[GOAL]
m n : ℤ
h : n % 2 = 0
⊢ n % 2 + 2 * (n / 2) = n / 2 + n / 2
[PROOFSTEP]
simp [← two_mul, h]
[GOAL]
m✝ n : ℤ
x✝ : Odd n
m : ℤ
hm : n = 2 * m + 1
⊢ n % 2 = 1
[PROOFSTEP]
rw [hm, add_emod]
[GOAL]
m✝ n : ℤ
x✝ : Odd n
m : ℤ
hm : n = 2 * m + 1
⊢ (2 * m % 2 + 1 % 2) % 2 = 1
[PROOFSTEP]
norm_num
[GOAL]
m n : ℤ
h : n % 2 = 1
⊢ n % 2 + 2 * (n / 2) = 2 * (n / 2) + 1
[PROOFSTEP]
rw [h]
[GOAL]
m n : ℤ
h : n % 2 = 1
⊢ 1 + 2 * (n / 2) = 2 * (n / 2) + 1
[PROOFSTEP]
abel
[GOAL]
m n : ℤ
h : n % 2 = 1
⊢ 1 + 2 * (n / 2) = 2 * (n / 2) + 1
[PROOFSTEP]
abel
[GOAL]
m n : ℤ
⊢ ¬Even n ↔ n % 2 = 1
[PROOFSTEP]
rw [even_iff, emod_two_ne_zero]
[GOAL]
m n : ℤ
⊢ ¬Odd n ↔ n % 2 = 0
[PROOFSTEP]
rw [odd_iff, emod_two_ne_one]
[GOAL]
m n : ℤ
⊢ Even n ↔ ¬Odd n
[PROOFSTEP]
rw [not_odd_iff, even_iff]
[GOAL]
m n : ℤ
⊢ Odd n ↔ ¬Even n
[PROOFSTEP]
rw [not_even_iff, odd_iff]
[GOAL]
m n : ℤ
⊢ IsCompl {n | Even n} {n | Odd n}
[PROOFSTEP]
simp [← Set.compl_setOf, isCompl_compl]
[GOAL]
m n✝ n : ℤ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1
[PROOFSTEP]
simpa only [two_mul, exists_or, Odd, Even] using even_or_odd n
[GOAL]
m n✝ n : ℤ
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]
cases even_or_odd n with
| inl h => exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
| inr h => exact Or.inr ⟨h, odd_iff_not_even.mp h⟩
[GOAL]
m n✝ n : ℤ
x✝ : Even n ∨ Odd n
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]
cases even_or_odd n with
| inl h => exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
| inr h => exact Or.inr ⟨h, odd_iff_not_even.mp h⟩
[GOAL]
case inl
m n✝ n : ℤ
h : Even n
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]

| inl h => exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
[GOAL]
case inl
m n✝ n : ℤ
h : Even n
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]
exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
[GOAL]
case inr
m n✝ n : ℤ
h : Odd n
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]

| inr h => exact Or.inr ⟨h, odd_iff_not_even.mp h⟩
[GOAL]
case inr
m n✝ n : ℤ
h : Odd n
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]
exact Or.inr ⟨h, odd_iff_not_even.mp h⟩
[GOAL]
m n✝ n : ℤ
⊢ ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)
[PROOFSTEP]
rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩)
[GOAL]
case inl.intro
m n k : ℤ
⊢ ∃ k_1, Xor' (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
[PROOFSTEP]
use k
[GOAL]
case inr.intro
m n k : ℤ
⊢ ∃ k_1, Xor' (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
[PROOFSTEP]
use k
[GOAL]
case h
m n k : ℤ
⊢ Xor' (k + k = 2 * k) (k + k = 2 * k + 1)
[PROOFSTEP]
simpa only [← two_mul, Xor', true_and_iff, eq_self_iff_true, not_true, or_false_iff, and_false_iff] using
  (succ_ne_self (2 * k)).symm
[GOAL]
case h
m n k : ℤ
⊢ Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
[PROOFSTEP]
simp only [Xor', add_right_eq_self, false_or_iff, eq_self_iff_true, not_true, not_false_iff, one_ne_zero, and_self_iff]
[GOAL]
m n : ℤ
⊢ ¬Even 1
[PROOFSTEP]
rw [even_iff]
[GOAL]
m n : ℤ
⊢ ¬1 % 2 = 0
[PROOFSTEP]
norm_num
[GOAL]
m n : ℤ
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
cases' emod_two_eq_zero_or_one m with h₁ h₁
[GOAL]
case inl
m n : ℤ
h₁ : m % 2 = 0
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inr
m n : ℤ
h₁ : m % 2 = 1
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inl.inl
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.add_emod]
[GOAL]
case inl.inr
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.add_emod]
[GOAL]
case inr.inl
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.add_emod]
[GOAL]
case inr.inr
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.add_emod]
[GOAL]
m n : ℤ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)
[PROOFSTEP]
rw [even_add, even_iff_not_odd, even_iff_not_odd, not_iff_not]
[GOAL]
m n✝ n : ℤ
⊢ ¬Even (bit1 n)
[PROOFSTEP]
simp [bit1, parity_simps]
[GOAL]
m n✝ n : ℤ
⊢ ¬2 ∣ 2 * n + 1
[PROOFSTEP]
simp [add_emod]
[GOAL]
m n : ℤ
⊢ Even (m - n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [sub_eq_add_neg, parity_simps]
[GOAL]
m n : ℤ
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)
[PROOFSTEP]
rw [even_sub, even_iff_not_odd, even_iff_not_odd, not_iff_not]
[GOAL]
m n : ℤ
⊢ Even (n + 1) ↔ ¬Even n
[PROOFSTEP]
simp [even_add]
[GOAL]
m n : ℤ
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
cases' emod_two_eq_zero_or_one m with h₁ h₁
[GOAL]
case inl
m n : ℤ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inr
m n : ℤ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inl.inl
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.mul_emod]
[GOAL]
case inl.inr
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.mul_emod]
[GOAL]
case inr.inl
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.mul_emod]
[GOAL]
case inr.inr
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.mul_emod]
[GOAL]
m n : ℤ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n
[PROOFSTEP]
simp [not_or, parity_simps]
[GOAL]
m n✝ : ℤ
n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
m n : ℤ
⊢ Even (m ^ Nat.zero) ↔ Even m ∧ Nat.zero ≠ 0
[PROOFSTEP]
simp [*, even_mul, pow_succ]
[GOAL]
case succ
m n✝ : ℤ
n : ℕ
ih : Even (m ^ n) ↔ Even m ∧ n ≠ 0
⊢ Even (m ^ Nat.succ n) ↔ Even m ∧ Nat.succ n ≠ 0
[PROOFSTEP]
simp [*, even_mul, pow_succ]
[GOAL]
case succ
m n✝ : ℤ
n : ℕ
ih : Even (m ^ n) ↔ Even m ∧ n ≠ 0
⊢ Even m → ¬n = 0 → Even m
[PROOFSTEP]
tauto
[GOAL]
m n✝ : ℤ
n : ℕ
⊢ Odd (m ^ n) ↔ Odd m ∨ n = 0
[PROOFSTEP]
rw [← not_iff_not, ← Int.even_iff_not_odd, not_or, ← Int.even_iff_not_odd, Int.even_pow]
[GOAL]
m n : ℤ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)
[PROOFSTEP]
rw [odd_iff_not_even, even_add, not_iff, odd_iff_not_even]
[GOAL]
m n : ℤ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)
[PROOFSTEP]
rw [add_comm, odd_add]
[GOAL]
m n : ℤ
h : Odd (m + n)
hnot : m = n
⊢ False
[PROOFSTEP]
simp [hnot, parity_simps] at h
[GOAL]
m n : ℤ
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)
[PROOFSTEP]
rw [odd_iff_not_even, even_sub, not_iff, odd_iff_not_even]
[GOAL]
m n : ℤ
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)
[PROOFSTEP]
rw [odd_iff_not_even, even_sub, not_iff, not_iff_comm, odd_iff_not_even]
[GOAL]
m n✝ n : ℤ
⊢ Even (n * (n + 1))
[PROOFSTEP]
simpa [even_mul, parity_simps] using n.even_or_odd
[GOAL]
m n✝ : ℤ
n : ℕ
⊢ Even ↑n ↔ Even n
[PROOFSTEP]
rw_mod_cast [even_iff, Nat.even_iff]
[GOAL]
m n✝ : ℤ
n : ℕ
⊢ Odd ↑n ↔ Odd n
[PROOFSTEP]
rw [odd_iff_not_even, Nat.odd_iff_not_even, even_coe_nat]
[GOAL]
m n : ℤ
⊢ Even (natAbs n) ↔ Even n
[PROOFSTEP]
simp [even_iff_two_dvd, dvd_natAbs, coe_nat_dvd_left.symm]
[GOAL]
m n : ℤ
⊢ Odd (natAbs n) ↔ Odd n
[PROOFSTEP]
rw [odd_iff_not_even, Nat.odd_iff_not_even, natAbs_even]
[GOAL]
m n a b : ℤ
ha : Odd a
hb : Odd b
⊢ 4 ∣ a + b ∨ 4 ∣ a - b
[PROOFSTEP]
obtain ⟨m, rfl⟩ := ha
[GOAL]
case intro
m✝ n b : ℤ
hb : Odd b
m : ℤ
⊢ 4 ∣ 2 * m + 1 + b ∨ 4 ∣ 2 * m + 1 - b
[PROOFSTEP]
obtain ⟨n, rfl⟩ := hb
[GOAL]
case intro.intro
m✝ n✝ m n : ℤ
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
obtain h | h := Int.even_or_odd (m + n)
[GOAL]
case intro.intro.inl
m✝ n✝ m n : ℤ
h : Even (m + n)
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
right
[GOAL]
case intro.intro.inl.h
m✝ n✝ m n : ℤ
h : Even (m + n)
⊢ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
rw [Int.even_add, ← Int.even_sub] at h
[GOAL]
case intro.intro.inl.h
m✝ n✝ m n : ℤ
h : Even (m - n)
⊢ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
obtain ⟨k, hk⟩ := h
[GOAL]
case intro.intro.inl.h.intro
m✝ n✝ m n k : ℤ
hk : m - n = k + k
⊢ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
convert dvd_mul_right 4 k using 1
[GOAL]
case h.e'_4
m✝ n✝ m n k : ℤ
hk : m - n = k + k
⊢ 2 * m + 1 - (2 * n + 1) = 4 * k
[PROOFSTEP]
rw [eq_add_of_sub_eq hk, mul_add, add_assoc, add_sub_cancel, ← two_mul, ← mul_assoc]
[GOAL]
case h.e'_4
m✝ n✝ m n k : ℤ
hk : m - n = k + k
⊢ 2 * 2 * k = 4 * k
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.inr
m✝ n✝ m n : ℤ
h : Odd (m + n)
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
left
[GOAL]
case intro.intro.inr.h
m✝ n✝ m n : ℤ
h : Odd (m + n)
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1)
[PROOFSTEP]
obtain ⟨k, hk⟩ := h
[GOAL]
case intro.intro.inr.h.intro
m✝ n✝ m n k : ℤ
hk : m + n = 2 * k + 1
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1)
[PROOFSTEP]
convert dvd_mul_right 4 (k + 1) using 1
[GOAL]
case h.e'_4
m✝ n✝ m n k : ℤ
hk : m + n = 2 * k + 1
⊢ 2 * m + 1 + (2 * n + 1) = 4 * (k + 1)
[PROOFSTEP]
rw [eq_sub_of_add_eq hk, add_right_comm, ← add_sub, mul_add, mul_sub, add_assoc, add_assoc, sub_add, add_assoc, ←
  sub_sub (2 * n), sub_self, zero_sub, sub_neg_eq_add, ← mul_assoc, mul_add]
[GOAL]
case h.e'_4
m✝ n✝ m n k : ℤ
hk : m + n = 2 * k + 1
⊢ 2 * 2 * k + (2 * 1 + (1 + 1)) = 4 * k + 4 * 1
[PROOFSTEP]
rfl
[GOAL]
m n : ℤ
⊢ Odd n → 2 * (n / 2) + 1 = n
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case intro
m c : ℤ
⊢ 2 * ((2 * c + 1) / 2) + 1 = 2 * c + 1
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case intro
m c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1
[PROOFSTEP]
convert Int.ediv_add_emod' (2 * c + 1) 2
[GOAL]
case h.e'_2.h.e'_6
m c : ℤ
⊢ 1 = (2 * c + 1) % 2
[PROOFSTEP]
simp [Int.add_emod]
[GOAL]
m n : ℤ
⊢ Odd n → n / 2 * 2 + 1 = n
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case intro
m c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1
[PROOFSTEP]
convert Int.ediv_add_emod' (2 * c + 1) 2
[GOAL]
case h.e'_2.h.e'_6
m c : ℤ
⊢ 1 = (2 * c + 1) % 2
[PROOFSTEP]
simp [Int.add_emod]
[GOAL]
m n : ℤ
⊢ Odd n → 1 + n / 2 * 2 = n
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case intro
m c : ℤ
⊢ 1 + (2 * c + 1) / 2 * 2 = 2 * c + 1
[PROOFSTEP]
rw [add_comm]
[GOAL]
case intro
m c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1
[PROOFSTEP]
convert Int.ediv_add_emod' (2 * c + 1) 2
[GOAL]
case h.e'_2.h.e'_6
m c : ℤ
⊢ 1 = (2 * c + 1) % 2
[PROOFSTEP]
simp [Int.add_emod]
[GOAL]
m✝ n✝ m n : ℤ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)
[PROOFSTEP]
simp [*, (by decide : ¬2 = 0), parity_simps]
[GOAL]
m✝ n✝ m n : ℤ
h : Even m
⊢ ¬2 = 0
[PROOFSTEP]
decide
[GOAL]
m n : ℤ
⊢ ¬Even 25394535
[PROOFSTEP]
simp


[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ a * a = b * b
[PROOFSTEP]
rw [← abs_eq_iff_mul_self_eq, abs_eq_natAbs, abs_eq_natAbs]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ ↑(natAbs a) = ↑(natAbs b)
[PROOFSTEP]
exact Int.coe_nat_inj'.symm
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ a * a < b * b
[PROOFSTEP]
rw [← abs_lt_iff_mul_self_lt, abs_eq_natAbs, abs_eq_natAbs]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ ↑(natAbs a) < ↑(natAbs b)
[PROOFSTEP]
exact Int.ofNat_lt.symm
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a ≤ natAbs b ↔ a * a ≤ b * b
[PROOFSTEP]
rw [← abs_le_iff_mul_self_le, abs_eq_natAbs, abs_eq_natAbs]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a ≤ natAbs b ↔ ↑(natAbs a) ≤ ↑(natAbs b)
[PROOFSTEP]
exact Int.ofNat_le.symm
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
h : a * b ∣ c
⊢ b ∣ c / a
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
a b✝ : ℤ
n : ℕ
b c : ℤ
h : 0 * b ∣ c
⊢ b ∣ c / 0
[PROOFSTEP]
simp only [Int.ediv_zero, dvd_zero]
[GOAL]
case inr
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a
[PROOFSTEP]
rcases h with ⟨d, rfl⟩
[GOAL]
case inr.intro
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≠ 0
d : ℤ
⊢ b ∣ a * b * d / a
[PROOFSTEP]
refine' ⟨d, _⟩
[GOAL]
case inr.intro
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≠ 0
d : ℤ
⊢ a * b * d / a = b * d
[PROOFSTEP]
rw [mul_assoc, Int.mul_ediv_cancel_left _ ha]
[GOAL]
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
⊢ x = 0
[PROOFSTEP]
by_cases hm : m = 0
[GOAL]
case pos
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
hm : m = 0
⊢ x = 0
[PROOFSTEP]
subst m
[GOAL]
case pos
a b : ℤ
n : ℕ
x : ℤ
h1 : 0 ∣ x
h2 : |x| < 0
⊢ x = 0
[PROOFSTEP]
exact zero_dvd_iff.mp h1
[GOAL]
case neg
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
hm : ¬m = 0
⊢ x = 0
[PROOFSTEP]
rcases h1 with ⟨d, rfl⟩
[GOAL]
case neg.intro
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : |m * d| < m
⊢ m * d = 0
[PROOFSTEP]
apply mul_eq_zero_of_right
[GOAL]
case neg.intro.h
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : |m * d| < m
⊢ d = 0
[PROOFSTEP]
rw [← abs_lt_one_iff, ← mul_lt_iff_lt_one_right (abs_pos.mpr hm), ← abs_mul]
[GOAL]
case neg.intro.h
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : |m * d| < m
⊢ |m * d| < |m|
[PROOFSTEP]
exact lt_of_lt_of_le h2 (le_abs_self m)


[GOAL]
α : Type u_1
R : Type u_2
inst✝ : DivisionRing R
n : ℕ
⊢ ↑(-↑n) = -↑n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
m n : ℤ
n_dvd : n ∣ m
n_nonzero : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
rcases n_dvd with ⟨k, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
n_nonzero : ↑n ≠ 0
k : ℤ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
[PROOFSTEP]
have : n ≠ 0 := by
  rintro rfl
  simp at n_nonzero
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
n_nonzero : ↑n ≠ 0
k : ℤ
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
k : ℤ
n_nonzero : ↑0 ≠ 0
⊢ False
[PROOFSTEP]
simp at n_nonzero
[GOAL]
case intro
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
n_nonzero : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
[PROOFSTEP]
rw [Int.mul_ediv_cancel_left _ this, mul_comm n k, Int.cast_mul, mul_div_cancel _ n_nonzero]


[GOAL]
a b x : ℤ
⊢ x ∈
      (fun a b => map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (toNat (b + 1 - a)))) a
        b ↔
    a ≤ x ∧ x ≤ b
[PROOFSTEP]
simp_rw [mem_map, mem_range, Int.lt_toNat, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
  addLeftEmbedding_apply]
[GOAL]
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b + 1 - a ∧ a + ↑a_1 = x) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b + 1 - a ∧ a + ↑a_1 = x) → a ≤ x ∧ x ≤ b
[PROOFSTEP]
rintro ⟨a, h, rfl⟩
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : ↑a < b + 1 - a✝
⊢ a✝ ≤ a✝ + ↑a ∧ a✝ + ↑a ≤ b
[PROOFSTEP]
rw [lt_sub_iff_add_lt, Int.lt_add_one_iff, add_comm] at h
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : a✝ + ↑a ≤ b
⊢ a✝ ≤ a✝ + ↑a ∧ a✝ + ↑a ≤ b
[PROOFSTEP]
exact ⟨Int.le.intro a rfl, h⟩
[GOAL]
case mpr
a b x : ℤ
⊢ a ≤ x ∧ x ≤ b → ∃ a_2, ↑a_2 < b + 1 - a ∧ a + ↑a_2 = x
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case mpr.intro
a b x : ℤ
ha : a ≤ x
hb : x ≤ b
⊢ ∃ a_1, ↑a_1 < b + 1 - a ∧ a + ↑a_1 = x
[PROOFSTEP]
use(x - a).toNat
[GOAL]
case h
a b x : ℤ
ha : a ≤ x
hb : x ≤ b
⊢ ↑(toNat (x - a)) < b + 1 - a ∧ a + ↑(toNat (x - a)) = x
[PROOFSTEP]
rw [← lt_add_one_iff] at hb
[GOAL]
case h
a b x : ℤ
ha : a ≤ x
hb : x < b + 1
⊢ ↑(toNat (x - a)) < b + 1 - a ∧ a + ↑(toNat (x - a)) = x
[PROOFSTEP]
rw [toNat_sub_of_le ha]
[GOAL]
case h
a b x : ℤ
ha : a ≤ x
hb : x < b + 1
⊢ x - a < b + 1 - a ∧ a + (x - a) = x
[PROOFSTEP]
exact ⟨sub_lt_sub_right hb _, add_sub_cancel'_right _ _⟩
[GOAL]
a b x : ℤ
⊢ x ∈ (fun a b => map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (toNat (b - a)))) a b ↔
    a ≤ x ∧ x < b
[PROOFSTEP]
simp_rw [mem_map, mem_range, Int.lt_toNat, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
  addLeftEmbedding_apply]
[GOAL]
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a ∧ a + ↑a_1 = x) ↔ a ≤ x ∧ x < b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a ∧ a + ↑a_1 = x) → a ≤ x ∧ x < b
[PROOFSTEP]
rintro ⟨a, h, rfl⟩
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : ↑a < b - a✝
⊢ a✝ ≤ a✝ + ↑a ∧ a✝ + ↑a < b
[PROOFSTEP]
exact ⟨Int.le.intro a rfl, lt_sub_iff_add_lt'.mp h⟩
[GOAL]
case mpr
a b x : ℤ
⊢ a ≤ x ∧ x < b → ∃ a_2, ↑a_2 < b - a ∧ a + ↑a_2 = x
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case mpr.intro
a b x : ℤ
ha : a ≤ x
hb : x < b
⊢ ∃ a_1, ↑a_1 < b - a ∧ a + ↑a_1 = x
[PROOFSTEP]
use(x - a).toNat
[GOAL]
case h
a b x : ℤ
ha : a ≤ x
hb : x < b
⊢ ↑(toNat (x - a)) < b - a ∧ a + ↑(toNat (x - a)) = x
[PROOFSTEP]
rw [toNat_sub_of_le ha]
[GOAL]
case h
a b x : ℤ
ha : a ≤ x
hb : x < b
⊢ x - a < b - a ∧ a + (x - a) = x
[PROOFSTEP]
exact ⟨sub_lt_sub_right hb _, add_sub_cancel'_right _ _⟩
[GOAL]
a b x : ℤ
⊢ x ∈
      (fun a b => map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (range (toNat (b - a)))) a
        b ↔
    a < x ∧ x ≤ b
[PROOFSTEP]
simp_rw [mem_map, mem_range, Int.lt_toNat, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
  addLeftEmbedding_apply]
[GOAL]
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a ∧ a + 1 + ↑a_1 = x) ↔ a < x ∧ x ≤ b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a ∧ a + 1 + ↑a_1 = x) → a < x ∧ x ≤ b
[PROOFSTEP]
rintro ⟨a, h, rfl⟩
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : ↑a < b - a✝
⊢ a✝ < a✝ + 1 + ↑a ∧ a✝ + 1 + ↑a ≤ b
[PROOFSTEP]
rw [← add_one_le_iff, le_sub_iff_add_le', add_comm _ (1 : ℤ), ← add_assoc] at h
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : a✝ + 1 + ↑a ≤ b
⊢ a✝ < a✝ + 1 + ↑a ∧ a✝ + 1 + ↑a ≤ b
[PROOFSTEP]
exact ⟨Int.le.intro a rfl, h⟩
[GOAL]
case mpr
a b x : ℤ
⊢ a < x ∧ x ≤ b → ∃ a_2, ↑a_2 < b - a ∧ a + 1 + ↑a_2 = x
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case mpr.intro
a b x : ℤ
ha : a < x
hb : x ≤ b
⊢ ∃ a_1, ↑a_1 < b - a ∧ a + 1 + ↑a_1 = x
[PROOFSTEP]
use(x - (a + 1)).toNat
[GOAL]
case h
a b x : ℤ
ha : a < x
hb : x ≤ b
⊢ ↑(toNat (x - (a + 1))) < b - a ∧ a + 1 + ↑(toNat (x - (a + 1))) = x
[PROOFSTEP]
rw [toNat_sub_of_le ha, ← add_one_le_iff, sub_add, add_sub_cancel]
[GOAL]
case h
a b x : ℤ
ha : a < x
hb : x ≤ b
⊢ x - a ≤ b - a ∧ a + 1 + (x - (a + 1)) = x
[PROOFSTEP]
exact ⟨sub_le_sub_right hb _, add_sub_cancel'_right _ _⟩
[GOAL]
a b x : ℤ
⊢ x ∈
      (fun a b =>
          map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (range (toNat (b - a - 1))))
        a b ↔
    a < x ∧ x < b
[PROOFSTEP]
simp_rw [mem_map, mem_range, Int.lt_toNat, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
  addLeftEmbedding_apply]
[GOAL]
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a - 1 ∧ a + 1 + ↑a_1 = x) ↔ a < x ∧ x < b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a - 1 ∧ a + 1 + ↑a_1 = x) → a < x ∧ x < b
[PROOFSTEP]
rintro ⟨a, h, rfl⟩
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : ↑a < b - a✝ - 1
⊢ a✝ < a✝ + 1 + ↑a ∧ a✝ + 1 + ↑a < b
[PROOFSTEP]
rw [sub_sub, lt_sub_iff_add_lt'] at h
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : a✝ + 1 + ↑a < b
⊢ a✝ < a✝ + 1 + ↑a ∧ a✝ + 1 + ↑a < b
[PROOFSTEP]
exact ⟨Int.le.intro a rfl, h⟩
[GOAL]
case mpr
a b x : ℤ
⊢ a < x ∧ x < b → ∃ a_2, ↑a_2 < b - a - 1 ∧ a + 1 + ↑a_2 = x
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case mpr.intro
a b x : ℤ
ha : a < x
hb : x < b
⊢ ∃ a_1, ↑a_1 < b - a - 1 ∧ a + 1 + ↑a_1 = x
[PROOFSTEP]
use(x - (a + 1)).toNat
[GOAL]
case h
a b x : ℤ
ha : a < x
hb : x < b
⊢ ↑(toNat (x - (a + 1))) < b - a - 1 ∧ a + 1 + ↑(toNat (x - (a + 1))) = x
[PROOFSTEP]
rw [toNat_sub_of_le ha, sub_sub]
[GOAL]
case h
a b x : ℤ
ha : a < x
hb : x < b
⊢ x - (a + 1) < b - (a + 1) ∧ a + 1 + (x - (a + 1)) = x
[PROOFSTEP]
exact ⟨sub_lt_sub_right hb _, add_sub_cancel'_right _ _⟩
[GOAL]
a b : ℤ
⊢ ofNat (card (range (toNat (a ⊔ b + 1 - a ⊓ b)))) = ofNat (natAbs (b - a) + 1)
[PROOFSTEP]
change ((↑) : ℕ → ℤ) _ = ((↑) : ℕ → ℤ) _
[GOAL]
a b : ℤ
⊢ ↑(card (range (toNat (a ⊔ b + 1 - a ⊓ b)))) = ↑(natAbs (b - a) + 1)
[PROOFSTEP]
rw [card_range, sup_eq_max, inf_eq_min, Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.ofNat_add,
  Int.coe_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]
[GOAL]
a b : ℤ
h : a ≤ b + 1
⊢ ↑(card (Icc a b)) = b + 1 - a
[PROOFSTEP]
rw [card_Icc, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a ≤ b
⊢ ↑(card (Ico a b)) = b - a
[PROOFSTEP]
rw [card_Ico, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a ≤ b
⊢ ↑(card (Ioc a b)) = b - a
[PROOFSTEP]
rw [card_Ioc, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a < b
⊢ ↑(card (Ioo a b)) = b - a - 1
[PROOFSTEP]
rw [card_Ioo, sub_sub, toNat_sub_of_le h]
[GOAL]
a b : ℤ
⊢ Fintype.card ↑(Set.Icc a b) = toNat (b + 1 - a)
[PROOFSTEP]
rw [← card_Icc, Fintype.card_ofFinset]
[GOAL]
a b : ℤ
⊢ Fintype.card ↑(Set.Ico a b) = toNat (b - a)
[PROOFSTEP]
rw [← card_Ico, Fintype.card_ofFinset]
[GOAL]
a b : ℤ
⊢ Fintype.card ↑(Set.Ioc a b) = toNat (b - a)
[PROOFSTEP]
rw [← card_Ioc, Fintype.card_ofFinset]
[GOAL]
a b : ℤ
⊢ Fintype.card ↑(Set.Ioo a b) = toNat (b - a - 1)
[PROOFSTEP]
rw [← card_Ioo, Fintype.card_ofFinset]
[GOAL]
a b : ℤ
⊢ Fintype.card ↑(Set.uIcc a b) = natAbs (b - a) + 1
[PROOFSTEP]
rw [← card_uIcc, Fintype.card_ofFinset]
[GOAL]
a b : ℤ
h : a ≤ b + 1
⊢ ↑(Fintype.card ↑(Set.Icc a b)) = b + 1 - a
[PROOFSTEP]
rw [card_fintype_Icc, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a ≤ b
⊢ ↑(Fintype.card ↑(Set.Ico a b)) = b - a
[PROOFSTEP]
rw [card_fintype_Ico, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a ≤ b
⊢ ↑(Fintype.card ↑(Set.Ioc a b)) = b - a
[PROOFSTEP]
rw [card_fintype_Ioc, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a < b
⊢ ↑(Fintype.card ↑(Set.Ioo a b)) = b - a - 1
[PROOFSTEP]
rw [card_fintype_Ioo, sub_sub, toNat_sub_of_le h]
[GOAL]
a✝ b n a : ℤ
h : 0 ≤ a
⊢ image (fun x => x % a) (Ico n (n + a)) = Ico 0 a
[PROOFSTEP]
obtain rfl | ha := eq_or_lt_of_le h
[GOAL]
case inl
a b n : ℤ
h : 0 ≤ 0
⊢ image (fun x => x % 0) (Ico n (n + 0)) = Ico 0 0
[PROOFSTEP]
simp
[GOAL]
case inr
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
⊢ image (fun x => x % a) (Ico n (n + a)) = Ico 0 a
[PROOFSTEP]
ext i
[GOAL]
case inr.a
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ i ∈ image (fun x => x % a) (Ico n (n + a)) ↔ i ∈ Ico 0 a
[PROOFSTEP]
simp only [mem_image, mem_range, mem_Ico]
[GOAL]
case inr.a
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a
[PROOFSTEP]
constructor
[GOAL]
case inr.a.mp
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → 0 ≤ i ∧ i < a
[PROOFSTEP]
rintro ⟨i, _, rfl⟩
[GOAL]
case inr.a.mp.intro.intro
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
left✝ : n ≤ i ∧ i < n + a
⊢ 0 ≤ i % a ∧ i % a < a
[PROOFSTEP]
exact ⟨emod_nonneg i ha.ne', emod_lt_of_pos i ha⟩
[GOAL]
case inr.a.mpr
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ 0 ≤ i ∧ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
[PROOFSTEP]
intro hia
[GOAL]
case inr.a.mpr
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
[PROOFSTEP]
have hn := Int.emod_add_ediv n a
[GOAL]
case inr.a.mpr
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
[PROOFSTEP]
obtain hi | hi := lt_or_le i (n % a)
[GOAL]
case inr.a.mpr.inl
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
[PROOFSTEP]
refine' ⟨i + a * (n / a + 1), ⟨_, _⟩, _⟩
[GOAL]
case inr.a.mpr.inl.refine'_1
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)
[PROOFSTEP]
rw [add_comm (n / a), mul_add, mul_one, ← add_assoc]
[GOAL]
case inr.a.mpr.inl.refine'_1
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a + a * (n / a)
[PROOFSTEP]
refine' hn.symm.le.trans (add_le_add_right _ _)
[GOAL]
case inr.a.mpr.inl.refine'_1
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a ≤ i + a
[PROOFSTEP]
simpa only [zero_add] using add_le_add hia.left (Int.emod_lt_of_pos n ha).le
[GOAL]
case inr.a.mpr.inl.refine'_2
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a
[PROOFSTEP]
refine' lt_of_lt_of_le (add_lt_add_right hi (a * (n / a + 1))) _
[GOAL]
case inr.a.mpr.inl.refine'_2
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) ≤ n + a
[PROOFSTEP]
rw [mul_add, mul_one, ← add_assoc, hn]
[GOAL]
case inr.a.mpr.inl.refine'_3
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
[PROOFSTEP]
rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hia.left hia.right]
[GOAL]
case inr.a.mpr.inr
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
[PROOFSTEP]
refine' ⟨i + a * (n / a), ⟨_, _⟩, _⟩
[GOAL]
case inr.a.mpr.inr.refine'_1
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ n ≤ i + a * (n / a)
[PROOFSTEP]
exact hn.symm.le.trans (add_le_add_right hi _)
[GOAL]
case inr.a.mpr.inr.refine'_2
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < n + a
[PROOFSTEP]
rw [add_comm n a]
[GOAL]
case inr.a.mpr.inr.refine'_2
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < a + n
[PROOFSTEP]
refine' add_lt_add_of_lt_of_le hia.right (le_trans _ hn.le)
[GOAL]
case inr.a.mpr.inr.refine'_2
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ a * (n / a) ≤ n % a + a * (n / a)
[PROOFSTEP]
simp only [zero_le, le_add_iff_nonneg_left]
[GOAL]
case inr.a.mpr.inr.refine'_2
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ 0 ≤ n % a
[PROOFSTEP]
exact Int.emod_nonneg n (ne_of_gt ha)
[GOAL]
case inr.a.mpr.inr.refine'_3
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ (i + a * (n / a)) % a = i
[PROOFSTEP]
rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hia.left hia.right]


[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
h : Monotone f
x✝¹ : α
x✝ : x✝¹ ∈ Icc a b
⊢ f x✝¹ ∈ Icc (f a) (f b)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
h : StrictMono f
x✝¹ : α
x✝ : x✝¹ ∈ Ioo a b
⊢ f x✝¹ ∈ Ioo (f a) (f b)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : Monotone f
x✝¹ : α
x✝ : x✝¹ ∈ Ici a
⊢ f x✝¹ ∈ Ici (f a)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : Monotone f
x✝¹ : α
x✝ : x✝¹ ∈ Iic a
⊢ f x✝¹ ∈ Iic (f a)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : StrictMono f
x✝¹ : α
x✝ : x✝¹ ∈ Ioi a
⊢ f x✝¹ ∈ Ioi (f a)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : StrictMono f
x✝¹ : α
x✝ : x✝¹ ∈ Iio a
⊢ f x✝¹ ∈ Iio (f a)
[PROOFSTEP]
aesop


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
src✝¹ : AddMonoidWithOne (α × β) := instAddMonoidWithOne
src✝ : AddGroup (α × β) := instAddGroup
x✝ : ℕ
⊢ IntCast.intCast ↑x✝ = ↑x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
src✝¹ : AddMonoidWithOne (α × β) := instAddMonoidWithOne
src✝ : AddGroup (α × β) := instAddGroup
x✝ : ℕ
⊢ (↑x✝, ↑x✝) = ↑x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
src✝¹ : AddMonoidWithOne (α × β) := instAddMonoidWithOne
src✝ : AddGroup (α × β) := instAddGroup
x✝ : ℕ
⊢ IntCast.intCast (Int.negSucc x✝) = -↑(x✝ + 1)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
src✝¹ : AddMonoidWithOne (α × β) := instAddMonoidWithOne
src✝ : AddGroup (α × β) := instAddGroup
x✝ : ℕ
⊢ (-1 + -↑x✝, -1 + -↑x✝) = -1 + -↑x✝
[PROOFSTEP]
rfl


[GOAL]
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0 : m = 0
⊢ m ∣ n
[PROOFSTEP]
simp [m0] at ae
[GOAL]
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
m0 : m = 0
ae : n = 0
⊢ m ∣ n
[PROOFSTEP]
simp [ae, m0]
[GOAL]
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
⊢ m ∣ n
[PROOFSTEP]
cases' eq_ofNat_of_zero_le (@nonneg_of_mul_nonneg_right ℤ _ m a (by simp [ae.symm]) (by simpa using m0l)) with k e
[GOAL]
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
⊢ 0 ≤ ↑m * a
[PROOFSTEP]
simp [ae.symm]
[GOAL]
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
⊢ 0 < ↑m
[PROOFSTEP]
simpa using m0l
[GOAL]
case intro
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
k : ℕ
e : a = ↑k
⊢ m ∣ n
[PROOFSTEP]
subst a
[GOAL]
case intro
m n : ℕ
x✝ : ↑m ∣ ↑n
m0l : m > 0
k : ℕ
ae : ↑n = ↑m * ↑k
⊢ m ∣ n
[PROOFSTEP]
exact ⟨k, Int.ofNat.inj ae⟩
[GOAL]
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ ↑m * ↑k = ↑n
[PROOFSTEP]
rw [e, Int.ofNat_mul]
[GOAL]
n : ℕ
z : ℤ
⊢ ↑n ∣ z ↔ n ∣ natAbs z
[PROOFSTEP]
rcases natAbs_eq z with (eq | eq)
[GOAL]
case inl
n : ℕ
z : ℤ
eq : z = ↑(natAbs z)
⊢ ↑n ∣ z ↔ n ∣ natAbs z
[PROOFSTEP]
rw [eq]
[GOAL]
case inr
n : ℕ
z : ℤ
eq : z = -↑(natAbs z)
⊢ ↑n ∣ z ↔ n ∣ natAbs z
[PROOFSTEP]
rw [eq]
[GOAL]
case inl
n : ℕ
z : ℤ
eq : z = ↑(natAbs z)
⊢ ↑n ∣ ↑(natAbs z) ↔ n ∣ natAbs ↑(natAbs z)
[PROOFSTEP]
simp [← coe_nat_dvd]
[GOAL]
case inr
n : ℕ
z : ℤ
eq : z = -↑(natAbs z)
⊢ ↑n ∣ -↑(natAbs z) ↔ n ∣ natAbs (-↑(natAbs z))
[PROOFSTEP]
simp [← coe_nat_dvd]
[GOAL]
n : ℕ
z : ℤ
⊢ z ∣ ↑n ↔ natAbs z ∣ n
[PROOFSTEP]
rcases natAbs_eq z with (eq | eq)
[GOAL]
case inl
n : ℕ
z : ℤ
eq : z = ↑(natAbs z)
⊢ z ∣ ↑n ↔ natAbs z ∣ n
[PROOFSTEP]
rw [eq]
[GOAL]
case inr
n : ℕ
z : ℤ
eq : z = -↑(natAbs z)
⊢ z ∣ ↑n ↔ natAbs z ∣ n
[PROOFSTEP]
rw [eq]
[GOAL]
case inl
n : ℕ
z : ℤ
eq : z = ↑(natAbs z)
⊢ ↑(natAbs z) ∣ ↑n ↔ natAbs ↑(natAbs z) ∣ n
[PROOFSTEP]
simp [← coe_nat_dvd]
[GOAL]
case inr
n : ℕ
z : ℤ
eq : z = -↑(natAbs z)
⊢ -↑(natAbs z) ∣ ↑n ↔ natAbs (-↑(natAbs z)) ∣ n
[PROOFSTEP]
simp [← coe_nat_dvd]


[GOAL]
u : ℤˣ
⊢ natAbs ↑u * natAbs ↑u⁻¹ = 1
[PROOFSTEP]
rw [← natAbs_mul, Units.mul_inv]
[GOAL]
u : ℤˣ
⊢ natAbs 1 = 1
[PROOFSTEP]
rfl
[GOAL]
u : ℤˣ
⊢ natAbs ↑u⁻¹ * natAbs ↑u = 1
[PROOFSTEP]
rw [← natAbs_mul, Units.inv_mul]
[GOAL]
u : ℤˣ
⊢ natAbs 1 = 1
[PROOFSTEP]
rfl
[GOAL]
u : ℤˣ
⊢ u = 1 ∨ u = -1
[PROOFSTEP]
simpa only [Units.ext_iff, units_natAbs] using natAbs_eq u
[GOAL]
a : ℤ
⊢ IsUnit a ↔ a = 1 ∨ a = -1
[PROOFSTEP]
refine' ⟨fun h => isUnit_eq_one_or h, fun h => _⟩
[GOAL]
a : ℤ
h : a = 1 ∨ a = -1
⊢ IsUnit a
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case inl
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
[GOAL]
case inr
⊢ IsUnit (-1)
[PROOFSTEP]
exact isUnit_one.neg
[GOAL]
a b : ℤ
ha : IsUnit a
hb : IsUnit b
⊢ a = b ∨ a = -b
[PROOFSTEP]
rcases isUnit_eq_one_or hb with (rfl | rfl)
[GOAL]
case inl
a : ℤ
ha : IsUnit a
hb : IsUnit 1
⊢ a = 1 ∨ a = -1
[PROOFSTEP]
exact isUnit_eq_one_or ha
[GOAL]
case inr
a : ℤ
ha : IsUnit a
hb : IsUnit (-1)
⊢ a = -1 ∨ a = - -1
[PROOFSTEP]
rwa [or_comm, neg_neg, ← isUnit_iff]
[GOAL]
z w : ℤ
h : z * w = 1
⊢ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
[PROOFSTEP]
have h' : w * z = 1 := mul_comm z w ▸ h
[GOAL]
z w : ℤ
h : z * w = 1
h' : w * z = 1
⊢ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
[PROOFSTEP]
rcases eq_one_or_neg_one_of_mul_eq_one h with (rfl | rfl)
[GOAL]
case inl
w : ℤ
h : 1 * w = 1
h' : w * 1 = 1
⊢ 1 = 1 ∧ w = 1 ∨ 1 = -1 ∧ w = -1
[PROOFSTEP]
rcases eq_one_or_neg_one_of_mul_eq_one h' with (rfl | rfl)
[GOAL]
case inr
w : ℤ
h : -1 * w = 1
h' : w * -1 = 1
⊢ -1 = 1 ∧ w = 1 ∨ -1 = -1 ∧ w = -1
[PROOFSTEP]
rcases eq_one_or_neg_one_of_mul_eq_one h' with (rfl | rfl)
[GOAL]
case inl.inl
h h' : 1 * 1 = 1
⊢ 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1
[PROOFSTEP]
tauto
[GOAL]
case inl.inr
h : 1 * -1 = 1
h' : -1 * 1 = 1
⊢ 1 = 1 ∧ -1 = 1 ∨ 1 = -1 ∧ -1 = -1
[PROOFSTEP]
tauto
[GOAL]
case inr.inl
h : -1 * 1 = 1
h' : 1 * -1 = 1
⊢ -1 = 1 ∧ 1 = 1 ∨ -1 = -1 ∧ 1 = -1
[PROOFSTEP]
tauto
[GOAL]
case inr.inr
h h' : -1 * -1 = 1
⊢ -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
[PROOFSTEP]
tauto
[GOAL]
z w : ℤ
⊢ z * w = 1 ↔ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
[PROOFSTEP]
refine' ⟨eq_one_or_neg_one_of_mul_eq_one', fun h => Or.elim h (fun H => _) fun H => _⟩
[GOAL]
case refine'_1
z w : ℤ
h : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
H : z = 1 ∧ w = 1
⊢ z * w = 1
[PROOFSTEP]
rcases H with ⟨rfl, rfl⟩
[GOAL]
case refine'_2
z w : ℤ
h : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
H : z = -1 ∧ w = -1
⊢ z * w = 1
[PROOFSTEP]
rcases H with ⟨rfl, rfl⟩
[GOAL]
case refine'_1.intro
h : 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1
⊢ 1 * 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.intro
h : -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
⊢ -1 * -1 = 1
[PROOFSTEP]
rfl
[GOAL]
z w : ℤ
h : z * w = -1
⊢ z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
[PROOFSTEP]
rcases isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1 with (rfl | rfl)
[GOAL]
case inl
w : ℤ
h : 1 * w = -1
⊢ 1 = 1 ∧ w = -1 ∨ 1 = -1 ∧ w = 1
[PROOFSTEP]
exact Or.inl ⟨rfl, one_mul w ▸ h⟩
[GOAL]
case inr
w : ℤ
h : -1 * w = -1
⊢ -1 = 1 ∧ w = -1 ∨ -1 = -1 ∧ w = 1
[PROOFSTEP]
exact Or.inr ⟨rfl, neg_inj.mp (neg_one_mul w ▸ h)⟩
[GOAL]
z w : ℤ
⊢ z * w = -1 ↔ z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
[PROOFSTEP]
refine' ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h => Or.elim h (fun H => _) fun H => _⟩
[GOAL]
case refine'_1
z w : ℤ
h : z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
H : z = 1 ∧ w = -1
⊢ z * w = -1
[PROOFSTEP]
rcases H with ⟨rfl, rfl⟩
[GOAL]
case refine'_2
z w : ℤ
h : z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
H : z = -1 ∧ w = 1
⊢ z * w = -1
[PROOFSTEP]
rcases H with ⟨rfl, rfl⟩
[GOAL]
case refine'_1.intro
h : 1 = 1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = 1
⊢ 1 * -1 = -1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.intro
h : -1 = 1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = 1
⊢ -1 * 1 = -1
[PROOFSTEP]
rfl
[GOAL]
n : ℤ
⊢ IsUnit n ↔ natAbs n = 1
[PROOFSTEP]
simp [natAbs_eq_iff, isUnit_iff, Nat.cast_zero]
[GOAL]
n : ℕ
⊢ IsUnit ↑n ↔ IsUnit n
[PROOFSTEP]
simp [isUnit_iff_natAbs_eq]
[GOAL]
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
rw [isUnit_iff] at ha hb hc hd
[GOAL]
a b c d : ℤ
ha : a = 1 ∨ a = -1
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases ha
[GOAL]
case inl
a b c d : ℤ
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝ : a = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hb
[GOAL]
case inr
a b c d : ℤ
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝ : a = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hb
[GOAL]
case inl.inl
a b c d : ℤ
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝¹ : a = 1
h✝ : b = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hc
[GOAL]
case inl.inr
a b c d : ℤ
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝¹ : a = 1
h✝ : b = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hc
[GOAL]
case inr.inl
a b c d : ℤ
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝¹ : a = -1
h✝ : b = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hc
[GOAL]
case inr.inr
a b c d : ℤ
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
h✝¹ : a = -1
h✝ : b = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hc
[GOAL]
case inl.inl.inl
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = 1
h✝¹ : b = 1
h✝ : c = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inl.inl.inr
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = 1
h✝¹ : b = 1
h✝ : c = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inl.inr.inl
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = 1
h✝¹ : b = -1
h✝ : c = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inl.inr.inr
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = 1
h✝¹ : b = -1
h✝ : c = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inr.inl.inl
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = -1
h✝¹ : b = 1
h✝ : c = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inr.inl.inr
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = -1
h✝¹ : b = 1
h✝ : c = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inr.inr.inl
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = -1
h✝¹ : b = -1
h✝ : c = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inr.inr.inr
a b c d : ℤ
hd : d = 1 ∨ d = -1
h✝² : a = -1
h✝¹ : b = -1
h✝ : c = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
cases hd
[GOAL]
case inl.inl.inl.inl
a b c d : ℤ
h✝³ : a = 1
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inl.inl.inr
a b c d : ℤ
h✝³ : a = 1
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inl.inr.inl
a b c d : ℤ
h✝³ : a = 1
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inl.inr.inr
a b c d : ℤ
h✝³ : a = 1
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inr.inl.inl
a b c d : ℤ
h✝³ : a = 1
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inr.inl.inr
a b c d : ℤ
h✝³ : a = 1
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inr.inr.inl
a b c d : ℤ
h✝³ : a = 1
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inr.inr.inr
a b c d : ℤ
h✝³ : a = 1
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inl.inl.inl
a b c d : ℤ
h✝³ : a = -1
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inl.inl.inr
a b c d : ℤ
h✝³ : a = -1
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inl.inr.inl
a b c d : ℤ
h✝³ : a = -1
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inl.inr.inr
a b c d : ℤ
h✝³ : a = -1
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inr.inl.inl
a b c d : ℤ
h✝³ : a = -1
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inr.inl.inr
a b c d : ℤ
h✝³ : a = -1
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inr.inr.inl
a b c d : ℤ
h✝³ : a = -1
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = 1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inr.inr.inr.inr
a b c d : ℤ
h✝³ : a = -1
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
[PROOFSTEP]
subst a
[GOAL]
case inl.inl.inl.inl
b c d : ℤ
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = 1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inl.inl.inr
b c d : ℤ
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = -1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inl.inr.inl
b c d : ℤ
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = 1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inl.inr.inr
b c d : ℤ
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = -1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inr.inl.inl
b c d : ℤ
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = 1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inr.inl.inr
b c d : ℤ
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = -1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inr.inr.inl
b c d : ℤ
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = 1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inr.inr.inr
b c d : ℤ
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = -1
⊢ 1 + b = c + d ↔ 1 = c ∧ b = d ∨ 1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inl.inl.inl
b c d : ℤ
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = 1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inl.inl.inr
b c d : ℤ
h✝² : b = 1
h✝¹ : c = 1
h✝ : d = -1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inl.inr.inl
b c d : ℤ
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = 1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inl.inr.inr
b c d : ℤ
h✝² : b = 1
h✝¹ : c = -1
h✝ : d = -1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inr.inl.inl
b c d : ℤ
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = 1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inr.inl.inr
b c d : ℤ
h✝² : b = -1
h✝¹ : c = 1
h✝ : d = -1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inr.inr.inl
b c d : ℤ
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = 1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inr.inr.inr.inr
b c d : ℤ
h✝² : b = -1
h✝¹ : c = -1
h✝ : d = -1
⊢ -1 + b = c + d ↔ -1 = c ∧ b = d ∨ -1 = d ∧ b = c
[PROOFSTEP]
subst b
[GOAL]
case inl.inl.inl.inl
c d : ℤ
h✝¹ : c = 1
h✝ : d = 1
⊢ 1 + 1 = c + d ↔ 1 = c ∧ 1 = d ∨ 1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inl.inl.inr
c d : ℤ
h✝¹ : c = 1
h✝ : d = -1
⊢ 1 + 1 = c + d ↔ 1 = c ∧ 1 = d ∨ 1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inl.inr.inl
c d : ℤ
h✝¹ : c = -1
h✝ : d = 1
⊢ 1 + 1 = c + d ↔ 1 = c ∧ 1 = d ∨ 1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inl.inr.inr
c d : ℤ
h✝¹ : c = -1
h✝ : d = -1
⊢ 1 + 1 = c + d ↔ 1 = c ∧ 1 = d ∨ 1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inr.inl.inl
c d : ℤ
h✝¹ : c = 1
h✝ : d = 1
⊢ 1 + -1 = c + d ↔ 1 = c ∧ -1 = d ∨ 1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inr.inl.inr
c d : ℤ
h✝¹ : c = 1
h✝ : d = -1
⊢ 1 + -1 = c + d ↔ 1 = c ∧ -1 = d ∨ 1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inr.inr.inl
c d : ℤ
h✝¹ : c = -1
h✝ : d = 1
⊢ 1 + -1 = c + d ↔ 1 = c ∧ -1 = d ∨ 1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inr.inr.inr
c d : ℤ
h✝¹ : c = -1
h✝ : d = -1
⊢ 1 + -1 = c + d ↔ 1 = c ∧ -1 = d ∨ 1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inl.inl.inl
c d : ℤ
h✝¹ : c = 1
h✝ : d = 1
⊢ -1 + 1 = c + d ↔ -1 = c ∧ 1 = d ∨ -1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inl.inl.inr
c d : ℤ
h✝¹ : c = 1
h✝ : d = -1
⊢ -1 + 1 = c + d ↔ -1 = c ∧ 1 = d ∨ -1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inl.inr.inl
c d : ℤ
h✝¹ : c = -1
h✝ : d = 1
⊢ -1 + 1 = c + d ↔ -1 = c ∧ 1 = d ∨ -1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inl.inr.inr
c d : ℤ
h✝¹ : c = -1
h✝ : d = -1
⊢ -1 + 1 = c + d ↔ -1 = c ∧ 1 = d ∨ -1 = d ∧ 1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inr.inl.inl
c d : ℤ
h✝¹ : c = 1
h✝ : d = 1
⊢ -1 + -1 = c + d ↔ -1 = c ∧ -1 = d ∨ -1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inr.inl.inr
c d : ℤ
h✝¹ : c = 1
h✝ : d = -1
⊢ -1 + -1 = c + d ↔ -1 = c ∧ -1 = d ∨ -1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inr.inr.inl
c d : ℤ
h✝¹ : c = -1
h✝ : d = 1
⊢ -1 + -1 = c + d ↔ -1 = c ∧ -1 = d ∨ -1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inr.inr.inr.inr
c d : ℤ
h✝¹ : c = -1
h✝ : d = -1
⊢ -1 + -1 = c + d ↔ -1 = c ∧ -1 = d ∨ -1 = d ∧ -1 = c
[PROOFSTEP]
subst c
[GOAL]
case inl.inl.inl.inl
d : ℤ
h✝ : d = 1
⊢ 1 + 1 = 1 + d ↔ 1 = 1 ∧ 1 = d ∨ 1 = d ∧ 1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inl.inl.inl.inr
d : ℤ
h✝ : d = -1
⊢ 1 + 1 = 1 + d ↔ 1 = 1 ∧ 1 = d ∨ 1 = d ∧ 1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inl.inl.inr.inl
d : ℤ
h✝ : d = 1
⊢ 1 + 1 = -1 + d ↔ 1 = -1 ∧ 1 = d ∨ 1 = d ∧ 1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inl.inl.inr.inr
d : ℤ
h✝ : d = -1
⊢ 1 + 1 = -1 + d ↔ 1 = -1 ∧ 1 = d ∨ 1 = d ∧ 1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inl.inr.inl.inl
d : ℤ
h✝ : d = 1
⊢ 1 + -1 = 1 + d ↔ 1 = 1 ∧ -1 = d ∨ 1 = d ∧ -1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inl.inr.inl.inr
d : ℤ
h✝ : d = -1
⊢ 1 + -1 = 1 + d ↔ 1 = 1 ∧ -1 = d ∨ 1 = d ∧ -1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inl.inr.inr.inl
d : ℤ
h✝ : d = 1
⊢ 1 + -1 = -1 + d ↔ 1 = -1 ∧ -1 = d ∨ 1 = d ∧ -1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inl.inr.inr.inr
d : ℤ
h✝ : d = -1
⊢ 1 + -1 = -1 + d ↔ 1 = -1 ∧ -1 = d ∨ 1 = d ∧ -1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inr.inl.inl.inl
d : ℤ
h✝ : d = 1
⊢ -1 + 1 = 1 + d ↔ -1 = 1 ∧ 1 = d ∨ -1 = d ∧ 1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inr.inl.inl.inr
d : ℤ
h✝ : d = -1
⊢ -1 + 1 = 1 + d ↔ -1 = 1 ∧ 1 = d ∨ -1 = d ∧ 1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inr.inl.inr.inl
d : ℤ
h✝ : d = 1
⊢ -1 + 1 = -1 + d ↔ -1 = -1 ∧ 1 = d ∨ -1 = d ∧ 1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inr.inl.inr.inr
d : ℤ
h✝ : d = -1
⊢ -1 + 1 = -1 + d ↔ -1 = -1 ∧ 1 = d ∨ -1 = d ∧ 1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inr.inr.inl.inl
d : ℤ
h✝ : d = 1
⊢ -1 + -1 = 1 + d ↔ -1 = 1 ∧ -1 = d ∨ -1 = d ∧ -1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inr.inr.inl.inr
d : ℤ
h✝ : d = -1
⊢ -1 + -1 = 1 + d ↔ -1 = 1 ∧ -1 = d ∨ -1 = d ∧ -1 = 1
[PROOFSTEP]
subst d
[GOAL]
case inr.inr.inr.inl
d : ℤ
h✝ : d = 1
⊢ -1 + -1 = -1 + d ↔ -1 = -1 ∧ -1 = d ∨ -1 = d ∧ -1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inr.inr.inr.inr
d : ℤ
h✝ : d = -1
⊢ -1 + -1 = -1 + d ↔ -1 = -1 ∧ -1 = d ∨ -1 = d ∧ -1 = -1
[PROOFSTEP]
subst d
[GOAL]
case inl.inl.inl.inl
⊢ 1 + 1 = 1 + 1 ↔ 1 = 1 ∧ 1 = 1 ∨ 1 = 1 ∧ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inl.inr
⊢ 1 + 1 = 1 + -1 ↔ 1 = 1 ∧ 1 = -1 ∨ 1 = -1 ∧ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr.inl
⊢ 1 + 1 = -1 + 1 ↔ 1 = -1 ∧ 1 = 1 ∨ 1 = 1 ∧ 1 = -1
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr.inr
⊢ 1 + 1 = -1 + -1 ↔ 1 = -1 ∧ 1 = -1 ∨ 1 = -1 ∧ 1 = -1
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl.inl
⊢ 1 + -1 = 1 + 1 ↔ 1 = 1 ∧ -1 = 1 ∨ 1 = 1 ∧ -1 = 1
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl.inr
⊢ 1 + -1 = 1 + -1 ↔ 1 = 1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = 1
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr.inl
⊢ 1 + -1 = -1 + 1 ↔ 1 = -1 ∧ -1 = 1 ∨ 1 = 1 ∧ -1 = -1
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr.inr
⊢ 1 + -1 = -1 + -1 ↔ 1 = -1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = -1
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl.inl
⊢ -1 + 1 = 1 + 1 ↔ -1 = 1 ∧ 1 = 1 ∨ -1 = 1 ∧ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl.inr
⊢ -1 + 1 = 1 + -1 ↔ -1 = 1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr.inl
⊢ -1 + 1 = -1 + 1 ↔ -1 = -1 ∧ 1 = 1 ∨ -1 = 1 ∧ 1 = -1
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr.inr
⊢ -1 + 1 = -1 + -1 ↔ -1 = -1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = -1
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl.inl
⊢ -1 + -1 = 1 + 1 ↔ -1 = 1 ∧ -1 = 1 ∨ -1 = 1 ∧ -1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl.inr
⊢ -1 + -1 = 1 + -1 ↔ -1 = 1 ∧ -1 = -1 ∨ -1 = -1 ∧ -1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr.inl
⊢ -1 + -1 = -1 + 1 ↔ -1 = -1 ∧ -1 = 1 ∨ -1 = 1 ∧ -1 = -1
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr.inr
⊢ -1 + -1 = -1 + -1 ↔ -1 = -1 ∧ -1 = -1 ∨ -1 = -1 ∧ -1 = -1
[PROOFSTEP]
simp