mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this✝ : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
Brec : (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)
Crec : (f fun i ↦ ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i ↦ g i (r i)
D : Disjoint (piFinset B) (piFinset C)
r : (a : ι) → α a
hr : r ∈ piFinset A
hri₀ : ¬r i₀ = j₂
i : ι
hi : i = i₀
this : r i₀ ∈ B i₀
⊢ r i ∈ B i

Tactic:
hi

Goal state after:
case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this✝ : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
Brec : (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)
Crec : (f fun i ↦ ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i ↦ g i (r i)
D : Disjoint (piFinset B) (piFinset C)
r : (a : ι) → α a
hr : r ∈ piFinset A
hri₀ : ¬r i₀ = j₂
i : ι
hi : i = i₀
this : r i₀ ∈ B i₀
⊢ r i₀ ∈ B i₀
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2._hc
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
⊢ k.castSucc < i.succ → update c k 0 i = 0

Tactic:
hi

Goal state after:
case refine_2._hc
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
hi : k.castSucc < i.succ
⊢ update c k 0 i = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ A.det = B.det

Tactic:
rw [← det_transpose A, ← det_transpose B]

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ Aᵀ.det = Bᵀ.det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_3.refine_3
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((σ.symm (x, k)).1, k) = σ.symm (x, k)
⊢ (fun k x ↦ { toFun := fun x ↦ (σ (x, k)).1, invFun := fun x ↦ (σ.symm (x, k)).1, left_inv := ⋯, right_inv := ⋯ }) ∈
    univ

Tactic:
apply Finset.mem_univ

Goal state after:
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
⊢ A.det = ∑ j, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det

Tactic:
rw [← det_transpose A, det_succ_column_zero]

Goal state after:
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
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
⊢ A.det = ∑ i, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
by
  rw [← det_transpose, det_succ_row _ j]
  refine Finset.sum_congr rfl fun i _ => ?_
  rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w'
inst✝ : F.IsRepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)} (F ⋙ uliftFunctor.{v, w'})

Tactic:
rw [preservesLimitsOfSize_iff_of_natIso (F ⋙ uliftFunctor.{v}).uliftYonedaReprXIso.symm]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w'
inst✝ : F.IsRepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftYoneda.{w', v, u}.obj (F ⋙ uliftFunctor.{v, w'}).reprX)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (α_ X (Y ⊗ 𝟙_ C) (𝟙_ C)).inv ≫ (X ◁ (ρ_ Y).hom) ▷ 𝟙_ C =
    (α_ X (Y ⊗ 𝟙_ C) (𝟙_ C)).inv ≫ (α_ X Y (𝟙_ C)).inv ▷ 𝟙_ C ≫ (ρ_ (X ⊗ Y)).hom ▷ 𝟙_ C

Tactic:
←
      cancel_epi (X ◁ (α_ _ _ _).inv),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ (α_ Y (𝟙_ C) (𝟙_ C)).inv ≫ (α_ X (Y ⊗ 𝟙_ C) (𝟙_ C)).inv ≫ (X ◁ (ρ_ Y).hom) ▷ 𝟙_ C =
    X ◁ (α_ Y (𝟙_ C) (𝟙_ C)).inv ≫ (α_ X (Y ⊗ 𝟙_ C) (𝟙_ C)).inv ≫ (α_ X Y (𝟙_ C)).inv ▷ 𝟙_ C ≫ (ρ_ (X ⊗ Y)).hom ▷ 𝟙_ C
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

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
E' : Type u₄
inst✝⁵ : Category.{v₄, u₄} E'
inst✝⁴ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝³ : F₁.LaxMonoidal
inst✝² : F₂.LaxMonoidal
inst✝¹ : F₃.LaxMonoidal
e : F₁ ≅ F₂
inst✝ : NatTrans.IsMonoidal e.hom
X Y : C
⊢ LaxMonoidal.μ F₂ X Y ≫ e.inv.app (X ⊗ Y) = (e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y

Tactic:
← cancel_mono (e.hom.app (X ⊗ Y)),

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
E' : Type u₄
inst✝⁵ : Category.{v₄, u₄} E'
inst✝⁴ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝³ : F₁.LaxMonoidal
inst✝² : F₂.LaxMonoidal
inst✝¹ : F₃.LaxMonoidal
e : F₁ ≅ F₂
inst✝ : NatTrans.IsMonoidal e.hom
X Y : C
⊢ (LaxMonoidal.μ F₂ X Y ≫ e.inv.app (X ⊗ Y)) ≫ e.hom.app (X ⊗ Y) =
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (X ⊗ Y)
Module: Mathlib.CategoryTheory.Monoidal.Linear

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ F.map ((r • f) ▷ Z) = F.map (r • f ▷ Z)

Tactic:
Functor.Monoidal.map_whiskerRight

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ Functor.OplaxMonoidal.δ F X Z ≫ F.map (r • f) ▷ F.obj Z ≫ Functor.LaxMonoidal.μ F Y Z = F.map (r • f ▷ Z)
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✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ { pt := (biproduct.bicone f).pt ⊗ X, π := fun j ↦ biproduct.π f j ▷ X, ι := fun j ↦ biproduct.ι f j ▷ X, ι_π := ⋯ }.π
      j✝ =
    (∑ j, biproduct.π f j ▷ X ≫ biproduct.ι (fun j ↦ f j ⊗ X) j) ≫ biproduct.π (fun j ↦ f j ⊗ X) j✝

Tactic:
simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero,
    Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]

Goal state after:
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
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
⊢ g = h

Tactic:
cases nonempty_fintype J
  apply (cancel_epi (rightDistributor f X).inv).mp
  ext
  simp [w]

Goal state after:
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
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
⊢ g = h

Tactic:
apply (cancel_epi (α_ _ _ _).inv).mp
  ext
  simp [w]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R}, 0 ▷ X = 0

Tactic:
intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp [ModuleCat.hom_whiskerRight]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_4
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R} (f g : Y ⟶ Z), (f + g) ▷ X = f ▷ X + g ▷ X

Tactic:
intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp [ModuleCat.hom_whiskerRight]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
⊢ ∀ (r : R) {Y Z : ModuleCat R} (f : Y ⟶ Z) (X : ModuleCat R), (r • f) ▷ X = r • f ▷ X

Tactic:
intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp [ModuleCat.hom_whiskerRight]

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
h : F.CoreMonoidal
x✝ : C
⊢ (ρ_ (F.obj x✝)).inv = F.map (ρ_ x✝).inv ≫ (h.μIso x✝ (𝟙_ C)).inv ≫ F.obj x✝ ◁ h.εIso.inv

Tactic:
rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]

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.leftOp
j : Jᵒᵖ
⊢ ((hc.desc (coconeOfConeLeftOp s)).unop ≫ (coneLeftOpOfCocone c).π.app j).op = (s.π.app j).op

Tactic:
by
      simp only [coneLeftOpOfCocone_π_app, op_comp, Quiver.Hom.op_unop, IsColimit.fac,
        coconeOfConeLeftOp_ι_app, op_unop]

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.leftOp
m : s.pt ⟶ (coneLeftOpOfCocone c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneLeftOpOfCocone c).π.app j = s.π.app j
⊢ m = (hc.desc (coconeOfConeLeftOp 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, coconeOfConeLeftOp_ι_app] using! w (op j)

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.leftOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeLeftOp c).pt
w : ∀ (j : J), m ≫ (coneOfCoconeLeftOp c).π.app j = s.π.app j
j : Jᵒᵖ
⊢ (c.ι.app j ≫ m.unop).op = (c.ι.app j ≫ (hc.desc (coconeLeftOpOfCone s)).op.unop).op

Tactic:
simpa only [Quiver.Hom.unop_op, IsColimit.fac, coneOfCoconeLeftOp_π_app] using! w (unop j)

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 : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C
⊢ (δ (F.prod' G) x✝¹ x✝ ≫ μ (F.prod' G) x✝¹ x✝).2 = (𝟙 ((F.prod' G).obj (x✝¹ ⊗ x✝))).2

Tactic:
· simp only [CategoryTheory.prod_comp_snd, prod'_μ_snd, prod'_δ_snd, δ_μ,
        prod'_obj, prod_id]

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
inst✝ : HasWidePushouts C
ι : Type w
⊢ HasLimitsOfShape (WidePullbackShape ι) Cᵒᵖ

Tactic:
rw [hasLimitsOfShape_opposite_iff]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasWidePushouts C
ι : Type w
⊢ HasColimitsOfShape (WidePullbackShape ι)ᵒᵖ C
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ HasWidePullbacks Cᵒᵖ ↔ HasWidePushouts C

Tactic:
by
  refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
  rw [← hasLimitsOfShape_opposite_opposite_iff]
  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

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✝
inst✝ : HasFiniteWidePushouts C
J : Type
x✝ : Finite J
⊢ HasLimitsOfShape (WidePullbackShape J) Cᵒᵖ

Tactic:
rw [hasLimitsOfShape_opposite_iff]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} J✝
inst✝ : HasFiniteWidePushouts C
J : Type
x✝ : Finite J
⊢ HasColimitsOfShape (WidePullbackShape J)ᵒᵖ C
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj W) ≫ G.map (f ≫ h)) ≫ 𝟙 (G.obj Z) = G.map f ≫ G.map h

Tactic:
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]

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

Goal state before:
pp: case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj X) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h

Tactic:
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]

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

Goal state before:
pp: case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj Y) ≫ G.map k) ≫ 𝟙 (G.obj Z) = G.map k

Tactic:
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]

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

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

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫
        F.obj W ◁ (β_ (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          (α_ (F.obj W) (F.obj Y ⊗ F.obj X) (F.obj Z)).inv ≫
            (F.obj W ◁ μ F Y X ≫ μ F W (Y ⊗ X) ≫ F.map (α_ W Y X).inv) ▷ F.obj Z ≫
              μ F ((W ⊗ Y) ⊗ X) Z ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ μ F W X ▷ (F.obj Y ⊗ F.obj Z) ≫
      F.obj (W ⊗ X) ◁ μ F Y Z ≫
        μ F (W ⊗ X) (Y ⊗ Z) ≫
          F.map (α_ (W ⊗ X) Y Z).inv ≫
            F.map ((α_ W X Y).hom ▷ Z) ≫
              F.map ((W ◁ (β_ X Y).hom) ▷ Z) ≫ F.map ((α_ W Y X).inv ▷ Z) ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: 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
⊢ (c.comapQuotientEquivOfSurj ↑f ⋯ hcd).symm ⟦f x⟧ = ↑x

Tactic:
by
  convert! RingEquiv.symm_apply_apply _ _
  rw [comapQuotientEquivOfSurj_mk, RingEquiv.coe_toRingHom]
  rfl

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x y z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 + x.2 <• y.1) <• z.1 = x.1 •> (y.1 •> z.2 + y.2 <• z.1) + x.2 <• (y.1 * z.1)

Tactic:
simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm, op_mul]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
l : List (tsze R M)
⊢ l.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst l)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst l)).prod)
        l.zipIdx).sum

Tactic:
induction l with

Goal state after: