awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DivisionMonoid α
s_1 t_1 : Set α
n : ℤ
s t : Set α
h : s * t = 1
obtain : ∀ (a b : α) (hab : a * b = 1) (h : HMul.hMul (α := Set α) {a} {b} = 1), Eq (α := Set α) {a}⁻¹ {b}
⊢ s⁻¹ = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := Set.mul_eq_one_iff.1 h

Premises used: Set.mul_eq_one_iff, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DivisionMonoid α
s t : Set α
n : ℤ
a b : α
hab : a * b = 1
h : HMul.hMul (α := Set α) {a} {b} = 1
rw : Eq (α := Set α) {a⁻¹} {b}
rw₁ rw₂ : Eq (α := Set α) {b} {b}
⊢ Eq (α := Set α) {a}⁻¹ {b}

Tactic:
rw [inv_singleton, inv_eq_of_mul_eq_one_right hab]

Premises used: inv_eq_of_mul_eq_one_right, Set.inv_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
mp : IsUnit s → ∃ (a : α), s = {a} ∧ IsUnit a
mpr : (∃ (a : α), s = {a} ∧ IsUnit a) → IsUnit s
⊢ IsUnit s ↔ ∃ (a : α), s = {a} ∧ IsUnit a

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Set α)ˣ
mp :
  ∀ (a b : α) (ha : (↑u : Set α) = {a}) (hb : (↑u⁻¹ : Set α) = {b}) (h : a * b = 1),
    ∃ (a : α), (↑u : Set α) = {a} ∧ IsUnit a
⊢ ∃ (a : α), (↑u : Set α) = {a} ∧ IsUnit a

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := Set.mul_eq_one_iff.1 u.mul_inv

Premises used: Set.mul_eq_one_iff, Units.mul_inv, Iff.mp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : (↑u : Set α) = {a}
hb : (↑u⁻¹ : Set α) = {b}
h : a * b = 1
⊢ ∃ (a : α), (↑u : Set α) = {a} ∧ IsUnit a

Tactic:
⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩

Premises used: Set.singleton_injective, And.intro, Units.mk, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : (↑u : Set α) = {a}
hb : (↑u⁻¹ : Set α) = {b}
h : a * b = 1
mp : Eq (α := Set α) {b * a} {1}
⊢ ∃ (a : α), (↑u : Set α) = {a} ∧ IsUnit a

Tactic:
refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : (↑u : Set α) = {a}
hb : (↑u⁻¹ : Set α) = {b}
h : a * b = 1
mp : (↑u⁻¹ : Set α) * (↑u : Set α) = {1}
⊢ Eq (α := Set α) {b * a} {1}

Tactic:
rw [← singleton_mul_singleton, ← ha, ← hb]

Premises used: Set.singleton_mul_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : (↑u : Set α) = {a}
hb : (↑u⁻¹ : Set α) = {b}
h : a * b = 1
⊢ (↑u⁻¹ : Set α) * (↑u : Set α) = {1}

Tactic:
u.inv_mul

Premises used: Units.inv_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : (↑u : Set α) = {a}
hb : (↑u⁻¹ : Set α) = {b}
h : a * b = 1
⊢ (↑u⁻¹ : Set α) * (↑u : Set α) = {1}

Tactic:
exact u.inv_mul

Premises used: Units.inv_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit (M := Set α) {a}

Tactic:
ha.set

Premises used: IsUnit.set
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit (M := Set α) {a}

Tactic:
exact ha.set

Premises used: IsUnit.set
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
⊢ HDiv.hDiv (α := Set α) univ univ = univ

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
rw : s ⊆ s * t⁻¹
⊢ s ⊆ s / t

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ 1 ∈ t⁻¹

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹

Tactic:
exact subset_mul_left _ <| by simpa

Premises used: Set.subset_mul_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
rw : t⁻¹ ⊆ s * t⁻¹
⊢ t⁻¹ ⊆ s / t

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹

Tactic:
subset_mul_right _ hs

Premises used: Set.subset_mul_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹

Tactic:
exact subset_mul_right _ hs

Premises used: Set.subset_mul_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
n : ℤ
hn : n ≠ 0
ofNat : ∀ (a : ℕ) (hn : Int.ofNat a ≠ 0), HPow.hPow (α := Set α) ∅ (Int.ofNat a) = ∅
negSucc : ∀ (a : ℕ) (hn : Int.negSucc a ≠ 0), HPow.hPow (α := Set α) ∅ (Int.negSucc a) = ∅
⊢ HPow.hPow (α := Set α) ∅ n = ∅

Tactic:
cases n
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
a : ℕ
hn : Int.ofNat a ≠ 0
⊢ HPow.hPow (α := Set α) ∅ (Int.ofNat a) = ∅

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
a : ℕ
hn : Int.negSucc a ≠ 0
⊢ HPow.hPow (α := Set α) ∅ (Int.negSucc a) = ∅

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ Int.negSucc n).Nonempty

Tactic:
simpa using hs.pow

Premises used: Set.Nonempty.pow
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
n : ℤ
mp : s ^ n = ∅ → s = ∅ ∧ n ≠ 0
mpr : s = ∅ ∧ n ≠ 0 → s ^ n = ∅
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
n : ℤ
mp : s.Nonempty ∨ n = 0 → (s ^ n).Nonempty
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose! +distrib
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
n : ℤ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

Tactic:
hs.zpow

Premises used: Set.Nonempty.zpow
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
n : ℤ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

Tactic:
exact hs.zpow

Premises used: Set.Nonempty.zpow
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
⊢ (HPow.hPow (β := ℤ) s 0).Nonempty

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ HPow.hPow (α := Set α) ∅ n = ∅

Tactic:
empty_zpow hn

Premises used: Set.empty_zpow
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ HPow.hPow (α := Set α) ∅ n = ∅

Tactic:
exact empty_zpow hn

Premises used: Set.empty_zpow
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
n : ℤ
ofNat : ∀ (a_1 : ℕ), HPow.hPow (α := Set α) {a} (Int.ofNat a_1) = {a ^ Int.ofNat a_1}
negSucc : ∀ (a_1 : ℕ), HPow.hPow (α := Set α) {a} (Int.negSucc a_1) = {a ^ Int.negSucc a_1}
⊢ HPow.hPow (α := Set α) {a} n = {a ^ n}

Tactic:
cases n
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
a_1 : ℕ
⊢ HPow.hPow (α := Set α) {a} (Int.ofNat a_1) = {a ^ Int.ofNat a_1}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
a_1 : ℕ
⊢ HPow.hPow (α := Set α) {a} (Int.negSucc a_1) = {a ^ Int.negSucc a_1}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
⊢ 1 ∈ s / t ↔ ¬Disjoint s t

Tactic:
simp [not_disjoint_iff_nonempty_inter, mem_div, div_eq_one, Set.Nonempty]

Premises used: Set.not_disjoint_iff_nonempty_inter, Set.mem_div, Set.Nonempty, div_eq_one
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
⊢ 1 ∈ t⁻¹ * s ↔ ¬Disjoint s t

Tactic:
aesop (add simp [not_disjoint_iff_nonempty_inter, mem_mul, mul_eq_one_iff_eq_inv, Set.Nonempty])

Premises used: mul_eq_one_iff_eq_inv, Set.not_disjoint_iff_nonempty_inter, Set.Nonempty, Set.mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
⊢ ¬1 ∈ s / t ↔ Disjoint s t

Tactic:
one_mem_div_iff.not_left

Premises used: Iff.not_left, Set.one_mem_div_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s t : Set α
⊢ ¬1 ∈ t⁻¹ * s ↔ Disjoint s t

Tactic:
one_mem_inv_mul_iff.not_left

Premises used: Iff.not_left, Set.one_mem_inv_mul_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s : Set α
h : s.Nonempty
⊢ 1 ∈ s / s

Tactic:
let ⟨a, ha⟩ := h
  mem_div.2 ⟨a, ha, a, ha, div_self' _⟩

Premises used: Iff.mpr, _private.0.Set.Nonempty.one_mem_div.match_1, Membership.mem, HDiv.hDiv, Set.mem_div, div_self', And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
a : α
⊢ IsUnit (M := Set α) {a}

