[GOAL]
G✝ : Type u_1
H : Type u_2
inst✝² : Mul G✝
inst✝¹ : Mul H
A✝ B✝ : Finset G✝
a0✝ b0✝ : G✝
G : Type u_3
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
ha : x✝¹ ∈ A
hb : x✝ ∈ B
k : x✝¹ ≠ a0 ∨ x✝ ≠ b0
⊢ x✝¹ * x✝ ≠ a0 * b0
[PROOFSTEP]
contrapose! k
[GOAL]
G✝ : Type u_1
H : Type u_2
inst✝² : Mul G✝
inst✝¹ : Mul H
A✝ B✝ : Finset G✝
a0✝ b0✝ : G✝
G : Type u_3
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
ha : x✝¹ ∈ A
hb : x✝ ∈ B
k : x✝¹ * x✝ = a0 * b0
⊢ x✝¹ = a0 ∧ x✝ = b0
[PROOFSTEP]
exact h ha hb k
[GOAL]
G : Type u_1
H : Type u_2
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}
[PROOFSTEP]
rintro ⟨x1, y1⟩ (hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0) ⟨x2, y2⟩ (hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0)
[GOAL]
case mk.mk
G : Type u_1
H : Type u_2
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)
[PROOFSTEP]
rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩
[GOAL]
case mk.mk.intro
G : Type u_1
H : Type u_2
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)
[PROOFSTEP]
rcases h hy.1 hy.2.1 hy.2.2 with ⟨rfl, rfl⟩
[GOAL]
case mk.mk.intro.intro
G : Type u_1
H : Type u_2
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)
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
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)
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
H : Type u_2
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)
[PROOFSTEP]
simpa
[GOAL]
G : Type u_1
H : Type u_2
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
[PROOFSTEP]
rintro ⟨x1, x2⟩ _ _ J x y hx hy l
[GOAL]
case mk
G : Type u_1
H : Type u_2
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
[PROOFSTEP]
rcases Prod.mk.inj_iff.mp (J (a0, b0) (Finset.mk_mem_product aA bB) rfl) with ⟨rfl, rfl⟩
[GOAL]
case mk.intro
G : Type u_1
H : Type u_2
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
[PROOFSTEP]
exact Prod.mk.inj_iff.mp (J (x, y) (Finset.mk_mem_product hx hy) l)
[GOAL]
G : Type u_1
H : Type u_2
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
[PROOFSTEP]
have h' := h
[GOAL]
G : Type u_1
H : Type u_2
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
[PROOFSTEP]
rcases h' with ⟨⟨a, b⟩, ⟨hab, rfl, -⟩, -⟩
[GOAL]
case intro.mk.intro.intro.intro
G : Type u_1
H : Type u_2
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
[PROOFSTEP]
cases' Finset.mem_product.mp hab with ha hb
[GOAL]
case intro.mk.intro.intro.intro.intro
G : Type u_1
H : Type u_2
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
[PROOFSTEP]
exact ⟨a, b, ha, hb, (iff_existsUnique ha hb).mpr h⟩
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
f : G →ₙ* H
hf : Function.Injective ↑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (↑f a0) (↑f b0)
⊢ UniqueMul (Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A)))
    (Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))) a0 b0
