-- Mathlib/CategoryTheory/Galois/Decomposition.lean
private lemma has_decomp_connected_components_aux (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
    (n : ℕ) : ∀ (X : C), n = Nat.card (F.obj X) → ∃ (ι : Type) (f : ι → C)
    (g : (i : ι) → (f i) ⟶ X) (_ : IsColimit (Cofan.mk X g)),
    (∀ i, IsConnected (f i)) ∧ Finite ι

Proof state:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).carrier → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).carrier
h : ¬IsConnected X
nhi : IsInitial X → False
Y : C
v : Y ⟶ X
hni : IsInitial Y → False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).carrier < n
i✝ : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier + Nat.card (F.obj Z).carrier
hn2 : Nat.card (F.obj Z).carrier < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
i : ι₁ ⊕ ι₂
⊢ IsConnected (Sum.elim f₁ f₂ i)

Tactic:
cases i

Result:
case h.inl
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).carrier → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).carrier
h : ¬IsConnected X
nhi : IsInitial X → False
Y : C
v : Y ⟶ X
hni : IsInitial Y → False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).carrier < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier + Nat.card (F.obj Z).carrier
hn2 : Nat.card (F.obj Z).carrier < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
val✝ : ι₁
⊢ IsConnected (Sum.elim f₁ f₂ (Sum.inl val✝))

case h.inr
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).carrier → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).carrier
h : ¬IsConnected X
nhi : IsInitial X → False
Y : C
v : Y ⟶ X
hni : IsInitial Y → False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).carrier < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier + Nat.card (F.obj Z).carrier
hn2 : Nat.card (F.obj Z).carrier < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
val✝ : ι₂
⊢ IsConnected (Sum.elim f₁ f₂ (Sum.inr val✝))

Proof state:
case pos.intro.intro.intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).carrier → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).carrier
h : ¬IsConnected X
nhi : IsInitial X → False
Y : C
v : Y ⟶ X
hni : IsInitial Y → False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).carrier < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier + Nat.card (F.obj Z).carrier
hn2 : Nat.card (F.obj Z).carrier < n
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
let ⟨ι₁, f₁, g₁, hc₁, hf₁, he₁⟩ := hi (Nat.card (F.obj Y)) hn1 Y rfl

Result:
case pos.intro.intro.intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).carrier → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).carrier
h : ¬IsConnected X
nhi : IsInitial X → False
Y : C
v : Y ⟶ X
hni : IsInitial Y → False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).carrier < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier + Nat.card (F.obj Z).carrier
hn2 : Nat.card (F.obj Z).carrier < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Proof state:
case pos.intro.intro.intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).carrier → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).carrier
h : ¬IsConnected X
nhi : IsInitial X → False
Y : C
v : Y ⟶ X
hni : IsInitial Y → False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).carrier < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier + Nat.card (F.obj Z).carrier
hn2 : Nat.card (F.obj Z).carrier < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
let ⟨ι₂, f₂, g₂, hc₂, hf₂, he₂⟩ := hi (Nat.card (F.obj Z)) hn2 Z rfl

Result:
case pos.intro.intro.intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).carrier → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).carrier
h : ¬IsConnected X
nhi : IsInitial X → False
Y : C
v : Y ⟶ X
hni : IsInitial Y → False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).carrier < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier + Nat.card (F.obj Z).carrier
hn2 : Nat.card (F.obj Z).carrier < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι