awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h_1 : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows Y π g
hf : h ≫ g = f
⊢ ∃ (α_1 : Type) (_ : Finite α_1) (Y_1 : α_1 → C) (π_1 : (a : α_1) → Y_1 a ⟶ Y₁),
    EffectiveEpiFamily Y_1 π_1 ∧
      ∀ (a : α_1),
        (Sieve.pullback g
              (Sieve.generate
                (Presieve.ofArrows
                  (fun (x : (x : α) × β x) ↦
                    match (motive := (x : α) × β x → C) x with
                    | ⟨a, b⟩ => Y_n a b)
                  fun (x : (x : α) × β x) ↦
                  match (motive :=
                    (x : (x : α) × β x) →
                      (fun (x : (x : α) × β x) ↦
                            (match (motive := (x : α) × β x → C) x with
                              | ⟨a, b⟩ => Y_n a b :
                              C))
                          x ⟶
                        X)
                    x with
                  | ⟨a, b⟩ => π_n a b ≫ π a))).arrows
          (π_1 a)
have a : ∀ ⦃Y_1 : C⦄ (i : α) (h : V ⟶ Y i) (hf : h ≫ π i = f),
  ∃ (α_1 : Type) (_ : Finite α_1) (Y_2 : α_1 → C) (π_1 : (a : α_1) → Y_2 a ⟶ Y i),
    EffectiveEpiFamily Y_2 π_1 ∧
      ∀ (a : α_1),
        (Sieve.pullback (π i)
              (Sieve.generate
                (Presieve.ofArrows
                  (fun (x : (x : α) × β x) ↦
                    match (motive := (x : α) × β x → C) x with
                    | ⟨a, b⟩ => Y_n a b)
                  fun (x : (x : α) × β x) ↦
                  match (motive :=
                    (x : (x : α) × β x) →
                      (fun (x : (x : α) × β x) ↦
                            (match (motive := (x : α) × β x → C) x with
                              | ⟨a, b⟩ => Y_n a b :
                              C))
                          x ⟶
                        X)
                    x with
                  | ⟨a, b⟩ => π_n a b ≫ π a))).arrows
          (π_1 a)
Tactic: obtain ⟨i⟩ := hY
Cleared hypotheses: Y₁, h, g, hY, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y Z : α → C
π : (a : α) → Y a ⟶ X
inst_3 : EffectiveEpiFamily Y π
f : (a : α) → Z a ⟶ Y a
h : ∀ (a : α), EffectiveEpi (f a)
⊢ EffectiveEpiFamily.{v_1, u_1, 0} (B := X) Z fun (a : α) ↦ f a ≫ π a
have h₁ : ∀ (a : α), EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y a) (fun (x : Unit) ↦ Z a) fun (x : Unit) ↦ f a
Tactic: simp_rw [effectiveEpi_iff_effectiveEpiFamily] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
have mp : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X →
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
mp :
  S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X →
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
have mpr : (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
  S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{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 (coherentCoverage C)) Y) T
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
have mp : ∀ (a : Type) (h : Finite a) (Y' : a → C) (π : (a : a) → Y' a ⟶ Y) (h' : T = Presieve.ofArrows Y' π),
  EffectiveEpiFamily Y' π →
    ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
      EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
Tactic: obtain ⟨a, h, Y', π, h', _⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y : C
T : Presieve.{v_1, u_1} Y
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π
right : EffectiveEpiFamily Y' π
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
have mp : ∀ (a' : a), (Sieve.generate T).arrows (π a')
Tactic: refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y : C
T : Presieve.{v_1, u_1} Y
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π
right : EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate T).arrows (π a')
have mp : (Sieve.generate (Presieve.ofArrows Y' π)).arrows (π a')
Tactic: obtain ⟨rfl, _⟩ := h'
Cleared hypotheses: T, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{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 (coherentCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
a :
  ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∃ (α : Type) (_ : Finite α) (Y_2 : α → C) (π : (a : α) → Y_2 a ⟶ Y_1),
        EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
have mp : ∀ (α : Type) (w : Finite α) (Y₁ : α → C) (π : (a : α) → Y₁ a ⟶ Y) (h₁ : EffectiveEpiFamily Y₁ π)
  (h₂ : ∀ (a : α), R.arrows (π a)),
  ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic: obtain ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{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 (coherentCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∃ (α : Type) (_ : Finite α) (Y_2 : α → C) (π : (a : α) → Y_2 a ⟶ Y_1),
        EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
have mp : ∀ (β : (a : α) → Type),
  (∀ (a : α), Finite (β a)) →
    ∀ (Y_n : (a : α) → β a → C) (π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a)
      (H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)),
      ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
        EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic: choose β _ Y_n π_n H using fun a => b (h₂ a)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
h : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
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 (coherentCoverage C)) Y) T),
  ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
Tactic: induction h with
    | of Y T hS =>
      obtain ⟨a, h, Y', π, h', _⟩ := hS
      refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
      obtain ⟨rfl, _⟩ := h'
      exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩
    | top Y =>
      exact ⟨Unit, inferInstance, fun _ => Y, fun _ => (𝟙 Y), inferInstance, by simp⟩
    | transitive Y R S _ _ a b =>
      obtain ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩ := a
      choose β _ Y_n π_n H using fun a => b (h₂ a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
        fun c => (H c.fst).2 c.snd⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
h : S ∈ (coherentTopology 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 (coherentCoverage C)) Y) T),
    ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
      EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
have mp₁ : ∀ (Y : C),
  ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), Sieve.arrows ⊤ (π a)
Tactic: induction h with
    | of Y T hS =>
      obtain ⟨a, h, Y', π, h', _⟩ := hS
      refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
      obtain ⟨rfl, _⟩ := h'
      exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩
    | top Y =>
      exact ⟨Unit, inferInstance, fun _ => Y, fun _ => (𝟙 Y), inferInstance, by simp⟩
    | transitive Y R S _ _ a b =>
      obtain ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩ := a
      choose β _ Y_n π_n H using fun a => b (h₂ a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
        fun c => (H c.fst).2 c.snd⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
h : S ∈ (coherentTopology 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 (coherentCoverage C)) Y) T),
    ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
      EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
mp₁ :
  ∀ (Y : C),
    ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
      EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), Sieve.arrows ⊤ (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
have mp₂ : ∀ (Y : C) (R S : Sieve.{v_1, u_1} Y),
  Coverage.Saturate (coherentCoverage C) Y R →
    (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)) →
      ∀
        (a :
          ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
            EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), R.arrows (π a))
        (b :
          ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
            R.arrows f →
              ∃ (α : Type) (_ : Finite α) (Y_2 : α → C) (π : (a : α) → Y_2 a ⟶ Y_1),
                EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)),
        ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
          EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic: induction h with
    | of Y T hS =>
      obtain ⟨a, h, Y', π, h', _⟩ := hS
      refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
      obtain ⟨rfl, _⟩ := h'
      exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩
    | top Y =>
      exact ⟨Unit, inferInstance, fun _ => Y, fun _ => (𝟙 Y), inferInstance, by simp⟩
    | transitive Y R S _ _ a b =>
      obtain ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩ := a
      choose β _ Y_n π_n H using fun a => b (h₂ a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
        fun c => (H c.fst).2 c.snd⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
have hp : (EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (x : PUnit.{1}) ↦ Z) fun (x : PUnit.{1}) ↦
    match (motive := (x : PUnit.{1}) → (fun (x : PUnit.{1}) ↦ Z) x ⟶ Y) x with
    | PUnit.unit => g) →
  ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
    EffectiveEpiFamily X₂ π₂ ∧
      ∃ (i : β → PUnit.{1}) (ι : (b : β) → X₂ b ⟶ Z),
        ∀ (b : β),
          (ι b ≫
              match (motive := (x : PUnit.{1}) → (fun (x : PUnit.{1}) ↦ Z) x ⟶ Y) i b with
              | PUnit.unit => g) =
            π₂ b ≫ f
Tactic: have hp := Precoherent.pullback f PUnit (fun () ↦ Z) (fun () ↦ g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
hp :
  (EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (x : PUnit.{1}) ↦ Z) fun (x : PUnit.{1}) ↦
      match (motive := (x : PUnit.{1}) → (fun (x : PUnit.{1}) ↦ Z) x ⟶ Y) x with
      | PUnit.unit => g) →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧
        ∃ (i : β → PUnit.{1}) (ι : (b : β) → X₂ b ⟶ Z),
          ∀ (b : β),
            (ι b ≫
                match (motive := (x : PUnit.{1}) → (fun (x : PUnit.{1}) ↦ Z) x ⟶ Y) i b with
                | PUnit.unit => g) =
              π₂ b ≫ f
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
have hp₁ : (EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (x : PUnit.{1}) ↦ Z) fun (x : PUnit.{1}) ↦ g) →
  ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
Tactic: simp only [exists_const] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
hp :
  (EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (x : PUnit.{1}) ↦ Z) fun (x : PUnit.{1}) ↦ g) →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
have hp₁ : EffectiveEpi g →
  ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
Tactic: rw [← effectiveEpi_iff_effectiveEpiFamily g] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
hp :
  EffectiveEpi g →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
have obtain : ∀ (β : Type),
  Finite β →
    ∀ (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X) (h : EffectiveEpiFamily X₂ π₂) (ι : (b : β) → X₂ b ⟶ Z)
      (hι : ∀ (b : β), ι b ≫ g = π₂ b ≫ f), ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
Tactic: obtain ⟨β, _, X₂, π₂, h, ι, hι⟩ := hp inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h_1 : EffectiveEpi g
hp :
  EffectiveEpi g →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
β : Type
w : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ X
h : EffectiveEpiFamily X₂ π₂
ι : (b : β) → X₂ b ⟶ Z
hι : ∀ (b : β), ι b ≫ g = π₂ b ≫ f
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
have refine : Eq (α := sigmaObj.{0, v_1, u_1} X₂ ⟶ Y) (Sigma.desc ι ≫ g) (Sigma.desc π₂ ≫ f)
Tactic: refine ⟨∐ X₂, Sigma.desc π₂, inferInstance, Sigma.desc ι, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h_1 : EffectiveEpi g
hp :
  EffectiveEpi g →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
β : Type
w : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ X
h : EffectiveEpiFamily X₂ π₂
ι : (b : β) → X₂ b ⟶ Z
hι : ∀ (b : β), ι b ≫ g = π₂ b ≫ f
⊢ Eq (α := sigmaObj.{0, v_1, u_1} X₂ ⟶ Y) (Sigma.desc ι ≫ g) (Sigma.desc π₂ ≫ f)
have h₁ : ∀ (b : β),
  CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X₂) (Sigma.ι X₂ b) (Sigma.desc ι ≫ g) =
    CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X₂) (Sigma.ι X₂ b) (Sigma.desc π₂ ≫ f)
Tactic: ext b
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
⊢ ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : β → α) (ι : (b : β) → X₂ b ⟶ X₁ (i b)), ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
have refine : ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
  EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
Tactic: refine ⟨α, inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
⊢ ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
have obtain : ∀ (Y : C) (g : Y ⟶ B₂),
  EffectiveEpi g →
    ∀ (g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁) (hg : g' ≫ Sigma.desc π₁ = g ≫ f),
      ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
        EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
Tactic: obtain ⟨Y, g, _, g', hg⟩ := Preregular.exists_fac f (Sigma.desc π₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
⊢ ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
have x : IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
  (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
Tactic: have _ := FinitaryPreExtensive.isIso_sigmaDesc_fst (fun a ↦ Sigma.ι X₁ a) g' inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
⊢ ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
have refine_1 : EffectiveEpiFamily X₂ π₂
Tactic: refine ⟨X₂, π₂, ?_, ?_⟩