mathlib-initiative/mathlib-tactics huggingface dataset:
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 ≠ (σ * τ) l
hl2 : l ∉ {τ⁻¹ j}
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
← mem_compl

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.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case insert.k
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ n

pp: case insert.x
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ ?insert.k ∉ s

pp: case insert.x
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ ∀ (i_1 j : n), A i_1 j = B.updateRow i (A i) i_1 j + update c i 0 i_1 * B.updateRow i (A i) ?insert.k j

Tactic:
· exact k

Goal state after:
case insert.x
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ k ∉ s

case insert.x
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ ∀ (i_1 j : n), A i_1 j = B.updateRow i (A i) i_1 j + update c i 0 i_1 * B.updateRow i (A i) k j
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: case mpr.refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : Limits.IsColimit (F.coconeTypesEquiv c)
x : c.pt
f₁ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := true }
f₂ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := decide (∃ a, F.descColimitType c a = x) }
⊢ ∃ a, F.descColimitType c a = x

Tactic:
suffices f₁ = f₂ by
        have := ConcreteCategory.congr_hom this x
        simpa [f₁, f₂] using this

Goal state after:
case mpr.refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : Limits.IsColimit (F.coconeTypesEquiv c)
x : c.pt
f₁ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := true }
f₂ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := decide (∃ a, F.descColimitType c a = x) }
⊢ f₁ = f₂
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
⊢ ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)

Tactic:
rw [Set.mem_toFinset] at hσn

Goal state after:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ ↑(sumCongrHom m n).range
⊢ ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
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 v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
⊢ (if i = j then s.piecewise a v j - b j else b j) = if j = i then a j - b j else b j

Tactic:
obtain rfl | hij := eq_or_ne i j

Goal state after:
case neg.inl
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 v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi hjs : i ∈ s
hji : ¬i < i
⊢ (if i = i then s.piecewise a v i - b i else b i) = if i = i then a i - b i else b i

case neg.inr
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 v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
hij : i ≠ j
⊢ (if i = j then s.piecewise a v j - b j else b j) = if j = i then a j - b j else b j
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFilteredOrEmpty J
D : Cocone F
hD : IsColimit D
x : ToType D.pt
k : J
⊢ ∃ j x_1 y, (ConcreteCategory.hom (D.ι.app j)) y = x

Tactic:
obtain ⟨j, y, rfl⟩ := isColimit_exists_rep F hD x

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFilteredOrEmpty J
D : Cocone F
hD : IsColimit D
k j : J
y : ToType (F.obj j)
⊢ ∃ j_1 x y_1, (ConcreteCategory.hom (D.ι.app j_1)) y_1 = (ConcreteCategory.hom (D.ι.app j)) y
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✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝ : (uliftYoneda.{w', v, u}.obj X).obj X✝
⊢ (ConcreteCategory.hom
          ((uliftYoneda.{w', v, u}.obj X).map f ≫ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso.hom ≫
            (shrinkYoneda.{max w' v, v, u}.obj X).map f)).toFun
      x✝

Tactic:
exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm _ _).symm

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 : Cᵒᵖ
P : C ⥤ Type w
s : P.obj (unop X)
Y : Cᵒᵖ
f : Y ⟶ X
⊢ (ConcreteCategory.hom ((shrinkCoyonedaEquiv.symm s).app (unop Y))) (shrinkCoyonedaObjObjEquiv.symm f.unop) =
    (ConcreteCategory.hom (P.map f.unop)) s

Tactic:
obtain ⟨g, rfl⟩ := shrinkCoyonedaEquiv.surjective s

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
Y : Cᵒᵖ
f : Y ⟶ X
g : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
⊢ (ConcreteCategory.hom ((shrinkCoyonedaEquiv.symm (shrinkCoyonedaEquiv g)).app (unop Y)))
      (shrinkCoyonedaObjObjEquiv.symm f.unop) =
    (ConcreteCategory.hom (P.map f.unop)) (shrinkCoyonedaEquiv g)
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_2.refine_2
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
⊢ ∀ (s : Cone F),
    (forget MonCat).map
        (ofHom
          {
            toFun :=
              ⇑(ConcreteCategory.hom
                  ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s))),
            map_one' := ⋯, map_mul' := ⋯ }) =
      (Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s)

Tactic:
exact fun _ ↦ rfl

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 ⥤ E
H : E ⥤ E'
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : H.LaxMonoidal
X Y : C
⊢ μ ((F ⋙ G) ⋙ H) X Y ≫ (F.associator G H).hom.app (X ⊗ Y) =
    ((F.associator G H).hom.app X ⊗ₘ (F.associator G H).hom.app Y) ≫ μ (F ⋙ G ⋙ H) X Y

Tactic:
by
    simp only [comp_obj, comp_μ, associator_hom_app, Functor.comp_map, map_comp,
      comp_id, tensorHom_id, id_whiskerRight, assoc, id_comp]

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
e : F₁ ≅ F₂
inst✝ : NatTrans.IsMonoidal e.hom
⊢ LaxMonoidal.ε F₂ ≫ e.inv.app (𝟙_ C) = LaxMonoidal.ε F₁

Tactic:
rw [← NatTrans.IsMonoidal.unit (τ := e.hom), assoc, hom_inv_id_app, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (G.mapCone (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ?m.108))

Tactic:
refine @isLimitOfPreserves _ _ _ _ _ _ _ _ _ ?_ ?_
      · apply PullbackCone.isLimitOfFlip
        apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)
        exact (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₁} _) _).invFun hc
      · dsimp
        infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ c.π.app WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr =
    c.π.app WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl

Tactic:
· exact
        (c.π.naturality WalkingCospan.Hom.inr).symm.trans
          (c.π.naturality WalkingCospan.Hom.inl :)

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ MorphismProperty.surjective C f

Tactic:
change Function.Surjective ((forget C).map f)

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ Function.Surjective ⇑(hom ((forget C).map f))
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'
e : C ≌ D
inst✝ : e.functor.Monoidal
this : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
⊢ e.inverse.Monoidal

Tactic:
have : IsIso (LaxMonoidal.ε e.inverse) := by
    simp only [this, Adjunction.rightAdjointLaxMonoidal_ε, Adjunction.homEquiv_unit]
    infer_instance

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'
e : C ≌ D
inst✝ : e.functor.Monoidal
this✝ : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
this : IsIso (LaxMonoidal.ε e.inverse)
⊢ e.inverse.Monoidal
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j'))
      ((ConcreteCategory.hom (F.map f)) x) =
    ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) x

Tactic:
refine eq_of_sub_eq_zero ?_

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j'))
        ((ConcreteCategory.hom (F.map f)) x) -
      ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) x =
    0
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
⊢ Quot (F ⋙ uliftFunctor) →+ Quot F

Tactic:
refine QuotientAddGroup.lift (Relations (F ⋙ uliftFunctor))
    (DFinsupp.sumAddHom (fun j ↦ (Quot.ι _ j).comp AddEquiv.ulift.toAddMonoidHom)) ?_

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ Relations (F ⋙ uliftFunctor) ≤ (DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R✝ : Type u
inst✝² : CommRing R✝
R : Type v
inst✝¹ : CommRing R
inst✝ : Small.{u, v} R
e : AlgCat R ≌ AlgCat (Shrink.{u, v} R) := restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)
this :
  e.inverse ⋙ forget₂ (AlgCat R) (ModuleCat R) =
    forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R)) ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse
⊢ (forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R)) ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse).IsRightAdjoint

Tactic:
have := (tensorAlgebraAdj (Shrink.{u} R)).isRightAdjoint

Goal state after:
R✝ : Type u
inst✝² : CommRing R✝
R : Type v
inst✝¹ : CommRing R
inst✝ : Small.{u, v} R
e : AlgCat R ≌ AlgCat (Shrink.{u, v} R) := restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)
this✝ :
  e.inverse ⋙ forget₂ (AlgCat R) (ModuleCat R) =
    forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R)) ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse
this : (forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R))).IsRightAdjoint
⊢ (forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R)) ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse).IsRightAdjoint
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
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (x ^ n).snd = n •> x.fst ^ n.pred •> x.snd

Tactic:
simp_rw [snd_pow_eq_sum, ← smul_comm (_ : R) (_ : Rᵐᵒᵖ), aux, smul_smul, ← pow_add]
  match n with
  | 0 => rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
  | (Nat.succ n) =>
    simp_rw [Nat.pred_succ]
    exact (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) (by grind)).trans
      (by rw [List.length_map, List.length_range])

Goal state after:
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:
by rw [← fst_mul, mul_invOf_self, fst_one]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ 0 = (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B

Tactic:
comp_zero,

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ 0 = (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ 0 = (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B

Tactic:
comp_zero,

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ 0 = (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
f g : A →ₗc[R] R
x : A
hf : counit (f x) = counit x
hg : counit (g x) = counit x
⊢ f x = g x

Tactic:
simp_all only [CommSemiring.counit_apply]

Goal state after:
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✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ (ConcreteCategory.hom (HomEquiv.fromExtendScalars f g)) (1 ⊗ₜ[R] x) = (Hom.hom g) x

Tactic:
erw [HomEquiv.fromExtendScalars_hom_apply]

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ (lift { toFun := fun s ↦ HomEquiv.evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (1 ⊗ₜ[R] x) = (Hom.hom g) x
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
⊢ LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul = (mk S (A ⊗[R] B) S).flip 1

Tactic:
by
    ext x y
    convert!
      congr((TensorProduct.rid S _).symm
        (TensorProduct.rid _ _ $(lTensor_counit_comul (R := S) x) ⊗ₜ[R]
          TensorProduct.rid _ _ $(lTensor_counit_comul (R := R) y)))
    · dsimp
      hopf_tensor_induction comul (R := S) x with x₁ x₂
      hopf_tensor_induction comul (R := R) y with y₁ y₂
      apply (TensorProduct.rid S _).injective
      dsimp
      rw [tmul_smul, smul_assoc, one_smul, smul_tmul']
    · dsimp
      simp only [one_smul]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b < ↑(count (normalize a) (normalizedFactors b) + 1)

Tactic:
lt_iff_not_ge,

Goal state after:
case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ¬↑(count (normalize a) (normalizedFactors b) + 1) ≤ emultiplicity a b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hx : x ≠ 0
⊢ (map (fun p ↦ p) (normalizedFactors x)).prod ~ᵤ x

Tactic:
Multiset.map_id'

Goal state after:
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hx : x ≠ 0
⊢ (normalizedFactors x).prod ~ᵤ x
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
s : S
⊢ Associated ((algebraMap R S) (sec x s).1) s

Tactic:
by
  rw [← IsLocalization.Away.sec_spec, map_pow]
  exact associated_mul_unit_left _ _ <| .pow _ <| IsLocalization.Away.algebraMap_isUnit _

Goal state after: