no goals
G : Type u_1
H : Type ?u.2277
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
x✝ : UniqueMul A B a0 b0
⊢ ∀ (y : (a0, b0) ∈ A ×ˢ B), (fun x => (a0, b0).fst * (a0, b0).snd = a0 * b0) y → y = (_ : (a0, b0) ∈ A ×ˢ B)
simp
no goals
G : Type u_1
H : Type ?u.2277
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
x✝ : UniqueMul A B a0 b0
⊢ ∀ (y : G × G), (fun ab => ∃! x, ab.fst * ab.snd = a0 * b0) y → y = (a0, b0)
simpa
case mk
G : Type u_1
H : Type ?u.2277
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab x, ab.fst * ab.snd = a0 * b0
x1 x2 : G
h✝ : (x1, x2) ∈ A ×ˢ B
a✝ : (x1, x2).fst * (x1, x2).snd = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B → y.fst * y.snd = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
⊢ x = a0 ∧ y = b0
G : Type u_1
H : Type ?u.2277
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab x, ab.fst * ab.snd = a0 * b0
⊢ ∀ (x : G × G),
    x ∈ A ×ˢ B →
      x.fst * x.snd = a0 * b0 → (∀ (y : G × G), y ∈ A ×ˢ B → y.fst * y.snd = a0 * b0 → y = x) → UniqueMul A B a0 b0
rintro ⟨x1, x2⟩ _ _ J x y hx hy l
case mk.intro
G : Type u_1
H : Type ?u.2277
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab x, ab.fst * ab.snd = a0 * b0
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
h✝ : (a0, b0) ∈ A ×ˢ B
a✝ : (a0, b0).fst * (a0, b0).snd = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B → y.fst * y.snd = a0 * b0 → y = (a0, b0)
⊢ x = a0 ∧ y = b0
case mk
G : Type u_1
H : Type ?u.2277
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab x, ab.fst * ab.snd = a0 * b0
x1 x2 : G
h✝ : (x1, x2) ∈ A ×ˢ B
a✝ : (x1, x2).fst * (x1, x2).snd = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B → y.fst * y.snd = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
⊢ x = a0 ∧ y = b0
rcases Prod.mk.inj_iff.mp (J (a0, b0) (Finset.mk_mem_product aA bB) rfl) with ⟨rfl, rfl⟩
no goals
case mk.intro
G : Type u_1
H : Type ?u.2277
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab x, ab.fst * ab.snd = a0 * b0
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
h✝ : (a0, b0) ∈ A ×ˢ B
a✝ : (a0, b0).fst * (a0, b0).snd = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B → y.fst * y.snd = a0 * b0 → y = (a0, b0)
⊢ x = a0 ∧ y = b0
exact Prod.mk.inj_iff.mp (J (x, y) (Finset.mk_mem_product hx hy) l)