awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
a b : α
⊢ HDiv.hDiv (α := Set α) {a} {b} = {a / b}

Tactic:
image2_singleton

Premises used: Set.image2_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s₁ s₂ t₁ t₂ : Set α
⊢ s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ / s₂ ⊆ t₁ / t₂

Tactic:
image2_subset

Premises used: Set.image2_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t₁ t₂ : Set α
⊢ t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂

Tactic:
image2_subset_left

Premises used: Set.image2_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s₁ s₂ t : Set α
⊢ s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t

Tactic:
image2_subset_right

Premises used: Set.image2_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t u : Set α
⊢ s / t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x / y ∈ u

Tactic:
image2_subset_iff

Premises used: Set.image2_subset_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s₁ s₂ t : Set α
⊢ (s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t

Tactic:
image2_union_left

Premises used: Set.image2_union_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t₁ t₂ : Set α
⊢ s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂

Tactic:
image2_union_right

Premises used: Set.image2_union_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s₁ s₂ t : Set α
⊢ s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)

Tactic:
image2_inter_subset_left

Premises used: Set.image2_inter_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t₁ t₂ : Set α
⊢ s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)

Tactic:
image2_inter_subset_right

Premises used: Set.image2_inter_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s₁ s₂ t₁ t₂ : Set α
⊢ s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂

Tactic:
image2_inter_union_subset_union

Premises used: Set.image2_inter_union_subset_union
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s₁ s₂ t₁ t₂ : Set α
⊢ (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂

Tactic:
image2_union_inter_subset_union

Premises used: Set.image2_union_inter_subset_union
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : CommSemigroup α
s t : Set α
⊢ s ∩ t * (s ∪ t) ⊆ s * t

Tactic:
image2_inter_union_subset mul_comm

Premises used: Set.image2_inter_union_subset, mul_comm
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : CommSemigroup α
s t : Set α
⊢ (s ∪ t) * (s ∩ t) ⊆ s * t

Tactic:
image2_union_inter_subset mul_comm

Premises used: mul_comm, Set.image2_union_inter_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : MulOneClass α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s * t

Tactic:
fun x hx =>
  ⟨x, hx, 1, ht, mul_one _⟩

Premises used: Set.Mem, setOf, Set.Subset, Set.image2, And.intro, Exists.intro, mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : MulOneClass α
s t : Set α
hs : 1 ∈ s
⊢ t ⊆ s * t

Tactic:
fun x hx =>
  ⟨1, hs, x, hx, one_mul _⟩

Premises used: Set.Mem, setOf, Set.Subset, Set.image2, And.intro, Exists.intro, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : MulOneClass α
⊢ Eq (α := (a : α) → Set α) (⇑singletonMonoidHom : (a : α) → Set α) singleton

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : MulOneClass α
a : α
⊢ Eq (α := Set α) ((singletonMonoidHom : (a : α) → Set α) a : Set α) ({a} : Set α)

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s : Set α
hs : 1 ∈ s
⊢ Monotone.{0, u_2} (β := Set α) fun (x : ℕ) ↦ s ^ x

Tactic:
pow_right_monotone <| one_subset.2 hs

Premises used: Iff.mpr, pow_right_monotone, Set.one_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
n : ℕ
hst : s ⊆ t
⊢ s ^ n ⊆ t ^ n

Tactic:
pow_left_mono _ hst

Premises used: pow_left_mono
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s : Set α
m n : ℕ
hs : 1 ∈ s
hmn : m ≤ n
⊢ s ^ m ⊆ s ^ n

Tactic:
Set.pow_right_monotone hs hmn

Premises used: Set.pow_right_monotone
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
m n : ℕ
hst : s ⊆ t
ht : 1 ∈ t
hmn : m ≤ n
⊢ s ^ m ⊆ t ^ n

Tactic:
(pow_subset_pow_left hst).trans (pow_subset_pow_right ht hmn)

Premises used: HasSubset.Subset.trans, Set.pow_subset_pow_right, Set.pow_subset_pow_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s : Set α
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Tactic:
simpa using pow_subset_pow_right hs <| Nat.one_le_iff_ne_zero.2 hn

Premises used: Iff.mpr, Set.pow_subset_pow_right, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
n : ℕ
hst : HPow.hPow (β := ℕ) s 2 ⊆ t * s
hn : n ≠ 0
⊢ s ^ n ⊆ t ^ (n - 1) * s

Tactic:
pow_le_pow_mul_of_sq_le_mul hst hn

Premises used: pow_le_pow_mul_of_sq_le_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
n_1 n : ℕ
hn : n + 1 ≠ 0
⊢ HPow.hPow (α := Set α) ∅ (n + 1) = ∅

Tactic:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s : Set α
hs : s.Nonempty
⊢ (HPow.hPow (β := ℕ) s 0).Nonempty

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
rw : (s ^ n * s).Nonempty
⊢ (s ^ (n + 1)).Nonempty

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty

Tactic:
hs.pow.mul hs

Premises used: Set.Nonempty.mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty

Tactic:
exact hs.pow.mul hs

Premises used: Set.Nonempty.mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
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 : Monoid α
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 : Monoid α
s : Set α
n : ℕ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

Tactic:
hs.pow

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

Tactic:
exact hs.pow

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

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

Tactic:
empty_pow hn

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

Tactic:
exact empty_pow hn

Premises used: Set.empty_pow
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
a : α
⊢ HPow.hPow (α := Set α) (β := ℕ) {a} 0 = {HPow.hPow (β := ℕ) a 0}

Tactic:
simp [singleton_one]

Premises used: Set.singleton_one
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
a : α
n : ℕ
⊢ HPow.hPow (α := Set α) {a} (n + 1) = {a ^ (n + 1)}

Tactic:
simp [pow_succ, singleton_pow _ n]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s : Set α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n

Tactic:
simpa using pow_subset_pow_left (singleton_subset_iff.2 ha)

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.pow_subset_pow_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s : Set α
n : ℕ
hs : 1 ∈ s
⊢ 1 ∈ s ^ n

Tactic:
simpa using pow_mem_pow hs

Premises used: Set.pow_mem_pow
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
n : ℕ
rs : (s ∩ t) ^ n ⊆ s ^ n
rt : (s ∩ t) ^ n ⊆ t ^ n
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
apply subset_inter

Premises used: Set.subset_inter
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
n : ℕ
rs : s ∩ t ⊆ s
⊢ (s ∩ t) ^ n ⊆ s ^ n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
n : ℕ
rt : s ∩ t ⊆ t
⊢ (s ∩ t) ^ n ⊆ t ^ n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ s

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ t

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

Tactic:
eq_univ_iff_forall.2 fun _ => mem_mul.2 ⟨_, hs, _, mem_univ _, one_mul _⟩

Premises used: Iff.mpr, Set.eq_univ_iff_forall, And.intro, Exists.intro, Set.mem_univ, OfNat.ofNat, one_mul, Set.mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
t : Set α
ht : 1 ∈ t
⊢ univ * t = univ

Tactic:
eq_univ_iff_forall.2 fun _ => mem_mul.2 ⟨_, mem_univ _, _, ht, mul_one _⟩

Premises used: Iff.mpr, Set.eq_univ_iff_forall, And.intro, Exists.intro, Set.mem_univ, mul_one, OfNat.ofNat, Set.mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
⊢ HMul.hMul (α := Set α) univ univ = univ

Tactic:
mul_univ_of_one_mem <| mem_univ _

Premises used: Set.mem_univ, Set.mul_univ_of_one_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
h : n + 2 ≠ 0
rw : HPow.hPow (α := Set α) univ (n + 1) * univ = univ
rw₁ : HMul.hMul (α := Set α) univ univ = univ
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set α) univ univ
⊢ HPow.hPow (α := Set α) univ (n + 2) = univ

Tactic:
rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]

Premises used: pow_succ, Set.univ_mul_univ, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Monoid α
a : α
⊢ IsUnit a → IsUnit (M := Set α) {a}

Tactic:
IsUnit.map (singletonMonoidHom : α →* Set α)

Premises used: setOf, Set.singleton, IsUnit.map, Set.singletonMonoidHom
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Monoid α
inst_1 : Monoid β
s : Set α
t : Set β
⊢ HPow.hPow (β := ℕ) (s ×ˢ t) 0 = HPow.hPow (β := ℕ) s 0 ×ˢ HPow.hPow (β := ℕ) t 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Monoid α
inst_1 : Monoid β
s : Set α
t : Set β
n : ℕ
⊢ s ×ˢ t ^ (n + 1) = (s ^ (n + 1)) ×ˢ (t ^ (n + 1))

Tactic:
simp [pow_succ, prod_pow _ _ n]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
s t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ c * a ≠ c * b

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
s t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ (s * t).Nontrivial

Tactic:
exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
s t : Set α
hs : s.Nontrivial
ht : t.Nontrivial
⊢ (s * t).Nontrivial

Tactic:
ht.mul_left hs.nonempty

Premises used: Set.Nontrivial.nonempty, Set.Nontrivial.mul_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ a * c ≠ b * c

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ (s * t).Nontrivial

Tactic:
exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : CancelMonoid α
s : Set α
hs : s.Nontrivial
h : Ne (α := ℕ) 1 0
⊢ (HPow.hPow (β := ℕ) s 1).Nontrivial

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : CancelMonoid α
s : Set α
hs : s.Nontrivial
n : ℕ
h : n + 2 ≠ 0
⊢ (s ^ (n + 2)).Nontrivial

Tactic:
simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs

Premises used: Set.Nontrivial.mul, pow_succ, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
⊢ s * t = 1 ↔ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
refine_1 : ∀ (h : s * t = 1), ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
refine_2 : (∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1
⊢ s * t = 1 ↔ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ (s * t).Nonempty

Tactic:
have hst : (s * t).Nonempty := h.symm.subst one_nonempty
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
refine_1 : ∀ (a : α) (ha : a ∈ s), ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
⊢ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
obtain ⟨a, ha⟩ := hst.of_image2_left

Premises used: Set.Nonempty.of_image2_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
refine_1 : ∀ (b : α) (hb : b ∈ t), ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
⊢ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
obtain ⟨b, hb⟩ := hst.of_image2_right

Premises used: Set.Nonempty.of_image2_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1

Tactic:
have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb =>
      h.subset <| mem_image2_of_mem ha hb
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
⟨a, b, ?_, ?_, H ha hb⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
refine_1 : s = {a}
refine_1₁ : t = {b}
⊢ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
refine ⟨a, b, ?_, ?_, H ha hb⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ s = {a}

Tactic:
eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩

Premises used: Iff.mpr, And.intro, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
refine_1 : ∀ (x : α) (hx : x ∈ s), x = a
⊢ s = {a}

Tactic:
refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩

Premises used: Iff.mpr, And.intro, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ t = {b}

Tactic:
eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩

Premises used: Iff.mpr, And.intro, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
refine_1 : ∀ (x : α) (hx : x ∈ t), x = b
⊢ t = {b}

Tactic:
refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩

Premises used: Iff.mpr, And.intro, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a

Tactic:
(eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)

Premises used: eq_inv_of_mul_eq_one_left, Eq.trans, inv_eq_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a

Tactic:
exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)

Premises used: eq_inv_of_mul_eq_one_left, Eq.trans, inv_eq_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b

Tactic:
(eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)

Premises used: inv_eq_of_mul_eq_one_right, eq_inv_of_mul_eq_one_right, Eq.trans
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b

Tactic:
exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)

Premises used: inv_eq_of_mul_eq_one_right, eq_inv_of_mul_eq_one_right, Eq.trans
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
b c : α
h : b * c = 1
refine_2 : Eq (α := Set α) {b * c} 1
refine_2₁ : Eq (α := Set α) {1} 1
refine_2₂ refine_2₃ : Eq.{u_2 + 1} (α := Set α) 1 1
⊢ HMul.hMul (α := Set α) {b} {c} = 1

