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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime #σ.support
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
⊢ closure {σ, swap x ((σ ^ n) x)} = ⊤

Tactic:
← h1.orderOf

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
⊢ closure {σ, swap x ((σ ^ n) x)} = ⊤
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ sign l.prod = (-1) ^ l.length

Tactic:
have h₁ : l.map sign = List.replicate l.length (-1) :=
    List.eq_replicate_iff.2
      ⟨by simp, fun u hu =>
        let ⟨g, hg⟩ := List.mem_map.1 hu
        hg.2 ▸ (hl _ hg.1).sign_eq⟩
  rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]

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

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

Tactic:
exact (support_pow_le _ n).antisymm h2

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ (orderOf f).Coprime n

Tactic:
rw [Nat.Prime.coprime_iff_not_dvd hf']

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ ¬orderOf f ∣ n
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
f : (i : ι) → H i
⊢ f ∈ (noncommPiCoprod ϕ hcomm).ker → f ∈ ⊥

Tactic:
heq1

Goal state after:
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ (noncommPiCoprod ϕ hcomm).ker
⊢ f ∈ ⊥
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a, σ.cycleType = {a}) ↔ σ.IsCycle

Tactic:
simp_rw [cycleType_def, Multiset.map_eq_singleton, ← Finset.singleton_val, Finset.val_inj,
    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: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
⊢ f = 1

Tactic:
rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]

Goal state after:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
⊢ orderOf f ∣ 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: 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

Tactic:
exact ha

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝ : Option α × Perm α
x : Option α
σ : Perm α
⊢ (fun σ ↦ (σ none, removeNone σ)) ((fun i ↦ swap none i.1 * optionCongr i.2) (x, σ)) = (x, σ)

Tactic:
have : removeNone (swap none x * σ.optionCongr) = σ :=
      Equiv.optionCongr_injective (by simp [← mul_assoc])
    simp [this]

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)
⊢ (k i * s.noncommProd k ⋯).cycleType = (k i).cycleType + ∑ x ∈ s, (k x).cycleType

Tactic:
Disjoint.cycleType_mul,

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).cycleType + (s.noncommProd k ⋯).cycleType = (k i).cycleType + ∑ x ∈ s, (k x).cycleType

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).Disjoint (s.noncommProd k ⋯)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0 : ¬m = 0
⊢ ¬g ^ m = 1

Tactic:
exact pow_ne_one_of_lt_orderOf hm0 div_euc.2

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (-(-1) ^ n) ^ σ.cycleType.card =
    if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)

Tactic:
if_neg (Nat.not_odd_iff_even.mpr h),

Goal state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (-(-1) ^ n) ^ σ.cycleType.card = (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
x : α
hx : x ∈ p.support
⊢ x ∈ f.support

Tactic:
rwa [mem_support, ← h.right x hx, ← mem_support]

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁶ : Finite ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : AddCommMonoid N
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) = g.compLinearMap fun i ↦ DFinsupp.lsingle (p i)
⊢ f = g

Tactic:
by
  ext x
  change f (fun i ↦ x i) = g (fun i ↦ x i)
  classical
  cases nonempty_fintype ι
  rw [funext (fun i ↦ Eq.symm (DFinsupp.sum_single (f := x i)))]
  simp_rw [DFinsupp.sum, MultilinearMap.map_sum_finset]
  congr! 1 with p
  simp_rw [MultilinearMap.ext_iff] at h
  exact h _ _

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

Goal state before:
pp: ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : g i • f (update v i (v i)) = 0
⊢ f v = 0

Tactic:
Function.update_eq_self,

Goal state after:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : g i • f v = 0
⊢ f v = 0
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 σ • detRowAlternating M = ↑↑(sign σ) * M.det

Tactic:
by simp [Units.smul_def, det]

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

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ ((s • M)ᵀ.updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det

Tactic:
transpose_smul,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ ((s • Mᵀ).updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := ⋯
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) := ⋯
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ ⟨F.obj j, ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩⟩ ∈ H

Tactic:
simp only [O, H, Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image,
    PSigma.mk.injEq, true_and, exists_and_left]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ ∃ a, F.obj a = F.obj j ∧ ∃ x x_1, ⟨F.obj x, ⟨⋯, ⟨⋯, F.map x_1⟩⟩⟩ ≍ ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩
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
G : J ⥤ Type w₀'
app : (j : J) → G.obj j → F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), app j' ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ app j
j✝ j'✝ : J
f : j✝ ⟶ j'✝
⊢ (c.ι j'✝ ∘ app j'✝) ∘ ⇑(ConcreteCategory.hom (G.map f)) = c.ι j✝ ∘ app j✝

Tactic:
rw [Function.comp_assoc, naturality, ← Function.comp_assoc, ι_naturality]

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ ∀ (a b : (j : J) × F.obj j),
    F.ColimitTypeRel a b →
      (match a with
        | ⟨j, x⟩ => c.ι j x) =
        match b with
        | ⟨j, x⟩ => c.ι j x

Tactic:
rintro _ _ ⟨_, _⟩; aesop

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : (hom (F.map f')) y.snd = (hom (F.map g')) z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ (hom (F.map ((g ≫ fl) ≫ n))) y.snd = (hom (F.map ((f' ≫ gl) ≫ n))) y.snd

Tactic:
rw [hn]

Goal state after:
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✝⁹ : 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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
⊢ ∀ (m : (i : { a // ¬P a }) → M₁ ↑i) (i : { a // ¬P a }) (x y : M₁ ↑i),
    f.domDomRestrict P (update m i (x + y)) = f.domDomRestrict P (update m i x) + f.domDomRestrict P (update m i y)

Tactic:
m

Goal state after:
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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
⊢ ∀ (i : { a // ¬P a }) (x y : M₁ ↑i),
    f.domDomRestrict P (update m i (x + y)) = f.domDomRestrict P (update m i x) + f.domDomRestrict P (update m i y)
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✝⁹ : 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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
⊢ ∀ (m : (i : { a // ¬P a }) → M₁ ↑i) (i : { a // ¬P a }) (c : R) (x : M₁ ↑i),
    f.domDomRestrict P (update m i (c • x)) = c • f.domDomRestrict P (update m i x)

Tactic:
m

Goal state after:
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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
⊢ ∀ (i : { a // ¬P a }) (c : R) (x : M₁ ↑i),
    f.domDomRestrict P (update m i (c • x)) = c • f.domDomRestrict P (update m i x)
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y y' : (j : J) × ↑(F.obj j)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) y y'
⊢ colimitMulAux F x y = colimitMulAux F x y'

Tactic:
by
  obtain ⟨j₁, y⟩ := y; obtain ⟨j₂, x⟩ := x; obtain ⟨j₃, y'⟩ := y'
  obtain ⟨l, f, g, hfg⟩ := hyy'
  simp only [Functor.comp_obj, Functor.comp_map, ConcreteCategory.hom_ofHom,
    TypeCat.Fun.coe_mk] at hfg
  obtain ⟨s, α, β, γ, h₁, h₂, h₃⟩ :=
    IsFiltered.tulip (IsFiltered.rightToMax j₂ j₁) (IsFiltered.leftToMax j₂ j₁)
      (IsFiltered.leftToMax j₂ j₃) (IsFiltered.rightToMax j₂ j₃) f g
  apply M.mk_eq
  use s, α, γ
  simp_rw [map_mul, ← comp_apply, ← F.map_comp, h₁, h₂, h₃, F.map_comp,
    comp_apply, hfg]

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
⊢ IsColimit d

Tactic:
have : (Cocone.functoriality K F).map f = i.hom :=
          (hd.ofIsoColimit i.symm).uniq_cocone_morphism

Goal state after:
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
⊢ IsColimit d
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
P : C ⥤ Type w
t : P.obj X
⊢ shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) t)) =
    shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f.op ≫ shrinkCoyonedaEquiv.symm t)

Tactic:
by
    obtain ⟨t, rfl⟩ := shrinkCoyonedaEquiv.surjective t
    rw [← shrinkCoyonedaEquiv_naturality]
    simp

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

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ (kernelIsoKer f).inv ≫ kernel.ι f = ofHom (Hom.hom f).ker.subtype

Tactic:
simp [kernelIsoKer]

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
X Y : C
⊢ μ (𝟭 C) X Y ≫ adj.unit.app (X ⊗ Y) = (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ (F ⋙ G) X Y

Tactic:
dsimp
    rw [← unit_app_tensor_comp_map_δ_assoc, id_comp, Monoidal.map_δ_μ, comp_id]

Goal state after:
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
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂),
    e.inverse.map (X ◁ f) =
      (e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj Y₁)).inv ≫
        e.inverse.obj X ◁ e.inverse.map f ≫ (e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj Y₂)).hom

Tactic:
by simp +zetaDelta +instances

Goal state after:
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
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D),
    e.inverse.map (f ▷ Y) =
      (e.unitIso.app (e.inverse.obj X₁ ⊗ e.inverse.obj Y)).inv ≫
        e.inverse.map f ▷ e.inverse.obj Y ≫ (e.unitIso.app (e.inverse.obj X₂ ⊗ e.inverse.obj Y)).hom

Tactic:
by simp +zetaDelta +instances

Goal state after:
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
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    e.inverse.map (f ⊗ₘ g) =
      (e.unitIso.app (e.inverse.obj X₁ ⊗ e.inverse.obj X₂)).inv ≫
        (e.inverse.map f ⊗ₘ e.inverse.map g) ≫ (e.unitIso.app (e.inverse.obj Y₁ ⊗ e.inverse.obj Y₂)).hom

Tactic:
by simp +zetaDelta +instances

Goal state after:
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
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X Y Z : D),
    e.inverse.map (α_ X Y Z).hom =
      (((e.unitIso.app (e.inverse.obj (X ⊗ Y) ⊗ e.inverse.obj Z)).symm ≪≫
            ((e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj Y)).symm ⊗ᵢ Iso.refl (e.inverse.obj Z))) ≪≫
          α_ (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫
            (Iso.refl (e.inverse.obj X) ⊗ᵢ e.unitIso.app (e.inverse.obj Y ⊗ e.inverse.obj Z)) ≪≫
              e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj (Y ⊗ Z))).hom

Tactic:
by simp +zetaDelta +instances

Goal state after:
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
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X : D),
    e.inverse.map (λ_ X).hom =
      (((e.unitIso.app (e.inverse.obj (𝟙_ D) ⊗ e.inverse.obj X)).symm ≪≫
            ((e.unitIso.app (𝟙_ C)).symm ⊗ᵢ Iso.refl (e.inverse.obj X))) ≪≫
          λ_ (e.inverse.obj X)).hom

Tactic:
by simp +zetaDelta +instances

Goal state after:
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
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X : D),
    e.inverse.map (ρ_ X).hom =
      (((e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj (𝟙_ D))).symm ≪≫
            (Iso.refl (e.inverse.obj X) ⊗ᵢ (e.unitIso.app (𝟙_ C)).symm)) ≪≫
          ρ_ (e.inverse.obj X)).hom

Tactic:
by simp +zetaDelta +instances

Goal state after: