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

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

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

Tactic:
· suffices l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1 by
      simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff, le_rfl]
    refine ⟨fun h => Or.inr h, ?_⟩
    rintro (h | h)
    · simp [← h.perm.length_eq]
    · exact h

Goal state after:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x y : α
l : List α
hl : (x :: y :: l).Nodup
⊢ (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (swap x y) y = a

Tactic:
swap_apply_def

Goal state after:
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (if y = x then y else if y = y then x else y) = a
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
⊢ (swap x ((Equiv.symm f) x)) (f⁻¹ ((Equiv.symm f) b)) ≠ (Equiv.symm f) b

Tactic:
swap_apply_def

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
⊢ (if f⁻¹ ((Equiv.symm f) b) = x then (Equiv.symm f) x
    else if f⁻¹ ((Equiv.symm f) b) = (Equiv.symm f) x then x else f⁻¹ ((Equiv.symm f) b)) ≠
    (Equiv.symm f) b
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ closure S, ∀ b ∈ closure T, _root_.Disjoint a.support b.support

Tactic:
intro a ha b hb
  have key1 := support_closure_subset_union S a ha
  have key2 := support_closure_subset_union T b hb
  have key := Set.disjoint_of_subset key1 key2
  simp_rw [Set.disjoint_iUnion_left, Set.disjoint_iUnion_right, Finset.disjoint_coe] at key
  exact key h

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = f x
⊢ f y = (swap x (f x)) y

Tactic:
by
        rw [swap_apply_of_ne_of_ne hyx hfyx]
        refine by_contradiction fun hy => ?_
        obtain ⟨j, hj⟩ := hz.2 hy
        rw [← sub_add_cancel j i, zpow_add, mul_apply, hi] at hj
        rcases zpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji | hji
        · rw [← hj, hji] at hyx
          tauto
        · rw [← hj, hji] at hfyx
          tauto

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

Tactic:
Function.Injective.eq_iff (f ^ a).injective

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
⊢ IsConj σ τ

Tactic:
refine
    isConj_of_support_equiv
      (hσ.zpowersEquivSupport.symm.trans <|
        (zpowersEquivZPowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
      ?_

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
⊢ ∀ (x : α) (hx : x ∈ ↑σ.support),
    ↑((hσ.zpowersEquivSupport.symm.trans ((zpowersEquivZPowers ⋯).trans hτ.zpowersEquivSupport)) ⟨σ x, ⋯⟩) =
      τ ↑((hσ.zpowersEquivSupport.symm.trans ((zpowersEquivZPowers ⋯).trans hτ.zpowersEquivSupport)) ⟨x, hx⟩)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : (f.cycleOf x) y ≠ y
hxy : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ (f.cycleOf x ^ i) x = y

Tactic:
cycleOf_zpow_apply_self,

Goal state after:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : (f.cycleOf x) y ≠ y
hxy : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ (f ^ i) x = y
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
e : Perm (Fin (n + 1))
p : Fin (n + 2)
⊢ (decomposeFin.symm (p, e)) 1 = (swap 0 p) (e 0).succ

Tactic:
rw [← Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ e p 0]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
⊢ ∀ {x_1 : α}, ((f.cycleOf x)⁻¹ * g) x_1 ≠ x_1 → x_1 ∈ l

Tactic:
rw [hfg hx]
            intro y hy
            exact List.mem_of_ne_of_mem
              (fun h : y = x => by
                rw [h, mul_apply, Ne, inv_eq_iff_eq, cycleOf_apply_self] at hy
                exact hy rfl)
              (hg fun h : g y = y => by
                rw [mul_apply, h, Ne, inv_eq_iff_eq, cycleOf_apply] at hy
                split_ifs at hy <;> tauto)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g) y ≠ y
⊢ f.cycleOf y = ((g.cycleOf x)⁻¹ * g).cycleOf y

Tactic:
simp [symm_apply_eq, cycleOf_apply, eq_comm (a := g y)] at hy

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ f.cycleOf y = ((g.cycleOf x)⁻¹ * g).cycleOf y
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ' ∈ τ.cycleFactorsFinset

Tactic:
rwa [Finset.mem_def]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
⊢ (1 ::ᵥ Vector.nil).head = 1 ∧ ∀ (x : List.Vector G 1), x.head = 1 → x = 1 ::ᵥ Vector.nil

Tactic:
List.Vector.head_cons,

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

Goal state before:
pp: case mpr.h₂.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ g a ∉ {g (g a)}

Tactic:
simpa using Ne.symm ha

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a = g (g a)
this : (g ^ 3) a = a
⊢ g a = a

Tactic:
by simpa [pow_succ, ← ha] using this

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

Goal state before:
pp: case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.add y) = descFunLift F s (x'.add y)

Tactic:
| add_1 x x' y r ih =>

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

Goal state before:
pp: case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.add y) = descFunLift F s (x'.add y)

Tactic:
| add_1 x x' y r ih =>

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
σ : n → n
hσ✝ : ¬Function.Injective σ
i j : n
hσ : σ i = σ j
hij : i ≠ j
k : n
⊢ σ ((swap i j) k) = σ k

Tactic:
swap_apply_def

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
σ : n → n
hσ✝ : ¬Function.Injective σ
i j : n
hσ : σ i = σ j
hij : i ≠ j
k : n
⊢ σ (if k = i then j else if k = j then i else k) = σ k
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
⊢ X.as = { as := PUnit.unit }.as

Tactic:
trivial

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ Y.as = { as := PUnit.unit }.as

Tactic:
trivial

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : D ⥤ C
R : C ⥤ D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ (h.homEquiv X (coeq (L.map f) (L.map g))) (L.map f ≫ coeqHom (L.map f) (L.map g)) =
    (h.homEquiv X (coeq (L.map f) (L.map g))) (L.map g ≫ coeqHom (L.map f) (L.map g))

Tactic:
coeq_condition

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : D ⥤ C
R : C ⥤ D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ (h.homEquiv X (coeq (L.map f) (L.map g))) (L.map g ≫ coeqHom (L.map f) (L.map g)) =
    (h.homEquiv X (coeq (L.map f) (L.map g))) (L.map g ≫ coeqHom (L.map f) (L.map g))
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 N : Matrix n n R
σ : Perm n
x✝ : σ ∈ univ
τ : Perm n
⊢ (∏ i, N (σ i) i) * ↑↑(sign τ) * ∏ j, M (τ j) (σ j) =
    (∏ i, N (σ i) i) * (↑↑(sign σ) * ↑↑(sign ((Equiv.mulRight σ⁻¹) τ))) * ∏ i, M (((Equiv.mulRight σ⁻¹) τ) i) i

Tactic:
have : (∏ j, M (τ j) (σ j)) = ∏ j, M ((τ * σ⁻¹) j) j := by
            rw [← (σ⁻¹ : _ ≃ _).prod_comp]
            simp

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
σ : Perm n
x✝ : σ ∈ univ
τ : Perm n
this : ∏ j, M (τ j) (σ j) = ∏ j, M ((τ * σ⁻¹) j) j
⊢ (∏ i, N (σ i) i) * ↑↑(sign τ) * ∏ j, M (τ j) (σ j) =
    (∏ i, N (σ i) i) * (↑↑(sign σ) * ↑↑(sign ((Equiv.mulRight σ⁻¹) τ))) * ∏ i, M (((Equiv.mulRight σ⁻¹) τ) i) i
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
mf' : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
⊢ X = X ∧ Y = Y

Tactic:
trivial

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
i j : n
h : i ≠ j
⊢ (A * adjp 1 A) i j = (A * adjp (-1) A) i j

Tactic:
by
  let A' : Matrix n n R := A.updateRow j (A i)
  have h' s : (A * adjp s A) i j = (A' * adjp s A') j j := sum_congr rfl fun _ _ ↦
    congr_arg₂ (· * ·) (by simp [A']) <| sum_congr rfl fun σ hσ ↦ prod_congr rfl fun _ _ ↦ by aesop
  simp_rw [h', mul_adjp_apply_eq]
  apply detp_eq_of_row_eq h
  simp [A', Matrix.row_apply', h]

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

Goal state before:
pp: case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
h : k ≠ j
⊢ (M.updateRow j (a • M j + ∑ x ∈ s✝, c x • M x)).det + c k * (M.updateRow j (M k)).det = a • M.det

Tactic:
det_updateRow_eq_zero h,

Goal state after:
case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
h : k ≠ j
⊢ (M.updateRow j (a • M j + ∑ x ∈ s✝, c x • M x)).det + c k * 0 = a • M.det
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ Y : Discrete PUnit.{u_1 + 1}
⊢ { as := PUnit.unit }.as = x✝.as

Tactic:
trivial

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ { as := PUnit.unit }.as = X.as

Tactic:
trivial

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → T' mX ≫ f = T' mY
mf' : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
⊢ X = X ∧ Y = Y

Tactic:
trivial

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
inst✝ : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
⊢ (equivShrink F.ColimitType) (F.ιColimitType i xi) = (equivShrink F.ColimitType) (F.ιColimitType j xj) ↔
    FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩

Tactic:
← (equivShrink _).symm.injective.eq_iff,

Goal state after:
J : Type v
inst✝² : Category.{w, v} J
F : J ⥤ Type u
inst✝¹ : IsFilteredOrEmpty J
inst✝ : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
⊢ (equivShrink F.ColimitType).symm ((equivShrink F.ColimitType) (F.ιColimitType i xi)) =
      (equivShrink F.ColimitType).symm ((equivShrink F.ColimitType) (F.ιColimitType j xj)) ↔
    FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
x : (i : ι) → M₁ i
i : ι
v : M₁ i
⊢ f (update x i v) = f x - f (update x i (x i - v))

Tactic:
rw [map_update_sub, update_eq_self, sub_sub_cancel]

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

Goal state before:
pp: C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F₁ F₂ : C × D ⥤ E
h : curry.obj F₁ = curry.obj F₂
⊢ F₁ = F₂

Tactic:
rw [← uncurry_obj_curry_obj F₁, ← uncurry_obj_curry_obj F₂, h]

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

Goal state before:
pp: case refine_3
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✝⁷ : Ring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M'
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x✝¹ : M₂
x✝ : x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
x : (i : ι) → M₁ i
hx : x ∈ {v | ∀ (i : ι), v i ∈ p i}
hf : f x = x✝¹
i : ι
this : DecidableEq ι := Classical.decEq ι
⊢ f (update x i (c • x i)) = c • f x

Tactic:
· rw [f.map_update_smul, update_eq_self]

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ Cᵒᵖ
X : C
s : ↑(F ⋙ yoneda.obj X).sections
j j' : J
f : j ⟶ j'
⊢ ((const J).obj (op X)).map f ≫ Quiver.Hom.op (↑s j') = Quiver.Hom.op (↑s j) ≫ F.map f

Tactic:
by
        dsimp
        rw [Category.id_comp]
        exact Quiver.Hom.unop_inj (s.property f).symm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
Y : C
⊢ ((colimitCocone X).ι.app Y ≫ ↾fun x ↦ (hom (s.ι.app (unop X))) (𝟙 (unop X))) = s.ι.app Y

Tactic:
by
    ext f
    simpa using congr_hom (s.w f).symm (𝟙 (unop X))

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), (colimitCocone X).ι.app j ≫ m = s.ι.app j
⊢ (hom m).toFun PUnit.unit = (hom (↾fun x ↦ (hom (s.ι.app (unop X))) (𝟙 (unop X)))).toFun PUnit.unit

Tactic:
simp [← w]

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
⊢ ∀ (c_1 : R) (x : ↑(((Functor.const J).obj c.pt).obj j)),
    ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) c_1 * x =
      x * ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) c_1

Tactic:
intro r x

Goal state after:
R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
r : R
x : ↑(((Functor.const J).obj c.pt).obj j)
⊢ ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) r * x =
    x * ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) r
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: case refine_2
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
⊢ ∀ (m : R) (x : ↑s.1),
    {
            toFun :=
              ⇑(ConcreteCategory.hom
                  ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s))),
            map_add' := ⋯ }.toFun
        (m • x) =
      (RingHom.id R) m •
        {
              toFun :=
                ⇑(ConcreteCategory.hom
                    ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift
                      ((forget (ModuleCat R)).mapCone s))),
              map_add' := ⋯ }.toFun
          x

Tactic:
intro r x

Goal state after:
case refine_2
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
r : R
x : ↑s.1
⊢ {
          toFun :=
            ⇑(ConcreteCategory.hom
                ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s))),
          map_add' := ⋯ }.toFun
      (r • x) =
    (RingHom.id R) r •
      {
            toFun :=
              ⇑(ConcreteCategory.hom
                  ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s))),
            map_add' := ⋯ }.toFun
        x
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
⊢ Linear R G

Tactic:
by
  refine ⟨fun {X Y} f r ↦ ?_⟩
  obtain ⟨X', Y', eX, eY, f', rfl⟩ :
      ∃ (X' Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y)
        (f' : X' ⟶ Y'), f = eX.inv ≫ F.map f' ≫ eY.hom := by
    obtain ⟨f', hf'⟩ :=
      F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
    exact ⟨_, _, F.objObjPreimageIso X, F.objObjPreimageIso Y, f', by cat_disch⟩
  simpa only [comp_map, map_smul, Linear.smul_comp, Linear.comp_smul, ← G.map_comp]
    using G.map eX.inv ≫= ((F ⋙ G).map_smul r f') =≫ G.map eY.hom

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ (μ G (F.obj x✝²) (F.obj x✝¹) ≫ G.map (μ F x✝² x✝¹)) ▷ G.obj (F.obj x✝) ≫
      (μ G (F.obj (x✝² ⊗ x✝¹)) (F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝)) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      G.obj (F.obj x✝²) ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))

Tactic:
simp_rw [comp_whiskerRight, assoc, μ_natural_left_assoc, MonoidalCategory.whiskerLeft_comp,
      assoc, μ_natural_right_assoc, ← associativity_assoc, ← G.map_comp, associativity]

Goal state after: