Theorem: Cantor (Tests/Demo.lean)

State before:
⊢ ∀ (X : Type u) (f : X → Set X), ¬Function.Surjective f
Tactic:
motivated_proof
  tree_rewrite_def [1, 1, 1, 2]
  tree_push_neg [1, 1]
  lib_rewrite [1, 1, 1, 2, 0, 1] Set.ext_iff [1, 1, 1, 1, 1, 2]
  tree_push_neg [1, 1, 1, 1]
  lib_rewrite [1, 1, 2, 0, 1] not_iff [1, 1, 1, 1, 1]
  unify_forall_exists [1, 1, 1]
  lib_apply refl [1, 1, 1, 1, 2]
State after:
no goals

State before:
⊢ ∀ X : Type u, f : X → Set X⠀
  ¬Function.Surjective f
Tactic:
tree_rewrite_def [1, 1, 1, 2]
State after:
⊢ ∀ X : Type u, f : X → Set X⠀
  ¬∀ b⋆ : Set X, ∃ a : X⠀
    f a = b⋆

State before:
⊢ ∀ X : Type u, f : X → Set X⠀
  ¬∀ b⋆ : Set X, ∃ a : X⠀
    f a = b⋆
Tactic:
tree_push_neg [1, 1]
State after:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X⠀
  ¬f x_1 = x•

State before:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X⠀
  ¬f x_1 = x•
Tactic:
lib_rewrite [1, 1, 1, 2, 0, 1] Set.ext_iff [1, 1, 1, 1, 1, 2]
State after:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X⠀
  ¬(∀ x_2⋆ : X⠀
    x_2⋆ ∈ f x_1 ↔ x_2⋆ ∈ x•)

State before:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X⠀
  ¬(∀ x_2⋆ : X⠀
    x_2⋆ ∈ f x_1 ↔ x_2⋆ ∈ x•)
Tactic:
tree_push_neg [1, 1, 1, 1]
State after:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X, ∃ x_2• : X⠀
  ¬(x_2• ∈ f x_1 ↔ x_2• ∈ x•)

State before:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X, ∃ x_2• : X⠀
  ¬(x_2• ∈ f x_1 ↔ x_2• ∈ x•)
Tactic:
lib_rewrite [1, 1, 2, 0, 1] not_iff [1, 1, 1, 1, 1]
State after:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X, ∃ x_2• : X⠀
  ¬x_2• ∈ f x_1 ↔ x_2• ∈ x•

State before:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X, ∃ x_2• : X⠀
  ¬x_2• ∈ f x_1 ↔ x_2• ∈ x•
Tactic:
unify_forall_exists [1, 1, 1]
State after:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ a : X⠀
  ¬a ∈ f a ↔ a ∈ x•

State before:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ a : X⠀
  ¬a ∈ f a ↔ a ∈ x•
Tactic:
lib_apply refl [1, 1, 1, 1, 2]
State after:
no goals