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

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

Tactic:
exact
        signAux_eq_signAux2 l f _ fun y (hy : f y ≠ y) =>
          List.mem_of_ne_of_mem (fun h : y = x => by simp [h, hfx.symm] at hy) (h y hy)

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

Goal state before:
pp: case intro.refine_2.inr.ha
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ (σ * τ) x ∈ ↑τ.support

Tactic:
Perm.mul_apply,

Goal state after:
case intro.refine_2.inr.ha
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ σ (τ x) ∈ ↑τ.support
Module: Mathlib.Data.Set.Pairwise.List

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
inst✝ : Std.Symm r
hl : l.Nodup
⊢ {a | a ∈ l}.Pairwise r ↔ Pairwise r l

Tactic:
by
  induction l with | nil => simp | cons a l ih => ?_
  rw [List.nodup_cons] at hl
  have : ∀ b ∈ l, ¬a = b → r a b ↔ r a b := fun b hb =>
    imp_iff_right (ne_of_mem_of_not_mem hb hl.1).symm
  simp [Set.ofPred_or, Set.pairwise_insert_of_symm, ih hl.2, and_comm, forall₂_congr this]

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

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : ℤˣ
h : a = -1
x y : α
hxy : x ≠ y
⊢ sign (swap x y) = a

Tactic:
rw [sign_swap hxy, h]

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

Goal state before:
pp: case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.negSucc a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a✝).support
⊢ f.IsCycle

Tactic:
simp only [zpow_negSucc, Perm.support_inv] at h1 h2
    exact (inv_inv (f ^ _) ▸ h1.inv).of_pow h2

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

Goal state before:
pp: α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
hx'' : x ∈ g.support
k : ℕ
hy : (f ^ k) x ∈ f.support
⊢ (g ^ k) x ∈ g.support

Tactic:
pow_apply_mem_support

Goal state after:
α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
hx'' : x ∈ g.support
k : ℕ
hy : (f ^ k) x ∈ f.support
⊢ x ∈ g.support
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case convert_4
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
f g : (i : ι) → N i
⊢ (↑Finset.univ).Pairwise fun x y ↦ Commute ((ϕ x) (g x)) ((ϕ y) (f y))

Tactic:
rintro i - j - h
      exact hcomm h _ _

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

Goal state before:
pp: α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
⊢ (f ^ Int.negSucc n) a = a ↔ ↑(#s) ∣ Int.negSucc n

Tactic:
rw [zpow_negSucc, ← inv_pow]
    exact (hf.inv.pow_apply_eq ha).trans (dvd_neg.trans Int.natCast_dvd_natCast).symm

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
P : Type u_4
inst✝ : Monoid P
f : M →* P
i j : ι
x : N i
h : ∀ (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
y : N j
⊢ Commute ((f.comp (ϕ i)) x) ((f.comp (ϕ j)) y)

Tactic:
by
        simp only [MonoidHom.coe_comp, Function.comp_apply, Commute.map (h y) f]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝ : DecidableRel f.SameCycle
hf : f.IsCycle
hx : f x ≠ x
y : α
h : f.SameCycle x y
⊢ (f.cycleOf x) y = f y

Tactic:
h.cycleOf_apply

Goal state after:
α : Type u_2
f : Perm α
x : α
inst✝ : DecidableRel f.SameCycle
hf : f.IsCycle
hx : f x ≠ x
y : α
h : f.SameCycle x y
⊢ f y = f y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i < #(f.cycleOf x).support, (f ^ i) x = y

Tactic:
rw [mem_support] at hx

Goal state after:
α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ ∃ i < #(f.cycleOf x).support, (f ^ i) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = ↑((c.subtypePerm ⋯ ^ n) ⟨x, hx⟩)

Tactic:
subtypePerm_zpow,

Goal state after:
case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = ↑(((c ^ n).subtypePerm ⋯) ⟨x, hx⟩)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg → c ^ n = ofSubtype (g.subtypePerm hg)

Tactic:
intro h; ext x
    rw [← h]
    by_cases hx : x ∈ s
    · rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx,
        subtypePerm_zpow, subtypePerm_apply]
    · rw [ofSubtype_apply_of_not_mem (subtypePerm c _ ^ n) hx,
        ← notMem_support]
      exact fun hx' ↦ hx (hc (support_zpow_le _ _ hx'))

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

Goal state before:
pp: case insert
α : 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)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ ((insert i s).noncommProd k hs'✝).cycleType = ∑ i ∈ insert i s, (k i).cycleType

Tactic:
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.sum_insert hi]

Goal state after:
case insert
α : 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)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ (k i * s.noncommProd k ⋯).cycleType = (k i).cycleType + ∑ x ∈ s, (k x).cycleType
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ IsConj σ τ

Tactic:
have hτ := card_cycleType_eq_one.2 hσ
    rw [h, card_cycleType_eq_one] at hτ
    apply hσ.isConj hτ
    rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h

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

Goal state before:
pp: case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ↑((finRotate (n + 2) * finRotate (n + 2) ^ x) 0) = ↑⟨x + 1, hx⟩

Tactic:
Perm.mul_apply,

Goal state after:
case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ↑((finRotate (n + 2)) ((finRotate (n + 2) ^ x) 0)) = ↑⟨x + 1, hx⟩
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
g : Perm α
hn2 : Fintype.card α < n + 2
hng : n ∈ g.cycleType
⊢ g.cycleType = {n}

Tactic:
obtain ⟨c, g', rfl, hd, hc, rfl⟩ := mem_cycleType_iff.1 hng

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
⊢ (c * g').cycleType = {#c.support}
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
x : α
hx : x ∈ σ.support
⊢ x ∈ l.prod.support

Tactic:
rw [mem_support] at hx

Goal state after:
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
x : α
hx : σ x ≠ x
⊢ x ∈ l.prod.support
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ ↑((j - i).castLT ⋯) < ↑(subNat (↑i) (Fin.cast ⋯ k) ⋯)

Tactic:
by simp [sub_val_of_le hij]; lia

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, τ x = l.prod x
x : α
hx : x ∈ σ.support ∩ τ.support
⊢ σ x = τ x

Tactic:
rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]

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

Goal state before:
pp: 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 := ⋯ }
k✝ k : ℕ
hk : ∀ (v : ↑(vectorsProdEqOne G p)), (σ ^ k) v = f k v
v : ↑(vectorsProdEqOne G p)
⊢ (σ ^ k * σ) v = f k.succ v

Tactic:
Perm.mul_apply,

Goal state after:
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 := ⋯ }
k✝ k : ℕ
hk : ∀ (v : ↑(vectorsProdEqOne G p)), (σ ^ k) v = f k v
v : ↑(vectorsProdEqOne G p)
⊢ (σ ^ k) (σ v) = f k.succ v
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ f⁻¹⁻¹⁻¹.IsThreeCycle → f⁻¹⁻¹.IsThreeCycle

Tactic:
apply inv

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

Goal state before:
pp: case a.neg_add_cancel
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.neg.add x) = descFunLift F s zero

Tactic:
| neg_add_cancel x =>

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

Goal state before:
pp: case neg
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
Ai_singleton : ∃ i, 1 < #(A i)
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)

Tactic:
obtain ⟨i₀, hi₀⟩ : ∃ i, 1 < #(A i) := Ai_singleton

Goal state after:
case neg
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₀)
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x + y) = descFun F s x + descFun F s y

Tactic:
by
      refine Quot.induction_on₂ x y fun a b => ?_
      dsimp [descFun]
      rw [← quot_add]
      rfl

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

Goal state before:
pp: case a.neg_add_cancel
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.neg.add x) = descFunLift F s zero

Tactic:
| neg_add_cancel x =>

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x + y) = descFun F s x + descFun F s y

Tactic:
by
      refine Quot.induction_on₂ x y fun a b => ?_
      dsimp [descFun]
      rw [← quot_add]
      rfl

Goal state after:
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
i : ι
hi : i = 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) i

Tactic:
rw [hi, update_self]

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
i : ι
hi : i = i₀
⊢ ∑ j ∈ A i₀, g i₀ j = ∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M N P : Matrix m m R
⊢ (M * (N * P)).det = (N * (M * P)).det

Tactic:
rw [← Matrix.mul_assoc, ← Matrix.mul_assoc, det_mul, det_mul_comm M N, ← det_mul]

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

Goal state before:
pp: m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (↑M * N * ↑M⁻¹).det = N.det

Tactic:
by
  rw [det_mul_right_comm, Units.mul_inv, one_mul]

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

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
⊢ A * adjp 1 A + detp (-1) A • 1 = A * adjp (-1) A + detp 1 A • 1

Tactic:
by
  ext i j
  rcases eq_or_ne i j with rfl | h <;> simp_rw [add_apply, smul_apply, smul_eq_mul]
  · simp_rw [mul_adjp_apply_eq, one_apply_eq, mul_one, add_comm]
  · simp_rw [mul_adjp_apply_ne A i j h, one_apply_ne h, mul_zero]

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

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
i j : n
hij : i ≠ j
⊢ ∀ (k : n), IsAddUnit (A i k * B k j)

Tactic:
← IsAddUnit.sum_univ_iff,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
i j : n
hij : i ≠ j
⊢ IsAddUnit (∑ a, A i a * B a j)
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
h : ∃ x, ¬1 x = (τ * σ) x
⊢ IsAddUnit ((∏ k, A k (σ k)) * ∏ k, B k (τ k))

Tactic:
Perm.mul_apply,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
h : ∃ x, ¬1 x = τ (σ x)
⊢ IsAddUnit ((∏ k, A k (σ k)) * ∏ k, B k (τ k))
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: 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 : Cone F) (y : c.pt), ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j
x : (c : Cone F) → c.pt → c✝.pt
hx :
  ∀ (c : Cone F) (y : c.pt),
    (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) (x c y) ∧
      ∀ (y_1 : c✝.pt), (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) y_1 → y_1 = x c y
c : Cone F
j : J
y : c.pt
⊢ (hom (↾x c ≫ c✝.π.app j)).toFun y = (hom (c.π.app j)).toFun y

Tactic:
exact (hx c y).1 j

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₁
inst✝¹ : Category.{w'₁, w₁} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : CreatesColimitsOfShape J F
K : J' ⥤ C
c : Cocone (K ⋙ F)
hc : IsColimit c
⊢ LiftableCocone K F c

Tactic:
by
        refine ⟨(Cocone.whiskeringEquivalence e).inverse.obj
          (liftColimit (hc.whiskerEquivalence e)), ?_⟩
        letI inner := (Cocone.whiskeringEquivalence (F := K ⋙ F) e).inverse.mapIso
          (liftedColimitMapsToOriginal (K := e.functor ⋙ K) (hc.whiskerEquivalence e))
        refine ?_ ≪≫ inner ≪≫ ((Cocone.whiskeringEquivalence e).unitIso.app c).symm
        exact Cocone.ext (Iso.refl _)

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' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ (f ⊗ₘ g) ⊗ₘ h = (α_ X Y Z).hom ≫ (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X' Y' Z').inv

Tactic:
associator_inv_naturality,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ (f ⊗ₘ g) ⊗ₘ h = (α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((f ⊗ₘ g) ⊗ₘ h)
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:
simp [fData.associator_eq]

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommSemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommSemiRingCat).sections
x✝¹ : (forget₂ CommSemiRingCat SemiRingCat).ReflectsIsomorphisms :=
  reflectsIsomorphisms_forget₂ CommSemiRingCat SemiRingCat
x✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommSemiRingCat SemiRingCat) ⋙ forget SemiRingCat).sections :=
  instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier._proof_1 F
c : Cone F :=
  { pt := of (Types.Small.limitCone (F ⋙ forget CommSemiRingCat)).pt,
    π :=
      { app := fun j ↦ ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ CommSemiRingCat SemiRingCat) j),
        naturality := ⋯ } }
c' : Cone (F ⋙ forget₂ CommSemiRingCat SemiRingCat)
t : IsLimit c'
⊢ IsLimit c

Tactic:
by
        refine IsLimit.ofFaithful (forget₂ CommSemiRingCat.{u} SemiRingCat.{u})
          (SemiRingCat.HasLimits.limitConeIsLimit.{v, u} _) (fun s => _) fun s => rfl

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 Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
    F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z

Tactic:
rw [← cancel_epi (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom, map_associator']
  simp

Goal state after: