mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
⊢ IsColimit t

Tactic:
by
  let α : t.pt → J := fun x => (hsurj x).choose
  let f : ∀ (x : t.pt), F.obj (α x) := fun x => (hsurj x).choose_spec.choose
  have hf : ∀ (x : t.pt), x = t.ι.app _ (f x) := fun x => (hsurj x).choose_spec.choose_spec
  exact
    { desc s := ↾fun x => s.ι.app _ (f x)
      fac := fun s j => by
        ext y
        obtain ⟨k, l, g, eq⟩ := hinj _ _ _ _ (hf (t.ι.app j y))
        have h := congr_hom (s.ι.naturality g) (f (t.ι.app j y))
        have h' := congr_hom (s.ι.naturality l) y
        simp only [Functor.const_obj_obj, comp_apply, Functor.const_obj_map, Category.comp_id,
          TypeCat.Fun.toFun_apply, hom_ofHom, TypeCat.Fun.coe_mk] at h h' ⊢
        rw [← h, ← eq, h']
      uniq := fun s m hm => by
        ext x
        dsimp
        nth_rw 1 [hf x]
        simp [← hm, comp_apply] }

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Finite ι
f g : MultilinearMap R (fun x ↦ R) M₂
h : (f fun x ↦ 1) = g fun x ↦ 1
x : ι → R
val✝ : Fintype ι
⊢ f x = g x

Tactic:
have hf := f.map_smul_univ x (fun _ ↦ 1)

Goal state after:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Finite ι
f g : MultilinearMap R (fun x ↦ R) M₂
h : (f fun x ↦ 1) = g fun x ↦ 1
x : ι → R
val✝ : Fintype ι
hf : (f fun i ↦ x i • 1) = (∏ i, x i) • f fun x ↦ 1
⊢ f x = g x
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x) +
      ∑ x_1 ∈ Finset.univ.powerset with #x_1 ≤ 1, f (x_1.piecewise h x) =
    f x + (f.linearDeriv x) h + ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x)

Tactic:
le_iff_lt_or_eq (b := 1),

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x) +
      ∑ x_1 ∈ Finset.univ.powerset with #x_1 < 1 ∨ #x_1 = 1, f (x_1.piecewise h x) =
    f x + (f.linearDeriv x) h + ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case refine_1
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁷ : Ring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M'
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x✝¹ : M₂
x✝ : x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
x : (i : ι) → M₁ i
hx : x ∈ {v | ∀ (i : ι), v i ∈ p i}
hf : f x = x✝¹
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : j = i
⊢ c • x i ∈ p i

Tactic:
exact (p i).smul_mem _ (hx i)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift

Goal state before:
pp: J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ Type u
c : Cone K
hc : IsLimit c
⊢ ∀ s ∈ (K ⋙ uliftFunctor.{v, u}).sections,
    ∃! x, ∀ (j : J), (ConcreteCategory.hom ((uliftFunctor.{v, u}.mapCone c).π.app j)) x = s j

Tactic:
intro s hs

Goal state after:
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ Type u
c : Cone K
hc : IsLimit c
s : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j
hs : s ∈ (K ⋙ uliftFunctor.{v, u}).sections
⊢ ∃! x, ∀ (j : J), (ConcreteCategory.hom ((uliftFunctor.{v, u}.mapCone c).π.app j)) x = s j
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j = F.map ((liftLimit t).π.app j)

Tactic:
rw [← liftedLimitMapsToOriginal_inv_map_π (t := t)]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ (liftedLimitMapsToOriginal t).hom.hom ≫ (liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((liftLimit t).π.app j) =
    F.map ((liftLimit t).π.app j)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ Cᵒᵖ
X : C
c : Cone F
hc : IsLimit c
⊢ ∀ s ∈ (F ⋙ yoneda.obj X).sections, ∃! x, ∀ (j : J), (hom (((yoneda.obj X).mapCone c).π.app j)) x = s j

Tactic:
intro s hs

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ Cᵒᵖ
X : C
c : Cone F
hc : IsLimit c
s : (j : J) → (F ⋙ yoneda.obj X).obj j
hs : s ∈ (F ⋙ yoneda.obj X).sections
⊢ ∃! x, ∀ (j : J), (hom (((yoneda.obj X).mapCone c).π.app j)) x = s j
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
X : Cᵒᵖ
c : Cone F
hc : IsLimit c
⊢ ∀ s ∈ (F ⋙ coyoneda.obj X).sections, ∃! x, ∀ (j : J), (hom (((coyoneda.obj X).mapCone c).π.app j)) x = s j

Tactic:
intro s hs

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
X : Cᵒᵖ
c : Cone F
hc : IsLimit c
s : (j : J) → (F ⋙ coyoneda.obj X).obj j
hs : s ∈ (F ⋙ coyoneda.obj X).sections
⊢ ∃! x, ∀ (j : J), (hom (((coyoneda.obj X).mapCone c).π.app j)) x = s j
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ (Hom.hom (s.ι.app j)) ((f i j h) x) = (Hom.hom (s.ι.app i)) x

Tactic:
simp only [Functor.const_obj_obj]

Goal state after:
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ (Hom.hom (s.ι.app j)) ((f i j h) x) = (Hom.hom (s.ι.app i)) x
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
this :
  ((L.associator R L).inv ≫ whiskerRight (inv h.unit) L) ≫
      whiskerRight h.unit L ≫ (L.associator R L).hom ≫ L.whiskerLeft h.counit =
    ((L.associator R L).inv ≫ whiskerRight (inv h.unit) L) ≫ L.leftUnitor.hom ≫ L.rightUnitor.inv
⊢ IsIso (L.whiskerLeft h.counit)

Tactic:
simp only [assoc, ← whiskerRight_comp_assoc, IsIso.inv_hom_id, whiskerRight_id', id_comp,
    Iso.inv_hom_id_assoc] at this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
this :
  L.whiskerLeft h.counit = (L.associator R L).inv ≫ whiskerRight (inv h.unit) L ≫ L.leftUnitor.hom ≫ L.rightUnitor.inv
⊢ IsIso (L.whiskerLeft h.counit)
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
⊢ IsLimit (limitCone F)

Tactic:
by
  refine IsLimit.ofFaithful (forget SemiRingCat.{u}) (Types.Small.limitConeIsLimit.{v, u} _)
    (fun s => ofHom { toFun := _, map_one' := ?_, map_mul' := ?_, map_zero' := ?_, map_add' := ?_ })
    (fun s => rfl)
  · simp
    rfl
  · intro x y
    simp [← equivShrink_mul]
    rfl
  · simp
    rfl
  · intro x y
    simp [← equivShrink_add]
    rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y Z : C
⊢ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom

Tactic:
associativity,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y Z : C
⊢ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z =
    F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
associativity,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z = F.map (α_ X Y Z).inv ≫ F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: case ih_η
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : p ⊗ f₁ ≅ pf₁
η_g₁ : p ⊗ g₁ ≅ pf₁
η_f₂ : pf₁ ⊗ f₂ ≅ pf₁f₂
η_g₂ : pf₁ ⊗ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ◁ η ▷ f₂ ≪≫ ?η_g = normalizeIsoComp η_f₁ η_f₂

pp: case ih_θ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : p ⊗ f₁ ≅ pf₁
η_g₁ : p ⊗ g₁ ≅ pf₁
η_f₂ : pf₁ ⊗ f₂ ≅ pf₁f₂
η_g₂ : pf₁ ⊗ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ◁ g₁ ◁ θ ≪≫ normalizeIsoComp η_g₁ η_g₂ = ?η_g

pp: case η_g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : p ⊗ f₁ ≅ pf₁
η_g₁ : p ⊗ g₁ ≅ pf₁
η_f₂ : pf₁ ⊗ f₂ ≅ pf₁f₂
η_g₂ : pf₁ ⊗ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ⊗ g₁ ⊗ f₂ ≅ pf₁f₂

Tactic:
· apply naturality_whiskerRight _ _ _ ih_η

Goal state after:
case ih_θ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : p ⊗ f₁ ≅ pf₁
η_g₁ : p ⊗ g₁ ≅ pf₁
η_f₂ : pf₁ ⊗ f₂ ≅ pf₁f₂
η_g₂ : pf₁ ⊗ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ◁ g₁ ◁ θ ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_g₁ η_f₂
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ η = θ

Tactic:
by
  apply Iso.ext
  calc
    η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_η)]
    _ = θ.hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_θ)]

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ G.map (δ F (X ⊗ Y) Z) ≫
      G.map (δ F X Y ▷ F.obj Z) ≫
        δ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫
          δ G (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫ (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom =
    G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        δ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))

