awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι : 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
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i
have heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
Tactic: have heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i := by
    simp only [Iso.trans_inv, Iso.symm_inv, Category.assoc]
    rw [← Iso.inv_comp_eq]
    refine Sigma.hom_ext _ _ (fun j ↦ ?_)
    suffices (functorToAction F).map (gf j) = (gu j).inv ≫ i' j by
      simpa [is2, u']
    simp only [h, Iso.inv_hom_id_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
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i
have refine : Mono (X := sigmaObj.{0, v_1, u_1} gZ) (Sigma.desc gf)
Tactic: refine ⟨∐ gZ, Sigma.desc gf, t.symm ≪≫ u' ≪≫ is2.symm, ?_, by simp [heq]⟩
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
⊢ Mono i
have this : Mono (u ≫ prod.fst)
Tactic: have : Mono (u ≫ prod.fst) := prod.lift_fst (𝟙 _) f ▸ inferInstance
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono (u ≫ prod.fst)
⊢ Mono i
have this₁ : Mono u
Tactic: have : Mono u := mono_of_mono u prod.fst
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
⊢ ∃ (a : X ⟶ Y), (functorToAction F).map a = f
have this : Mono i
Tactic: have : Mono i := by
      have : Mono (u ≫ prod.fst) := prod.lift_fst (𝟙 _) f ▸ inferInstance
      have : Mono u := mono_of_mono u prod.fst
      apply mono_comp u _
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
⊢ ∃ (a : X ⟶ Y), (functorToAction F).map a = f
have obtain : ∀ (Z : C) (g : Z ⟶ Limits.prod.{v_1, u_1} X Y) (v : (functorToAction F).obj X ≅ (functorToAction F).obj Z),
  Mono g → ∀ (hvgi : v.hom ≫ (functorToAction F).map g = i), ∃ (a : X ⟶ Y), (functorToAction F).map a = f
Tactic: obtain ⟨Z, g, v, _, hvgi⟩ := exists_lift_of_mono F (Limits.prod X Y)
      ((functorToAction F).obj X) i
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
⊢ ∃ (a : X ⟶ Y), (functorToAction F).map a = f
have hgvi : (functorToAction F).map g = v.inv ≫ i
Tactic: have hgvi : (functorToAction F).map g = v.inv ≫ i := by simp [← hvgi]
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ IsIso ((functorToAction F).map ψ)
have simp : IsIso (v.inv ≫ i ≫ (functorToAction F).map prod.fst)
Tactic: simp only [map_comp, hgvi, 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ IsIso (i ≫ (functorToAction F).map prod.fst)
have suffices : IsIso (𝟙 ((functorToAction F).obj X))
Tactic: suffices h : IsIso (𝟙 ((functorToAction F).obj X)) by simpa [i, u]
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ IsIso (v.inv ≫ i ≫ (functorToAction F).map prod.fst)
have this₁ : IsIso (i ≫ (functorToAction F).map prod.fst)
Tactic: have : IsIso (i ≫ (functorToAction F).map prod.fst) := by
        suffices h : IsIso (𝟙 ((functorToAction F).obj X)) by simpa [i, u]
        infer_instance
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ ∃ (a : X ⟶ Y), (functorToAction F).map a = f
have this₁ : IsIso ((functorToAction F).map ψ)
Tactic: have : IsIso ((functorToAction F).map ψ) := by
      simp only [map_comp, hgvi, Category.assoc, ψ]
      have : IsIso (i ≫ (functorToAction F).map prod.fst) := by
        suffices h : IsIso (𝟙 ((functorToAction F).obj X)) by simpa [i, u]
        infer_instance
      apply IsIso.comp_isIso
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this : IsIso ((functorToAction F).map ψ)
⊢ ∃ (a : X ⟶ Y), (functorToAction F).map a = f
have this₁ : IsIso ψ
Tactic: have : IsIso ψ := isIso_of_reflects_iso ψ (functorToAction F)
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this_2 : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
⊢ ∃ (a : X ⟶ Y), (functorToAction F).map a = f
have h : (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = f
Tactic: use inv ψ ≫ g ≫ prod.snd
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this_2 : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
⊢ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = f
have h : (functorToAction F).map ψ ≫ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = (functorToAction F).map ψ ≫ f
Tactic: rw [← cancel_epi ((functorToAction F).map ψ)]
-- 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 Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this_2 : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
⊢ (functorToAction F).map ψ ≫ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = (functorToAction F).map ψ ≫ f
have h : ∀ (z : (F.obj Z).obj),
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
    ((@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))
            _ _ _ ((functorToAction F).map ψ ≫ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd)).hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Z).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
    ((@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))
            _ _ _ ((functorToAction F).map ψ ≫ f).hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Z).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
Tactic: ext (z : F.obj Z)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.GaloisObjects (goal)
Goal:
G : Type v
inst : Group G
inst_1 : Finite G
⊢ PreservesColimitsOfShape.{v, 0, w, w, w + 1, w + 1} (SingleObj G) FintypeCat.incl
have choose : ∀ (G' : Type) (hg : Group G') (hf : Fintype G') (e : Nonempty.{max 1 (v + 1)} (G ≃* G')),
  PreservesColimitsOfShape.{v, 0, w, w, w + 1, w + 1} (SingleObj G) FintypeCat.incl
Tactic: choose G' hg hf e using Finite.exists_type_univ_nonempty_mulEquiv G
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.GaloisObjects (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X : C
g h : Aut X
a : (F.obj X).obj
⊢ (g * h) • a = g • h • a
have change : 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 (h.hom ≫ g.hom)) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a :
    (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 h.hom ≫ F.map g.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a :
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
Tactic: change F.map (h.hom ≫ g.hom) a = (F.map h.hom ≫ F.map g.hom) a
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.GaloisObjects (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X : C
a : (F.obj X).obj
⊢ HSMul.hSMul.{u₂, w, w} (α := Aut X) 1 a = a
have change : (@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 (𝟙 X)) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    a =
  a
Tactic: change F.map (𝟙 X) a = a
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.GaloisObjects (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
inst_3 : IsConnected.{u₁, u₂} X
J : Functor.{u₂, u₂, 0, u₁} (SingleObj.{u₂} (Aut X)) C := SingleObj.functor (Aut.toEnd X)
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient.{u₂, w} (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) :=
  preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫ (SingleObj.Types.colimitEquivQuotient (J ⋙ F ⋙ FintypeCat.incl)).toIso
⊢ IsTerminal.{u₂, u₁} (colimit.{u₂, 0, u₂, u₁} (J := SingleObj.{u₂} (Aut X)) (SingleObj.functor (Aut.toEnd X))) ≃
    Unique (MulAction.orbitRel.Quotient.{u₂, w} (Aut X) (F.obj X).obj)
have e₁ : IsTerminal.{u₂, u₁} (colimit.{u₂, 0, u₂, u₁} (J := SingleObj.{u₂} (Aut X)) (SingleObj.functor (Aut.toEnd X))) ≃
  IsLimit
    (asEmptyCone
      (Quot (α := (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))
        (⇑(MulAction.orbitRel (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))) :
          (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) →
            (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) → Prop)))
Tactic: apply Equiv.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.GaloisObjects (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
inst_3 : IsConnected.{u₁, u₂} X
J : Functor.{u₂, u₂, 0, u₁} (SingleObj.{u₂} (Aut X)) C := SingleObj.functor (Aut.toEnd X)
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient.{u₂, w} (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) :=
  preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫ (SingleObj.Types.colimitEquivQuotient (J ⋙ F ⋙ FintypeCat.incl)).toIso
e₁ :
  IsTerminal.{u₂, u₁} (colimit.{u₂, 0, u₂, u₁} (J := SingleObj.{u₂} (Aut X)) (SingleObj.functor (Aut.toEnd X))) ≃
    IsLimit
      (asEmptyCone
        (Quot (α := (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))
          (⇑(MulAction.orbitRel (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))) :
            (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) →
              (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) → Prop)))
⊢ IsTerminal.{u₂, u₁} (colimit.{u₂, 0, u₂, u₁} (J := SingleObj.{u₂} (Aut X)) (SingleObj.functor (Aut.toEnd X))) ≃
    Unique (MulAction.orbitRel.Quotient.{u₂, w} (Aut X) (F.obj X).obj)
have e₂ : IsLimit
    (asEmptyCone
      (Quot (α := (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))
        (⇑(MulAction.orbitRel (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))) :
          (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) →
            (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) → Prop))) ≃
  Unique (MulAction.orbitRel.Quotient.{u₂, w} (Aut X) (F.obj X).obj)
Tactic: apply Equiv.trans