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

Goal state before:
pp: case comm.a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
a : ↥f.cycleFactorsFinset
a✝¹ : a ∈ ↑univ
b : ↥f.cycleFactorsFinset
a✝ : b ∈ ↑univ
h : a ≠ b
⊢ (fun i ↦ ((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) i) (v i)) b ∈ Subgroup.zpowers ↑b

Tactic:
simp only [Subgroup.coe_subtype, SetLike.coe_mem]

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✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
f : ((i : ι) → M₁ i) → M₂
h₁ : ∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), f (update m i (x + y)) = f (update m i x) + f (update m i y)
h₂ : ∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (update m i (c • x)) = c • f (update m i x)
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update m i (c • x)) = c • f (update m i x)

Tactic:
convert! h₂ m i c x

Goal state after:
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 : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
⊢ f ((insert i t).piecewise (m + m') m') = ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')

Tactic:
A,

Goal state after:
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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
⊢ f (update (t.piecewise (m + m') m') i (m i + m' i)) = ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ IsFiltered α

Tactic:
by infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderTop α
⊢ IsFiltered α

Tactic:
by infer_instance

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:
det_updateRow_smul_left

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 ^ (Fintype.card n - 1) * (Mᵀ.updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det
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 : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ∈ (σ * τ).support
hl2 : l ≠ τ⁻¹ j
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
rw [mem_support, ne_comm] at hl1

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 : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ≠ (σ * τ) l
hl2 : l ≠ τ⁻¹ j
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
⊢ IsCofiltered α

Tactic:
by infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ IsCofiltered α

Tactic:
by infer_instance

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
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
⊢ f = g

Tactic:
by
    suffices Equiv.ulift.{w₃}.invFun.comp f =
        Equiv.ulift.invFun.comp g by
      ext x
      simpa using congr_fun this x
    exact hc.funext (fun j ↦ by simp [Function.comp_assoc, h])

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
hc : c.IsColimitCore
j : J
⊢ (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = id ∘ c.ι j

Tactic:
by
              rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι]

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✝¹⁰ : Semiring R
inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
⊢ domDomCongr σ.symm (domDomCongr σ m) = m

Tactic:
ext
    simp [domDomCongr]

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✝¹⁰ : Semiring R
inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
⊢ domDomCongr σ (domDomCongr σ.symm m) = m

Tactic:
ext
    simp [domDomCongr]

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✝¹⁰ : Semiring R
inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
a b : MultilinearMap R (fun x ↦ M₂) M₃
⊢ domDomCongr σ (a + b) = domDomCongr σ a + domDomCongr σ b

Tactic:
ext
    simp [domDomCongr]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x : (j : J) × ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j
⊢ (Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel x)⁻¹ *
      Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel x =
    1

Tactic:
change (G.mk _ _)⁻¹ * G.mk _ _ = _

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x : (j : J) × ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j
⊢ (G.mk F x)⁻¹ * G.mk F x = 1
Module: Mathlib.Algebra.Category.Grp.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x : (j : J) × ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j
⊢ (G.mk F x)⁻¹ * G.mk F x = 1

Tactic:
obtain ⟨j, x⟩ := x

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
j : J
x : ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j
⊢ (G.mk F ⟨j, x⟩)⁻¹ * G.mk F ⟨j, x⟩ = 1
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ 0 * Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x = 0

Tactic:
obtain ⟨j, x⟩ := x

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ 0 * Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j, x⟩ = 0
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x * 0 = 0

Tactic:
obtain ⟨j, x⟩ := x

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j, x⟩ * 0 = 0
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ (ConcreteCategory.hom (t.ι.app i)) x *
      (ConcreteCategory.hom (t.ι.app (IsFiltered.max i j)))
        ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax i j))) y) =
    (ConcreteCategory.hom (t.ι.app i)) x * (ConcreteCategory.hom (t.ι.app j)) y

Tactic:
t.w_apply

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ (ConcreteCategory.hom (t.ι.app i)) x * (ConcreteCategory.hom (t.ι.app j)) y =
    (ConcreteCategory.hom (t.ι.app i)) x * (ConcreteCategory.hom (t.ι.app j)) y
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s✝ : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec : f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m
A : update (s.piecewise (fun i ↦ c i • m i) m) j (m j) = s.piecewise (fun i ↦ c i • m i) m
⊢ c j • f (update (s.piecewise (fun i ↦ c i • m i) m) j (m j)) = (∏ i ∈ insert j s, c i) • f m

Tactic:
A,

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s✝ : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec : f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m
A : update (s.piecewise (fun i ↦ c i • m i) m) j (m j) = s.piecewise (fun i ↦ c i • m i) m
⊢ c j • f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ insert j s, c i) • f m
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: α β : Type u
f : α ⟶ β
⊢ ∀ {X Y : Type u} (f : X ⟶ Y), HasImage f

Tactic:
by infer_instance

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
t : Cocone F
x : ↑(R F)
⊢ (descMonoidHom t) x = (descAddMonoidHom t) x

Tactic:
obtain ⟨j, x⟩ := x

Goal state after:
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
x✝ : ↑(R F)
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ (descMonoidHom t) (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j, x⟩) =
    (descAddMonoidHom t) (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j, x⟩)
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 ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ 0 +
        ((f.linearDeriv x) h - (f.linearDeriv x) h' +
          (∑ s with 2 ≤ #s, f (s.piecewise h x) - ∑ s with 2 ≤ #s, f (s.piecewise h' x))) -
      (f.linearDeriv x) (h - h') =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))

Tactic:
zero_add,

Goal state after:
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 ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ (f.linearDeriv x) h - (f.linearDeriv x) h' +
        (∑ s with 2 ≤ #s, f (s.piecewise h x) - ∑ s with 2 ≤ #s, f (s.piecewise h' x)) -
      (f.linearDeriv x) (h - h') =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))
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 ⋙ coyoneda.obj (op X)).sections
j j' : J
f : j ⟶ j'
⊢ 𝟙 X ≫ ↑s j' = ↑s j ≫ F.map f

Tactic:
rw [Category.id_comp]

Goal state after:
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 ⋙ coyoneda.obj (op X)).sections
j j' : J
f : j ⟶ j'
⊢ ↑s j' = ↑s j ≫ F.map f
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'
⊢ 𝟙 (op X) ≫ (↑s j').op = (↑s j).op ≫ F.map f

Tactic:
rw [Category.id_comp]

Goal state after:
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'
⊢ (↑s j').op = (↑s j).op ≫ F.map f
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
x✝ : J
⊢ ((forget MonCat).mapCone
            { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
              π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } }).π.app
      x✝ =
    ((Types.isLimitEquivSections t).trans (equivShrink ↑(F ⋙ forget MonCat).sections)).symm.toIso.hom ≫ c.π.app x✝

Tactic:
ext
    simp [Types.isLimitEquivSections]
    simp [← CategoryTheory.comp_apply]
    rfl

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ (Hom.hom (s.ι.app j)) ((f i j h) x) = (Hom.hom (s.ι.app i)) x

Tactic:
by
      simp only [Functor.const_obj_obj]
      rw [← s.w (homOfLE h)]
      rfl

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
f : ℕ → AddCommGrpCat
⊢ HasProduct f

Tactic:
by infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
inst✝ : HasLimit F
j : J
⊢ colimit.ι F.rightOp j ≫ (colimitRightOpIsoUnopLimit F).hom = (limit.π F (op j)).op

Tactic:
by
  simp [colimitRightOpIsoUnopLimit]

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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      G.obj (F.obj X) ◁
          (adj.unit.app (Y ⊗ Z) ≫
            G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
              G.map (F.map (μ G (F.obj Y) (F.obj Z))) ≫ G.map (adj.counit.app (F.obj Y ⊗ F.obj Z))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
unit_naturality_assoc,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      G.obj (F.obj X) ◁
          ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫
            adj.unit.app (G.obj (F.obj Y) ⊗ G.obj (F.obj Z)) ≫
              G.map (F.map (μ G (F.obj Y) (F.obj Z))) ≫ G.map (adj.counit.app (F.obj Y ⊗ F.obj Z))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      (G.obj (F.obj X) ◁ (adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫
          G.obj (F.obj X) ◁
            (adj.unit.app (G.obj (F.obj Y) ⊗ G.obj (F.obj Z)) ≫
              G.map (F.map (μ G (F.obj Y) (F.obj Z))) ≫ G.map (adj.counit.app (F.obj Y ⊗ F.obj Z)))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
unit_naturality_assoc,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      (G.obj (F.obj X) ◁ (adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫
          G.obj (F.obj X) ◁
            (μ G (F.obj Y) (F.obj Z) ≫
              adj.unit.app (G.obj (F.obj Y ⊗ F.obj Z)) ≫ G.map (adj.counit.app (F.obj Y ⊗ F.obj Z)))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d c : RingCon M
s t : ↑(Set.Ici c)
⊢ (∀ (x x_1 : M), (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1) → (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1)) ↔
    ∀ {x y : M}, ↑s x y → ↑t x y

Tactic:
simp_rw [mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le s.2) c.mk'_surjective,
      mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le t.2) c.mk'_surjective]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r₁ r₂ : R
⊢ 0 = 0 + 0 <• r₂

Tactic:
zero_add,

Goal state after:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r₁ r₂ : R
⊢ 0 = 0 <• r₂
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
m₁ m₂ : M
⊢ 0 + m₁ <• 0 = 0

Tactic:
zero_add,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
m₁ m₂ : M
⊢ m₁ <• 0 = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 0 + x.2 <• 1 = x.2

Tactic:
zero_add,

Goal state after:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x.2 <• 1 = x.2
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 0 + 0 <• x.1 = 0

Tactic:
zero_add,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 0 <• x.1 = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 0 + 0 •> x.2 = 0

Tactic:
zero_add,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 0 •> x.2 = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x
⊢ x.fst * (⅟x).fst = 1

Tactic:
rw [← fst_mul, mul_invOf_self, fst_one]

Goal state after: