-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- A mono between objects with equally sized fibers is an iso. -/
lemma isIso_of_mono_of_eq_card_fiber {X Y : C} (f : X ⟶ Y) [Mono f]
    (h : Nat.card (F.obj X) = Nat.card (F.obj Y)) : IsIso f

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
⊢ Function.Bijective ⇑(ConcreteCategory.hom (F.map f))

Tactic:
apply (Fintype.bijective_iff_injective_and_card (F.map f)).mpr

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
⊢ Function.Injective (F.map f) ∧ Fintype.card (F.obj X).carrier = Fintype.card (F.obj Y).carrier

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
⊢ IsIso (F.map f)

Tactic:
apply (ConcreteCategory.isIso_iff_bijective (F.map f)).mpr

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
⊢ Function.Bijective ⇑(ConcreteCategory.hom (F.map f))

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
⊢ IsIso f

Tactic:
have : IsIso (F.map f) := by
  apply (ConcreteCategory.isIso_iff_bijective (F.map f)).mpr
  apply (Fintype.bijective_iff_injective_and_card (F.map f)).mpr
  refine ⟨injective_of_mono_of_preservesPullback (F.map f), ?_⟩
  simp only [← Nat.card_eq_fintype_card, h]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
this : IsIso (F.map f)
⊢ IsIso f

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
⊢ Fintype.card (F.obj X).carrier = Fintype.card (F.obj Y).carrier

Tactic:
simp only [← Nat.card_eq_fintype_card, h]

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
this : IsIso (F.map f)
⊢ IsIso f

Tactic:
exact isIso_of_reflects_iso f F

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
⊢ Function.Injective (F.map f) ∧ Fintype.card (F.obj X).carrier = Fintype.card (F.obj Y).carrier

Tactic:
refine ⟨injective_of_mono_of_preservesPullback (F.map f), ?_⟩

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
⊢ Fintype.card (F.obj X).carrier = Fintype.card (F.obj Y).carrier