G : Type u_1
H : Type ?u.9715
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
g : G
h h' : ∃! ab x, ab.fst * ab.snd = g
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
G : Type u_1
H : Type ?u.9715
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
g : G
h : ∃! ab x, ab.fst * ab.snd = g
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
have h' := h
case intro.mk.intro.intro.intro
G : Type u_1
H : Type ?u.9715
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab x, ab.fst * ab.snd = (a, b).fst * (a, b).snd
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
G : Type u_1
H : Type ?u.9715
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
g : G
h h' : ∃! ab x, ab.fst * ab.snd = g
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
rcases h' with ⟨⟨a, b⟩, ⟨hab, rfl, -⟩, -⟩
case intro.mk.intro.intro.intro.intro
G : Type u_1
H : Type ?u.9715
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab x, ab.fst * ab.snd = (a, b).fst * (a, b).snd
ha : (a, b).fst ∈ A
hb : (a, b).snd ∈ B
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
case intro.mk.intro.intro.intro
G : Type u_1
H : Type ?u.9715
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab x, ab.fst * ab.snd = (a, b).fst * (a, b).snd
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
cases' Finset.mem_product.mp hab with ha hb
no goals
case intro.mk.intro.intro.intro.intro
G : Type u_1
H : Type ?u.9715
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab x, ab.fst * ab.snd = (a, b).fst * (a, b).snd
ha : (a, b).fst ∈ A
hb : (a, b).snd ∈ B
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
exact ⟨a, b, ha, hb, (iff_existsUnique ha hb).mpr h⟩