[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Mul α
s t u : Set α
a : α
⊢ op '' s • t = t * s
[PROOFSTEP]
rw [← image2_smul, ← image2_mul, image2_image_left, image2_swap]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Mul α
s t u : Set α
a : α
⊢ image2 (fun a b => SMul.smul (op b) a) t s = image2 (fun x x_1 => x * x_1) t s
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b✝ : β
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
T : Set γ
⊢ (a • b) • T = a • b • T
[PROOFSTEP]
simp only [← image_smul, image_image, smul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Set β
⊢ (fun x => 1 • x) '' s = s
[PROOFSTEP]
simp_rw [one_smul, image_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝¹ : Monoid α
inst✝ : MulAction α β
⊢ ∀ (b : Set β), 1 • b = b
[PROOFSTEP]
intros
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝¹ : Monoid α
inst✝ : MulAction α β
b✝ : Set β
⊢ 1 • b✝ = b✝
[PROOFSTEP]
simp only [← image_smul, one_smul, image_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝¹ : Monoid α
inst✝ : MulAction α β
⊢ ∀ (x y : α) (b : Set β), (x * y) • b = x • y • b
[PROOFSTEP]
intros
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝¹ : Monoid α
inst✝ : MulAction α β
x✝ y✝ : α
b✝ : Set β
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝
[PROOFSTEP]
simp only [← image_smul, image_image, ← mul_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝² : Monoid α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
x✝ : α
⊢ {x✝ • 0} = 0
[PROOFSTEP]
rw [smul_zero, singleton_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ {x✝ • 1} = 1
[PROOFSTEP]
rw [smul_one, singleton_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
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
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
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
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
h : s • t = 0
H : s ≠ 0 ∧ t ≠ 0
hst : Set.Nonempty (s • t)
⊢ False
[PROOFSTEP]
rw [Ne.def, ← hst.of_smul_left.subset_zero_iff, Ne.def, ← hst.of_smul_right.subset_zero_iff] at H 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
h : s • t = 0
H : ¬s ⊆ 0 ∧ ¬t ⊆ 0
hst : Set.Nonempty (s • t)
⊢ False
[PROOFSTEP]
simp only [not_subset, mem_zero] at H 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
h : s • t = 0
hst : Set.Nonempty (s • t)
H : (∃ a, a ∈ s ∧ ¬a = 0) ∧ ∃ a, a ∈ t ∧ ¬a = 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
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a✝ : α
b✝ : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Set α
t : Set β
h : s • t = 0
hst : Set.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 <| h.subset <| smul_mem_smul hs ht).elim ha hb
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
a : α
s : Set β
h : a • s = 0
⊢ a = 0 ∨ s = 0
[PROOFSTEP]
by_contra' H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
a : α
s : Set β
h : a • s = 0
H : a ≠ 0 ∧ s ≠ 0
⊢ False
[PROOFSTEP]
have hst : (a • s).Nonempty := h.symm.subst zero_nonempty
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
a : α
s : Set β
h : a • s = 0
H : a ≠ 0 ∧ s ≠ 0
hst : Set.Nonempty (a • s)
⊢ False
[PROOFSTEP]
rw [Ne.def, Ne.def, ← hst.of_image.subset_zero_iff, not_subset] at H 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
a : α
s : Set β
h : a • s = 0
H : ¬a = 0 ∧ ∃ a, a ∈ s ∧ ¬a ∈ 0
hst : Set.Nonempty (a • s)
⊢ False
[PROOFSTEP]
obtain ⟨ha, b, ht, hb⟩ := H
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b✝ : β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
a : α
s : Set β
h : a • s = 0
hst : Set.Nonempty (a • s)
ha : ¬a = 0
b : β
ht : b ∈ s
hb : ¬b ∈ 0
⊢ False
[PROOFSTEP]
exact (eq_zero_or_eq_zero_of_smul_eq_zero <| h.subset <| smul_mem_smul_set ht).elim ha hb
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
x✝ : γ
⊢ x✝ ∈ (op a • s) • t ↔ x✝ ∈ s • a • t
[PROOFSTEP]
simp [mem_smul, mem_smul_set, h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s✝ : Set α
t : Set β
s : Set α
⊢ s • 0 ⊆ 0
[PROOFSTEP]
simp [subset_def, mem_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s : Set α
t✝ t : Set β
⊢ 0 • t ⊆ 0
[PROOFSTEP]
simp [subset_def, mem_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s : Set α
t : Set β
hs : Set.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 α β
s : Set α
t : Set β
ht : Set.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 α β
s✝ : Set α
t s : Set β
h : Set.Nonempty s
⊢ 0 • s = 0
[PROOFSTEP]
simp only [← image_smul, image_eta, zero_smul, h.image_const, singleton_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
⊢ 0 ∈ s • t ↔ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
⊢ 0 ∈ s • t → 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
[PROOFSTEP]
rintro ⟨a, b, ha, hb, h⟩
[GOAL]
case mp.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a✝ a : α
b : β
ha : a ∈ s
hb : b ∈ t
h : (fun x x_1 => x • x_1) a b = 0
⊢ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
[PROOFSTEP]
obtain rfl | rfl := eq_zero_or_eq_zero_of_smul_eq_zero h
[GOAL]
case mp.intro.intro.intro.intro.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
b : β
hb : b ∈ t
ha : 0 ∈ s
h : (fun x x_1 => x • x_1) 0 b = 0
⊢ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
[PROOFSTEP]
exact Or.inl ⟨ha, b, hb⟩
[GOAL]
case mp.intro.intro.intro.intro.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a✝ a : α
ha : a ∈ s
hb : 0 ∈ t
h : (fun x x_1 => x • x_1) a 0 = 0
⊢ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
[PROOFSTEP]
exact Or.inr ⟨hb, a, ha⟩
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
⊢ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s → 0 ∈ s • t
[PROOFSTEP]
rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
[GOAL]
case mpr.inl.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
hs : 0 ∈ s
b : β
hb : b ∈ t
⊢ 0 ∈ s • t
[PROOFSTEP]
exact ⟨0, b, hs, hb, zero_smul _ _⟩
[GOAL]
case mpr.inr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a✝ : α
ht : 0 ∈ t
a : α
ha : a ∈ s
⊢ 0 ∈ s • t
[PROOFSTEP]
exact ⟨a, 0, ha, ht, smul_zero _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t
[PROOFSTEP]
refine' ⟨_, zero_mem_smul_set⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
⊢ 0 ∈ a • t → 0 ∈ t
[PROOFSTEP]
rintro ⟨b, hb, h⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
s : Set α
t : Set β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
b : β
hb : b ∈ t
h : (fun x => a • x) b = 0
⊢ 0 ∈ t
[PROOFSTEP]
rwa [(eq_zero_or_eq_zero_of_smul_eq_zero h).resolve_left ha] at hb 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s t A B : Set β
a : α
x : β
⊢ x ∈ a⁻¹ • A ↔ a • x ∈ A
[PROOFSTEP]
simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
[PROOFSTEP]
rw [← nonempty_iff_ne_empty]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ Set.Nonempty (x • s ∩ t) ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ Set.Nonempty (x • s ∩ t) → ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
[PROOFSTEP]
rintro ⟨a, h, ha⟩
[GOAL]
case mp.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x✝ : β
s t : Set α
x a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
[GOAL]
case mp.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
[PROOFSTEP]
exact ⟨x • b, b, ⟨ha, hb⟩, by simp⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ x • b * b⁻¹ = x
[PROOFSTEP]
simp
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → Set.Nonempty (x • s ∩ t)
[PROOFSTEP]
rintro ⟨a, b, ⟨ha, hb⟩, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x : β
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ Set.Nonempty ((a * b⁻¹) • s ∩ t)
[PROOFSTEP]
exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x : β
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ (a * b⁻¹) • b = a
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x
[PROOFSTEP]
simp_rw [smul_inter_ne_empty_iff, div_eq_mul_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
⊢ x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
[PROOFSTEP]
rw [← nonempty_iff_ne_empty]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
⊢ Set.Nonempty (x • s ∩ t) ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
⊢ Set.Nonempty (x • s ∩ t) → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
[PROOFSTEP]
rintro ⟨a, h, ha⟩
[GOAL]
case mp.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
[GOAL]
case mp.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
[PROOFSTEP]
exact ⟨b, x • b, ⟨hb, ha⟩, by simp⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ b⁻¹ * x • b = unop x
[PROOFSTEP]
simp
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → Set.Nonempty (x • s ∩ t)
[PROOFSTEP]
rintro ⟨a, b, ⟨ha, hb⟩, H⟩
[GOAL]
case mpr.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
⊢ Set.Nonempty (x • s ∩ t)
[PROOFSTEP]
have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H
[GOAL]
case mpr.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
this : op (a⁻¹ * b) = x
⊢ Set.Nonempty (x • s ∩ t)
[PROOFSTEP]
exact ⟨b, mem_inter (mem_smul_set.mpr ⟨a, ha, by simp [← this]⟩) hb⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a✝ : α
x✝ : β
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
this : op (a⁻¹ * b) = x
⊢ x • a = b
[PROOFSTEP]
simp [← this]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t A B : Set β
a : α
x : β
s : Set β
⊢ ⋃ (g : α), g • s = {a | ∃ g, g • a ∈ s}
[PROOFSTEP]
simp_rw [← iUnion_setOf, ← iUnion_inv_smul, ← preimage_smul, preimage]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
a : α
s : Set α
t : Set β
⊢ a • -t = -(a • t)
[PROOFSTEP]
simp_rw [← image_smul, ← image_neg, image_image, smul_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
a : α
s : Set α
t : Set β
⊢ 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 α β
a : α
s : Set α
t : Set β
⊢ s • Neg.neg '' t = Neg.neg '' (s • t)
[PROOFSTEP]
exact image_image2_right_comm smul_neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
⊢ (a + b) • s ⊆ a • s + b • s
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
x : β
hx : x ∈ s
⊢ (fun x => (a + b) • x) x ∈ a • s + b • s
[PROOFSTEP]
simpa only [add_smul] using add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hx)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
s : Set α
t : Set β
⊢ -a • t = -(a • t)
[PROOFSTEP]
simp_rw [← image_smul, ← image_neg, image_image, neg_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
s : Set α
t : Set β
⊢ -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 α β
a : α
s : Set α
t : Set β
⊢ Neg.neg '' s • t = Neg.neg '' (s • t)
[PROOFSTEP]
exact image2_image_left_comm neg_smul
