mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a'✝ ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
⊢ ∀ (y : a'✝ ⟶ a), (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ ≫ ψ

Tactic:
intro π

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a'✝ ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a'✝ ⟶ a
⊢ (fun χ ↦ p.IsHomLift 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 φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
use τ' ≫ Φ.hom

Goal state after:
case h
𝒮 : 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' := ⋯
Φ : a' ≅ a := ⋯
⊢ (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ' ≫ Φ.hom) ∧
    ∀ (y : c ⟶ a), (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: case h.refine_2
𝒮 : 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 φ) φ ψ
⊢ ∀ (y : c ⟶ a), (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom

Tactic:
intro π

Goal state after:
case h.refine_2
𝒮 : 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 φ) φ ψ
π : c ⟶ a
⊢ (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') π → π = τ' ≫ Φ.hom
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.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst✝ : p.IsHomLift (𝟙 S) φ'.hom
⊢ ∀ {b'_1 : 𝒳} (φ'_1 : a ⟶ b'_1) [p.IsHomLift f φ'_1], ∃! χ, p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = φ'_1

Tactic:
by
    intro c ψ hψ
    use φ'.inv ≫ IsCocartesian.map p f φ ψ
    refine ⟨⟨inferInstance, by simp⟩, ?_⟩
    rintro τ ⟨hτ₁, hτ₂⟩
    rw [Iso.eq_inv_comp]
    apply map_uniq
    exact ((assoc φ _ _) ▸ hτ₂)

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
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ IsIso (v.inv ≫ i ≫ (functorToAction F).map prod.fst)

Tactic:
have : IsIso (i ≫ (functorToAction F).map prod.fst) := by
        suffices h : IsIso (𝟙 ((functorToAction F).obj X)) by simpa [i, u]
        infer_instance

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 i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this : IsIso (i ≫ (functorToAction F).map prod.fst)
⊢ IsIso (v.inv ≫ i ≫ (functorToAction F).map prod.fst)
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
⊢ ∀ (i j : (PointedGaloisObject F)ᵒᵖ)
    (xi : (fun X ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj i))
    (xj : (fun X ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj j)),
    (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app i)) xi =
        (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map f)) xi =
          (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map g)) xj

Tactic:
intro ⟨A, a, _⟩ ⟨B, b, _⟩ (u : (A : C) ⟶ X) (v : (B : C) ⟶ X) (h : F.map u a = F.map v b)
    obtain ⟨⟨Z, z, _⟩, ⟨f, hf⟩, ⟨g, hg⟩, _⟩ :=
      IsFilteredOrEmpty.cocone_objs (C := (PointedGaloisObject F)ᵒᵖ)
        ⟨{ obj := A, pt := a}⟩ ⟨{obj := B, pt := b}⟩
    refine ⟨⟨{ obj := Z, pt := z }⟩, ⟨f, hf⟩, ⟨g, hg⟩, ?_⟩
    apply evaluation_injective_of_isConnected F Z X z
    change F.map (f ≫ u) z = F.map (g ≫ v) z
    rw [map_comp, FintypeCat.comp_apply, hf, map_comp, FintypeCat.comp_apply, hg, h]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul (Aut F) X.V.obj
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)

Tactic:
obtain ⟨ι, hfin, f, ⟨u⟩⟩ := has_decomp_quotients X

Goal state after:
C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul (Aut F) X.V.obj
ι : Type
hfin : Finite ι
f : ι → OpenSubgroup (Aut F)
u : (∐ fun i ↦ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i)))) ≅ X
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
f : d ⟶ d
hf : ∃ a b g, ∃ (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

Tactic:
obtain ⟨c, d, g, ec, ed, eg, gS, eg⟩ := hf

Goal state after:
case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d✝ : D
c d : C
g : c ⟶ d
ec : φ.obj c = d✝
ed : φ.obj d = d✝
eg : g ∈ S.arrows c d
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d✝
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
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows (φ.obj c') (φ.obj c')

Tactic:
have : g ∈ (im φ hφ).arrows (φ.obj c) (φ.obj c') := by rw [hφ']; trivial

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
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
this : g ∈ (im φ hφ).arrows (φ.obj c) (φ.obj c')
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows (φ.obj c') (φ.obj c')
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasCoproducts A
J : Type w
f : J → FormalCoproduct C
F : C ⥤ A
s : Cocone (Discrete.functor f ⋙ (eval C A).obj F)
m : (((eval C A).obj F).mapCocone (cofan J f)).pt ⟶ s.pt
h : ∀ (j : Discrete J), (((eval C A).obj F).mapCocone (cofan J f)).ι.app j ≫ m = s.ι.app j
x✝ : (cofan J f).pt.I
i₁ : J
i₂ : (f i₁).I
⊢ Sigma.ι (fun i ↦ F.obj ((cofan J f).pt.obj i)) ⟨i₁, i₂⟩ ≫ m =
    Sigma.ι (fun i ↦ F.obj ((cofan J f).pt.obj i)) ⟨i₁, i₂⟩ ≫
      Sigma.desc fun i ↦ Sigma.ι (F.obj ∘ (f i.fst).obj) i.snd ≫ s.ι.app { as := i.fst }

Tactic:
simp [← h, cofan, Function.comp_def]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₂ ≫ h₁₂.p₂ ≫ f₂ = h.p

Tactic:
p₁₂_p₂_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂ ≫ f₂ = h.p
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
⊢ False

Tactic:
let md := Σ Z W : C, Z ⟶ W

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
⊢ False
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
f : X ⟶ yp
⊢ Pi.lift ((fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) f) = f

Tactic:
ext ⟨j⟩

Goal state after:
case refine_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
f : X ⟶ yp
j : C
snd✝ : (W : C) × (j ⟶ W)
⊢ Pi.lift ((fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) f) ≫ Pi.π (fun a ↦ Y) ⟨j, snd✝⟩ = f ≫ Pi.π (fun a ↦ Y) ⟨j, snd✝⟩
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
m : (cowedge F).pt ⟶ s.pt
h : ∀ (j : WalkingMultispan (multispanShapeCoend J)), (cowedge F).ι.app j ≫ m = s.ι.app j
⊢ m = ↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯

Tactic:
ext ⟨j⟩

Goal state after:
case mk
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
m : (cowedge F).pt ⟶ s.pt
h : ∀ (j : WalkingMultispan (multispanShapeCoend J)), (cowedge F).ι.app j ≫ m = s.ι.app j
x✝ : (cowedge F).pt
j : (j : J) × (F.obj (op j)).obj j
⊢ (hom m).toFun (Quot.mk (coendRel F) j) =
    (hom (↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯)).toFun (Quot.mk (coendRel F) j)
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: case refine_2
J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j✝ j'✝ : J
g : j✝ ⟶ j'✝
y : (F.obj (op j'✝)).obj j✝
⊢ (hom ((G.obj (op j'✝)).map g)) ((hom ((f.app (op j'✝)).app j✝)) y) =
    (hom ((f.app (op j'✝)).app j'✝)) ((Hom.hom ((F.obj (op j'✝)).map g)) y)

Tactic:
simp [← NatTrans.naturality_apply]

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

Goal state before:
pp: C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f : X ⟶ Y),
    Quot.map (fun f ↦ f.whiskerRight unit) ⋯ f ≫
        { hom := ⟦Hom.ρ_hom Y⟧, inv := ⟦Hom.ρ_inv Y⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
      { hom := ⟦Hom.ρ_hom X⟧, inv := ⟦Hom.ρ_inv X⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ f

Tactic:
rintro ⟨f⟩
    exact Quotient.sound (ρ_naturality _)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ : C
⊢ (mopEquiv (D ⥤ D)).inverse.map
      (Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ c₂ x).inv, naturality := ⋯ } ▷ (curriedActionMop C D).obj c₃ ≫
        Quiver.Hom.mop { app := fun x ↦ (αₗ (c₁ ⊗ c₂) c₃ x).inv, naturality := ⋯ } ≫
          (curriedActionMop C D).map (α_ c₁ c₂ c₃).hom) =
    (mopEquiv (D ⥤ D)).inverse.map
      ((α_ ((curriedActionMop C D).obj c₁) ((curriedActionMop C D).obj c₂) ((curriedActionMop C D).obj c₃)).hom ≫
        (curriedActionMop C D).obj c₁ ◁ Quiver.Hom.mop { app := fun x ↦ (αₗ c₂ c₃ x).inv, naturality := ⋯ } ≫
          Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ (c₂ ⊗ c₃) x).inv, naturality := ⋯ })

Tactic:
ext d

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ : C
d : D
⊢ ((mopEquiv (D ⥤ D)).inverse.map
          (Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ c₂ x).inv, naturality := ⋯ } ▷ (curriedActionMop C D).obj c₃ ≫
            Quiver.Hom.mop { app := fun x ↦ (αₗ (c₁ ⊗ c₂) c₃ x).inv, naturality := ⋯ } ≫
              (curriedActionMop C D).map (α_ c₁ c₂ c₃).hom)).app
      d =
    ((mopEquiv (D ⥤ D)).inverse.map
          ((α_ ((curriedActionMop C D).obj c₁) ((curriedActionMop C D).obj c₂) ((curriedActionMop C D).obj c₃)).hom ≫
            (curriedActionMop C D).obj c₁ ◁ Quiver.Hom.mop { app := fun x ↦ (αₗ c₂ c₃ x).inv, naturality := ⋯ } ≫
              Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ (c₂ ⊗ c₃) x).inv, naturality := ⋯ })).app
      d
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
w : C
x y z : D
f : x ⟶ y
g : y ⟶ z
⊢ w ⊴ₗ (f ≫ g) = w ⊴ₗ f ≫ w ⊴ₗ g

Tactic:
by
  simp [← id_actionHom, ← actionHom_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
w : D
x y z : C
f : x ⟶ y
g : y ⟶ z
⊢ w ⊴ᵣ (f ≫ g) = w ⊴ᵣ f ≫ w ⊴ᵣ g

Tactic:
by
  simp [← id_actionHom, ← actionHom_comp]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
c₁ c₂ c₃ : C
⊢ { app := fun x ↦ (αᵣ x c₁ c₂).inv, naturality := ⋯ } ▷ (curriedAction C D).obj c₃ ≫
      { app := fun x ↦ (αᵣ x (c₁ ⊗ c₂) c₃).inv, naturality := ⋯ } ≫ (curriedAction C D).map (α_ c₁ c₂ c₃).hom =
    (α_ ((curriedAction C D).obj c₁) ((curriedAction C D).obj c₂) ((curriedAction C D).obj c₃)).hom ≫
      (curriedAction C D).obj c₁ ◁ { app := fun x ↦ (αᵣ x c₂ c₃).inv, naturality := ⋯ } ≫
        { app := fun x ↦ (αᵣ x c₁ (c₂ ⊗ c₃)).inv, naturality := ⋯ }

Tactic:
ext d

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
c₁ c₂ c₃ : C
d : D
⊢ ({ app := fun x ↦ (αᵣ x c₁ c₂).inv, naturality := ⋯ } ▷ (curriedAction C D).obj c₃ ≫
          { app := fun x ↦ (αᵣ x (c₁ ⊗ c₂) c₃).inv, naturality := ⋯ } ≫ (curriedAction C D).map (α_ c₁ c₂ c₃).hom).app
      d =
    ((α_ ((curriedAction C D).obj c₁) ((curriedAction C D).obj c₂) ((curriedAction C D).obj c₃)).hom ≫
          (curriedAction C D).obj c₁ ◁ { app := fun x ↦ (αᵣ x c₂ c₃).inv, naturality := ⋯ } ≫
            { app := fun x ↦ (αᵣ x c₁ (c₂ ⊗ c₃)).inv, naturality := ⋯ }).app
      d
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
c✝ c'✝ : C
d✝ d'✝ : D
f : c✝ ⟶ c'✝
g : d✝ ⟶ d'✝
⊢ (f.op ⊙ₗₘ g.op).unop = (f.op ⊵ₗ op d✝).unop ≫ (op c'✝ ⊴ₗ g.op).unop

Tactic:
by
    apply Quiver.Hom.op_inj
    simpa [MonoidalLeftAction.action_exchange] using
      MonoidalLeftAction.actionHom_def f.op g.op

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
c✝ c'✝ : C
d✝ d'✝ : D
f : d✝ ⟶ d'✝
g : c✝ ⟶ c'✝
⊢ (f.op ⊙ᵣₘ g.op).unop.op = ((f.op ⊵ᵣ op c✝).unop ≫ (op d'✝ ⊴ᵣ g.op).unop).op

Tactic:
simpa [MonoidalRightAction.action_exchange] using
      MonoidalRightAction.actionHom_def f.op g.op

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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
inst✝⁵ : MonoidalCategory D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetractionAux adj c d = (ihom.ev d).app (R.obj c)

Tactic:
simp only [id_obj, adjRetractionAux, Functor.map_inv, Functor.comp_map,
    braiding_naturality_right_assoc]

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
inst✝⁵ : MonoidalCategory D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      adj.unit.app ((ihom d).obj (R.obj c)) ▷ d ≫
        (L ⋙ R).obj ((ihom d).obj (R.obj c)) ◁ adj.unit.app d ≫
          adj.unit.app ((L ⋙ R).obj ((ihom d).obj (R.obj c)) ⊗ (L ⋙ R).obj d) ≫
            inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))) ≫
              R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom) ≫
                R.map (L.map ((ihom.ev d).app (R.obj c))) ≫ inv (adj.unit.app (R.1 c)) =
    (ihom.ev d).app (R.obj c)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (limitCone F c hc).pt
w : ∀ (j : J), m ≫ (limitCone F c hc).π.app j = s.π.app j
j : J
⊢ m.hom ≫ c.π.app j = { hom := hc.lift ((forget C).mapCone s), isMonHom_hom := ⋯ }.hom ≫ c.π.app j

Tactic:
simpa using congr($(w j).hom)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (expComparison F A).natTrans
⊢ IsIso (frobeniusMorphism F h A).natTrans

Tactic:
rw [← frobeniusMorphism_mate F h] at i
  exact @conjugateEquiv_of_iso _ _ _ _ _ _ _ _ _ _ _ i

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

Goal state before:
pp: C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ normalizeIsoApp C (X.tensor Y) n = normalizeIsoApp' C (X.tensor Y) n.as

Tactic:
normalizeIsoApp,

Goal state after:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusion.obj { as := n.as }) X Y).symm ≪≫
      normalizeIsoApp C X n ▷ᵢ Y ≪≫ normalizeIsoApp C Y { as := X.normalizeObj n.as } =
    normalizeIsoApp' C (X.tensor Y) n.as
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁵ : Category.{v₂, u₂} V
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory V
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
x : C
⊢ (λ_ (F.obj x)).inv ≫
      ((ConcreteCategory.hom
                (𝟙
                  (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                    prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 C) ⋙ tensor C ⋙ U ⊛ F)))
              ((prod.leftInverseUnitor C).whiskerLeft
                (((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ U ⊛ F))
                  (((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) (U ⊛ F)) (𝟙 (U ⊛ F)))))).app
          x ≫
        (U ⊛ F).map (λ_ x).hom =
    (λ_ (F.obj x)).inv ≫ can ▷ F.obj x ≫ (DayConvolution.unit U F).app (𝟙_ C, x) ≫ (U ⊛ F).map (λ_ x).hom

Tactic:
id_apply

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁵ : Category.{v₂, u₂} V
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory V
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
x : C
⊢ (λ_ (F.obj x)).inv ≫
      ((prod.leftInverseUnitor C).whiskerLeft
              (((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ U ⊛ F))
                (((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) (U ⊛ F)) (𝟙 (U ⊛ F))))).app
          x ≫
        (U ⊛ F).map (λ_ x).hom =
    (λ_ (F.obj x)).inv ≫ can ▷ F.obj x ≫ (DayConvolution.unit U F).app (𝟙_ C, x) ≫ (U ⊛ F).map (λ_ x).hom