Tactic:
(Group.isUnit a).set

Premises used: Group.isUnit, IsUnit.set
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s : Set α
⊢ IsUnit s ↔ ∃ (a : α), s = {a}

Tactic:
simp only [isUnit_iff, Group.isUnit, and_true]

Premises used: and_true, Set.isUnit_iff, Group.isUnit
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
t : Set α
a : α
h₁ : LeftInverse (fun (x : α) ↦ a⁻¹ * x) fun (x : α) ↦ a * x
h₂ : RightInverse (fun (x : α) ↦ a⁻¹ * x) fun (x : α) ↦ a * x
⊢ Eq (α := Set α) ((fun (x : α) ↦ a * x) '' t) ((fun (x : α) ↦ a⁻¹ * x) ⁻¹' t)

Tactic:
rw [image_eq_preimage_of_inverse]

Premises used: Set.image_eq_preimage_of_inverse
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
t : Set α
a c : α
⊢ (fun (x : α) ↦ a⁻¹ * x) ((fun (x : α) ↦ a * x) c) = c

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
t : Set α
a c : α
⊢ (fun (x : α) ↦ a * x) ((fun (x : α) ↦ a⁻¹ * x) c) = c

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
t : Set α
b : α
h₁ : LeftInverse (fun (x : α) ↦ x * b⁻¹) fun (x : α) ↦ x * b
h₂ : RightInverse (fun (x : α) ↦ x * b⁻¹) fun (x : α) ↦ x * b
⊢ Eq (α := Set α) ((fun (x : α) ↦ x * b) '' t) ((fun (x : α) ↦ x * b⁻¹) ⁻¹' t)

Tactic:
rw [image_eq_preimage_of_inverse]

Premises used: Set.image_eq_preimage_of_inverse
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
t : Set α
b c : α
⊢ (fun (x : α) ↦ x * b⁻¹) ((fun (x : α) ↦ x * b) c) = c

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
t : Set α
b c : α
⊢ (fun (x : α) ↦ x * b) ((fun (x : α) ↦ x * b⁻¹) c) = c

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
t : Set α
a : α
⊢ Eq (α := Set α) ((fun (x : α) ↦ a⁻¹ * x) '' t) ((fun (x : α) ↦ a * x) ⁻¹' t)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
t : Set α
b : α
⊢ Eq (α := Set α) ((fun (x : α) ↦ x * b⁻¹) '' t) ((fun (x : α) ↦ x * b) ⁻¹' t)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
a b : α
rw : Eq (α := Set α) ((fun (x : α) ↦ a⁻¹ * x) '' {b}) {a⁻¹ * b}
rw₁ rw₂ : Eq (α := Set α) {a⁻¹ * b} {a⁻¹ * b}
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ a * x) {b}) {a⁻¹ * b}

Tactic:
rw [← image_mul_left', image_singleton]

Premises used: Set.image_singleton, Set.image_mul_left'
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
a b : α
rw : Eq (α := Set α) ((fun (x : α) ↦ x * a⁻¹) '' {b}) {b * a⁻¹}
rw₁ rw₂ : Eq (α := Set α) {b * a⁻¹} {b * a⁻¹}
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ x * a) {b}) {b * a⁻¹}

Tactic:
rw [← image_mul_right', image_singleton]

Premises used: Set.image_singleton, Set.image_mul_right'
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
a : α
rw : Eq (α := Set α) ((fun (x : α) ↦ a⁻¹ * x) '' 1) {a⁻¹}
rw₁ : Eq (α := Set α) {a⁻¹ * 1} {a⁻¹}
rw₂ rw₃ : Eq (α := Set α) {a⁻¹} {a⁻¹}
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ a * x) 1) {a⁻¹}

Tactic:
rw [← image_mul_left', image_one, mul_one]

Premises used: Set.image_one, Set.image_mul_left', mul_one
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
b : α
rw : Eq (α := Set α) ((fun (x : α) ↦ x * b⁻¹) '' 1) {b⁻¹}
rw₁ : Eq (α := Set α) {1 * b⁻¹} {b⁻¹}
rw₂ rw₃ : Eq (α := Set α) {b⁻¹} {b⁻¹}
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ x * b) 1) {b⁻¹}

