awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
X : C
R : Presieve.{v_1, u_1} X
refine_1 :
  ∀
    (h :
      Membership.mem (γ := Set (Presieve (F.obj X))) (Types.jointlySurjectivePrecoverage.coverings (F.obj X)) (map F R))
    (x : F.obj X),
    ∃ (Y : C) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
              (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
          x
refine_2 :
  ∀
    (h :
      ∀ (x : F.obj X),
        ∃ (Y : C) (f : Y ⟶ X),
          R f ∧
            Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
              (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
                  (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
              x)
    (x : F.obj X),
    ∃ (Y : Type u) (g : Y ⟶ F.obj X),
      map F R g ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) Y)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) (F.obj X)))
          x
⊢ Membership.mem (γ := Set (Presieve (F.obj X))) (Types.jointlySurjectivePrecoverage.coverings (F.obj X)) (map F R) ↔
    ∀ (x : F.obj X),
      ∃ (Y : C) (f : Y ⟶ X),
        R f ∧
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
            (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
                (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
            x

Tactic:
refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- 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)
X : C
R : Presieve.{v_1, u_1} X
h : Membership.mem (γ := Set (Presieve (F.obj X))) (Types.jointlySurjectivePrecoverage.coverings (F.obj X)) (map F R)
x : F.obj X
refine_1 :
  ∀ ⦃Y : Type u⦄ {Y : C} {u : Y ⟶ X} (hf : R u)
    (hi :
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map u)) :
            (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
        x),
    ∃ (Y : C) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
              (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
          x
⊢ ∃ (Y : C) (f : Y ⟶ X),
    R f ∧
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
        x

Tactic:
obtain ⟨-, -, ⟨hf⟩, hi⟩ := h x
-- 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)
X : C
R : Presieve.{v_1, u_1} X
h : Membership.mem (γ := Set (Presieve (F.obj X))) (Types.jointlySurjectivePrecoverage.coverings (F.obj X)) (map F R)
x : F.obj X
Y : Type u
Y_1 : C
u : Y_1 ⟶ X
hf : R u
hi :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y_1))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map u)) :
        (a : (fun (X : Type u) ↦ X) (F.obj Y_1)) → (fun (X : Type u) ↦ X) (F.obj X)))
    x
⊢ ∃ (Y : C) (f : Y ⟶ X),
    R f ∧
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
        x

Tactic:
⟨_, _, hf, hi⟩

Premises used: And.intro, Exists.intro
-- 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)
X : C
R : Presieve.{v_1, u_1} X
h : Membership.mem (γ := Set (Presieve (F.obj X))) (Types.jointlySurjectivePrecoverage.coverings (F.obj X)) (map F R)
x : F.obj X
Y : Type u
Y_1 : C
u : Y_1 ⟶ X
hf : R u
hi :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y_1))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map u)) :
        (a : (fun (X : Type u) ↦ X) (F.obj Y_1)) → (fun (X : Type u) ↦ X) (F.obj X)))
    x
⊢ ∃ (Y : C) (f : Y ⟶ X),
    R f ∧
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
        x

Tactic:
exact ⟨_, _, hf, hi⟩
-- 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)
X : C
R : Presieve.{v_1, u_1} X
h :
  ∀ (x : F.obj X),
    ∃ (Y : C) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
              (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
          x
x : F.obj X
refine_2 :
  ∀ (Y : C) (g : Y ⟶ X) (hg : R g)
    (hi :
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
            (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
        x),
    ∃ (Y : Type u) (g : Y ⟶ F.obj X),
      map F R g ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) Y)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) (F.obj X)))
          x
⊢ ∃ (Y : Type u) (g : Y ⟶ F.obj X),
    map F R g ∧
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
        (Set.range (ι := (fun (X : Type u) ↦ X) Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
            (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) (F.obj X)))
        x

