awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (hypothesis)
Goal:
X : TopCat
U : Opens (↑X : Type u)
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : (↑(G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
c : Set (Under g s)
h : IsChain (fun (x y : Under g s) ↦ Nonempty.{u + 1} (y ⟶ x)) c
f : (↑c : Type u) → Opens (↑X : Type u) :=
  fun (x : (↑c : Type u)) ↦
    unop
      ((StructuredArrow.right (↑x : Under g s)).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c))
t :
  ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (iSup f)))
ht :
  IsGluing (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))) f
    (fun (x : (↑c : Type u)) ↦
      (StructuredArrow.right (↑x : Under g s)).snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c))
    t
right :
  ∀
    (y :
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (iSup f)))),
    (fun
            (s_1 :
              ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj
                  (op (iSup f)))) ↦
          IsGluing (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))) f
            (fun (x : (↑c : Type u)) ↦
              (StructuredArrow.right (↑x : Under g s)).snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
                      CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                        (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
                  c))
            s_1)
        y →
      y = t
⊢ ∃ (ub : Under g s), ∀ a ∈ c, Nonempty.{u + 1} (ub ⟶ a)
have le₁ : iSup f ≤ U
Tactic: have le₁ : iSup f ≤ U := iSup_le <| fun j => leOfHom j.1.hom.1.unop
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (goal)
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
⊢ Epi (X := S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U))
    (S.g.hom.app (op U))
have refine : ∀
  (s :
    (↑(S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
      Type u)),
  ∃ (a :
    (↑(S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
      Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U))
            (S.g.hom.app (op U)) :
          (a : (↑(S.X₂.obj.obj (op U)) : Type u)) → (↑(S.X₃.obj.obj (op U)) : Type u))
        a =
      s
Tactic: refine (AddCommGrpCat.epi_iff_surjective _).mpr (fun s ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (goal)
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
s : (↑(S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
⊢ ∃ (a :
    (↑(S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
      Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U))
            (S.g.hom.app (op U)) :
          (a : (↑(S.X₂.obj.obj (op U)) : Type u)) → (↑(S.X₃.obj.obj (op U)) : Type u))
        a =
      s
have obtain : ∀ (t : Under S.g s) (ht : ∀ (a : Under S.g s), Nonempty.{u + 1} (a ⟶ t) → Nonempty.{u + 1} (t ⟶ a)),
  ∃ (a :
    (↑(S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
      Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U))
            (S.g.hom.app (op U)) :
          (a : (↑(S.X₂.obj.obj (op U)) : Type u)) → (↑(S.X₃.obj.obj (op U)) : Type u))
        a =
      s
Tactic: obtain ⟨t, ht⟩ := exists_maximal_of_chains_bounded
    (structured_arrows_elements_sheaf_chains_bounded S.g s)
    (fun ⟨f⟩ ⟨g⟩ ↦ ⟨g ≫ f⟩)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (hypothesis)
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
s : (↑(S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty.{u + 1} (a ⟶ t) → Nonempty.{u + 1} (t ⟶ a)
⊢ ∃ (a :
    (↑(S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
      Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U))
            (S.g.hom.app (op U)) :
          (a : (↑(S.X₂.obj.obj (op U)) : Type u)) → (↑(S.X₃.obj.obj (op U)) : Type u))
        a =
      s
have tle : unop
    ((StructuredArrow.right t).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
      (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
            CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
              (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
        c)) ≤
  U
Tactic: have tle : t.right.1.unop ≤ U := leOfHom t.hom.1.unop
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (goal)
Goal:
X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
inst_1 : S.X₂.IsFlasque
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
⊢ Epi (S.g.hom.app U ≫ S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i)
have rw : Epi (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i ≫ S.g.hom.app V)
Tactic: rw [← S.g.hom.naturality i]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (hypothesis)
Goal:
X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
inst_1 : S.X₂.IsFlasque
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
⊢ Epi (S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i)
have this : Epi (S.g.hom.app U ≫ S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i)
Tactic: have : Epi (S.g.1.app U ≫ S.X₃.obj.map i) := by
      rw [← S.g.hom.naturality i]
      exact CategoryTheory.epi_comp' inferInstance (epi_of_shortExact hS)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (goal)
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
have pos : ∀ (h1 : p₀ ∈ unop U),
  Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
Tactic: by_cases h1 : p₀ ∈ unop U
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (goal)
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
pos :
  ∀ (h1 : p₀ ∈ unop U),
    Epi (X :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        U)
      (CategoryTheory.Functor.map
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        r)
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
have neg : ∀ (h1 : p₀ ∉ unop U),
  Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
Tactic: by_cases h1 : p₀ ∈ unop U
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (goal)
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
have pos : ∀ (h2 : p₀ ∈ unop V),
  Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
Tactic: by_cases h2 : p₀ ∈ unop V
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (goal)
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
pos :
  ∀ (h2 : p₀ ∈ unop V),
    Epi (X :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        U)
      (CategoryTheory.Functor.map
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        r)
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
have neg : ∀ (h2 : p₀ ∉ unop V),
  Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
Tactic: by_cases h2 : p₀ ∈ unop V
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (goal)
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
h2 : p₀ ∈ unop V
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
have pos : Epi.{v_1, u_1} (X := if p₀ ∈ unop U then A else terminal.{v_1, u_1} C) (eqToHom sorry)
Tactic: simp_all only [skyscraperSheaf_obj_obj, skyscraperSheaf_obj_map, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (goal)
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
h2 : p₀ ∉ unop V
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
have neg : Epi.{v_1, u_1} (C := C) (X := if p₀ ∈ unop U then A else terminal.{v_1, u_1} C) (Y :=
  if p₀ ∈ unop V then A else terminal.{v_1, u_1} C)
  (if h : p₀ ∈ unop V then eqToHom sorry
  else
    IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{v_1, u_1} C = x) ↦ IsTerminal.{v_1, u_1} x) terminalIsTerminal
        (if p₀ ∈ unop V then A else terminal.{v_1, u_1} C) sorry)
      (if p₀ ∈ unop U then A else terminal.{v_1, u_1} C))
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (hypothesis)
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∉ unop U
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
have h2 : p₀ ∉ unop V
Tactic: have h2 : p₀ ∉ unop V := fun hV => h1 (r.unop.le hV)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (hypothesis)
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∉ unop U
h2 : p₀ ∉ unop V
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
have this : IsIso (X :=
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
    U)
  (CategoryTheory.Functor.map
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
    r)
Tactic: have := isIso_of_isTerminal (isTerminalSkyscraperSheafObjObjOfNotMem h1)
        (isTerminalSkyscraperSheafObjObjOfNotMem h2) ((skyscraperSheaf p₀ A).obj.map r)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Functors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f_1 : X ⟶ Y
ι : Type w
U : ι → Opens (↑Y : Type w)
A : Type u_1
inst_1 : Category.{w, u_1} A
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
FA : A → A → Type u_2
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_2 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory A FA (CC := CA)
inst_4 : HasColimits.{w, u_1} A
inst_5 : HasLimits.{w, u_1} A
inst_6 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_7 : PreservesFilteredColimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_8 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ Iso (C := TopCat.Sheaf A Y ⥤ TopCat.Sheaf A X) (Sheaf.pullback A (FA := FA) (CA := CA) f) (sheafPullback A hf)
have refine_1 : (F : TopCat.Sheaf A Y) →
  Functor.obj (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A)
      F ≅
    Functor.obj (sheafPullback A hf) F
Tactic: refine Sheaf.pullbackIso A f ≪≫ NatIso.ofComponents (fun F ↦ ?_) (fun u ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Functors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f_1 : X ⟶ Y
ι : Type w
U : ι → Opens (↑Y : Type w)
A : Type u_1
inst_1 : Category.{w, u_1} A
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
FA : A → A → Type u_2
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_2 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory A FA (CC := CA)
inst_4 : HasColimits.{w, u_1} A
inst_5 : HasLimits.{w, u_1} A
inst_6 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_7 : PreservesFilteredColimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_8 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CA))
X_1 Y_1 : TopCat.Sheaf A Y
u : X_1 ⟶ Y_1
⊢ Eq (α :=
    ObjectProperty.FullSubcategory.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
        (Functor.obj (presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A)
          (Functor.obj (Presheaf.pullback A f)
            (X_1.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w)))))) ⟶
      hf.functor.op ⋙ Y_1.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w))))
    (sheafifyLift (Opens.grothendieckTopology (↑X : Type w))
      (NatTrans.app (Iso.hom ⋯.pullbackIso)
          (X_1.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w)))) ≫
        ⋯.functor.op.whiskerLeft u.hom)
      ⋯)
    (sheafifyLift (Opens.grothendieckTopology (↑X : Type w))
        (NatTrans.app (Iso.hom ⋯.pullbackIso)
          (X_1.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w)))))
        ⋯ ≫
      hf.functor.op.whiskerLeft u.hom)
