-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem of_mulHom (f : H →ₙ* G)
    (hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d)
    [UniqueProds G] : UniqueProds H where
  uniqueMul_of_nonempty {A B} A0 B0

Proof state:
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
classical
obtain ⟨a0, ha0, b0, hb0, h⟩ := uniqueMul_of_nonempty (A0.image f) (B0.image f)
obtain ⟨a', ha', rfl⟩ := mem_image.mp ha0
obtain ⟨b', hb', rfl⟩ := mem_image.mp hb0
exact ⟨a', ha', b', hb', UniqueMul.of_mulHom_image f hf h⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
b0 : G
hb0 : b0 ∈ image (⇑f) B
a' : H
ha' : a' ∈ A
ha0 : f a' ∈ image (⇑f) A
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a') b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨b', hb', rfl⟩ := mem_image.mp hb0

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
a' : H
ha' : a' ∈ A
ha0 : f a' ∈ image (⇑f) A
b' : H
hb' : b' ∈ B
hb0 : f b' ∈ image (⇑f) B
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a') (f b')
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
a' : H
ha' : a' ∈ A
ha0 : f a' ∈ image (⇑f) A
b' : H
hb' : b' ∈ B
hb0 : f b' ∈ image (⇑f) B
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a') (f b')
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
exact ⟨a', ha', b', hb', UniqueMul.of_mulHom_image f hf h⟩

Result:
no goals

Proof state:
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨a0, ha0, b0, hb0, h⟩ := uniqueMul_of_nonempty (A0.image f) (B0.image f)

Result:
case intro.intro.intro.intro
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
a0 : G
ha0 : a0 ∈ image (⇑f) A
b0 : G
hb0 : b0 ∈ image (⇑f) B
h : UniqueMul (image (⇑f) A) (image (⇑f) B) a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Proof state:
case intro.intro.intro.intro
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
a0 : G
ha0 : a0 ∈ image (⇑f) A
b0 : G
hb0 : b0 ∈ image (⇑f) B
h : UniqueMul (image (⇑f) A) (image (⇑f) B) a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨a', ha', rfl⟩ := mem_image.mp ha0

Result:
case intro.intro.intro.intro.intro.intro
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
b0 : G
hb0 : b0 ∈ image (⇑f) B
a' : H
ha' : a' ∈ A
ha0 : f a' ∈ image (⇑f) A
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a') b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0