awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (hypothesis)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : ↥U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
V : Opens (↑X : Type v)
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hmem :
  ∃ (h : (↑y : (↑X : Type v)) ∈ V),
    Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
            (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
          (surjInv ⋯ g) :
        CC (F.stalk (↑y : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) ⋯) :
            (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
          f :
        CC (F.stalk (↑y : (↑X : Type v))))
hyV : (↑y : (↑X : Type v)) ∈ V
⊢ ∀ᶠ (a : ↥U) in 𝓝 y,
    Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
      {g : F.EtaleSpace (CC := CC) (FC := FC) |
        ∃ (h : g.base (CC := CC) (FC := FC) ∈ V),
          g.germ (CC := CC) (FC := FC) =
            (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (g.base (CC := CC) (FC := FC)) h) :
                (a : CC (F.obj (op V))) → CC (F.stalk g.base))
              f}
      (mk (CC := CC) (FC := FC) (↑a : (↑X : Type v))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑a : (↑X : Type v)) ⋯) :
            (a_1 : CC (F.obj (op U))) → CC (F.stalk (↑a : (↑X : Type v))))
          (surjInv ⋯ g)))
have hgf : Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) sorry) :
        (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
      (surjInv sorry g) :
    CC (F.stalk (↑y : (↑X : Type v))))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) sorry) :
        (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
      f :
    CC (F.stalk (↑y : (↑X : Type v))))
Tactic: rcases hmem with ⟨hyV, hgf⟩
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : ↥U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
V : Opens (↑X : Type v)
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hyV : (↑y : (↑X : Type v)) ∈ V
hgf :
  Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
        (surjInv ⋯ g) :
      CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
        f :
      CC (F.stalk (↑y : (↑X : Type v))))
⊢ ∀ᶠ (a : ↥U) in 𝓝 y,
    Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
      {g : F.EtaleSpace (CC := CC) (FC := FC) |
        ∃ (h : g.base (CC := CC) (FC := FC) ∈ V),
          g.germ (CC := CC) (FC := FC) =
            (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (g.base (CC := CC) (FC := FC)) h) :
                (a : CC (F.obj (op V))) → CC (F.stalk g.base))
              f}
      (mk (CC := CC) (FC := FC) (↑a : (↑X : Type v))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑a : (↑X : Type v)) ⋯) :
            (a_1 : CC (F.obj (op U))) → CC (F.stalk (↑a : (↑X : Type v))))
          (surjInv ⋯ g)))
have rcases : ∀ (W : Opens (↑X : Type v)) (hyW : (↑y : (↑X : Type v)) ∈ W) (ιWU : W ⟶ U) (ιWV : W ⟶ V)
  (hW :
    Eq (α := CC (F.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W)))
          (surjInv sorry g) :
        CC (F.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) f :
        CC (F.obj (op W)))),
  ∀ᶠ (a : ↥U) in 𝓝 y,
    Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
      {g : F.EtaleSpace (CC := CC) (FC := FC) |
        ∃ (h : g.base (CC := CC) (FC := FC) ∈ V),
          g.germ (CC := CC) (FC := FC) =
            (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (g.base (CC := CC) (FC := FC)) h) :
                (a : CC (F.obj (op V))) → CC (F.stalk g.base))
              f}
      (mk (CC := CC) (FC := FC) (↑a : (↑X : Type v))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑a : (↑X : Type v)) sorry) :
            (a_1 : CC (F.obj (op U))) → CC (F.stalk (↑a : (↑X : Type v))))
          (surjInv sorry g)))
Tactic: rcases F.germ_eq _ _ _ _ _ hgf with ⟨W, hyW, ιWU, ιWV, hW⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : ↥U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
V : Opens (↑X : Type v)
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hyV : (↑y : (↑X : Type v)) ∈ V
hgf :
  Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
        (surjInv ⋯ g) :
      CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
        f :
      CC (F.stalk (↑y : (↑X : Type v))))
W : Opens (↑X : Type v)
hyW : (↑y : (↑X : Type v)) ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W)))
        (surjInv ⋯ g) :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) f :
      CC (F.obj (op W)))
⊢ ∀ᶠ (a : ↥U) in 𝓝 y,
    Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
      {g : F.EtaleSpace (CC := CC) (FC := FC) |
        ∃ (h : g.base (CC := CC) (FC := FC) ∈ V),
          g.germ (CC := CC) (FC := FC) =
            (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (g.base (CC := CC) (FC := FC)) h) :
                (a : CC (F.obj (op V))) → CC (F.stalk g.base))
              f}
      (mk (CC := CC) (FC := FC) (↑a : (↑X : Type v))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑a : (↑X : Type v)) ⋯) :
            (a_1 : CC (F.obj (op U))) → CC (F.stalk (↑a : (↑X : Type v))))
          (surjInv ⋯ g)))
have h : ∀ (z : ↥U)
  (hz :
    Membership.mem (γ := Set ↥U) (Subtype.val (p := fun (x : (↑X : Type v)) ↦ x ∈ U) ⁻¹' (↑W : Set (↑X : Type v))) z),
  ∃ (h : (↑z : (↑X : Type v)) ∈ V),
    Eq (α := CC (F.stalk (↑z : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑z : (↑X : Type v)) sorry) :
            (a : CC (F.obj (op U))) → CC (F.stalk (↑z : (↑X : Type v))))
          (surjInv sorry g) :
        CC (F.stalk (↑z : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑z : (↑X : Type v)) h) :
            (a : CC (F.obj (op V))) → CC (F.stalk (↑z : (↑X : Type v))))
          f :
        CC (F.stalk (↑z : (↑X : Type v))))
Tactic: filter_upwards [W.isOpen.preimage continuous_subtype_val |>.mem_nhds hyW] with z hz
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : ↥U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
V : Opens (↑X : Type v)
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hyV : (↑y : (↑X : Type v)) ∈ V
hgf :
  Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
        (surjInv ⋯ g) :
      CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
        f :
      CC (F.stalk (↑y : (↑X : Type v))))
W : Opens (↑X : Type v)
hyW : (↑y : (↑X : Type v)) ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W)))
        (surjInv ⋯ g) :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) f :
      CC (F.obj (op W)))
z : ↥U
hz : Membership.mem (γ := Set ↥U) (Subtype.val (p := fun (x : (↑X : Type v)) ↦ x ∈ U) ⁻¹' (↑W : Set (↑X : Type v))) z
⊢ ∃ (h : (↑z : (↑X : Type v)) ∈ V),
    Eq (α := CC (F.stalk (↑z : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑z : (↑X : Type v)) ⋯) :
            (a : CC (F.obj (op U))) → CC (F.stalk (↑z : (↑X : Type v))))
          (surjInv ⋯ g) :
        CC (F.stalk (↑z : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑z : (↑X : Type v)) h) :
            (a : CC (F.obj (op V))) → CC (F.stalk (↑z : (↑X : Type v))))
          f :
        CC (F.stalk (↑z : (↑X : Type v))))
have h : Eq (α := CC (F.stalk (↑z : (↑X : Type v))))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑z : (↑X : Type v)) sorry) :
        (a : CC (F.obj (op U))) → CC (F.stalk (↑z : (↑X : Type v))))
      (surjInv sorry g) :
    CC (F.stalk (↑z : (↑X : Type v))))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑z : (↑X : Type v)) sorry) :
        (a : CC (F.obj (op V))) → CC (F.stalk (↑z : (↑X : Type v))))
      f :
    CC (F.stalk (↑z : (↑X : Type v))))
Tactic: use ιWV.le hz
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : ↥U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
V : Opens (↑X : Type v)
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hyV : (↑y : (↑X : Type v)) ∈ V
hgf :
  Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
        (surjInv ⋯ g) :
      CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
        f :
      CC (F.stalk (↑y : (↑X : Type v))))
W : Opens (↑X : Type v)
hyW : (↑y : (↑X : Type v)) ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W)))
        (surjInv ⋯ g) :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) f :
      CC (F.obj (op W)))
z : ↥U
hz : Membership.mem (γ := Set ↥U) (Subtype.val (p := fun (x : (↑X : Type v)) ↦ x ∈ U) ⁻¹' (↑W : Set (↑X : Type v))) z
⊢ Eq (α := CC (F.stalk (↑z : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑z : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op U))) → CC (F.stalk (↑z : (↑X : Type v))))
        (surjInv ⋯ g) :
      CC (F.stalk (↑z : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑z : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op V))) → CC (F.stalk (↑z : (↑X : Type v))))
        f :
      CC (F.stalk (↑z : (↑X : Type v))))
have h : Eq (α := CC (F.stalk (↑z : (↑X : Type v))))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W (↑z : (↑X : Type v)) hz) :
        (a : CC (F.obj (op W))) → CC (F.stalk (↑z : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W)))
          (surjInv sorry g) :
        CC (F.obj (op W))) :
    CC (F.stalk (↑z : (↑X : Type v))))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑z : (↑X : Type v)) sorry) :
        (a : CC (F.obj (op V))) → CC (F.stalk (↑z : (↑X : Type v))))
      f :
    CC (F.stalk (↑z : (↑X : Type v))))
