awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Stalks
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
⊢ 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:
exact Functor.map_isIso (forget C) ((stalkFunctor C (⟨x, hx⟩ : U).1).map f.1)

Premises used: CategoryTheory.Functor.map, Subtype.mk, CategoryTheory.forget, CategoryTheory.Functor.map_isIso, CategoryTheory.InducedCategory.Hom.hom, Subtype.val, TopCat.Presheaf.stalkFunctor
-- Module: Mathlib.Topology.Sheaves.Stalks
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)
this : IsIso (X := obj (Sheaf.forget C X) F) (map (Sheaf.forget C X) f)
⊢ IsIso f

Tactic:
isIso_of_fully_faithful (Sheaf.forget C X) f

Premises used: CategoryTheory.isIso_of_fully_faithful, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Stalks
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)
this : IsIso (X := obj (Sheaf.forget C X) F) (map (Sheaf.forget C X) f)
⊢ IsIso f

Tactic:
exact isIso_of_fully_faithful (Sheaf.forget C X) f

Premises used: CategoryTheory.isIso_of_fully_faithful, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Stalks
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)
suffices : IsIso (X := obj (Sheaf.forget C X) F) (map (Sheaf.forget C X) f)
⊢ IsIso f

Tactic:
suffices IsIso ((Sheaf.forget C X).map f) by exact isIso_of_fully_faithful (Sheaf.forget C X) f
-- Module: Mathlib.Topology.Sheaves.Stalks
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)
this : ∀ (U : (Opens (↑X : Type v))ᵒᵖ), IsIso (f.hom.app U)
⊢ IsIso (X := obj (Sheaf.forget C X) F) (map (Sheaf.forget C X) f)

Tactic:
@NatIso.isIso_of_isIso_app _ _ _ _ F.1 G.1 f.1 this

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app, TopCat.Presheaf, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Topology.Sheaves.Stalks
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)
this : ∀ (U : (Opens (↑X : Type v))ᵒᵖ), IsIso (f.hom.app U)
⊢ IsIso (X := obj (Sheaf.forget C X) F) (map (Sheaf.forget C X) f)

Tactic:
exact @NatIso.isIso_of_isIso_app _ _ _ _ F.1 G.1 f.1 this

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Topology.Sheaves.Stalks
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)
suffices : ∀ (U : (Opens (↑X : Type v))ᵒᵖ), IsIso (f.hom.app U)
⊢ IsIso (X := obj (Sheaf.forget C X) F) (map (Sheaf.forget C X) f)

Tactic:
suffices ∀ U : (Opens X)ᵒᵖ, IsIso (f.1.app U) by
    exact @NatIso.isIso_of_isIso_app _ _ _ _ F.1 G.1 f.1 this
-- Module: Mathlib.Topology.Sheaves.Stalks
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))ᵒᵖ
op :
  ∀ (unop : Opens (↑X : Type v)),
    IsIso (X :=
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (Opposite.op unop))
      (f.hom.app (Opposite.op unop))
⊢ IsIso (f.hom.app U)

Tactic:
induction U
-- Module: Mathlib.Topology.Sheaves.Stalks
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)
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:
apply app_isIso_of_stalkFunctor_map_iso

Premises used: TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
v : PartialRefinement u s p
i : ι
⊢ v.toFun (u := u) (s := s) (p := p) i ⊆ u i

Tactic:
if h : i ∈ v.carrier then subset_closure.trans (v.closure_subset h) else (v.apply_eq h).le

Premises used: subset_closure, HasSubset.Subset.trans, Eq.le, ShrinkingLemma.PartialRefinement.apply_eq, dite, ShrinkingLemma.PartialRefinement.closure_subset
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
v : PartialRefinement u s p
i : ι
⊢ v.toFun (u := u) (s := s) (p := p) i ⊆ u i

Tactic:
exact if h : i ∈ v.carrier then subset_closure.trans (v.closure_subset h) else (v.apply_eq h).le

Premises used: ShrinkingLemma.PartialRefinement.carrier
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
v : PartialRefinement u s p
i : ι
⊢ v.toFun (u := u) (s := s) (p := p) i ⊆ u i

Tactic:
classical
  exact if h : i ∈ v.carrier then subset_closure.trans (v.closure_subset h) else (v.apply_eq h).le

Premises used: ShrinkingLemma.PartialRefinement.carrier
-- Module: Mathlib.Topology.ShrinkingLemma
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
v₁ v₂ : PartialRefinement u s p
h₁ : v₁ ∈ c
h₂ : v₂ ∈ c
i : ι
hi₁ : i ∈ v₁.carrier (u := u) (s := s) (p := p)
hi₂ : i ∈ v₂.carrier (u := u) (s := s) (p := p)
⊢ v₁.toFun (u := u) (s := s) (p := p) i = v₂.toFun (u := u) (s := s) (p := p) i

Tactic:
(hc.total h₁ h₂).elim (fun hle => hle.2 _ hi₁) (fun hle => (hle.2 _ hi₂).symm)

Premises used: And.right, Or.elim, Eq.symm, IsChain.total
-- Module: Mathlib.Topology.ShrinkingLemma
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
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
⊢ find (u := u) (s := s) (p := p) c ne i ∈ c

Tactic:
rw [find]

Premises used: ShrinkingLemma.PartialRefinement.find
-- Module: Mathlib.Topology.ShrinkingLemma
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
neg : ∀ (h : ¬∃ v ∈ c, i ∈ v.carrier (u := u) (s := s) (p := p)), ne.some (s := c) ∈ 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

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.ShrinkingLemma
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)
⊢ h.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)) ∈ c

Tactic:
h.choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.Topology.ShrinkingLemma
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)
⊢ ne.some (s := c) ∈ c

Tactic:
ne.some_mem

Premises used: Set.Nonempty.some_mem
-- Module: Mathlib.Topology.ShrinkingLemma
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)
⊢ h.choose (p := fun (v : PartialRefinement u s p) ↦ v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)) ∈ c

Tactic:
exacts [h.choose_spec.1, ne.some_mem]

Premises used: Exists.choose_spec, Set.Nonempty.some_mem, And.left
-- Module: Mathlib.Topology.ShrinkingLemma
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
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
⊢ 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

Tactic:
rw [find]

Premises used: ShrinkingLemma.PartialRefinement.find
-- Module: Mathlib.Topology.ShrinkingLemma
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
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
⊢ 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:
split_ifs with h
-- Module: Mathlib.Topology.ShrinkingLemma
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)
⊢ 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
-- Module: Mathlib.Topology.ShrinkingLemma
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)
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)
⊢ 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:
iff_of_true this.2 (mem_iUnion₂.2 ⟨_, this.1, this.2⟩)

Premises used: Iff.mpr, Set.mem_iUnion₂, iff_of_true, And.right, And.left, Exists.intro
-- Module: Mathlib.Topology.ShrinkingLemma
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)
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)
⊢ 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:
exact iff_of_true this.2 (mem_iUnion₂.2 ⟨_, this.1, this.2⟩)

Premises used: Iff.mpr, Set.mem_iUnion₂, iff_of_true, And.right, And.left, Exists.intro
-- Module: Mathlib.Topology.ShrinkingLemma
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)
⊢ ∀ (v : PartialRefinement u s p) (_ : v ∈ c), i ∉ v.carrier (u := u) (s := s) (p := p)

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Topology.ShrinkingLemma
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

Tactic:
iff_of_false (h _ ne.some_mem) ?_

Premises used: Set.Nonempty.some_mem, iff_of_false
-- Module: Mathlib.Topology.ShrinkingLemma
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)
neg : i ∉ chainSupCarrier (u := u) (s := s) (p := p) c
⊢ i ∈ ne.some (s := c).carrier (u := u) (s := s) (p := p) ↔ i ∈ chainSupCarrier (u := u) (s := s) (p := p) c

Tactic:
refine iff_of_false (h _ ne.some_mem) ?_

Premises used: Set.Nonempty.some_mem, iff_of_false
-- Module: Mathlib.Topology.ShrinkingLemma
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 ∉ chainSupCarrier (u := u) (s := s) (p := p) c

Tactic:
simpa only [chainSupCarrier, mem_iUnion₂, not_exists]

Premises used: not_exists, Set.mem_iUnion₂, ShrinkingLemma.PartialRefinement.chainSupCarrier
-- Module: Mathlib.Topology.ShrinkingLemma
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
i : ι
v : PartialRefinement u s p
hv : v ∈ c
hi : i ∈ v.carrier (u := u) (s := s) (p := p)
⊢ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i = v.toFun (u := u) (s := s) (p := p) i

Tactic:
apply_eq_of_chain hc (find_mem _ _) hv ((mem_find_carrier_iff _).2 <| mem_iUnion₂.2 ⟨v, hv, hi⟩)
    hi

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro, ShrinkingLemma.PartialRefinement.find_mem, ShrinkingLemma.PartialRefinement.apply_eq_of_chain, ShrinkingLemma.PartialRefinement.mem_find_carrier_iff
-- Module: Mathlib.Topology.ShrinkingLemma
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
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
⊢ ∃ (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)

Premises used: Membership.mem, Exists, em, And, ShrinkingLemma.PartialRefinement.chainSupCarrier, Not
-- Module: Mathlib.Topology.ShrinkingLemma
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
h : 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

Tactic:
use i
-- Module: Mathlib.Topology.ShrinkingLemma
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
⊢ x ∈ (find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i

Tactic:
simpa only [(find c ne i).apply_eq (mt (mem_find_carrier_iff _).1 hi)]

Premises used: ShrinkingLemma.PartialRefinement.find, mt, ShrinkingLemma.PartialRefinement.apply_eq, Iff.mp, ShrinkingLemma.PartialRefinement.mem_find_carrier_iff
-- Module: Mathlib.Topology.ShrinkingLemma
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
⊢ ∀ (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

Premises used: not_exists, Set.mem_iUnion₂, ShrinkingLemma.PartialRefinement.chainSupCarrier, not_and, not_imp_not