awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
pos :
  ∀ (i : X ≅ coprod.{u₂, u₁} Y Z),
    ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
      (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
have i : X ≅ Y ⨿ Z := (colimit.isoColimitCocone t).symm
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
rw : Nat.card.{w} (F.obj (coprod.{u₂, u₁} Y Z)).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
⊢ Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj

Tactic:
rw [card_fiber_eq_of_iso F i]

Premises used: CategoryTheory.PreGaloisCategory.card_fiber_eq_of_iso
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
⊢ Nat.card.{w} (F.obj (coprod.{u₂, u₁} Y Z)).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj

Tactic:
card_fiber_coprod_eq_sum F Y Z

Premises used: CategoryTheory.PreGaloisCategory.card_fiber_coprod_eq_sum
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
⊢ Nat.card.{w} (F.obj (coprod.{u₂, u₁} Y Z)).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj

Tactic:
exact card_fiber_coprod_eq_sum F Y Z

Premises used: CategoryTheory.PreGaloisCategory.card_fiber_coprod_eq_sum
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
⊢ Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj

Tactic:
have hnn : Nat.card (F.obj X) = Nat.card (F.obj Y) + Nat.card (F.obj Z) := by
      rw [card_fiber_eq_of_iso F i]
      exact card_fiber_coprod_eq_sum F Y Z
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
rw : 0 < Nat.card.{w} (F.obj Y).obj
⊢ Nat.card.{w} (F.obj Z).obj < n

Tactic:
rw [hn, hnn, lt_add_iff_pos_left]

Premises used: lt_add_iff_pos_left
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
⊢ 0 < Nat.card.{w} (F.obj Y).obj

Tactic:
Nat.pos_of_ne_zero (non_zero_card_fiber_of_not_initial F Y hni)

Premises used: CategoryTheory.PreGaloisCategory.non_zero_card_fiber_of_not_initial, Nat.pos_of_ne_zero
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
⊢ 0 < Nat.card.{w} (F.obj Y).obj

Tactic:
exact Nat.pos_of_ne_zero (non_zero_card_fiber_of_not_initial F Y hni)

Premises used: CategoryTheory.PreGaloisCategory.non_zero_card_fiber_of_not_initial, Nat.pos_of_ne_zero
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
⊢ Nat.card.{w} (F.obj Z).obj < n

Tactic:
have hn2 : Nat.card (F.obj Z) < n := by
      rw [hn, hnn, lt_add_iff_pos_left]
      exact Nat.pos_of_ne_zero (non_zero_card_fiber_of_not_initial F Y hni)
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
pos :
  ∀ (ι₁ : Type) (f₁ : ι₁ → C) (g₁ : (i : ι₁) → f₁ i ⟶ Y) (hc₁ : IsColimit (Cofan.mk Y g₁))
    (hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)) (he₁ : Finite ι₁),
    ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
      (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
let ⟨ι₁, f₁, g₁, hc₁, hf₁, he₁⟩ := hi (Nat.card (F.obj Y)) hn1 Y rfl
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
pos :
  ∀ (ι₂ : Type) (f₂ : ι₂ → C) (g₂ : (i : ι₂) → f₂ i ⟶ Z) (hc₂ : IsColimit (Cofan.mk Z g₂))
    (hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)) (he₂ : Finite ι₂),
    ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
      (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
let ⟨ι₂, f₂, g₂, hc₂, hf₂, he₂⟩ := hi (Nat.card (F.obj Z)) hn2 Z rfl
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)
he₂ : Finite ι₂
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
⟨ι₁ ⊕ ι₂, Sum.elim f₁ f₂,
      Cofan.combPairHoms (Cofan.mk Y g₁) (Cofan.mk Z g₂) (BinaryCofan.mk v u), ?_⟩

Premises used: Sum, CategoryTheory.Limits.Cofan.combPairHoms, CategoryTheory.Limits.BinaryCofan.mk, Exists.intro, CategoryTheory.Limits.Cofan.mk, Sum.elim
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)
he₂ : Finite ι₂
pos :
  ∃ (x :
    IsColimit.{0, u₂, 0, u₁} (J := Discrete (ι₁ ⊕ ι₂)) (F := Discrete.functor (Sum.elim f₁ f₂))
      (Cofan.mk X
        ((Cofan.mk Y g₁).combPairHoms (Cofan.mk Z g₂) (BinaryCofan.mk v u) :
          (i : ι₁ ⊕ ι₂) → Sum.elim f₁ f₂ i ⟶ (BinaryCofan.mk v u).pt))),
    (∀ (i : ι₁ ⊕ ι₂), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)) ∧ Finite (ι₁ ⊕ ι₂)
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
refine ⟨ι₁ ⊕ ι₂, Sum.elim f₁ f₂,
      Cofan.combPairHoms (Cofan.mk Y g₁) (Cofan.mk Z g₂) (BinaryCofan.mk v u), ?_⟩
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)
he₂ : Finite ι₂
h₁ : (∀ (i : ι₁ ⊕ ι₂), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)) ∧ Finite (ι₁ ⊕ ι₂)
⊢ ∃ (x :
    IsColimit.{0, u₂, 0, u₁} (J := Discrete (ι₁ ⊕ ι₂)) (F := Discrete.functor (Sum.elim f₁ f₂))
      (Cofan.mk X
        ((Cofan.mk Y g₁).combPairHoms (Cofan.mk Z g₂) (BinaryCofan.mk v u) :
          (i : ι₁ ⊕ ι₂) → Sum.elim f₁ f₂ i ⟶ (BinaryCofan.mk v u).pt))),
    (∀ (i : ι₁ ⊕ ι₂), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)) ∧ Finite (ι₁ ⊕ ι₂)

Tactic:
use Cofan.combPairIsColimit hc₁ hc₂ c

Premises used: CategoryTheory.Limits.Cofan.combPairIsColimit
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)
he₂ : Finite ι₂
⊢ (∀ (i : ι₁ ⊕ ι₂), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)) ∧ Finite (ι₁ ⊕ ι₂)

Tactic:
⟨fun i ↦ ?_, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)
he₂ : Finite ι₂
h₁ : ∀ (i : ι₁ ⊕ ι₂), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)
⊢ (∀ (i : ι₁ ⊕ ι₂), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)) ∧ Finite (ι₁ ⊕ ι₂)

Tactic:
refine ⟨fun i ↦ ?_, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i_1 : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)
he₂ : Finite ι₂
i : ι₁ ⊕ ι₂
h₁ : ∀ (val : ι₁), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ (Sum.inl val))
h₂ : ∀ (val : ι₂), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ (Sum.inr val))
⊢ IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)

Tactic:
cases i
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)
he₂ : Finite ι₂
val : ι₁
⊢ IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ (Sum.inl val))

Tactic:
hf₁ _

Premises used: Sum.elim