-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this_1 : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
this : ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : (p : G × (f i).V.obj) → G × X.V.obj :=
  fun (p : G × (f i).V.obj) ↦
    (p.1,
      (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ r.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
        p.2)
q : (p : G × X.V.obj) → X.V.obj :=
  fun (p : G × X.V.obj) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((X.ρ : (a : G) → End X.V) p.1)) :
        (a : (fun (X : Type u_1) ↦ X) X.V.obj) → (fun (X : Type u_1) ↦ X) X.V.obj)
      p.2
q' : (p : G × (f i).V.obj) → (f i).V.obj :=
  fun (p : G × (f i).V.obj) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) (((f i).ρ : (a : G) → End (f i).V) p.1)) :
        (a : (fun (X : Type u_1) ↦ X) (f i).V.obj) → (fun (X : Type u_1) ↦ X) (f i).V.obj)
      p.2
heq :
  q ∘ r'' =
    (⇑(@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ r.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) ∘
      q'
⊢ Continuous (Y := (f i).V.obj) fun (p : G × (f i).V.obj) ↦ p.1 • p.2
have hrinj : Function.Injective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) (β :=
  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
  (⇑(@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
        _ _ _ r.hom) :
    (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
Tactic: have hrinj : Function.Injective r.hom :=
      (ConcreteCategory.mono_iff_injective_of_preservesPullback r).mp <| mono_comp _ _