Theorem: BishopFin.card_sum_eq (Fifteen/Logic/BishopFin.lean)

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ card (α ⊕ β) = card α + card β
Tactic:
show ((elems α).map Sum.inl ++ (elems β).map Sum.inr).length = _
State after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ List.length (List.map Sum.inl (elems α) ++ List.map Sum.inr (elems β)) = card α + card β

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ List.length (List.map Sum.inl (elems α) ++ List.map Sum.inr (elems β)) = card α + card β
Tactic:
simp only [List.length_append, List.length_map]
State after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ List.length (elems α) + List.length (elems β) = card α + card β

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ List.length (elems α) + List.length (elems β) = card α + card β
Tactic:
rfl
State after:
no goals