awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨i, hx⟩ := h x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
⊢ ∃ (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
have w₁ : Y i ⟶ X
Tactic: use Y i, f i, ⟨i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
⊢ ∃ (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
have left : Presieve.ofArrows Y f (f i)
Tactic: use Y i, f i, ⟨i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
S T : Type u_1
f : S ⟶ T
hf : IsIso f
x : T
⊢ ∃ (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
have 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
Tactic: use S, f, ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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))
⊢ (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
have 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
Tactic: simp_rw [ofArrows_mem_jointlySurjectivePrecoverage_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
⊢ ∃ (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
have 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)
Tactic: obtain ⟨i, y, rfl⟩ := hf x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨j, z, rfl⟩ := hg i y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use ⟨i, j⟩, z
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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) (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
have 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
Tactic: obtain ⟨Y, f, hf, hx⟩ := hR x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
⊢ ∃ (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
have left : (R ⊔ S) f
Tactic: use Y, f, .inl hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
Goal:
X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
⊢ E.Small
have 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
Tactic: choose i y hy using ofArrows_mem_jointlySurjectivePrecoverage_iff.mp E.mem₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
have refine : (E.restrictIndex i).presieve₀ ∈ jointlySurjectivePrecoverage.coverings X
Tactic: refine ⟨X, i, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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.restrictIndex i).presieve₀ ∈ jointlySurjectivePrecoverage.coverings X
have 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
Tactic: rw [ofArrows_mem_jointlySurjectivePrecoverage_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
⊢ ∃ (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
have w : (E.restrictIndex i).I₀
Tactic: use x, y x, hy x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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₀
⊢ ∃ (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
have w₁ : (fun (X : Type u) ↦ X) ((E.restrictIndex i).X x)
Tactic: use x, y x, hy x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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)
⊢ ∃ (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
have 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
Tactic: use x, y x, hy x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
have 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
Tactic: refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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 : 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
have 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
Tactic: obtain ⟨-, -, ⟨hf⟩, hi⟩ := h x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.JointlySurjective (goal)
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 : 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
have 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
Tactic: obtain ⟨Y, g, hg, hi⟩ := h x