Tactic:
associativity,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ G.map (δ F (X ⊗ Y) Z) ≫
      G.map (δ F X Y ▷ F.obj Z) ≫
        G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫
          δ G (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.obj (F.obj X) ◁ δ G (F.obj Y) (F.obj Z) =
    G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        δ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ G.map (δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫
      δ G (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.obj (F.obj X) ◁ δ G (F.obj Y) (F.obj Z) =
    G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        δ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))

Tactic:
associativity,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ G.map (F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z) ≫
      δ G (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.obj (F.obj X) ◁ δ G (F.obj Y) (F.obj Z) =
    G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        δ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod G) ≫ ε (F.prod G)).1 = (𝟙 ((F.prod G).obj (𝟙_ (C × E)))).1

Tactic:
apply Monoidal.η_ε

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

Goal state before:
pp: case h₂
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
inst✝⁸ : MonoidalCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod G) ≫ ε (F.prod G)).2 = (𝟙 ((F.prod G).obj (𝟙_ (C × E)))).2

Tactic:
apply Monoidal.η_ε

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.unop
m : s.pt ⟶ (coneUnopOfCocone c).pt
w : ∀ (j : J), m ≫ (coneUnopOfCocone c).π.app j = s.π.app j
⊢ m = (hc.desc (coconeOfConeUnop s)).unop

Tactic:
by
    refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
    simpa only [Quiver.Hom.op_unop, IsColimit.fac] using! w (unop j)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y : Cᵒᵖ
X : C
f : Opposite.op X ⟶ Y
⊢ identities Cᵒᵖ f ↔ identities C f.unop

Tactic:
obtain ⟨f⟩ := f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
Y : Cᵒᵖ
X : C
f : Opposite.unop Y ⟶ Opposite.unop (Opposite.op X)
⊢ identities Cᵒᵖ (Opposite.op f) ↔ identities C (Quiver.Hom.unop (Opposite.op f))
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case map
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ (W.strictMap F).multiplicativeClosure (F.map f✝)

Tactic:
induction hf with
  | of f hf => exact le_multiplicativeClosure _ _ ⟨hf⟩
  | id x => simpa using .id (F.obj x)
  | comp_of _ _ hf hg h =>
    simpa using multiplicativeClosure.comp_of _ _ h (strictMap.map hg)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.injective C f
hg : MorphismProperty.injective C g
⊢ MorphismProperty.injective C (f ≫ g)

Tactic:
delta MorphismProperty.injective
    rw [hom_comp]
    exact hg.comp hf

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ Function.Bijective ⇑(hom f)

Tactic:
by
  rw [bijective_iff_isIso_ofHom]
  refine ⟨fun _ ↦ inferInstance, fun h ↦ ?_⟩
  have : IsIso ((forget C).map f) := h
  exact isIso_of_reflects_iso f (forget C)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c → IsLimit c.op

Tactic:
intro h
    exact (IsLimit.postcomposeHomEquiv _ _).invFun
      ((IsLimit.whiskerEquivalenceEquiv walkingSpanOpEquiv.symm).toFun h.op)

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

Goal state before:
pp: case e_a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫ F.obj (X ⊗ Y) ◁ i.inv.app Z ≫ LaxMonoidal.μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫ (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z)

Tactic:
rw [← whisker_exchange_assoc]

Goal state after:
case e_a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      (F.obj X ⊗ F.obj Y) ◁ i.inv.app Z ≫
        LaxMonoidal.μ F X Y ▷ F.obj Z ≫ LaxMonoidal.μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫ (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : ↑(Set.Ici c)
x✝ y✝ : M
⊢ ↑((fun d ↦ ⟨d.comap c.mk', ⋯⟩) ((fun d ↦ mapGen ⇑c.mk') d)) x✝ y✝ ↔ ↑d x✝ y✝

Tactic:
simp only [comap_rel]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : ↑(Set.Ici c)
x✝ y✝ : M
⊢ (mapGen ⇑c.mk') (c.mk' x✝) (c.mk' y✝) ↔ ↑d x✝ y✝
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case e'_2.e'_6
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ ⟦f x⟧ = (c.comapQuotientEquivOfSurj ↑f ⋯ hcd) ↑x

Tactic:
comapQuotientEquivOfSurj_mk,

Goal state after:
case e'_2.e'_6
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ ⟦f x⟧ = ↑(↑f x)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
| f x

Tactic:
← ι_comp_lift f

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
| (((lift R) f).toLinearMap ∘ₗ ι R) x
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (ι R) x = 0 ↔ x = 0

Tactic:
rw [← ι_inj R x 0, map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
d : D
⊢ L₂.map (((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app d =
    ((conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
exact (conjugateEquiv_counit adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) d)

Goal state after: