awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
a : α
W : C
g₁ : W ⟶ X
g₂ : Y a ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π a = g₂ ≫ F.map g₁
⊢ S.arrows (F.preimage (g₀ a ≫ π a))
have refine_2 : S.arrows (F.preimage (g₀ a ≫ g₂ ≫ F.map g₁))
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
a : α
W : C
g₁ : W ⟶ X
g₂ : Y a ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π a = g₂ ≫ F.map g₁
⊢ S.arrows (F.preimage (g₀ a ≫ g₂ ≫ F.map g₁))
have h : F.preimage (g₀ a ≫ g₂ ≫ F.map g₁) = F.preimage (g₀ a ≫ g₂) ≫ g₁
Tactic: convert! S.downward_closed h₁ (F.preimage (g₀ a ≫ g₂))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
⊢ coherentTopology C = F.inducedTopology (coherentTopology D)
have h : ∀ (X : C) (S : Sieve.{v_1, u_1} X),
  S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
    S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
Tactic: ext X S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
    S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
have this : Precoherent.{v_1, u_1} C
Tactic: have := F.reflects_precoherent
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
this : Precoherent.{v_1, u_1} C
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
    S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
have h : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic: rw [← exists_effectiveEpiFamily_iff_mem_induced F X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
this : Precoherent.{v_1, u_1} C
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
have h : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
Tactic: rw [← coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily S]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
⊢ ∀ {X : C} {S : Sieve.{v_1, u_1} X},
    Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj X))) ((coherentTopology D : (a : D) → Set (Sieve a)) (F.obj X))
        (Sieve.functorPushforward F S) ↔
      S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
have rw : ∀ {X : C} {S : Sieve.{v_1, u_1} X},
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj X))) ((coherentTopology D : (a : D) → Set (Sieve a)) (F.obj X))
      (Sieve.functorPushforward F S) ↔
    S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
Tactic: rw [eq_induced F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
⊢ F.IsCoverDense (regularTopology D)
have refine : ∀ (B : D),
  Sieve.generate
      (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
        (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B)) ∈
    (regularTopology D : (a : D) → Set (Sieve a)) B
Tactic: refine F.isCoverDense_of_generate_singleton_functor_π_mem _ fun B ↦ ⟨_, F.effectiveEpiOver B, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
B : D
⊢ Sieve.generate
      (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
        (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B)) ∈
    (regularTopology D : (a : D) → Set (Sieve a)) B
have hS : Membership.mem (γ := Set (Presieve.{v_2, u_2} B)) (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage D)) B)
  (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
    (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B))
Tactic: apply Coverage.Saturate.of
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
B : D
⊢ Membership.mem (γ := Set (Presieve.{v_2, u_2} B))
    (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage D)) B)
    (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B))
have hS : Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
    (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) =
  Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦ F.effectiveEpiOver B
Tactic: refine ⟨F.effectiveEpiOverObj B, F.effectiveEpiOver B, ?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
B : D
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) =
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦ F.effectiveEpiOver B
have hS : ∀ (x : D) (x_1 : x ⟶ B),
  Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 =
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
B x : D
x_1 : x ⟶ B
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 =
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1
have hS : Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
    (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 ↔
  Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
B x : D
x_1 : x ⟶ B
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 ↔
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1
have hS : Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1 →
  Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
    (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1
Tactic: refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
⊢ (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) ↔
    S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
have refine_1 : (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) →
  ∀ (Y : C) (π : Y ⟶ X) (H₁ : EffectiveEpi π) (H₂ : S.arrows π),
    S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Tactic: refine ⟨fun ⟨Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
refine_1 :
  (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) →
    ∀ (Y : C) (π : Y ⟶ X) (H₁ : EffectiveEpi π) (H₂ : S.arrows π),
      S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
⊢ (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) ↔
    S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
have refine_2 : ∀ (hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X),
  ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
Tactic: refine ⟨fun ⟨Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
h : ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
have refine_1 : ∃ (Y : D) (π : Y ⟶ F.obj X), EffectiveEpi π ∧ (Sieve.functorPushforward F S).arrows π
Tactic: apply (mem_sieves_iff_hasEffectiveEpi (Sieve.functorPushforward _ S)).mpr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
h : ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ ∃ (Y : D) (π : Y ⟶ F.obj X), EffectiveEpi π ∧ (Sieve.functorPushforward F S).arrows π
have refine_1 : EffectiveEpi (F.map π)
Tactic: refine ⟨F.obj Y, F.map π, ⟨?_, Sieve.image_mem_functorPushforward F S H₂⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
have refine_2 : ∀ (Y : D) (π : Y ⟶ F.obj X) (H₁ : EffectiveEpi π) (H₂ : (Sieve.functorPushforward F S).arrows π),
  ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
Tactic: obtain ⟨Y, π, ⟨H₁, H₂⟩⟩ := (mem_sieves_iff_hasEffectiveEpi _).mp hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
have refine_2 : EffectiveEpi (F.preimage (g₀ ≫ π))
Tactic: refine ⟨_, F.preimage (g₀ ≫ π), ?_, (?_ : S.arrows (F.preimage _))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
refine_2 : EffectiveEpi (F.preimage (g₀ ≫ π))
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
have refine_2₁ : S.arrows (F.preimage (g₀ ≫ π))
Tactic: refine ⟨_, F.preimage (g₀ ≫ π), ?_, (?_ : S.arrows (F.preimage _))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ EffectiveEpi (F.preimage (g₀ ≫ π))
have refine_2 : EffectiveEpi (F.map (F.preimage (g₀ ≫ π)))
Tactic: refine F.effectiveEpi_of_map _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ EffectiveEpi (F.map (F.preimage (g₀ ≫ π)))
have refine_2 : EffectiveEpi (g₀ ≫ π)
Tactic: simp only [map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ S.arrows (F.preimage (g₀ ≫ π))
have refine_2 : ∀ (W : C) (g₁ : W ⟶ X) (g₂ : Y ⟶ F.obj W) (h₁ : S.arrows g₁) (h₂ : π = g₂ ≫ F.map g₁), S.arrows (F.preimage (g₀ ≫ π))
Tactic: obtain ⟨W, g₁, g₂, h₁, h₂⟩ := H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
⊢ S.arrows (F.preimage (g₀ ≫ π))
have refine_2 : S.arrows (F.preimage (g₀ ≫ g₂ ≫ F.map g₁))
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
⊢ S.arrows (F.preimage (g₀ ≫ g₂ ≫ F.map g₁))
have h : F.preimage (g₀ ≫ g₂ ≫ F.map g₁) = F.preimage (g₀ ≫ g₂) ≫ g₁
Tactic: convert! S.downward_closed h₁ (F.preimage (g₀ ≫ g₂))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
⊢ regularTopology C = F.inducedTopology (regularTopology D)
have h : ∀ (X : C) (S : Sieve.{v_1, u_1} X),
  S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔
    S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Tactic: ext X S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
⊢ S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔
    S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
have this : Preregular.{v_1, u_1} C
Tactic: have := F.reflects_preregular
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
this : Preregular.{v_1, u_1} C
⊢ S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔
    S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
have h : S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
Tactic: rw [← exists_effectiveEpi_iff_mem_induced F X]