mathlib-initiative/mathlib-tactics huggingface dataset:
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
Y' : C
g : Y ⟶ Y'
⊢ (R.extMk f m hm hf).comp (Ext.mk₀ g) ⋯ = R.extMk (f ≫ g) m hm ⋯

Tactic:
by
  have := HasDerivedCategory.standard C
  ext
  simp only [extMk, Ext.comp_hom, Int.cast_ofNat_Int, Ext.mk₀_hom,
    extEquivCohomologyClass_symm_mk_hom]
  simp only [← Category.assoc]
  rw [Cocycle.toSingleMk_postcomp _ _ _ _
      (by simpa [cochainComplex_d _ _ _ m n rfl rfl]) g,
    Cocycle.equivHomShift_symm_postcomp,
    ← ShiftedHom.comp_mk₀ _ 0 rfl,
    ShiftedHom.map_comp, ShiftedHom.map_mk₀,
    ShiftedHom.comp_assoc _ _ _ (add_zero _) (zero_add _) (by simp),
    ShiftedHom.comp_assoc _ _ _ (zero_add _) (zero_add _) (by simp),
    ShiftedHom.comp_assoc _ _ _ (zero_add _) (zero_add _) (by simp),
    ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀, ← NatTrans.naturality]
  dsimp

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.EssSurj
⊢ [Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0].TFAE

Tactic:
tfae_have 1 → 2 := fun _ ↦ by
    have hf : L.map (kernel.ι f) = 0 := by
      rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]
    simpa [hf] using! map_comp_eq_zero_iff_of_epi_mono L P (𝟙 _) (kernel.ι f)

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
⊢ [Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0].TFAE
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
x✝ : SingleObj M
⊢ (↾fun x ↦ 𝟙 x✝ • x) = 𝟙 X

Tactic:
by ext; exact MulAction.one_smul _

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))
f :
  s.pt ⟶
    { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt
h : ∀ (j : Discrete ι), f ≫ { hom := ↾fun x ↦ x j.as, comm := ⋯ } = s.π.app j
x : s.pt.V
j : ι
⊢ (ConcreteCategory.hom f.hom) x j = (ConcreteCategory.hom (s.π.app { as := j }).hom) x

Tactic:
rw [← h ⟨j⟩]

Goal state after:
ι : 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))
f :
  s.pt ⟶
    { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt
h : ∀ (j : Discrete ι), f ≫ { hom := ↾fun x ↦ x j.as, comm := ⋯ } = s.π.app j
x : s.pt.V
j : ι
⊢ (ConcreteCategory.hom f.hom) x j = (ConcreteCategory.hom (f ≫ { hom := ↾fun x ↦ x { as := j }.as, comm := ⋯ }).hom) x
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
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
a b : N ⋊[φ] G
this : ∀ (n : G) (g : N), fn ((φ n) g) = fg n * fn g * (fg n)⁻¹
⊢ fn (a * b).left * fg (a * b).right = fn a.left * fg a.right * (fn b.left * fg b.right)

Tactic:
simp only [mul_left, mul_right, map_mul, this, mul_assoc, inv_mul_cancel_left]

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 ⥤ SingleObj G ⥤ V
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ PreservesColimit K F

Tactic:
by
  apply preservesColimit_of_evaluation
  intro _
  exact h

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
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
b✝ : X ⟶ Y
⊢ (1 • b✝).hom = b✝.hom

Tactic:
exact one_smul _ _

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.Monoidal
x✝¹ x✝ : Action V G
⊢ δ F x✝¹.V x✝.V ≫ μ F x✝¹.V x✝.V = 𝟙 (F.obj (x✝¹.V ⊗ x✝.V))

Tactic:
δ_μ

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.Monoidal
x✝¹ x✝ : Action V G
⊢ 𝟙 (F.obj (x✝¹.V ⊗ x✝.V)) = 𝟙 (F.obj (x✝¹.V ⊗ x✝.V))
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapId a ≫ θ.naturality (𝟙 a)) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)

Tactic:
rw [naturality_id]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ ((ρ_ (θ.app a)).hom ≫ (λ_ (θ.app a)).inv ≫ G.mapId a ▷ θ.app a) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a

Tactic:
rw [naturality_id]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      ((ρ_ (η.app a)).hom ≫ (λ_ (η.app a)).inv ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case mk.mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).toFunctor.obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).toFunctor.obj b.fiber
hfg₁ : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }

Tactic:
dsimp at hfg₁

Goal state after:
case mk.mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).toFunctor.obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).toFunctor.obj b.fiber
hfg₁ : base✝¹ = base✝
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv

Tactic:
eqToHom_trans,

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f

Tactic:
eqToHom_trans,

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
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
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)

Tactic:
have h₁ := (((associator L W ε).hom.app Y₁).app Y₂).naturality f₃
  have h₂ := NatTrans.congr_app (((associator L W ε).hom.app Y₁).naturality f₂) X₃
  have h₃ := NatTrans.congr_app (NatTrans.congr_app ((associator L W ε).hom.naturality f₁) X₂) X₃
  simp +instances only [monoidalCategoryStruct, Functor.map_comp, assoc]
  dsimp at h₁ h₂ h₃ ⊢
  rw [h₁, assoc, reassoc_of% h₂, reassoc_of% h₃]

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 c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 T) ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
obtain rfl : S = T := by rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 S) ψ
⊢ p.IsHomLift f (φ ≫ ψ)
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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ ((homEquiv V) (f ≫ g) ≫ precompEnrichedHom V F₁ F₃ (Under.forget j)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k =
    ((λ_ (𝟙_ V)).inv ≫
        ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗ₘ
            (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
          enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k

Tactic:
homEquiv_comp,

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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ (((λ_ (𝟙_ V)).inv ≫ ((homEquiv V) f ⊗ₘ (homEquiv V) g) ≫ enrichedComp V F₁ F₂ F₃) ≫
        precompEnrichedHom V F₁ F₃ (Under.forget j)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k =
    ((λ_ (𝟙_ V)).inv ≫
        ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗ₘ
            (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
          enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k
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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ (functorHomEquiv V) (f ≫ g) =
    (λ_ (𝟙_ (J ⥤ V))).inv ≫ ((functorHomEquiv V) f ⊗ₘ (functorHomEquiv V) g) ≫ functorEnrichedComp V F₁ F₂ F₃

Tactic:
ext j
  dsimp
  ext k
  rw [homEquiv_comp, assoc, assoc, assoc, assoc, assoc, end_.lift_π, enrichedComp_π]
  simp [tensorHom_comp_tensorHom_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
G : D ⥤ H
β : L ⋙ G ⟶ F
⊢ G.IsLeftDerivedFunctor β W ↔ IsIso (LF.leftDerivedLift α W G β)

Tactic:
isLeftDerivedFunctor_iff_isRightKanExtension

Goal state after:
C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
G : D ⥤ H
β : L ⋙ G ⟶ F
⊢ G.IsRightKanExtension β ↔ IsIso (LF.leftDerivedLift α W G β)
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✝⁵ : HasZeroMorphisms C
inst✝⁴ : (i : I) → HasZeroMorphisms (D i)
inst✝³ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), (F i).PreservesHomology
inst✝ : HasZeroObject C
S : ShortComplex C
⊢ S.Exact ↔ ∀ (i : I), (S.map (F i)).Exact

Tactic:
by
  refine ⟨fun hS i ↦ hS.map _, fun hS ↦ ?_⟩
  simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢
  rw [hP.isZero_iff]
  exact fun i ↦ (hS i).of_iso (S.mapHomologyIso (F i)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) ≫ L₂.map (adj.counit.app (G.obj X₁)) = α.app X₁

Tactic:
reassoc_of% eq₃,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁)) ≫ L₂.map (adj.counit.app (G.obj X₁)) = α.app X₁
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
⊢ ∀ (X : D₁), G'.map (η.app X) ≫ ε.app (G'.obj X) = 𝟙 (G'.obj X)

Tactic:
suffices G'.leftUnitor.inv ≫ whiskerRight η G' ≫ (Functor.associator _ _ _).hom ≫
        whiskerLeft G' ε ≫ G'.rightUnitor.hom = 𝟙 _ from
      fun Y₁ ↦ by simpa using congr_app this Y₁
    apply G'.leftDerived_ext α W₁
    ext X₁
    have eq₁ := ε.naturality (α.app X₁)
    have eq₂ := G'.congr_map (hη X₁)
    have eq₃ := α.naturality (adj.unit.app X₁)
    dsimp at eq₁ eq₂ eq₃ ⊢
    simp only [Functor.map_comp] at eq₂
    rw [Category.assoc, Category.assoc, Category.assoc, Category.comp_id,
      Category.id_comp, Category.id_comp, Category.id_comp, ← eq₁, reassoc_of% eq₂,
      hε (G.obj X₁), reassoc_of% eq₃, ← L₂.map_comp, adj.left_triangle_components,
      Functor.map_id, Category.comp_id]

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

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

Tactic:
refine Nonempty.elim ?_ h

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : ∀ (a : IsInitial X), False
hzero : Nat.card (F.obj X).obj = 0
⊢ Nonempty (IsInitial X)
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
A : C
inst✝ : IsConnected A
⊢ Finite (Aut A)

Tactic:
let F := GaloisCategory.getFiberFunctor C
  obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
  apply Finite.of_injective (fun f ↦ F.map f.hom a)
  exact evaluation_aut_injective_of_isConnected F A a

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

Goal state before:
pp: case h.right
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a

Tactic:
· refine ⟨evaluation_injective_of_isConnected F A X a, ?_⟩
    intro x
    use u ≫ Pi.π _ x
    exact (selfProdProj_fiber h1) x

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X✝ : C
inst✝ : IsConnected X✝
x y : (F.obj X✝).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X✝).obj := (e X✝).symm x
hx' : x' = (e X✝).symm x
y' : (F'.obj X✝).obj := (e X✝).symm y
hy' : y' = (e X✝).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X✝)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (gapp Y).hom = (gapp X).hom ≫ F.map f

Tactic:
by
      ext x
      dsimp [gapp, e]
      erw [FintypeCat.uSwitchEquiv_naturality (F.map f)]
      rw [← Functor.comp_map]
      erw [← NatTrans.naturality_apply, FintypeCat.uSwitchEquiv_symm_naturality (F.map f)]
      rfl

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

Goal state before:
pp: C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
⊢ f = g

Tactic:
have := h d

Goal state after:
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f = g