awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 }
⊢ Nat.card.{w} (F.obj Y).obj < n
have rw : Nat.card.{w} (F.obj Y).obj < Nat.card.{w} (F.obj X).obj
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (hypothesis)
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 }
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have hn1 : Nat.card.{w} (F.obj Y).obj < n
Tactic: have hn1 : Nat.card (F.obj Y) < n := by
      rw [hn]
      exact lt_card_fiber_of_mono_of_notIso F v hvnoiso
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have 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 ι
Tactic: have i : X ≅ Y ⨿ Z := (colimit.isoColimitCocone t).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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
have 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
Tactic: rw [card_fiber_eq_of_iso F i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (hypothesis)
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
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have hnn : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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
have rw : 0 < Nat.card.{w} (F.obj Y).obj
Tactic: rw [hn, hnn, lt_add_iff_pos_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (hypothesis)
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
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have hn2 : 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have 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 ι
Tactic: let ⟨ι₁, f₁, g₁, hc₁, hf₁, he₁⟩ := hi (Nat.card (F.obj Y)) hn1 Y rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have 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 ι
Tactic: let ⟨ι₂, f₂, g₂, hc₂, hf₂, he₂⟩ := hi (Nat.card (F.obj Z)) hn2 Z rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 ι
have 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 (ι₁ ⊕ ι₂)
Tactic: refine ⟨ι₁ ⊕ ι₂, Sum.elim f₁ f₂,
      Cofan.combPairHoms (Cofan.mk Y g₁) (Cofan.mk Z g₂) (BinaryCofan.mk v u), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 ι₂
⊢ ∃ (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 (ι₁ ⊕ ι₂)
have h₁ : (∀ (i : ι₁ ⊕ ι₂), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)) ∧ Finite (ι₁ ⊕ ι₂)
Tactic: use Cofan.combPairIsColimit hc₁ hc₂ c
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 (ι₁ ⊕ ι₂)
have h₁ : ∀ (i : ι₁ ⊕ ι₂), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)
Tactic: refine ⟨fun i ↦ ?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 : ι₁ ⊕ ι₂
⊢ IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)
have h₁ : ∀ (val : ι₁), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ (Sum.inl val))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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))
⊢ IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ i)
have h₂ : ∀ (val : ι₂), IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ (Sum.inr val))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (hypothesis)
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
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have nhi₁ : ∃ (x : IsInitial.{u₂, u₁} X), True
Tactic: simp only [not_forall, not_false_eq_true] at nhi
Cleared hypotheses: nhi
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 : ∃ (x : IsInitial.{u₂, u₁} X), True
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have neg : ∀ (hi : IsInitial.{u₂, u₁} X),
  True →
    ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
      (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
Tactic: obtain ⟨hi⟩ := nhi
Cleared hypotheses: nhi
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X : C
⊢ ∃ (ι : Type) (x : Finite ι) (f : ι → C) (x : sigmaObj.{0, u₂, u₁} f ≅ X), ∀ (i : ι), IsConnected.{u₁, u₂} (f i)
have obtain : ∀ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (hl : IsColimit (Cofan.mk X g))
  (hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)) (hf : Finite ι),
  ∃ (ι : Type) (x : Finite ι) (f : ι → C) (x : sigmaObj.{0, u₂, u₁} f ≅ X), ∀ (i : ι), IsConnected.{u₁, u₂} (f i)
Tactic: obtain ⟨ι, f, g, hl, hc, hf⟩ := has_decomp_connected_components X
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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
X : C
x : (F.obj X).obj
⊢ ∃ (Y : C) (i : Y ⟶ X) (y : (F.obj Y).obj),
    (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (F.map i) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          y =
        x ∧
      IsConnected.{u₁, u₂} Y ∧ Mono i
have obtain : ∀ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (hl : IsColimit (Cofan.mk X g))
  (hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)) (he : Finite ι),
  ∃ (Y : C) (i : Y ⟶ X) (y : (F.obj Y).obj),
    (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (F.map i) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          y =
        x ∧
      IsConnected.{u₁, u₂} Y ∧ Mono i
Tactic: obtain ⟨ι, f, g, hl, hc, he⟩ := has_decomp_connected_components X