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

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ card α ≥ card β
Tactic:
dsimp only [card]
State after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ List.length (elems α) ≥ List.length (elems β)

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ List.length (elems α) ≥ List.length (elems β)
Tactic:
conv =>
  lhs; equals ((elems α).map f).length => rw [List.length_map]
State after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ List.length (List.map f (elems α)) ≥ List.length (elems β)

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ List.length (List.map f (elems α)) ≥ List.length (elems β)
Tactic:
refine nodup_elems.length_le_of_subset ?_
State after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ elems β ⊆ List.map f (elems α)

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ elems β ⊆ List.map f (elems α)
Tactic:
intro b _
State after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
b : β
a✝ : b ∈ elems β
⊢ b ∈ List.map f (elems α)

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
b : β
a✝ : b ∈ elems β
⊢ b ∈ List.map f (elems α)
Tactic:
simp only [List.mem_map, mem_elems, true_and]
State after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
b : β
a✝ : b ∈ elems β
⊢ ∃ a, f a = b

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
b : β
a✝ : b ∈ elems β
⊢ ∃ a, f a = b
Tactic:
exact f_surj b
State after:
no goals

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ List.length (elems α) = List.length (List.map f (elems α))
Tactic:
rw [List.length_map]
State after:
no goals