awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (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
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
e : (Y : C) → Equiv.{u₂ + 1, w + 1} (F'.obj Y).obj (F.obj Y).obj := fun (Y : C) ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
hx' : x' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
y' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y
hy' : y' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y
⊢ ∃ (g : Aut F), g • x = y
have obtain : ∀ (g' : Aut F')
  (hg' :
    (@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))
            _ _ _ (g'.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' =
      y'),
  ∃ (g : Aut F), g • x = y
Tactic: obtain ⟨g', (hg' : g'.hom.app X x' = y')⟩ := MulAction.exists_smul_eq (Aut F') x' y'
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
σ τ : Aut F
h :
  Eq (α := (X : C) → Aut (F.obj X))
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ : (X : C) → Aut (F.obj X))
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) τ : (X : C) → Aut (F.obj X))
⊢ σ = τ
have h₁ : ∀ (X : C) (x : (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))
            _ _ _ (σ.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 :
      (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))
            _ _ _ (τ.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 :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
σ τ : Aut F
h :
  Eq (α := (X : C) → Aut (F.obj X))
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ : (X : C) → Aut (F.obj X))
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) τ : (X : C) → Aut (F.obj X))
X : C
x : (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))
            _ _ _ (σ.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 :
      (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))
            _ _ _ (τ.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 :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
have this : Iso.app σ X = Iso.app τ X
Tactic: have : σ.app X = τ.app X := congr_fun h X
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
⊢ Eq (α := Set ((X : C) → Aut (F.obj X)))
    (Set.range (ι := Aut F) (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)))
    (⋂ (f : Arrow.{u₂, u₁} C),
      {a : (X : C) → Aut (F.obj X) | F.map f.hom ≫ Iso.hom (a f.right) = Iso.hom (a f.left) ≫ F.map f.hom})
have h : ∀ (a : (X : C) → Aut (F.obj X)),
  Membership.mem (γ := Set ((X : C) → Aut (F.obj X)))
      (Set.range (ι := Aut F) (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X))) a ↔
    Membership.mem (γ := Set ((X : C) → Aut (F.obj X)))
      (⋂ (f : Arrow.{u₂, u₁} C),
        {a : (X : C) → Aut (F.obj X) | F.map f.hom ≫ Iso.hom (a f.right) = Iso.hom (a f.left) ≫ F.map f.hom})
      a
Tactic: ext a
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
a : (X : C) → Aut (F.obj X)
⊢ Membership.mem (γ := Set ((X : C) → Aut (F.obj X)))
      (Set.range (ι := Aut F) (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X))) a ↔
    Membership.mem (γ := Set ((X : C) → Aut (F.obj X)))
      (⋂ (f : Arrow.{u₂, u₁} C),
        {a : (X : C) → Aut (F.obj X) | F.map f.hom ≫ Iso.hom (a f.right) = Iso.hom (a f.left) ≫ F.map f.hom})
      a
have h : (∃ (y : Aut F), (autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) y = a) ↔
  ∀ (i : Arrow.{u₂, u₁} C), F.map i.hom ≫ Iso.hom (a i.right) = Iso.hom (a i.left) ≫ F.map i.hom
Tactic: simp +instances only [Set.mem_range, Set.mem_iInter, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
a : (X : C) → Aut (F.obj X)
⊢ (∃ (y : Aut F), (autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) y = a) ↔
    ∀ (i : Arrow.{u₂, u₁} C), F.map i.hom ≫ Iso.hom (a i.right) = Iso.hom (a i.left) ≫ F.map i.hom
have h : ∀ (h : ∀ (i : Arrow.{u₂, u₁} C), F.map i.hom ≫ Iso.hom (a i.right) = Iso.hom (a i.left) ≫ F.map i.hom),
  ∃ (y : Aut F), (autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) y = a
Tactic: refine ⟨fun ⟨σ, h⟩ i ↦ by cat_disch, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow.{u₂, u₁} C), F.map i.hom ≫ Iso.hom (a i.right) = Iso.hom (a i.left) ≫ F.map i.hom
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (a Y).hom = (a 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 ≫ (a 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))
            _ _ _ ((a 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.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
⊢ IsClosed (X := (X : C) → Aut (F.obj X))
    (Set.range (ι := Aut F) (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)))
have rw : IsClosed (X := (X : C) → Aut (F.obj X))
  (⋂ (f : Arrow.{u₂, u₁} C),
    {a : (X : C) → Aut (F.obj X) | F.map f.hom ≫ Iso.hom (a f.right) = Iso.hom (a f.left) ≫ F.map f.hom})
Tactic: rw [autEmbedding_range]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X : C
⊢ ContinuousSMul.{w, w} (Aut (F.obj X)) (F.obj X).obj
have continuous_smul : Continuous (Y := (F.obj X).obj) fun (p : Aut (F.obj X) × (F.obj X).obj) ↦ p.1 • p.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X : C
g : Aut (F.obj X) × (F.obj X).obj → (F.obj X).obj :=
  fun (x : Aut (F.obj X) × (F.obj X).obj) ↦
    match (motive := Aut (F.obj X) × (F.obj X).obj → (F.obj X).obj) x with
    | (σ, 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))
            _ _ _ σ.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x
h : (q : Aut F × (F.obj X).obj) → Aut (F.obj X) × (F.obj X).obj :=
  fun (q : Aut F × (F.obj X).obj) ↦
    (((fun (p : (X : C) → Aut (F.obj X)) ↦ p X) ∘ (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X))) q.1, q.2)
⊢ Continuous (Y := (F.obj X).obj) fun (p : Aut F × (F.obj X).obj) ↦ p.1 • p.2
have change : Continuous (g ∘ h)
Tactic: change Continuous (g ∘ h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : FintypeCat ⥤ FintypeCat
⊢ Continuous (X := Aut F) (Y := Aut (obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F))
    (⇑(mapAut F (obj (whiskeringRight C FintypeCat FintypeCat) G)) :
      (a : Aut F) → Aut (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F))
have rw : ∀ (i : C),
  Continuous (Y := Aut ((obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F).obj i)) fun (a : Aut F) ↦
    Function.comp (β := Aut (obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F))
      (⇑(autEmbedding (obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F)) :
        (a : Aut (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F)) →
          (X : C) → Aut ((((whiskeringRight C FintypeCat FintypeCat).obj G).obj F).obj X))
      (⇑(mapAut F (obj (whiskeringRight C FintypeCat FintypeCat) G)) :
        (a : Aut F) → Aut (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F))
      a i
Tactic: rw [Topology.IsInducing.continuous_iff (autEmbedding_isClosedEmbedding _).isInducing,
    continuous_pi_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : FintypeCat ⥤ FintypeCat
X : C
⊢ Continuous (Y := Aut ((obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F).obj X)) fun (a : Aut F) ↦
    Function.comp (β := Aut (obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F))
      (⇑(autEmbedding (obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F)) :
        (a : Aut (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F)) →
          (X : C) → Aut ((((whiskeringRight C FintypeCat FintypeCat).obj G).obj F).obj X))
      (⇑(mapAut F (obj (whiskeringRight C FintypeCat FintypeCat) G)) :
        (a : Aut F) → Aut (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F))
      a X
have change : Continuous (Y := Aut (G.obj (F.obj X))) fun (a : Aut F) ↦
  (mapAut (F.obj X) G : (a : Aut (F.obj X)) → Aut (G.obj (F.obj X)))
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) a X)
Tactic: change Continuous fun a ↦ G.mapAut (F.obj X) (autEmbedding F a X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
H : Set (Aut F)
h1 : 1 ∈ H
h : IsOpen H
⊢ ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ H
have obtain : ∀ (U : Set ((X : C) → Aut (F.obj X))) (hUopen : IsOpen U)
  (h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1)
  (h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)),
  ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F),
        (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
          Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
Tactic: obtain ⟨U, hUopen, rfl⟩ := isOpen_induced_iff.mp h
Cleared hypotheses: H, h1, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
⊢ ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F),
        (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
          Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
have obtain : ∀ (I : Finset C) (u : (a : C) → Set (Aut (F.obj a))) (ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a)
  (ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U),
  ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F),
        (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
          Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
Tactic: obtain ⟨I, u, ho, ha⟩ := isOpen_pi_iff.mp hUopen 1 h1
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
⊢ ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F),
        (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
          Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
have choose : ∀ (fι : (X : ↥I) → Type) (ff : (X : ↥I) → fι X → C) (fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C))
  (h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X)))
  (h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)) (h6 : ∀ (X : ↥I), Finite (fι X)),
  ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F),
        (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
          Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
Tactic: choose fι ff fc h4 h5 h6 using (fun X : I => has_decomp_connected_components X.val)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
⊢ ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F),
        (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
          Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
have refine_1 : ∀ (X : C), Membership.mem (γ := Set C) (⋃ (X : ↥I), Set.range (ff X)) X → IsConnected.{u₁, u₂} X
Tactic: refine ⟨⋃ X, Set.range (ff X), Fintype.ofFinite _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
refine_1 : ∀ (X : C), Membership.mem (γ := Set C) (⋃ (X : ↥I), Set.range (ff X)) X → IsConnected.{u₁, u₂} X
⊢ ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F),
        (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
          Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
have refine_2 : ∀ (σ : Aut F),
  (∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
    Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
Tactic: refine ⟨⋃ X, Set.range (ff X), Fintype.ofFinite _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
X : C
Y : ↥I
hA2 : Membership.mem (γ := Set C) ((fun (X : ↥I) ↦ Set.range (ff X)) Y) X
⊢ IsConnected.{u₁, u₂} X
have refine_1 : ∀ (i : fι Y), IsConnected.{u₁, u₂} (ff Y i)
Tactic: obtain ⟨i, rfl⟩ := hA2
Cleared hypotheses: X, hA2
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Topology (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
⊢ ∀ (σ : Aut F),
    (∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
      Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
have refine_2 : ∀ (σ : Aut F) (h : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) (X : C)
  (XinI : X ∈ (↑I : Set C)),
  Membership.mem (α := (fun (a : C) ↦ Aut (F.obj a)) X) (u X)
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X : Aut (F.obj X))
Tactic: refine fun σ h ↦ ha (fun X XinI ↦ ?_)