mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : ↑(colimitCocone F).pt
⊢ (Hom.hom m) x = (Hom.hom (descMorphism F s)) x

Tactic:
by
    refine Quot.inductionOn x ?_
    intro x
    induction x with
    | zero => simp
    | one => simp
    | neg x ih => simp [ih]
    | of j x =>
      exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
    | add x y ih_x ih_y => simp [ih_x, ih_y]
    | mul x y ih_x ih_y => simp [ih_x, ih_y]

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
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, Mᵀ (σ i) i = ∑ σ, ↑↑(sign σ) * ∏ i, M (σ i) i

Tactic:
refine Fintype.sum_bijective _ inv_involutive.bijective _ _ ?_

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∀ (x : Perm n), ↑↑(sign x) * ∏ i, Mᵀ (x i) i = ↑↑(sign x⁻¹) * ∏ i, M (x⁻¹ i) i
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
⊢ (A * adjp 1 A + detp (-1) A • 1) i j = (A * adjp (-1) A + detp 1 A • 1) i j

Tactic:
rcases eq_or_ne i j with rfl | h

Goal state after:
case inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i : n
⊢ (A * adjp 1 A + detp (-1) A • 1) i i = (A * adjp (-1) A + detp 1 A • 1) i i

case inr
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 + detp (-1) A • 1) i j = (A * adjp (-1) A + detp 1 A • 1) i j
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
A : Matrix n n R
⊢ (-A).det = (-1) ^ Fintype.card n • A.det

Tactic:
rw [← det_smul_of_tower, Units.neg_smul, one_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) +
      ((detp 1 A * detp (-1) B) • 1 + (detp (-1) A * detp 1 B) • 1) =
    detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B) +
      ((detp 1 A * detp (-1) B) • 1 + (detp (-1) A * detp 1 B) • 1)
⊢ B * A = 1

Tactic:
← smul_smul

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) +
      (detp 1 A • detp (-1) B • 1 + detp (-1) A • detp 1 B • 1) =
    detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B) +
      (detp 1 A • detp (-1) B • 1 + detp (-1) A • detp 1 B • 1)
⊢ B * A = 1
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat) ⟨j, 0 * x⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩

Tactic:
zero_mul 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
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat) ⟨j, 0⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩
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 ι
⊢ f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m

Tactic:
refine s.induction_on (by simp) ?_
  intro j s j_notMem_s Hrec
  have A :
    Function.update (s.piecewise (fun i => c i • m i) m) j (m j) =
      s.piecewise (fun i => c i • m i) m := by
    ext i
    by_cases h : i = j
    · rw [h]
      simp [j_notMem_s]
    · simp [h]
  rw [s.piecewise_insert, f.map_update_smul, A, Hrec]
  simp [j_notMem_s, mul_smul]

Goal state after:
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✝ : Fintype ι
c : ι → R
m : (i : ι) → M₁ i
⊢ (f fun i ↦ c i • m i) = (∏ i, c i) • f m

Tactic:
by
  classical simpa using map_piecewise_smul f c m Finset.univ

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

Goal state before:
pp: α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f

Tactic:
by
  ext x
  change (F'.e ≫ F'.m) _ = _
  rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
  rfl

Goal state after:
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 r
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
⊢ Function.Injective fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x

Tactic:
intro (x : E.pt) y H

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
x : E.pt
y : ToType D.pt
H : (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) x = (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) y
⊢ x = y
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ W ◁ (f ≫ g) = W ◁ f ≫ W ◁ g

Tactic:
by
  simp [← id_tensorHom]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ (ρ_ Y).hom = (α_ X Y (𝟙_ C)).inv ≫ (ρ_ (X ⊗ Y)).hom

Tactic:
← whiskerRight_iff,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (X ◁ (ρ_ Y).hom) ▷ 𝟙_ C = ((α_ X Y (𝟙_ C)).inv ≫ (ρ_ (X ⊗ Y)).hom) ▷ 𝟙_ C
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case η
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ η F = η F

Tactic:
rw [← cancel_epi (εIso _).hom]
    rw [εIso_hom, ε_η, ← @ε_η _ _ _ _ _ _ _ a, ← εIso_hom]
    exact congr(($eq.symm).ε ≫ _)

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
⊢ HasLimitsOfShape Jᵒᵖ Cᵒᵖ ↔ HasColimitsOfShape J C

Tactic:
by
  refine ⟨fun _ ↦ hasColimitsOfShape_of_hasLimitsOfShape_op, fun _ ↦ ?_⟩
  have : HasColimitsOfShape Jᵒᵖᵒᵖ C := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm
  exact hasLimitsOfShape_op_of_hasColimitsOfShape

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ_ X).hom

Tactic:
← whiskerRight_iff,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((β_ X (𝟙_ C)).hom ≫ (λ_ X).hom) ▷ 𝟙_ C = (ρ_ X).hom ▷ 𝟙_ C
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
R : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Semiring N
inst✝² : Algebra R N
inst✝¹ : Semiring P
inst✝ : Algebra R P
c✝ d✝ : RingCon M
f : M →ₐ[R] P
c : RingCon M
d : RingCon N
e : M ≃ₐ[R] N
h : c = d.comap e
r : R
⊢ (RingCon.congr e.toRingEquiv h).toFun ((algebraMap R c.Quotient) r) = (algebraMap R d.Quotient) r

Tactic:
simp [← coe_algebraMap]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (RingCon.mkₐ R (ringCon R M)) (FreeAlgebra.ι R m) = (ι R) m

Tactic:
rw [ι]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (RingCon.mkₐ R (ringCon R M)) (FreeAlgebra.ι R m) =
    { toFun := fun m ↦ ↑(FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ } m
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ (fun F ↦ F.toLinearMap ∘ₗ ι R) ((fun f ↦ (ringCon R M).liftₐ ((FreeAlgebra.lift R) ⇑f) ⋯) f) = f

Tactic:
rw [ι]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ (fun F ↦ F.toLinearMap ∘ₗ { toFun := fun m ↦ ↑(FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ })
      ((fun f ↦ (ringCon R M).liftₐ ((FreeAlgebra.lift R) ⇑f) ⋯) f) =
    f
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ (⇑(((fun f ↦ (ringCon R M).liftₐ ((FreeAlgebra.lift R) ⇑f) ⋯) ((fun F ↦ F.toLinearMap ∘ₗ ι R) F)).comp
            (RingCon.mkₐ R (ringCon R M))) ∘
        FreeAlgebra.ι R)
      x =
    (⇑(F.comp (RingCon.mkₐ R (ringCon R M))) ∘ FreeAlgebra.ι R) x

Tactic:
rw [ι]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ (⇑(((fun f ↦ (ringCon R M).liftₐ ((FreeAlgebra.lift R) ⇑f) ⋯)
                ((fun F ↦ F.toLinearMap ∘ₗ { toFun := fun m ↦ ↑(FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ })
                  F)).comp
            (RingCon.mkₐ R (ringCon R M))) ∘
        FreeAlgebra.ι R)
      x =
    (⇑(F.comp (RingCon.mkₐ R (ringCon R M))) ∘ FreeAlgebra.ι R) x
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
⊢ (map f) (inr x) = inr (f x)

Tactic:
by
  rw [map, liftEquivOfComm_apply, lift_apply_inr, LinearMap.comp_apply, inrHom_apply]

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

Goal state before:
pp: R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
              Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
              (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).hom ≫
                ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
          M))
      (1 ⊗ₜ[R₁] m)

Tactic:
have h₂ := extendScalarsComp_hom_app_one_tmul f₁₂ (f₃₄.comp f₂₃) M m

Goal state after:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
              Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
              (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).hom ≫
                ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
          M))
      (1 ⊗ₜ[R₁] m)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] m)
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
⊢ (Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp f₁₂ f₂₃).hom.app M))) (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)) =
    (Hom.hom ((extendScalarsComp f₂₃ f₃₄).hom.app ((extendScalars f₁₂).obj M)))
      ((Hom.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m))

Tactic:
erw [h₂]

Goal state after:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] m)
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
⊢ (Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp f₁₂ f₂₃).hom.app M))) (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)) =
    (Hom.hom ((extendScalarsComp f₂₃ f₃₄).hom.app ((extendScalars f₁₂).obj M))) (1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m))
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
N' : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : N →ₗ[R] N'
g : P →ₗ[R] M ⊗[R] N
⊢ (α ∘ₗ ρ⁻¹ ⊗ₘ f) ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) ∘ₗ g

Tactic:
← assoc_comp_map_rid_symm

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
h : P →ₗ[R] M ⊗[R] N
⊢ β ∘ₗ f ⊗ₘ g ∘ₗ h = g ⊗ₘ f ∘ₗ β ∘ₗ h

Tactic:
simp only [← LinearMap.comp_assoc, symm_comp_map]

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

Goal state before:
pp: case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : a ^ (n + 1) * c ≠ 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)

Tactic:
rw [Ne, pow_succ', mul_assoc, mul_eq_zero, not_or] at hb

Goal state after:
case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
G : CommMonCat
⊢ R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
      {
            app := fun S ↦
              Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                ⋯,
            naturality := ⋯ }.app
        (R.monoidAlgebra.obj G) =
    𝟙 (R.monoidAlgebra.obj G)

Tactic:
by
    ext : 2
    apply MonoidAlgebra.ringHom_ext <;> intro <;> simp [MonoidAlgebra.liftNCRingHom]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
⊢ a ∣ b ↔ ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b

Tactic:
classical
  refine ⟨fun h _ _ ↦ emultiplicity_le_emultiplicity_of_dvd_right h, fun h ↦ ?_⟩
  by_cases hb : b = 0
  · simp_all
  let : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
  rw [dvd_iff_normalizedFactors_le_normalizedFactors ha hb, Multiset.le_iff_count]
  intro q
  by_cases hq : q ∈ normalizedFactors a
  · have hqprime : Prime q := prime_of_normalized_factor q hq
    have h1 := emultiplicity_eq_count_normalizedFactors hqprime.irreducible ha
    have h2 := emultiplicity_eq_count_normalizedFactors hqprime.irreducible hb
    rw [normalize_normalized_factor q hq] at h1 h2
    simpa [h1, h2] using h q hqprime
  · simp [Multiset.count_eq_zero_of_notMem hq]

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
α : Type u_3
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Rˣ
f : α → M
g : α → R
hgi : Function.Injective g
hg : ∀ (s : α), Irreducible (g s)
r : R
hr : r ≠ 0
⊢ Function.HasFiniteMulSupport fun s ↦ f s ^ multiplicity (g s) r

Tactic:
classical
  simp only [multiplicity_eq_count_normalizedFactors (hg _) hr, normalize_eq]
  fun_prop

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
⊢ span s ≤ span t

Tactic:
intro x hx
  rw [mem_span_iff] at hx ⊢
  exact fun I hI => hx I <| h.trans hI

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
refine .inr <| ⟨x * r' * y, ⟨x * r', mem_univ _, y, hy, ?_⟩, ⟨r, mem_univ _, ?_⟩⟩
        all_goals simp [mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
by_cases! hd : d ≤ 0

Goal state after:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ selfZPow x B d * selfZPow x B (-d) = 1

case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ selfZPow x B d * selfZPow x B (-d) = 1
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 = selfZPow x B d * b
this : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b * (selfZPow x B d * selfZPow x B (-d))
⊢ selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b

Tactic:
selfZPow_mul_neg,

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 = selfZPow x B d * b
this : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b * 1
⊢ selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
this : η = η
⊢ h₁ = h₂

Tactic:
cases h₁

Goal state after:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₂ : MonObj X
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
H : μ = μ
this : η = η
⊢ { one := one✝, mul := mul✝, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ } = h₂