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

Goal state before:
pp: case refine_1
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✝
X Y : C
f : X ⟶ Y
hf : Epi (L.map f)
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))

Tactic:
rw [epi_map_iff L P] at hf

Goal state after:
case refine_1
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✝
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map 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✝ : HasFiniteColimits V
⊢ PreservesFiniteColimits (forget V G)

Tactic:
by
  change PreservesFiniteColimits ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))
  have : PreservesFiniteColimits ((evaluation (SingleObj G) V).obj (SingleObj.star G)) := by
    constructor
    intro _ _ _
    infer_instance
  apply comp_preservesFiniteColimits

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

Goal state before:
pp: case inr
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
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
⊢ ∃ l, L.map (cokernel.π f) ≫ l = w

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.isoModSerre
      (w ≫ (L.objObjPreimageIso W).inv)
    rw [← cancel_mono (L.map φ.s), Category.assoc,
      MorphismProperty.LeftFraction.map_comp_map_s] at hφ
    obtain ⟨l, hl⟩ := this _ (L.map φ.f) (by rw [← hφ, reassoc_of% hw, zero_comp]) ⟨_, rfl, by simp⟩
    exact ⟨l ≫ inv (L.map φ.s) ≫ (L.objObjPreimageIso W).hom, by simp [reassoc_of% hl, ← hφ]⟩

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
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
let v : G × (forget₂ _ TopCat).obj X → H × (forget₂ _ TopCat).obj X := fun p ↦ (f p.1, p.2)

Goal state after:
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
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
⊢ Continuous fun p ↦ p.1 • p.2
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: case refine_1
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ s.ι ≫ (h X).left = s.ι ≫ (h X).right

Tactic:
← cancel_mono (adj₁.unit.app ((h X).Z)),

Goal state after:
case refine_1
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ (s.ι ≫ (h X).left) ≫ adj₁.unit.app (h X).Z = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
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
⊢ t.leftToRight =
    F.leftUnitor.inv ≫
      inv (whiskerRight t.adj₂.counit F) ≫ (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom

Tactic:
by
  ext X; dsimp [leftToRight]; simp only [Category.id_comp, Category.comp_id, NatIso.isIso_inv_app]
  rw [IsIso.comp_inv_eq, Category.assoc, IsIso.eq_inv_comp]
  refine Eq.trans ?_ (t.adj₁.counit_naturality <| (whiskerRight t.adj₁.unit H).app X)
  rw [whiskerRight_app _ H, (asIso (t.adj₂.counit.app (G.obj _))).eq_comp_inv.2
      (t.adj₂.counit_naturality (t.adj₁.unit.app X)),
    ← (asIso _).comp_hom_eq_id.1 <| t.adj₂.left_triangle_components (F.obj X)]
  simp

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

Goal state before:
pp: case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η' : Hom₂ f g
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
induction η' with
  | id => simp
  | vcomp η θ ihf ihg =>
    simp only [mk_vcomp, whiskerLeft_comp]
    slice_lhs 2 3 => rw [ihg]
    slice_lhs 1 2 => rw [ihf]
    simp
  -- p ≠ nil required! See the docstring of `normalizeAux`.
  | whisker_left _ _ ih =>
    dsimp
    rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
    simp
  | whisker_right h η' ih =>
    dsimp
    rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]
    have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))
    dsimp at this; simp [this]
  | _ => simp

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
⊢ (𝟭 (a ⟶ b)).map η ≫ ((λ_ g).symm ≪≫ normalizeIso nil g).hom =
    ((λ_ f).symm ≪≫ normalizeIso nil f).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map η

Tactic:
leftUnitor_inv_naturality_assoc,

Goal state after:
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
⊢ (λ_ ((𝟭 (a ⟶ b)).obj f)).inv ≫ 𝟙 a ◁ (𝟭 (a ⟶ b)).map η ≫ (normalizeIso nil g).hom =
    ((λ_ f).symm ≪≫ normalizeIso nil f).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map η
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:
| cons _ _ ih =>

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
⊢ StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h) =
    StructuredArrow.hom (t.whisker h)

Tactic:
← cancel_mono (α_ _ _ _).inv

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
⊢ (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
    StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:

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

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
⊢ 𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ leftZigzag adj.unit adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) = s.unit

Tactic:
by
          rw [adj.left_triangle]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ 𝟙 (h ≫ 𝟙 a) ⊗≫ ((h ≫ 𝟙 a) ◁ adj.unit ≫ s.unit ▷ (f ≫ u)) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u) =
    s.unit ⊗≫ s.lift ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (s.lift ≫ u)

Tactic:
whisker_exchange,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ 𝟙 (h ≫ 𝟙 a) ⊗≫ (s.unit ▷ 𝟙 a ≫ (s.lift ≫ u) ◁ adj.unit) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u) =
    s.unit ⊗≫ s.lift ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (s.lift ≫ u)
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ τ = 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift

Tactic:
by
          rw [adj.left_triangle]; bicategory

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

Goal state before:
pp: case e'_3
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
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫
      (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
        L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y =
    ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫
      (L'.obj X' ⊗ L'.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y
this :
  ((e₁.symm.hom ⊗ₘ ε.symm.hom) ⊗ₘ e₂.symm.hom) ≫
      (α_ (L'.obj X') (L.obj (𝟙_ C)) (L'.obj Y')).hom ≫ (e₁.symm.inv ⊗ₘ ε.symm.inv ⊗ₘ e₂.symm.inv) =
    (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom
e_1✝ : ((X ⊗ 𝟙_ (LocalizedMonoidal L W ε)) ⊗ Y ⟶ X ⊗ Y) = ((X ⊗ unit) ⊗ Y ⟶ X ⊗ Y)
⊢ (ρ_ X).hom ▷ Y =
    ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫
      (L'.obj X' ⊗ L'.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y

Tactic:
· exact triangle_aux₃ _ _ _ e₁ e₂

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
S : 𝒮
ha : 𝒳.p.obj a = S
⊢ 𝒴.p.IsHomLift (𝟙 S) (α.app a)

Tactic:
subst ha; infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p✝ : 𝒳 ⥤ 𝒮
S✝ : 𝒮
p : 𝒳 ⥤ 𝒮
S : 𝒮
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ 𝒳
hF : F ⋙ p = (const C).obj S
X✝ Y✝ : C
φ : X✝ ⟶ Y✝
⊢ p.map (F.map φ) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ 𝟙 S

Tactic:
simpa using (eqToIso hF).hom.naturality φ

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

Goal state before:
pp: case refine_2
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift g χ'
hφ' : (forget F).IsHomLift (g ≫ f) (χ' ≫ cartesianLift a f)
⊢ χ' = homCartesianLift f g (χ' ≫ cartesianLift a f)

Tactic:
obtain ⟨rfl⟩ : g = χ'.1 := by simpa using IsHomLift.fac (forget F) g χ'

Goal state after:
case refine_2
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift χ'.base χ'
hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)
⊢ χ' = homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: 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₁ S₂ : ShortComplex C
f : S₁ ⟶ S₂
hf : ∀ (i : I), ShortComplex.QuasiIso ((F i).mapShortComplex.map f)
⊢ ShortComplex.QuasiIso f

Tactic:
simp only [ShortComplex.quasiIso_iff] at hf ⊢

Goal state after:
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₁ S₂ : ShortComplex C
f : S₁ ⟶ S₂
hf : ∀ (i : I), IsIso (ShortComplex.homologyMap ((F i).mapShortComplex.map f))
⊢ IsIso (ShortComplex.homologyMap f)
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝² : Group G
X : Action FintypeCat G
inst✝¹ : IsConnected X
x : X.V.obj
inst✝ : Fintype (G ⧸ MulAction.stabilizer G x)
this : MulAction.IsPretransitive G X.V.obj
e : X.V.obj ≃ G ⧸ MulAction.stabilizer G x :=
  (Equiv.Set.univ X.V.obj).symm.trans ((Equiv.setCongr ⋯).trans (MulAction.orbitEquivQuotientStabilizer G x))
σ τ : G
⊢ (ConcreteCategory.hom
        ((Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).ρ σ ≫
          (FintypeCat.equivEquivIso e.symm).hom))
      ⟦τ⟧ =
    (ConcreteCategory.hom ((FintypeCat.equivEquivIso e.symm).hom ≫ X.ρ σ)) ⟦τ⟧

Tactic:
exact mul_smul σ τ x

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

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

Tactic:
let i' (j : ι) : f j ⟶ (functorToAction F).obj X := Sigma.ι f j ≫ t.hom ≫ i

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
ι : 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
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
⊢ ∃ a, (ConcreteCategory.hom ((autGaloisSystem F).map f)) a = φ

Tactic:
obtain ⟨ψ, hψ⟩ := autMap_surjective_of_isGalois f.val φ

Goal state after:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
ψ : Aut A.obj
hψ : autMap f.val ψ = φ
⊢ ∃ a, (ConcreteCategory.hom ((autGaloisSystem F).map f)) a = φ
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 : End F
A : PointedGaloisObject F
⊢ (ConcreteCategory.hom
        (F.map
          (↑((ConcreteCategory.hom ((sectionsFunctor (PointedGaloisObject F)).map (autIsoFibers F).inv))
                  ((endEquivSectionsFibers F) f))
              A).hom))
      A.pt =
    (ConcreteCategory.hom (f.app A.obj)) A.pt

Tactic:
dsimp [autIsoFibers]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ (ConcreteCategory.hom (F.map ((evaluationEquivOfIsGalois F A.obj A.pt).symm (↑((endEquivSectionsFibers F) f) A)).hom))
      A.pt =
    (ConcreteCategory.hom (f.app A.obj)) A.pt
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ Function.Injective S.hom.obj

Tactic:
rintro ⟨c, hc⟩ ⟨d, hd⟩ hcd
  simp only [Subtype.mk_eq_mk]; exact hcd

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ (∀ (c d : C), X c d ⊆ S.arrows c d) → generatedNormal X ≤ S

Tactic:
· rintro h
    apply @sInf_le (Subgroupoid C) _
    exact ⟨h, Sn⟩

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 ⋯
⊢ f ≫ g ∈ S.arrows c✝ c₄

Tactic:
exact S.mul hf hg

Goal state after:
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
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback b.inr 0 b.fst 0

Tactic:
by
  apply flip
  refine of_bot ?_ (by simp) (of_isBilimit h)
  simp

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : f ≈ g
⊢ projectMapAux f✝ f = projectMapAux f✝ g

Tactic:
induction h with
    | refl => rfl
    | symm _ _ _ hfg' => exact hfg'.symm
    | trans _ _ hfg hgh => exact hfg.trans hgh
    | comp _ _ hf hg => dsimp only [projectMapAux]; rw [hf, hg]
    | whiskerLeft _ _ _ _ hf => dsimp only [projectMapAux, projectObj]; rw [hf]
    | whiskerRight _ _ _ _ hf => dsimp only [projectMapAux, projectObj]; rw [hf]
    | tensor _ _ hfg hfg' => dsimp only [projectMapAux]; rw [hfg, hfg']
    | tensorHom_def _ _ =>
        dsimp only [projectMapAux, projectObj]; rw [MonoidalCategory.tensorHom_def]
    | comp_id => dsimp only [projectMapAux]; rw [Category.comp_id]
    | id_comp => dsimp only [projectMapAux]; rw [Category.id_comp]
    | assoc => dsimp only [projectMapAux]; rw [Category.assoc]
    | id_tensorHom_id => dsimp only [projectMapAux]; rw [MonoidalCategory.id_tensorHom_id]; rfl
    | tensorHom_comp_tensorHom =>
      dsimp only [projectMapAux]; rw [MonoidalCategory.tensorHom_comp_tensorHom]
    | whiskerLeft_id =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.whiskerLeft_id]
    | id_whiskerRight =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.id_whiskerRight]
    | α_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | α_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | associator_naturality =>
        dsimp only [projectMapAux]; rw [MonoidalCategory.associator_naturality]
    | ρ_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | ρ_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | ρ_naturality =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.rightUnitor_naturality]
    | l_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | l_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | l_naturality =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.leftUnitor_naturality]
    | pentagon =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.pentagon]
    | triangle =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.triangle]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝³ x✝² : Type u
x✝¹ : x✝³ ⟶ x✝²
x✝ : (__Functor✝ ⋙ __Functor✝).obj x✝³
⊢ (ConcreteCategory.hom ((__Functor✝ ⋙ __Functor✝).map x✝¹ ≫ ↾joinM)).toFun x✝ =
    (ConcreteCategory.hom (↾joinM ≫ __Functor✝.map x✝¹)).toFun x✝

Tactic:
exact joinM_map_map _ _

Goal state after:
Module: Mathlib.CategoryTheory.Monad.EquivMon

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : Mon (C ⥤ C)
X : C
⊢ η.app (M.X.obj X) ≫ μ.app X = 𝟙 ((𝟭 C).obj (M.X.obj X))

Tactic:
by
    simpa [-MonObj.mul_one] using! congrArg (fun t ↦ t.app X) (mul_one M.X)

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

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalRightAction C D
inst✝¹ : MonoidalRightAction C D'
inst✝ : F.LaxRightLinear C
d : D
c c' : C
⊢ μᵣ F d c ⊵ᵣ c' ≫ μᵣ F (d ⊙ᵣ c) c' ≫ F.map (αᵣ d c c').inv = (αᵣ (F.obj d) c c').inv ≫ μᵣ F d (c ⊗ c')

Tactic:
simpa [-μᵣ_associativity, -μᵣ_associativity_assoc] using
    (αᵣ _ _ _).inv ≫=
      (μᵣ_associativity F d c c').symm =≫
      F.map (αᵣ _ _ _).inv

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ Δ.hom ≫ ε.hom ▷ M.X.X = (λ_ M.X.X).inv

Tactic:
by
    rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.counit_comul]

Goal state after: