mathlib-initiative/mathlib-tactics huggingface dataset:
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
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
⊢ lift a b h ≫ fst f g = a

Tactic:
let adj := mapPullbackAdj g
  let a' : (Over.map g).obj (Over.mk b) ⟶ Over.mk f := Over.homMk a h
  have : (Over.map g).map (adj.homEquiv (.mk b) (.mk f) (Over.homMk a)) ≫ fst' f g = a' := by
    simp only [← Adjunction.homEquiv_counit, Equiv.symm_apply_apply, adj, a']
  exact congr_arg CommaMorphism.left this

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ≫
          (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
            L'.map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷
        L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁
          ((μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
            (μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
              L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom

Tactic:
whiskerLeft_comp,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ≫
          (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
            L'.map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷
        L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
          L'.obj X₁ ◁
            ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
              L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom
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 ▷ (enrichedHom V F₂ F₃ ⊗ enrichedHom V F₃ F₄) ≫
    ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁ (end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁
          eComp V (Opposite.unop (F₂.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j)

Tactic:
← 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
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) ≫
    ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁
        eComp V (Opposite.unop (F₂.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j) ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j)
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
hF : W.IsInvertedBy F
⊢ F.HasPointwiseLeftDerivedFunctor W

Tactic:
intro X

Goal state after:
C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
hF : W.IsInvertedBy F
X : C
⊢ F.HasPointwiseLeftDerivedFunctorAt W X
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 Y : C} (f : X ⟶ Y), Mono (F.map f) → Mono f

Tactic:
intro X

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ ∀ {Y : C} (f : X ⟶ Y), Mono (F.map f) → Mono f
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 Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj
⊢ Fintype.card ((fun X ↦ X.obj) (F.obj X)) = Fintype.card ((fun X ↦ X.obj) (F.obj Y))

Tactic:
simp only [← Nat.card_eq_fintype_card, h]

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

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
⊢ Nonempty (IsTerminal (colimit (SingleObj.functor (Aut.toEnd X)))) ↔ MulAction.IsPretransitive (Aut X) (F.obj X).obj

Tactic:
Equiv.nonempty_congr <| quotientByAutTerminalEquivUniqueQuotient F X

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
⊢ Nonempty (Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).obj)) ↔
    MulAction.IsPretransitive (Aut X) (F.obj X).obj
Module: Mathlib.CategoryTheory.Galois.Decomposition

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

Tactic:
intro X

Goal state after:
case ind
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
⊢ n = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
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:
simp [heq]

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
⊢ ∀ (i : C),
    Continuous fun a ↦
      (⇑(autEmbedding (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F)) ∘
          ⇑(mapAut F ((whiskeringRight C FintypeCat FintypeCat).obj G)))
        a i

Tactic:
intro X

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : FintypeCat ⥤ FintypeCat
X : C
⊢ Continuous fun a ↦
    (⇑(autEmbedding (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F)) ∘
        ⇑(mapAut F ((whiskeringRight C FintypeCat FintypeCat).obj G)))
      a X
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
⊢ ∀ (X : ↑I), t.hom.app ↑X = 𝟙 (F.obj ↑X)

Tactic:
intro X

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
X : ↑I
⊢ t.hom.app ↑X = 𝟙 (F.obj ↑X)
Module: Mathlib.CategoryTheory.Generator.Type

Goal state before:
pp: ⊢ IsSeparator PUnit.{u + 1}

Tactic:
intro X

Goal state after:
X : Type u
⊢ ∀ ⦃Y : Type u⦄ (f g : X ⟶ Y),
    (∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
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
g : G
⊢ ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (isoOnObj F g Y).hom = (isoOnObj F g X).hom ≫ F.map f

Tactic:
intro X

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
g : G
X : C
⊢ ∀ {Y : C} (f : X ⟶ Y), F.map f ≫ (isoOnObj F g Y).hom = (isoOnObj F g X).hom ≫ F.map f
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 y : G),
    NatIso.ofComponents (isoOnObj F (x * y)) ⋯ =
      NatIso.ofComponents (isoOnObj F x) ⋯ * NatIso.ofComponents (isoOnObj F y) ⋯

Tactic:
intro g h
    ext X x
    apply mul_smul

Goal state after:
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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
⊢ c.Nonempty

Tactic:
rw [← Set.univ_inter c]

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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
⊢ (Set.univ ∩ c).Nonempty
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: case htc
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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := ⋯
c : Set G := ⋯
⊢ ∀ (i : PointedGaloisObject F), IsClosed (cl i)

Tactic:
intro X

Goal state after:
case htc
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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
X : PointedGaloisObject F
⊢ IsClosed (cl X)
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: case h
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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs : ∀ (i : ↥s) (x : (F.obj (↑i).obj).obj), gs • x = (ConcreteCategory.hom (t.hom.app (↑i).obj)) x
⊢ ∀ i ∈ s, gs ∈ cl i

Tactic:
intro X

Goal state after:
case h
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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs : ∀ (i : ↥s) (x : (F.obj (↑i).obj).obj), gs • x = (ConcreteCategory.hom (t.hom.app (↑i).obj)) x
X : PointedGaloisObject F
⊢ X ∈ s → gs ∈ cl X
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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
g : G
hg : g ∈ c
X : C
x✝ : IsGalois X
x : (F.obj X).obj
⊢ g ∈ gi { obj := X, pt := x, isGalois := ⋯ } • ↑(MulAction.stabilizer G x)

Tactic:
simp only [Set.mem_iInter, c] at hg

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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
g : G
X : C
x✝ : IsGalois X
x : (F.obj X).obj
hg : ∀ (i : PointedGaloisObject F), g ∈ cl i
⊢ g ∈ gi { obj := X, pt := x, isGalois := ⋯ } • ↑(MulAction.stabilizer G x)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ d : C
⊢ 𝟙 c✝ ≫ 𝟙 c✝ ∈ {p | Discrete.Arrows c✝ c✝ p}

Tactic:
rw [Category.comp_id]

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ d : C
⊢ 𝟙 c✝ ∈ {p | Discrete.Arrows c✝ c✝ p}
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inr s ≫ 0 = PushoutCocone.inr s ≫ 𝟙 s.pt

Tactic:
by simpa using PushoutCocone.condition s

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
⊢ IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J

Tactic:
refine ⟨fun G ⟨⟨c, α, hc⟩, H⟩ i j f ↦ ⟨⟨by simp⟩, ⟨Limits.PullbackCone.isLimitAux' _ fun s ↦ ?_⟩⟩⟩

Goal state after:
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
⊢ { l //
    l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt},
          m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝ : W₂.HasTwoOutOfThreeProperty
⊢ W₂ ≤ (W₂.inverseImage Φ.functor).inverseImage ρ

Tactic:
intro X

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝ : W₂.HasTwoOutOfThreeProperty
X : C₂
⊢ ∀ ⦃Y : C₂⦄ (f : X ⟶ Y), W₂ f → (W₂.inverseImage Φ.functor).inverseImage ρ f
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝ : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
⊢ (W₂.inverseImage Φ.functor).inverseImage ρ f

Tactic:
have := i.naturality f

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝ : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
this : (𝟭 C₂).map f ≫ i.app Y = i.app X ≫ (ρ ⋙ Φ.functor).map f
⊢ (W₂.inverseImage Φ.functor).inverseImage ρ f
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case refine_1
J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
⊢ (MorphismProperty.pi fun x ↦ W) ≤ (W.functorCategory (Discrete J)).isoClosure.inverseImage E.functor

Tactic:
intro X

Goal state after:
case refine_1
J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
X : J → C
⊢ ∀ ⦃Y : J → C⦄ (f : X ⟶ Y),
    MorphismProperty.pi (fun x ↦ W) f → (W.functorCategory (Discrete J)).isoClosure.inverseImage E.functor f