awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact u (Finset.mem_preimage.mp ha) (Finset.mem_preimage.mp hb) ab

Premises used: Finset.mem_preimage, Iff.mp
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
inst_2 : DecidableEq H
f : G →ₙ* H
hf :
  ∀ ⦃a b c d : G⦄,
    a * b = c * d →
      Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) c : H) ∧
          Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) b : H) ((f : (a : G) → H) d : H) →
        a = c ∧ b = d
h :
  UniqueMul.{u_2} (G := H) (image (⇑f : (a : G) → H) A : Finset H) (image (⇑f : (a : G) → H) B : Finset H)
    ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
simp_rw : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) (a * b) : H) ((f : (a : G) → H) (a0 * b0) : H)
⊢ 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)

Tactic:
simp_rw [← map_mul, ab]

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
inst_2 : DecidableEq H
f : G →ₙ* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h : UniqueMul A B a0 b0
x x_1 : H
simp_rw :
  (∃ a ∈ A, (f : (a : G) → H) a = x) →
    (∃ a ∈ B, (f : (a : G) → H) a = x_1) →
      x * x_1 = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H) →
        x = (f : (a : G) → H) a0 ∧ x_1 = (f : (a : G) → H) b0
⊢ Membership.mem (γ := Finset H) (image (⇑f : (a : G) → H) A) x →
    Membership.mem (γ := Finset H) (image (⇑f : (a : G) → H) B) x_1 →
      x * x_1 = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H) →
        x = (f : (a : G) → H) a0 ∧ x_1 = (f : (a : G) → H) b0

Tactic:
simp_rw [Finset.mem_image]

Premises used: Finset.mem_image
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
inst_2 : DecidableEq H
f : G →ₙ* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h : UniqueMul A B a0 b0
a : G
aA : a ∈ A
b : G
bB : b ∈ B
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)
simp_rw : ∀ (ab : a * b = a0 * b0), a = a0 ∧ b = b0
⊢ 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:
simp_rw [← map_mul, hf.eq_iff] 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
A B : Finset G
a0 b0 : G
inst_2 : DecidableEq H
f : G →ₙ* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h : UniqueMul A B a0 b0
a : G
aA : a ∈ A
b : G
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
h aA bB ab
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
inst_2 : DecidableEq H
f : G →ₙ* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h : UniqueMul A B a0 b0
a : G
aA : a ∈ A
b : G
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
exact h aA bB ab
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul :
  ∀ (x y : G),
    (f : (a : G) → H) (x * y) = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
simp_rw :
  UniqueMul.{u_2} (G := H) (image (⇑f : (a : G) → H) A : Finset H) (image (⇑f : (a : G) → H) B : Finset H)
      ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H) ↔
    UniqueMul.{u_2} (G := H)
      (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) A : Finset H)
      (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) B : Finset H)
      (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) a0 : H)
      (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) b0 : H)
⊢ UniqueMul (map f A) (map f B) ((f : (a : G) → H) a0) ((f : (a : G) → H) b0) ↔ UniqueMul A B a0 b0

Tactic:
simp_rw [← mulHom_image_iff ⟨f, mul⟩ f.2, Finset.map_eq_image]

Premises used: UniqueMul.mulHom_image_iff, Function.Embedding.inj', MulHom.mk, Finset.map_eq_image, DFunLike.coe
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul :
  ∀ (x y : G),
    (f : (a : G) → H) (x * y) = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
⊢ UniqueMul.{u_2} (G := H) (image (⇑f : (a : G) → H) A : Finset H) (image (⇑f : (a : G) → H) B : Finset H)
      ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H) ↔
    UniqueMul.{u_2} (G := H)
      (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) A : Finset H)
      (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) B : Finset H)
      (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) a0 : H)
      (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) b0 : H)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul :
  ∀ (x y : G),
    (f : (a : G) → H) (x * y) = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
