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

Goal state before:
pp: case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
h : (f ^ 1) ((f ^ ↑a) x) = (f ^ ↑a) ((f ^ 1) x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
simp only [zpow_one, zpow_natCast] at h

Goal state after:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
h : f ((f ^ a) x) = (f ^ a) (f x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case cons.inl
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, (σ a) b)

Tactic:
prodExtendRight_apply_ne _ fun h : a = a' => (List.nodup_cons.mp hl).1 (h ▸ mem_l)

Goal state after:
case cons.inl
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ (a, (σ a) b) = (a, (σ a) b)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
b : α
inst✝ : DecidableEq α
y : α
hab : y ≠ b
⊢ id y = y

Tactic:
id

Goal state after:
α : Type u_2
b : α
inst✝ : DecidableEq α
y : α
hab : y ≠ b
⊢ y = y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ id y = y

Tactic:
id

Goal state after:
α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ y = y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ (f.cycleOf x) y = if f.SameCycle x y then f y else y

Tactic:
dsimp only [cycleOf]

Goal state after:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ (ofSubtype (f.subtypePerm ⋯)) y = if f.SameCycle x y then f y else y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
⊢ c.subtypePermOfSupport ^ k = g.subtypePerm ⋯ ↔ c ^ k = ofSubtype (g.subtypePerm ⋯)

Tactic:
subtypePermOfSupport,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
⊢ c.subtypePerm ⋯ ^ k = g.subtypePerm ⋯ ↔ c ^ k = ofSubtype (g.subtypePerm ⋯)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∈ c.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

Tactic:
rw [iff_true_left (fun b ↦ (ha b).elim), ofSubtype_apply_of_not_mem, ← notMem_support]

Goal state after:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ (c ^ k).support

case neg.ha
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ c.support
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
Fin.cycleRange_of_lt hlt,

Goal state after:
case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ i.succ.succAbove (j + 1) = (swap 0 i.succ) j.succ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : n ∈ List.map (Finset.card ∘ support) l
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n

Tactic:
List.mem_map

Goal state after:
case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a ∈ l, (Finset.card ∘ support) a = n
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: G : Type u_2
inst✝ : Group G
⊢ 1 ::ᵥ Vector.nil ∈ vectorsProdEqOne G 1 ∧ ∀ x ∈ vectorsProdEqOne G 1, x = 1 ::ᵥ Vector.nil

Tactic:
mem_iff,

Goal state after:
G : Type u_2
inst✝ : Group G
⊢ (1 ::ᵥ Vector.nil).toList.prod = 1 ∧ ∀ (x : List.Vector G 1), x.toList.prod = 1 → x = 1 ::ᵥ Vector.nil
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : List.Vector G n
⊢ v.toList.prod⁻¹ ::ᵥ v ∈ vectorsProdEqOne G (n + 1)

Tactic:
mem_iff,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : List.Vector G n
⊢ (v.toList.prod⁻¹ ::ᵥ v).toList.prod = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (↑↑v).length g
⊢ g ^ p = 1

Tactic:
rw [← List.prod_replicate, ← v.1.2, ← hg, show v.val.val.prod = 1 from v.2]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Tactic:
suffices f = g → (g.IsCycle ↔ f.IsCycle) by
    rw [cycleFactorsFinset_eq_finset]
    simpa [eq_comm]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ f = g → (g.IsCycle ↔ f.IsCycle)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : n = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle

Tactic:
rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]

Goal state after:
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 : ι) → AddCommMonoid (M₁ i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : ι) → Module R (M₁ i)
inst✝ : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
⊢ f m = 0

Tactic:
by
  classical
    have : (0 : R) • (0 : M₁ i) = 0 := by simp
    rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]

Goal state after:
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 : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : Nonempty ι
⊢ f 0 = 0

Tactic:
obtain ⟨i, _⟩ : ∃ i : ι, i ∈ Set.univ := Set.exists_mem_of_nonempty ι

Goal state after:
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₂
inst✝ : Nonempty ι
i : ι
h✝ : i ∈ Set.univ
⊢ f 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case e'_2.h
n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
A : Matrix n n R
inst✝ : IsEmpty n
⊢ {x ∈ {default} | sign x = -1} = ∅

Tactic:
simp +decide

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.mul y).mul z) = descFunLift F s (x.mul (y.mul z))

Tactic:
dsimp; rw [mul_assoc]

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 ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s ((x.mul y).mul z) = descFunLift F s (x.mul (y.mul z))

Tactic:
dsimp; rw [mul_assoc]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ Z h, f ≫ h = g ≫ h
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
A : Matrix n n R
j : n
c : n → R
x✝ : n
⊢ ∑ i, c i • A x✝ i = (∑ k, c k • Aᵀ k) x✝

Tactic:
simp only [smul_eq_mul, Finset.sum_apply, Pi.smul_apply, transpose_apply]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
⊢ ∃ W h, h ≫ f = h ≫ g

Tactic:
obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ W h, h ≫ f = h ≫ g
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: case mk
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
t : F.ColimitType
fst✝ : J
snd✝ : F.obj fst✝
⊢ ∃ j x, F.ιColimitType j x = Quot.mk F.ColimitTypeRel ⟨fst✝, snd✝⟩

Tactic:
exact ⟨_, _, rfl⟩

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

Goal state before:
pp: case refine_1
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
σ : (a : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ ∀ (x : n × o), ((prodCongrLeft fun k ↦ σ k ⋯) x).2 = x.2

Tactic:
rintro ⟨-, x⟩

Goal state after:
case refine_1
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
σ : (a : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
fst✝ : n
x : o
⊢ ((prodCongrLeft fun k ↦ σ k ⋯) (fst✝, x)).2 = (fst✝, x).2
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✝¹¹ : Semiring R
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M₂
inst✝⁶ : Semiring S
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass R S M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module S M₃
inst✝¹ : Module R M₃
inst✝ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f₁ f₂ : MultilinearMap R M₁ M₂
⊢ { toFun := ⇑(f₁ + f₂) ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ } =
    { toFun := ⇑f₁ ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ } +
      { toFun := ⇑f₂ ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ }

Tactic:
ext
    simp only [Function.comp, coe_mk, add_apply]

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

Goal state before:
pp: case e'_3.e'_5
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 : ι
f₁ f₂ : M₁ i →ₗ[R] M₁' i
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f ↦ f (x i)
j : ι
⊢ (update f i f₁ j) (x j) = update (fun j ↦ (f j) (x j)) i (f₁ (x i)) j

Tactic:
exact Function.apply_update c f i f₁ j

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
C : Matrix n m R
D : Matrix n n R
⊢ (fromBlocks Aᵀ Cᵀ 0ᵀ Dᵀ).det = A.det * D.det

Tactic:
transpose_zero,

Goal state after:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
C : Matrix n m R
D : Matrix n n R
⊢ (fromBlocks Aᵀ Cᵀ 0 Dᵀ).det = A.det * D.det
Module: Mathlib.CategoryTheory.Limits.Types.Limits

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

Tactic:
let cs := coneOfSection hs

Goal state after:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
x✝ : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
cs : Cone F := coneOfSection ⋯
⊢ ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j
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
this : ∀ (c_1 : Cone F) (y : c_1.pt), ∃! x, ∀ (j : J), (hom (c.π.app j)) x = ↑(sectionOfCone c_1 y) j
⊢ IsLimit c

Tactic:
choose x hx using fun c y ↦ h _ (sectionOfCone c y).2

Goal state after:
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
this : ∀ (c_1 : Cone F) (y : c_1.pt), ∃! x, ∀ (j : J), (hom (c.π.app j)) x = ↑(sectionOfCone c_1 y) j
x : (c_1 : Cone F) → c_1.pt → c.pt
hx :
  ∀ (c_1 : Cone F) (y : c_1.pt),
    (fun x ↦ ∀ (j : J), (hom (c.π.app j)) x = ↑(sectionOfCone c_1 y) j) (x c_1 y) ∧
      ∀ (y_1 : c.pt), (fun x ↦ ∀ (j : J), (hom (c.π.app j)) x = ↑(sectionOfCone c_1 y) j) y_1 → y_1 = x c_1 y
⊢ IsLimit c
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e_a
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
j : Fin n.succ
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * (A (i.cycleRange⁻¹ 0) (id j) * (A.submatrix (fun x ↦ i.cycleRange⁻¹ x.succ) j.succAbove).det) =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)

Tactic:
id

Goal state after:
case e_a
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
j : Fin n.succ
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * (A (i.cycleRange⁻¹ 0) j * (A.submatrix (fun x ↦ i.cycleRange⁻¹ x.succ) j.succAbove).det) =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)
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ᵒᵖ
c : Cone F
hc : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s : Cone F
j : J
⊢ (Quiver.Hom.op ((hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s))) (𝟙 (unop s.pt))) ≫
        c.π.app j).unop =
    (s.π.app j).unop

Tactic:
by
    simpa using congr_hom ((hc s.pt.unop).fac ((yoneda.obj s.pt.unop).mapCone s) j) (𝟙 (unop s.pt))

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✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (K.map f ≫ F.preimage (l.ι.app Z ≫ i.inv)) = F.map (F.preimage (l.ι.app Y ≫ i.inv) ≫ ((const J).obj X).map f)

Tactic:
simpa [← cancel_mono i.hom] using l.w f

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
⊢ (c : Cone (F ⋙ forget MonCat)) → (t : IsLimit c) → LiftsToLimit F (forget MonCat) c t

Tactic:
intro c t

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
⊢ LiftsToLimit F (forget MonCat) c t
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ ⟨(ConcreteCategory.hom (kernel.ι f)) 0, ⋯⟩ = 0

Tactic:
refine Subtype.ext ?_
        simp only [map_zero, ZeroMemClass.coe_zero]

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 ▷ Y = 𝟙 (X ⊗ Y)

Tactic:
by intros; simp [← tensorHom_id, id_tensorHom_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
⊢ (α_ (𝟙_ C) (𝟙_ C) X).hom ▷ Y ≫ (α_ (𝟙_ C) (𝟙_ C ⊗ X) Y).hom ≫ 𝟙_ C ◁ (λ_ X).hom ▷ Y =
    (α_ (𝟙_ C ⊗ 𝟙_ C) X Y).hom ≫ (ρ_ (𝟙_ C)).hom ▷ (X ⊗ Y)

Tactic:
← associator_naturality_middle,

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
x✝² x✝¹ x✝ : D
⊢ (fData.μIso x✝² x✝¹).hom ▷ F.obj x✝ ≫ (fData.μIso (x✝² ⊗ x✝¹) x✝).hom ≫ F.map (α_ x✝² x✝¹ x✝).hom =
    (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom ≫ F.obj x✝² ◁ (fData.μIso x✝¹ x✝).hom ≫ (fData.μIso x✝² (x✝¹ ⊗ x✝)).hom

Tactic:
by simp [fData.associator_eq]

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

Goal state before:
pp: case intro
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
j : J
val✝ : Fintype J
⊢ biproduct.ι (fun j ↦ X ⊗ f j) j ≫ (leftDistributor X f).inv = X ◁ biproduct.ι f j

Tactic:
simp [leftDistributor_inv, Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp]

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
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X Y Z : C
⊢ (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)

Tactic:
associativity

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.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      μ G (F.obj x✝² ⊗ F.obj x✝¹) (F.obj x✝) ≫
        G.map (μ F x✝² x✝¹ ▷ F.obj x✝ ≫ μ F (x✝² ⊗ x✝¹) x✝ ≫ F.map (α_ x✝² x✝¹ x✝).hom) =
    μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      μ G (F.obj x✝² ⊗ F.obj x✝¹) (F.obj x✝) ≫
        G.map ((α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom ≫ F.obj x✝² ◁ μ F x✝¹ x✝ ≫ μ F x✝² (x✝¹ ⊗ x✝))

Tactic:
associativity

Goal state after: