mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
a : ι₂
⊢ c₂.inj a ≫ inj bc WalkingPair.right ≫ m =
    c₂.inj a ≫
      inj bc WalkingPair.right ≫
        IsColimit.desc h fun i ↦
          WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
            (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
            (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
⊢ ∀ (X : C), n = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
w : WalkingPair
⊢ inj bc w ≫ m =
    inj bc w ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), IsConnected (f i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
⊢ ∃ Y i y, (ConcreteCategory.hom (F.map i)) y = x ∧ IsConnected Y ∧ Mono i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
j : ι
this : (functorToAction F).map (gf j) = (gu j).inv ≫ i' j
⊢ Sigma.ι (fun i ↦ (functorToAction F).obj (gZ i)) j ≫ is2.inv ≫ (functorToAction F).map (Sigma.desc gf) =
    Sigma.ι (fun i ↦ (functorToAction F).obj (gZ i)) j ≫ u'.inv ≫ t.hom ≫ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
⊢ (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
x✝² x✝¹ : (PointedGaloisObject F)ᵒᵖ
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝ :
  Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ Opposite.op { obj := B, pt := b, isGalois := isGalois✝ }
f :
  (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })).obj
hf : (ConcreteCategory.hom (F.map f)) b = a
Y : C
g : A ⟶ Y
h : (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map f)) b) = (ConcreteCategory.hom (F.map g)) a
⊢ (ConcreteCategory.hom
          ((((incl F).op ⋙ coyoneda).map (Opposite.op { val := f, comp := hf }) ≫
                match Opposite.op { obj := B, pt := b, isGalois := isGalois✝ } with
                | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
                  { app := fun X ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }).app
            Y)).toFun
      g =
    (ConcreteCategory.hom
          (((match Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } with
                | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
                  { app := fun X ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }) ≫
                ((const (PointedGaloisObject F)ᵒᵖ).obj (F ⋙ FintypeCat.incl)).map
                  (Opposite.op { val := f, comp := hf })).app
            Y)).toFun
      g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
⊢ (t.symm ≪≫ u' ≪≫ is2.symm).hom ≫ (functorToAction F).map (Sigma.desc gf) = i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
x✝² x✝¹ : (PointedGaloisObject F)ᵒᵖ
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝ :
  Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ Opposite.op { obj := B, pt := b, isGalois := isGalois✝ }
f :
  (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })).obj
hf : (ConcreteCategory.hom (F.map f)) b = a
⊢ (((incl F).op ⋙ coyoneda).map (Opposite.op { val := f, comp := hf }) ≫
      match Opposite.op { obj := B, pt := b, isGalois := isGalois✝ } with
      | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
        { app := fun X ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }) =
    (match Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } with
      | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
        { app := fun X ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }) ≫
      ((const (PointedGaloisObject F)ᵒᵖ).obj (F ⋙ FintypeCat.incl)).map (Opposite.op { val := f, comp := hf })

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
⊢ Mono i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
hn : ∀ (a : IsInitial Y), False
this✝ : IsIso u
this : IsIso v
hu : (ConcreteCategory.hom (G.map u)) y = a
hv : (ConcreteCategory.hom (G.map v)) y = b
⊢ (ConcreteCategory.hom (F.map u ≫ F.map ((asIso u).symm ≪≫ asIso v).hom)) y = (ConcreteCategory.hom (F.map v)) y

Tactic:
simp only [← F.map_comp, Iso.trans_hom, Iso.symm_hom, asIso_inv, asIso_hom,
    IsIso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) a = b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) (mkSelfProdFib F X) = t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
x✝¹ x✝ : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
⊢ ∃ W x x, True

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
x : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (selfProdProj u x))) a = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
⊢ (functorToAction F).map g = v.inv ≫ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
x✝³ x✝² : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝¹ x✝ : { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ { obj := B, pt := b, isGalois := isGalois✝ }
f : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hf :
  (ConcreteCategory.hom (F.map f)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
g : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hg :
  (ConcreteCategory.hom (F.map g)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
⊢ ∃ W h, h ≫ { val := f, comp := hf } = h ≫ { val := g, comp := hg }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
h : IsIso (𝟙 ((functorToAction F).obj X))
⊢ IsIso (i ≫ (functorToAction F).map prod.fst)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
⊢ (F.obj X).obj ≃ (F.obj X).obj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ IsIso (i ≫ (functorToAction F).map prod.fst)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ Function.Injective ⇑(autEmbedding F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X Y : C
⊢ instTopologicalSpaceHomFintypeCatObj F = ⊥

Tactic:
simp [DiscreteTopology.eq_bot]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X Y : C
⊢ instTopologicalSpaceHomFintypeCatObj F = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ IsIso ((functorToAction F).map ψ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
x✝ : ∃ y, (autEmbedding F) y = a
i : Arrow C
σ : Aut F
h : (autEmbedding F) σ = a
⊢ F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow C), F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (a Y).hom = (a X).hom ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ Set.range ⇑(autEmbedding F) = ⋂ f, {a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
⊢ (ConcreteCategory.hom (F.map u)) b = (ConcreteCategory.hom (F.map (selfProdPermIncl h b))) a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
f : Arrow C
⊢ Continuous fun a ↦ F.map f.hom ≫ (a f.right).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝² : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝¹ : IsConnected A
inst✝ : Mono u
b : (F.obj A).obj
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) b = a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
⊢ ∃ a, (functorToAction F).map a = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
f : Arrow C
⊢ Continuous fun a ↦ (a f.left).hom ≫ F.map f.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ IsClosed (Set.range ⇑(autEmbedding F))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
⊢ ContinuousSMul (Aut (F.obj X)) (F.obj X).obj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
⊢ ∃ A a, IsGalois A ∧ Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
⊢ ∃ A f a, IsGalois A ∧ (ConcreteCategory.hom (F.map f)) a = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
h : Nonempty (F.obj X).obj
⊢ ∃ A x, IsGalois A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
X : C
x : (F.obj X).obj
⊢ (ConcreteCategory.hom (t.app X)) x = (ConcreteCategory.hom (s.app X)) x

Tactic:
obtain ⟨A, f, a, _, rfl⟩ := exists_hom_from_galois_of_fiber F X x

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
X A : C
f : A ⟶ X
a : (F.obj A).obj
left✝ : IsGalois A
⊢ (ConcreteCategory.hom (t.app X)) ((ConcreteCategory.hom (F.map f)) a) =
    (ConcreteCategory.hom (s.app X)) ((ConcreteCategory.hom (F.map f)) a)
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
⊢ t = s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : FintypeCat ⥤ FintypeCat
⊢ Continuous ⇑(mapAut F ((whiskeringRight C FintypeCat FintypeCat).obj G))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Equivalence

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F✝ : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F✝
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : ContAction FintypeCat (Aut F)
⊢ (functorToContAction F).essImage X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ Continuous fun p ↦ X.obj.V.uSwitchEquiv.symm p

Tactic:
by

Goal state after: