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
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
intro a b ha hb ab
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
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
rw [← hf.eq_iff, ← hf.eq_iff]
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
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
rw [← hf.eq_iff, map_mul, map_mul] at ab
no goals
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
exact u (Finset.mem_preimage.mp ha) (Finset.mem_preimage.mp hb) ab