F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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
rw [← nonempty_iff_ne_empty]
case mp
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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

case mpr
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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)
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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
constructor
case mp.intro.intro
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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
case mp
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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
rintro ⟨a, h, ha⟩
case mp.intro.intro.intro.intro
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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
case mp.intro.intro
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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
obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
no goals
case mp.intro.intro.intro.intro
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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
exact ⟨x • b, b, ⟨ha, hb⟩, by simp⟩
no goals
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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
simp
case mpr.intro.intro.intro.intro
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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)
case mpr
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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)
rintro ⟨a, b, ⟨ha, hb⟩, rfl⟩
no goals
case mpr.intro.intro.intro.intro
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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)
exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩
no goals
F : Type ?u.137905
α : Type u_1
β : Type ?u.137911
γ : Type ?u.137914
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
simp