classical :
  UniqueMul (map f A) (map f B) ((f : (a : G) → H) a0) ((f : (a : G) → H) b0) ↔
    UniqueMul.{u_2} (G := H)
      (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) A : Finset H)
      (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) B : Finset H)
      (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) a0 : H)
      (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) b0 : H)
classical₁ classical₂ :
  UniqueMul.{u_2} (G := H) (image (⇑f : (a : G) → H) A : Finset H) (image (⇑f : (a : G) → H) B : Finset H)
      ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H) ↔
    UniqueMul.{u_2} (G := H)
      (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) A : Finset H)
      (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) B : Finset H)
      (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) a0 : H)
      (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) b0 : H)
⊢ UniqueMul (map f A) (map f B) ((f : (a : G) → H) a0) ((f : (a : G) → H) b0) ↔ UniqueMul A B a0 b0

Tactic:
classical simp_rw [← mulHom_image_iff ⟨f, mul⟩ f.2, Finset.map_eq_image]; rfl

Premises used: Finset.map_eq_image
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul (map { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } B) (map { toFun := op, inj' := ⋯ } A) (op b0) (op a0)
a b : G
aA : a ∈ A
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
simpa [and_comm] using h (mem_map_of_mem _ bB) (mem_map_of_mem _ aA) (congr_arg op ab)

Premises used: and_comm, congr_arg, Finset.mem_map_of_mem, MulOpposite.op
-- 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
simp_rw :
  UniqueMul
    (map (Function.Embedding.trans { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } { toFun := op, inj' := ⋯ : Gᵐᵒᵖ ↪ Gᵐᵒᵖᵐᵒᵖ }) A)
    (map (Function.Embedding.trans { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } { toFun := op, inj' := ⋯ }) B) (op (op a0))
    (op (op b0))
⊢ UniqueMul (map { toFun := op, inj' := ⋯ : Gᵐᵒᵖ ↪ Gᵐᵒᵖᵐᵒᵖ } (map { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } A))
    (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } B)) (op (op a0)) (op (op b0))

Tactic:
simp_rw [map_map]

Premises used: Finset.map_map
-- 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
⊢ (Function.Embedding.trans { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } { toFun := op, inj' := ⋯ } : (a : G) → Gᵐᵒᵖᵐᵒᵖ)
      (x * x_1) =
    HMul.hMul (α := Gᵐᵒᵖᵐᵒᵖ) (β := Gᵐᵒᵖᵐᵒᵖ)
      ((Function.Embedding.trans { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } { toFun := op, inj' := ⋯ : Gᵐᵒᵖ ↪ Gᵐᵒᵖᵐᵒᵖ } :
            (a : G) → Gᵐᵒᵖᵐᵒᵖ)
          x :
        Gᵐᵒᵖᵐᵒᵖ)
      ((Function.Embedding.trans { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } { toFun := op, inj' := ⋯ : Gᵐᵒᵖ ↪ Gᵐᵒᵖᵐᵒᵖ } :
            (a : G) → Gᵐᵒᵖᵐᵒᵖ)
          x_1 :
        Gᵐᵒᵖᵐᵒᵖ)

Tactic:
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
⊢ UniqueMul
    (map (Function.Embedding.trans { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } { toFun := op, inj' := ⋯ : Gᵐᵒᵖ ↪ Gᵐᵒᵖᵐᵒᵖ }) A)
    (map (Function.Embedding.trans { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } { toFun := op, inj' := ⋯ }) B) (op (op a0))
    (op (op b0))

Tactic:
exact (mulHom_map_iff _ fun _ _ ↦ by rfl).mpr h

Premises used: Iff.mpr, UniqueMul.mulHom_map_iff
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
⊢ UniqueMul (map { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } B) (map { toFun := op, inj' := ⋯ } A) (op b0) (op a0) ↔
    UniqueMul A B a0 b0

Tactic:
⟨of_mulOpposite, to_mulOpposite⟩

Premises used: UniqueMul.of_mulOpposite, Iff.intro, UniqueMul.to_mulOpposite
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huH : UniqueMul (image (⇑f : (a : G) → H) A) (image (⇑f : (a : G) → H) B) aH bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b : H) = aH * bH →
    (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH

Tactic:
specialize huH (mem_image_of_mem _ ha) (mem_image_of_mem _ hb)

Premises used: Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH :
  HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b : H) = aH * bH →
    (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
⊢ aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH

Tactic:
rw [← map_mul, he, map_mul, hae, hbe] at huH

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
⊢ a = aG ∧ b = bG

Tactic:
huG ?_ ?_ he
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
refine_1 : a ∈ {a ∈ A | (f : (a : G) → H) a = aH}
refine_2 : b ∈ {b ∈ B | (f : (a : G) → H) b = bH}
⊢ a = aG ∧ b = bG

Tactic:
refine huG ?_ ?_ he
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
refine_1 : a ∈ A ∧ (f : (a : G) → H) a = aH
⊢ a ∈ {a ∈ A | (f : (a : G) → H) a = aH}

Tactic:
rw [mem_filter]

Premises used: Finset.mem_filter
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
refine_2 : b ∈ B ∧ (f : (a : G) → H) b = bH
⊢ b ∈ {b ∈ B | (f : (a : G) → H) b = bH}

Tactic:
rw [mem_filter]

Premises used: Finset.mem_filter
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
⊢ a ∈ A ∧ (f : (a : G) → H) a = aH

Tactic:
⟨ha, (huH rfl).1⟩

Premises used: And.left, And.intro, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
⊢ b ∈ B ∧ (f : (a : G) → H) b = bH

Tactic:
⟨hb, (huH rfl).2⟩

Premises used: And.right, And.intro, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
⊢ a ∈ A ∧ (f : (a : G) → H) a = aH

Tactic:
exacts [⟨ha, (huH rfl).1⟩, ⟨hb, (huH rfl).2⟩]
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
pos : ∀ (hc : #A ≤ 1 ∧ #B ≤ 1), ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
neg : ∀ (hc : 1 < #A ∨ 1 < #B), ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
by_cases! +distrib hc : #A ≤ 1 ∧ #B ≤ 1
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
hc : #A ≤ 1 ∧ #B ≤ 1
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
UniqueMul.of_card_le_one hA hB hc.1 hc.2

Premises used: UniqueMul.of_card_le_one, And.right, And.left
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
hc : #A ≤ 1 ∧ #B ≤ 1
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
exact UniqueMul.of_card_le_one hA hB hc.1 hc.2

Premises used: UniqueMul.of_card_le_one, And.right, And.left
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
hc : 1 < #A ∨ 1 < #B
⊢ 0 < #A

Tactic:
rw [← Finset.card_pos] at hA hB

Premises used: Finset.card_pos
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
hc : 1 < #A ∨ 1 < #B
hA₁ : 0 < #A
⊢ 0 < #B

Tactic:
rw [← Finset.card_pos] at hA hB

Premises used: Finset.card_pos
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
hc : 1 < #A ∨ 1 < #B
hA₁ : 0 < #A
hB₁ : 0 < #B
⊢ 1 < #A ∨ 1 < #B

Tactic:
rw [← Finset.card_pos] at hA hB

Premises used: Finset.card_pos
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
neg :
  ∀ (p : G × G) (hp : p ∈ A ×ˢ B),
    ∀ w ∈ A ×ˢ B, p ≠ w → ∀ (hu : UniqueMul A B p.1 p.2), UniqueMul A B w.1 w.2 → ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
obtain ⟨p, hp, _, _, _, hu, _⟩ := h (Nat.one_lt_mul_iff.mpr ⟨hA, hB, hc⟩)

Premises used: Iff.mpr, And.intro, Nat.one_lt_mul_iff
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
p : G × G
hp : p ∈ A ×ˢ B
w : G × G
left : w ∈ A ×ˢ B
left_1 : p ≠ w
hu : UniqueMul A B p.1 p.2
right : UniqueMul A B w.1 w.2
neg :
  ∀ (hp : p.1 ∈ A ∧ p.2 ∈ B),
    ∀ w ∈ A ×ˢ B, p ≠ w → ∀ (hu : UniqueMul A B p.1 p.2), UniqueMul A B w.1 w.2 → ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
rw [Finset.mem_product] at hp

Premises used: Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
p : G × G
hp : p.1 ∈ A ∧ p.2 ∈ B
w : G × G
left : w ∈ A ×ˢ B
left_1 : p ≠ w
hu : UniqueMul A B p.1 p.2
right : UniqueMul A B w.1 w.2
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
⟨p.1, hp.1, p.2, hp.2, hu⟩

Premises used: Prod.fst, And.right, And.left, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
p : G × G
hp : p.1 ∈ A ∧ p.2 ∈ B
w : G × G
left : w ∈ A ×ˢ B
left_1 : p ≠ w
hu : UniqueMul A B p.1 p.2
right : UniqueMul A B w.1 w.2
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
exact ⟨p.1, hp.1, p.2, hp.2, hu⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
x y : G × H
h :
  ULift.down.{v, u}
      ((fun (x : G × H) (t : Bool) ↦
          (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 } { down := x.2 } t : I G H t))
        (x * y) false) =
    ULift.down.{v, u}
      (HMul.hMul (α := (b : Bool) → I G H b) (β := (b : Bool) → I G H b)
        ((fun (x : G × H) (t : Bool) ↦
            (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 : ULift.{v, u} G }
                { down := x.2 : ULift.{u, v} H } t :
              I G H t))
          x)
        ((fun (x : G × H) (t : Bool) ↦
            (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 : ULift.{v, u} G }
                { down := x.2 : ULift.{u, v} H } t :
              I G H t))
          y)
        false)
h₁ :
  ULift.down.{u, v}
      ((fun (x : G × H) (t : Bool) ↦
          (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 } { down := x.2 } t : I G H t))
        (x * y) true) =
    ULift.down.{u, v}
      (HMul.hMul (α := (b : Bool) → I G H b) (β := (b : Bool) → I G H b)
        ((fun (x : G × H) (t : Bool) ↦
            (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 : ULift.{v, u} G }
                { down := x.2 : ULift.{u, v} H } t :
              I G H t))
          x)
        ((fun (x : G × H) (t : Bool) ↦
            (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 : ULift.{v, u} G }
                { down := x.2 : ULift.{u, v} H } t :
              I G H t))
          y)
        true)
⊢ (fun (x : G × H) (t : Bool) ↦
        (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 } { down := x.2 } t : I G H t))
      (x * y) =
    HMul.hMul (α := (b : Bool) → I G H b)
      ((fun (x : G × H) (t : Bool) ↦
          (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 : ULift.{v, u} G }
              { down := x.2 : ULift.{u, v} H } t :
            I G H t))
        x)
      ((fun (x : G × H) (t : Bool) ↦
          (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 : ULift.{v, u} G }
              { down := x.2 : ULift.{u, v} H } t :
            I G H t))
        y)

Tactic:
ext (_ | _)
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
x y : G × H
⊢ ULift.down.{v, u}
      ((fun (x : G × H) (t : Bool) ↦
          (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 } { down := x.2 } t : I G H t))
        (x * y) false) =
    ULift.down.{v, u}
      (HMul.hMul (α := (b : Bool) → I G H b) (β := (b : Bool) → I G H b)
        ((fun (x : G × H) (t : Bool) ↦
            (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 : ULift.{v, u} G }
                { down := x.2 : ULift.{u, v} H } t :
              I G H t))
          x)
        ((fun (x : G × H) (t : Bool) ↦
            (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 : ULift.{v, u} G }
                { down := x.2 : ULift.{u, v} H } t :
              I G H t))
          y)
        false)

Tactic:
rfl