awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
⊢ IsIso (X :=
    obj (forget C (FC := FC) (CC := CC))
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (map (forget C (FC := FC) (CC := CC)) (f.hom.app (op U)))
have rw : Function.Bijective (α :=
  (fun (X : Type v) ↦ X)
    (obj (forget C (FC := FC) (CC := CC))
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))))
  (β :=
  (fun (X : Type v) ↦ X)
    (obj (forget C (FC := FC) (CC := CC))
      (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (map (forget C (FC := FC) (CC := CC)) (f.hom.app (op U)))) :
    (a : (fun (X : Type v) ↦ X) ((forget C).obj (F.obj.obj (op U)))) →
      (fun (X : Type v) ↦ X) ((forget C).obj (G.obj.obj (op U))))
Tactic: rw [isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
⊢ Function.Bijective (α :=
    (fun (X : Type v) ↦ X)
      (obj (forget C (FC := FC) (CC := CC))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))))
    (β :=
    (fun (X : Type v) ↦ X)
      (obj (forget C (FC := FC) (CC := CC))
        (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (map (forget C (FC := FC) (CC := CC)) (f.hom.app (op U)))) :
      (a : (fun (X : Type v) ↦ X) ((forget C).obj (F.obj.obj (op U)))) →
        (fun (X : Type v) ↦ X) ((forget C).obj (G.obj.obj (op U))))
have h : ∀ x ∈ U,
  Function.Bijective.{v + 1, v + 1} (α :=
    obj (forget C (FC := FC) (CC := CC))
      (obj (stalkFunctor C x)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
    (β :=
    obj (forget C (FC := FC) (CC := CC))
      (obj (stalkFunctor C x)
        (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
    (⇑(ConcreteCategory.hom (FC := FC) (CC := obj (forget C (FC := FC) (CC := CC))) (map (stalkFunctor C x) f.hom)) :
      (a : (forget C).obj ((stalkFunctor C x).obj F.obj)) → (forget C).obj ((stalkFunctor C x).obj G.obj))
Tactic: apply app_bijective_of_stalkFunctor_map_bijective
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
x : (↑X : Type v)
hx : x ∈ U
⊢ Function.Bijective.{v + 1, v + 1} (α :=
    obj (forget C (FC := FC) (CC := CC))
      (obj (stalkFunctor C x)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
    (β :=
    obj (forget C (FC := FC) (CC := CC))
      (obj (stalkFunctor C x)
        (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
    (⇑(ConcreteCategory.hom (FC := FC) (CC := obj (forget C (FC := FC) (CC := CC))) (map (stalkFunctor C x) f.hom)) :
      (a : (forget C).obj ((stalkFunctor C x).obj F.obj)) → (forget C).obj ((stalkFunctor C x).obj G.obj))
have h : IsIso.{v, v + 1} (X :=
  obj (forget C (FC := FC) (CC := CC))
    (obj (stalkFunctor C x) (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
  (Y :=
  obj (forget C (FC := FC) (CC := CC))
    (obj (stalkFunctor C x) (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
  (↾(⇑(ConcreteCategory.hom (FC := FC) (CC := obj (forget C (FC := FC) (CC := CC))) (map (stalkFunctor C x) f.hom)) :
      (a : (forget C).obj ((stalkFunctor C x).obj F.obj)) → (forget C).obj ((stalkFunctor C x).obj G.obj)))
Tactic: apply (bijective_iff_isIso_ofHom _).mpr
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
inst_7 :
  ∀ (x : (↑X : Type v)),
    IsIso (X :=
      obj (stalkFunctor C x) (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C x) f.hom)
⊢ IsIso f
have suffices : IsIso (X := obj (Sheaf.forget C X) F) (map (Sheaf.forget C X) f)
Tactic: suffices IsIso ((Sheaf.forget C X).map f) by exact isIso_of_fully_faithful (Sheaf.forget C X) f
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
inst_7 :
  ∀ (x : (↑X : Type v)),
    IsIso (X :=
      obj (stalkFunctor C x) (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C x) f.hom)
⊢ IsIso (X := obj (Sheaf.forget C X) F) (map (Sheaf.forget C X) f)
have suffices : ∀ (U : (Opens (↑X : Type v))ᵒᵖ), IsIso (f.hom.app U)
Tactic: suffices ∀ U : (Opens X)ᵒᵖ, IsIso (f.1.app U) by
    exact @NatIso.isIso_of_isIso_app _ _ _ _ F.1 G.1 f.1 this
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
inst_7 :
  ∀ (x : (↑X : Type v)),
    IsIso (X :=
      obj (stalkFunctor C x) (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C x) f.hom)
U : (Opens (↑X : Type v))ᵒᵖ
⊢ IsIso (f.hom.app U)
have op : ∀ (unop : Opens (↑X : Type v)),
  IsIso (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op unop))
    (f.hom.app (op unop))
Tactic: induction U
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
⊢ find (u := u) (s := s) (p := p) c ne i ∈ c
have rw : (if hi : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p) then
    hi.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p))
  else ne.some (s := c)) ∈
  c
Tactic: rw [find]
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
⊢ (if hi : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p) then
      hi.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p))
    else ne.some (s := c)) ∈
    c
have pos : ∀ (h : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p)),
  h.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)) ∈ c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
pos :
  ∀ (h : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p)),
    h.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)) ∈ c
⊢ (if hi : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p) then
      hi.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p))
    else ne.some (s := c)) ∈
    c
have neg : ∀ (h : ¬∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p)), ne.some (s := c) ∈ c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
⊢ i ∈ (find (u := u) (s := s) (p := p) c ne i).carrier (u := u) (s := s) (p := p) ↔
    i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
