Theorem: cantor_end (Tests/Moves/TreeApply.lean)

State before:
⊢ ∀ (X : Type u) (f : X → Set X), ∃ a, ∀ (a_1 : X), a_1 ∉ f a_1 ↔ a_1 ∈ a
Tactic:
make_tree
State after:
⊢ MotivatedTree.Forall (Type u) fun X =>
    MotivatedTree.Forall (X → Set X) fun f =>
      MotivatedTree.Exists (Set X) fun a => MotivatedTree.Forall X fun a_1 => MotivatedTree.Not (a_1 ∈ f a_1) ↔ a_1 ∈ a

State before:
⊢ MotivatedTree.Forall (Type u) fun X =>
    MotivatedTree.Forall (X → Set X) fun f =>
      MotivatedTree.Exists (Set X) fun a => MotivatedTree.Forall X fun a_1 => MotivatedTree.Not (a_1 ∈ f a_1) ↔ a_1 ∈ a
Tactic:
lib_apply [1,1,1,1] refl [1, 1, 1, 1, 2]
State after:
no goals