Theorem: Set.eq_top_iff_ncard (Jordan/Mathlib/Set.lean)

State before:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ B = ⊤ ↔ ncard B = Fintype.card α
Tactic:
rw [top_eq_univ, ← Set.compl_empty_iff, ← Set.ncard_eq_zero]
State after:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = Fintype.card α

State before:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = Fintype.card α
Tactic:
rw [← Nat.card_eq_fintype_card]
State after:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = Nat.card α

State before:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = Nat.card α
Tactic:
rw [← Set.ncard_add_ncard_compl B]
State after:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = ncard B + ncard Bᶜ

State before:
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 ↔ ncard B = ncard B + ncard Bᶜ
Tactic:
constructor
State after:
case mp
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 → ncard B = ncard B + ncard Bᶜ

case mpr
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard B = ncard B + ncard Bᶜ → ncard Bᶜ = 0

State before:
case mp
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard Bᶜ = 0 → ncard B = ncard B + ncard Bᶜ
Tactic:
intro H
State after:
case mp
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
H : ncard Bᶜ = 0
⊢ ncard B = ncard B + ncard Bᶜ

State before:
case mp
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
H : ncard Bᶜ = 0
⊢ ncard B = ncard B + ncard Bᶜ
Tactic:
rw [H, add_zero]
State after:
no goals

State before:
case mpr
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
⊢ ncard B = ncard B + ncard Bᶜ → ncard Bᶜ = 0
Tactic:
intro H
State after:
case mpr
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
H : ncard B = ncard B + ncard Bᶜ
⊢ ncard Bᶜ = 0

State before:
case mpr
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
B : Set α
H : ncard B = ncard B + ncard Bᶜ
⊢ ncard Bᶜ = 0
Tactic:
exact Nat.add_left_cancel H.symm
State after:
no goals