awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
G : Functor.{u₂, w, u₁, w + 1} C FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], t.app X = s.app X
⊢ t = s
have w : ∀ (X : C) (x : (F.obj X).obj),
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.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))
            _ _ _ (t.app X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.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))
            _ _ _ (s.app X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
⊢ ∃ (ι : Type) (x : Finite ι) (f : ι → OpenSubgroup G),
    Nonempty.{u_1 + 1}
      ((∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑(f i) : Subgroup G)))) ≅ X)
have obtain : ∀ (ι : Type) (hf : Finite ι) (f : ι → Action FintypeCat G) (u : ∐ f ≅ X) (hc : ∀ (i : ι), IsConnected (f i)),
  ∃ (ι : Type) (x : Finite ι) (f : ι → OpenSubgroup G),
    Nonempty.{u_1 + 1}
      ((∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑(f i) : Subgroup G)))) ≅ X)
Tactic: obtain ⟨ι, hf, f, u, hc⟩ := has_decomp_connected_components' X
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
⊢ ∃ (ι : Type) (x : Finite ι) (f : ι → OpenSubgroup G),
    Nonempty.{u_1 + 1}
      ((∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑(f i) : Subgroup G)))) ≅ X)
have this₁ : ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj
Tactic: haveI (i : ι) : DiscreteTopology (f i).V := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this_1 : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
this : ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : (p : G × (f i).V.obj) → G × X.V.obj :=
  fun (p : G × (f i).V.obj) ↦
    (p.1,
      (@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))
            _ _ _ r.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
        p.2)
q : (p : G × X.V.obj) → X.V.obj :=
  fun (p : G × X.V.obj) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((X.ρ : (a : G) → End X.V) p.1)) :
        (a : (fun (X : Type u_1) ↦ X) X.V.obj) → (fun (X : Type u_1) ↦ X) X.V.obj)
      p.2
q' : (p : G × (f i).V.obj) → (f i).V.obj :=
  fun (p : G × (f i).V.obj) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) (((f i).ρ : (a : G) → End (f i).V) p.1)) :
        (a : (fun (X : Type u_1) ↦ X) (f i).V.obj) → (fun (X : Type u_1) ↦ X) (f i).V.obj)
      p.2
⊢ q ∘ r'' =
    (⇑(@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))
            _ _ _ r.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) ∘
      q'
have h : ∀ (p : G × (f i).V.obj),
  (q ∘ r'') p =
    ((⇑(@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))
              _ _ _ r.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) ∘
        q')
      p
Tactic: ext (p : G × (f i).V)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this_1 : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
this : ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : (p : G × (f i).V.obj) → G × X.V.obj :=
  fun (p : G × (f i).V.obj) ↦
    (p.1,
      (@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))
            _ _ _ r.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
        p.2)
q : (p : G × X.V.obj) → X.V.obj :=
  fun (p : G × X.V.obj) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((X.ρ : (a : G) → End X.V) p.1)) :
        (a : (fun (X : Type u_1) ↦ X) X.V.obj) → (fun (X : Type u_1) ↦ X) X.V.obj)
      p.2
q' : (p : G × (f i).V.obj) → (f i).V.obj :=
  fun (p : G × (f i).V.obj) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) (((f i).ρ : (a : G) → End (f i).V) p.1)) :
        (a : (fun (X : Type u_1) ↦ X) (f i).V.obj) → (fun (X : Type u_1) ↦ X) (f i).V.obj)
      p.2
⊢ Continuous (Y := (f i).V.obj) fun (p : G × (f i).V.obj) ↦ p.1 • p.2
have heq : q ∘ r'' =
  (⇑(@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))
          _ _ _ r.hom) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) ∘
    q'
Tactic: have heq : q ∘ r'' = r.hom ∘ q' := by
      ext (p : G × (f i).V)
      exact (ConcreteCategory.congr_hom (r.comm p.1) p.2).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this_1 : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
this : ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj
⊢ ∃ (ι : Type) (x : Finite ι) (f : ι → OpenSubgroup G),
    Nonempty.{u_1 + 1}
      ((∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑(f i) : Subgroup G)))) ≅ X)
have this₁ : ∀ (i : ι), ContinuousSMul G (f i).V.obj
Tactic: have (i : ι) : ContinuousSMul G (f i).V := ContinuousSMul.mk <| by
    let r : f i ⟶ X := Sigma.ι f i ≫ u.hom
    let r'' (p : G × (f i).V) : G × X.V := (p.1, r.hom p.2)
    let q (p : G × X.V) : X.V := (X.ρ p.1).hom p.2
    let q' (p : G × (f i).V) : (f i).V := ((f i).ρ p.1).hom p.2
    have heq : q ∘ r'' = r.hom ∘ q' := by
      ext (p : G × (f i).V)
      exact (ConcreteCategory.congr_hom (r.comm p.1) p.2).symm
    have hrinj : Function.Injective r.hom :=
      (ConcreteCategory.mono_iff_injective_of_preservesPullback r).mp <| mono_comp _ _
    let t₁ : TopologicalSpace (G × (f i).V) := inferInstance
    change @Continuous _ _ _ ⊥ q'
    have : TopologicalSpace.induced r.hom inferInstance = ⊥ := by
      rw [← le_bot_iff]
      exact fun s _ ↦ ⟨r.hom '' s, ⟨isOpen_discrete (r.hom '' s), Set.preimage_image_eq s hrinj⟩⟩
    rw [← this, continuous_induced_rng, ← heq]
    exact Continuous.comp continuous_smul (by fun_prop)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this_1 : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
this_2 : ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj
this : ∀ (i : ι), ContinuousSMul G (f i).V.obj
i : ι
⊢ ∃ (U : OpenSubgroup G),
    Nonempty.{u_1 + 1} (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑U : Subgroup G))))
have obtain : ∀ (x : (f i).V.obj),
  ∃ (U : OpenSubgroup G),
    Nonempty.{u_1 + 1} (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑U : Subgroup G))))
Tactic: obtain ⟨(x : (f i).V)⟩ := nonempty_fiber_of_isConnected (forget₂ _ _) (f i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this_1 : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
this_2 : ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj
this : ∀ (i : ι), ContinuousSMul G (f i).V.obj
⊢ ∃ (ι : Type) (x : Finite ι) (f : ι → OpenSubgroup G),
    Nonempty.{u_1 + 1}
      ((∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑(f i) : Subgroup G)))) ≅ X)
have this₁ : ∀ (i : ι),
  ∃ (U : OpenSubgroup G),
    Nonempty.{u_1 + 1} (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑U : Subgroup G))))
Tactic: have (i : ι) : ∃ (U : OpenSubgroup (G)), (Nonempty ((f i) ≅ G ⧸ₐ U.toSubgroup)) := by
    obtain ⟨(x : (f i).V)⟩ := nonempty_fiber_of_isConnected (forget₂ _ _) (f i)
    let U : OpenSubgroup (G) := ⟨MulAction.stabilizer (G) x, stabilizer_isOpen (G) x⟩
    exact ⟨U, ⟨FintypeCat.isoQuotientStabilizerOfIsConnected (f i) x⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this_1 : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
this_2 : ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj
this_3 : ∀ (i : ι), ContinuousSMul G (f i).V.obj
this :
  ∀ (i : ι),
    ∃ (U : OpenSubgroup G),
      Nonempty.{u_1 + 1} (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑U : Subgroup G))))
⊢ ∃ (ι : Type) (x : Finite ι) (f : ι → OpenSubgroup G),
    Nonempty.{u_1 + 1}
      ((∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑(f i) : Subgroup G)))) ≅ X)
have choose : ∀ (g : (i : ι) → OpenSubgroup G)
  (ui :
    ∀ (i : ι), Nonempty.{u_1 + 1} (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑(g i) : Subgroup G))))),
  ∃ (ι : Type) (x : Finite ι) (f : ι → OpenSubgroup G),
    Nonempty.{u_1 + 1}
      ((∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑(f i) : Subgroup G)))) ≅ X)
Tactic: choose g ui using this
Cleared hypotheses: this
-- 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
m :
  HasQuotient.Quotient ↥V (B := Subgroup ↥(↑V : Subgroup (Aut F)))
    ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))
⊢ Eq (α :=
    Quiver.Hom (V := Action FintypeCat (Aut F)) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F)))))
      (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))))
    (u.inv ≫
        CategoryStruct.comp (Y :=
          (quotientDiag V h u ⋙ functorToAction F).obj
            (SingleObj.star
              (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))))
          ((functorToAction F).map ((quotientDiag V h u).map m))
          (u.hom ≫ quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV) :
      Quiver.Hom (V := Action FintypeCat (Aut F))
        (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F)))))
        (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))))
    (quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV :
      Quiver.Hom (V := Action FintypeCat (Aut F))
        (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F)))))
        (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))))
have h₁ : Eq (α :=
  Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
    Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))))
  (Action.Hom.hom
      (u.inv ≫
        CategoryStruct.comp (Y :=
          (quotientDiag V h u ⋙ functorToAction F).obj
            (SingleObj.star
              (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))))
          ((functorToAction F).map ((quotientDiag V h u).map m))
          (u.hom ≫ quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV)) :
    Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
      Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))))
  (Action.Hom.hom (quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV) :
    Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
      Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))))
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
σ : ↥(↑V : Subgroup (Aut F))
μ : Aut F
⊢ ⟦μ * (↑σ⁻¹ : Aut F)⟧ = ⟦μ⟧
have h₁ : μ * (↑σ⁻¹ : Aut F) ≈ μ
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
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
σ : ↥(↑V : Subgroup (Aut F))
μ : Aut F
⊢ μ * (↑σ⁻¹ : Aut F) ≈ μ
have h₁ : (μ * (↑σ⁻¹ : Aut F))⁻¹ * μ ∈ (↑V : Subgroup (Aut F))
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
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)
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 ≫ coconeQuotientDiagDesc h u hUinV s = s.ι.app j
have apply : u.inv ≫ NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s =
  u.inv ≫ s.ι.app j
Tactic: apply (cancel_epi u.inv).mp
-- 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)
j :
  SingleObj.{u₁}
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))
⊢ u.inv ≫ NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s =
    u.inv ≫ s.ι.app j
have h₁ : Action.Hom.hom (u.inv ≫ NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s) =
  (u.inv ≫ s.ι.app j).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)
j :
  SingleObj.{u₁}
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))
⊢ Action.Hom.hom
      (u.inv ≫ NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s) =
    (u.inv ≫ s.ι.app j).hom
have h₁ : ∀ (x : Aut F ⧸ (↑U : 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))
            _ _ _
            (Action.Hom.hom
                (u.inv ≫
                  NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s) :
              Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶ s.pt.V) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).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))
            _ _ _ (u.inv ≫ s.ι.app j).hom :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).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 ⧸ U.toSubgroup)