Theorem: LeanColls.Insert.toList_empty (LeanColls/Classes/Ops/Insert.lean)

State before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
⊢ toList empty = []
Tactic:
rw [List.eq_nil_iff_forall_not_mem]
State after:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
⊢ ∀ (a : τ), a ∉ toList empty

State before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
⊢ ∀ (a : τ), a ∉ toList empty
Tactic:
intro x
State after:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
x : τ
⊢ x ∉ toList empty

State before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
x : τ
⊢ x ∉ toList empty
Tactic:
rw [← Mem.ToList.mem_iff_mem_toList]
State after:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
x : τ
⊢ x ∉ empty

State before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
x : τ
⊢ x ∉ empty
Tactic:
apply Mem.mem_empty
State after:
no goals