Theorem: mem_minimals_iff_forall_diff_singleton (Matroid/ForMathlib/Order/Minimal.lean)

State before:
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
⊢ s ∈ minimals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∈ s, ¬P (s \ {x})
Tactic:
simp only [mem_minimals_iff, mem_setOf_eq, and_congr_right_iff]
State after:
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
⊢ P s → ((∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y) ↔ ∀ x ∈ s, ¬P (s \ {x}))

State before:
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
⊢ P s → ((∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y) ↔ ∀ x ∈ s, ¬P (s \ {x}))
Tactic:
refine fun _ ↦ ⟨fun h x hx hxs ↦ ?_, fun h t ht hst ↦ Eq.symm <| hst.antisymm (fun x hxs ↦ ?_)⟩
State after:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y
x : α
hx : x ∈ s
hxs : P (s \ {x})
⊢ False

case refine_2
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ x ∈ s, ¬P (s \ {x})
t : Set α
ht : P t
hst : t ⊆ s
x : α
hxs : x ∈ s
⊢ x ∈ t

State before:
case refine_2
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ x ∈ s, ¬P (s \ {x})
t : Set α
ht : P t
hst : t ⊆ s
x : α
hxs : x ∈ s
⊢ x ∈ t
Tactic:
exact by_contra fun hxt ↦ h x hxs (hP ht (subset_diff_singleton hst hxt))
State after:
no goals

State before:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y
x : α
hx : x ∈ s
hxs : P (s \ {x})
⊢ False
Tactic:
rw [(h hxs diff_subset)] at hx
State after:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y
x : α
hx : x ∈ s \ {x}
hxs : P (s \ {x})
⊢ False

State before:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y
x : α
hx : x ∈ s \ {x}
hxs : P (s \ {x})
⊢ False
Tactic:
simp at hx
State after:
no goals