awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
f : Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV) ⟶ s.pt
hf :
  ∀
    (j :
      SingleObj.{u₁}
        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))),
    NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ f = s.ι.app j
⊢ f = coconeQuotientDiagDesc h u hUinV s
have h₁ : f.hom = (coconeQuotientDiagDesc h u hUinV s).hom
Tactic: apply Action.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
f : Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV) ⟶ s.pt
hf :
  ∀
    (j :
      SingleObj.{u₁}
        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))),
    NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ f = s.ι.app j
⊢ f.hom = (coconeQuotientDiagDesc h u hUinV s).hom
have h₁ : ∀ (x : Aut F ⧸ (↑V : Subgroup (Aut F))),
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.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))
            _ _ _ f.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (coconeQuotientDiag h u hUinV).pt.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.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))
            _ _ _ (coconeQuotientDiagDesc h u hUinV s).hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (coconeQuotientDiag h u hUinV).pt.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
Tactic: ext (x : Aut F ⧸ V.toSubgroup)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have obtain : ∀ (I : Set C) (hf : Fintype (↑I : Type u₁)) (hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X)
  (hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))),
  ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
Tactic: obtain ⟨I, hf, hc, hi⟩ := exists_set_ker_evaluation_subset_of_isOpen F (one_mem V) V.isOpen'
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have this : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
Tactic: haveI (X : I) : IsConnected X.val := hc X X.property
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have this₁ : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
Tactic: haveI (X : I) : Nonempty (F.obj X.val) := nonempty_fiber_of_isConnected F X
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
Tactic: have hn : Nonempty (F.obj <| (∏ᶜ fun X : I => X)) := nonempty_fiber_pi_of_nonempty_of_finite F _
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have obtain : ∀ (A : C) (f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) (hgal : IsGalois.{u₁, u₂} A),
  ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
Tactic: obtain ⟨A, f, hgal⟩ := exists_hom_from_galois_of_fiber_nonempty F (∏ᶜ fun X : I => X) hn
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have obtain : ∀ (a : (F.obj A).obj),
  ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
Tactic: obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have hUnormal : (↑U : Subgroup (Aut F)).Normal
Tactic: have hUnormal : U.toSubgroup.Normal := stabilizer_normal_of_isGalois F A a
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U : Subgroup (Aut F)).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ Eq (α := Quotient (α := Aut F) (QuotientGroup.leftRel (MulAction.stabilizer (Aut F) a))) ⟦σ * τ⟧ ⟦τ⟧
have h : σ * τ ≈ τ
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U : Subgroup (Aut F)).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ σ * τ ≈ τ
have h : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a) ((σ * τ)⁻¹ * τ)
Tactic: apply (QuotientGroup.leftRel_apply).mpr
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U : Subgroup (Aut F)).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a) ((σ * τ)⁻¹ * τ)
have h : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a) (τ⁻¹ * σ⁻¹ * τ)
Tactic: simp only [mul_inv_rev]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U : Subgroup (Aut F)).Normal
σ : Aut F
σinU : σ ∈ U
⊢ σ.hom.app A = 𝟙 (F.obj A)
have hi₁ : Eq (α :=
  End
    (Action.V (G := Aut F)
      (Action.FintypeCat.ofMulAction (Aut F)
        (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))))
  ((Action.ρ
          (Action.FintypeCat.ofMulAction (Aut F)
            (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a)))) :
        (a_1 : Aut F) →
          End (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V)
      σ :
    End
      (Action.V (G := Aut F)
        (Action.FintypeCat.ofMulAction (Aut F)
          (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))))
  (𝟙
      (Action.V (G := Aut F)
        (Action.FintypeCat.ofMulAction (Aut F)
          (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))) :
    Action.V (G := Aut F)
        (Action.FintypeCat.ofMulAction (Aut F)
          (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a)))) ⟶
      Action.V (G := Aut F)
        (Action.FintypeCat.ofMulAction (Aut F)
          (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a)))))
Tactic: have hi : (Aut F ⧸ₐ MulAction.stabilizer (Aut F) a).ρ σ = 𝟙 _ := by
      refine FintypeCat.hom_ext _ _ (fun x ↦ ?_)
      induction x using Quotient.inductionOn with | _ τ
      change ⟦σ * τ⟧ = ⟦τ⟧
      apply Quotient.sound
      apply (QuotientGroup.leftRel_apply).mpr
      simp only [mul_inv_rev]
      exact Subgroup.Normal.conj_mem hUnormal _ (Subgroup.inv_mem U.toSubgroup σinU) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U : Subgroup (Aut F)).Normal
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have h1 : ∀ (σ : Aut F) (σinU : σ ∈ U), σ.hom.app A = 𝟙 (F.obj A)
Tactic: have h1 (σ : Aut F) (σinU : σ ∈ U) : σ.hom.app A = 𝟙 (F.obj A) := by
    have hi : (Aut F ⧸ₐ MulAction.stabilizer (Aut F) a).ρ σ = 𝟙 _ := by
      refine FintypeCat.hom_ext _ _ (fun x ↦ ?_)
      induction x using Quotient.inductionOn with | _ τ
      change ⟦σ * τ⟧ = ⟦τ⟧
      apply Quotient.sound
      apply (QuotientGroup.leftRel_apply).mpr
      simp only [mul_inv_rev]
      exact Subgroup.Normal.conj_mem hUnormal _ (Subgroup.inv_mem U.toSubgroup σinU) _
    simp [← cancel_mono u.hom.hom, show σ.hom.app A ≫ u.hom.hom = _ from u.hom.comm σ, hi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U : Subgroup (Aut F)).Normal
h1 : ∀ (σ : Aut F) (σinU : σ ∈ U), σ.hom.app A = 𝟙 (F.obj A)
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have h2 : ∀ (σ : Aut F) (σinU : σ ∈ U) (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
Tactic: have h2 (σ : Aut F) (σinU : σ ∈ U) : ∀ X : I, σ.hom.app X = 𝟙 (F.obj X) := by
    intro ⟨X, hX⟩
    ext (x : F.obj X)
    let p : A ⟶ X := f ≫ Pi.π (fun Z : I => (Z : C)) ⟨X, hX⟩
    have : IsConnected X := hc X hX
    obtain ⟨a, rfl⟩ := surjective_of_nonempty_fiber_of_isConnected F p x
    simp only [FintypeCat.id_apply, NatTrans.naturality_apply, h1 σ σinU]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U : Subgroup (Aut F)).Normal
h1 : ∀ (σ : Aut F) (σinU : σ ∈ U), σ.hom.app A = 𝟙 (F.obj A)
h2 : ∀ (σ : Aut F) (σinU : σ ∈ U) (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have hUinV : (↑U : Set (Aut F)) ≤ (↑V : Set (Aut F))
Tactic: have hUinV : (U : Set (Aut F)) ≤ V := fun u uinU ↦ hi u (h2 u uinU)