awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))
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)
⊢ 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 β : Type (w + 1)
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
⊢ IsGalois.{u₁, u₂} X ↔ MulAction.IsPretransitive.{u₂, w} (Aut X) (F.obj X).obj
have rw : Nonempty.{w + 1} (Unique (MulAction.orbitRel.Quotient.{u₂, w} (Aut X) (F.obj X).obj)) ↔
  MulAction.IsPretransitive.{u₂, w} (Aut X) (F.obj X).obj
Tactic: rw [isGalois_iff_aux, Equiv.nonempty_congr <| quotientByAutTerminalEquivUniqueQuotient F X]
-- 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 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
n : Aut F
ninstab : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) x) n
g : Aut F
⊢ (g * n * g⁻¹) • x = x
have change : g • n • g⁻¹ • x = x
Tactic: change g • n • (g⁻¹ • x) = x
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.GaloisObjects (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
X : C
inst_3 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
n : Aut F
ninstab : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) x) n
g : Aut F
⊢ g • n • g⁻¹ • x = x
have this : ∃ (φ : Aut 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 φ.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      x =
    g⁻¹ • x
Tactic: have : ∃ (φ : Aut X), F.map φ.hom x = g⁻¹ • x :=
      MulAction.IsPretransitive.exists_smul_eq x (g⁻¹ • x)
-- 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 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
n : Aut F
ninstab : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) x) n
g : Aut F
this :
  ∃ (φ : Aut 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 φ.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x =
      g⁻¹ • x
⊢ g • n • g⁻¹ • x = x
have obtain : ∀ (φ : Aut X)
  (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))
            _ _ _ (F.map φ.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x =
      g⁻¹ • x),
  g • n • g⁻¹ • x = x
Tactic: obtain ⟨φ, h⟩ := this
Cleared hypotheses: this
-- 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 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
n : Aut F
ninstab : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) x) n
g : Aut F
φ : Aut X
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))
          _ _ _ (F.map φ.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      x =
    g⁻¹ • x
⊢ g • n • g⁻¹ • x = x
have rw : g • g⁻¹ • x = x
Tactic: rw [← h, mulAction_naturality, ninstab, h]
-- 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
A : C
inst_3 : IsGalois.{u₁, u₂} A
a b : (F.obj A).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 (Iso.hom (((evaluationEquivOfIsGalois F A a).symm : (a : (F.obj A).obj) → Aut A) b)) :
            F.obj A ⟶ F.obj A) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    b
have change : (evaluationEquivOfIsGalois F A a : (a : Aut A) → (F.obj A).obj)
    (((evaluationEquivOfIsGalois F A a).symm : (a : (F.obj A).obj) → Aut A) b) =
  b
Tactic: change (evaluationEquivOfIsGalois F 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
A B : C
f : A ⟶ B
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ ∃! τ : Aut B, f ≫ τ.hom = σ.hom ≫ f
have obtain : ∀ (a : (F.obj A).obj), ∃! τ : Aut B, f ≫ τ.hom = σ.hom ≫ f
Tactic: obtain ⟨a⟩ := nonempty_fiber_of_isConnected F 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
A B : C
f : A ⟶ B
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ ∃! τ : Aut B, f ≫ τ.hom = σ.hom ≫ f
have refine_1 : Aut B
Tactic: refine ⟨?_, ?_, ?_⟩
-- 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
A B : C
f : A ⟶ B
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
refine_1 : Aut B
⊢ ∃! τ : Aut B, f ≫ τ.hom = σ.hom ≫ f
have refine_2 : (fun (τ : Aut B) ↦ f ≫ τ.hom = σ.hom ≫ f)
  (((evaluationEquivOfIsGalois F B
          ((@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 A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
            a)).symm :
      (a : (F.obj B).obj) → Aut B)
    ((@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 (σ.hom ≫ f)) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)))
Tactic: refine ⟨?_, ?_, ?_⟩
-- 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
X Y Z : C
inst_2 : IsConnected.{u₁, u₂} X
inst_3 : IsGalois.{u₁, u₂} Y
inst_4 : IsGalois.{u₁, u₂} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ autMap (f ≫ g) = autMap g ∘ autMap f
have refine : ∀ (σ : Aut X), (f ≫ g) ≫ ((autMap g ∘ autMap f) σ).hom = σ.hom ≫ f ≫ g
Tactic: refine funext fun σ ↦ autMap_unique _ σ _ ?_
-- 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
X Y Z : C
inst_2 : IsConnected.{u₁, u₂} X
inst_3 : IsGalois.{u₁, u₂} Y
inst_4 : IsGalois.{u₁, u₂} Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ g) ≫ ((autMap g ∘ autMap f) σ).hom = σ.hom ≫ f ≫ g
have rw : (f ≫ (autMap f σ).hom) ≫ g = σ.hom ≫ f ≫ g
Tactic: rw [Function.comp_apply, Category.assoc, comp_autMap, ← Category.assoc]
-- 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
A B : C
inst_2 : IsGalois.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ ∃ (a : Aut A), autMap f a = σ
have obtain : ∀ (a : (F.obj A).obj), ∃ (a : Aut A), autMap f a = σ
Tactic: obtain ⟨a⟩ := nonempty_fiber_of_isConnected F 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
A B : C
inst_2 : IsGalois.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ ∃ (a : Aut A), autMap f a = σ
have obtain : ∀ (a' : (F.obj A).obj)
  (ha' :
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
      ((@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 A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
          a' :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
      ((@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 σ.hom) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
          ((@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 A)) →
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
              a :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))),
  ∃ (a : Aut A), autMap f a = σ
Tactic: obtain ⟨a', ha'⟩ := surjective_of_nonempty_fiber_of_isConnected F f (F.map σ.hom (F.map f 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
A B : C
inst_2 : IsGalois.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a a' : (F.obj A).obj
ha' :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
    ((@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 A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
        a' :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
    ((@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 σ.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
        ((@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 A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
            a :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
τ : Aut A
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))
          _ _ _ (F.map τ.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    a'
⊢ ∃ (a : Aut A), autMap f a = σ
have h : autMap f τ = σ
Tactic: use τ
-- 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
A B : C
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
f : A ⟶ B
σ τ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ autMap f (σ * τ) = autMap f σ * autMap f τ
have obtain : ∀ (a : (F.obj A).obj), autMap f (σ * τ) = autMap f σ * autMap f τ
Tactic: obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
g : G
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (isoOnObj F g Y).hom = (isoOnObj F g X).hom ≫ F.map f
have h : ∀ (x : (F.obj X).obj),
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    ((@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 ≫ (isoOnObj F g Y).hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    ((@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))
            _ _ _ ((isoOnObj F g X).hom ≫ F.map f) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
⊢ NatIso.ofComponents (isoOnObj.{u₁, u₂, w, u_1} F (G := G) 1) ⋯ = 1
have h : ∀ (x : C) (x_1 : (F.obj x).obj),
  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))
            _ _ _ ((NatIso.ofComponents (isoOnObj.{u₁, u₂, w, u_1} F (G := G) 1) sorry).hom.app x) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj x)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj x))
        x_1 :
      (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))
            _ _ _ (NatTrans.app (Iso.hom 1) x : F.obj x ⟶ F.obj x) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj x)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj x))
        x_1 :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj x))
Tactic: ext