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

State before:
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α = card β
Tactic:
refine Nat.le_antisymm ?_ ?_
State after:
case refine_1
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α ≤ card β

case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α

State before:
case refine_1
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α ≤ card β

case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α
Tactic:
. exact card_le_card_of_inj f f_inj
State after:
case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α

State before:
case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α
Tactic:
. exact card_ge_card_of_surj f f_surj
State after:
no goals

State before:
case refine_1
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α ≤ card β
Tactic:
exact card_le_card_of_inj f f_inj
State after:
no goals

State before:
case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α
Tactic:
exact card_ge_card_of_surj f f_surj
State after:
no goals