Theorem: Set.coe_le_encard_iff (Matroid/ForMathlib/Card.lean)

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard
Tactic:
obtain (hfin | hinf) := s.finite_or_infinite
State after:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hfin : s.Finite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard

case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard

State before:
case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard
Tactic:
rw [hinf.encard_eq, iff_true_intro le_top, true_iff, iff_false_intro hinf, false_imp_iff]
State after:
case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ True

State before:
case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ True
Tactic:
trivial
State after:
no goals

State before:
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hfin : s.Finite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard
Tactic:
rw [← hfin.cast_ncard_eq, iff_true_intro hfin, Nat.cast_le, true_imp_iff]
State after:
no goals