Theorem: Partition.partOf_mem (Matroid/ForMathlib/SetPartition.lean)

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
⊢ P.partOf x ∈ P
Tactic:
obtain ⟨t, ⟨h', h⟩⟩ := P.exists_unique_of_mem_set hx
State after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
⊢ P.partOf x ∈ P

State before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
⊢ P.partOf x ∈ P
Tactic:
have hrw : {t | t ∈ P ∧ x ∈ t} = {t} := by
  ext t'
  simp only [mem_setOf_eq, mem_singleton_iff]
  exact ⟨h t', by rintro rfl; exact h'⟩
State after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
hrw : {t | t ∈ P ∧ x ∈ t} = {t}
⊢ P.partOf x ∈ P

State before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
hrw : {t | t ∈ P ∧ x ∈ t} = {t}
⊢ P.partOf x ∈ P
Tactic:
rw [partOf, hrw, sUnion_singleton]
State after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
hrw : {t | t ∈ P ∧ x ∈ t} = {t}
⊢ t ∈ P

State before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
hrw : {t | t ∈ P ∧ x ∈ t} = {t}
⊢ t ∈ P
Tactic:
exact h'.1
State after:
no goals

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
⊢ {t | t ∈ P ∧ x ∈ t} = {t}
Tactic:
ext t'
State after:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' ∈ {t | t ∈ P ∧ x ∈ t} ↔ t' ∈ {t}

State before:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' ∈ {t | t ∈ P ∧ x ∈ t} ↔ t' ∈ {t}
Tactic:
simp only [mem_setOf_eq, mem_singleton_iff]
State after:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' ∈ P ∧ x ∈ t' ↔ t' = t

State before:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' ∈ P ∧ x ∈ t' ↔ t' = t
Tactic:
exact ⟨h t', by rintro rfl; exact h'⟩
State after:
no goals

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' = t → t' ∈ P ∧ x ∈ t'
Tactic:
rintro rfl
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t' : Set α
h' : t' ∈ P ∧ x ∈ t'
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t'
⊢ t' ∈ P ∧ x ∈ t'

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t' : Set α
h' : t' ∈ P ∧ x ∈ t'
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t'
⊢ t' ∈ P ∧ x ∈ t'
Tactic:
exact h'
State after:
no goals