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

case mpr
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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)
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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
constructor
case mp.intro.intro
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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
case mp
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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
rintro ⟨a, h, ha⟩
case mp.intro.intro.intro.intro
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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
case mp.intro.intro
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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
obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
no goals
case mp.intro.intro.intro.intro
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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
exact ⟨b, x • b, ⟨hb, ha⟩, by simp⟩
no goals
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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
simp
case mpr.intro.intro.intro.intro
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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)
case mpr
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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)
rintro ⟨a, b, ⟨ha, hb⟩, H⟩
case mpr.intro.intro.intro.intro
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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)
case mpr.intro.intro.intro.intro
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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)
have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H
no goals
case mpr.intro.intro.intro.intro
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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)
exact ⟨b, mem_inter (mem_smul_set.mpr ⟨a, ha, by simp [← this]⟩) hb⟩
no goals
F : Type ?u.145512
α : Type u_1
β : Type ?u.145518
γ : Type ?u.145521
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
simp [← this]