[PROOFSTEP]
intro a b ha hb ab
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
f : G →ₙ* H
hf : Function.Injective ↑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (↑f a0) (↑f b0)
a b : G
ha : a ∈ Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A))
hb : b ∈ Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
rw [← hf.eq_iff, ← hf.eq_iff]
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
f : G →ₙ* H
hf : Function.Injective ↑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (↑f a0) (↑f b0)
a b : G
ha : a ∈ Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A))
hb : b ∈ Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))
ab : a * b = a0 * b0
⊢ ↑f a = ↑f a0 ∧ ↑f b = ↑f b0
[PROOFSTEP]
rw [← hf.eq_iff, map_mul, map_mul] at ab 
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
f : G →ₙ* H
hf : Function.Injective ↑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (↑f a0) (↑f b0)
a b : G
ha : a ∈ Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A))
hb : b ∈ Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))
ab : ↑f a * ↑f b = ↑f a0 * ↑f b0
⊢ ↑f a = ↑f a0 ∧ ↑f b = ↑f b0
[PROOFSTEP]
exact u (Finset.mem_preimage.mp ha) (Finset.mem_preimage.mp hb) ab
[GOAL]
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
⊢ UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0) ↔ UniqueMul A B a0 b0
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun h ↦ _⟩
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0)
⊢ UniqueMul A B a0 b0
[PROOFSTEP]
intro a b ha hb ab
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
rw [← hf.eq_iff, ← hf.eq_iff]
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
⊢ ↑f a = ↑f a0 ∧ ↑f b = ↑f b0
[PROOFSTEP]
rw [← hf.eq_iff, map_mul, map_mul] at ab 
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : ↑f a * ↑f b = ↑f a0 * ↑f b0
⊢ ↑f a = ↑f a0 ∧ ↑f b = ↑f b0
[PROOFSTEP]
exact h (Finset.mem_image.mpr ⟨_, ha, rfl⟩) (Finset.mem_image.mpr ⟨_, hb, rfl⟩) ab
[GOAL]
case refine'_2
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
⊢ UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0)
[PROOFSTEP]
intro a b aA bB ab
[GOAL]
case refine'_2
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
a b : H
aA : a ∈ Finset.image (↑f) A
bB : b ∈ Finset.image (↑f) B
ab : a * b = ↑f a0 * ↑f b0
⊢ a = ↑f a0 ∧ b = ↑f b0
[PROOFSTEP]
obtain ⟨a, ha, rfl⟩ : ∃ a' ∈ A, f a' = a := Finset.mem_image.mp aA
[GOAL]
case refine'_2.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
b : H
bB : b ∈ Finset.image (↑f) B
a : G
ha : a ∈ A
aA : ↑f a ∈ Finset.image (↑f) A
ab : ↑f a * b = ↑f a0 * ↑f b0
⊢ ↑f a = ↑f a0 ∧ b = ↑f b0
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ : ∃ b' ∈ B, f b' = b := Finset.mem_image.mp bB
[GOAL]
case refine'_2.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
a : G
ha : a ∈ A
aA : ↑f a ∈ Finset.image (↑f) A
b : G
hb : b ∈ B
bB : ↑f b ∈ Finset.image (↑f) B
ab : ↑f a * ↑f b = ↑f a0 * ↑f b0
⊢ ↑f a = ↑f a0 ∧ ↑f b = ↑f b0
[PROOFSTEP]
rw [hf.eq_iff, hf.eq_iff]
[GOAL]
case refine'_2.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
a : G
ha : a ∈ A
aA : ↑f a ∈ Finset.image (↑f) A
b : G
hb : b ∈ B
bB : ↑f b ∈ Finset.image (↑f) B
ab : ↑f a * ↑f b = ↑f a0 * ↑f b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
rw [← map_mul, ← map_mul, hf.eq_iff] at ab 
[GOAL]
case refine'_2.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
a : G
ha : a ∈ A
aA : ↑f a ∈ Finset.image (↑f) A
b : G
hb : b ∈ B
bB : ↑f b ∈ Finset.image (↑f) B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
exact h ha hb ab
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
⊢ UniqueMul (Finset.map f A) (Finset.map f B) (↑f a0) (↑f b0) ↔ UniqueMul A B a0 b0
[PROOFSTEP]
classical convert @mulHom_image_iff G H _ _ A B a0 b0 _ ⟨f, mul⟩ f.2 using 2 <;>
  · ext
    simp only [Finset.mem_map, MulHom.coe_mk, Finset.mem_image]
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
⊢ UniqueMul (Finset.map f A) (Finset.map f B) (↑f a0) (↑f b0) ↔ UniqueMul A B a0 b0
[PROOFSTEP]
convert @mulHom_image_iff G H _ _ A B a0 b0 _ ⟨f, mul⟩ f.2 using 2
[GOAL]
case h.e'_1.h.e'_3
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
⊢ Finset.map f A = Finset.image (↑{ toFun := ↑f, map_mul' := mul }) A
[PROOFSTEP]
ext
[GOAL]
case h.e'_1.h.e'_3.a
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
a✝ : H
⊢ a✝ ∈ Finset.map f A ↔ a✝ ∈ Finset.image (↑{ toFun := ↑f, map_mul' := mul }) A
[PROOFSTEP]
simp only [Finset.mem_map, MulHom.coe_mk, Finset.mem_image]
[GOAL]
case h.e'_1.h.e'_4
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
⊢ Finset.map f B = Finset.image (↑{ toFun := ↑f, map_mul' := mul }) B
[PROOFSTEP]
ext
[GOAL]
case h.e'_1.h.e'_4.a
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
a✝ : H
⊢ a✝ ∈ Finset.map f B ↔ a✝ ∈ Finset.image (↑{ toFun := ↑f, map_mul' := mul }) B
[PROOFSTEP]
simp only [Finset.mem_map, MulHom.coe_mk, Finset.mem_image]
[GOAL]
M : Type ?u.148083
inst✝¹ : Add M
inst✝ : UniqueSums M
A B : Finset (Multiplicative M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
let A' : Finset M := A
[GOAL]
M : Type ?u.148083
inst✝¹ : Add M
inst✝ : UniqueSums M
A B : Finset (Multiplicative M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
have hA' : A'.Nonempty := hA
[GOAL]
M : Type ?u.148083
inst✝¹ : Add M
inst✝ : UniqueSums M
A B : Finset (Multiplicative M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
hA' : Finset.Nonempty A'
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
obtain ⟨a0, hA0, b0, hB0, J⟩ := UniqueSums.uniqueAdd_of_nonempty hA' hB
[GOAL]
case intro.intro.intro.intro
M : Type ?u.148083
inst✝¹ : Add M
inst✝ : UniqueSums M
A B : Finset (Multiplicative M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
hA' : Finset.Nonempty A'
a0 : M
hA0 : a0 ∈ A'
b0 : M
hB0 : b0 ∈ B
J : UniqueAdd A' B a0 b0
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
exact ⟨ofAdd a0, hA0, ofAdd b0, hB0, fun a b aA bB H ↦ J aA bB H⟩
[GOAL]
M : Type ?u.148565
inst✝¹ : Mul M
inst✝ : UniqueProds M
A B : Finset (Additive M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0
[PROOFSTEP]
let A' : Finset M := A
[GOAL]
M : Type ?u.148565
inst✝¹ : Mul M
inst✝ : UniqueProds M
A B : Finset (Additive M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0
[PROOFSTEP]
have hA' : A'.Nonempty := hA
[GOAL]
M : Type ?u.148565
inst✝¹ : Mul M
inst✝ : UniqueProds M
A B : Finset (Additive M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
hA' : Finset.Nonempty A'
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0
[PROOFSTEP]
obtain ⟨a0, hA0, b0, hB0, J⟩ := UniqueProds.uniqueMul_of_nonempty hA' hB
[GOAL]
case intro.intro.intro.intro
M : Type ?u.148565
inst✝¹ : Mul M
inst✝ : UniqueProds M
A B : Finset (Additive M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
hA' : Finset.Nonempty A'
a0 : M
hA0 : a0 ∈ A'
b0 : M
hB0 : b0 ∈ B
J : UniqueMul A' B a0 b0
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0
[PROOFSTEP]
exact ⟨ofMul a0, hA0, ofMul b0, hB0, fun a b aA bB H ↦ J aA bB H⟩
