mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Mono f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) → ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
⊢ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Mono f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) → ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
⊢ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Epi f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Epi (L.map f) → ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Epi f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Epi (L.map f) → ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteLimits V
this : PreservesFiniteLimits ((evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ PreservesFiniteLimits ((functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
apply comp_preservesFiniteLimits

Goal state after:
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
g : G
⊢ F.map (𝟙 (𝟙_ V)) ≫ η F = η F ≫ 𝟙 (𝟙_ W)

Tactic:
rw [map_id, Category.id_comp, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (X : C), Epi (q.leftTriple.rightToLeft.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.leftToRight.app X)

Tactic:
mono_leftToRight_app_iff_mono_adj₂_unit_app,

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (X : C), Epi (q.leftTriple.rightToLeft.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.adj₂.unit.app (F.obj X))
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫ η.app a ◁ ((Γ.as.app a ▷ H.map f ≫ ι.naturality f)) ⊗≫
              η.naturality f ▷ (ι.app b) ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality f ⊗≫
              ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫ 𝟙 _ := by
          rw [Γ.as.naturality]
          bicategory
        _ = _ := by
          rw [whisker_exchange]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Core C
f g : X ⟶ Y
h : f.iso.hom = g.iso.hom
⊢ f = g

Tactic:
apply CoreHom.ext
  exact Iso.ext h

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq t l r b
φ : X₁ ⟶ Y₂
hφ : t ≫ r = φ
⊢ l ≫ b = φ

Tactic:
by rw [← hφ, sq.w]

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := ⋯
i : J
hi : i ∈ l
⊢ Zigzag j₂ j₂

Tactic:
· apply Relation.ReflTransGen.refl

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

pp: case inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : b ∈ f.fix a'
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

Tactic:
· refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
      · injection Part.mem_unique ⟨h₁, h₂⟩ h'
      · rw [WellFounded.fixF_eq]
        -- Porting note: used to be simp [h₁, h₂]
        apply Part.mem_assert h₁
        split
        next e =>
          injection h₂.symm.trans e with h; simp [h]
        next e =>
          injection h₂.symm.trans e

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : b ∈ f.fix a'
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case mpr
X Y : RelCat
r : X ⟶ Y
⊢ (∃ f, graphFunctor.map f.hom = r) → IsIso r

Tactic:
rintro ⟨f, rfl⟩
    apply graphFunctor.map_isIso

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝² : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst✝¹ : ChosenPullbacksAlong g'
inst✝ : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_3
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_5
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_7
⊢ g'' ≫ δ₃ ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g

Tactic:
by rw [reassoc_of% comm₂', comm₂, assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ C
H I : B ⥤ C
α : F ⟶ G
β : H ⟶ I
X Y : A ⊕ B
f : X ⟶ Y
⊢ ((F.sum' H).map f ≫
      match Y with
      | inl X => α.app X
      | inr X => β.app X) =
    (match X with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map f

Tactic:
by
    cases f <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i)) ≫
    (ρ_ (F₁.obj i ⟶[V] F₃.obj i)).inv ≫
      (F₁.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)

Tactic:
rw [assoc, tensorHom_def_assoc]

Goal state after:
V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
      eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ≫
        (ρ_ (F₁.obj i ⟶[V] F₃.obj i)).inv ≫
          (F₁.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)
Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : HasFibers p
S : 𝒮
a : Fib p S
⊢ p.obj ((ι S).obj a) = S

Tactic:
by
  simp only [← comp_obj, comp_const, const_obj_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
⊢ (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      (α_ (F₁.obj j ⟶[V] F₂.obj j) (F₂.obj j ⟶[V] F₃.obj j) (F₃.obj j ⟶[V] F₄.obj j)).inv ≫
        (eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ▷ F₃.obj j ⟶[V] F₄.obj j) ≫ eComp V (F₁.obj j) (F₃.obj j) (F₄.obj j) =
    (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      (F₁.obj j ⟶[V] F₂.obj j) ◁ eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₄.obj j)

Tactic:
e_assoc

Goal state after:
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
⊢ (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      (F₁.obj j ⟶[V] F₂.obj j) ◁ eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₄.obj j) =
    (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      (F₁.obj j ⟶[V] F₂.obj j) ◁ eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₄.obj j)
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
⊢ (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j))) ≫
      ((diagram V F₁ F₂).obj (Opposite.op j)).map f =
    (s.π.app j' ≫ enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j'))) ≫
      ((diagram V F₁ F₂).map f.op).app j'

Tactic:
dsimp
    rw [← s.w f, assoc, assoc, assoc]
    -- this was produced by `simp?`
    simp only [functorEnrichedHom_obj, functorEnrichedHom_map, end_.lift_π_assoc, diagram_obj_obj,
      Functor.comp_obj, Under.forget_obj, Under.mk_right, Under.map_obj_right, Iso.refl_inv,
      NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom, eHomWhiskerLeft_id, comp_id]
    have := enrichedHom_condition V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)
      (Under.homMk f : Under.mk (𝟙 j) ⟶ Under.mk f)
    dsimp at this
    rw [this]
    congr 3
    simp [Under.map, Comma.mapLeft]
    rfl

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ (∀ (a : IsInitial X), False) ↔ Nonempty (F.obj X).obj

Tactic:
rw [← not_isEmpty_iff]
  refine ⟨fun h he ↦ ?_, fun h hin ↦ h <| (initial_iff_fiber_empty F X).mp ⟨hin⟩⟩
  exact Nonempty.elim ((initial_iff_fiber_empty F X).mpr he) h

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

Goal state before:
pp: G : Type u
inst✝ : Group G
⊢ PreservesFiniteLimits (Action.forget FintypeCat G ⋙ FintypeCat.incl)

Tactic:
apply comp_preservesFiniteLimits

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
g h : Aut X
a : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (h.hom ≫ g.hom))) a = (ConcreteCategory.hom (F.map h.hom ≫ F.map g.hom)) a

Tactic:
simp only [map_comp, FintypeCat.comp_apply]

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
this✝ : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
⊢ ∃ a, (functorToAction F).map a = f

Tactic:
use inv ψ ≫ g ≫ prod.snd

Goal state after:
case h
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 := ⋯
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) := ⋯
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 := ⋯
hgvi : (functorToAction F).map g = v.inv ≫ i
this✝ : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
⊢ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = f
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
    ext; simpa using ConcreteCategory.congr_hom (h ⟨X, Y, f⟩) _

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 : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).obj
fi1 : A ≅ A
hfi1 : (ConcreteCategory.hom (F.map fi1.hom)) x = a
fi2 : A ≅ A
hfi2 : (ConcreteCategory.hom (F.map fi2.hom)) y = a
⊢ fi1 ≪≫ fi2.symm • x = y

