awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
refine_1 :
  ∀ (h : Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X) (x : (fun (X : Type u) ↦ X) X),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
            (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
        x
refine_2 :
  ∀
    (h :
      ∀ (x : (fun (X : Type u) ↦ X) X),
        ∃ (i : ι),
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
            (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
                (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
            x)
    (x : X),
    ∃ (Y_1 : Type u) (g : Y_1 ⟶ X),
      Presieve.ofArrows Y f g ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
          (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) X))
          x
⊢ Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X ↔
    ∀ (x : (fun (X : Type u) ↦ X) X),
      ∃ (i : ι),
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
          (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
              (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
          x

Tactic:
refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
h : Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X
x : (fun (X : Type u) ↦ X) X
refine_1 :
  ∀ ⦃Y_1 : Type u⦄ (i : ι)
    (hx :
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
            (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
        x),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
            (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
        x
⊢ ∃ (i : ι),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
          (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
      x

Tactic:
obtain ⟨Y, g, ⟨i⟩, hx⟩ := h x
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
ι : Type u_1
Y_1 : ι → Type u
f : (i : ι) → Y_1 i ⟶ X
h : Presieve.ofArrows Y_1 f ∈ jointlySurjectivePrecoverage.coverings X
x : (fun (X : Type u) ↦ X) X
Y : Type u
i : ι
hx :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
    (Set.range (ι := (fun (X : Type u) ↦ X) (Y_1 i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
        (a : (fun (X : Type u) ↦ X) (Y_1 i)) → (fun (X : Type u) ↦ X) X))
    x
w : ι
h₁ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
    (Set.range (ι := (fun (X : Type u) ↦ X) (Y_1 i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
        (a : (fun (X : Type u) ↦ X) (Y_1 i)) → (fun (X : Type u) ↦ X) X))
    x
⊢ ∃ (i : ι),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.range (ι := (fun (X : Type u) ↦ X) (Y_1 i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
          (a : (fun (X : Type u) ↦ X) (Y_1 i)) → (fun (X : Type u) ↦ X) X))
      x

Tactic:
use i
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
h :
  ∀ (x : (fun (X : Type u) ↦ X) X),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
            (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
        x
x : X
refine_2 :
  ∀ (i : ι)
    (hx :
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
            (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
        x),
    ∃ (Y_1 : Type u) (g : Y_1 ⟶ X),
      Presieve.ofArrows Y f g ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
          (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) X))
          x
⊢ ∃ (Y_1 : Type u) (g : Y_1 ⟶ X),
    Presieve.ofArrows Y f g ∧
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) X))
        x

Tactic:
obtain ⟨i, hx⟩ := h x
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
h :
  ∀ (x : (fun (X : Type u) ↦ X) X),
    ∃ (i : ι),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
            (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
        x
x : X
i : ι
hx :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
    (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
        (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
    x
w : Type u
w₁ : Y i ⟶ X
left : Presieve.ofArrows Y f (f i)
right :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
    (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
        (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
    x
⊢ ∃ (Y_1 : Type u) (g : Y_1 ⟶ X),
    Presieve.ofArrows Y f g ∧
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) X))
        x

Tactic:
use Y i, f i, ⟨i⟩
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
S T : Type u_1
f : S ⟶ T
hf : IsIso f
x : T
right :
  Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) T))
    (Set.range (ι := (fun (X : Type u_1) ↦ X) S)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u_1) ↦ X) S) → (fun (X : Type u_1) ↦ X) T))
    x
⊢ ∃ (Y : Type u_1) (g : Y ⟶ T),
    Presieve.singleton f g ∧
      Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) T))
        (Set.range (ι := (fun (X : Type u_1) ↦ X) Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
            (a : (fun (X : Type u_1) ↦ X) Y) → (fun (X : Type u_1) ↦ X) T))
        x

Tactic:
use S, f, ⟨⟩
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
S T : Type u_1
f : S ⟶ T
hf : IsIso f
x : T
⊢ Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) T))
    (Set.range (ι := (fun (X : Type u_1) ↦ X) S)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u_1) ↦ X) S) → (fun (X : Type u_1) ↦ X) T))
    x

Tactic:
surjective_of_epi f x

Premises used: Set.Mem, setOf, CategoryTheory.surjective_of_epi, Set.range
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
S T : Type u_1
f : S ⟶ T
hf : IsIso f
x : T
⊢ Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) T))
    (Set.range (ι := (fun (X : Type u_1) ↦ X) S)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u_1) ↦ X) S) → (fun (X : Type u_1) ↦ X) T))
    x

Tactic:
exact surjective_of_epi f x

Premises used: CategoryTheory.surjective_of_epi
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ jointlySurjectivePrecoverage.coverings S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve (X i))) (jointlySurjectivePrecoverage.coverings (X i))
      (Presieve.ofArrows (Y i) (g i))
simp_rw :
  ∀
    (hf :
      ∀ (x : S),
        ∃ (i : ι),
          Membership.mem (γ := Set S)
            (Set.range (ι := X i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) : (a : X i) → S)) x)
    (hg :
      ∀ (i : ι) (x : X i),
        ∃ (i_1 : σ i),
          Membership.mem (γ := Set (X i))
            (Set.range (ι := Y i i_1) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (g i i_1)) : (a : Y i i_1) → X i)) x)
    (x : S),
    ∃ (i : (i : ι) × σ i),
      Membership.mem (γ := Set S)
        (Set.range (ι := Y (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (g (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i)) ≫
                  f (i.fst (β := fun (i : ι) ↦ σ i)))) :
            (a : Y i.fst i.snd) → S))
        x
⊢ (Presieve.ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      fun (x : (i : ι) × σ i) ↦
      g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i))) ∈
    jointlySurjectivePrecoverage.coverings S

Tactic:
simp_rw [ofArrows_mem_jointlySurjectivePrecoverage_iff] at hf hg ⊢

Premises used: CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf :
  ∀ (x : S),
    ∃ (i : ι),
      Membership.mem (γ := Set S)
        (Set.range (ι := X i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) : (a : X i) → S)) x
hg :
  ∀ (i : ι) (x : X i),
    ∃ (i_1 : σ i),
      Membership.mem (γ := Set (X i))
        (Set.range (ι := Y i i_1) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (g i i_1)) : (a : Y i i_1) → X i)) x
x : S
obtain :
  ∀ (i : ι) (y : X i),
    ∃ (i_1 : (i : ι) × σ i),
      Membership.mem (α := S) (γ := Set S)
        (Set.range (ι := Y (i_1.fst (β := fun (i : ι) ↦ σ i)) (i_1.snd (β := fun (i : ι) ↦ σ i)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (g (i_1.fst (β := fun (i : ι) ↦ σ i)) (i_1.snd (β := fun (i : ι) ↦ σ i)) ≫
                  f (i_1.fst (β := fun (i : ι) ↦ σ i)))) :
            (a : Y i_1.fst i_1.snd) → S))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f i) : (a : X i) → S) y : S)
⊢ ∃ (i : (i : ι) × σ i),
    Membership.mem (γ := Set S)
      (Set.range (ι := Y (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (g (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i)) ≫
                f (i.fst (β := fun (i : ι) ↦ σ i)))) :
          (a : Y i.fst i.snd) → S))
      x

Tactic:
obtain ⟨i, y, rfl⟩ := hf x

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf :
  ∀ (x : S),
    ∃ (i : ι),
      Membership.mem (γ := Set S)
        (Set.range (ι := X i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) : (a : X i) → S)) x
hg :
  ∀ (i : ι) (x : X i),
    ∃ (i_1 : σ i),
      Membership.mem (γ := Set (X i))
        (Set.range (ι := Y i i_1) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (g i i_1)) : (a : Y i i_1) → X i)) x
i : ι
y : X i
obtain :
  ∀ (j : σ i) (z : Y i j),
    ∃ (i_1 : (i : ι) × σ i),
      Membership.mem (α := S) (γ := Set S)
        (Set.range (ι := Y (i_1.fst (β := fun (i : ι) ↦ σ i)) (i_1.snd (β := fun (i : ι) ↦ σ i)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (g (i_1.fst (β := fun (i : ι) ↦ σ i)) (i_1.snd (β := fun (i : ι) ↦ σ i)) ≫
                  f (i_1.fst (β := fun (i : ι) ↦ σ i)))) :
            (a : Y i_1.fst i_1.snd) → S))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f i) : (a : X i) → S)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (g i j) : (a : Y i j) → X i) z : X i) :
          S)
⊢ ∃ (i_1 : (i : ι) × σ i),
    Membership.mem (α := S) (γ := Set S)
      (Set.range (ι := Y (i_1.fst (β := fun (i : ι) ↦ σ i)) (i_1.snd (β := fun (i : ι) ↦ σ i)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (g (i_1.fst (β := fun (i : ι) ↦ σ i)) (i_1.snd (β := fun (i : ι) ↦ σ i)) ≫
                f (i_1.fst (β := fun (i : ι) ↦ σ i)))) :
          (a : Y i_1.fst i_1.snd) → S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f i) : (a : X i) → S) y : S)

Tactic:
obtain ⟨j, z, rfl⟩ := hg i y

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf :
  ∀ (x : S),
    ∃ (i : ι),
      Membership.mem (γ := Set S)
        (Set.range (ι := X i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) : (a : X i) → S)) x
hg :
  ∀ (i : ι) (x : X i),
    ∃ (i_1 : σ i),
      Membership.mem (γ := Set (X i))
        (Set.range (ι := Y i i_1) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (g i i_1)) : (a : Y i i_1) → X i)) x
i : ι
j : σ i
z : Y i j
h :
  Eq (α := S)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (g ((Sigma.mk (β := fun (i : ι) ↦ σ i) i j).fst (β := fun (i : ι) ↦ σ i))
                ((Sigma.mk (β := fun (i : ι) ↦ σ i) i j).snd (β := fun (i : ι) ↦ σ i)) ≫
              f ((Sigma.mk (β := fun (i : ι) ↦ σ i) i j).fst (β := fun (i : ι) ↦ σ i))) :
          (a : Y ⟨i, j⟩.fst ⟨i, j⟩.snd) → S)
        z :
      S)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f i) : (a : X i) → S)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (g i j) : (a : Y i j) → X i) z : X i) :
      S)
⊢ ∃ (i_1 : (i : ι) × σ i),
    Membership.mem (α := S) (γ := Set S)
      (Set.range (ι := Y (i_1.fst (β := fun (i : ι) ↦ σ i)) (i_1.snd (β := fun (i : ι) ↦ σ i)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (g (i_1.fst (β := fun (i : ι) ↦ σ i)) (i_1.snd (β := fun (i : ι) ↦ σ i)) ≫
                f (i_1.fst (β := fun (i : ι) ↦ σ i)))) :
          (a : Y i_1.fst i_1.snd) → S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f i) : (a : X i) → S)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (g i j) : (a : Y i j) → X i) z : X i) :
        S)

Tactic:
use ⟨i, j⟩, z
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf :
  ∀ (x : S),
    ∃ (i : ι),
      Membership.mem (γ := Set S)
        (Set.range (ι := X i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) : (a : X i) → S)) x
hg :
  ∀ (i : ι) (x : X i),
    ∃ (i_1 : σ i),
      Membership.mem (γ := Set (X i))
        (Set.range (ι := Y i i_1) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (g i i_1)) : (a : Y i i_1) → X i)) x
i : ι
j : σ i
z : Y i j
⊢ Eq (α := S)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (g ((Sigma.mk (β := fun (i : ι) ↦ σ i) i j).fst (β := fun (i : ι) ↦ σ i))
                ((Sigma.mk (β := fun (i : ι) ↦ σ i) i j).snd (β := fun (i : ι) ↦ σ i)) ≫
              f ((Sigma.mk (β := fun (i : ι) ↦ σ i) i j).fst (β := fun (i : ι) ↦ σ i))) :
          (a : Y ⟨i, j⟩.fst ⟨i, j⟩.snd) → S)
        z :
      S)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f i) : (a : X i) → S)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (g i j) : (a : Y i j) → X i) z : X i) :
      S)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u_1
R S : Presieve X
hR : R ∈ jointlySurjectivePrecoverage.coverings X
h : S ∈ jointlySurjectivePrecoverage.coverings X
x : X
obtain :
  ∀ (Y : Type u_1) (f : Y ⟶ X) (hf : R f)
    (hx :
      Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) X))
        (Set.range (ι := (fun (X : Type u_1) ↦ X) Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
            (a : (fun (X : Type u_1) ↦ X) Y) → (fun (X : Type u_1) ↦ X) X))
        x),
    ∃ (Y : Type u_1) (g : Y ⟶ X),
      (R ⊔ S) g ∧
        Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) X))
          (Set.range (ι := (fun (X : Type u_1) ↦ X) Y)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u_1) ↦ X) Y) → (fun (X : Type u_1) ↦ X) X))
          x
⊢ ∃ (Y : Type u_1) (g : Y ⟶ X),
    (R ⊔ S) g ∧
      Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) X))
        (Set.range (ι := (fun (X : Type u_1) ↦ X) Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
            (a : (fun (X : Type u_1) ↦ X) Y) → (fun (X : Type u_1) ↦ X) X))
        x

Tactic:
obtain ⟨Y, f, hf, hx⟩ := hR x
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u_1
R S : Presieve X
hR : R ∈ jointlySurjectivePrecoverage.coverings X
h : S ∈ jointlySurjectivePrecoverage.coverings X
x : X
Y : Type u_1
f : Y ⟶ X
hf : R f
hx :
  Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) X))
    (Set.range (ι := (fun (X : Type u_1) ↦ X) Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u_1) ↦ X) Y) → (fun (X : Type u_1) ↦ X) X))
    x
w : Type u_1
w₁ : Y ⟶ X
left : (R ⊔ S) f
right :
  Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) X))
    (Set.range (ι := (fun (X : Type u_1) ↦ X) Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u_1) ↦ X) Y) → (fun (X : Type u_1) ↦ X) X))
    x
⊢ ∃ (Y : Type u_1) (g : Y ⟶ X),
    (R ⊔ S) g ∧
      Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) X))
        (Set.range (ι := (fun (X : Type u_1) ↦ X) Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
            (a : (fun (X : Type u_1) ↦ X) Y) → (fun (X : Type u_1) ↦ X) X))
        x

Tactic:
use Y, f, .inl hf
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
choose :
  ∀ (i : (x : X) → E.I₀) (y : (x : X) → (fun (X : Type u) ↦ X) (E.X (i x)))
    (hy :
      ∀ (x : X),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (E.f (i x)) :
              (a : (fun (X : Type u) ↦ X) (E.X (i x))) → (fun (X : Type u) ↦ X) X)
            (y x) =
          x),
    E.Small
⊢ E.Small

Tactic:
choose i y hy using ofArrows_mem_jointlySurjectivePrecoverage_iff.mp E.mem₀

Premises used: Iff.mp, CategoryTheory.Precoverage.ZeroHypercover.mem₀, CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : (x : X) → E.I₀
y : (x : X) → (fun (X : Type u) ↦ X) (E.X (i x))
hy :
  ∀ (x : X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (E.f (i x)) :
          (a : (fun (X : Type u) ↦ X) (E.X (i x))) → (fun (X : Type u) ↦ X) X)
        (y x) =
      x
⊢ E.Small

Tactic:
⟨X, i, ?_⟩

Premises used: Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.Small.mk
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : (x : X) → E.I₀
y : (x : X) → (fun (X : Type u) ↦ X) (E.X (i x))
hy :
  ∀ (x : X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (E.f (i x)) :
          (a : (fun (X : Type u) ↦ X) (E.X (i x))) → (fun (X : Type u) ↦ X) X)
        (y x) =
      x
refine : (E.restrictIndex i).presieve₀ ∈ jointlySurjectivePrecoverage.coverings X
⊢ E.Small

Tactic:
refine ⟨X, i, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : (x : X) → E.I₀
y : (x : X) → (fun (X : Type u) ↦ X) (E.X (i x))
hy :
  ∀ (x : X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (E.f (i x)) :
          (a : (fun (X : Type u) ↦ X) (E.X (i x))) → (fun (X : Type u) ↦ X) X)
        (y x) =
      x
rw :
  ∀ (x : (fun (X : Type u) ↦ X) X),
    ∃ (i_1 : (E.restrictIndex i).I₀),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
        (Set.range (ι := (fun (X : Type u) ↦ X) ((E.restrictIndex i).X i_1))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((E.restrictIndex i).f i_1)) :
            (a : (fun (X : Type u) ↦ X) ((E.restrictIndex i).X i_1)) → (fun (X : Type u) ↦ X) X))
        x
⊢ (E.restrictIndex i).presieve₀ ∈ jointlySurjectivePrecoverage.coverings X

Tactic:
rw [ofArrows_mem_jointlySurjectivePrecoverage_iff]

Premises used: CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : (x : X) → E.I₀
y : (x : X) → (fun (X : Type u) ↦ X) (E.X (i x))
hy :
  ∀ (x : X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (E.f (i x)) :
          (a : (fun (X : Type u) ↦ X) (E.X (i x))) → (fun (X : Type u) ↦ X) X)
        (y x) =
      x
x : X
w : (E.restrictIndex i).I₀
w₁ : (fun (X : Type u) ↦ X) ((E.restrictIndex i).X x)
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((E.restrictIndex i).f x) :
        (a : (fun (X : Type u) ↦ X) ((E.restrictIndex i).X x)) → (fun (X : Type u) ↦ X) X)
      (y x) =
    x
⊢ ∃ (i_1 : (E.restrictIndex i).I₀),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.range (ι := (fun (X : Type u) ↦ X) ((E.restrictIndex i).X i_1))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((E.restrictIndex i).f i_1)) :
          (a : (fun (X : Type u) ↦ X) ((E.restrictIndex i).X i_1)) → (fun (X : Type u) ↦ X) X))
      x

Tactic:
use x, y x, hy 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
⊢ 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:
⟨fun h x ↦ ?_, fun h x ↦ ?_⟩

Premises used: Iff.intro