mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂
inst✝ : IsIso (biprod.inl ≫ f.hom ≫ biprod.fst)
⊢ IsIso
    (ofComponents (biprod.inl ≫ f.hom ≫ biprod.fst) (biprod.inl ≫ f.hom ≫ biprod.snd) (biprod.inr ≫ f.hom ≫ biprod.fst)
      (biprod.inr ≫ f.hom ≫ biprod.snd))

Tactic:
simp only [Biprod.ofComponents_eq]
    infer_instance

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
c : Composition 0
⊢ c.blocks = []

Tactic:
rw [← length_eq_zero_iff, ← nonpos_iff_eq_zero]

Goal state after:
case mpr
c : Composition 0
⊢ c.blocks.length ≤ 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst = 0

Tactic:
conv_lhs =>
      slice 1 3
      rw [a₁]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ ((0 ≫ biprod.inl) ≫ inv f) ≫ biprod.fst = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
this : HasProduct fun b ↦ F.obj (f b)
that :
  piComparison F f =
    (F.mapIso (biproduct.isoProduct f)).inv ≫ F.biproductComparison f ≫ (biproduct.isoProduct (F.obj ∘ f)).hom
⊢ PreservesBiproduct f F

Tactic:
have : IsIso (biproductComparison F f) := isIso_of_mono_of_isSplitEpi _

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
this✝ : HasProduct fun b ↦ F.obj (f b)
that :
  piComparison F f =
    (F.mapIso (biproduct.isoProduct f)).inv ≫ F.biproductComparison f ≫ (biproduct.isoProduct (F.obj ∘ f)).hom
this : IsIso (F.biproductComparison f)
⊢ PreservesBiproduct f F
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ (∀ (a : α), σ a ≠ a ↔ False) ↔ σ = 1

Tactic:
iff_false,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ (∀ (a : α), ¬σ a ≠ a) ↔ σ = 1
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := ⋯
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ h.symm f ∈ map (mapRange.addEquiv e.symm).toEmbedding (s.finsuppAntidiag (e n))

Tactic:
rw [← mem_map_equiv]

Goal state after:
case mpr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := (mapRange.addEquiv e).toEquiv
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ f ∈ map h.toEmbedding (map (mapRange.addEquiv e.symm).toEmbedding (s.finsuppAntidiag (e n)))
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case h
n✝ n : ℕ
c : CompositionAsSet (n + 1)
k : Fin n
i_mem : k.castSucc.succ ∈ c.boundaries
i_ne_last : k.castSucc.succ ≠ Fin.last (n + 1)
⊢ ⟨↑k + 1, ⋯⟩ ∈ c.boundaries ∧ ↑k.castSucc.succ = ↑k + 1

Tactic:
simpa using! i_mem

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ ↑s ⊆ ↑(insert i s)

Tactic:
simp only [Finset.coe_insert, Set.subset_insert]

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = (y :: l)[n + 1]
⊢ (x :: y :: l).formPerm (x :: y :: l)[n + 1] = (x :: y :: l)[n + 1 + 1]

Tactic:
simp only [swap_apply_eq_iff, coe_mul, formPerm_cons_cons, Function.comp]

Goal state after:
case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = (y :: l)[n + 1]
⊢ (y :: l).formPerm (x :: y :: l)[n + 1] = (Equiv.swap x y) (x :: y :: l)[n + 1 + 1]
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

Tactic:
have : ¬b₁ < b₂ := hb.le.not_gt

Goal state after:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩
this : ¬b₁ < b₂
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ (swap x y).signAux = -1

Tactic:
by
    have h2n : 2 ≤ n + 2 := by exact le_add_self
    rw [← isConj_iff_eq, ← signAux_swap_zero_one h2n]
    exact (MonoidHom.mk' signAux signAux_mul).map_isConj
      (isConj_swap hxy (by exact of_decide_eq_true rfl))

Goal state after:
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f

Tactic:
have : f = 1 := Equiv.ext fun y => Classical.not_not.1 (mt (h y) List.not_mem_nil)

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
this : f = 1
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : ¬z = y
⊢ swap y z ∈ H

Tactic:
← swap_mul_swap_mul_swap h5 h6,

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : ¬z = y
⊢ swap x y * swap z x * swap x y ∈ H
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case refine_2
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ (∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)) → a ∈ s ∧ b ∈ s

Tactic:
rintro ⟨n, a, ha, ⟨⟩⟩

Goal state after:
case refine_2
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a : α
n : ℤ
ha : a ∈ s
⊢ a ∈ s ∧ (f ^ n) a ∈ s
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case refine_2
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
⊢ (∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b) → a ∈ s ∧ b ∈ s

Tactic:
· rintro ⟨n, -, a, ha, rfl, rfl⟩
    exact ⟨ha, (hf.1.iterate _).mapsTo ha⟩

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x✝ : α
hx✝ : x✝ ∈ c.support
x : α
hx : x ∈ c.support
hix : ((fun x ↦ c.subtypePermOfSupport ^ x) i) ⟨x, hx⟩ = (g.subtypePerm hc') ⟨x, hx⟩
⊢ g x = (c ^ i) x

Tactic:
simp only [← Subtype.coe_inj, subtypePermOfSupport, subtypePerm_apply,
        subtypePerm_apply_zpow_of_mem] at hix

Goal state after:
case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x✝ : α
hx✝ : x✝ ∈ c.support
x : α
hx : x ∈ c.support
hix : (c ^ i) x = g x
⊢ g x = (c ^ i) x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
⊢ ↑s ⊆ ↑(insert i s)

Tactic:
simp only [Finset.coe_insert, Set.subset_insert]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i : Fin n
inst✝ : NeZero n
x : Fin n
⊢ ↑((cycleIcc 0 i) x) = ↑(i.cycleRange x)

Tactic:
rcases lt_trichotomy x i with ch | ch | ch

Goal state after:
case inl
n : ℕ
i : Fin n
inst✝ : NeZero n
x : Fin n
ch : x < i
⊢ ↑((cycleIcc 0 i) x) = ↑(i.cycleRange x)

case inr.inl
n : ℕ
i : Fin n
inst✝ : NeZero n
x : Fin n
ch : x = i
⊢ ↑((cycleIcc 0 i) x) = ↑(i.cycleRange x)

case inr.inr
n : ℕ
i : Fin n
inst✝ : NeZero n
x : Fin n
ch : i < x
⊢ ↑((cycleIcc 0 i) x) = ↑(i.cycleRange x)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inr.inl
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch✝ : i ≤ x
ch : k < x
⊢ ↑((⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k)) x) = ↑((i.cycleIcc k) x)

Tactic:
simp [cycleIcc_of_gt (lt_of_le_of_lt hjk ch), cycleIcc_of_gt ch]

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

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

Tactic:
use g.cycleOf x, cycleOf_mem_cycleFactorsFinset_iff.mpr h

Goal state after:
case right
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ x ∈ (g.cycleOf x).support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : f x = x
⊢ (g * f⁻¹) x = x ∨ f x = x

Tactic:
exact Or.inr hx

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
m : ℕ
h : n + (m + ((σ.cycleType.erase n).erase m).sum) = 3
hm : m ∈ σ.cycleType.erase n
this : ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False
⊢ σ.IsThreeCycle

Tactic:
cases this (two_le_of_mem_cycleType (mem_of_mem_erase hm)) (two_le_of_mem_cycleType hn) h

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

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

Tactic:
rw [mul_zero]

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

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

Tactic:
rw [mul_zero]

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

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : X ∉ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → Nonempty (X ⟶ S)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (X_1 ⟶ S)

Tactic:
obtain ⟨S', w'⟩ := h

Goal state after:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (X ⟶ S')
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (X_1 ⟶ S)
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (X ⟶ S')
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (X_1 ⟶ S)

Tactic:
use max X S'

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (X ⟶ S')
⊢ ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (X_1 ⟶ max X S')
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
σ : Perm n
M : Matrix n n R
⊢ ↑↑(sign σ) * Mᵀ.det = ↑↑(sign σ) * M.det

Tactic:
det_transpose

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
σ : Perm n
M : Matrix n n R
⊢ ↑↑(sign σ) * M.det = ↑↑(sign σ) * M.det
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
α : Type u_3
inst✝³ : Monoid α
inst✝² : MulAction α R
inst✝¹ : IsScalarTower α R R
inst✝ : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ c ^ Fintype.card n • 1 * A.det = c ^ Fintype.card n • A.det

Tactic:
smul_mul_assoc,

Goal state after:
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
R : Type v
inst✝⁴ : CommRing R
α : Type u_3
inst✝³ : Monoid α
inst✝² : MulAction α R
inst✝¹ : IsScalarTower α R R
inst✝ : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ c ^ Fintype.card n • (1 * A.det) = c ^ Fintype.card n • A.det
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
inst✝ : Nontrivial n
u v : n → R
⊢ (vecMulVec u v).det = 0

Tactic:
obtain ⟨i, j, hij⟩ := exists_pair_ne n

Goal state after:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
⊢ (vecMulVec u v).det = 0
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → Nonempty (S ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (S ⟶ X_1)

Tactic:
obtain ⟨S', w'⟩ := h

Goal state after:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (S ⟶ X_1)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_1
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
B : Matrix m n R
D : Matrix n n R
⊢ ∀ a ∈ univ, a.1.sumCongr a.2 ∈ (↑(sumCongrHom m n).range).toFinset

Tactic:
intro σ₁₂

Goal state after:
case e'_3.refine_1
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
B : Matrix m n R
D : Matrix n n R
σ₁₂ : Perm m × Perm n
⊢ σ₁₂ ∈ univ → σ₁₂.1.sumCongr σ₁₂.2 ∈ (↑(sumCongrHom m n).range).toFinset
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
⊢ A.det * Dᵀ.det = A.det * D.det

Tactic:
det_transpose

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
⊢ A.det * D.det = A.det * D.det
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.submatrix (⇑i.cycleRange⁻¹) id 0 j * ((A.submatrix (⇑i.cycleRange⁻¹) id).submatrix Fin.succ j.succAbove).det) =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)

Tactic:
Matrix.submatrix_apply,

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) (id j) * ((A.submatrix (⇑i.cycleRange⁻¹) id).submatrix Fin.succ j.succAbove).det) =
    (-1) ^ ↑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✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
⊢ IsIso ((Cone.functoriality K F).map f)

Tactic:
by
          rw [this]
          infer_instance

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.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
⊢ IsIso ((Cocone.functoriality K F).map f)

Tactic:
by
          rw [this]
          infer_instance

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.IsEquivalence
⊢ IsIso h.unit

Tactic:
have := h.isEquivalence_right_of_isEquivalence_left
  infer_instance

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

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

Tactic:
by
  simp only [← tensorHom_id]
  rw [associator_naturality]
  simp

Goal state after:
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ ε (G ⋙ F) ≫ adj.counit.app (𝟙_ D) = ε (𝟭 D)

Tactic:
by
    dsimp
    rw [assoc, map_ε_comp_counit_app_unit adj, ε_η]

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

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

Tactic:
rw [associativity, Iso.inv_hom_id_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ δ F X Y ≫ T ◁ μ F X Y = 𝟙 (T ⊗ F.obj (X ⊗ Y))

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, δ_μ, MonoidalCategory.whiskerLeft_id]

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
⊢ (η (F.prod' G) ≫ ε (F.prod' G)).2 = (𝟙 ((F.prod' G).obj (𝟙_ C))).2

Tactic:
simp only [CategoryTheory.prod_comp_snd, prod'_ε_snd, prod'_η_snd, η_ε,
        prod_id, prod'_obj]

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
inst✝ : HasColimit F
j : J
⊢ (limitRightOpIsoOpColimit F).inv ≫ limit.π F.rightOp j = (colimit.ι F (op j)).op

Tactic:
simp [limitRightOpIsoOpColimit]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝¹ : PreservesLimit (cospan f g) G
inst✝ : HasPullback f g
⊢ G.map (pullback.fst f g) ≫ G.map f = G.map (pullback.snd f g) ≫ G.map g

Tactic:
by
      simp only [← G.map_comp, pullback.condition]

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

Goal state before:
pp: case e'_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X) ≫ (α_ Z Y X).hom =
    (α_ X Y Z).inv ≫
      (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom

pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).inv ≫ 𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)) ≫
      (α_ Z Y X).hom =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom

Tactic:
all_goals monoidal

Goal state after: