Equal then isomorphic

Stream: Is there code for X?

[brokkilisoup]

import Mathlib.GroupTheory.Sylow
import Mathlib.GroupTheory.Perm.Cycle.Concrete
import Mathlib.GroupTheory.Perm.Subgroup
import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.Subgroup.Basic

open QuotientGroup

theorem first_isomorphism_theorem {G : Type*} [Group G] {H : Type*} [Group H] (f : G →* H) : ((G ⧸ f.ker) ≃* f.range) := by
 sorry

lemma ProdCylic {G : Type*} [Group G] {H K : Subgroup G} [H.Normal] [K.Normal] (h : Disjoint H K) (p: ℕ) (hp : Nat.Prime p) (h1 : H.index = p) (h2 : K.index = p) : G ≃* (G ⧸ H) × (G ⧸ K) := by
 let f : G →* (G ⧸ H) × (G ⧸ K) := (QuotientGroup.mk' H).prod (QuotientGroup.mk' K)
 have fSurj : Function.Surjective f := by
  unfold Function.Surjective
  intro x
  rcases x with ⟨x1,x2⟩
  have projH := QuotientGroup.mk'_surjective H
  unfold Function.Surjective at projH
  rcases projH x1 with ⟨y,hx1'⟩
  have projK := QuotientGroup.mk'_surjective K
  unfold Function.Surjective at projK
  rcases projK x2 with ⟨y,hx2'⟩
  simp only [MonoidHom.prod_apply]
  use y
  rw[←hx1',←hx2']
  sorry
 have KerCap : f.ker = H ⊓ K := by
  rw[MonoidHom.ker_prod]
  rw[QuotientGroup.ker_mk',QuotientGroup.ker_mk']
  done
 have KerCapBot : f.ker = ⊥ := by
    rw[KerCap]
    exact h.eq_bot
    done
 have fImage : f.range = ((G ⧸ H) × (G ⧸ K)) := by
  sorry
 have FirstIso := first_isomorphism_theorem f
 have KerTrivial := (QuotientGroup.quotientMulEquivOfEq KerCapBot).symm
 have GBot : G ≃* G ⧸ ⊥ := by
  exact QuotientGroup.quotientBot.symm
  done
 have concatenation : G ≃* G⧸MonoidHom.ker f := by
  exact MulEquiv.trans GBot KerTrivial
  done
 have finalIso : G ≃* MonoidHom.range f := by
  exact MulEquiv.trans concatenation FirstIso
  done
 have fImageIso : f.range ≃* ((G ⧸ H) × (G ⧸ K)) := by
  sorry
 have finalIso : G ≃* ((G ⧸ H) × (G ⧸ K)) := by
  exact MulEquiv.trans finalIso fImageIso
  done
 exact finalIso

My problem is the followinf. I should know that f.range = ((G ⧸ H) × (G ⧸ K)) (this is because I previously proved that f is surjective). and I want a proof that f.range ≃* ((G ⧸ H) × (G ⧸ K)) to use exact MulEquiv.trans, but I'm unable to find on moogle.ai for example the proof of the fact that equal implies isomorphic in this case, anyone does know how to solve this problem?
Any help would be appreciated.

[Yaël Dillies]

docs#MulEquiv.subgroupCongr

[Yaël Dillies]

This one was not super easy to find. I was expecting something like Subgroup.equivOfEq.

[Yaël Dillies]

although I assume that by f.range = (G ⧸ H) × (G ⧸ K) you mean f.range = ⊤. You will find docs#Subgroup.topEquiv useful.

[brokkilisoup]

Yaël Dillies ha scritto:

although I assume that by f.range = (G ⧸ H) × (G ⧸ K) you mean f.range = ⊤. You will find docs#Subgroup.topEquiv useful.

But should I prove than that (G ⧸ H) × (G ⧸ K) = ⊤ or Lean does know it some how? because f being surjective is f.range = (G ⧸ H) × (G ⧸ K)

[Kevin Buzzard]

That statement is essentially meaningless in lean because f.range is a set and the product is a type.

[Kevin Buzzard]

A type can have a subset whose elements are the entire type though, that's what \top is.

[Yaël Dillies]

As Kevin says, there's a difference between (G ⧸ H) × (G ⧸ K) (a type) and ⊤ : Subgroup ((G ⧸ H) × (G ⧸ K)) (a term).