Tactic:
rw [← image_mul_right', image_one, one_mul]

Premises used: Set.image_mul_right', Set.image_one, one_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
a : α
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ a⁻¹ * x) 1) {a}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
b : α
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ x * b⁻¹) 1) {b}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
s : Set α
hs : s.Nonempty
⊢ s * univ = univ

Tactic:
let ⟨a, ha⟩ := hs
  eq_univ_of_forall fun b => ⟨a, ha, a⁻¹ * b, trivial, mul_inv_cancel_left ..⟩

Premises used: trivial, HMul.hMul, Set.univ, _private.0.Set.Nonempty.one_mem_div.match_1, Inv.inv, Set.eq_univ_of_forall, And.intro, Exists.intro, mul_inv_cancel_left, Eq
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Group α
t : Set α
ht : t.Nonempty
⊢ univ * t = univ

Tactic:
let ⟨a, ha⟩ := ht
  eq_univ_of_forall fun b => ⟨b * a⁻¹, trivial, a, ha, inv_mul_cancel_right ..⟩

Premises used: trivial, HMul.hMul, Set.univ, _private.0.Set.Nonempty.one_mem_div.match_1, Inv.inv, Set.eq_univ_of_forall, And.intro, Exists.intro, inv_mul_cancel_right, Eq
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
s : Set α
rw :
  Eq.{u_3 + 1} (α := Set β) (image (α := α) (⇑f : (a : α) → β) ((fun (x : α) ↦ x⁻¹) '' s))
    ((fun (x : β) ↦ x⁻¹) '' (⇑f : (a : α) → β) '' s)
⊢ Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s⁻¹) ((⇑f : (a : α) → β) '' s)⁻¹

Tactic:
rw [← image_inv_eq_inv, ← image_inv_eq_inv]

Premises used: Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
s : Set α
⊢ Eq.{u_3 + 1} (α := Set β) (image (α := α) (⇑f : (a : α) → β) ((fun (x : α) ↦ x⁻¹) '' s))
    ((fun (x : β) ↦ x⁻¹) '' (⇑f : (a : α) → β) '' s)

Tactic:
image_comm (map_inv _)

Premises used: map_inv, Set.image_comm
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
s : Set α
⊢ Eq.{u_3 + 1} (α := Set β) (image (α := α) (⇑f : (a : α) → β) ((fun (x : α) ↦ x⁻¹) '' s))
    ((fun (x : β) ↦ x⁻¹) '' (⇑f : (a : α) → β) '' s)

Tactic:
exact image_comm (map_inv _)

Premises used: map_inv, Set.image_comm
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
s t : Set α
⊢ (⇑m : (a : α) → β) '' (s * t) = HMul.hMul (α := Set β) ((⇑m : (a : α) → β) '' s) ((⇑m : (a : α) → β) '' t)

Tactic:
image_image2_distrib <| map_mul m

Premises used: map_mul, Set.image_image2_distrib
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
a : β
ha : a ∈ s
b : β
hb : b ∈ t
obtain :
  ∀ (a : α) (ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)),
    Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
      ((fun (x1 x2 : β) ↦ x1 * x2) ((m : (a : α) → β) a) b)
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)) ((fun (x1 x2 : β) ↦ x1 * x2) a b)

Tactic:
obtain ⟨a, rfl⟩ := hs ha

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
b : β
hb : b ∈ t
a : α
ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)
obtain :
  ∀ (b : α) (hb : Membership.mem (α := β) t ((m : (a : α) → β) b : β)),
    Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
      ((fun (x1 x2 : β) ↦ x1 * x2) ((m : (a : α) → β) a) ((m : (a : α) → β) b))
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 * x2) ((m : (a : α) → β) a) b)

Tactic:
obtain ⟨b, rfl⟩ := ht hb

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
a : α
ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)
b : α
hb : Membership.mem (α := β) t ((m : (a : α) → β) b : β)
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 * x2) ((m : (a : α) → β) a) ((m : (a : α) → β) b))

Tactic:
⟨a * b, map_mul ..⟩

