Theorem: Set.sep_of_subset (Sion/Concavexity.lean)

State before:
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
⊢ {x | x ∈ s ∧ p x} = {x | x ∈ t ∧ p x} ∩ s
Tactic:
ext x
State after:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ x ∈ {x | x ∈ s ∧ p x} ↔ x ∈ {x | x ∈ t ∧ p x} ∩ s

State before:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ x ∈ {x | x ∈ s ∧ p x} ↔ x ∈ {x | x ∈ t ∧ p x} ∩ s
Tactic:
simp only [mem_sep_iff, mem_inter_iff]
State after:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ x ∈ s ∧ p x ↔ (x ∈ t ∧ p x) ∧ x ∈ s

State before:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ x ∈ s ∧ p x ↔ (x ∈ t ∧ p x) ∧ x ∈ s
Tactic:
rw [and_assoc, and_comm]
State after:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ p x ∧ x ∈ s ↔ x ∈ t ∧ p x ∧ x ∈ s

State before:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ p x ∧ x ∈ s ↔ x ∈ t ∧ p x ∧ x ∈ s
Tactic:
simp only [iff_and_self, and_imp]
State after:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ p x → x ∈ s → x ∈ t

State before:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ p x → x ∈ s → x ∈ t
Tactic:
exact fun _ h' => hst h'
State after:
no goals