Apply andI to the current goal.
We will prove ((first_countable_space Q_infty Q_infty_topology ∨ ¬ first_countable_space Q_infty Q_infty_topology) ∧ (second_countable_space Q_infty Q_infty_topology ∨ ¬ second_countable_space Q_infty Q_infty_topology)) ∧ (Lindelof_space Q_infty Q_infty_topology ∨ ¬ Lindelof_space Q_infty Q_infty_topology).
Apply andI to the current goal.
We will prove (first_countable_space Q_infty Q_infty_topology ∨ ¬ first_countable_space Q_infty Q_infty_topology) ∧ (second_countable_space Q_infty Q_infty_topology ∨ ¬ second_countable_space Q_infty Q_infty_topology).
Apply andI to the current goal.
An exact proof term for the current goal is (xm (first_countable_space Q_infty Q_infty_topology)).
An exact proof term for the current goal is (xm (second_countable_space Q_infty Q_infty_topology)).
An exact proof term for the current goal is (xm (Lindelof_space Q_infty Q_infty_topology)).
An exact proof term for the current goal is (xm (∃D : set, D ⊆ Q_infty ∧ countable D ∧ dense_in D Q_infty Q_infty_topology)).
∎