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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
⊢ ∃ S T, ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → T mX ≫ f = T mY

Tactic:
classical
  induction H using Finset.induction with
  | empty =>
    obtain ⟨S, f⟩ := inf_objs_exists O
    exact ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩
  | insert h' H' nmf h'' =>
    obtain ⟨X, Y, mX, mY, f⟩ := h'
    obtain ⟨S', T', w'⟩ := h''
    refine ⟨eq (T' mX ≫ f) (T' mY), fun mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ, ?_⟩
    intro X' Y' mX' mY' f' mf'
    rw [Category.assoc]
    by_cases h : X = X' ∧ Y = Y'
    · rcases h with ⟨rfl, rfl⟩
      grind [eq_condition]
    · rw [@w' _ _ mX' mY' f' _]
      apply Finset.mem_of_mem_insert_of_ne mf'
      contrapose h
      obtain ⟨rfl, h⟩ := h
      trivial

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case insert.x
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ k ∉ s

pp: case insert.x
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ ∀ (i_1 j : n), A i_1 j = B.updateRow i (A i) i_1 j + update c i 0 i_1 * B.updateRow i (A i) k j

Tactic:
· exact fun h => hk (Finset.mem_insert_of_mem h)

Goal state after:
case insert.x
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ ∀ (i_1 j : n), A i_1 j = B.updateRow i (A i) i_1 j + update c i 0 i_1 * B.updateRow i (A i) k j
Module: Mathlib.Algebra.Category.Grp.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget GrpCat) x y
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨x.fst, x.snd⁻¹⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, y.snd⁻¹⟩.snd

Tactic:
obtain ⟨k, f, g, hfg⟩ := h

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg :
  (ConcreteCategory.hom ((F ⋙ forget GrpCat).map f)) x.snd = (ConcreteCategory.hom ((F ⋙ forget GrpCat).map g)) y.snd
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨x.fst, x.snd⁻¹⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, y.snd⁻¹⟩.snd
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: 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✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
a : R
f₀ : M₁ i →ₗ[R] M₁' i
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
⊢ ((compLinearMapₗ (update f i (a • f₀))) g) x = ((a • compLinearMapₗ (update f i f₀)) g) x

Tactic:
change (g fun j ↦ update f i (a • f₀) j <| x j) = a • g fun j ↦ update f i f₀ j (x j)

Goal state after:
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✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
a : R
f₀ : M₁ i →ₗ[R] M₁' i
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
⊢ (g fun j ↦ (update f i (a • f₀) j) (x j)) = a • g fun j ↦ (update f i f₀ j) (x j)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ ∑ i, (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
    ∑ j, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det

Tactic:
refine Finset.sum_congr rfl fun i _ => ?_

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
    (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f

Tactic:
ext x
  change (F'.e ≫ F'.m) _ = _
  rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)
⊢ (ConcreteCategory.hom (F.map (Opposite.op { down := { down := ⋯ } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p.succ)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)

Tactic:
← ih

Goal state after:
case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)
⊢ (ConcreteCategory.hom (F.map (Opposite.op { down := { down := ⋯ } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p.succ)) =
    (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p))
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ ∑ j_1, (-1) ^ (↑j + ↑j_1) * Aᵀ j j_1 * (Aᵀ.submatrix j.succAbove j_1.succAbove).det =
    ∑ i, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
refine Finset.sum_congr rfl fun i _ => ?_

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ (↑j + ↑i) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
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
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : CreatesLimit K F
inst✝ : CreatesLimit (K ⋙ F) G
c : Cone (K ⋙ F ⋙ G)
t : IsLimit c
c' : Cone ((K ⋙ F) ⋙ G) := c
t' : IsLimit c' := t
⊢ LiftableCone K (F ⋙ G) c

Tactic:
exact
      { liftedCone := liftLimit (liftedLimitIsLimit t')
        validLift := (Cone.functoriality (K ⋙ F) G).mapIso
            (liftedLimitMapsToOriginal (liftedLimitIsLimit t')) ≪≫
          liftedLimitMapsToOriginal t' }

Goal state after:
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
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : CreatesLimit K F
inst✝ : CreatesLimit (K ⋙ F) G
c : Cone (K ⋙ F ⋙ G)
t : IsLimit c
⊢ LiftableCone K (F ⋙ G) c

Tactic:
by
    let c' : Cone ((K ⋙ F) ⋙ G) := c
    let t' : IsLimit c' := t
    exact
      { liftedCone := liftLimit (liftedLimitIsLimit t')
        validLift := (Cone.functoriality (K ⋙ F) G).mapIso
            (liftedLimitMapsToOriginal (liftedLimitIsLimit t')) ≪≫
          liftedLimitMapsToOriginal t' }

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (preservesLimitIso ((evaluation K C).obj k) F).inv ≫ (limit.π F j).app k = limit.π (F ⋙ (evaluation K C).obj k) j

Tactic:
Iso.inv_comp_eq

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (limit.π F j).app k = (preservesLimitIso ((evaluation K C).obj k) F).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
⊢ CreatesLimit F (forget GrpCat)

Tactic:
set e : forget₂ GrpCat.{u} MonCat.{u} ⋙ forget MonCat.{u} ≅ forget GrpCat.{u} := Iso.refl _
  exact createsLimitOfNatIso e

Goal state after:
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 :
  (R.associator L R).inv ≫ whiskerRight h.counit R = inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (whiskerRight h.counit R)

Tactic:
Iso.inv_comp_eq

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 :
  whiskerRight h.counit R = (R.associator L R).hom ≫ inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (whiskerRight h.counit R)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
⊢ (X ◁ if h : P then f h else f' h) = if h : P then X ◁ f h else X ◁ f' h

Tactic:
split_ifs

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ X ◁ f h✝ = X ◁ f h✝

case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ X ◁ f' h✝ = X ◁ f' h✝
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
⊢ (if h : P then f h else f' h) ▷ Z = if h : P then f h ▷ Z else f' h ▷ Z

Tactic:
split_ifs

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
h✝ : P
⊢ f h✝ ▷ Z = f h✝ ▷ Z

case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
h✝ : ¬P
⊢ f' h✝ ▷ Z = f' h✝ ▷ Z
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (f ⊗ₘ if h : P then g h else g' h) = if h : P then f ⊗ₘ g h else f ⊗ₘ g' h

Tactic:
split_ifs

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ f ⊗ₘ g h✝ = f ⊗ₘ g h✝

case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ f ⊗ₘ g' h✝ = f ⊗ₘ g' h✝
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (if h : P then g h else g' h) ⊗ₘ f = if h : P then g h ⊗ₘ f else g' h ⊗ₘ f

Tactic:
split_ifs

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ g h✝ ⊗ₘ f = g h✝ ⊗ₘ f

case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ g' h✝ ⊗ₘ f = g' h✝ ⊗ₘ f
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
Y : C
⊢ (leftDistributor X f ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ X ⊗ f j) Y =
    α_ X (⨁ f) Y ≪≫
      (asIso (𝟙 X) ⊗ᵢ rightDistributor f Y) ≪≫
        (leftDistributor X fun j ↦ f j ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ X (f x) Y).symm

Tactic:
cases nonempty_fintype J
  ext
  simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom,
    asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor,
    tensor_sum, comp_tensor_id, tensorIso_hom, leftDistributor_hom, rightDistributor_hom,
    biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π, Finset.sum_dite_irrel,
    Finset.sum_dite_eq', Finset.sum_const_zero, Finset.mem_univ, if_true]
  simp_rw [← tensorHom_id, ← id_tensorHom]
  simp only [← comp_tensor_id, ← id_tensor_comp_assoc, Category.assoc, biproduct.ι_π, comp_dite,
    dite_comp, tensor_dite, dite_tensor]
  simp

Goal state after:
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 ◁ g₁ ◁ θ ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_g₁ η_f₂

Tactic:
apply naturality_whiskerLeft _ _ _ ih_θ

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ η_f = η_g

Tactic:
← ih

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g
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
x✝¹ x✝ : C × E
⊢ (μ (F.prod G) x✝¹ x✝ ≫ δ (F.prod G) x✝¹ x✝).1 = (𝟙 ((F.prod G).obj x✝¹ ⊗ (F.prod G).obj x✝)).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
x✝¹ x✝ : C × E
⊢ (μ (F.prod G) x✝¹ x✝ ≫ δ (F.prod G) x✝¹ x✝).2 = (𝟙 ((F.prod G).obj x✝¹ ⊗ (F.prod G).obj x✝)).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
x✝ : HasColimitsOfShape J C
⊢ HasLimitsOfShape Jᵒᵖ Cᵒᵖ

Tactic:
have : HasColimitsOfShape Jᵒᵖᵒᵖ C := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
x✝ : HasColimitsOfShape J C
this : HasColimitsOfShape Jᵒᵖᵒᵖ C
⊢ HasLimitsOfShape Jᵒᵖ Cᵒᵖ
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : naturalityProperty app f
hg : naturalityProperty app g
⊢ naturalityProperty app (f ≫ g)

Tactic:
simp only [naturalityProperty] at hf hg ⊢
    simp only [Functor.map_comp, Category.assoc, hg]
    slice_lhs 1 2 => rw [hf]
    rw [Category.assoc]

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

Goal state before:
pp: case of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g : Y✝ ⟶ Z✝
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
hf₀ : W f✝
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure (f ≫ f✝)

Tactic:
| of _ hf₀ =>

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

Goal state before:
pp: case of
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
hf₀ : W f✝
⊢ W f✝

Tactic:
| of _ hf₀ =>

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.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✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ (F.obj X✝) (F.obj Y✝) (F.obj Z✝)).hom ≫
      (β_ (F.obj X✝) (F.obj Y✝ ⊗ F.obj Z✝)).hom ≫ μ F Y✝ Z✝ ▷ F.obj X✝ ≫ μ F (Y✝ ⊗ Z✝) X✝ ≫ F.map (α_ Y✝ Z✝ X✝).hom =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫
        F.obj Y✝ ◁ (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ F.obj Y✝ ◁ μ F Z✝ X✝ ≫ μ F Y✝ (Z✝ ⊗ X✝)

Tactic:
Functor.LaxMonoidal.associativity,

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 C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ (F.obj X✝) (F.obj Y✝) (F.obj Z✝)).hom ≫
      (β_ (F.obj X✝) (F.obj Y✝ ⊗ F.obj Z✝)).hom ≫
        (α_ (F.obj Y✝) (F.obj Z✝) (F.obj X✝)).hom ≫ F.obj Y✝ ◁ μ F Z✝ X✝ ≫ μ F Y✝ (Z✝ ⊗ X✝) =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫
        F.obj Y✝ ◁ (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ F.obj Y✝ ◁ μ F Z✝ X✝ ≫ μ F Y✝ (Z✝ ⊗ X✝)
Module: Mathlib.Algebra.Category.ModuleCat.EpiMono

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by
  rw [epi_iff_range_eq_top, LinearMap.range_eq_top]

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 : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ δ e.functor X Y ≫
      e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
        e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y)) =
    e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y)

Tactic:
apply e.inverse.map_injective

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 : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ e.inverse.map
      (δ e.functor X Y ≫
        e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
          e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y))) =
    e.inverse.map (e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y))
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'
e : C ≌ D
inst✝⁵ : e.functor.Monoidal
inst✝⁴ : e.inverse.Monoidal
inst✝³ : e.IsMonoidal
e' : D ≌ E
inst✝² : e'.functor.Monoidal
inst✝¹ : e'.inverse.Monoidal
inst✝ : e'.IsMonoidal
⊢ (e.trans e').IsMonoidal

Tactic:
by
  dsimp [Equivalence.IsMonoidal]
  rw [trans_toAdjunction]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a} ⊆
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom).ker

Tactic:
intro _ hx

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
hx : a✝ ∈ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a}
⊢ a✝ ∈ ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom).ker
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) a) - DFinsupp.single j a} ⊆
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker

Tactic:
intro _ hx

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑((F ⋙ uliftFunctor).obj j)
hx :
  a✝ ∈
    {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) a) - DFinsupp.single j a}
⊢ a✝ ∈ ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker