mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < ↑⌊c ^ i⌋₊, 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ ∑ i ∈ range N with j < c ^ i, 1 / ↑⌊c ^ i⌋₊ ^ 2

Tactic:
gcongr with k hk

Goal state after:
case h₂
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
k : ℕ
hk : k ∈ range N
⊢ ↑⌊c ^ k⌋₊ ≤ c ^ k
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case base
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := f x, property := ⋯ }.obj

Tactic:
| base x =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (ConcreteCategory.hom ((colimit.ι F i).app (Opposite.op A.left))) y
y' : CostructuredArrow yoneda (F.obj i) := CostructuredArrow.mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ ∃ i_1,
    ∃ x ∈ s i_1, (CostructuredArrow.map (colimit.ι F i_1)).obj x = (CostructuredArrow.map (colimit.ι F i)).obj (j i y')

Tactic:
exact ⟨i, j i y', hjs _ _, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ Mono (I.ι.f n)

Tactic:
cases n
  · exact mono_of_isLimit_fork I.isLimitKernelFork
  · rw [ι_f_succ]; infer_instance

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
ha : a ∈ (ModuleCat.Hom.hom x.hom).range
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range

Tactic:
obtain ⟨a', ha'⟩ := ha

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
ha : a ∈ (ModuleCat.Hom.hom y.hom).range
⊢ a ∈ (ModuleCat.Hom.hom x.hom).range

Tactic:
obtain ⟨a', ha'⟩ := ha

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
⊢ a ∈ (ModuleCat.Hom.hom x.hom).range
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ P.isoModSerre (Abelian.image.ι f)

Tactic:
rw [isoModSerre_iff_of_mono]
  dsimp [epiModSerre] at hf ⊢
  exact P.prop_of_iso
    (asIso (cokernel.map f _ (Abelian.factorThruImage f) (𝟙 Y) (by simp))) hf

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

Goal state before:
pp: ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
g : G
x : s.pt.V
j : ι
⊢ (ConcreteCategory.hom (s.pt.ρ g ≫ ↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x)).toFun x j =
    (ConcreteCategory.hom
          ((↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x) ≫
            { pt := ofMulAction G ((i : ι) → F i),
                    π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt.ρ
              g)).toFun
      x j

Tactic:
exact ConcreteCategory.congr_hom ((s.π.app ⟨j⟩).comm g) x

Goal state after:
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 : C
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.EssSurj
this : ∀ (W : D) (z : L.obj Y ⟶ W), L.map f ≫ z = 0 → ∃ l, L.map (cokernel.π f) ≫ l = z
s : Cofork (L.map f) 0
x✝¹ x✝ : (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) L).pt ⟶ s.pt
h₁ : Cofork.π (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) L) ≫ x✝¹ = s.π
h₂ : Cofork.π (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) L) ≫ x✝ = s.π
⊢ x✝¹ = x✝

Tactic:
by simpa [cancel_epi] using h₁.trans h₂.symm

Goal state after:
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
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ Action V G
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ forget V G)
⊢ PreservesLimit K F

Tactic:
let F' : C ⥤ SingleObj G ⥤ V := F ⋙ (Action.functorCategoryEquivalence V G).functor
  have : PreservesLimit K F' := SingleObj.preservesLimit _ _ h
  apply preservesLimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁴ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝³ : ConcreteCategory V FV
inst✝² : HasForget₂ V TopCat
G : Type u_4
inst✝¹ : Monoid G
inst✝ : TopologicalSpace G
X : Action V G
x : ↑((forget₂ (Action V G) TopCat).obj X)
⊢ 1 • x = x

Tactic:
change ((CategoryTheory.forget₂ _ TopCat).map (X.ρ 1)) x = x
    simp

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

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map (G.map (H.map (t.adj₁.unit.app X))) ≫ t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)

Tactic:
(asIso (t.adj₂.counit.app (G.obj _))).eq_comp_inv.2
      (t.adj₂.counit_naturality (t.adj₁.unit.app X)),

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map ((t.adj₂.counit.app ((𝟭 C).obj X) ≫ t.adj₁.unit.app X) ≫ (asIso (t.adj₂.counit.app (G.obj (F.obj X)))).inv) ≫
      t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
⊢ Mono (t.adj₂.unit.app (F.obj X))

Tactic:
simpa using h (F.obj X)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.map₂ (ρ_ (𝟙 { as := { as := () } })).hom ≫ (λ_ (F.map (𝟙 { as := { as := () } }))).inv =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv

Tactic:
F.map₂_inv_hom_assoc

Goal state after:
B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ (λ_ (F.map (𝟙 { as := { as := () } }))).inv = (λ_ (F.map (𝟙 { as := { as := () } }))).inv
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.map₂ (ρ_ (𝟙 { as := { as := () } })).hom ≫ (ρ_ (F.map (𝟙 { as := { as := () } }))).inv =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv

Tactic:
F.map₂_inv_hom_assoc

Goal state after:
B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ (ρ_ (F.map (𝟙 { as := { as := () } }))).inv = (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X✝ : Type u
C✝ : Cat
C : Cat
X : Type u
G : C ⟶ typeToCat.obj X
⊢ (TypeCat.homEquiv.trans
          ((ConnectedComponents.typeToCatHomEquiv (↑C) X).trans (Functor.equivCatHom (↑C) (Discrete X)))).symm
      G =
    connectedComponents.map G ≫
      { app := fun X ↦ ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj X)) (𝟙 typeToCat.obj X).toFunctor,
            naturality := ⋯ }.app
        X

Tactic:
by
      ext cc
      obtain ⟨_, _⟩ := Quotient.exists_rep cc
      cat_disch

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case mp.inl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inl b ∈ f a
⊢ b ∈ f.fix a'

Tactic:
cases Part.mem_unique ha' h'

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case mp.inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a✝ a' : α
ha' : Sum.inr a' ∈ f a✝
b : β
h : b ∈ f.fix a✝
a : α
h' : Sum.inr a ∈ f a✝
e' : b ∈ f.fix a
⊢ b ∈ f.fix a'

Tactic:
cases Part.mem_unique ha' h'

Goal state after:
case mp.inr.refl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inr a' ∈ f a
e' : b ∈ f.fix a'
⊢ b ∈ f.fix a'
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
⊢ eqToHom ⋯ ≫ ((s.π.app j).toFunctor ⋙ (F.map h).toFunctor).map f ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯

Tactic:
have := congr($((s.π.naturality h).symm).toFunctor)

Goal state after:
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
this : (s.π.app j ≫ F.map h).toFunctor = (((Functor.const J).obj s.pt).map h ≫ s.π.app j').toFunctor
⊢ eqToHom ⋯ ≫ ((s.π.app j).toFunctor ⋙ (F.map h).toFunctor).map f ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯
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
adj : map g ⊣ pullback g := mapPullbackAdj g
a' : (map g).obj (Over.mk b) ⟶ Over.mk f := homMk a h
⊢ lift a b h ≫ fst f g = a

Tactic:
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']

Goal state after:
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
adj : map g ⊣ pullback g := mapPullbackAdj g
a' : (map g).obj (Over.mk b) ⟶ Over.mk f := homMk a h
this : (map g).map ((adj.homEquiv (Over.mk b) (Over.mk f)) (homMk a ⋯)) ≫ fst' f g = a'
⊢ lift a b h ≫ fst f g = a
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₁.str ≫ F.map (inv f.f) = inv f.f ≫ V₀.str

Tactic:
by
        rw [IsIso.eq_inv_comp f.1, ← Category.assoc, ← f.h, Category.assoc]
        simp

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

Goal state before:
pp: case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ (map p f φ ⋯ (map p g ψ ⋯ τ) ≫ φ) ≫ ψ = τ

Tactic:
fac,

Goal state after:
case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ map p g ψ ⋯ τ ≫ ψ = τ
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
let Φ := domainUniqueUpToIso p (p.map φ) φ ψ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

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.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
ψ ψ' : b ⟶ b'
inst✝¹ : p.IsHomLift g ψ
inst✝ : p.IsHomLift g ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ ψ = ψ'

Tactic:
rw [map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ rfl, map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ' h.symm]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFiltered C
inst✝ : ∀ (c : C), IsFiltered ↑(F.obj c)
c : C
f : ↑(F.obj c)
⊢ Nonempty (Grothendieck F)

Tactic:
exact ⟨⟨c, f⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
this : Mono S.f
⊢ S.ShortExact

Tactic:
have : Epi S.g := by
      rw [hP.jointlyReflectEpimorphisms.epi_iff]
      exact fun i ↦ (hS i).epi_g

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
this✝ : Mono S.f
this : Epi S.g
⊢ S.ShortExact
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
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Tactic:
by
  obtain ⟨y⟩ := nonempty_fiber_of_isConnected (forget₂ _ FintypeCat) Y
  obtain ⟨Z, f, z, hz, hc, hm⟩ := fiber_in_connected_component F X (i.hom y)
  have : IsConnected ((functorToAction F).obj Z) := PreservesIsConnected.preserves
  obtain ⟨u, hu⟩ := connected_component_unique
    (forget₂ (Action FintypeCat (Aut F)) FintypeCat) (B := (functorToAction F).obj Z)
    y z i ((functorToAction F).map f) hz.symm
  refine ⟨Z, f, u, hc, hm, ?_⟩
  apply evaluation_injective_of_isConnected
    (forget₂ (Action FintypeCat (Aut F)) FintypeCat) Y ((functorToAction F).obj X) y
  suffices h : i.hom y = F.map f z by simpa [hu]
  exact hz.symm

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:
have : Mono (u ≫ prod.fst) := prod.lift_fst (𝟙 _) f ▸ inferInstance

Goal state after:
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 (u ≫ prod.fst)
⊢ Mono i
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
t : Aut F
⊢ (fun t ↦ asIso ((endMulEquivAutGalois F).symm t)) (((↑(endMulEquivAutGalois F)).comp (Aut.toEnd F)) t) = t

Tactic:
simp only [MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
      MulEquiv.symm_apply_apply]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
t : Aut F
⊢ asIso ((Aut.toEnd F) t) = t
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
t : (AutGalois F)ᵐᵒᵖ
⊢ ((↑(endMulEquivAutGalois F)).comp (Aut.toEnd F)) ((fun t ↦ asIso ((endMulEquivAutGalois F).symm t)) t) = t

Tactic:
by
    simp only [MonoidHom.coe_comp, MonoidHom.coe_coe]
    exact (MulEquiv.eq_symm_apply (endMulEquivAutGalois F)).mp rfl

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refl
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
f : c✝ ⟶ d✝
hf : f ∈ S.arrows c✝ d✝
c₄ : C
q : φ.obj d✝ ⟶ φ.obj c₄
hq : q ∈ {x | Map.Arrows φ hφ S (φ.obj d✝) (φ.obj c₄) x}
g : d✝ ⟶ c₄
he : φ.obj d✝ = φ.obj d✝
hg : g ∈ S.arrows d✝ c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ φ.map f ≫ q ∈ {x | Map.Arrows φ hφ S (φ.obj c✝) (φ.obj c₄) x}

Tactic:
rw [gq, ← eq_conj_eqToHom, ← φ.map_comp]

Goal state after:
case refl
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
f : c✝ ⟶ d✝
hf : f ∈ S.arrows c✝ d✝
c₄ : C
q : φ.obj d✝ ⟶ φ.obj c₄
hq : q ∈ {x | Map.Arrows φ hφ S (φ.obj d✝) (φ.obj c₄) x}
g : d✝ ⟶ c₄
he : φ.obj d✝ = φ.obj d✝
hg : g ∈ S.arrows d✝ c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ φ.map (f ≫ g) ∈ {x | Map.Arrows φ hφ S (φ.obj c✝) (φ.obj c₄) x}
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case inr
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
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
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
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
⊢ IsPullback (G.left.map f) (G.hom.app U) (G.hom.app V) (F.map f)

Tactic:
have inst : IsConnected (WithTerminal J) := isConnected_of_hasTerminal _

Goal state after:
case inr
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
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
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
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ IsPullback (G.left.map f) (G.hom.app U) (G.hom.app V) (F.map f)
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 Y : C
inst✝ : HasBinaryProduct X Y
⊢ IsPullback prod.fst prod.snd 0 0

Tactic:
by
  convert! @of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal
    <;> subsingleton

Goal state after: