-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem op_smul_inter_ne_empty_iff {s t : Set α} {x : αᵐᵒᵖ} :
    x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x

Proof state:
case mp.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
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

Tactic:
exact ⟨b, x • b, ⟨hb, ha⟩, by simp⟩

Result:
no goals

Proof state:
case mp.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Tactic:
obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h

Result:
case mp.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
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

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Tactic:
rw [← nonempty_iff_ne_empty]

Result:
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Proof state:
α : Type u_2
inst✝ : Group α
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

Tactic:
simp [← this]

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
⊢ (x • s ∩ t).Nonempty

Tactic:
have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H

Result:
case mpr.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
this : op (a⁻¹ * b) = x
⊢ (x • s ∩ t).Nonempty

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty

Proof state:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Tactic:
rintro ⟨a, h, ha⟩

Result:
case mp.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
this : op (a⁻¹ * b) = x
⊢ (x • s ∩ t).Nonempty

Tactic:
exact ⟨b, mem_inter (mem_smul_set.mpr ⟨a, ha, by simp [← this]⟩) hb⟩

Result:
no goals

Proof state:
case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty

Tactic:
rintro ⟨a, b, ⟨ha, hb⟩, H⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
⊢ (x • s ∩ t).Nonempty

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ b⁻¹ * x • b = unop x

Tactic:
simp

Result:
no goals