Premises used: HMul.hMul, Set.Mem, setOf, map_mul, Exists.intro, Set.range
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
a : α
ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)
b : α
hb : Membership.mem (α := β) t ((m : (a : α) → β) b : β)
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 * x2) ((m : (a : α) → β) a) ((m : (a : α) → β) b))

Tactic:
exact ⟨a * b, map_mul ..⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
s t : Set β
w : α
left : Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' s) w
w_1 : α
left_1 : Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' t) w_1
⊢ Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' (s * t)) ((fun (x1 x2 : α) ↦ x1 * x2) w w_1)

Tactic:
⟨_, ‹_›, _, ‹_›, (map_mul m ..).symm⟩

Premises used: Set.Mem, setOf, map_mul, Set.preimage, Set.image2, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
s t : Set β
w : α
left : Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' s) w
w_1 : α
left_1 : Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' t) w_1
⊢ Membership.mem (γ := Set α) ((⇑m : (a : α) → β) ⁻¹' (s * t)) ((fun (x1 x2 : α) ↦ x1 * x2) w w_1)

Tactic:
exact ⟨_, ‹_›, _, ‹_›, (map_mul m ..).symm⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
hm : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑m : (a : α) → β)
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
rw :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) =
    HMul.hMul (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' s))
      (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t))
rw₁ :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) =
    s * image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t)
rw₂ : image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) = s * t
rw₃ rw₄ : s * t = s * t
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)))
    ((⇑m : (a : α) → β) '' HMul.hMul (α := Set α) ((⇑m : (a : α) → β) ⁻¹' s) ((⇑m : (a : α) → β) ⁻¹' t))

Tactic:
rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (mul_subset_range m hs ht)]

Premises used: Iff.mpr, Set.image_mul, Set.mul_subset_range, Set.image_preimage_eq_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid α
inst_1 : Monoid β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
h : Ne (α := ℕ) 1 0
⊢ ∀ (f : F) (s : Set α),
    (⇑f : (a : α) → β) '' HPow.hPow (β := ℕ) s 1 = HPow.hPow (α := Set β) (β := ℕ) ((⇑f : (a : α) → β) '' s) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid α
inst_1 : Monoid β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
n : ℕ
h : n + 2 ≠ 0
⊢ ∀ (f : F) (s : Set α), (⇑f : (a : α) → β) '' s ^ (n + 2) = HPow.hPow (α := Set β) ((⇑f : (a : α) → β) '' s) (n + 2)

Tactic:
simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

Premises used: pow_succ, Set.image_mul, Nat.succ
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid α
inst_1 : Monoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
s : Set α
⊢ (⇑f : (a : α) → β) '' HPow.hPow (β := ℕ) s 0 = HPow.hPow (α := Set β) (β := ℕ) ((⇑f : (a : α) → β) '' s) 0

Tactic:
simp [singleton_one]

Premises used: Set.singleton_one
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid α
inst_1 : Monoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
s : Set β
⊢ HPow.hPow (α := Set α) (β := ℕ) ((⇑f : (a : α) → β) ⁻¹' s) 0 ⊆ (⇑f : (a : α) → β) ⁻¹' HPow.hPow (β := ℕ) s 0

Tactic:
simp [Set.subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid α
inst_1 : Monoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
s : Set β
n : ℕ
⊢ HPow.hPow (α := Set α) ((⇑f : (a : α) → β) ⁻¹' s) (n + 1) ⊆ (⇑f : (a : α) → β) ⁻¹' s ^ (n + 1)

Tactic:
simpa [pow_succ] using Subset.trans (mul_subset_mul_right
    (preimage_pow_subset f s n)) (preimage_mul_preimage_subset f)

Premises used: Set.Subset.trans, pow_succ, Set.preimage_mul_preimage_subset, Set.mul_subset_mul_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
s t : Set α
⊢ (⇑m : (a : α) → β) '' (s / t) = HDiv.hDiv (α := Set β) ((⇑m : (a : α) → β) '' s) ((⇑m : (a : α) → β) '' t)

Tactic:
image_image2_distrib <| map_div m

Premises used: Set.image_image2_distrib, map_div