awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
refine_1 :
  Function.Injective (α := Y.V.obj) (β := (Action.V (Action.FintypeCat.ofMulAction G X)).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))
          _ _ _ i.hom) :
      (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
⊢ IsIso i.hom
have refine_2 : ∀ (x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj),
  ∃ (a : Y.V.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))
            _ _ _ i.hom :
          (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
        a =
      x'
Tactic: refine (ConcreteCategory.isIso_iff_bijective i.hom).mpr ⟨?_, fun x' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (hypothesis)
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
⊢ Function.Injective (α := Y.V.obj) (β := (Action.V (Action.FintypeCat.ofMulAction G X)).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))
          _ _ _ i.hom) :
      (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
have this : Mono i.hom
Tactic: haveI : Mono i.hom := map_mono (forget₂ _ _) i
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj
x : X.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))
        _ _ _ i.hom :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
    y
⊢ ∃ (a : Y.V.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))
            _ _ _ i.hom :
          (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
        a =
      x'
have refine_2 : ∀ (σ : G) (hσ : σ • x = x'),
  ∃ (a : Y.V.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))
            _ _ _ i.hom :
          (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
        a =
      x'
Tactic: obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq G x x'
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj
x : X.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))
        _ _ _ i.hom :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
    y
σ : G
hσ : σ • x = x'
⊢ ∃ (a : Y.V.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))
            _ _ _ i.hom :
          (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
        a =
      x'
have h₁ : (@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))
        _ _ _ i.hom :
      (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
    (σ • y) =
  x'
Tactic: use σ • y
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj
x : X.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))
        _ _ _ i.hom :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
    y
σ : G
hσ : σ • x = x'
⊢ (@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))
          _ _ _ i.hom :
        (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
      (σ • y) =
    x'
have h₁ : (@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))
        _ _ _ ((Y.ρ : (a : G) → End Y.V) σ ≫ i.hom : Y.V ⟶ Action.V (Action.FintypeCat.ofMulAction G X)) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
    y =
  x'
Tactic: change (Y.ρ σ ≫ i.hom) y = x'
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (hypothesis)
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
⊢ IsIso i
have this : IsIso i.hom
Tactic: have : IsIso i.hom := by
      refine (ConcreteCategory.isIso_iff_bijective i.hom).mpr ⟨?_, fun x' ↦ ?_⟩
      · haveI : Mono i.hom := map_mono (forget₂ _ _) i
        exact ConcreteCategory.injective_of_mono_of_preservesPullback i.hom
      · letI x : X := i.hom y
        obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq G x x'
        use σ • y
        change (Y.ρ σ ≫ i.hom) y = x'
        rw [i.comm, FintypeCat.comp_apply]
        exact hσ
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Full (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
inst_4 : IsConnected Y
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
    IsConnected.{u_1, v_1} Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f
have obtain : ∀
  (y :
    (obj
        (forget₂ (Action FintypeCat (Aut F)) (FC :=
          Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
          (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
          fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
          fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
        Y).obj),
  ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
    IsConnected.{u_1, v_1} Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f
Tactic: obtain ⟨y⟩ := nonempty_fiber_of_isConnected (forget₂ _ FintypeCat) Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Full (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
inst_4 : IsConnected Y
y :
  (obj
      (forget₂ (Action FintypeCat (Aut F)) (FC :=
        Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
        (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
        fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
      Y).obj
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
    IsConnected.{u_1, v_1} Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f
have obtain : ∀ (Z : C) (f : Z ⟶ X) (z : (F.obj Z).obj)
  (hz :
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      ((@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 f) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          z :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      ((@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))
              _ _ _ i.hom :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
          y :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V))
  (hc : IsConnected.{u_1, v_1} Z) (hm : Mono f),
  ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
    IsConnected.{u_1, v_1} Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f
Tactic: obtain ⟨Z, f, z, hz, hc, hm⟩ := fiber_in_connected_component F X (i.hom y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Full (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
inst_4 : IsConnected Y
y :
  (obj
      (forget₂ (Action FintypeCat (Aut F)) (FC :=
        Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
        (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
        fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
      Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@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 f) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@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))
            _ _ _ i.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
        y :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
hc : IsConnected.{u_1, v_1} Z
hm : Mono f
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
    IsConnected.{u_1, v_1} Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f
have this : IsConnected ((functorToAction F).obj Z)
Tactic: have : IsConnected ((functorToAction F).obj Z) := PreservesIsConnected.preserves
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Full (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i
have obtain : ∀ (ι : Type) (hf : Finite ι) (f : ι → Action FintypeCat (Aut F)) (t : ∐ f ≅ Y) (hc : ∀ (i : ι), IsConnected (f i)),
  ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i
Tactic: obtain ⟨ι, hf, f, t, hc⟩ := has_decomp_connected_components' Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Full (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i
have choose : ∀ (gZ : (i : ι) → C) (gf : (i : ι) → gZ i ⟶ X) (gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)),
  (∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)) →
    (∀ (i : ι), Mono (gf i)) →
      ∀ (h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)),
        ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i
Tactic: choose gZ gf gu _ _ h using fun i ↦ exists_lift_of_mono_of_isConnected F X (f i) (i' i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Full (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
⊢ (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
have simp : (functorToAction F).map (Sigma.desc gf) = is2.hom ≫ u'.inv ≫ t.hom ≫ i
Tactic: simp only [Iso.trans_inv, Iso.symm_inv, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Full (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
⊢ (functorToAction F).map (Sigma.desc gf) = is2.hom ≫ u'.inv ≫ t.hom ≫ i
have rw : is2.inv ≫ (functorToAction F).map (Sigma.desc gf) = u'.inv ≫ t.hom ≫ i
Tactic: rw [← Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Full (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
⊢ is2.inv ≫ (functorToAction F).map (Sigma.desc gf) = u'.inv ≫ t.hom ≫ i
have refine : ∀ (j : ι),
  Sigma.ι (C := Action FintypeCat (Aut F)) (fun (i : ι) ↦ (functorToAction F).obj (gZ i)) j ≫
      is2.inv ≫ (functorToAction F).map (Sigma.desc gf) =
    Sigma.ι (C := Action FintypeCat (Aut F)) (fun (i : ι) ↦ (functorToAction F).obj (gZ i)) j ≫ u'.inv ≫ t.hom ≫ i
Tactic: refine Sigma.hom_ext _ _ (fun j ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Full (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
j : ι
⊢ Sigma.ι (C := Action FintypeCat (Aut F)) (fun (i : ι) ↦ (functorToAction F).obj (gZ i)) j ≫
      is2.inv ≫ (functorToAction F).map (Sigma.desc gf) =
    Sigma.ι (C := Action FintypeCat (Aut F)) (fun (i : ι) ↦ (functorToAction F).obj (gZ i)) j ≫ u'.inv ≫ t.hom ≫ i
have suffices : (functorToAction F).map (gf j) = (gu j).inv ≫ i' j
Tactic: suffices (functorToAction F).map (gf j) = (gu j).inv ≫ i' j by
      simpa [is2, u']