-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_1 : HasPullback f g],
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (pullback f g))) (β :=
      (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison F f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (pullback f g))) → (fun (X : Type u) ↦ X) (pullback (F.map f) (F.map g)))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf :
  ∀ (x : (fun (X : Type u) ↦ X) (F.obj S)),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
            (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
        x
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi :
  Membership.mem (α := (fun (X : Type u) ↦ X) (F.obj S)) (γ := Set ((fun (X : Type u) ↦ X) (F.obj S)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
        (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj S))
        x :
      (fun (X : Type u) ↦ X) (F.obj S))
this_1 : HasPullback g (f i)
this :
  F.map (p₁ i) =
    CategoryStruct.comp (Y := F.obj (pullback g (f i))) (F.map (Iso.hom ⋯.isoPullback))
      (CategoryStruct.comp (Y := pullback (F.map g) (F.map (f i))) (pullbackComparison F g (f i))
        (pullback.fst (F.map g) (F.map (f i))))
h₁ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := F.obj (pullback g (f i))) (F.map (Iso.hom ⋯.isoPullback))
              (CategoryStruct.comp (Y := pullback (F.map g) (F.map (f i))) (pullbackComparison F g (f i))
                (pullback.fst (F.map g) (F.map (f i)))))) :
        (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
    x
h₂ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
      (Function.comp (β := (fun (X : Type u) ↦ X) (F.obj (pullback g (f i))))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := pullback (F.map g) (F.map (f i))) (pullbackComparison F g (f i))
                (pullback.fst (F.map g) (F.map (f i))))) :
          (a : (fun (X : Type u) ↦ X) (F.obj (pullback g (f i)))) → (fun (X : Type u) ↦ X) (F.obj Y))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Iso.hom ⋯.isoPullback))) :
          (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (F.obj (P i)))) →
            (fun (X : Type u) ↦ X) (F.obj (pullback g (f i))))))
    x
h₃ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
      (Function.comp (β := (fun (X : Type u) ↦ X) (F.obj (pullback g (f i))))
        (Function.comp (β := (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i))))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.fst (F.map g) (F.map (f i)))) :
            (a : (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i)))) → (fun (X : Type u) ↦ X) (F.obj Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison F g (f i))) :
            (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (F.obj (pullback g (f i))))) →
              (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i)))))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Iso.hom ⋯.isoPullback))) :
          (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (F.obj (P i)))) →
            (fun (X : Type u) ↦ X) (F.obj (pullback g (f i))))))
    x
h₄ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
      (Function.comp (β := (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i))))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.fst (F.map g) (F.map (f i)))) :
          (a : (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i)))) → (fun (X : Type u) ↦ X) (F.obj Y))
        (Function.comp (β := (fun (X : Type u) ↦ X) (F.obj (pullback g (f i))))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison F g (f i))) :
            (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (F.obj (pullback g (f i))))) →
              (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i))))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Iso.hom ⋯.isoPullback))) :
            (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (F.obj (P i)))) →
              (fun (X : Type u) ↦ X) (F.obj (pullback g (f i)))))))
    x
h₅ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.image (α := (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i))))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.fst (F.map g) (F.map (f i)))) :
        (a : (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i)))) → (fun (X : Type u) ↦ X) (F.obj Y))
      (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
        (Function.comp (β := (fun (X : Type u) ↦ X) (F.obj (pullback g (f i))))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison F g (f i))) :
            (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (F.obj (pullback g (f i))))) →
              (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i))))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Iso.hom ⋯.isoPullback))) :
            (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (F.obj (P i)))) →
              (fun (X : Type u) ↦ X) (F.obj (pullback g (f i)))))))
    x
h₆ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.image (α := (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i))))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.fst (F.map g) (F.map (f i)))) :
        (a : (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i)))) → (fun (X : Type u) ↦ X) (F.obj Y))
      Set.univ)
    x
h₇ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i))))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.fst (F.map g) (F.map (f i)))) :
        (a : (fun (X : Type u) ↦ X) (pullback (F.map g) (F.map (f i)))) → (fun (X : Type u) ↦ X) (F.obj Y)))
    x
h₈ h₉ h₁₀ h₁₁ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.preimage (β := (fun (X : Type u) ↦ X) (F.obj S))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj S))
      (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (X i)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
          (a : (fun (X : Type u) ↦ X) (F.obj (X i))) → (fun (X : Type u) ↦ X) (F.obj S))))
    x
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj Y)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (P i)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (p₁ i))) :
        (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
    x

Tactic:
rwa [this, types_comp, types_comp, Function.comp_assoc, Set.range_comp,
      Function.Surjective.range_eq <| (H _ _).comp (surjective_of_epi _), Set.image_univ,
      Types.range_pullbackFst]

Premises used: Set.range_comp, Set.image_univ, CategoryTheory.Limits.Types.range_pullbackFst, CategoryTheory.types_comp, Function.Surjective.range_eq, Function.Surjective.comp, CategoryTheory.surjective_of_epi, Function.comp_assoc