have refine_2 : Eq (α :=
  ObjectProperty.FullSubcategory.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
      (Functor.obj (presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A)
        (Functor.obj (Presheaf.pullback A f)
          (X_1.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w)))))) ⟶
    hf.functor.op ⋙ Y_1.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w))))
  (sheafifyLift (Opens.grothendieckTopology (↑X : Type w))
      (NatTrans.app (Iso.hom sorry.pullbackIso)
        (X_1.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w)))))
      sorry ≫
    sorry.functor.op.whiskerLeft u.hom)
  (sheafifyLift (Opens.grothendieckTopology (↑X : Type w))
      (NatTrans.app (Iso.hom sorry.pullbackIso)
        (X_1.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w)))))
      sorry ≫
    hf.functor.op.whiskerLeft u.hom)
Tactic: rw [CategoryTheory.sheafifyLift_comp]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
Goal:
X : TopCat
T_1 : (↑X : Type u_2) → Type u_1
T : Type u_3
inst : TopologicalSpace T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) (U := V) fun (x : ↥V) ↦
        f ((i : (a : ↥V) → ↥U) x)
⊢ (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) f
have apply : ∀ (x : ↥U), ContinuousAt f x
Tactic: apply continuous_iff_continuousAt.2
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (hypothesis)
Goal:
X : TopCat
T_1 : (↑X : Type u_2) → Type u_1
T : Type u_3
inst : TopologicalSpace T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) (U := V) fun (x : ↥V) ↦
        f ((i : (a : ↥V) → ↥U) x)
x : ↥U
⊢ ContinuousAt f x
have w₁ : ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
  (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
Tactic: specialize w x
Cleared hypotheses: w