awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.TypeTags.Pointwise
Goal:
M : Type u_1
inst : AddMonoid M
s t : Set M
rw :
  Set.image (α := M) (⇑ofAdd : (a : M) → Multiplicative M) (Set.image2 (fun (x1 x2 : M) ↦ x1 + x2) s t) =
    HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
rw₁ :
  Set.image2 (α := Multiplicative M) (β := Multiplicative M) HMul.hMul ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t) =
    HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
rw₂ rw₃ :
  HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t) =
    HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
⊢ (⇑ofAdd : (a : M) → Multiplicative M) '' (s + t) =
    HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t)

Tactic:
rw [← Set.image2_add, Set.image_image2_distrib ofAdd_add, Set.image2_mul]

Premises used: ofAdd_add, Set.image2_mul, Set.image_image2_distrib, Set.image2_add
-- Module: Mathlib.Algebra.Group.TypeTags.Pointwise
Goal:
M : Type u_1
inst : AddMonoid M
s : Set M
zero : Eq (α := Set (Multiplicative M)) {1} 1
⊢ (⇑ofAdd : (a : M) → Multiplicative M) '' HSMul.hSMul (α := ℕ) 0 s =
    HPow.hPow (α := Set (Multiplicative M)) (β := ℕ) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.TypeTags.Pointwise
Goal:
M : Type u_1
inst : AddMonoid M
s : Set M
⊢ Eq (α := Set (Multiplicative M)) {1} 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Pointwise
Goal:
M : Type u_1
inst : AddMonoid M
s : Set M
n : ℕ
IH :
  (⇑ofAdd : (a : M) → Multiplicative M) '' (n • s) =
    HPow.hPow (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) n
⊢ (⇑ofAdd : (a : M) → Multiplicative M) '' ((n + 1) • s) =
    HPow.hPow (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) (n + 1)

Tactic:
simp [succ_nsmul, pow_succ, IH]

Premises used: pow_succ, succ_nsmul
-- Module: Mathlib.Algebra.Group.TypeTags.Pointwise
Goal:
M : Type u_1
inst : AddMonoid M
n : ℕ
s : Set M
zero :
  (⇑ofAdd : (a : M) → Multiplicative M) '' HSMul.hSMul (α := ℕ) 0 s =
    HPow.hPow (α := Set (Multiplicative M)) (β := ℕ) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) 0
succ :
  ∀ (n : ℕ)
    (IH :
      (⇑ofAdd : (a : M) → Multiplicative M) '' (n • s) =
        HPow.hPow (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) n),
    (⇑ofAdd : (a : M) → Multiplicative M) '' ((n + 1) • s) =
      HPow.hPow (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) (n + 1)
⊢ (⇑ofAdd : (a : M) → Multiplicative M) '' (n • s) =
    HPow.hPow (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) n

Tactic:
induction n with
  | zero => simp; rfl
  | succ n IH => simp [succ_nsmul, pow_succ, IH]

Premises used: pow_succ, succ_nsmul
-- Module: Mathlib.Algebra.Group.TypeTags.Pointwise
Goal:
M : Type u_1
inst : AddMonoid M
s t : Set (Multiplicative M)
rw :
  Set.image (α := Multiplicative M) (⇑toAdd : (a : Multiplicative M) → M)
      (Set.image2 (fun (x1 x2 : Multiplicative M) ↦ x1 * x2) s t) =
    HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
rw₁ :
  Set.image2 (α := M) (β := M) HAdd.hAdd ((⇑toAdd : (a : Multiplicative M) → M) '' s)
      ((⇑toAdd : (a : Multiplicative M) → M) '' t) =
    HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
rw₂ rw₃ :
  HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t) =
    HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
⊢ (⇑toAdd : (a : Multiplicative M) → M) '' (s * t) =
    HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)

Tactic:
rw [← Set.image2_mul, Set.image_image2_distrib toAdd_mul, Set.image2_add]

Premises used: toAdd_mul, Set.image2_mul, Set.image_image2_distrib, Set.image2_add
-- Module: Mathlib.Algebra.Group.TypeTags.Pointwise
Goal:
M : Type u_1
inst : AddMonoid M
s : Set (Multiplicative M)
zero : Eq (α := Set M) {0} 0
⊢ (⇑toAdd : (a : Multiplicative M) → M) '' HPow.hPow (β := ℕ) s 0 =
    HSMul.hSMul (α := ℕ) (β := Set M) 0 ((⇑toAdd : (a : Multiplicative M) → M) '' s)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.TypeTags.Pointwise
Goal:
M : Type u_1
inst : AddMonoid M
s : Set (Multiplicative M)
⊢ Eq (α := Set M) {0} 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Pointwise
Goal:
M : Type u_1
inst : AddMonoid M
s : Set (Multiplicative M)
n : ℕ
IH :
  (⇑toAdd : (a : Multiplicative M) → M) '' s ^ n =
    HSMul.hSMul (β := Set M) n ((⇑toAdd : (a : Multiplicative M) → M) '' s)
⊢ (⇑toAdd : (a : Multiplicative M) → M) '' s ^ (n + 1) =
    HSMul.hSMul (β := Set M) (n + 1) ((⇑toAdd : (a : Multiplicative M) → M) '' s)

Tactic:
simp [succ_nsmul, pow_succ, IH]

Premises used: pow_succ, succ_nsmul
-- Module: Mathlib.Algebra.Group.TypeTags.Pointwise
Goal:
M : Type u_1
inst : AddMonoid M
n : ℕ
s : Set (Multiplicative M)
zero :
  (⇑toAdd : (a : Multiplicative M) → M) '' HPow.hPow (β := ℕ) s 0 =
    HSMul.hSMul (α := ℕ) (β := Set M) 0 ((⇑toAdd : (a : Multiplicative M) → M) '' s)
succ :
  ∀ (n : ℕ)
    (IH :
      (⇑toAdd : (a : Multiplicative M) → M) '' s ^ n =
        HSMul.hSMul (β := Set M) n ((⇑toAdd : (a : Multiplicative M) → M) '' s)),
    (⇑toAdd : (a : Multiplicative M) → M) '' s ^ (n + 1) =
      HSMul.hSMul (β := Set M) (n + 1) ((⇑toAdd : (a : Multiplicative M) → M) '' s)
⊢ (⇑toAdd : (a : Multiplicative M) → M) '' s ^ n =
    HSMul.hSMul (β := Set M) n ((⇑toAdd : (a : Multiplicative M) → M) '' s)

Tactic:
induction n with
  | zero => simp; rfl
  | succ n IH => simp [succ_nsmul, pow_succ, IH]

Premises used: pow_succ, succ_nsmul
-- Module: Mathlib.Algebra.Group.ULift
Goal:
α : Type u
inst : One α
⊢ Eq.{u + 1} (α := α) (down.{u_1, u} 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.ULift
Goal:
α : Type u
x y : ULift.{w, u} α
inst : Mul α
⊢ down.{w, u} (x * y) = x.down * y.down

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.ULift
Goal:
α : Type u
x y : ULift.{w, u} α
inst : Div α
⊢ down.{w, u} (x / y) = x.down / y.down

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.ULift
Goal:
α : Type u
x : ULift.{w, u} α
inst : Inv α
⊢ down.{w, u} x⁻¹ = x.down⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.ULift
Goal:
α : Type u
β : Type v
inst : Pow α β
a : ULift.{w, u} α
b : β
⊢ down.{w, u} (a ^ b) = a.down ^ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.ULift
Goal:
α : Type u
β : Type v
x y : ULift.{w, u} α
inst : MulOneClass α
x_1 y_1 : ULift.{u_1, u} α
⊢ (Equiv.ulift : (a : ULift α) → α) (x_1 * y_1) =
    HMul.hMul (α := α) (β := α) ((Equiv.ulift : (a : ULift α) → α) x_1 : α) ((Equiv.ulift : (a : ULift α) → α) y_1 : α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.ULift
Goal:
α : Type u
β : Type v
x y : ULift.{w, u} α
inst : Nontrivial α
⊢ Nontrivial (ULift.{u_1, u} α)

Tactic:
Equiv.ulift.symm.injective.nontrivial

Premises used: Function.Injective.nontrivial, Equiv.ulift, Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
A' B' : Finset G
hA : A ⊆ A'
hB : B ⊆ B'
h : UniqueMul A' B' a0 b0
⊢ UniqueMul A B a0 b0

Tactic:
fun _ _ ha hb he ↦ h (hA ha) (hB hb) he

Premises used: UniqueMul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : Subsingleton G
⊢ UniqueMul A B a0 b0

Tactic:
simp [UniqueMul, eq_iff_true_of_subsingleton]

Premises used: UniqueMul, eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : #A ≤ 1
hB1 : #B ≤ 1
⊢ ∀ {a b : G}, a ∈ A → b ∈ A → a = b

Tactic:
rw [Finset.card_le_one_iff] at hA1 hB1

Premises used: Finset.card_le_one_iff
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : #A ≤ 1
hB1 : #B ≤ 1
hA1₁ : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
⊢ ∀ {a b : G}, a ∈ B → b ∈ B → a = b

Tactic:
rw [Finset.card_le_one_iff] at hA1 hB1

Premises used: Finset.card_le_one_iff
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
obtain : ∀ (a : G) (ha : a ∈ A), ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
obtain ⟨a, ha⟩ := hA
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
obtain : ∀ (b : G) (hb : b ∈ B), ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
obtain ⟨b, hb⟩ := hB
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
b : G
hb : b ∈ B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
⟨a, ha, b, hb, fun _ _ ha' hb' _ ↦ ⟨hA1 ha' ha, hB1 hb' hb⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
b : G
hb : b ∈ B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
exact ⟨a, ha, b, hb, fun _ _ ha' hb' _ ↦ ⟨hA1 ha' ha, hB1 hb' hb⟩⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x x_1 : G
ha : x ∈ A
hb : x_1 ∈ B
k : x ≠ a0 ∨ x_1 ≠ b0
contrapose! : ∀ (k : x * x_1 = a0 * b0), x = a0 ∧ x_1 = b0
⊢ x * x_1 ≠ a0 * b0

Tactic:
contrapose! k
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x x_1 : G
ha : x ∈ A
hb : x_1 ∈ B
k : x * x_1 = a0 * b0
⊢ x = a0 ∧ x_1 = b0

Tactic:
h ha hb k
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x x_1 : G
ha : x ∈ A
hb : x_1 ∈ B
k : x * x_1 = a0 * b0
⊢ x = a0 ∧ x_1 = b0

Tactic:
exact h ha hb k
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ Subsingleton.{max 1 (u_1 + 1)} { ab : G × G // ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0 }

Tactic:
⟨fun ⟨⟨_a, _b⟩, ha, hb, ab⟩ ⟨⟨_a', _b'⟩, ha', hb', ab'⟩ ↦
    Subtype.ext <|
      Prod.ext ((h ha hb ab).1.trans (h ha' hb' ab').1.symm) <|
        (h ha hb ab).2.trans (h ha' hb' ab').2.symm⟩

Premises used: Prod.mk, Subtype.mk, Subsingleton.intro, And.right, And.left, _private.0.UniqueMul.subsingleton.match_1, Prod.ext, And.intro, Eq.symm, Eq, Eq.trans, Subtype.ext
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x1 y1 : G
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0
x2 y2 : G
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0
⊢ UniqueMul A B x1 y1

Tactic:
rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩

Premises used: And.right, And.left, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x1 y1 : G
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0
x2 y2 : G
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0
h₁ : UniqueMul A B x1 y1
⊢ x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = x1 * y1

Tactic:
rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩

Premises used: And.right, And.left, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x1 y1 : G
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0
x2 y2 : G
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0
h₁ : UniqueMul A B x1 y1
hx₁ : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = x1 * y1
⊢ x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x1 * y1

Tactic:
rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩

Premises used: And.right, And.left, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
x1 y1 x2 y2 : G
h : UniqueMul A B x1 y1
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = x1 * y1
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x1 * y1
rcases : ∀ (h : UniqueMul A B x2 y2) (hx hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x2 * y2), (x2, y2) = (x2, y2)
⊢ (x1, y1) = (x2, y2)

Tactic:
rcases h hy.1 hy.2.1 hy.2.2 with ⟨rfl, rfl⟩

Premises used: And.right, And.left, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
x2 y2 : G
h : UniqueMul A B x2 y2
hx hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x2 * y2
⊢ (x2, y2) = (x2, y2)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : UniqueMul A B a0 b0
⊢ ∀ (y : G × G), (fun (ab : G × G) ↦ ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0) y → y = (a0, b0)

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x1 x2 : G
h_1 : (x1, x2) ∈ A ×ˢ B ∧ (x1, x2).1 * (x1, x2).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
⊢ (a0, b0) ∈ A ×ˢ B ∧ (a0, b0).1 * (a0, b0).2 = a0 * b0

Tactic:
rcases Prod.mk_inj.mp (J (a0, b0) ⟨Finset.mk_mem_product aA bB, rfl⟩) with ⟨rfl, rfl⟩

Premises used: Prod.mk_inj, Finset.mk_mem_product, Prod.mk, And.intro, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x1 x2 : G
h_1 : (x1, x2) ∈ A ×ˢ B ∧ (x1, x2).1 * (x1, x2).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
a : (a0, b0) ∈ A ×ˢ B ∧ (a0, b0).1 * (a0, b0).2 = a0 * b0
⊢ ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (a0, b0)

Tactic:
rcases Prod.mk_inj.mp (J (a0, b0) ⟨Finset.mk_mem_product aA bB, rfl⟩) with ⟨rfl, rfl⟩

Premises used: Prod.mk_inj, Finset.mk_mem_product, Prod.mk, And.intro, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
h_1 : (a0, b0) ∈ A ×ˢ B ∧ (a0, b0).1 * (a0, b0).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (a0, b0)
⊢ x = a0 ∧ y = b0

Tactic:
Prod.mk_inj.mp (J (x, y) ⟨Finset.mk_mem_product hx hy, l⟩)

Premises used: Prod.mk_inj, Finset.mk_mem_product, Prod.mk, And.intro, Iff.mp
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
h_1 : (a0, b0) ∈ A ×ˢ B ∧ (a0, b0).1 * (a0, b0).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (a0, b0)
⊢ x = a0 ∧ y = b0

Tactic:
exact Prod.mk_inj.mp (J (x, y) ⟨Finset.mk_mem_product hx hy, l⟩)

Premises used: Prod.mk_inj, Finset.mk_mem_product, Prod.mk, And.intro, Iff.mp
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
simp_rw :
  UniqueMul A B a0 b0 ↔
    ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
⊢ UniqueMul A B a0 b0 ↔ #({p ∈ A ×ˢ B | p.1 * p.2 = a0 * b0}) ≤ 1

Tactic:
simp_rw [card_le_one_iff, mem_filter, mem_product]

Premises used: Finset.card_le_one_iff, Finset.mem_filter, Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
⊢ UniqueMul A B a0 b0 ↔
    ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b

Tactic:
⟨fun h p1 p2 ⟨⟨ha1, hb1⟩, he1⟩ ⟨⟨ha2, hb2⟩, he2⟩ ↦ ?_, fun h a b ha hb he ↦ ?_⟩

Premises used: _private.0.UniqueMul.iff_card_le_one.match_3, Iff.intro, Eq
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
refine_1 :
  ∀ (h : UniqueMul A B a0 b0) (p1 p2 : G × G),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0 →
      (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0 →
        ∀ (ha1 : p1.1 ∈ A) (hb1 : p1.2 ∈ B) (he1 : p1.1 * p1.2 = a0 * b0) (ha2 : p2.1 ∈ A) (hb2 : p2.2 ∈ B)
          (he2 : p2.1 * p2.2 = a0 * b0), p1 = p2
refine_2 :
  ∀ (h : ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b)
    (a b : G) (ha : a ∈ A) (hb : b ∈ B) (he : a * b = a0 * b0), a = a0 ∧ b = b0
⊢ UniqueMul A B a0 b0 ↔
    ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b

Tactic:
refine ⟨fun h p1 p2 ⟨⟨ha1, hb1⟩, he1⟩ ⟨⟨ha2, hb2⟩, he2⟩ ↦ ?_, fun h a b ha hb he ↦ ?_⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
h_1 : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
h_2 : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
⊢ p1.1 = a0 ∧ p1.2 = b0

Tactic:
have h1 := h ha1 hb1 he1
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
h_1 : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
h_2 : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
h1 : p1.1 = a0 ∧ p1.2 = b0
⊢ p2.1 = a0 ∧ p2.2 = b0

Tactic:
have h2 := h ha2 hb2 he2
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
h_1 : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
h_2 : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
h1 : p1.1 = a0 ∧ p1.2 = b0
h2 : p2.1 = a0 ∧ p2.2 = b0
⊢ p1 = p2

Tactic:
grind
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
Prod.ext_iff.1 (@h (a, b) (a0, b0) ⟨⟨ha, hb⟩, he⟩ ⟨⟨ha0, hb0⟩, rfl⟩)

Premises used: Prod.ext_iff, And.intro, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
exact Prod.ext_iff.1 (@h (a, b) (a0, b0) ⟨⟨ha, hb⟩, he⟩ ⟨⟨ha0, hb0⟩, rfl⟩)

Premises used: Prod.ext_iff, And.intro, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h_1 : ∃ (g : G), ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
g : G
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
⊢ ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g

Tactic:
have h' := h
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h_1 : ∃ (g : G), ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
g : G
h h' : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
rcases :
  ∀ (a b : G) (hab : (a, b) ∈ A ×ˢ B) (h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2),
    ∃ (a0 : G) (b0 : G), a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
⊢ ∃ (a0 : G) (b0 : G), a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Tactic:
rcases h' with ⟨⟨a, b⟩, ⟨hab, rfl, -⟩, -⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h_1 : ∃ (g : G), ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
⊢ (a, b).1 ∈ A

Tactic:
obtain ⟨ha, hb⟩ := Finset.mem_product.mp hab

Premises used: Iff.mp, Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h_1 : ∃ (g : G), ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
ha : (a, b).1 ∈ A
⊢ (a, b).2 ∈ B

Tactic:
obtain ⟨ha, hb⟩ := Finset.mem_product.mp hab

Premises used: Iff.mp, Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h_1 : ∃ (g : G), ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
ha : (a, b).1 ∈ A
hb : (a, b).2 ∈ B
⊢ ∃ (a0 : G) (b0 : G), a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Tactic:
⟨a, b, ha, hb, (iff_existsUnique ha hb).mpr h⟩

Premises used: Iff.mpr, UniqueMul.iff_existsUnique, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h_1 : ∃ (g : G), ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
ha : (a, b).1 ∈ A
hb : (a, b).2 ∈ B
⊢ ∃ (a0 : G) (b0 : G), a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Tactic:
exact ⟨a, b, ha, hb, (iff_existsUnique ha hb).mpr h⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
f : G →ₙ* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
a0 b0 : G
A B : Finset H
u : UniqueMul A B ((f : (a : G) → H) a0) ((f : (a : G) → H) b0)
a b : G
ha : a ∈ A.preimage (⇑f : (a : G) → H) ⋯
hb : b ∈ B.preimage (⇑f : (a : G) → H) ⋯
ab : a * b = a0 * b0
simp :
  ∀
    (ab :
      HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b : H) =
        HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H)),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) a0 : H) ∧
      Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) b : H) ((f : (a : G) → H) b0 : H)
⊢ a = a0 ∧ b = b0

Tactic:
simp only [← hf.eq_iff, map_mul] at ab ⊢

Premises used: Function.Injective.eq_iff, map_mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
f : G →ₙ* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
a0 b0 : G
A B : Finset H
u : UniqueMul A B ((f : (a : G) → H) a0) ((f : (a : G) → H) b0)
a b : G
ha : a ∈ A.preimage (⇑f : (a : G) → H) ⋯
hb : b ∈ B.preimage (⇑f : (a : G) → H) ⋯
ab :
  HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b : H) =
    HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H)
⊢ Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) a0 : H) ∧
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) b : H) ((f : (a : G) → H) b0 : H)

Tactic:
u (Finset.mem_preimage.mp ha) (Finset.mem_preimage.mp hb) ab

Premises used: Finset.mem_preimage, Iff.mp