English
Define an isomorphism using isomorphisms fn, fg that respects φ₁ and φ₂ under a compatibility h.
Русский
Определить изоморфизм, используя изоморфизммы fn, fg и совместимость h, сохраняющую φ₁ и φ₂.
LaTeX
$$$ congr' : N_1⋊[φ_1]G_1 \cong N_2⋊[φ_2] G_2 $ with h$$
Lean4
/-- Define an isomorphism from `N₁ ⋊[φ₁] G₁` to `N₂ ⋊[φ₂] G₂` given isomorphisms `N₁ ≃* N₂` and
`G₁ ≃* G₂` that satisfy a commutativity condition `∀ n g, fn (φ₁ g n) = φ₂ (fg g) (fn n)`. -/
@[simps]
def congr : N₁ ⋊[φ₁] G₁ ≃* N₂ ⋊[φ₂] G₂ where
toFun x := ⟨fn x.1, fg x.2⟩
invFun x := ⟨fn.symm x.1, fg.symm x.2⟩
left_inv _ := by simp
right_inv _ := by simp
map_mul' x
y := by
replace h := DFunLike.ext_iff.1 (h x.right) y.left
ext <;> simp_all
