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

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

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ 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_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.length (List.map f (elems α)) ≤ List.length (elems β)

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.length (List.map f (elems α)) ≤ List.length (elems β)
Tactic:
refine List.Nodup.length_le_of_subset ?_ ?_
State after:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.Nodup (List.map f (elems α))

case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.map f (elems α) ⊆ elems β

State before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.Nodup (List.map f (elems α))

case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.map f (elems α) ⊆ elems β
Tactic:
. exact nodup_elems.map f f_inj
State after:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.map f (elems α) ⊆ elems β

State before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.map f (elems α) ⊆ elems β
Tactic:
. exact subset_elems _
State after:
no goals

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

State before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.Nodup (List.map f (elems α))
Tactic:
exact nodup_elems.map f f_inj
State after:
no goals

State before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.map f (elems α) ⊆ elems β
Tactic:
exact subset_elems _
State after:
no goals