awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s₁ s₂ : Set α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s₁ s₂ : Set α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s₁ s₂ : Set α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
t : Set β
a : α
s : Set α
⊢ a ∈ s → a • t ⊆ s • t

Tactic:
image_subset_image2_right

Premises used: Set.image_subset_image2_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
t : Set β
a : α
⊢ (fun (x : β) ↦ a • x) '' t = a • t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
t : Set β
a : α
x : β
⊢ x ∈ a • t ↔ ∃ (y : β), y ∈ t ∧ a • y = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set β
a : α
b : β
⊢ b ∈ s → a • b ∈ a • s

Tactic:
mem_image_of_mem _

Premises used: Set.Mem, Set.mem_image_of_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : α
⊢ HSMul.hSMul (β := Set β) a ∅ = ∅

Tactic:
image_empty _

Premises used: Set.image_empty
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set β
a : α
⊢ a • s = ∅ ↔ s = ∅

Tactic:
image_eq_empty

Premises used: Set.image_eq_empty
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set β
a : α
⊢ (a • s).Nonempty ↔ s.Nonempty

Tactic:
image_nonempty

Premises used: Set.image_nonempty
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : α
b : β
⊢ HSMul.hSMul (β := Set β) a {b} = {a • b}

Tactic:
image_singleton

Premises used: Set.image_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s t : Set β
a : α
⊢ s ⊆ t → a • s ⊆ a • t

Tactic:
image_mono

Premises used: Set.image_mono
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s t : Set β
a : α
⊢ a • s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a • b ∈ t

Tactic:
image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image_subset_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
t₁ t₂ : Set β
a : α
⊢ a • (t₁ ∪ t₂) = a • t₁ ∪ a • t₂

Tactic:
image_union ..

Premises used: Set.image_union
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : α
b : β
s : Set β
⊢ a • insert b s = insert (a • b) (a • s)

Tactic:
image_insert_eq ..

Premises used: Set.image_insert_eq
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
t₁ t₂ : Set β
a : α
⊢ a • (t₁ ∩ t₂) ⊆ a • t₁ ∩ a • t₂

Tactic:
image_inter_subset ..

Premises used: Set.image_inter_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set β
a : α
⊢ s.Nonempty → (a • s).Nonempty

Tactic:
Nonempty.image _

Premises used: Set.Nonempty.image
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
M : Type u_5
ι : Type u_6
π : ι → Type u_7
inst : (i : ι) → SMul.{u_5, u_7} M (π i)
c : M
I : Set ι
s : (i : ι) → Set (π i)
hsurj : ∀ (i : ι), ¬i ∈ I → Surjective (β := π i) fun (x : π i) ↦ c • x
⊢ c • I.pi (α := π) s = I.pi (α := π) (c • s)

Tactic:
piMap_image_pi hsurj s

Premises used: Pi.map, Set.piMap_image_pi
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
M : Type u_5
ι : Type u_6
π : ι → Type u_7
inst : (i : ι) → SMul.{u_5, u_7} M (π i)
c : M
s : (i : ι) → Set (π i)
⊢ c • pi (α := π) univ s = pi (α := π) univ (c • s)

Tactic:
piMap_image_univ_pi _ s

Premises used: Set.piMap_image_univ_pi, Pi.map
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
ι : Type u_5
κ : Type u_6
inst : SMul α β
b : ι → α
c : κ → β
⊢ range b • range c = range fun (p : ι × κ) ↦ b p.1 • c p.2

Tactic:
image2_range ..

Premises used: Set.image2_range
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
ι : Sort u_5
a : α
f : ι → β
⊢ a • range f = range fun (i : ι) ↦ a • f i

Tactic:
(range_comp ..).symm

Premises used: Set.range_comp, Eq.symm
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
ι : Sort u_5
a : α
f : ι → β
⊢ (range fun (i : ι) ↦ a • f i) = a • range f

Tactic:
(smul_set_range ..).symm

Premises used: Set.smul_set_range, Eq.symm
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s t : Set β
⊢ image2 (fun (x1 x2 : β) ↦ x1 -ᵥ x2) s t = s -ᵥ t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s t : Set β
b c : β
hb : b ∈ s
hc : c ∈ t
⊢ b -ᵥ c ∈ s -ᵥ t

