Theorem: IsTrivialBlock.of_card_le_2 (Jordan/Primitive.lean)

State before:
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
⊢ IsTrivialBlock B
Tactic:
cases' le_or_lt (Fintype.card B) 1 with h1 h1
State after:
case inl
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ IsTrivialBlock B

case inr
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ IsTrivialBlock B

State before:
case inl
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ IsTrivialBlock B
Tactic:
apply Or.intro_left
State after:
case inl.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ Set.Subsingleton B

State before:
case inl.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ Set.Subsingleton B
Tactic:
rw [← Set.subsingleton_coe, ← Fintype.card_le_one_iff_subsingleton]
State after:
case inl.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ Fintype.card ↑B ≤ 1

State before:
case inl.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ Fintype.card ↑B ≤ 1
Tactic:
exact h1
State after:
no goals

State before:
case inr
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ IsTrivialBlock B
Tactic:
apply Or.intro_right
State after:
case inr.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ B = ⊤

State before:
case inr.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ B = ⊤
Tactic:
rw [Set.top_eq_univ, ← set_fintype_card_eq_univ_iff]
State after:
case inr.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ Fintype.card ↑B = Fintype.card X

State before:
case inr.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ Fintype.card ↑B = Fintype.card X
Tactic:
exact le_antisymm (set_fintype_card_le_univ B) (le_trans hX h1)
State after:
no goals