Tactic:
obtain ⟨Y, g, hg, hi⟩ := h x
-- 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)
X : C
R : Presieve.{v_1, u_1} X
h :
  ∀ (x : F.obj X),
    ∃ (Y : C) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
              (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
          x
x : F.obj X
Y : C
g : Y ⟶ X
hg : R g
hi :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
    x
⊢ ∃ (Y : Type u) (g : Y ⟶ F.obj X),
    map F R g ∧
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
        (Set.range (ι := (fun (X : Type u) ↦ X) Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
            (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) (F.obj X)))
        x

Tactic:
⟨_, _, ⟨hg⟩, hi⟩

Premises used: And.intro, Exists.intro, CategoryTheory.Presieve.map.of
-- 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)
X : C
R : Presieve.{v_1, u_1} X
h :
  ∀ (x : F.obj X),
    ∃ (Y : C) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
              (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
          x
x : F.obj X
Y : C
g : Y ⟶ X
hg : R g
hi :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (F.obj X)))
    x
⊢ ∃ (Y : Type u) (g : Y ⟶ F.obj X),
    map F R g ∧
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
        (Set.range (ι := (fun (X : Type u) ↦ X) Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
            (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) (F.obj X)))
        x

Tactic:
exact ⟨_, _, ⟨hg⟩, hi⟩
-- 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)
X : C
ι : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings X ↔
    ∀ (x : F.obj X),
      ∃ (i : ι),
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (F.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (F.obj (Y i)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f i))) :
              (a : (fun (X : Type u) ↦ X) (F.obj (Y i))) → (fun (X : Type u) ↦ X) (F.obj X)))
          x

Tactic:
simp
-- 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 : Presieve.ofArrows X f ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings S
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)
rw :
  ∀
    (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 : (fun (X : Type u) ↦ X) (F.obj Y)),
    ∃ (i : ι),
      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
⊢ Presieve.ofArrows P p₁ ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings Y

Tactic:
rw [Precoverage.mem_comap_iff, Presieve.map_ofArrows,
      Types.ofArrows_mem_jointlySurjectivePrecoverage_iff] at hf ⊢

Premises used: CategoryTheory.Presieve.map_ofArrows, CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff, CategoryTheory.Precoverage.mem_comap_iff
-- 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
obtain :
  ∀ (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))),
    ∃ (i : ι),
      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
⊢ ∃ (i : ι),
    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:
obtain ⟨i, hi⟩ := hf (F.map g x)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, DFunLike.coe
-- 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))
⊢ HasPullback g (f i)

Tactic:
have : HasPullback g (f i) := (h i).hasPullback
-- 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 : HasPullback g (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) (F.map (p₁ i))) :
        (a : (fun (X : Type u) ↦ X) (F.obj (P i))) → (fun (X : Type u) ↦ X) (F.obj Y)))
    x
⊢ ∃ (i : ι),
    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:
use i
-- 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 : HasPullback g (f i)
⊢ 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))))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : HasPullback g (f i)
⊢ 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))))

Tactic:
have : F.map (p₁ i) = F.map ((h i).isoPullback.hom) ≫ pullbackComparison F g (f i) ≫
        pullback.fst _ _ := by simp [← Functor.map_comp]
-- 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)
rw : (Precoverage.comap (𝟭 (Type u_2)) Types.jointlySurjectivePrecoverage).IsStableUnderBaseChange
⊢ Types.jointlySurjectivePrecoverage.IsStableUnderBaseChange

Tactic:
rw [← Precoverage.comap_id Types.jointlySurjectivePrecoverage]

Premises used: CategoryTheory.Types.jointlySurjectivePrecoverage, CategoryTheory.Precoverage.comap_id
-- 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 : Type u_2} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective (α := (fun (X : Type u_2) ↦ X) (Functor.obj (𝟭 (Type u_2)) (pullback f g))) (β :=
      (fun (X : Type u_2) ↦ X)
        (pullback (X := Functor.obj (𝟭 (Type u_2)) X) (Functor.map (𝟭 (Type u_2)) f) (Functor.map (𝟭 (Type u_2)) g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison (𝟭 (Type u_2)) f g)) :
        (a : (fun (X : Type u_2) ↦ X) ((𝟭 (Type u_2)).obj (pullback f g))) →
          (fun (X : Type u_2) ↦ X) (pullback ((𝟭 (Type u_2)).map f) ((𝟭 (Type u_2)).map g)))
⊢ (Precoverage.comap (𝟭 (Type u_2)) Types.jointlySurjectivePrecoverage).IsStableUnderBaseChange

Tactic:
apply isStableUnderBaseChange_comap_jointlySurjectivePrecoverage

Premises used: CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage