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

Goal state before:
pp: case intro.refine_2.inl
α : 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
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))

Tactic:
rw [Set.union_apply_left, Set.union_apply_left]

Goal state after:
case intro.refine_2.inl
α : 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
⊢ ↑((Set.union hd2'').symm
        (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inl ⟨↑⟨(σ * τ) x, ⋯⟩, ?intro.refine_2.inl.ha✝⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm
          (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inl ⟨↑⟨x, ⋯⟩, ?intro.refine_2.inl.ha⟩)))

case intro.refine_2.inl.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

case intro.refine_2.inl.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.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
⊢ (permsOfList (a :: l)).Nodup

Tactic:
by
    have hl' : l.Nodup := hl.of_cons
    have hln' : (permsOfList l).Nodup := nodup_permsOfList hl'
    have hmeml : ∀ {f : Perm α}, f ∈ permsOfList l → f a = a := fun {f} hf =>
      not_not.1 (mt (mem_of_mem_permsOfList hf) (nodup_cons.1 hl).1)
    rw [permsOfList, List.nodup_append', List.nodup_flatMap, pairwise_iff_getElem]
    refine ⟨?_, ⟨⟨?_,?_ ⟩, ?_⟩⟩
    · exact hln'
    · exact fun _ _ => hln'.map fun _ _ => mul_left_cancel
    · intro i j hi hj hij x hx₁ hx₂
      let ⟨f, hf⟩ := List.mem_map.1 hx₁
      let ⟨g, hg⟩ := List.mem_map.1 hx₂
      have hix : x a = l[i] := by
        rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
      have hiy : x a = l[j] := by
        rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
      have hieqj : i = j := hl'.getElem_inj_iff.1 (hix.symm.trans hiy)
      exact absurd hieqj (_root_.ne_of_lt hij)
    · intro f hf₁ hf₂
      let ⟨x, hx, hx'⟩ := List.mem_flatMap.1 hf₂
      let ⟨g, hg⟩ := List.mem_map.1 hx'
      obtain rfl : g.symm x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
      have hxa : x ≠ g.symm x := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)
      exact (List.nodup_cons.1 hl).1 <| mem_of_mem_permsOfList hg.1 (by simpa using hxa)

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

Goal state before:
pp: case cons.cons.cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' y' : α
l' : List α
hl' : (x' :: y' :: l').Nodup
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔
    x :: y :: l ~r x' :: y' :: l' ∨ (x :: y :: l).length ≤ 1 ∧ (x' :: y' :: l').length ≤ 1

Tactic:
simp [-formPerm_cons_cons, formPerm_ext_iff hl hl']

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
⊢ _root_.Disjoint (ofSubtype x).support σ.support

Tactic:
by
  rw [Finset.disjoint_iff_ne]
  rintro a ha b hb rfl
  rw [mem_support] at ha hb
  exact ha (ofSubtype_apply_of_not_mem x (mt Function.mem_fixedPoints_iff.mp hb))

Goal state after:
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: ι : Type u_1
x : ℕ
t : Finset ι
s : ι → ℕ
⊢ x.Coprime (∏ i ∈ t, s i) ↔ ∀ i ∈ t, x.Coprime (s i)

Tactic:
simpa using coprime_multiset_prod_right_iff (m := t.val.map s)

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ ((f ^ n) ^ m).IsCycle

Tactic:
rwa [hm]

Goal state after:
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
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
· have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
        simp only [zpow_one, zpow_natCast] at h
        rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
        contradiction

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

Goal state before:
pp: α : Type u_2
f : Perm α
⊢ f.IsCycle ↔ ∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s

Tactic:
refine ⟨fun hf => ⟨{ x | f x ≠ x }, ?_, hf.isCycleOn, fun _ => id⟩, ?_⟩
  · obtain ⟨a, ha⟩ := hf
    exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩
  · rintro ⟨s, hs, hf, hsf⟩
    obtain ⟨a, ha⟩ := hs.nonempty
    exact ⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ sign (prodCongrRight σ) = ∏ k, sign (σ k)

Tactic:
obtain ⟨l, hl, mem_l⟩ := Finite.exists_univ_list α
  have l_to_finset : l.toFinset = Finset.univ := by
    apply eq_top_iff.mpr
    intro b _
    exact List.mem_toFinset.mpr (mem_l b)
  rw [← prod_prodExtendRight σ hl mem_l, map_list_prod sign, List.map_map, ← l_to_finset,
    List.prod_toFinset _ hl]
  simp_rw [← fun a => sign_prodExtendRight a (σ a), Function.comp_def]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, σ.cycleFactorsFinset = {a_1} ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle

Tactic:
cycleFactorsFinset_eq_singleton_iff

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype ↥(H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j))
⊢ iSupIndep H

Tactic:
simpa using
    MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype)
      (commute_subtype_of_commute hcomm) hcoprime

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

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
⊢ j.cycleRange i = if i = j then 0 else i + 1

Tactic:
have iin : i ∈ Set.range (castLEEmb (n := j + 1) (by lia)) := by
    simp; lia
  have : (castLEEmb (by lia)).toEquivRange (castLT i (by lia)) = ⟨i, iin⟩ := by
    simp [coe_castLEEmb]; rfl
  rw [cycleRange,
    (finRotate (j + 1)).extendDomain_apply_subtype (castLEEmb (by lia)).toEquivRange iin,
    Function.Embedding.toEquivRange_apply]
  split_ifs with ch
  · have : ((castLEEmb (by lia)).toEquivRange.symm ⟨i, iin⟩) = last j := by
      simpa only [coe_castLEEmb, ← this, symm_apply_apply] using eq_of_val_eq (by simp [ch])
    rw [this, finRotate_last]
    rfl
  · have hj1 : (i + 1).1 = i.1 + 1 := val_add_one_of_lt' (by lia)
    have hj2 : (i.castLT (by lia) + 1 : Fin (j + 1)).1 =
      (i.castLT (by lia) : Fin (j + 1)) + 1 := val_add_one_of_lt' (by simp; lia)
    exact eq_of_val_eq (by simp [← this, hj1, hj2])

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
h : IsConj σ (π * σ * π⁻¹)
⊢ σ.cycleType = (π * σ * π⁻¹).cycleType

Tactic:
cycleType_conj

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
h : IsConj σ (π * σ * π⁻¹)
⊢ σ.cycleType = σ.cycleType
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
⊢ ∃ x, orderOf x = p

Tactic:
have hf1 : ∀ v, f 0 v = v := VectorsProdEqOne.rotate_zero

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
⊢ ∃ x, orderOf x = p
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f✝ f' : M [⋀^ι]→ₗ[R] N
g✝ g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
f g : M [⋀^ι]→ₗ[R] N
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨⟨_, _, _⟩, _⟩
    rcases g with ⟨⟨_, _, _⟩, _⟩
    congr

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
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₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i ≃ₗ[R] M₁' i
⊢ (g.compLinearMap fun i ↦ ↑(f i)) = 0 ↔ g = 0

Tactic:
by
  set f' := fun i => (f i : M₁ i →ₗ[R] M₁' i)
  rw [← zero_compLinearMap f', compLinearMap_inj f' fun i => (f i).surjective]

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
⊢ ∏ i, 1 = 1

Tactic:
prod_const_one

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ 1 = 1
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
d : n → R
σ : Perm n
hσ : σ ∈ ofSign (-1)
⊢ ∏ k, diagonal d k (σ k) = 0

Tactic:
have hσ1 : σ ≠ 1 := by
    contrapose hσ
    rw [hσ, mem_ofSign, sign_one]
    decide

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
σ : Perm n
hσ : σ ∈ ofSign (-1)
hσ1 : σ ≠ 1
⊢ ∏ k, diagonal d k (σ k) = 0
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
rw [add_zero]

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

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

Tactic:
rw [add_zero]

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
inst✝ : IsDomain R
A : Matrix m m R
hA : A.det ≠ 0
⊢ LinearIndependent R fun i ↦ A i

Tactic:
contrapose hA
  exact det_eq_zero_of_not_linearIndependent_rows hA

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ⊇ x2) ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, ij⟩)
        ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) z) ∧
      (fun x1 x2 ↦ x1 ⊇ x2) ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k, kj⟩)
        ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) z)

Tactic:
let ⟨l, li, lk, e⟩ := cospan ij kj

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ⊇ x2) ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, ij⟩)
        ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) z) ∧
      (fun x1 x2 ↦ x1 ⊇ x2) ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k, kj⟩)
        ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) z)
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
y : F.ColimitType
⊢ hc.down.desc F.coconeTypes (F.descColimitType c y) = y

Tactic:
by
          obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y
          simp

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : ↑(R F)
⊢ x * 0 = 0

Tactic:
by
      refine Quot.inductionOn x ?_; clear x; intro x
      obtain ⟨j, x⟩ := x
      erw [colimit_zero_eq _ j, colimit_mul_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]
      rw [CategoryTheory.Functor.map_id]
      dsimp
      rw [mul_zero x]
      rfl

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
⊢ ∑ σ ∈ Finset.map decomposeFin.symm.toEmbedding univ, sign σ • ∏ i, A (σ i) i =
    ∑ i, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det

Tactic:
← Finset.univ_product_univ

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ ∑ σ ∈ Finset.map decomposeFin.symm.toEmbedding (univ ×ˢ univ), sign σ • ∏ i, A (σ i) i =
    ∑ i, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det
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 : ι) → 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
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₂ : ¬k = i
h₁ : (i = k ∨ i ∈ s) ∧ k ≤ i
⊢ s.piecewise b a i = b i

Tactic:
s.piecewise_eq_of_mem _ _ (h₁.1.resolve_left <| Ne.symm h₂)

Goal state after:
case neg
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
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₂ : ¬k = i
h₁ : (i = k ∨ i ∈ s) ∧ k ≤ i
⊢ b i = b i
Module: Mathlib.CategoryTheory.Limits.Preserves.Limits

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (X✝ ⋙ G) j ≫ (preservesColimitIso G X✝).inv ≫ G.map (colimMap f) =
    colimit.ι (X✝ ⋙ G) j ≫ colimMap (Functor.whiskerRight f G) ≫ (preservesColimitIso G Y✝).inv

Tactic:
rw [ι_colimMap_assoc]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (X✝ ⋙ G) j ≫ (preservesColimitIso G X✝).inv ≫ G.map (colimMap f) =
    (Functor.whiskerRight f G).app j ≫ colimit.ι (Y✝ ⋙ G) j ≫ (preservesColimitIso G Y✝).inv
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
⊢ ∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
    (shrinkYoneda.{v, v, u}.obj X).map f ≫ shrinkYonedaObjObjEquiv.toIso.hom =
      shrinkYonedaObjObjEquiv.toIso.hom ≫ (yoneda.obj X).map f

Tactic:
intros; ext; simp [shrinkYonedaObjObjEquiv_obj_map]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    shrinkCoyoneda.{v, v, u}.map f ≫ (NatIso.ofComponents (fun Y_1 ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun Y ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom ≫ coyoneda.map f

Tactic:
intros; ext; simp [shrinkYonedaObjObjEquiv_obj_map]

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
G₁ G₂ : D ⥤ E
inst✝² : G₁.LaxMonoidal
inst✝¹ : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst✝ : IsMonoidal τ'
⊢ IsMonoidal (F₁.whiskerLeft τ')

Tactic:
← Functor.id_hcomp

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
G₁ G₂ : D ⥤ E
inst✝² : G₁.LaxMonoidal
inst✝¹ : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst✝ : IsMonoidal τ'
⊢ IsMonoidal (𝟙 F₁ ◫ τ')
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x✝ : W.ContainsIdentities
⊢ identities C ≤ W

Tactic:
intro _ _ _ ⟨_⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x✝ : W.ContainsIdentities
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ W (𝟙 X✝)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case e_a
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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ⊗ₘ 𝟙 (G.obj Z)) ≫
      (α_ (F.obj X) (F.obj Y) (G.obj Z)).hom ≫
        F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫ F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫ (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z)

Tactic:
associator_naturality_assoc

Goal state after:
case e_a
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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      (i.inv.app X ⊗ₘ i.inv.app Y ⊗ₘ 𝟙 (G.obj Z)) ≫
        F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫ F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫ (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a ∈
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom).ker

Tactic:
SetLike.mem_coe,

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a ∈
    (DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom).ker
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot (F ⋙ uliftFunctor)
j : J
a : ↑((F ⋙ uliftFunctor).obj j)
⊢ (quotToQuotUlift F) ((Quot.ι F j) a.down) = (Quot.ι (F ⋙ uliftFunctor) j) a

Tactic:
quotToQuotUlift_ι

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot (F ⋙ uliftFunctor)
j : J
a : ↑((F ⋙ uliftFunctor).obj j)
⊢ (Quot.ι (F ⋙ uliftFunctor) j) { down := a.down } = (Quot.ι (F ⋙ uliftFunctor) j) a
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
⊢ { toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction f,
          invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction f, left_inv := ⋯, right_inv := ⋯ }.symm
      g =
    (restrictScalars f).map g ≫ (RestrictionCoextensionAdj.counit' f).app Y

Tactic:
by
      ext
      simp [RestrictionCoextensionAdj.counit']

Goal state after: