awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
a :
  Coverage.Saturate.{v_1, u_1} (regularCoverage C) X
    (Sieve.generate
      (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
        | PUnit.unit => π))
⊢ Sieve.generate
      (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
        | PUnit.unit => π' ≫ π) ∈
    (regularTopology C : (a : C) → Set (Sieve a)) X
have a₁ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
  Sieve.arrows
      (Sieve.generate
        (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
          | PUnit.unit => π))
      f →
    Coverage.Saturate (regularCoverage C) Y_1
      (Sieve.pullback f
        (Sieve.generate
          (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
            | PUnit.unit => π' ≫ π)))
Tactic: apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows (fun () ↦ Y)
      (fun () ↦ π)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
⊢ Coverage.Saturate.{v_1, u_1} (regularCoverage C) X
    (Sieve.generate
      (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
        | PUnit.unit => π))
have a : Membership.mem (γ := Set (Presieve.{v_1, u_1} X)) (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X)
  (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
    match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
    | PUnit.unit => π)
Tactic: apply Coverage.Saturate.of
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
w : C
w₁ : Y ⟶ X
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X)
    (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
have h : Eq (α := Presieve.{v_1, u_1} X)
    (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
    (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π) ∧
  EffectiveEpi π
Tactic: use Y, π
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
⊢ Sieve.arrows
      (Sieve.generate
        (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
          | PUnit.unit => π))
      f →
    Coverage.Saturate (regularCoverage C) V
      (Sieve.pullback f
        (Sieve.generate
          (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
            | PUnit.unit => π' ≫ π)))
have a : ∀ (Y₁ : C) (h : V ⟶ Y₁) (g : Y₁ ⟶ X)
  (hY :
    Presieve.ofArrows (fun (x : Unit) ↦ Y)
      (fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
        | PUnit.unit => π)
      g)
  (hf : h ≫ g = f),
  Coverage.Saturate (regularCoverage C) V
    (Sieve.pullback f
      (Sieve.generate
        (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
          | PUnit.unit => π' ≫ π)))
Tactic: ⟨Y₁, h, g, ⟨hY, hf⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY :
  Presieve.ofArrows (fun (x : Unit) ↦ Y)
    (fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
    g
hf : h ≫ g = f
⊢ Coverage.Saturate (regularCoverage C) V
    (Sieve.pullback f
      (Sieve.generate
        (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
          | PUnit.unit => π' ≫ π)))
have a : Coverage.Saturate (regularCoverage C) V
  (Sieve.pullback h
    (Sieve.pullback g
      (Sieve.generate
        (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
          | PUnit.unit => π' ≫ π))))
Tactic: rw [← hf, Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY :
  Presieve.ofArrows (fun (x : Unit) ↦ Y)
    (fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
    g
hf : h ≫ g = f
⊢ Coverage.Saturate (regularCoverage C) V
    (Sieve.pullback h
      (Sieve.pullback g
        (Sieve.generate
          (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
            | PUnit.unit => π' ≫ π))))
have a : Membership.mem (γ := Set (Sieve.{v_1, u_1} Y₁)) (GrothendieckTopology.sieves (regularTopology C) Y₁)
  (Sieve.pullback g
    (Sieve.generate
      (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
        | PUnit.unit => π' ≫ π)))
Tactic: apply (regularTopology C).pullback_stable'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY :
  Presieve.ofArrows (fun (x : Unit) ↦ Y)
    (fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
    g
hf : h ≫ g = f
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} Y₁)) (GrothendieckTopology.sieves (regularTopology C) Y₁)
    (Sieve.pullback g
      (Sieve.generate
        (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
          | PUnit.unit => π' ≫ π)))
have a : ∃ (Y_1 : C) (π_1 : Y_1 ⟶ Y₁),
  EffectiveEpi π_1 ∧
    (Sieve.pullback g
          (Sieve.generate
            (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
              match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
              | PUnit.unit => π' ≫ π))).arrows
      π_1
Tactic: apply regularTopology.mem_sieves_of_hasEffectiveEpi
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY :
  Presieve.ofArrows (fun (x : Unit) ↦ Y)
    (fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
    g
hf : h ≫ g = f
⊢ ∃ (Y_1 : C) (π_1 : Y_1 ⟶ Y₁),
    EffectiveEpi π_1 ∧
      (Sieve.pullback g
            (Sieve.generate
              (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
                match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
                | PUnit.unit => π' ≫ π))).arrows
        π_1
have a : ∀ (i : Unit) (h : V ⟶ Y)
  (hf :
    (h ≫
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) i with
        | PUnit.unit => π) =
      f),
  ∃ (Y_1 : C) (π_1 : Y_1 ⟶ Y),
    EffectiveEpi π_1 ∧
      Sieve.arrows
        (Sieve.pullback (X := X)
          (match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) i with
          | PUnit.unit => π)
          (Sieve.generate
            (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
              match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
              | PUnit.unit => π' ≫ π)))
        π_1
Tactic: cases hY
Cleared hypotheses: Y₁, h, g, hY, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
⊢ S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
have mp : S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X → ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
mp : S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X → ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
⊢ S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
have mpr : (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y : C
T : Presieve.{v_1, u_1} Y
hS :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) Y) T
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π
have mp : ∀ (Y' : C) (π : Y' ⟶ Y) (h' : (T = Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦ π) ∧ EffectiveEpi π),
  ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π
Tactic: rcases hS with ⟨Y', π, h'⟩
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y : C
T : Presieve.{v_1, u_1} Y
Y' : C
π : Y' ⟶ Y
h' : (T = Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦ π) ∧ EffectiveEpi π
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π
have mp : (Sieve.generate T).arrows π
Tactic: refine ⟨Y', π, h'.2, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y : C
T : Presieve.{v_1, u_1} Y
Y' : C
π : Y' ⟶ Y
h' : (T = Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦ π) ∧ EffectiveEpi π
⊢ (Sieve.generate T).arrows π
have mp : EffectiveEpi π → Sieve.arrows (Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦ π)) π
Tactic: rcases h' with ⟨rfl, _⟩
Cleared hypotheses: T, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S_1 : Sieve.{v_1, u_1} X
Y : C
R S : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (regularCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (regularCoverage C) Y_1 (Sieve.pullback f S)
a : ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ R.arrows π
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ (Y_2 : C) (π : Y_2 ⟶ Y_1), EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π
have mp : ∀ (Y₁ : C) (π : Y₁ ⟶ Y) (h₁ : EffectiveEpi π) (h₂ : R.arrows π), ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π
Tactic: rcases a with ⟨Y₁, π, ⟨h₁, h₂⟩⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S_1 : Sieve.{v_1, u_1} X
Y : C
R S : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (regularCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (regularCoverage C) Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ (Y_2 : C) (π : Y_2 ⟶ Y_1), EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π
have mp : ∀ (Y' : C) (π' : Y' ⟶ Y₁),
  EffectiveEpi π' → ∀ (H : (Sieve.pullback π S).arrows π'), ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π
Tactic: choose Y' π' _ H using b h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
h : S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
have mp : ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
  (hS :
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
      (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) Y) T),
  ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π
Tactic: induction h with
    | of Y T hS =>
      rcases hS with ⟨Y', π, h'⟩
      refine ⟨Y', π, h'.2, ?_⟩
      rcases h' with ⟨rfl, _⟩
      exact ⟨Y', 𝟙 Y', π, Presieve.ofArrows.mk (), (by simp)⟩
    | top Y => exact ⟨Y, (𝟙 Y), inferInstance, by simp only [Sieve.top_apply]⟩
    | transitive Y R S _ _ a b =>
      rcases a with ⟨Y₁, π, ⟨h₁, h₂⟩⟩
      choose Y' π' _ H using b h₂
      exact ⟨Y', π' ≫ π, inferInstance, (by simpa using H)⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
h : S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X
mp :
  ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
    (hS :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) Y) T),
    ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
have mp₁ : ∀ (Y : C), ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ Sieve.arrows ⊤ π
Tactic: induction h with
    | of Y T hS =>
      rcases hS with ⟨Y', π, h'⟩
      refine ⟨Y', π, h'.2, ?_⟩
      rcases h' with ⟨rfl, _⟩
      exact ⟨Y', 𝟙 Y', π, Presieve.ofArrows.mk (), (by simp)⟩
    | top Y => exact ⟨Y, (𝟙 Y), inferInstance, by simp only [Sieve.top_apply]⟩
    | transitive Y R S _ _ a b =>
      rcases a with ⟨Y₁, π, ⟨h₁, h₂⟩⟩
      choose Y' π' _ H using b h₂
      exact ⟨Y', π' ≫ π, inferInstance, (by simpa using H)⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
h : S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X
mp :
  ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
    (hS :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) Y) T),
    ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π
mp₁ : ∀ (Y : C), ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ Sieve.arrows ⊤ π
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
have mp₂ : ∀ (Y : C) (R S : Sieve.{v_1, u_1} Y),
  Coverage.Saturate (regularCoverage C) Y R →
    (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (regularCoverage C) Y_1 (Sieve.pullback f S)) →
      ∀ (a : ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ R.arrows π)
        (b :
          ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
            R.arrows f → ∃ (Y_2 : C) (π : Y_2 ⟶ Y_1), EffectiveEpi π ∧ (Sieve.pullback f S).arrows π),
        ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π
Tactic: induction h with
    | of Y T hS =>
      rcases hS with ⟨Y', π, h'⟩
      refine ⟨Y', π, h'.2, ?_⟩
      rcases h' with ⟨rfl, _⟩
      exact ⟨Y', 𝟙 Y', π, Presieve.ofArrows.mk (), (by simp)⟩
    | top Y => exact ⟨Y, (𝟙 Y), inferInstance, by simp only [Sieve.top_apply]⟩
    | transitive Y R S _ _ a b =>
      rcases a with ⟨Y₁, π, ⟨h₁, h₂⟩⟩
      choose Y' π' _ H using b h₂
      exact ⟨Y', π' ≫ π, inferInstance, (by simpa using H)⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X)
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
    (F.obj (op (n + 1))).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')),
    Eq (α := (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (InducedCategory.Hom.hom (F.map (Quiver.Hom.op (homOfLE ⋯)))) (op X')) :
            (a : (fun (X : Type v) ↦ X) ((F.obj (op (n + 1))).obj.obj (op X'))) →
              (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X')))
          x :
        (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map φ.op) :
            (a : (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X))) →
              (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X')))
          y :
        (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))
have this : Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE sorry).op)
Tactic: have := hF n
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X)
this : Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
    (F.obj (op (n + 1))).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')),
    Eq (α := (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (InducedCategory.Hom.hom (F.map (Quiver.Hom.op (homOfLE ⋯)))) (op X')) :
            (a : (fun (X : Type v) ↦ X) ((F.obj (op (n + 1))).obj.obj (op X'))) →
              (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X')))
          x :
        (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map φ.op) :
            (a : (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X))) →
              (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X')))
          y :
        (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))
have this₁ : ∀ (X : C) (y : ToType (FC := TypeCat.Fun) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))),
  ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
    ToType (FC := TypeCat.Fun) ((F.obj (op n.succ)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))),
    Eq (α := (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map (homOfLE sorry).op).hom.app (op X')) :
            (a : (F.obj (op n.succ)).obj.obj (op X')) → (F.obj (op n)).obj.obj (op X'))
          x :
        (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map (op φ)) :
            (a : (F.obj (op n)).obj.obj (op X)) → (F.obj (op n)).obj.obj (op X'))
          y :
        (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
Tactic: rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
⊢ Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F₁ :=
    Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)) (c.π.app (op 0))
have rw : ∀ (X : C) (y : ToType (FC := TypeCat.Fun) ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))),
  ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
    ToType (FC := TypeCat.Fun)
      ((Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)).obj (P :=
            Presheaf.IsSheaf (coherentTopology C)).obj
        (op X'))),
    Eq (α := (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (InducedCategory.Hom.hom (c.π.app (op 0))) (op X')) :
            (a : (((Functor.const ℕᵒᵖ).obj c.pt).obj (op 0)).obj.obj (op X')) → (F.obj (op 0)).obj.obj (op X'))
          x :
        (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map (op φ)) :
            (a : (F.obj (op 0)).obj.obj (op X)) → (F.obj (op 0)).obj.obj (op X'))
          y :
        (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
Tactic: rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff]