Theorem: LO.FirstOrder.Derivation.ProofList.Finset.toList_subset_toList (Logic/FirstOrder/Computability/Calculus.lean)

State before:
μ : Type ?u.904427
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
s₁ s₂ : Finset α
⊢ s₁.toList ⊆ s₂.toList ↔ s₁ ⊆ s₂
Tactic:
simp[List.subset_def]
State after:
μ : Type ?u.904427
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
s₁ s₂ : Finset α
⊢ (∀ {a : α}, a ∈ s₁ → a ∈ s₂) ↔ s₁ ⊆ s₂

State before:
μ : Type ?u.904427
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
s₁ s₂ : Finset α
⊢ (∀ {a : α}, a ∈ s₁ → a ∈ s₂) ↔ s₁ ⊆ s₂
Tactic:
rfl
State after:
no goals