case refine'_1
G : Type u_2
H : Type u_1
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

case refine'_2
G : Type u_2
H : Type u_1
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)
G : Type u_2
H : Type u_1
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
refine' ⟨fun h ↦ _, fun h ↦ _⟩
case refine'_1
G : Type u_2
H : Type u_1
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
case refine'_1
G : Type u_2
H : Type u_1
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
intro a b ha hb ab
case refine'_1
G : Type u_2
H : Type u_1
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
case refine'_1
G : Type u_2
H : Type u_1
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
rw [← hf.eq_iff, ← hf.eq_iff]
case refine'_1
G : Type u_2
H : Type u_1
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
case refine'_1
G : Type u_2
H : Type u_1
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
rw [← hf.eq_iff, map_mul, map_mul] at ab
no goals
case refine'_1
G : Type u_2
H : Type u_1
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
exact h (Finset.mem_image.mpr ⟨_, ha, rfl⟩) (Finset.mem_image.mpr ⟨_, hb, rfl⟩) ab
case refine'_2
G : Type u_2
H : Type u_1
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
case refine'_2
G : Type u_2
H : Type u_1
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)
intro a b aA bB ab
case refine'_2.intro.intro
G : Type u_2
H : Type u_1
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
case refine'_2
G : Type u_2
H : Type u_1
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
obtain ⟨a, ha, rfl⟩ : ∃ a' ∈ A, f a' = a := Finset.mem_image.mp aA
case refine'_2.intro.intro.intro.intro
G : Type u_2
H : Type u_1
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
case refine'_2.intro.intro
G : Type u_2
H : Type u_1
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
obtain ⟨b, hb, rfl⟩ : ∃ b' ∈ B, f b' = b := Finset.mem_image.mp bB
case refine'_2.intro.intro.intro.intro
G : Type u_2
H : Type u_1
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
case refine'_2.intro.intro.intro.intro
G : Type u_2
H : Type u_1
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
rw [hf.eq_iff, hf.eq_iff]
case refine'_2.intro.intro.intro.intro
G : Type u_2
H : Type u_1
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
case refine'_2.intro.intro.intro.intro
G : Type u_2
H : Type u_1
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
rw [← map_mul, ← map_mul, hf.eq_iff] at ab
no goals
case refine'_2.intro.intro.intro.intro
G : Type u_2
H : Type u_1
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
exact h ha hb ab