awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
a : α
b : β
T : Set γ
⊢ (a • b) • T = a • b • T

Tactic:
simp only [← image_smul, image_image, smul_assoc]

Premises used: Set.image_image, Set.image_smul, smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
⊢ IsScalarTower.{u_2, u_3, u_4} α (Set β) (Set γ)

Tactic:
⟨fun _ _ _ ↦ image2_image_left_comm <| smul_assoc _⟩

Premises used: smul_assoc, Set.image2_image_left_comm, IsScalarTower.mk
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul α β
inst_1 : SMul.{u_2, u_3} αᵐᵒᵖ β
inst_2 : IsCentralScalar α β
⊢ IsCentralScalar.{u_2, u_3} α (Set β)

Tactic:
⟨fun _ S ↦ (congr_arg fun f ↦ f '' S) <| funext fun _ ↦ op_smul_eq_smul _ _⟩

Premises used: congr_arg, funext, IsCentralScalar.mk, Set.image, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
inst_1 : MulAction α β
s : Set β
simp_rw : (fun (a : β) ↦ a) '' s = s
⊢ (fun (x2 : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 1 x2) '' s = s

Tactic:
simp_rw [one_smul, image_id']

Premises used: Set.image_id', one_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
inst_1 : MulAction α β
x x_1 : α
x_2 : Set β
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
simp only [← image_smul, image_image, ← mul_smul]

Premises used: Set.image_image, Set.image_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
inst_1 : MulAction α β
x : Set β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 1 x = x

Tactic:
simp only [← image_smul, one_smul, image_id']

Premises used: Set.image_smul, Set.image_id', one_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
a : α
x : β
⊢ a • x ∈ a • s ↔ x ∈ s

Tactic:
(MulAction.injective _).mem_set_image

Premises used: Set.Mem, MulAction.injective, Function.Injective.mem_set_image
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A : Set β
a : α
x : β
⊢ x ∈ a • A ↔ a⁻¹ • x ∈ A

Tactic:
show x ∈ MulAction.toPerm a '' A ↔ _ from mem_image_equiv

Premises used: Set.Mem, Set.mem_image_equiv
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A : Set β
a : α
x : β
⊢ x ∈ a⁻¹ • A ↔ a • x ∈ A

Tactic:
simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]

Premises used: Set.image_smul, inv_smul_eq_iff, Set.mem_image, exists_eq_right
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
a b : α
s : Set α
⊢ a ∈ b • s⁻¹ ↔ b ∈ a • s

Tactic:
simp [mem_smul_set_iff_inv_smul_mem]

Premises used: Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
a : α
t : Set β
⊢ (fun (x : β) ↦ a • x) ⁻¹' t = a⁻¹ • t

Tactic:
((MulAction.toPerm a).image_symm_eq_preimage _).symm

Premises used: MulAction.toPerm, Eq.symm, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
a : α
t : Set β
⊢ (fun (x : β) ↦ a⁻¹ • x) ⁻¹' t = a • t

Tactic:
preimage_smul (toUnits a)⁻¹ t

Premises used: Set.preimage_smul, Inv.inv, toUnits, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ a • A ⊆ a • B ↔ A ⊆ B

Tactic:
image_subset_image_iff <| MulAction.injective _

Premises used: Set.image_subset_image_iff, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ a • A ⊆ B ↔ A ⊆ a⁻¹ • B

Tactic:
image_subset_iff.trans ?_

Premises used: Iff.trans, Set.image_subset_iff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
refine : A ⊆ (fun (x : β) ↦ a • x) ⁻¹' B ↔ A ⊆ a⁻¹ • B
⊢ a • A ⊆ B ↔ A ⊆ a⁻¹ • B

Tactic:
refine image_subset_iff.trans ?_

Premises used: Iff.trans, Set.image_subset_iff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
a₁ : (fun (x : β) ↦ a • x) ⁻¹' B = a⁻¹ • B
⊢ A ⊆ (fun (x : β) ↦ a • x) ⁻¹' B ↔ A ⊆ a⁻¹ • B

Tactic:
congr! 1
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ (fun (x : β) ↦ a • x) ⁻¹' B = a⁻¹ • B

Tactic:
((MulAction.toPerm _).image_symm_eq_preimage _).symm

Premises used: MulAction.toPerm, Eq.symm, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ (fun (x : β) ↦ a • x) ⁻¹' B = a⁻¹ • B

Tactic:
exact ((MulAction.toPerm _).image_symm_eq_preimage _).symm

Premises used: MulAction.toPerm, Eq.symm, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ A ⊆ a • B ↔ a⁻¹ • A ⊆ B

Tactic:
(image_subset_iff.trans ?_).symm

Premises used: Iff.trans, Set.image_subset_iff, Iff.symm
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
refine : A ⊆ (fun (x : β) ↦ a⁻¹ • x) ⁻¹' B ↔ A ⊆ a • B
⊢ A ⊆ a • B ↔ a⁻¹ • A ⊆ B

Tactic:
refine (image_subset_iff.trans ?_).symm

Premises used: Iff.trans, Set.image_subset_iff, Iff.symm
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
a₁ : (fun (x : β) ↦ a⁻¹ • x) ⁻¹' B = a • B
⊢ A ⊆ (fun (x : β) ↦ a⁻¹ • x) ⁻¹' B ↔ A ⊆ a • B

Tactic:
congr! 1
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ (fun (x : β) ↦ a⁻¹ • x) ⁻¹' B = a • B

Tactic:
((MulAction.toPerm _).image_eq_preimage_symm _).symm

Premises used: MulAction.toPerm, Equiv.image_eq_preimage_symm, Eq.symm
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ (fun (x : β) ↦ a⁻¹ • x) ⁻¹' B = a • B

Tactic:
exact ((MulAction.toPerm _).image_eq_preimage_symm _).symm

Premises used: MulAction.toPerm, Equiv.image_eq_preimage_symm, Eq.symm
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s t : Set β
a : α
⊢ a • (s ∩ t) = a • s ∩ a • t

Tactic:
image_inter <| MulAction.injective a

Premises used: Set.image_inter, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
ι : Sort u_5
a : α
t : ι → Set β
⊢ HSMul.hSMul (β := Set β) a (⋂ (i : ι), t i) = ⋂ (i : ι), a • t i

Tactic:
image_iInter (MulAction.bijective a) t

Premises used: MulAction.bijective, Set.image_iInter
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s t : Set β
a : α
⊢ a • (s \ t) = a • s \ a • t

Tactic:
image_diff (MulAction.injective a) _ _

Premises used: Set.image_diff, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s t : Set β
a : α
⊢ a • s ∆ t = (a • s) ∆ (a • t)

Tactic:
image_symmDiff (MulAction.injective a) _ _

Premises used: Set.image_symmDiff, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
a : α
⊢ HSMul.hSMul (β := Set β) a univ = univ

Tactic:
image_univ_of_surjective <| MulAction.surjective a

Premises used: Set.image_univ_of_surjective, MulAction.surjective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
a : α
rw : s = HSMul.hSMul (β := Set β) a⁻¹ univ ↔ s = univ
rw₁ rw₂ : s = univ ↔ s = univ
⊢ a • s = univ ↔ s = univ

Tactic:
rw [smul_eq_iff_eq_inv_smul, smul_set_univ]

Premises used: Set.smul_set_univ, smul_eq_iff_eq_inv_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set α
hs : s.Nonempty
⊢ HSMul.hSMul (β := Set β) s univ = univ

Tactic:
let ⟨a, ha⟩ := hs
  eq_univ_of_forall fun b ↦ ⟨a, ha, a⁻¹ • b, trivial, smul_inv_smul _ _⟩

Premises used: trivial, Set.univ, _private.0.Set.smul_univ.match_1, smul_inv_smul, Inv.inv, Set.eq_univ_of_forall, And.intro, Exists.intro, HSMul.hSMul, Eq
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
a : α
simp_rw : a • (univ \ s) = univ \ a • s
simp_rw₁ : HSMul.hSMul (β := Set β) a univ \ a • s = univ \ a • s
⊢ a • sᶜ = (a • s)ᶜ

Tactic:
simp_rw [Set.compl_eq_univ_diff, smul_set_sdiff, smul_set_univ]

Premises used: Set.smul_set_sdiff, Set.smul_set_univ, Set.compl_eq_univ_diff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
mp : (x • s ∩ t).Nonempty → ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
mpr : (∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty
⊢ (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
x a : α
h : a ∈ x • s
ha : a ∈ t
mp : ∀ (b : α) (hb : b ∈ s) (h : x • b ∈ x • s) (ha : x • b ∈ t), ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
⊢ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

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

Premises used: Set.mem_smul_set, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ x • b * b⁻¹ = x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : 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 ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
exact ⟨x • b, b, ⟨ha, hb⟩, by simp⟩
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ (a * b⁻¹) • b = a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ ((a * b⁻¹) • s ∩ t).Nonempty

Tactic:
exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
rw : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
rw₁ rw₂ : (∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
⊢ x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
rw [← nonempty_iff_ne_empty, smul_inter_nonempty_iff]

Premises used: Set.smul_inter_nonempty_iff, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
simp_rw : (∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
⊢ (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x

Tactic:
simp_rw [smul_inter_nonempty_iff, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Set.smul_inter_nonempty_iff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
rw : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
rw₁ rw₂ : (∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x) ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
⊢ x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x

Tactic:
rw [← nonempty_iff_ne_empty, smul_inter_nonempty_iff']

Premises used: Set.nonempty_iff_ne_empty, Set.smul_inter_nonempty_iff'
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : αᵐᵒᵖ
mp : (x • s ∩ t).Nonempty → ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
mpr : (∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty
⊢ (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : αᵐᵒᵖ
a : α
h : a ∈ x • s
ha : a ∈ t
mp : ∀ (b : α) (hb : b ∈ s) (h : x • b ∈ x • s) (ha : x • b ∈ t), ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
⊢ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

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

Premises used: Set.mem_smul_set, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : 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
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : 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⟩
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
⊢ op (a⁻¹ * b) = x

Tactic:
have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : 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]
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : 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⟩
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : αᵐᵒᵖ
rw : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
rw₁ rw₂ :
  (∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
⊢ x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Tactic:
rw [← nonempty_iff_ne_empty, op_smul_inter_nonempty_iff]

Premises used: Set.op_smul_inter_nonempty_iff, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g⁻¹ • s) (⋃ (g : α), g • s)

Tactic:
(Function.Surjective.iSup_congr _ inv_surjective) fun _ ↦ rfl

Premises used: inv_surjective, Function.Surjective.iSup_congr, Set.iUnion, rfl
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
simp_rw : Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g • s) (⋃ (i : α), {x : β | i • x ∈ s})
simp_rw₁ : Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g⁻¹ • s) (⋃ (i : α), {x : β | i • x ∈ s})
simp_rw₂ : Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), (fun (x : β) ↦ g • x) ⁻¹' s) (⋃ (i : α), {x : β | i • x ∈ s})
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g • s) {a : β | ∃ (g : α), g • a ∈ s}

Tactic:
simp_rw [← iUnion_setOf, ← iUnion_inv_smul, ← preimage_smul, preimage]

Premises used: Set.iUnion_inv_smul, Set.preimage_smul, Set.preimage, Set.iUnion_setOf
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
a : α
s : Set α
h : ∀ (x : α), x ∈ (a • s)⁻¹ ↔ x ∈ op a⁻¹ • s⁻¹
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
a : α
s : Set α
x : α
⊢ x ∈ (a • s)⁻¹ ↔ x ∈ op a⁻¹ • s⁻¹

Tactic:
simp [mem_smul_set_iff_inv_smul_mem]

Premises used: Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
a : α
s : Set α
h : ∀ (x : α), x ∈ (op a • s)⁻¹ ↔ x ∈ a⁻¹ • s⁻¹
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
a : α
s : Set α
x : α
⊢ x ∈ (op a • s)⁻¹ ↔ x ∈ a⁻¹ • s⁻¹

Tactic:
simp [mem_smul_set_iff_inv_smul_mem]

Premises used: Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s t : Set β
a : α
⊢ Disjoint (a • s) (a • t) ↔ Disjoint s t

Tactic:
disjoint_image_iff <| MulAction.injective _

Premises used: Set.disjoint_image_iff, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s t : Set β
a : α
⊢ Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t)

Tactic:
simpa using disjoint_smul_set (a := a) (t := a⁻¹ • t)

Premises used: Set.disjoint_smul_set
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s t : Set β
a : α
⊢ Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t

Tactic:
simpa using disjoint_smul_set (a := a) (s := a⁻¹ • s)

Premises used: Set.disjoint_smul_set
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
simp_rw : (∀ ⦃i j : α⦄, ((j⁻¹ * i) • s ∩ s).Nonempty → i = j) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
⊢ Pairwise.{u_2} (α := α) (onFun.{u_2 + 1, u_3 + 1, 1} (β := Set β) Disjoint fun (a : α) ↦ a • s) ↔
    ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

Tactic:
simp_rw [Pairwise, disjoint_smul_set_right, ← mul_smul,
    ← not_imp_not (b := _ ≠ _), not_ne_iff, not_disjoint_iff_nonempty_inter]

Premises used: Set.not_disjoint_iff_nonempty_inter, not_ne_iff, Pairwise, Set.disjoint_smul_set_right, SemigroupAction.mul_smul, not_imp_not
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
h : ∀ ⦃i j : α⦄, ((j⁻¹ * i) • s ∩ s).Nonempty → i = j
a : α
⊢ (a • s ∩ s).Nonempty → a = 1

Tactic:
simpa using @h a 1
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
h : ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
i j : α
ne : ((j⁻¹ * i) • s ∩ s).Nonempty
⊢ i = j

Tactic:
simpa [inv_mul_eq_one, eq_comm] using h _ ne

Premises used: eq_comm, inv_mul_eq_one
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
⊢ (∀ ⦃i j : α⦄, ((j⁻¹ * i) • s ∩ s).Nonempty → i = j) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

Tactic:
exact ⟨fun h a ↦ by simpa using @h a 1,
    fun h i j ne ↦ by simpa [inv_mul_eq_one, eq_comm] using h _ ne⟩
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b : α
inl : ∀ (hAB : a • s ∩ b • t = ∅), ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
inr : ∀ (z : α) (hzA : z ∈ a • s) (hzB : z ∈ b • t), ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
⊢ ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
obtain hAB | ⟨z, hzA, hzB⟩ := (a • s ∩ b • t).eq_empty_or_nonempty

Premises used: Inter.inter, Set.eq_empty_or_nonempty, HSMul.hSMul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b : α
hAB : a • s ∩ b • t = ∅
⊢ a • s ∩ b • t ⊆ HSMul.hSMul (α := α) 1 (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
simp [hAB]
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b : α
hAB : a • s ∩ b • t = ∅
⊢ ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
exact ⟨1, by simp [hAB]⟩
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
⟨z, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
inr : a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
⊢ ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
refine ⟨z, ?_⟩
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
h₁ : a • s ⊆ z • s⁻¹ * s
h₂ : b • t ⊆ z • t⁻¹ * t
⊢ a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
h₁ : a ∈ z • s⁻¹
⊢ a • s ⊆ z • s⁻¹ * s

Tactic:
apply smul_set_subset_mul

Premises used: Set.smul_set_subset_mul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
h₂ : b ∈ z • t⁻¹
⊢ b • t ⊆ z • t⁻¹ * t

Tactic:
apply smul_set_subset_mul

Premises used: Set.smul_set_subset_mul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a ∈ z • s⁻¹

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ b ∈ z • t⁻¹

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
simp_rw : z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s) ∩ z • (t⁻¹ * t)
⊢ z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
simp_rw [Set.smul_set_inter, smul_mul_assoc]

Premises used: Set.smul_set_inter, smul_mul_assoc
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
a₁ : a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)
a₂ : z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s ∩ (t⁻¹ * t))
⊢ a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
calc
    a • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by
      gcongr <;> apply smul_set_subset_mul <;> simpa
    _ = z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by simp_rw [Set.smul_set_inter, smul_mul_assoc]

Premises used: HMul.hMul, Inter.inter, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Monoid α
inst_1 : MulAction α β
s : Set β
a : α
b : β
inst_2 : Invertible a
⊢ b ∈ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ • s ↔ a • b ∈ s

Tactic:
mem_inv_smul_set_iff (a := unitOfInvertible a)

Premises used: Set.Mem, Set.mem_inv_smul_set_iff