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

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

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

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

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

State before:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y
x : α
hx : x ∉ s
hxs : P (insert x s)
⊢ x ∈ s
Tactic:
rw [h hxs (subset_insert _ _)]
State after:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y
x : α
hx : x ∉ s
hxs : P (insert x s)
⊢ x ∈ insert x s

State before:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y
x : α
hx : x ∉ s
hxs : P (insert x s)
⊢ x ∈ insert x s
Tactic:
apply mem_insert
State after:
no goals