mathlib-initiative/mathlib-tactics huggingface dataset:
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
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
⊢ φ.map L ⋯ ≫ L.map φ.s = 0

Tactic:
MorphismProperty.LeftFraction.map_comp_map_s

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 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
⊢ L.map φ.f = 0
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
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = φ.map L ⋯ ≫ L.map φ.s
⊢ ∃ l, L.map (cokernel.π f) ≫ l = w

Tactic:
MorphismProperty.LeftFraction.map_comp_map_s

Goal state after:
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
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = L.map φ.f
⊢ ∃ l, L.map (cokernel.π f) ≫ l = w
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 = b

Tactic:
by intros; ext; exact one_smul _ _

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
W : Type u_2
inst✝² : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝¹ : Monoid G
inst✝ : F.Faithful
X✝ Y✝ : Action V G
a₁✝ a₂✝ : X✝ ⟶ Y✝
eq : (F.mapAction G).map a₁✝ = (F.mapAction G).map a₂✝
⊢ a₁✝.hom = a₂✝.hom

Tactic:
apply_fun (fun f ↦ f.hom) at eq

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
W : Type u_2
inst✝² : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝¹ : Monoid G
inst✝ : F.Faithful
X✝ Y✝ : Action V G
a₁✝ a₂✝ : X✝ ⟶ Y✝
eq : ((F.mapAction G).map a₁✝).hom = ((F.mapAction G).map a₂✝).hom
⊢ a₁✝.hom = a₂✝.hom
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: 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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (adj₁.unit.app (U.obj X) ≫ U.map (adj₁.counit.app X)) = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))

Tactic:
adj₁.right_triangle_components

Goal state after:
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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (𝟙 (U.obj X)) = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η → ∀ (c : C), Mono (η.app c)

pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Mono (η.app c)) → Mono η

Tactic:
· intro h c
    exact (inferInstance : Mono (((evaluation _ _).obj c).map η))

Goal state after:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Mono (η.app c)) → Mono η
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih : (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (f✝ ≫ g✝) = normalizeAux x✝ (f✝ ≫ h✝)

Tactic:
apply congr_fun ih

Goal state after:
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
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)

Tactic:
η.naturality_naturality

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      (η.naturality f ≫ η.app a ◁ G.map₂ β) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)
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
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ F.mapId a ▷ η.vCompApp θ a ≫ η.vCompNaturality θ (𝟙 a) =
    (λ_ (η.vCompApp θ a)).hom ≫ (ρ_ (η.vCompApp θ a)).inv ≫ η.vCompApp θ a ◁ H.mapId a

Tactic:
by
  calc
    _ = 𝟙 _ ⊗≫ (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
          η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 _ := by
      rw [η.naturality_id]
      bicategory
    _ = _ := by
      rw [θ.naturality_id]
      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)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ 𝟙 (u ≫ h) ⊗≫ u ◁ adj.unit ▷ h ⊗≫ (adj.counit ▷ (u ≫ h) ≫ 𝟙 b ◁ τ) ⊗≫ 𝟙 s.extension =
    𝟙 (u ≫ h) ⊗≫ u ◁ (adj.unit ▷ h ⊗≫ f ◁ τ) ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension

Tactic:
by
        rw [← whisker_exchange]; 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)
⊢ ((LeftLift.mk f adj.unit).whisker h).unit ≫ (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ▷ u =
    𝟙 (h ≫ 𝟙 a) ⊗≫ ((h ≫ 𝟙 a) ◁ adj.unit ≫ s.unit ▷ (f ≫ u)) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u)

Tactic:
by
        dsimp only [whisker_lift, StructuredArrow.mk_right, whisker_unit,
          StructuredArrow.mk_hom_eq_self]
        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)
τ₀ : (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 ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift

Tactic:
by
          rw [whisker_exchange]; bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)

Tactic:
by
          rw [whisker_exchange]; 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
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s : LeftExtension f (g ≫ h)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
Hσ : t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ
⊢ (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
    t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)

Tactic:
by
          rw [whisker_exchange]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := ⋯
i : J
hi : i ∈ l
⊢ ∀ ⦃x y : J⦄, Zag x y → Zigzag y j₂ → Zigzag x j₂

Tactic:
intro j k

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := fun x h ↦ { obj := x, property := ⋯ }
i : J
hi : i ∈ l
j k : J
⊢ Zag j k → Zigzag k j₂ → Zigzag j j₂
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u =
    𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)

Tactic:
by
        rw [← whisker_exchange]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case mp
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), ((a, b) ∈ (r ≫ inv r).rel) = ((a, b) ∈ (𝟙 X).rel)
⊢ ∃ f, graphFunctor.map f.hom = r

Tactic:
have h2 := congr_fun₂ congr((· ~[($h.inv_hom_id).rel] ·))

Goal state after:
case mp
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), ((a, b) ∈ (r ≫ inv r).rel) = ((a, b) ∈ (𝟙 X).rel)
h2 : ∀ (a b : Y), ((a, b) ∈ (inv r ≫ r).rel) = ((a, b) ∈ (𝟙 Y).rel)
⊢ ∃ f, graphFunctor.map f.hom = r
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₃ : C
⊢ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom =
    ((μ L W ε X₁ X₂).hom ⊗ₘ 𝟙 (L'.obj X₃)) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ (𝟙 (L'.obj X₁) ⊗ₘ (μ L W ε X₂ X₃).inv)

Tactic:
by
  dsimp +instances [monoidalCategoryStruct, associator]
  simp only [Functor.map_id, comp_id, NatTrans.id_app, id_comp]
  rw [Localization.associator_hom_app_app_app]
  rfl

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

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

Tactic:
← id_tensorHom,

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

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

Tactic:
← id_tensorHom,

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ Y₁ Y₂ Y₃).hom ▷ Y₄ ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom) =
    (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ▷ L'.obj X₄ ≫
          (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
            (𝟙 (L'.obj X₁) ⊗ₘ (α_ (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom)) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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

Tactic:
← comp_id e₁.hom,

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ ((α_ Y₁ Y₂ Y₃).hom ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom) =
    (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ⊗ₘ 𝟙 (L'.obj X₄)) ≫
        (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
          (e₁.hom ≫ 𝟙 Y₁ ⊗ₘ ((e₂.hom ⊗ₘ e₃.hom) ⊗ₘ e₄.hom) ≫ (α_ Y₂ Y₃ Y₄).hom)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case e_f
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' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (e₁.inv ⊗ₘ 𝟙 (𝟙_ (LocalizedMonoidal L W ε))) ≫
      L'.obj X' ◁ (ε' L W ε).inv ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom =
    (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom

Tactic:
← id_tensorHom,

Goal state after:
case e_f
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' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (e₁.inv ⊗ₘ 𝟙 (𝟙_ (LocalizedMonoidal L W ε))) ≫
      (𝟙 (L'.obj X') ⊗ₘ (ε' L W ε).inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom =
    (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : 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' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ (homCartesianLift f g φ' ≫ cartesianLift a f).fiber = φ'.fiber ≫ eqToHom ⋯

Tactic:
simp [← Cat.Hom₂.comp_app]

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

Goal state before:
pp: case refine_2.hfg₁
𝒮 : 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)
⊢ χ'.base = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).base

Tactic:
simp [← Cat.Hom₂.comp_app]

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

Goal state before:
pp: case hfg₂
𝒮 : 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)
⊢ χ'.fiber = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).fiber ≫ eqToHom ⋯

Tactic:
simp [← Cat.Hom₂.comp_app]

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

Goal state before:
pp: case refine_1
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 : S.ShortExact
i : I
this✝ : Mono S.f
this : Epi S.g
⊢ (S.map (F i)).ShortExact

Tactic:
exact hS.map (F i)

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 A : C
inst✝ : IsConnected A
h : Nonempty (F.obj X).obj
f : X ⟶ A
Z : C
u v : A ⟶ Z
huv : f ≫ u = f ≫ v
⊢ u = v

Tactic:
apply evaluation_injective_of_isConnected F A Z (F.map f (Classical.arbitrary _))

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X A : C
inst✝ : IsConnected A
h : Nonempty (F.obj X).obj
f : X ⟶ A
Z : C
u v : A ⟶ Z
huv : f ≫ u = f ≫ v
⊢ (fun f_1 ↦
        (ConcreteCategory.hom (F.map f_1))
          ((ConcreteCategory.hom (F.map f)) (Classical.arbitrary ((fun X ↦ X.obj) (F.obj X)))))
      u =
    (fun f_1 ↦
        (ConcreteCategory.hom (F.map f_1))
          ((ConcreteCategory.hom (F.map f)) (Classical.arbitrary ((fun X ↦ X.obj) (F.obj X)))))
      v
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 A : C
inst✝¹ : Nonempty (F.obj X).obj
inst✝ : IsConnected A
f : X ⟶ A
⊢ Function.Surjective ⇑(ConcreteCategory.hom (F.map f))

Tactic:
have : Epi f := epi_of_nonempty_of_isConnected F f

Goal state after:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
X A : C
inst✝¹ : Nonempty (F.obj X).obj
inst✝ : IsConnected A
f : X ⟶ A
this : Epi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (F.map f))