mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    ((ConcreteCategory.hom
            ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv ≫ uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i)))
          a).down =
      ((ConcreteCategory.hom (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i)) a).down
⊢ ((ConcreteCategory.hom (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i))
        ((ConcreteCategory.hom (HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom)
          ((ConcreteCategory.hom (colimitYonedaHomIsoLimitOp F G).hom) η))).down =
    (ConcreteCategory.hom (η.app (op (F.obj (unop i)))))
      ((ConcreteCategory.hom ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))))) (𝟙 (F.obj (unop i))))

Tactic:
HasLimit.isoOfNatIso_hom_π_apply

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    ((ConcreteCategory.hom
            ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv ≫ uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i)))
          a).down =
      ((ConcreteCategory.hom (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i)) a).down
⊢ ((ConcreteCategory.hom ((F.op.associator G uliftFunctor.{u, v}).symm.hom.app i))
        ((ConcreteCategory.hom (limit.π (F.op ⋙ G ⋙ uliftFunctor.{u, v}) i))
          ((ConcreteCategory.hom (colimitYonedaHomIsoLimitOp F G).hom) η))).down =
    (ConcreteCategory.hom (η.app (op (F.obj (unop i)))))
      ((ConcreteCategory.hom ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))))) (𝟙 (F.obj (unop i))))
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ C
F : C ⥤ Type u₂
inst✝¹ : HasColimit (D.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) (op i)))
      ((ConcreteCategory.hom (colimitCoyonedaHomIsoLimit D F).hom) f) =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj (op i))))
          ((ConcreteCategory.hom ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)))) (𝟙 (D.obj (op i)))) }

Tactic:
change ((colimitCoyonedaHomIsoLimit D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) (op i))) f = _

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ C
F : C ⥤ Type u₂
inst✝¹ : HasColimit (D.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom ((colimitCoyonedaHomIsoLimit D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) (op i))) f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj (op i))))
          ((ConcreteCategory.hom ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)))) (𝟙 (D.obj (op i)))) }
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms → (yoneda.obj J).PreservesEpimorphisms

Tactic:
intro
    exact (inferInstance : (preadditiveYonedaObj J ⋙ forget _).PreservesEpimorphisms)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsZero (Ψ.r.obj (Φ.quotient.obj X))
inv : (Φ.colon Ψ).r.obj X ⟶ (KernelFork.ofι (Φ.ι.app X) ⋯).pt
hinv : inv ≫ Fork.ι (KernelFork.ofι (Φ.ι.app X) ⋯) = (Φ.colon Ψ).ι.app X
⊢ IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X)

Tactic:
dsimp at hinv

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsZero (Ψ.r.obj (Φ.quotient.obj X))
inv : (Φ.colon Ψ).r.obj X ⟶ (KernelFork.ofι (Φ.ι.app X) ⋯).pt
hinv : inv ≫ Φ.ι.app X = (Φ.colon Ψ).ι.app X
⊢ IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X)
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extMk f m hm hf + R.extMk g m hm hg = R.extMk (f + g) m hm ⋯

Tactic:
by
  simp only [extMk, Preadditive.comp_add]
  rw [Cocycle.toSingleMk_add _ _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
p : ℕ
hp : p + 1 = n
x✝ :
  ∃ g,
    ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-↑p) p ⋯).inv) ≫ g =
      (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f
g : R.cochainComplex.X (-↑p) ⟶ Y
hg :
  ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-↑p) p ⋯).inv) ≫ g =
    (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f
⊢ (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-↑p) p ⋯).inv ≫ g =
    (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f

Tactic:
simpa [Category.assoc] using hg

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ P.isoModSerre.IsStableUnderBaseChange

Tactic:
by
  dsimp [isoModSerre]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ P.isoModSerre.IsStableUnderCobaseChange

Tactic:
by
  dsimp [isoModSerre]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Injective X
⊢ IsIso
    (((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).liftCycles (F.map (𝟙 X)) 1
      toRightDerivedZero'._proof_1 ⋯)

Tactic:
rw [CochainComplex.isIso_liftCycles_iff]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Injective X
⊢ { X₁ := F.obj X, X₂ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).X 0,
        X₃ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).X 1,
        f := F.map (𝟙 X),
        g := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).d 0 1,
        zero := ⋯ }.Exact ∧
    Mono (F.map (𝟙 X))
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
⊢ ∀ {X Y Z : C} (i : Y ⟶ Z), isomorphisms C i → ∀ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P Q (f ≫ i)

Tactic:
intro X Y Z i hi f ⟨hY, hZ⟩
    rw [isomorphisms.iff] at hi
    exact ⟨hY, (Q.prop_iff_of_isIso i).mp hZ⟩

Goal state after:
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
⊢ ⟨fun b ↦ F.map (homOfPair b 1), 1⟩ = 1

Tactic:
ext1

Goal state after:
case left
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
⊢ ⟨fun b ↦ F.map (homOfPair b 1), 1⟩.left = left 1

case right
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
⊢ ⟨fun b ↦ F.map (homOfPair b 1), 1⟩.right = right 1
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
⊢ f = g

Tactic:
rw [lift_unique f, lift_unique g]

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
⊢ lift (f.comp inl) (f.comp inr) ⋯ = lift (g.comp inl) (g.comp inr) ⋯
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (x y : R) (b : F ⟶ G), (x * y) • b = x • y • b

Tactic:
by
        intros
        ext
        apply mul_smul

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

Goal state before:
pp: case succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
⊢ ((ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f).2 x =
    (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ).2 x

Tactic:
induction x using Fin.cases
    <;> simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]
    <;> rfl

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 (inv (q.adj₁.counit.app (G.obj X)) ≫ L.map (q.adj₂.counit.app X))) ↔
    ∀ (X : D), Mono (q.adj₃.unit.app (F.obj X))

Tactic:
simp_rw [epi_comp_iff_of_epi, epi_iff_forall_injective, mono_iff_forall_injective]

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) (Z : D), Function.Injective fun g ↦ L.map (q.adj₂.counit.app X) ≫ g) ↔
    ∀ (X : D) (Z : C), Function.Injective fun g ↦ g ≫ q.adj₃.unit.app (F.obj X)
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case cons
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih :
  (inclusionPath a b✝ ⋙ (normalize B).mapFunctor a b✝).obj { as := a✝¹ } = (𝟭 (Discrete (Path a b✝))).obj { as := a✝¹ }
⊢ (inclusionPath a c✝ ⋙ (normalize B).mapFunctor a c✝).obj { as := a✝¹.cons a✝ } =
    (𝟭 (Discrete (Path a c✝))).obj { as := a✝¹.cons a✝ }

Tactic:
ext1

Goal state after:
case cons
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih :
  (inclusionPath a b✝ ⋙ (normalize B).mapFunctor a b✝).obj { as := a✝¹ } = (𝟭 (Discrete (Path a b✝))).obj { as := a✝¹ }
⊢ ((inclusionPath a c✝ ⋙ (normalize B).mapFunctor a c✝).obj { as := a✝¹.cons a✝ }).as =
    ((𝟭 (Discrete (Path a c✝))).obj { as := a✝¹.cons a✝ }).as
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f g : a ⟶ b
hfg₁ : f.base = g.base
hfg₂ : f.fiber = g.fiber ≫ eqToHom ⋯
⊢ f = g

Tactic:
by
  cases f; cases g
  dsimp at hfg₁
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a : ∫ᶜ F
⊢ { base := (𝟙 a).base,
      fiber :=
        (α.app { as := op a.base }).toFunctor.map (𝟙 a).fiber ≫
          (α.naturality (𝟙 a).base.op.toLoc).hom.toNatTrans.app a.fiber } =
    𝟙 { base := a.base, fiber := (α.app { as := op a.base }).toFunctor.obj a.fiber }

Tactic:
ext1

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a : ∫ᶜ F
⊢ { base := (𝟙 a).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (𝟙 a).fiber ≫
            (α.naturality (𝟙 a).base.op.toLoc).hom.toNatTrans.app a.fiber }.base =
    (𝟙 { base := a.base, fiber := (α.app { as := op a.base }).toFunctor.obj a.fiber }).base

case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a : ∫ᶜ F
⊢ { base := (𝟙 a).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (𝟙 a).fiber ≫
            (α.naturality (𝟙 a).base.op.toLoc).hom.toNatTrans.app a.fiber }.fiber =
    (𝟙 { base := a.base, fiber := (α.app { as := op a.base }).toFunctor.obj a.fiber }).fiber ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ limitConeLift F s = m

