[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : One α
s : Finset α
a : α
inst✝² : DecidableEq β
inst✝¹ : One β
inst✝ : OneHomClass F α β
f : F
⊢ image (↑f) 1 = 1
[PROOFSTEP]
rw [image_one, map_one, singleton_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s : Finset α
⊢ ↑(preimage s Inv.inv (_ : Set.InjOn Inv.inv (Inv.inv ⁻¹' ↑s))) = ↑s⁻¹
[PROOFSTEP]
rw [coe_preimage, Set.inv_preimage, coe_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
⊢ ↑(s ^ n) = ↑s ^ n
[PROOFSTEP]
change ↑(npowRec n s) = (s : Set α) ^ n
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
⊢ ↑(npowRec n s) = ↑s ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n : ℕ
s : Finset α
⊢ ↑(npowRec Nat.zero s) = ↑s ^ Nat.zero
[PROOFSTEP]
rw [npowRec, pow_zero, coe_one]
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec (Nat.succ n) s) = ↑s ^ Nat.succ n
[PROOFSTEP]
rw [npowRec, pow_succ, coe_mul, ih]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
ha : a ∈ s
n : ℕ
⊢ a * a ^ n ∈ s ^ (n + 1)
[PROOFSTEP]
exact mul_mem_mul ha (pow_mem_pow ha n)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hst : s ⊆ t
⊢ s ^ 0 ⊆ t ^ 0
[PROOFSTEP]
simp [pow_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s * s ^ n ⊆ t ^ (n + 1)
[PROOFSTEP]
exact mul_subset_mul hst (pow_subset_pow hst n)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ m ≤ n → s ^ m ⊆ s ^ n
[PROOFSTEP]
apply Nat.le_induction
[GOAL]
case base
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ s ^ m ⊆ s ^ m
[PROOFSTEP]
exact fun _ hn => hn
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ ∀ (n : ℕ), m ≤ n → s ^ m ⊆ s ^ n → s ^ m ⊆ s ^ (n + 1)
[PROOFSTEP]
intro n _ hmn
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hs : 1 ∈ s
n : ℕ
hn✝ : m ≤ n
hmn : 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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hs : 1 ∈ s
n : ℕ
hn✝ : m ≤ n
hmn : s ^ m ⊆ s ^ n
⊢ s ^ m ⊆ s * s ^ n
[PROOFSTEP]
exact hmn.trans (subset_mul_right (s ^ n) hs)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a✝ : α
m n : ℕ
a : α
s : Fin n → Finset α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a✝ : α
m n : ℕ
a : α
s : Fin n → Finset α
⊢ (∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
simp [← mem_coe, coe_pow, Set.mem_pow]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m 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✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Monoid α
s t : Finset α
a : α
m n : ℕ
inst✝ : Fintype α
hn : n ≠ 0
⊢ ↑(univ ^ n) = ↑univ
[PROOFSTEP]
rw [coe_pow, coe_univ, Set.univ_pow hn]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s✝ t s : Finset α
n : ℕ
⊢ ↑(s ^ Int.negSucc n) = ↑s ^ Int.negSucc n
[PROOFSTEP]
refine' (coe_inv _).trans _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s✝ t s : Finset α
n : ℕ
⊢ (↑(npowRec (Nat.succ n) s))⁻¹ = ↑s ^ Int.negSucc n
[PROOFSTEP]
exact congr_arg Inv.inv (coe_pow _ _)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
[PROOFSTEP]
simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ 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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ 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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
[PROOFSTEP]
obtain ⟨a, b, ha, hb, h⟩ := Finset.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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ (∃ 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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
a : α
ha : IsUnit a
⊢ IsUnit {a}
[PROOFSTEP]
exact ha.finset
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ IsUnit ↑s ↔ IsUnit s
[PROOFSTEP]
simp_rw [isUnit_iff, Set.isUnit_iff, coe_eq_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : MulZeroClass α
s✝ t s : Finset α
⊢ s * 0 ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : MulZeroClass α
s✝ t s : Finset α
⊢ 0 * s ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : MulZeroClass α
s t : Finset α
hs : Finset.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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : MulZeroClass α
s t : Finset α
hs : Finset.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✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ 1 ∈ s / t ↔ ¬Disjoint s t
[PROOFSTEP]
rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
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✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ (∃ a, s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a}
[PROOFSTEP]
simp only [Group.isUnit, and_true_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ ↑(image (fun b => a * b) t) =
    ↑(preimage t (fun b => a⁻¹ * b) (_ : Set.InjOn ((fun x x_1 => x * x_1) a⁻¹) ((fun b => a⁻¹ * b) ⁻¹' ↑t)))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ ↑(image (fun x => x * b) t) =
    ↑(preimage t (fun x => x * b⁻¹) (_ : Set.InjOn (fun x => x * b⁻¹) ((fun x => x * b⁻¹) ⁻¹' ↑t)))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ image (fun b => a⁻¹ * b) t =
    preimage t (fun b => a * b) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun b => a * b) ⁻¹' ↑t))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ image (fun x => x * b⁻¹) t = preimage t (fun x => x * b) (_ : Set.InjOn (fun x => x * b) ((fun x => x * b) ⁻¹' ↑t))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s✝ t s : Finset α
⊢ s / 0 ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_div]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s✝ t s : Finset α
⊢ 0 / s ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_div]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s t : Finset α
hs : Finset.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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s t : Finset α
hs : Finset.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✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} ((fun x x_1 => x * x_1) a)
      (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' ↑{b})) =
    {a⁻¹ * b}
[PROOFSTEP]
classical rw [← image_mul_left', image_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} ((fun x x_1 => x * x_1) a)
      (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((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 : Finset α
a b : α
⊢ preimage {b} (fun x => x * a) (_ : Set.InjOn (fun x => x * a) ((fun x => x * a) ⁻¹' ↑{b})) = {b * a⁻¹}
[PROOFSTEP]
classical rw [← image_mul_right', image_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} (fun x => x * a) (_ : Set.InjOn (fun x => x * a) ((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 : Finset α
a b : α
⊢ preimage 1 ((fun x x_1 => x * x_1) a) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' ↑1)) =
    {a⁻¹}
[PROOFSTEP]
classical 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 : Finset α
a b : α
⊢ preimage 1 ((fun x x_1 => x * x_1) a) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((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 : Finset α
a b : α
⊢ preimage 1 (fun x => x * b) (_ : Set.InjOn (fun x => x * b) ((fun x => x * b) ⁻¹' ↑1)) = {b⁻¹}
[PROOFSTEP]
classical 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 : Finset α
a b : α
⊢ preimage 1 (fun x => x * b) (_ : Set.InjOn (fun x => x * 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 : Finset α
a b : α
⊢ preimage 1 ((fun x x_1 => x * x_1) a⁻¹)
      (_ : Set.InjOn ((fun x x_1 => x * x_1) a⁻¹) ((fun x x_1 => x * x_1) a⁻¹ ⁻¹' ↑1)) =
    {a}
[PROOFSTEP]
rw [preimage_mul_left_one, inv_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage 1 (fun x => x * b⁻¹) (_ : Set.InjOn (fun x => x * b⁻¹) ((fun x => x * b⁻¹) ⁻¹' ↑1)) = {b}
[PROOFSTEP]
rw [preimage_mul_right_one, inv_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : DecidableEq β
inst✝ : SMul α β
s s₁ s₂ t u : Finset β
a : α
b x : β
⊢ x ∈ a • s ↔ ∃ y, y ∈ s ∧ a • y = x
[PROOFSTEP]
simp only [Finset.smul_finset_def, and_assoc, mem_image, exists_prop, Prod.exists, mem_product]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq γ
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : SMulCommClass α β γ
a : α
s : Finset β
t : Finset γ
⊢ ↑(a • s • t) = ↑(s • a • t)
[PROOFSTEP]
simp only [coe_smul_finset, coe_smul, smul_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq γ
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : SMulCommClass α β γ
s : Finset α
t : Finset β
u : Finset γ
⊢ ↑(s • t • u) = ↑(t • s • u)
[PROOFSTEP]
simp_rw [coe_smul, smul_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
s : Finset γ
⊢ (a • b) • s = a • b • s
[PROOFSTEP]
simp only [← image_smul, image_image, smul_assoc, Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
s : Finset β
t : Finset γ
⊢ ↑((a • s) • t) = ↑(a • s • t)
[PROOFSTEP]
simp only [coe_smul_finset, coe_smul, smul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : Finset α
s : Finset β
t : Finset γ
⊢ ↑((a • s) • t) = ↑(a • s • t)
[PROOFSTEP]
simp only [coe_smul_finset, coe_smul, smul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : DecidableEq β
inst✝² : SMul α β
inst✝¹ : SMul αᵐᵒᵖ β
inst✝ : IsCentralScalar α β
a : α
s : Finset β
⊢ ↑(op a • s) = ↑(a • s)
[PROOFSTEP]
simp only [coe_smul_finset, coe_smul, op_smul_eq_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : DecidableEq β
inst✝² : DecidableEq α
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Finset β
⊢ image (fun b => 1 • b) s = s
[PROOFSTEP]
simp_rw [one_smul, image_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
⊢ ∀ {c : Finset α} {x : Finset β}, c • x = 0 → c = 0 ∨ x = 0
[PROOFSTEP]
intro s t h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
⊢ s = 0 ∨ t = 0
[PROOFSTEP]
by_contra H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
H : ¬(s = 0 ∨ t = 0)
⊢ False
[PROOFSTEP]
have hst : (s • t).Nonempty := h.symm.subst zero_nonempty
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
H : ¬(s = 0 ∨ t = 0)
hst : Finset.Nonempty (s • t)
⊢ False
[PROOFSTEP]
rw [← hst.of_smul_left.subset_zero_iff, ← hst.of_smul_right.subset_zero_iff] at H 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
H : ¬(s ⊆ 0 ∨ t ⊆ 0)
hst : Finset.Nonempty (s • t)
⊢ False
[PROOFSTEP]
push_neg at H 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
hst : Finset.Nonempty (s • t)
H : ¬s ⊆ 0 ∧ ¬t ⊆ 0
⊢ False
[PROOFSTEP]
simp_rw [not_subset, mem_zero] at H 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
hst : Finset.Nonempty (s • t)
H : (∃ x, x ∈ s ∧ ¬x = 0) ∧ ∃ x, x ∈ t ∧ ¬x = 0
⊢ False
[PROOFSTEP]
obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
[GOAL]
case intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
hst : Finset.Nonempty (s • t)
a : α
hs : a ∈ s
ha : ¬a = 0
b : β
ht : b ∈ t
hb : ¬b = 0
⊢ False
[PROOFSTEP]
exact (eq_zero_or_eq_zero_of_smul_eq_zero <| mem_zero.1 <| subset_of_eq h <| smul_mem_smul hs ht).elim ha hb
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
a✝ : γ
⊢ a✝ ∈ (op a • s) • t ↔ a✝ ∈ s • a • t
[PROOFSTEP]
simp [mem_smul, mem_smul_finset, h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LeftCancelSemigroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Set α
t : Finset α
⊢ (Set.PairwiseDisjoint s fun x => x • t) ↔ Set.InjOn (fun p => p.fst * p.snd) (s ×ˢ ↑t)
[PROOFSTEP]
simp_rw [← pairwiseDisjoint_coe, coe_smul_finset, Set.pairwiseDisjoint_smul_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ a⁻¹ • b ∈ s ↔ b ∈ a • s
[PROOFSTEP]
rw [← smul_mem_smul_finset_iff a, smul_inv_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ b ∈ a⁻¹ • s ↔ a • b ∈ s
[PROOFSTEP]
rw [← smul_mem_smul_finset_iff a, smul_inv_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ a • s ⊆ t ↔ s ⊆ a⁻¹ • t
[PROOFSTEP]
simp_rw [← coe_subset]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ ↑(a • s) ⊆ ↑t ↔ ↑s ⊆ ↑(a⁻¹ • t)
[PROOFSTEP]
push_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ a • ↑s ⊆ ↑t ↔ ↑s ⊆ a⁻¹ • ↑t
[PROOFSTEP]
exact Set.set_smul_subset_iff
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ s ⊆ a • t ↔ a⁻¹ • s ⊆ t
[PROOFSTEP]
simp_rw [← coe_subset]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ ↑s ⊆ ↑(a • t) ↔ ↑(a⁻¹ • s) ⊆ ↑t
[PROOFSTEP]
push_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ ↑s ⊆ a • ↑t ↔ a⁻¹ • ↑s ⊆ ↑t
[PROOFSTEP]
exact Set.subset_set_smul_iff
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(s • univ) = ↑univ
[PROOFSTEP]
push_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : Finset.Nonempty s
⊢ ↑s • Set.univ = Set.univ
[PROOFSTEP]
exact Set.smul_univ hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬s ⊆ 0
⊢ ↑(s • univ) = ↑univ
[PROOFSTEP]
rw [← coe_subset] at hs 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ ↑0
⊢ ↑(s • univ) = ↑univ
[PROOFSTEP]
push_cast at hs ⊢
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ 0
⊢ ↑s • Set.univ = Set.univ
[PROOFSTEP]
exact Set.smul_univ₀ hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s t : Finset β
a : α
b : β
inst✝ : Fintype β
ha : a ≠ 0
⊢ ↑(a • univ) = ↑univ
[PROOFSTEP]
push_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s t : Finset β
a : α
b : β
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • Set.univ = Set.univ
[PROOFSTEP]
exact Set.smul_set_univ₀ ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s✝ : Finset α
t : Finset β
s : Finset α
⊢ s • 0 ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s : Finset α
t✝ t : Finset β
⊢ 0 • t ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
hs : Finset.Nonempty s
⊢ 0 ⊆ s • 0
[PROOFSTEP]
simpa [mem_smul] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
ht : Finset.Nonempty t
⊢ 0 ⊆ 0 • t
[PROOFSTEP]
simpa [mem_smul] using ht
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s✝ : Finset α
t s : Finset β
h : Finset.Nonempty s
⊢ ↑(0 • s) = ↑0
[PROOFSTEP]
simpa using @Set.zero_smul_set α _ _ _ _ _ h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
inst✝ : NoZeroSMulDivisors α β
a : α
⊢ 0 ∈ s • t ↔ 0 ∈ s ∧ Finset.Nonempty t ∨ 0 ∈ t ∧ Finset.Nonempty s
[PROOFSTEP]
rw [← mem_coe, coe_smul, Set.zero_mem_smul_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
inst✝ : NoZeroSMulDivisors α β
a : α
⊢ 0 ∈ ↑s ∧ Set.Nonempty ↑t ∨ 0 ∈ ↑t ∧ Set.Nonempty ↑s ↔ 0 ∈ s ∧ Finset.Nonempty t ∨ 0 ∈ t ∧ Finset.Nonempty s
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t
[PROOFSTEP]
rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff ha, mem_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
inst✝² : AddGroup β
inst✝¹ : DistribMulAction α β
inst✝ : DecidableEq β
a : α
s : Finset α
t : Finset β
⊢ a • -t = -(a • t)
[PROOFSTEP]
simp only [← image_smul, ← image_neg, Function.comp, image_image, smul_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
inst✝² : AddGroup β
inst✝¹ : DistribMulAction α β
inst✝ : DecidableEq β
a : α
s : Finset α
t : Finset β
⊢ s • -t = -(s • t)
[PROOFSTEP]
simp_rw [← image_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
inst✝² : AddGroup β
inst✝¹ : DistribMulAction α β
inst✝ : DecidableEq β
a : α
s : Finset α
t : Finset β
⊢ s • image (fun x => -x) t = image (fun x => -x) (s • t)
[PROOFSTEP]
exact image_image₂_right_comm smul_neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Ring α
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
a : α
⊢ -a • t = -(a • t)
[PROOFSTEP]
simp only [← image_smul, ← image_neg, image_image, neg_smul, Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Ring α
inst✝³ : AddCommGroup β
inst✝² : Module α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
a : α
inst✝ : DecidableEq α
⊢ -s • t = -(s • t)
[PROOFSTEP]
simp_rw [← image_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Ring α
inst✝³ : AddCommGroup β
inst✝² : Module α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
a : α
inst✝ : DecidableEq α
⊢ image (fun x => -x) s • t = image (fun x => -x) (s • t)
[PROOFSTEP]
exact image₂_image_left_comm neg_smul
