case mk.mk
G : Type u_1
H : Type ?u.1533
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : 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
⊢ (x1, y1) = (x2, y2)
G : Type u_1
H : Type ?u.1533
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ Set.Subsingleton {ab | ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst * ab.snd = a0 * b0}
rintro ⟨x1, y1⟩ (hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0) ⟨x2, y2⟩
  (hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0)
case mk.mk.intro
G : Type u_1
H : Type ?u.1533
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0 b0 : 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
⊢ (x1, y1) = (x2, y2)
case mk.mk
G : Type u_1
H : Type ?u.1533
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : 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
⊢ (x1, y1) = (x2, y2)
rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩
case mk.mk.intro.intro
G : Type u_1
H : Type ?u.1533
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0 b0 : 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)
case mk.mk.intro
G : Type u_1
H : Type ?u.1533
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0 b0 : 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
⊢ (x1, y1) = (x2, y2)
rcases h hy.1 hy.2.1 hy.2.2 with ⟨rfl, rfl⟩
no goals
case mk.mk.intro.intro
G : Type u_1
H : Type ?u.1533
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0 b0 : 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)
rfl