Tactic: rw [← F.germ_res_apply ιWU z hz, hW, F.germ_res_apply]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
hF_bij :
  ∀ (x : (↑X : Type v)),
    ∃ (U : Opens (↑X : Type v)),
      x ∈ U ∧
        ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
          Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
            (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
⊢ IsCoveringMap (E := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC))
have refine : ∀ (x : (↑X : Type v)),
  IsEvenlyCovered (E := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC)) x
    (WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
Tactic: refine fun x ↦ .to_isEvenlyCovered_preimage (I := WithDiscreteTopology (ToType (F.stalk x))) ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
hF_bij :
  ∀ (x : (↑X : Type v)),
    ∃ (U : Opens (↑X : Type v)),
      x ∈ U ∧
        ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
          Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
            (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
x : (↑X : Type v)
⊢ IsEvenlyCovered (E := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC)) x
    (WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
have right : ∃ (U : Set (↑X : Type v)),
  x ∈ U ∧
    IsOpen U ∧
      IsOpen (X := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC) ⁻¹' U) ∧
        ∃ (H :
          (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v) ≃ₜ
            (↑U : Type v) × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))),
          ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v)),
            (↑((H : (a : (↑(base ⁻¹' U) : Type v)) → (↑U : Type v) × WithDiscreteTopology (ToType (F.stalk x))) x_1).1 :
                (↑X : Type v)) =
              (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)
Tactic: use inferInstance
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
hF_bij :
  ∀ (x : (↑X : Type v)),
    ∃ (U : Opens (↑X : Type v)),
      x ∈ U ∧
        ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
          Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
            (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
x : (↑X : Type v)
⊢ ∃ (U : Set (↑X : Type v)),
    x ∈ U ∧
      IsOpen U ∧
        IsOpen (X := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC) ⁻¹' U) ∧
          ∃ (H :
            (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v) ≃ₜ
              (↑U : Type v) × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))),
            ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v)),
              (↑((H : (a : (↑(base ⁻¹' U) : Type v)) → (↑U : Type v) × WithDiscreteTopology (ToType (F.stalk x)))
                        x_1).1 :
                  (↑X : Type v)) =
                (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)
have right : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U)
  (hU_bij :
    ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
      Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
        (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))),
  ∃ (U : Set (↑X : Type v)),
    x ∈ U ∧
      IsOpen U ∧
        IsOpen (X := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC) ⁻¹' U) ∧
          ∃ (H :
            (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v) ≃ₜ
              (↑U : Type v) × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))),
            ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v)),
              (↑((H : (a : (↑(base ⁻¹' U) : Type v)) → (↑U : Type v) × WithDiscreteTopology (ToType (F.stalk x)))
                        x_1).1 :
                  (↑X : Type v)) =
                (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)
Tactic: rcases hF_bij x with ⟨U, hxU, hU_bij⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
hF_bij :
  ∀ (x : (↑X : Type v)),
    ∃ (U : Opens (↑X : Type v)),
      x ∈ U ∧
        ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
          Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
            (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
hU_bij :
  ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
⊢ ∃ (U : Set (↑X : Type v)),
    x ∈ U ∧
      IsOpen U ∧
        IsOpen (X := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC) ⁻¹' U) ∧
          ∃ (H :
            (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v) ≃ₜ
              (↑U : Type v) × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))),
            ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v)),
              (↑((H : (a : (↑(base ⁻¹' U) : Type v)) → (↑U : Type v) × WithDiscreteTopology (ToType (F.stalk x)))
                        x_1).1 :
                  (↑X : Type v)) =
                (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)
have h : ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)),
  (↑((homeomorph (CC := CC) (FC := FC) U hU_bij x hxU :
              (a : (↑(base ⁻¹' (↑U : Set (↑X : Type v))) : Type v)) →
                (↑(↑U : Set (↑X : Type v)) : Type v) × WithDiscreteTopology (ToType (F.stalk x)))
            x_1).1 :
      (↑X : Type v)) =
    (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)
Tactic: use U, hxU, U.isOpen, U.isOpen.preimage (continuous_base F), homeomorph U hU_bij x hxU
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Flasque (goal)
Goal:
X : TopCat
C : Type v
inst : Category.{w, v} C
F : Presheaf.{u, w, v} C X
Y : TopCat
inst_1 : F.IsFlasque
f : X ⟶ Y
U V : (Opens (↑Y : Type u))ᵒᵖ
i : U ⟶ V
⊢ Epi ((Functor.obj (pushforward C f) F).map i)
have simp : Epi (F.map ((Opens.map f).map i.unop).op)
Tactic: simp only [pushforward_obj_obj, pushforward_obj_map]