Tactic:
change F.map (fi1.hom ≫ fi2.inv) x = y

Goal state after:
case h
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
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).obj
fi1 : A ≅ A
hfi1 : (ConcreteCategory.hom (F.map fi1.hom)) x = a
fi2 : A ≅ A
hfi2 : (ConcreteCategory.hom (F.map fi2.hom)) y = a
⊢ (ConcreteCategory.hom (F.map (fi1.hom ≫ fi2.inv))) x = y
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 : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).obj
fi1 : A ≅ A
hfi1 : (ConcreteCategory.hom (F.map fi1.hom)) x = a
fi2 : A ≅ A
hfi2 : (ConcreteCategory.hom (F.map fi2.hom)) y = a
⊢ (ConcreteCategory.hom (F.map (fi1.hom ≫ fi2.inv))) x = y

Tactic:
simp only [map_comp, FintypeCat.comp_apply]

Goal state after:
case h
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
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).obj
fi1 : A ≅ A
hfi1 : (ConcreteCategory.hom (F.map fi1.hom)) x = a
fi2 : A ≅ A
hfi2 : (ConcreteCategory.hom (F.map fi2.hom)) y = a
⊢ (ConcreteCategory.hom (F.map fi2.inv)) ((ConcreteCategory.hom (F.map fi1.hom)) x) = y
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 : C
inst✝ : IsConnected X
A : C
f : A ⟶ X
hgal : IsGalois A
hs : Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
x y : (F.obj X).obj
a : (F.obj A).obj
ha : (ConcreteCategory.hom (F.map f)) a = x
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨b, hb⟩ := hs y

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
A : C
f : A ⟶ X
hgal : IsGalois A
hs : Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
x y : (F.obj X).obj
a : (F.obj A).obj
ha : (ConcreteCategory.hom (F.map f)) a = x
b : (F.obj A).obj
hb : (ConcreteCategory.hom (F.map f)) b = y
⊢ ∃ g, g • x = y
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : 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 ↦ ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.obj → G × X.V.obj := fun p ↦ (p.1, (ConcreteCategory.hom r.hom) p.2)
q : G × X.V.obj → X.V.obj := fun p ↦ (ConcreteCategory.hom (X.ρ p.1).hom) p.2
q' : G × (f i).V.obj → (f i).V.obj := fun p ↦ (ConcreteCategory.hom ((f i).ρ p.1).hom) p.2
heq : q ∘ r'' = ⇑(ConcreteCategory.hom r.hom) ∘ q'
hrinj : Function.Injective ⇑(ConcreteCategory.hom r.hom)
t₁ : TopologicalSpace (G × (f i).V.obj) := inferInstance
⊢ TopologicalSpace.induced (⇑(ConcreteCategory.hom r.hom)) inferInstance = ⊥

Tactic:
← le_bot_iff

Goal state after:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : 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 ↦ ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.obj → G × X.V.obj := fun p ↦ (p.1, (ConcreteCategory.hom r.hom) p.2)
q : G × X.V.obj → X.V.obj := fun p ↦ (ConcreteCategory.hom (X.ρ p.1).hom) p.2
q' : G × (f i).V.obj → (f i).V.obj := fun p ↦ (ConcreteCategory.hom ((f i).ρ p.1).hom) p.2
heq : q ∘ r'' = ⇑(ConcreteCategory.hom r.hom) ∘ q'
hrinj : Function.Injective ⇑(ConcreteCategory.hom r.hom)
t₁ : TopologicalSpace (G × (f i).V.obj) := inferInstance
⊢ TopologicalSpace.induced (⇑(ConcreteCategory.hom r.hom)) inferInstance ≤ ⊥
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
x✝¹ : C
x✝ : (F.obj x✝¹).obj
⊢ (ConcreteCategory.hom ((NatIso.ofComponents (isoOnObj F 1) ⋯).hom.app x✝¹)) x✝ =
    (ConcreteCategory.hom ((Iso.hom 1).app x✝¹)) x✝

Tactic:
dsimp [isoOnObj]

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
x✝¹ : C
x✝ : (F.obj x✝¹).obj
⊢ 1 • x✝ = (ConcreteCategory.hom ((Iso.hom 1).app x✝¹)) x✝