-- Mathlib/Topology/ShrinkingLemma.lean
theorem mem_find_carrier_iff {c : Set (PartialRefinement u s p)} {i : ι} (ne : c.Nonempty) :
    i ∈ (find c ne i).carrier ↔ i ∈ chainSupCarrier c

Proof state:
ι : 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 c ne i).carrier ↔ i ∈ chainSupCarrier c

Tactic:
rw [find]

Result:
ι : 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 ∈ (if hi : ∃ v ∈ c, i ∈ v.carrier then hi.choose else ne.some).carrier ↔ i ∈ chainSupCarrier c

Proof state:
case neg
ι : 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
⊢ i ∈ ne.some.carrier ↔ i ∈ chainSupCarrier c

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

Result:
case neg
ι : 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
⊢ i ∉ chainSupCarrier c

Proof state:
case neg
ι : 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
⊢ i ∉ chainSupCarrier c

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

Result:
no goals

Proof state:
case neg
ι : 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
⊢ i ∈ ne.some.carrier ↔ i ∈ chainSupCarrier c

Tactic:
push_neg at h

Result:
case neg
ι : 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
⊢ i ∈ ne.some.carrier ↔ i ∈ chainSupCarrier c

Proof state:
case pos
ι : 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
⊢ i ∈ h.choose.carrier ↔ i ∈ chainSupCarrier c

Tactic:
have := h.choose_spec

Result:
case pos
ι : 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
this : h.choose ∈ c ∧ i ∈ h.choose.carrier
⊢ i ∈ h.choose.carrier ↔ i ∈ chainSupCarrier c

Proof state:
ι : 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 ∈ (if hi : ∃ v ∈ c, i ∈ v.carrier then hi.choose else ne.some).carrier ↔ i ∈ chainSupCarrier c

Tactic:
split_ifs with h

Result:
case pos
ι : 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
⊢ i ∈ h.choose.carrier ↔ i ∈ chainSupCarrier c

case neg
ι : 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
⊢ i ∈ ne.some.carrier ↔ i ∈ chainSupCarrier c

Proof state:
case pos
ι : 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
this : h.choose ∈ c ∧ i ∈ h.choose.carrier
⊢ i ∈ h.choose.carrier ↔ i ∈ chainSupCarrier c

Tactic:
exact iff_of_true this.2 (mem_iUnion₂.2 ⟨_, this.1, this.2⟩)

Result:
no goals