awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq β
inst_1 : DecidableEq γ
inst_2 : SMul.{u_2, u_3} αᵐᵒᵖ β
inst_3 : SMul β γ
inst_4 : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
a_1 : γ
⊢ a_1 ∈ (op a • s) • t ↔ a_1 ∈ s • a • t

Tactic:
simp [mem_smul, mem_smul_finset, h]

Premises used: Finset.mem_smul_finset, Finset.mem_smul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq β
inst_1 : DecidableEq γ
inst_2 : SMul α β
inst_3 : SMul α γ
f : β → γ
a : α
s : Finset β
⊢ (∀ (b : β), f (a • b) = a • f b) → image f (a • s) = a • image f s

Tactic:
image_comm

Premises used: Finset.image_comm
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
inst_1 : DecidableEq β
s : Set α
t : Set β
inst_2 : Fintype (↑s : Type u_2)
inst_3 : Fintype (↑t : Type u_3)
inst_4 : Fintype (↑(s • t) : Type u_3)
⊢ (s • t).toFinset = s.toFinset • t.toFinset

Tactic:
toFinset_image2 _ _ _

Premises used: Set.toFinset_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
inst_1 : DecidableEq β
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
hf : (s • t).Finite
⊢ hf.toFinset (s := s • t) = hs.toFinset (s := s) • ht.toFinset (s := t)

Tactic:
Finite.toFinset_image2 _ _ _

Premises used: Set.Finite.image2, Set.Finite.toFinset_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
a : α
s : Set β
inst_2 : Fintype (↑s : Type u_3)
inst_3 : Fintype (↑(a • s) : Type u_3)
⊢ (a • s).toFinset = a • s.toFinset

Tactic:
toFinset_image _ _

Premises used: Set.toFinset_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
a : α
s : Set β
hs : s.Finite
hf : (a • s).Finite
⊢ hf.toFinset (s := a • s) = a • hs.toFinset (s := s)

Tactic:
Finite.toFinset_image _ _ _

Premises used: Set.Finite.toFinset_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : VSub α β
s t : Set β
inst_2 : Fintype (↑s : Type u_3)
inst_3 : Fintype (↑t : Type u_3)
inst_4 : Fintype (↑(s -ᵥ t) : Type u_2)
⊢ (s -ᵥ t).toFinset = s.toFinset -ᵥ t.toFinset

Tactic:
toFinset_image2 _ _ _

Premises used: Set.toFinset_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : VSub α β
s t : Set β
hs : s.Finite
ht : t.Finite
hf : (s -ᵥ t).Finite
⊢ hf.toFinset (s := s -ᵥ t) = hs.toFinset (s := s) -ᵥ ht.toFinset (s := t)

Tactic:
Finite.toFinset_image2 _ _ _

Premises used: Set.Finite.image2, Set.Finite.toFinset_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : One α
⊢ Eq (α := Set α) {1} 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : One α
a : α
⊢ Membership.mem (γ := Set α) 1 a ↔ a = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : One α
⊢ Membership.mem (γ := Set α) 1 1

Tactic:
Eq.refl _

Premises used: Set.Mem, setOf, Set.singleton, Eq.refl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : One α
s : Set α
⊢ 1 ⊆ s ↔ 1 ∈ s

Tactic:
singleton_subset_iff

Premises used: Set.singleton_subset_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : One α
⊢ Set.Nonempty.{u_2} (α := α) 1

Tactic:
⟨1, rfl⟩

Premises used: Set.Nonempty, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
f : α → β
⊢ f '' 1 = {f 1}

Tactic:
image_singleton

Premises used: Set.image_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : One α
s : Set α
⊢ s ⊆ 1 ↔ s = ∅ ∨ s = 1

Tactic:
subset_singleton_iff_eq

Premises used: Set.subset_singleton_iff_eq
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : One α
s : Set α
h : s.Nonempty
⊢ s ⊆ 1 ↔ s = 1

Tactic:
h.subset_singleton_iff

Premises used: Set.Nonempty.subset_singleton_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : One α
⊢ Eq (α := (a : α) → Set α) (⇑singletonOneHom : (a : α) → Set α) singleton

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : One α
⊢ Eq.{u_2 + 1} (α := Set αᵐᵒᵖ) (op '' 1) 1

Tactic:
image_singleton

Premises used: Set.image_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : One β
h : ∀ (x : α × β), x ∈ SProd.sprod (α := Set α) (β := Set β) 1 1 ↔ Membership.mem (γ := Set (α × β)) 1 x
⊢ SProd.sprod (α := Set α) (β := Set β) 1 1 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : One β
x : α × β
⊢ x ∈ SProd.sprod (α := Set α) (β := Set β) 1 1 ↔ Membership.mem (γ := Set (α × β)) 1 x

Tactic:
simp [Prod.ext_iff]

Premises used: Prod.ext_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Inv α
p : α → Prop
⊢ Eq.{u_2 + 1} (α := Set α) {x : α | p x}⁻¹ {x : α | p x⁻¹}

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Inv α
s : Set α
a : α
⊢ a ∈ s⁻¹ ↔ a⁻¹ ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Inv α
s : Set α
⊢ Inv.inv ⁻¹' s = s⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Inv α
⊢ Eq.{u_2 + 1} (α := Set α) ∅⁻¹ ∅

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Inv α
⊢ Eq.{u_2 + 1} (α := Set α) univ⁻¹ univ

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Inv α
s t : Set α
⊢ (s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹

Tactic:
preimage_inter

Premises used: Set.preimage_inter
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Inv α
s t : Set α
⊢ (s ∪ t)⁻¹ = s⁻¹ ∪ t⁻¹

Tactic:
preimage_union

Premises used: Set.preimage_union
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Inv α
s : Set α
⊢ sᶜ⁻¹ = s⁻¹ᶜ

Tactic:
preimage_compl

Premises used: Set.Mem, setOf, Set.preimage_compl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Inv α
inst_1 : Inv β
s : Set α
t : Set β
⊢ (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
a : α
⊢ a⁻¹ ∈ s⁻¹ ↔ a ∈ s

Tactic:
simp only [mem_inv, inv_inv]

Premises used: inv_inv, Set.mem_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
⊢ s⁻¹.Nonempty ↔ s.Nonempty

Tactic:
inv_involutive.surjective.nonempty_preimage

Premises used: Function.Involutive.surjective, inv_involutive, Function.Surjective.nonempty_preimage
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
h : s.Nonempty
⊢ s⁻¹.Nonempty

Tactic:
nonempty_inv.2 h

Premises used: Iff.mpr, Set.nonempty_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
⊢ (fun (x : α) ↦ x⁻¹) '' s = s⁻¹

Tactic:
congr_fun (image_eq_preimage_of_inverse inv_involutive.leftInverse inv_involutive.rightInverse) _

Premises used: Function.Involutive.rightInverse, inv_involutive, Set.image_eq_preimage_of_inverse, congr_fun, Function.Involutive.leftInverse
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
rw : Eq (α := Set α) ((fun (x : α) ↦ x⁻¹) '' s) ∅ ↔ s = ∅
rw₁ rw₂ : s = ∅ ↔ s = ∅
⊢ s⁻¹ = ∅ ↔ s = ∅

Tactic:
rw [← image_inv_eq_inv, image_eq_empty]

Premises used: Set.image_eq_empty, 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 : InvolutiveInv α
s_1 t : Set α
a : α
s : Set α
⊢ s⁻¹⁻¹ = s

Tactic:
simp only [← inv_preimage, preimage_preimage, inv_inv, preimage_id']

Premises used: Set.preimage_preimage, Set.preimage_id', inv_inv, Set.inv_preimage
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s t : Set α
⊢ s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t

Tactic:
(Equiv.inv α).surjective.preimage_subset_preimage_iff

Premises used: Function.Surjective.preimage_subset_preimage_iff, Equiv.inv, Equiv.surjective
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s t : Set α
rw : s⁻¹⁻¹ ⊆ t⁻¹ ↔ s ⊆ t⁻¹
rw₁ rw₂ : s ⊆ t⁻¹ ↔ s ⊆ t⁻¹
⊢ s⁻¹ ⊆ t ↔ s ⊆ t⁻¹

Tactic:
rw [← inv_subset_inv, inv_inv]

Premises used: inv_inv, Set.inv_subset_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
⊢ s⁻¹ = s ↔ s⁻¹ ⊆ s

Tactic:
⟨le_of_eq, fun h => antisymm h <| inv_subset.mp h⟩

Premises used: Iff.intro, antisymm, Iff.mp, Set.inv_subset, le_of_eq
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
a : α
rw : Eq (α := Set α) ((fun (x : α) ↦ x⁻¹) '' {a}) {a⁻¹}
rw₁ rw₂ : Eq (α := Set α) {a⁻¹} {a⁻¹}
⊢ Eq (α := Set α) {a}⁻¹ {a⁻¹}

Tactic:
rw [← image_inv_eq_inv, image_singleton]

Premises used: Set.image_singleton, Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
a : α
s : Set α
rw : ({a} ∪ s)⁻¹ = insert a⁻¹ s⁻¹
rw₁ : {a}⁻¹ ∪ s⁻¹ = insert a⁻¹ s⁻¹
rw₂ : {a⁻¹} ∪ s⁻¹ = insert a⁻¹ s⁻¹
rw₃ rw₄ : {a⁻¹} ∪ s⁻¹ = {a⁻¹} ∪ s⁻¹
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹

Tactic:
rw [insert_eq, union_inv, inv_singleton, insert_eq]

Premises used: Set.insert_eq, Set.union_inv, Set.inv_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
ι : Sort u_5
f : ι → α
rw : Eq (α := Set α) ((fun (x : α) ↦ x⁻¹) '' range f) (range fun (i : ι) ↦ (f i)⁻¹)
⊢ (range f)⁻¹ = range fun (i : ι) ↦ (f i)⁻¹

Tactic:
rw [← image_inv_eq_inv]

Premises used: Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ Eq (α := Set α) ((fun (x : α) ↦ x⁻¹) '' range f) (range fun (i : ι) ↦ (f i)⁻¹)

Tactic:
(range_comp ..).symm

Premises used: Set.range_comp, Eq.symm
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ Eq (α := Set α) ((fun (x : α) ↦ x⁻¹) '' range f) (range fun (i : ι) ↦ (f i)⁻¹)

Tactic:
exact (range_comp ..).symm

Premises used: Set.range_comp, Eq.symm
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
ι : Type u_5
f : ι → α
⊢ (range f)⁻¹ = range f⁻¹

Tactic:
inv_range

Premises used: Set.inv_range
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
rw : (fun (x : α) ↦ f x⁻¹) '' s = g '' s
⊢ f '' s⁻¹ = g '' s

Tactic:
rw [← Set.image_inv_eq_inv, Set.image_image]

Premises used: Set.image_image, Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ (fun (x : α) ↦ f x⁻¹) '' s = g '' s

Tactic:
Set.image_congr H

Premises used: Set.image_congr
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ (fun (x : α) ↦ f x⁻¹) '' s = g '' s

Tactic:
exact Set.image_congr H

Premises used: Set.image_congr
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : InvolutiveInv α
s : Set α
inst_1 : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
rw : f '' s⁻¹
| (g '' s)⁻¹

Tactic:
rw [← image_inv_eq_inv, image_image, ← image_inv_of_apply_inv_eq H]

Premises used: Set.image_image, Set.image_inv_of_apply_inv_eq, Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : InvolutiveInv α
s : Set α
inst_1 : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
conv_rhs : f '' s⁻¹ = (g '' s)⁻¹
conv_rhs₁ : f '' s⁻¹ = f '' s⁻¹
⊢ f '' s⁻¹ = (g '' s)⁻¹

Tactic:
conv_rhs => rw [← image_inv_eq_inv, image_image, ← image_inv_of_apply_inv_eq H]

Premises used: Set.image_image, Set.image_inv_of_apply_inv_eq, Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
p : α → Prop
rw :
  (∀ (a : α), Membership.mem (α := α) s (((Equiv.inv α : (a : α) → α) a)⁻¹ : α) → p ((Equiv.inv α : (a : α) → α) a)) ↔
    ∀ (x : α), x ∈ s → p x⁻¹
⊢ (∀ (x : α), x⁻¹ ∈ s → p x) ↔ ∀ (x : α), x ∈ s → p x⁻¹

Tactic:
rw [← (Equiv.inv _).forall_congr_right]

Premises used: Equiv.inv, Equiv.forall_congr_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∀ (a : α), Membership.mem (α := α) s (((Equiv.inv α : (a : α) → α) a)⁻¹ : α) → p ((Equiv.inv α : (a : α) → α) a)) ↔
    ∀ (x : α), x ∈ s → p x⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
p : α → Prop
rw :
  (∃ (a : α), Membership.mem (α := α) s (((Equiv.inv α : (a : α) → α) a)⁻¹ : α) ∧ p ((Equiv.inv α : (a : α) → α) a)) ↔
    ∃ (x : α), x ∈ s ∧ p x⁻¹
⊢ (∃ (x : α), x⁻¹ ∈ s ∧ p x) ↔ ∃ (x : α), x ∈ s ∧ p x⁻¹

Tactic:
rw [← (Equiv.inv _).exists_congr_right]

Premises used: Equiv.exists_congr_right, Equiv.inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∃ (a : α), Membership.mem (α := α) s (((Equiv.inv α : (a : α) → α) a)⁻¹ : α) ∧ p ((Equiv.inv α : (a : α) → α) a)) ↔
    ∃ (x : α), x ∈ s ∧ p x⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
simp_rw : Eq (α := Set αᵐᵒᵖ) (op '' (fun (x : α) ↦ x⁻¹) '' s) ((fun (x : αᵐᵒᵖ) ↦ x⁻¹) '' op '' s)
⊢ op '' s⁻¹ = (op '' s)⁻¹

Tactic:
simp_rw [← image_inv_eq_inv, Function.Semiconj.set_image op_inv s]

Premises used: Function.Semiconj.set_image, Set.image_inv_eq_inv, MulOpposite.op_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ image2 (fun (x1 x2 : α) ↦ x1 * x2) s t = s * t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
a : α
⊢ a ∈ s * t ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : α), y ∈ t ∧ x * y = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
a b : α
⊢ a ∈ s → b ∈ t → a * b ∈ s * t

Tactic:
mem_image2_of_mem

Premises used: Set.Mem, Set.mem_image2_of_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ (fun (x : α × α) ↦ x.1 * x.2) '' s ×ˢ t = s * t

Tactic:
image_prod _

Premises used: Set.image_prod
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s : Set α
⊢ ∅ * s = ∅

Tactic:
image2_empty_left

Premises used: Set.image2_empty_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s : Set α
⊢ s * ∅ = ∅

Tactic:
image2_empty_right

Premises used: Set.image2_empty_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ s * t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
image2_eq_empty_iff

Premises used: Set.image2_eq_empty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ (s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image2_nonempty_iff

Premises used: Set.image2_nonempty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ s.Nonempty → t.Nonempty → (s * t).Nonempty

Tactic:
Nonempty.image2

Premises used: Set.Nonempty.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ (s * t).Nonempty → s.Nonempty

Tactic:
Nonempty.of_image2_left

Premises used: Set.Nonempty.of_image2_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ (s * t).Nonempty → t.Nonempty

Tactic:
Nonempty.of_image2_right

Premises used: Set.Nonempty.of_image2_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s : Set α
b : α
⊢ s * {b} = (fun (x : α) ↦ x * b) '' s

Tactic:
image2_singleton_right

Premises used: Set.image2_singleton_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
t : Set α
a : α
⊢ {a} * t = (fun (x : α) ↦ a * x) '' t

Tactic:
image2_singleton_left

Premises used: Set.image2_singleton_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
a b : α
⊢ HMul.hMul (α := 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 : Mul α
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 : Mul α
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 : Mul α
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 : Mul α
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 : Mul α
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 : Mul α
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 : Mul α
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 : Mul α
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 : Mul α
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 : Mul α
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 : Mul α
⊢ Eq (α := (a : α) → Set α) (⇑singletonMulHom : (a : α) → Set α) singleton

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
a : α
⊢ Eq (α := Set α) ((singletonMulHom : (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 : Mul α
s t : Set α
⊢ op '' (s * t) = op '' t * op '' s

Tactic:
image_image2_antidistrib op_mul

Premises used: MulOpposite.op_mul, Set.image_image2_antidistrib
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
h : ∀ (x : α × β), x ∈ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ ↔ x ∈ (s₁ * s₂) ×ˢ (t₁ * t₂)
⊢ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x : α × β
h :
  (∃ (a : α), ∃ (b : β), (a ∈ s₁ ∧ b ∈ t₁) ∧ ∃ (a_1 : α), ∃ (b_1 : β), (a_1 ∈ s₂ ∧ b_1 ∈ t₂) ∧ (a * a_1, b * b_1) = x) ↔
    (∃ (x_1 : α), x_1 ∈ s₁ ∧ ∃ (y : α), y ∈ s₂ ∧ x_1 * y = x.1) ∧
      ∃ (x_1 : β), x_1 ∈ t₁ ∧ ∃ (y : β), y ∈ t₂ ∧ x_1 * y = x.2
⊢ x ∈ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ ↔ x ∈ (s₁ * s₂) ×ˢ (t₁ * t₂)

Tactic:
simp [mem_mul]

Premises used: Set.mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x : α × β
⊢ (∃ (a : α), ∃ (b : β), (a ∈ s₁ ∧ b ∈ t₁) ∧ ∃ (a_1 : α), ∃ (b_1 : β), (a_1 ∈ s₂ ∧ b_1 ∈ t₂) ∧ (a * a_1, b * b_1) = x) ↔
    (∃ (x_1 : α), x_1 ∈ s₁ ∧ ∃ (y : α), y ∈ s₂ ∧ x_1 * y = x.1) ∧
      ∃ (x_1 : β), x_1 ∈ t₁ ∧ ∃ (y : β), y ∈ t₂ ∧ x_1 * y = x.2

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t : Set α
⊢ image2 (fun (x1 x2 : α) ↦ x1 / x2) s t = s / t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t : Set α
a : α
⊢ a ∈ s / t ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : α), y ∈ t ∧ x / y = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t : Set α
a b : α
⊢ a ∈ s → b ∈ t → a / b ∈ s / t

Tactic:
mem_image2_of_mem

Premises used: Set.Mem, Set.mem_image2_of_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t : Set α
⊢ (fun (x : α × α) ↦ x.1 / x.2) '' s ×ˢ t = s / t

Tactic:
image_prod _

Premises used: Set.image_prod
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s : Set α
⊢ ∅ / s = ∅

Tactic:
image2_empty_left

Premises used: Set.image2_empty_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s : Set α
⊢ s / ∅ = ∅

Tactic:
image2_empty_right

Premises used: Set.image2_empty_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t : Set α
⊢ s / t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
image2_eq_empty_iff

Premises used: Set.image2_eq_empty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t : Set α
⊢ (s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image2_nonempty_iff

Premises used: Set.image2_nonempty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t : Set α
⊢ s.Nonempty → t.Nonempty → (s / t).Nonempty

Tactic:
Nonempty.image2

Premises used: Set.Nonempty.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t : Set α
⊢ (s / t).Nonempty → s.Nonempty

Tactic:
Nonempty.of_image2_left

Premises used: Set.Nonempty.of_image2_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s t : Set α
⊢ (s / t).Nonempty → t.Nonempty

Tactic:
Nonempty.of_image2_right

Premises used: Set.Nonempty.of_image2_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
s : Set α
b : α
⊢ s / {b} = (fun (x : α) ↦ x / b) '' s

Tactic:
image2_singleton_right

Premises used: Set.image2_singleton_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Div α
t : Set α
a : α
⊢ {a} / t = (fun (x1 x2 : α) ↦ x1 / x2) a '' t

Tactic:
image2_singleton_left

Premises used: Set.image2_singleton_left