awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
F : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim
        (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim
              (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i ⟶
            S)
        i with
      | Sum.inl i =>
        Iso.hom (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
⊢ E ≅ F
have refine_1 : (i : E.I₀) → E.X i ≅ F.X ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) i)
Tactic: refine PreZeroHypercover.isoMk (Equiv.refl _) (fun i ↦ ?_) (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
F : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim
        (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim
              (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i ⟶
            S)
        i with
      | Sum.inl i =>
        Iso.hom (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i_1 : E.I₀
i : (↑R.uncurry : Type (max u v))
⊢ E.X (Sum.inl i) ≅ F.X ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) (Sum.inl i))
have dsimp : (↑i : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S) ≅ YR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) sorry
Tactic: dsimp [E, F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
F : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim
        (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim
              (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i ⟶
            S)
        i with
      | Sum.inl i =>
        Iso.hom (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i_1 : E.I₀
i : (↑R.uncurry : Type (max u v))
⊢ (↑i : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S) ≅
    YR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯
have symm : YR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) sorry ≅ (↑i : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
F : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim
        (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim
              (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i ⟶
            S)
        i with
      | Sum.inl i =>
        Iso.hom (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i_1 : E.I₀
i : (↑T.uncurry : Type (max u v))
⊢ E.X (Sum.inr i) ≅ F.X ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) (Sum.inr i))
have dsimp : YT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) sorry ≅ (↑i : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)
Tactic: dsimp [E, F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ F.presieve₀ ∈ J.coverings S
have refine_1 : ∀ ⦃Z : C⦄ (g : Z ⟶ S), E.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), F.presieve₀ (e.hom ≫ g)
Tactic: refine Precoverage.RespectsIso.of_forall_exists_iso ?_ ?_ hE
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
refine_1 : ∀ ⦃Z : C⦄ (g : Z ⟶ S), E.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), F.presieve₀ (e.hom ≫ g)
⊢ F.presieve₀ ∈ J.coverings S
have refine_2 : ∀ ⦃Z : C⦄ (g : Z ⟶ S), F.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), E.presieve₀ (e.hom ≫ g)
Tactic: refine Precoverage.RespectsIso.of_forall_exists_iso ?_ ?_ hE
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g : Z ⟶ S
⊢ E.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), F.presieve₀ (e.hom ≫ g)
have refine_1 : ∀ (i : E.I₀), ∃ (Y : C) (e : Y ≅ E.X i), F.presieve₀ (e.hom ≫ E.f i)
Tactic: ⟨i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g : Z ⟶ S
i : E.I₀
⊢ ∃ (Y : C) (e : Y ≅ E.X i), F.presieve₀ (e.hom ≫ E.f i)
have h : F.presieve₀ ((asIso (e.hom.h₀ i)).symm.hom ≫ E.f i)
Tactic: use F.X (e.hom.s₀ i), (asIso (e.hom.h₀ i)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g : Z ⟶ S
⊢ F.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), E.presieve₀ (e.hom ≫ g)
have refine_2 : ∀ (i : F.I₀), ∃ (Y : C) (e : Y ≅ F.X i), E.presieve₀ (e.hom ≫ F.f i)
Tactic: ⟨i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g : Z ⟶ S
i : F.I₀
⊢ ∃ (Y : C) (e : Y ≅ F.X i), E.presieve₀ (e.hom ≫ F.f i)
have h : E.presieve₀ ((asIso (e.inv.h₀ i)).symm.hom ≫ F.f i)
Tactic: use E.X (e.inv.s₀ i), (asIso (e.inv.h₀ i)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.IsStableUnderComposition
E : ZeroHypercover.{w, v, u} J T
F : ZeroHypercover.{w', v, u} J T
inst_3 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
⊢ (PreZeroHypercover.inter.{w', w, v, u} E.toPreZeroHypercover F.toPreZeroHypercover).presieve₀ ∈ J.coverings T
have rw : (PreZeroHypercover.bind.{w', w, v, u} E.toPreZeroHypercover fun (i : E.I₀) ↦
      PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).presieve₀ ∈
  J.coverings T
Tactic: rw [PreZeroHypercover.inter_def, PreZeroHypercover.presieve₀_reindex]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
inst_1 : J.IsStableUnderSup
E : ZeroHypercover.{w, v, u} J S
F : ZeroHypercover.{w', v, u} J S
⊢ (PreZeroHypercover.sum.{w', w, v, u} E.toPreZeroHypercover F.toPreZeroHypercover).presieve₀ ∈ J.coverings S
have rw : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover ⊔
    PreZeroHypercover.presieve₀.{w', v, u} F.toPreZeroHypercover ∈
  J.coverings S
Tactic: rw [PreZeroHypercover.presieve₀_sum]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F_1 : Functor.{v, v_1, u, u_1} C D
K : Precoverage.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
E : ZeroHypercover.{w, v, u} J S
h : J ≤ comap F K
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (K.coverings (F.obj S))
    (PreZeroHypercover.presieve₀.{w, v_1, u_1} (PreZeroHypercover.map F E.toPreZeroHypercover))
have rw : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover ∈ (comap F K).coverings S
Tactic: rw [PreZeroHypercover.presieve₀_map, ← mem_comap_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
E : ZeroHypercover.{w, v, u} J S
⊢ ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S
have obtain : ∀ (ι : Type (max u v)) (Y : ι → C) (f : (i : ι) → Y i ⟶ S)
  (h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f),
  ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S
Tactic: obtain ⟨ι, Y, f, h⟩ := E.presieve₀.exists_eq_ofArrows
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
E : ZeroHypercover.{w, v, u} J S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
Z : C
g : Z ⟶ S
hg : Presieve.ofArrows Y f g
⊢ ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j
have obtain : ∀ ⦃Y_1 : C⦄ (j : E.I₀) (hg : Presieve.ofArrows Y f (E.f j)),
  ∃ (j_1 : E.I₀) (h : E.X j = E.X j_1), E.f j = eqToHom h ≫ E.f j_1
Tactic: obtain ⟨j⟩ : E.presieve₀ g := by rwa [h]
Cleared hypotheses: Z, g, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
E : ZeroHypercover.{w, v, u} J S
ι : Type (max u v)
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y_1 f
Y : C
j : E.I₀
hg : Presieve.ofArrows Y_1 f (E.f j)
⊢ ∃ (j_1 : E.I₀) (h : E.X j = E.X j_1), E.f j = eqToHom h ≫ E.f j_1
have h₁ : E.f j = eqToHom sorry ≫ E.f j
Tactic: use j, rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
E : ZeroHypercover.{w, v, u} J S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
⊢ ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S
have this : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j
Tactic: have (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g) :
        ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j := by
      obtain ⟨j⟩ : E.presieve₀ g := by rwa [h]
      use j, rfl
      simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
E : ZeroHypercover.{w, v, u} J S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
this : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j
⊢ ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S
have choose : ∀ (j : (Z : C) → (g : Z ⟶ S) → (hg : Presieve.ofArrows Y f g) → E.I₀)
  (h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg))
  (h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom sorry ≫ E.f (j Z g hg)),
  ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S
Tactic: choose j h₁ h₂ using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
E : ZeroHypercover.{w, v, u} J S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
j : (Z : C) → (g : Z ⟶ S) → (hg : Presieve.ofArrows Y f g) → E.I₀
h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg)
h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)
⊢ ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S
have refine : (E.restrictIndex fun (i : ι) ↦ j (Y i) (f i) sorry).presieve₀ ∈ J.coverings S
Tactic: refine ⟨ι, fun i ↦ j _ _ (.mk i), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
E : ZeroHypercover.{w, v, u} J S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
j : (Z : C) → (g : Z ⟶ S) → (hg : Presieve.ofArrows Y f g) → E.I₀
h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg)
h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)
⊢ (E.restrictIndex fun (i : ι) ↦ j (Y i) (f i) ⋯).presieve₀ ∈ J.coverings S
have h₃ : (E.restrictIndex fun (i : ι) ↦ j (Y i) (f i) sorry).presieve₀ = PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover
Tactic: convert! E.mem₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T_1 : C
E : ZeroHypercover.{w, v, u} J S
inst_1 : E.Small
T : C
f : T ⟶ S
inst_2 : J.IsStableUnderBaseChange
inst_3 : ∀ (i : E.I₀), HasPullback f (E.f i)
⊢ (pullback₁ f E).Small
have h : PreZeroHypercover.presieve₀.{w', v, u}
    (PreZeroHypercover.restrictIndex.{w', w, v, u} (pullback₁ f E).toPreZeroHypercover (ι := Small.Index E)
      (Small.restrictFun E)) ∈
  J.coverings T
Tactic: use Small.Index E, Small.restrictFun E
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T_1 : C
E : ZeroHypercover.{w, v, u} J S
inst_1 : E.Small
T : C
f : T ⟶ S
inst_2 : J.IsStableUnderBaseChange
inst_3 : ∀ (i : E.I₀), HasPullback f (E.f i)
i : E.restrictIndexOfSmall.I₀
⊢ HasPullback f (E.restrictIndexOfSmall.f i)
have dsimp : HasPullback (Y := E.X (Small.restrictFun E i)) f (E.f (Small.restrictFun E i))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T_1 : C
E : ZeroHypercover.{w, v, u} J S
inst_1 : E.Small
T : C
f : T ⟶ S
inst_2 : J.IsStableUnderBaseChange
inst_3 : ∀ (i : E.I₀), HasPullback f (E.f i)
⊢ PreZeroHypercover.presieve₀.{w', v, u}
      (PreZeroHypercover.restrictIndex.{w', w, v, u} (pullback₁ f E).toPreZeroHypercover (ι := Small.Index E)
        (Small.restrictFun E)) ∈
    J.coverings T
have x : ∀ (i : E.restrictIndexOfSmall.I₀), HasPullback f (E.restrictIndexOfSmall.f i)
Tactic: have _ (i) : HasPullback f (E.restrictIndexOfSmall.f i) := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
X : C
R : Presieve.{v, u} X
⊢ R ∈ J.coverings X ↔ ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
have refine : ∀ (hR : R ∈ J.coverings X), ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
Tactic: refine ⟨fun hR ↦ ?_, fun ⟨𝒰, hR⟩ ↦ hR ▸ 𝒰.mem₀⟩