Tactic:
mem_image2_of_mem hb hc

Premises used: Set.Mem, Set.mem_image2_of_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
t : Set β
⊢ ∅ -ᵥ t = ∅

Tactic:
image2_empty_left

Premises used: Set.image2_empty_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s : Set β
⊢ s -ᵥ ∅ = ∅

Tactic:
image2_empty_right

Premises used: Set.image2_empty_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s t : Set β
⊢ s.Nonempty → t.Nonempty → (s -ᵥ t).Nonempty

Tactic:
.image2

Premises used: Set.Nonempty.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s t : Set β
⊢ (s -ᵥ t).Nonempty → s.Nonempty

Tactic:
.of_image2_left

Premises used: Set.Nonempty.of_image2_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s t : Set β
⊢ (s -ᵥ t).Nonempty → t.Nonempty

Tactic:
.of_image2_right

Premises used: Set.Nonempty.of_image2_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
t : Set β
b : β
⊢ {b} -ᵥ t = (fun (x : β) ↦ b -ᵥ x) '' t

Tactic:
image2_singleton_left

Premises used: Set.image2_singleton_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
b c : β
⊢ VSub.vsub (P := Set β) {b} {c} = {b -ᵥ c}

Tactic:
image2_singleton

Premises used: Set.image2_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s₁ s₂ t₁ t₂ : Set β
⊢ s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂

Tactic:
image2_subset

Premises used: Set.image2_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s t : Set β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s t : Set β
h : s ⊆ t
⊢ s -ᵥ s ⊆ t -ᵥ t

Tactic:
vsub_subset_vsub h h

Premises used: Set.vsub_subset_vsub
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul α β
inst_1 : SMul α γ
f : β → γ
a : α
s : Set β
⊢ (∀ (b : β), f (a • b) = a • f b) → f '' (a • s) = a • f '' s

Tactic:
image_comm

Premises used: Set.image_comm
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul.{u_2, u_3} αᵐᵒᵖ β
inst_1 : SMul β γ
inst_2 : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
h₁ : ∀ (x : γ), x ∈ (op a • s) • t ↔ x ∈ s • a • t
⊢ (op a • s) • t = s • a • t

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul.{u_2, u_3} αᵐᵒᵖ β
inst_1 : SMul β γ
inst_2 : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
x : γ
⊢ x ∈ (op a • s) • t ↔ x ∈ s • a • t

Tactic:
simp [mem_smul, mem_smul_set, h]

Premises used: Set.mem_smul, Set.mem_smul_set
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Small
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Zero α
⊢ Small.{u, u_1} (↑0 : Type u_1)

Tactic:
small_single _

Premises used: small_single
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Small
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : One α
⊢ Small.{u, u_1} (↑1 : Type u_1)

Tactic:
small_single _

Premises used: small_single
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Small
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : InvolutiveNeg α
inst_1 : Small.{u, u_1} (↑s : Type u_1)
rw : Small.{u, u_1} (↑((fun (x : α) ↦ -x) '' s) : Type u_1)
⊢ Small.{u, u_1} (↑(-s) : Type u_1)

Tactic:
rw [← Set.image_neg_eq_neg]

Premises used: Set.image_neg_eq_neg
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Small
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : InvolutiveNeg α
inst_1 : Small.{u, u_1} (↑s : Type u_1)
⊢ Small.{u, u_1} (↑((fun (x : α) ↦ -x) '' s) : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Small
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Add α
inst_1 : Small.{u, u_1} (↑s : Type u_1)
inst_2 : Small.{u, u_1} (↑t : Type u_1)
⊢ Small.{u, u_1} (↑(s + t) : Type u_1)

Tactic:
small_image2 ..

Premises used: small_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Small
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Sub α
inst_1 : Small.{u, u_1} (↑s : Type u_1)
inst_2 : Small.{u, u_1} (↑t : Type u_1)
⊢ Small.{u, u_1} (↑(s - t) : Type u_1)

Tactic:
small_image2 ..

Premises used: small_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Small
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Mul α
inst_1 : Small.{u, u_1} (↑s : Type u_1)
inst_2 : Small.{u, u_1} (↑t : Type u_1)
⊢ Small.{u, u_1} (↑(s * t) : Type u_1)

Tactic:
small_image2 ..

Premises used: small_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Small
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Div α
inst_1 : Small.{u, u_1} (↑s : Type u_1)
inst_2 : Small.{u, u_1} (↑t : Type u_1)
⊢ Small.{u, u_1} (↑(s / t) : Type u_1)

Tactic:
small_image2 ..

Premises used: small_image2
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : Mul N
b₁ b₂ : N
rw : (HMul.hMul (α := M) 1 1, b₁ * b₂) = (1, b₁ * b₂)
rw₁ rw₂ : Eq (α := M × N) (1, b₁ * b₂) (1, b₁ * b₂)
⊢ HMul.hMul (α := M × N) (1, b₁) (1, b₂) = (1, b₁ * b₂)

Tactic:
rw [mk_mul_mk, mul_one]

Premises used: Prod.mk_mul_mk, mul_one
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : Mul M
inst_1 : MulOneClass N
a₁ a₂ : M
rw : (a₁ * a₂, HMul.hMul (α := N) 1 1) = (a₁ * a₂, 1)
rw₁ rw₂ : Eq (α := M × N) (a₁ * a₂, 1) (a₁ * a₂, 1)
⊢ HMul.hMul (α := M × N) (a₁, 1) (a₂, 1) = (a₁ * a₂, 1)

Tactic:
rw [mk_mul_mk, mul_one]

Premises used: Prod.mk_mul_mk, mul_one
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
p : M × N
⊢ (p.1, 1) * (1, p.2) = p

Tactic:
Prod.ext (mul_one p.1) (one_mul p.2)

Premises used: Prod.fst, Prod.ext, mul_one, Prod.snd, one_mul
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Semigroup M
inst_1 : Semigroup N
x x_1 x_2 : M × N
fst : (x * x_1 * x_2).1 = (x * (x_1 * x_2)).1
snd : (x * x_1 * x_2).2 = (x * (x_1 * x_2)).2
⊢ x * x_1 * x_2 = x * (x_1 * x_2)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Semigroup M
inst_1 : Semigroup N
x x_1 x_2 : M × N
⊢ (x * x_1 * x_2).1 = (x * (x_1 * x_2)).1

Tactic:
mul_assoc ..

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Semigroup M
inst_1 : Semigroup N
x x_1 x_2 : M × N
⊢ (x * x_1 * x_2).1 = (x * (x_1 * x_2)).1

Tactic:
exact mul_assoc ..

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Semigroup M
inst_1 : Semigroup N
x x_1 x_2 : M × N
⊢ (x * x_1 * x_2).2 = (x * (x_1 * x_2)).2

Tactic:
mul_assoc ..

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Semigroup M
inst_1 : Semigroup N
x x_1 x_2 : M × N
⊢ (x * x_1 * x_2).2 = (x * (x_1 * x_2)).2

Tactic:
exact mul_assoc ..

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemigroup G
inst_1 : CommSemigroup H
x x_1 : G × H
fst : (x * x_1).1 = (x_1 * x).1
snd : (x * x_1).2 = (x_1 * x).2
⊢ x * x_1 = x_1 * x

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemigroup G
inst_1 : CommSemigroup H
x x_1 : G × H
⊢ (x * x_1).1 = (x_1 * x).1

Tactic:
mul_comm ..

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemigroup G
inst_1 : CommSemigroup H
x x_1 : G × H
⊢ (x * x_1).1 = (x_1 * x).1

Tactic:
exact mul_comm ..

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemigroup G
inst_1 : CommSemigroup H
x x_1 : G × H
⊢ (x * x_1).2 = (x_1 * x).2

Tactic:
mul_comm ..

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemigroup G
inst_1 : CommSemigroup H
x x_1 : G × H
⊢ (x * x_1).2 = (x_1 * x).2

Tactic:
exact mul_comm ..

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
fst : (1 * x).1 = x.1
snd : (1 * x).2 = x.2
⊢ 1 * x = x

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
⊢ (1 * x).1 = x.1

Tactic:
one_mul _

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
⊢ (1 * x).1 = x.1

Tactic:
exact one_mul _

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
⊢ (1 * x).2 = x.2

Tactic:
one_mul _

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
⊢ (1 * x).2 = x.2

Tactic:
exact one_mul _

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
fst : (x * 1).1 = x.1
snd : (x * 1).2 = x.2
⊢ x * 1 = x

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
⊢ (x * 1).1 = x.1

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
⊢ (x * 1).1 = x.1

Tactic:
exact mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
⊢ (x * 1).2 = x.2

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
⊢ (x * 1).2 = x.2

Tactic:
exact mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
⊢ ∀ (a : M × N), 1 * a = a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
⊢ ∀ (a : M × N), a * 1 = a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree M
inst_3 : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : Eq (α := M × N) ((fun (a : M × N) ↦ a ^ n) a) ((fun (a : M × N) ↦ a ^ n) b)
fst : a.1 = b.1
snd : a.2 = b.2
⊢ a = b

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree M
inst_3 : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : Eq (α := M × N) ((fun (a : M × N) ↦ a ^ n) a) ((fun (a : M × N) ↦ a ^ n) b)
fst : Eq.{u_3 + 1} (α := M) ((fun (a : M) ↦ a ^ n) a.1) ((fun (a : M) ↦ a ^ n) b.1)
⊢ a.1 = b.1

Tactic:
apply pow_left_injective hn

Premises used: pow_left_injective
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree M
inst_3 : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : Eq (α := M × N) ((fun (a : M × N) ↦ a ^ n) a) ((fun (a : M × N) ↦ a ^ n) b)
snd : Eq.{u_4 + 1} (α := N) ((fun (a : N) ↦ a ^ n) a.2) ((fun (a : N) ↦ a ^ n) b.2)
⊢ a.2 = b.2

Tactic:
apply pow_left_injective hn

Premises used: pow_left_injective
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree M
inst_3 : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : Eq (α := M × N) ((fun (a : M × N) ↦ a ^ n) a) ((fun (a : M × N) ↦ a ^ n) b)
⊢ Eq.{u_3 + 1} (α := M) ((fun (a : M) ↦ a ^ n) a.1) ((fun (a : M) ↦ a ^ n) b.1)

Tactic:
congr(($hab).1)

Premises used: congrArg, id, Prod.fst
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree M
inst_3 : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : Eq (α := M × N) ((fun (a : M × N) ↦ a ^ n) a) ((fun (a : M × N) ↦ a ^ n) b)
⊢ Eq.{u_4 + 1} (α := N) ((fun (a : N) ↦ a ^ n) a.2) ((fun (a : N) ↦ a ^ n) b.2)

Tactic:
congr(($hab).2)

Premises used: congrArg, id, Prod.snd
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree M
inst_3 : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : Eq (α := M × N) ((fun (a : M × N) ↦ a ^ n) a) ((fun (a : M × N) ↦ a ^ n) b)
⊢ Eq.{u_3 + 1} (α := M) ((fun (a : M) ↦ a ^ n) a.1) ((fun (a : M) ↦ a ^ n) b.1)

Tactic:
exacts [congr(($hab).1), congr(($hab).2)]
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x x_1 : G × H
fst : (x / x_1).1 = (x * x_1⁻¹).1
snd : (x / x_1).2 = (x * x_1⁻¹).2
⊢ x / x_1 = x * x_1⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x x_1 : G × H
⊢ (x / x_1).1 = (x * x_1⁻¹).1

Tactic:
div_eq_mul_inv ..

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x x_1 : G × H
⊢ (x / x_1).1 = (x * x_1⁻¹).1

Tactic:
exact div_eq_mul_inv ..

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x x_1 : G × H
⊢ (x / x_1).2 = (x * x_1⁻¹).2

Tactic:
div_eq_mul_inv ..

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x x_1 : G × H
⊢ (x / x_1).2 = (x * x_1⁻¹).2

Tactic:
exact div_eq_mul_inv ..

Premises used: div_eq_mul_inv