Tactic:
rw [singleton_mul_singleton, h, singleton_one]

Premises used: Set.singleton_one, Set.singleton_mul_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
rw : (((fun (x : α) ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
⊢ ((fun (x : α) ↦ a⁻¹ * x) '' s ∩ t).Nonempty ↔ ((fun (x : α) ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
rw [← nonempty_inv, inter_inv]

Premises used: Set.inter_inv, Set.nonempty_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
simp_rw :
  Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹) '' (fun (x : α) ↦ a⁻¹ * x) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ x * a) '' (fun (x : α) ↦ x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
simp_rw₁ :
  Set.Nonempty (α := α) ((fun (x : α) ↦ (a⁻¹ * x)⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹ * a) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
simp_rw₂ :
  Set.Nonempty (α := α) ((fun (a_1 : α) ↦ a_1⁻¹ * a⁻¹⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹ * a) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
⊢ (((fun (x : α) ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]

Premises used: Set.image_image, inv_inv, mul_inv_rev, Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
rw : (((fun (x : α) ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
⊢ ((fun (x : α) ↦ x * a⁻¹) '' s ∩ t).Nonempty ↔ ((fun (x : α) ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
rw [← nonempty_inv, inter_inv]

Premises used: Set.inter_inv, Set.nonempty_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
simp_rw :
  Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹) '' (fun (x : α) ↦ x * a⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
simp_rw₁ :
  Set.Nonempty (α := α) ((fun (x : α) ↦ (x * a⁻¹)⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ a * x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
simp_rw₂ :
  Set.Nonempty (α := α) ((fun (a_1 : α) ↦ a⁻¹⁻¹ * a_1⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ a * x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
⊢ (((fun (x : α) ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]

Premises used: Set.image_image, inv_inv, mul_inv_rev, Set.image_inv_eq_inv
-- 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 α
rw : id '' (s / t) = s * (fun (x : α) ↦ x⁻¹) '' t
⊢ s / t = s * t⁻¹

Tactic:
rw [← image_id (s / t), ← image_inv_eq_inv]

Premises used: HDiv.hDiv, Set.image_inv_eq_inv, Set.image_id
-- 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 α
⊢ id '' (s / t) = s * (fun (x : α) ↦ x⁻¹) '' t

Tactic:
image_image2_distrib_right div_eq_mul_inv

Premises used: div_eq_mul_inv, Set.image_image2_distrib_right
-- 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 α
⊢ id '' (s / t) = s * (fun (x : α) ↦ x⁻¹) '' t

Tactic:
exact image_image2_distrib_right div_eq_mul_inv

Premises used: Set.image_image2_distrib_right
-- 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 α
simp_rw : (fun (x : α) ↦ x⁻¹) '' (s * t) = HMul.hMul (α := Set α) ((fun (x : α) ↦ x⁻¹) '' t) ((fun (x : α) ↦ x⁻¹) '' s)
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹

Tactic:
simp_rw [← 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
γ : Type u_4
inst : DivisionMonoid α
s_1 t_1 : Set α
n : ℤ
s t : Set α
⊢ (fun (x : α) ↦ x⁻¹) '' (s * t) = HMul.hMul (α := Set α) ((fun (x : α) ↦ x⁻¹) '' t) ((fun (x : α) ↦ x⁻¹) '' s)

Tactic:
image_image2_antidistrib mul_inv_rev

Premises used: mul_inv_rev, Set.image_image2_antidistrib
-- 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 α
⊢ (fun (x : α) ↦ x⁻¹) '' (s * t) = HMul.hMul (α := Set α) ((fun (x : α) ↦ x⁻¹) '' t) ((fun (x : α) ↦ x⁻¹) '' s)

Tactic:
exact image_image2_antidistrib mul_inv_rev

Premises used: mul_inv_rev, Set.image_image2_antidistrib