mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f x = x
⊢ #(f.cycleOf x).support < 2

Tactic:
← cycleOf_eq_one_iff

Goal state after:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f.cycleOf x = 1
⊢ #(f.cycleOf x).support < 2
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ (Multiset.map (fun n ↦ -(-1) ^ n) 0).prod = (-1) ^ (Multiset.sum 0 + card 0)

Tactic:
| empty =>

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
← cycleOf_eq_one_iff

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f.cycleOf x = 1
⊢ orderOf (f.cycleOf x) ∣ orderOf f
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
hs : (↑∅).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑∅).Pairwise fun i j ↦ Commute (k i) (k j)
⊢ (∅.noncommProd k hs').cycleType = ∑ i ∈ ∅, (k i).cycleType

Tactic:
| empty =>

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * τ * σ'⁻¹)

Tactic:
mul_assoc

Goal state after:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
⊢ {Fintype.card (Fin (n + 2))} = {n + 2}

Tactic:
Fintype.card_fin

Goal state after:
n : ℕ
⊢ {n + 2} = {n + 2}
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case h
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
z : α
⊢ (g * g.cycleOf x) z = (g.cycleOf x * g) z

Tactic:
by_cases hz : SameCycle g x z

Goal state after:
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
z : α
hz : g.SameCycle x z
⊢ (g * g.cycleOf x) z = (g.cycleOf x * g) z

case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
z : α
hz : ¬g.SameCycle x z
⊢ (g * g.cycleOf x) z = (g.cycleOf x * g) z
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
hc : f x = x
⊢ ¬(f.cycleOf x).IsCycle

Tactic:
← cycleOf_eq_one_iff

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
hc : f.cycleOf x = 1
⊢ ¬(f.cycleOf x).IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ¬g x = x

Tactic:
← cycleOf_eq_one_iff

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ¬g.cycleOf x = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
⊢ k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

Tactic:
by
    refine ⟨fun h ↦ ?_, imp_lemma⟩
    have aux : ∀ h : Perm α, h = k⁻¹ * (k * h * k⁻¹) * k := fun _ ↦ by group
    rw [aux g, aux c]
    exact imp_lemma h

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
⊢ c (d x) = d x ↔ c x = x

Tactic:
· rw [← Perm.mul_apply,
      Commute.eq (cycleFactorsFinset_mem_commute g hc hd h),
      mul_apply, EmbeddingLike.apply_eq_iff_eq]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ g = swap a (g a) * swap (g a) (g (g a))

Tactic:
have ha' := hg3.support_eq_iff_mem_support.mpr ha

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
⊢ g = swap a (g a) * swap (g a) (g (g a))
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ g.subtypePerm ⋯ = c.subtypePermOfSupport

Tactic:
ext ⟨x, hx⟩
  simp only [subtypePerm_apply, Subtype.coe_mk, subtypePermOfSupport]
  exact ((mem_cycleFactorsFinset_iff.mp hc).2 x hx).symm

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
e₁ e₂ : m ≃ n
h : (A.submatrix ⇑e₁ ⇑e₂).IsDetpBalanced a b
⊢ A.IsDetpBalanced a b

Tactic:
by simpa using h.submatrix_equiv e₁.symm e₂.symm

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

Goal state before:
pp: case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * descFunLift F s y * descFunLift F s z =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)

Tactic:
mul_assoc

Goal state after:
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * (descFunLift F s y * descFunLift F s z) =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * descFunLift F s y * descFunLift F s z =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)

Tactic:
mul_assoc

Goal state after:
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * (descFunLift F s y * descFunLift F s z) =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case empty
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
⊢ ∃ S, ∀ {X : C}, X ∈ ∅ → Nonempty (X ⟶ S)

Tactic:
| empty =>

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

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ (diagonal d).det = ∏ i, d i

Tactic:
by
  rw [det_apply']
  refine (Finset.sum_eq_single 1 ?_ ?_).trans ?_
  · rintro σ - h2
    obtain ⟨x, h3⟩ := not_forall.1 (mt Equiv.ext h2)
    convert! mul_zero (ε σ)
    apply Finset.prod_eq_zero (mem_univ x)
    exact if_neg h3
  · simp
  · simp

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

Goal state before:
pp: case empty
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered 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⟩⟩⟩⟩ ∈ ∅ → f ≫ T mY = T mX

Tactic:
| empty =>

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

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ¬Bijective p
i j : n
hpij : p i = p j
hij : i ≠ j
σ : Perm n
x✝ : σ ∈ univ
⊢ ↑↑(sign σ) * ∏ x, M (σ x) (p x) * N (p x) x +
      ↑↑(sign (σ * Equiv.swap i j)) * ∏ x, M ((σ * Equiv.swap i j) x) (p x) * N (p x) x =
    0

Tactic:
have : (∏ x, M (σ x) (p x)) = ∏ x, M ((σ * Equiv.swap i j) x) (p x) :=
          Fintype.prod_equiv (swap i j) _ _ (by simp [apply_swap_eq_self hpij])

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ¬Bijective p
i j : n
hpij : p i = p j
hij : i ≠ j
σ : Perm n
x✝ : σ ∈ univ
this : ∏ x, M (σ x) (p x) = ∏ x, M ((σ * Equiv.swap i j) x) (p x)
⊢ ↑↑(sign σ) * ∏ x, M (σ x) (p x) * N (p x) x +
      ↑↑(sign (σ * Equiv.swap i j)) * ∏ x, M ((σ * Equiv.swap i j) x) (p x) * N (p x) x =
    0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case empty
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
hj : j ∉ ∅
⊢ (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det

Tactic:
| empty =>

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

Goal state before:
pp: case empty
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
⊢ ∀ (c : n → R), (∀ i ∉ ∅, c i = 0) → ∀ k ∉ ∅, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det

Tactic:
| empty =>

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

Goal state before:
pp: case empty
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
⊢ ∃ S, ∀ {X : C}, X ∈ ∅ → Nonempty (S ⟶ X)

Tactic:
| empty =>

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

Goal state before:
pp: case empty
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⟩⟩⟩⟩ ∈ ∅ → T mX ≫ f = T mY

Tactic:
| empty =>

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsCofilteredOrEmpty C
I : Type u_1
inst✝ : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
this : IsCofiltered C
⊢ ∃ k fki g, ∀ (x : I), g x ≫ f x = fki

Tactic:
cases nonempty_fintype I
  obtain ⟨k, fk, hk⟩ := IsCofiltered.inf_exists (insert i (Finset.univ.image j))
    (Finset.univ.image fun x ↦ ⟨j x, i, by simp, by simp, f x⟩)
  exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : c.IsColimit
s : Cocone F
j : J
x : F.obj j
⊢ (ConcreteCategory.hom ((F.coconeTypesEquiv c).ι.app j ≫ ↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x)).toFun x =
    (ConcreteCategory.hom (s.ι.app j)).toFun x

Tactic:
exact congr_fun (hc.fac (F.coconeTypesEquiv.symm s) j) x

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
G : J ⥤ Type w₀'
e : (j : J) → G.obj j ≃ F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)
c' : G.CoconeTypes
j : J
⊢ hc.desc (c'.precompose (fun {j'} ↦ ⇑(e j').symm) ⋯) ∘ (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).ι j = c'.ι j

Tactic:
precompose_ι,

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
G : J ⥤ Type w₀'
e : (j : J) → G.obj j ≃ F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)
c' : G.CoconeTypes
j : J
⊢ hc.desc (c'.precompose (fun {j'} ↦ ⇑(e j').symm) ⋯) ∘ (fun j ↦ c.ι j ∘ ⇑(e j)) j = c'.ι j
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
G : J ⥤ Type w₀'
e : (j : J) → G.obj j ≃ F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)
c' : G.CoconeTypes
j : J
⊢ (c'.precompose (fun {j'} ↦ ⇑(e j').symm) ⋯).ι j ∘ ⇑(e j) = c'.ι j

Tactic:
precompose_ι,

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
G : J ⥤ Type w₀'
e : (j : J) → G.obj j ≃ F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)
c' : G.CoconeTypes
j : J
⊢ (fun j ↦ c'.ι j ∘ ⇑(e j).symm) j ∘ ⇑(e j) = c'.ι j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case empty
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_2
inst✝ : DecidableEq ι
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
⊢ f (update m i (∑ a ∈ ∅, g a)) = ∑ a ∈ ∅, f (update m i (g a))

Tactic:
| empty =>

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

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j
⊢ IsLimit c

Tactic:
· have := fun c y ↦ h _ (sectionOfCone c y).2
    choose x hx using fun c y ↦ h _ (sectionOfCone c y).2
    exact ⟨fun d ↦ ↾(x d), fun c j ↦ by ext y; exact (hx c y).1 j,
      fun c f hf ↦ by ext y; exact (hx c y).2 (f y) (fun j ↦ congr_hom (hf j) y)⟩

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

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ ((if i.succ = 0 then 1 else -1) * sign σ) • ∏ x, A ((decomposeFin.symm (i.succ, σ)) x) x =
    -1 *
      (A i.succ 0 *
        sign σ • ∏ i_1, (of fun i_2 j ↦ A (i.succ.succAbove i_2) j.succ).submatrix (⇑i.cycleRange) id (σ i_1) i_1)

Tactic:
if_neg (Fin.succ_ne_zero i)

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ (-1 * sign σ) • ∏ x, A ((decomposeFin.symm (i.succ, σ)) x) x =
    -1 *
      (A i.succ 0 *
        sign σ • ∏ i_1, (of fun i_2 j ↦ A (i.succ.succAbove i_2) j.succ).submatrix (⇑i.cycleRange) id (σ i_1) i_1)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case empty
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✝ : LinearOrder ι
a b : (i : ι) → M₁ i
⊢ f a - f (∅.piecewise b a) = ∑ i ∈ ∅, f fun j ↦ if j ∈ ∅ → j < i then a j else if i = j then a j - b j else b j

Tactic:
| empty =>

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
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det =
    (-1) ^ ↑i * ∑ i_1, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Tactic:
mul_assoc

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ (-1) ^ ↑i * (↑↑(sign i.cycleRange⁻¹) * A.det) =
    (-1) ^ ↑i * ∑ i_1, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : (forget C).IsCorepresentable
J : Type w
inst✝¹ : Category.{t, w} J
G : J ⥤ C
inst✝ : HasLimit G
⊢ Small.{v, max v w} ↑(G ⋙ forget C).sections

Tactic:
rw [← Types.hasLimit_iff_small_sections]
  infer_instance

Goal state after:
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)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
⊢ ↟(f X✝ Z✝ ⋯) = ↟(f X✝ Y✝ ⋯) ≫ ↟(f Y✝ Z✝ ⋯)

Tactic:
ext
    symm
    apply Module.DirectedSystem.map_map f

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
⊢ ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
by intros; simp [← id_tensorHom, ← tensorHom_id, triangle]

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

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

Tactic:
by
  rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y X' Y' : C
f : X ≅ Y
g : X' ≅ Y'
⊢ (f.hom ⊗ₘ g.hom) ≫ (f.inv ⊗ₘ g.inv) = 𝟙 (X ⊗ X')

Tactic:
simp [Iso.hom_inv_id, Iso.hom_inv_id]

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

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

Tactic:
rw [← triangle, Iso.inv_hom_id_assoc]

Goal state after:
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
⊢ ∀ (X : D) {Y Z : D} (r : R) (f : Y ⟶ Z), X ◁ (r • f) = r • X ◁ f

Tactic:
intro X Y Z r f
      apply F.map_injective
      rw [Functor.Monoidal.map_whiskerLeft]
      simp

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
⊢ HasLimitsOfShape Jᵒᵖ Cᵒᵖ ↔ HasColimitsOfShape J C

Tactic:
refine ⟨fun _ ↦ hasColimitsOfShape_of_hasLimitsOfShape_op, fun _ ↦ ?_⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
x✝ : 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
W : MorphismProperty C
F : C ⥤ D
⊢ W.multiplicativeClosure.strictMap F ≤ (W.strictMap F).multiplicativeClosure

Tactic:
intro _ _ f hf
  induction hf with | map hf
  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.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
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
⊢ MorphismProperty.injective C = monomorphisms C → (forget C).PreservesMonomorphisms

pp: case mpr
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
⊢ (forget C).PreservesMonomorphisms → MorphismProperty.injective C = monomorphisms C

Tactic:
· intro h
    constructor
    rintro _ _ f (hf : monomorphisms C f)
    rw [mono_iff_injective]
    rw [← h] at hf
    exact hf

Goal state after:
case mpr
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
⊢ (forget C).PreservesMonomorphisms → MorphismProperty.injective C = monomorphisms C
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (λ_ X).hom ▷ 𝟙_ C =
    (β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C

Tactic:
by
      simp

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
X : C
⊢ 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Tactic:
by
      simp

Goal state after: