Theorem: indicator_card_gt_real_card (meetings/ex5.lean)

State before:
⊢ Cardinal.mk ↑indicator > Cardinal.mk ↑Set.univ
Tactic:
simp only [Cardinal.mk_univ, indicator]
State after:
⊢ Cardinal.mk (ℝ → ↑binary') > Cardinal.mk ℝ

State before:
⊢ Cardinal.mk (ℝ → ↑binary') > Cardinal.mk ℝ
Tactic:
rw [binary', ←Cardinal.power_def, Cardinal.mk_insert (by simp), Cardinal.mk_singleton]
State after:
⊢ (1 + 1) ^ Cardinal.mk ℝ > Cardinal.mk ℝ

State before:
⊢ (1 + 1) ^ Cardinal.mk ℝ > Cardinal.mk ℝ
Tactic:
ring_nf
State after:
⊢ 2 ^ Cardinal.mk ℝ > Cardinal.mk ℝ

State before:
⊢ 2 ^ Cardinal.mk ℝ > Cardinal.mk ℝ
Tactic:
exact Cardinal.cantor (Cardinal.mk ℝ)
State after:
no goals

State before:
⊢ 0 ∉ {1}
Tactic:
simp
State after:
no goals