awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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
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:
exact (ConcreteCategory.congr_hom (r.comm p.1) p.2).symm

Premises used: Prod.fst, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, Prod.snd, Action.Hom.comm
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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'

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
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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 : ι), 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)
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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 : ι
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))))
⊢ ∃ (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)

Premises used: CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected, CategoryTheory.forget₂, Action.V
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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 : ι
x : (f i).V.obj
U : OpenSubgroup G := { toSubgroup := MulAction.stabilizer G x, isOpen' := ⋯ }
⊢ ∃ (U : OpenSubgroup G),
    Nonempty.{u_1 + 1} (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑U : Subgroup G))))

Tactic:
⟨U, ⟨FintypeCat.isoQuotientStabilizerOfIsConnected (f i) x⟩⟩

Premises used: CategoryTheory.FintypeCat.isoQuotientStabilizerOfIsConnected, Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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 : ι
x : (f i).V.obj
U : OpenSubgroup G := { toSubgroup := MulAction.stabilizer G x, isOpen' := ⋯ }
⊢ ∃ (U : OpenSubgroup G),
    Nonempty.{u_1 + 1} (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑U : Subgroup G))))

Tactic:
exact ⟨U, ⟨FintypeCat.isoQuotientStabilizerOfIsConnected (f i) x⟩⟩
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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))))

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⟩⟩
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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))))
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)
⊢ ∃ (ι : 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
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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
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:
⟨ι, hf, g, ⟨(Sigma.mapIso (fun i ↦ (ui i).some)).symm ≪≫ u⟩⟩

Premises used: Nonempty.some, CategoryTheory.Limits.Sigma.mapIso, Nonempty.intro, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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
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:
exact ⟨ι, hf, g, ⟨(Sigma.mapIso (fun i ↦ (ui i).some)).symm ≪≫ u⟩⟩
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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 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))))
m :
  Quiver.Hom (V :=
    SingleObj.{u₁}
      (HasQuotient.Quotient ↥V (B := Subgroup ↥(↑V : Subgroup (Aut F)))
        ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
    (SingleObj.star
      (HasQuotient.Quotient ↥V (B := Subgroup ↥(↑V : Subgroup (Aut F)))
        ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
    (SingleObj.star
      (HasQuotient.Quotient ↥V (B := Subgroup ↥(↑V : Subgroup (Aut F)))
        ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
⊢ (functorToAction F).map
      ((quotientToEndObjectHom V h u :
          (a : ↥(↑V : Subgroup (Aut F)) ⧸ (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))) → End A)
        m) =
    u.hom ≫
      ((quotientToEndHom (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) :
              HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                  ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))) →*
                End (C := Action FintypeCat (Aut F))
                  (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F)))))) :
            (a : ↥(↑V : Subgroup (Aut F)) ⧸ (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))) →
              End (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))))
          m ≫
        u.inv

Tactic:
simp [← cancel_epi u.inv, ← cancel_mono u.hom, ← Iso.conj_apply, quotientToEndObjectHom]

Premises used: _private.0.CategoryTheory.PreGaloisCategory.quotientToEndObjectHom, CategoryTheory.cancel_mono, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Iso.conj_apply
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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)))
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))))))
⊢ 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))))))

Tactic:
apply Action.hom_ext

Premises used: Action.hom_ext
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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_1 : (↑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
h : ⟦μ * (↑σ⁻¹ : Aut F)⟧ = ⟦μ⟧
⊢ ((@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 ≫
                  (u.hom ≫
                      ((quotientToEndHom (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) :
                              HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                                  ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))) →*
                                End (C := Action FintypeCat (Aut F))
                                  (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F)))))) :
                            (a :
                                ↥(↑V : Subgroup (Aut F)) ⧸ (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))) →
                              End (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))))
                          ⟦σ⟧ ≫
                        u.inv) ≫
                    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)))))) :
          TypeCat.Fun
            (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F)))))).obj
            (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))).obj) :
        (a : (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).V.obj) →
          (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))).V.obj)
      ⟦μ⟧ =
    ⟦μ⟧

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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
h₁ : μ * (↑σ⁻¹ : Aut F) ≈ μ
⊢ ⟦μ * (↑σ⁻¹ : Aut F)⟧ = ⟦μ⟧

Tactic:
apply Quotient.sound

Premises used: Quotient.sound
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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
h₁ : (μ * (↑σ⁻¹ : Aut F))⁻¹ * μ ∈ (↑V : Subgroup (Aut F))
⊢ μ * (↑σ⁻¹ : Aut F) ≈ μ

Tactic:
apply (QuotientGroup.leftRel_apply).mpr

Premises used: Iff.mpr, QuotientGroup.leftRel_apply
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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))⁻¹ * μ ∈ (↑V : Subgroup (Aut F))

Tactic:
simp