have rw : Membership.mem (γ := Set ι)
    (carrier (u := u) (s := s) (p := p)
      (if hi : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p) then
        hi.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p))
      else ne.some (s := c)))
    i ↔
  i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
Tactic: rw [find]
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
⊢ Membership.mem (γ := Set ι)
      (carrier (u := u) (s := s) (p := p)
        (if hi : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p) then
          hi.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p))
        else ne.some (s := c)))
      i ↔
    i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
have pos : ∀ (h : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p)),
  i ∈
      h.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)).carrier (u :=
        u) (s := s) (p := p) ↔
    i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
pos :
  ∀ (h : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p)),
    i ∈
        h.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)).carrier
          (u := u) (s := s) (p := p) ↔
      i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
⊢ Membership.mem (γ := Set ι)
      (carrier (u := u) (s := s) (p := p)
        (if hi : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p) then
          hi.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p))
        else ne.some (s := c)))
      i ↔
    i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
have neg : ∀ (h : ¬∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p)),
  i ∈ ne.some (s := c).carrier (u := u) (s := s) (p := p) ↔ i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
h : ∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p)
⊢ i ∈
      h.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)).carrier (u :=
        u) (s := s) (p := p) ↔
    i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
have this : h.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)) ∈ c ∧
  i ∈
    h.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)).carrier (u :=
      u) (s := s) (p := p)
Tactic: have := h.choose_spec
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
h : ¬∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p)
⊢ i ∈ ne.some (s := c).carrier (u := u) (s := s) (p := p) ↔ i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
have h₁ : ∀ (v : PartialRefinement u s p) (_ : v ∈ c), i ∉ v.carrier (u := u) (s := s) (p := p)
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
h : ∀ (v : PartialRefinement u s p) (_ : v ∈ c), i ∉ v.carrier (u := u) (s := s) (p := p)
⊢ i ∈ ne.some (s := c).carrier (u := u) (s := s) (p := p) ↔ i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
have neg : i ∉ chainSupCarrier (u := u) (s := s) (p := p) c
Tactic: refine iff_of_false (h _ ne.some_mem) ?_
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
⊢ ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
have inl : ∀ (i : ι) (hi : i ∉ chainSupCarrier (u := u) (s := s) (p := p) c) (hxi : x ∈ u i),
  ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
Tactic: rcases em (∃ i, i ∉ chainSupCarrier c ∧ x ∈ u i) with (⟨i, hi, hxi⟩ | hx)
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
inl :
  ∀ (i : ι) (hi : i ∉ chainSupCarrier (u := u) (s := s) (p := p) c) (hxi : x ∈ u i),
    ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
⊢ ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
have inr : ∀ (hx : ¬∃ i ∉ chainSupCarrier (u := u) (s := s) (p := p) c, x ∈ u i),
  ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
Tactic: rcases em (∃ i, i ∉ chainSupCarrier c ∧ x ∈ u i) with (⟨i, hi, hxi⟩ | hx)
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
i : ι
hi : i ∉ chainSupCarrier (u := u) (s := s) (p := p) c
hxi : x ∈ u i
⊢ ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
have h : x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
hx : ¬∃ i ∉ chainSupCarrier (u := u) (s := s) (p := p) c, x ∈ u i
⊢ ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
have hx₁ : ∀ (x_1 : ι), x ∈ u x_1 → ∃ (i : PartialRefinement u s p) (_ : i ∈ c), x_1 ∈ i.carrier (u := u) (s := s) (p := p)
Tactic: simp_rw [not_exists, not_and, not_imp_not, chainSupCarrier, mem_iUnion₂] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
hx : ∀ (x_1 : ι), x ∈ u x_1 → ∃ (i : PartialRefinement u s p) (_ : i ∈ c), x_1 ∈ i.carrier (u := u) (s := s) (p := p)
⊢ ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
have this : Nonempty (PartialRefinement u s p)
Tactic: haveI : Nonempty (PartialRefinement u s p) := ⟨ne.some⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
hx : ∀ (x_1 : ι), x ∈ u x_1 → ∃ (i : PartialRefinement u s p) (_ : i ∈ c), x_1 ∈ i.carrier (u := u) (s := s) (p := p)
this : Nonempty (PartialRefinement u s p)
⊢ ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
have inr : ∀ (v : (x : ι) → PartialRefinement u s p) (hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c)
  (hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier (u := u) (s := s) (p := p)),
  ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
Tactic: choose! v hvc hiv using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s p)
v : (x : ι) → PartialRefinement u s p
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier (u := u) (s := s) (p := p)
⊢ ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
have inr : ∀ (i : ι) (hxi : x ∈ u i) (hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v j ≤ v i),
  ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
Tactic: rcases (hfin x hxs).exists_maximalFor v _ (mem_iUnion.1 (hU hxs)) with
        ⟨i, hxi : x ∈ u i, hmax : ∀ j, x ∈ u j → v i ≤ v j → v j ≤ v i⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s p)
v : (x : ι) → PartialRefinement u s p
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier (u := u) (s := s) (p := p)
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v j ≤ v i
⊢ ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
have inr : ∀ (j : ι) (hj : x ∈ (v i).toFun (u := u) (s := s) (p := p) j),
  ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
Tactic: rcases mem_iUnion.1 ((v i).subset_iUnion hxs) with ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s p)
v : (x : ι) → PartialRefinement u s p
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier (u := u) (s := s) (p := p)
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v j ≤ v i
j : ι
hj : x ∈ (v i).toFun (u := u) (s := s) (p := p) j
⊢ ∃ (i : ι), x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i
have h : x ∈ (find (u := u) (s := s) (p := p) c ne j).toFun (u := u) (s := s) (p := p) j
Tactic: use j
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s p)
v : (x : ι) → PartialRefinement u s p
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier (u := u) (s := s) (p := p)
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v j ≤ v i
j : ι
hj : x ∈ (v i).toFun (u := u) (s := s) (p := p) j
⊢ x ∈ (find (u := u) (s := s) (p := p) c ne j).toFun (u := u) (s := s) (p := p) j
have hj' : x ∈ u j
Tactic: have hj' : x ∈ u j := (v i).subset _ hj