Theorem: encard_pair_le (Matroid/ForMathlib/Card.lean)

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e f : α
⊢ {e, f}.encard ≤ 2
Tactic:
obtain (rfl | hne) := eq_or_ne e f
State after:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ {e, e}.encard ≤ 2

case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e f : α
hne : e ≠ f
⊢ {e, f}.encard ≤ 2

State before:
case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e f : α
hne : e ≠ f
⊢ {e, f}.encard ≤ 2
Tactic:
rw [encard_pair hne]
State after:
no goals

State before:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ {e, e}.encard ≤ 2
Tactic:
simp only [mem_singleton_iff, insert_eq_of_mem, encard_singleton]
State after:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ 1 ≤ 2

State before:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ 1 ≤ 2
Tactic:
norm_num
State after:
no goals