mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case pos
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
obtain ⟨Y, v, hni, hvmono, hvnoiso⟩ :=
      has_non_trivial_subobject_of_not_isConnected_of_not_initial X h nhi

Goal state after:
case pos
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case convert_2
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
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (selfProdProj u t))) b =
    (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) ((ConcreteCategory.hom (F.map (selfProdPermIncl h b))) a)

Tactic:
dsimp only [selfProdPermIncl, Pi.whiskerEquiv]

Goal state after:
case convert_2
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
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (selfProdProj u t))) b =
    (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t)))
      ((ConcreteCategory.hom (F.map (u ≫ Pi.map' ⇑(fiberPerm h b) fun j ↦ (Iso.refl X).hom))) a)
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
⊢ ContinuousSMul (Aut (F.obj X)) (F.obj X).obj

Tactic:
by
  constructor
  fun_prop

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

Goal state before:
pp: C : Type u_1
inst✝ : Groupoid C
⊢ Quiver.IsThin C ↔ ∀ (c : C), Subsingleton (c ⟶ c)

Tactic:
by
  refine ⟨fun h c => h c c, fun h c d => Subsingleton.intro fun f g => ?_⟩
  have := h d
  calc
    f = f ≫ inv g ≫ g := by simp only [inv_eq_inv, IsIso.inv_hom_id, Category.comp_id]
    _ = f ≫ inv f ≫ g := by congr 1
                            simp only [inv_eq_inv, IsIso.inv_hom_id, eq_iff_true_of_subsingleton]
    _ = g := by simp only [inv_eq_inv, IsIso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝⁵ : AddCommMonoid I
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝² : BraidedCategory C
inst✝¹ : X.HasTensor Y
inst✝ : Y.HasTensor X
k i j : I
hij : i + j = k
⊢ j + i = k

Tactic:
simpa only [add_comm j i] using hij

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
⊢ ∀ {c d e : C} {p : c ⟶ d},
    p ∈ {_f | c ∈ D ∧ d ∈ D} → ∀ {q : d ⟶ e}, q ∈ {_f | d ∈ D ∧ e ∈ D} → p ≫ q ∈ {_f | c ∈ D ∧ e ∈ D}

Tactic:
by rintro _ _ _ _ ⟨⟩ _ ⟨⟩; constructor <;> assumption

Goal state after:
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: case refine_1
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
⊢ Function.LeftInverse (fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) Pi.lift

Tactic:
intro f

Goal state after:
case refine_1
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 : md → (X ⟶ Y)
⊢ (fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) (Pi.lift f) = f
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
⊢ Function.RightInverse (fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) Pi.lift

Tactic:
intro f

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
⊢ Pi.lift ((fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) f) = f
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)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ (X ⟶ yp) → md

Tactic:
intro f

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)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
f : X ⟶ yp
⊢ md
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: case mp
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
x : (F.obj (op j)).obj j
x' : (F.obj (op j')).obj j'
⊢ coendRel F ⟨j, x⟩ ⟨j', x'⟩ → ∃ f y, (hom ((F.map f.op).app j)) y = x ∧ (hom ((F.obj (op j')).map f)) y = x'

pp: case mpr
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
x : (F.obj (op j)).obj j
x' : (F.obj (op j')).obj j'
⊢ (∃ f y, (hom ((F.map f.op).app j)) y = x ∧ (hom ((F.obj (op j')).map f)) y = x') → coendRel F ⟨j, x⟩ ⟨j', x'⟩

Tactic:
· rintro ⟨f, x⟩
    exact ⟨f, x, by simp⟩

Goal state after:
case mpr
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
x : (F.obj (op j)).obj j
x' : (F.obj (op j')).obj j'
⊢ (∃ f y, (hom ((F.map f.op).app j)) y = x ∧ (hom ((F.obj (op j')).map f)) y = x') → coendRel F ⟨j, x⟩ ⟨j', x'⟩
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case h.tensor
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X✝ Y✝ : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
W X Y Z : F C
f : W ⟶ᵐ Y
g : X ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
this : homMk f ⊗ₘ homMk g = homMk f ▷ X ≫ Y ◁ homMk g
⊢ motive (homMk f ▷ X ≫ Y ◁ homMk g)

Tactic:
exact comp _ _ (whiskerRight _ _ hf) (whiskerLeft _ _ hg)

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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro f

Goal state after:
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫
        (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫
          F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv)) ≫ F.map (Y₁ ◁ e₂.hom) ≫ F.map (e₁.hom ▷ L.obj X₂)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫
        (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫
          F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv)) ≫ F.map (Y₁ ◁ e₂.hom ≫ e₁.hom ▷ L.obj X₂)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫
        (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv)) ≫ F.map (e₁.hom ⊗ₘ e₂.hom)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫
        (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map ((δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv)) ≫ (e₁.hom ⊗ₘ e₂.hom))
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ curry (β_ I A).hom ≫ (ihom I).map (Hom.left u) ≫ (ihom I).map X.hom = toUnit A ≫ curryRightUnitorHom I

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ curry (β_ I A).hom ≫ (ihom I).map (Hom.left u ≫ X.hom) = toUnit A ≫ curryRightUnitorHom I
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ ∀ (a : F.obj A.A ⟶ B),
    F.map A.a ≫ a = adj.counit.app (F.obj A.A) ≫ a ↔
      G.map (F.map ((adj.homEquiv A.A B) a)) ≫ G.map (adj.counit.app B) = A.a ≫ (adj.homEquiv A.A B) a

Tactic:
intro f

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ F.map A.a ≫ f = adj.counit.app (F.obj A.A) ≫ f ↔
    G.map (F.map ((adj.homEquiv A.A B) f)) ≫ G.map (adj.counit.app B) = A.a ≫ (adj.homEquiv A.A B) f
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ G.map (F.map A.a) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))

Tactic:
by rw [← G.map_comp, coequalizer.condition, G.map_comp]

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
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
| (∀ (c : C) (d : D), IsIso ((pre (adj.unit.app d)).app (R.obj c))) ↔ ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))

Tactic:
lhs

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
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
| ∀ (c : C) (d : D), IsIso ((pre (adj.unit.app d)).app (R.obj c))
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ ((f ⊗ₘ f) ≫ μ) ⊵ₗ M ≫ γ = (f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ γ

Tactic:
tensorHom_def,

Goal state after:
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ ((f ▷ A ≫ B ◁ f) ≫ μ) ⊵ₗ M ≫ γ = (f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ γ
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
⊢ R ◁ σ ≫ μ = lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ ↔ ∀ ⦃X : C⦄ (a b c : X ⟶ R), a * (b + c) = a * b + a * c

Tactic:
refine ⟨fun h _ a b c ↦ ?_, fun h ↦ ?_⟩
  · have := lift a (lift b c) ≫= h
    simp only [lift_whiskerLeft_assoc] at this
    simp only [Hom.add_def, Hom.mul_def, this, ← Category.assoc]
    cat_disch
  · replace h := h (fst R (R ⊗ R)) (snd _ _ ≫ fst _ _) (snd _ _ ≫ snd _ _)
    simp only [Hom.mul_def, Hom.add_def] at h
    convert! h using 2
    · cat_disch
    · ext
      · simp only [lift_fst]
        congr 1
        cat_disch
      · simp only [lift_snd]
        congr 1
        cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid

Goal state before:
pp: D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (ihom.coev (F.obj Y)).app (G.obj X) ≫ (ihom (F.obj Y)).map (F.obj Y ◁ G.map f) =
    (ihom.coev (F.obj Y)).app (G.obj X) ≫
      (ihom (F.obj Y)).map (CategoryTheory.inv (F.map f) ▷ G.obj X) ≫ (ihom (F.obj Y)).map (F.map f ⊗ₘ G.map f)

Tactic:
← Functor.map_comp,

Goal state after:
D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (ihom.coev (F.obj Y)).app (G.obj X) ≫ (ihom (F.obj Y)).map (F.obj Y ◁ G.map f) =
    (ihom.coev (F.obj Y)).app (G.obj X) ≫
      (ihom (F.obj Y)).map (CategoryTheory.inv (F.map f) ▷ G.obj X ≫ (F.map f ⊗ₘ G.map f))
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
      (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))).inv ≫
        enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
            ((Enriched.FunctorCategory.homEquiv C) f₃ ≫ precompEnrichedHom C F₃ F₃' (Under.forget j)) ≫
          (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k ⊗ₘ
              end_.π (diagram C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) k) ≫
            eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
              ((Under.forget j ⋙ F₃').obj k)

Tactic:
tensorHom_def,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
      (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))).inv ≫
        enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
            ((Enriched.FunctorCategory.homEquiv C) f₃ ≫ precompEnrichedHom C F₃ F₃' (Under.forget j)) ≫
          (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k ▷
                end_ (diagram C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) ≫
              ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
                end_.π (diagram C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) k) ≫
            eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
              ((Under.forget j ⋙ F₃').obj k)