[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