Tactic:
ext1

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ (limitConeLift F s).toFunctor = m.toFunctor
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
⊢ f ≫ eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯ = 𝟙 R

Tactic:
subst_hom_lift p f φ.hom; simp [← p.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
⊢ (eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯) ≫ f = 𝟙 S

Tactic:
subst_hom_lift p f φ.hom; simp [← p.map_comp]

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

Goal state before:
pp: case refine_2
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.FintypeCat.ofMulAction G X).V.obj
x : X.obj := (ConcreteCategory.hom i.hom) y
⊢ ∃ a, (ConcreteCategory.hom i.hom) a = x'

Tactic:
obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq G x x'

Goal state after:
case refine_2
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.FintypeCat.ofMulAction G X).V.obj
x : X.obj := (ConcreteCategory.hom i.hom) y
σ : G
hσ : σ • x = x'
⊢ ∃ a, (ConcreteCategory.hom i.hom) a = x'
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
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz : (ConcreteCategory.hom (F.map f)) z = (ConcreteCategory.hom i.hom) y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom)) y = z
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Tactic:
refine ⟨Z, f, u, hc, hm, ?_⟩

Goal state after:
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
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz : (ConcreteCategory.hom (F.map f)) z = (ConcreteCategory.hom i.hom) y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom)) y = z
⊢ i = u.hom ≫ (functorToAction F).map f
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
f g : End F
A : PointedGaloisObject F
⊢ (ConcreteCategory.hom (f.app A.obj)) ((ConcreteCategory.hom (g.app A.obj)) A.pt) =
    (ConcreteCategory.hom (f.app A.obj ≫ F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom)) A.pt

Tactic:
← f.naturality,

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ (ConcreteCategory.hom (f.app A.obj)) ((ConcreteCategory.hom (g.app A.obj)) A.pt) =
    (ConcreteCategory.hom (F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom ≫ f.app A.obj)) A.pt
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
t : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
x : (F.obj X).obj
hg : g • x = (ConcreteCategory.hom (t.app X)) x
y : (F.obj X).obj
⊢ g • y = (ConcreteCategory.hom (t.app X)) y

Tactic:
obtain ⟨φ, (rfl : F.map φ.hom y = x)⟩ := MulAction.exists_smul_eq (Aut X) y x
  have : Function.Injective (F.map φ.hom) :=
    ConcreteCategory.injective_of_mono_of_preservesPullback (F.map φ.hom)
  apply this
  rw [IsNaturalSMul.naturality, hg, FunctorToFintypeCat.naturality]

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
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (ConcreteCategory.hom (t.hom.app (X i))) x

Tactic:
let x (i : ι) : F.obj (X i) := (nonempty_fiber_of_isConnected F (X i)).some
  let P : C := ∏ᶜ X
  let is₁ : F.obj P ≅ ∏ᶜ fun i ↦ (F.obj (X i)) := PreservesProduct.iso F X
  let is₂ : (∏ᶜ fun i ↦ F.obj (X i) : FintypeCat) ≃ ∀ i, F.obj (X i) :=
    Limits.FintypeCat.productEquiv (fun i ↦ (F.obj (X i)))
  let px : F.obj P := is₁.inv (is₂.symm x)
  have hpx (i : ι) : F.map (Pi.π X i) px = x i := by
    simp only [px, is₁, is₂, ← piComparison_comp_π, ← PreservesProduct.iso_hom,
      FintypeCat.comp_apply]
    rw [FintypeCat.inv_hom_id_apply, FintypeCat.productEquiv_symm_comp_π_apply]
  obtain ⟨A, f, a, _, hfa⟩ := exists_hom_from_galois_of_fiber F P px
  obtain ⟨g, hg⟩ := toAut_surjective_isGalois F G t A
  refine ⟨g, fun i y ↦ action_ext_of_isGalois F (x i) ?_ _⟩
  rw [← hpx i, ← IsNaturalSMul.naturality, FunctorToFintypeCat.naturality,
    ← hfa, FunctorToFintypeCat.naturality, ← IsNaturalSMul.naturality, hg]

Goal state after:
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
X : PointedGaloisObject F
hXmem : X ∈ s
⊢ (gi X)⁻¹ * gs ∈ MulAction.stabilizer G X.pt

Tactic:
MulAction.mem_stabilizer_iff,

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
hXmem : X ∈ s
⊢ ((gi X)⁻¹ * gs) • X.pt = X.pt