mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ x.fst •> xs.prod.snd + x.snd <• xs.prod.fst =
    (x.snd <• (List.map fst xs).prod ::
        List.map
          (fun x_1 ↦
            x.fst •> (List.take x_1.2 (List.map fst xs)).prod •> x_1.1.snd <•
              (List.drop (x_1.2 + 1) (List.map fst xs)).prod)
          xs.zipIdx).sum

Tactic:
List.sum_cons,

Goal state after:
case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ x.fst •> xs.prod.snd + x.snd <• xs.prod.fst =
    x.snd <• (List.map fst xs).prod +
      (List.map
          (fun x_1 ↦
            x.fst •> (List.take x_1.2 (List.map fst xs)).prod •> x_1.1.snd <•
              (List.drop (x_1.2 + 1) (List.map fst xs)).prod)
          xs.zipIdx).sum
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
inst✝² : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
⊢ (⅟x).snd = -(⅟x.fst •> x.snd <• ⅟x.fst)

Tactic:
let := invertibleOfInvertibleFst x

Goal state after:
R : Type u
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Semiring R
inst✝⁴ : Module Rᵐᵒᵖ M
inst✝³ : Module R M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
⊢ (⅟x).snd = -(⅟x.fst •> x.snd <• ⅟x.fst)
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
⊢ (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₂₃.comp f₁₂) 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)
⊢ (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.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
⊢ Bialgebra S (A ⊗[R] B)

Tactic:
have hcounit := congr(DFunLike.coe $(counit_eq_algHom_toLinearMap R S A B))

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
hcounit :
  ⇑counit =
    ⇑((↑(Algebra.TensorProduct.rid R S S)).comp
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap
⊢ Bialgebra S (A ⊗[R] B)
Module: Mathlib.Order.Category.Preord

Goal state before:
pp: X✝ Y✝ : Preord
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : preordToCat.map a₁✝ = preordToCat.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext x; exact Functor.congr_obj congr(($h).toFunctor) x

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
f : M →ₗ[R] M ⊗[R] M₃
⊢ α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ ∘ₗ f = f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id ∘ₗ f

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

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ ((α ∘ₗ β ⊗ₘ f) ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
    ((((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α) ∘ₗ
        LinearMap.rTensor M δ) ∘ₗ
      δ

Tactic:
congr 2

Goal state after:
case e_f.e_f
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ α ∘ₗ β ⊗ₘ f = ((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α
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))

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
⊢ ↑(count (normalize a) (normalizedFactors b)) ≤ emultiplicity a b

Tactic:
· apply Order.le_of_lt_add_one
    rw [← Nat.cast_one, ← Nat.cast_add, lt_iff_not_ge,
      le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]
    simp

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)) ≤ emultiplicity a b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case inl.succ
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hnorm : normalize 0 = 0
n✝ : ℕ
hle : 0 ^ (n✝ + 1) ∣ x
hlt : ¬0 ^ (n✝ + 1 + 1) ∣ x
⊢ count 0 (normalizedFactors x) = n✝ + 1

Tactic:
rw [zero_pow (Nat.succ_ne_zero _)] at hle hlt

Goal state after:
case inl.succ
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hnorm : normalize 0 = 0
n✝ : ℕ
hle : 0 ∣ x
hlt : ¬0 ∣ x
⊢ count 0 (normalizedFactors x) = n✝ + 1
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
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : P) (n : ℕ), ∃ b m k, f (r ^ (k + n) * b) = f r ^ (k + m) * a) ↔ ∀ (a : P), ∃ b m, f b = f r ^ m * a

Tactic:
· refine ⟨fun H x ↦ ⟨_, _, (H x 0).choose_spec.choose_spec.choose_spec⟩, fun H a n ↦ ?_⟩
    obtain ⟨b, m, e⟩ := H a
    exact ⟨b, n + m, 0, by simp [e, pow_add]; ring_nf⟩

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ ↑(jacobson (R ⧸ I)) = ↑(Module.jacobson R (R ⧸ I))

Tactic:
let f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := ⟨AddHom.id _, fun _ _ ↦ rfl⟩

Goal state after:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ ↑(jacobson (R ⧸ I)) = ↑(Module.jacobson R (R ⧸ I))
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ sInf {J | True ∧ J.IsMaximal} = sInf {m | IsCoatom m}

Tactic:
true_and,

Goal state after:
R : Type u
inst✝ : Ring R
⊢ sInf {J | J.IsMaximal} = sInf {m | IsCoatom m}
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Ring.jacobson R • Submodule.map N.subtype ⊤

pp: case e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = Submodule.map N.subtype ⊤

Tactic:
all_goals rw [Submodule.map_top, range_subtype]

Goal state after:
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2) • f i = ↑(∏ i ∈ s, (sec M (f i)).2) • f i

Tactic:
congr 2

Goal state after:
case refine_2.e_a
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2 = ↑(∏ i ∈ s, (sec M (f i)).2)
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
m : M
s : ↥S
h : ⋯.unit⁻¹ • f (m, s).1 = x
⊢ f (m, s).1 ∈ ↑(span R (⇑f '' v))

Tactic:
rw [← LinearMap.coe_restrictScalars R, ← LinearMap.map_span, hv]

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
m : M
s : ↥S
h : ⋯.unit⁻¹ • f (m, s).1 = x
⊢ (↑R f) (m, s).1 ∈ ↑(map (↑R f) ⊤)
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent Rₛ (⇑f ∘ v)

Tactic:
rw [linearIndependent_iff'ₛ] at hv ⊢

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
⊢ ∀ (s : Finset ι) (f_1 g : ι → Rₛ), ∑ i ∈ s, f_1 i • (⇑f ∘ v) i = ∑ i ∈ s, g i • (⇑f ∘ v) i → ∀ i ∈ s, f_1 i = g i
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
i : ι
⊢ (ofIsLocalizedModule Rₛ S f b) i = f (b i)

Tactic:
rw [ofIsLocalizedModule, coe_mk, Function.comp_apply]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ η ≫ (β_ X Y).hom = η

Tactic:
simp only [tensorObj.one_def, Category.assoc, BraidedCategory.braiding_naturality,
    braiding_tensorUnit_right, Iso.cancel_iso_inv_left]
  monoidal

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (((((((((β_ X Y).hom ▷ (X ⊗ Y) ≫ (α_ (Y ⊗ X) X Y).inv) ≫ (α_ (Y ⊗ X) X Y).hom) ≫ (α_ Y X (X ⊗ Y)).hom) ≫
                Y ◁ X ◁ (β_ X Y).hom) ≫
              Y ◁ (α_ X Y X).inv) ≫
            Y ◁ (β_ X Y).hom ▷ X) ≫
          Y ◁ (α_ Y X X).hom) ≫
        (α_ Y Y (X ⊗ X)).inv) ≫
      (μ ⊗ₘ μ) =
    ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫
      (α_ Y X (Y ⊗ X)).hom ≫
        Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ)

Tactic:
slice_lhs 2 3 =>
    rw [Iso.inv_hom_id]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (β_ X Y).hom ▷ (X ⊗ Y) ≫
      ((((((𝟙 ((Y ⊗ X) ⊗ X ⊗ Y) ≫ (α_ Y X (X ⊗ Y)).hom) ≫ Y ◁ X ◁ (β_ X Y).hom) ≫ Y ◁ (α_ X Y X).inv) ≫
              Y ◁ (β_ X Y).hom ▷ X) ≫
            Y ◁ (α_ Y X X).hom) ≫
          (α_ Y Y (X ⊗ X)).inv) ≫
        (μ ⊗ₘ μ) =
    ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫
      (α_ Y X (Y ⊗ X)).hom ≫
        Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a.a
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
M N O X✝ : C
inst✝¹² : MonObj M
inst✝¹¹ : MonObj N
inst✝¹⁰ : MonObj O
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
| F.map (μ ▷ X) ≫ F.map μ

pp: case a
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
M N O X✝ : C
inst✝¹² : MonObj M
inst✝¹¹ : MonObj N
inst✝¹⁰ : MonObj O
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
| «μ» F X X ▷ F.obj X

pp: case a.a
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
M N O X✝ : C
inst✝¹² : MonObj M
inst✝¹¹ : MonObj N
inst✝¹⁰ : MonObj O
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
| «μ» F (X ⊗ X) X

Tactic:
← F.map_comp,

Goal state after:
case a.a
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
M N O X✝ : C
inst✝¹² : MonObj M
inst✝¹¹ : MonObj N
inst✝¹⁰ : MonObj O
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
| F.map (μ ▷ X ≫ μ)

case a
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
M N O X✝ : C
inst✝¹² : MonObj M
inst✝¹¹ : MonObj N
inst✝¹⁰ : MonObj O
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
| «μ» F X X ▷ F.obj X

case a.a
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
M N O X✝ : C
inst✝¹² : MonObj M
inst✝¹¹ : MonObj N
inst✝¹⁰ : MonObj O
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
| «μ» F (X ⊗ X) X
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_1.h₁
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
⊢ (l ≫ t₁.snd) ≫ t₂.snd = s.snd ≫ t₂.snd

Tactic:
· simpa using hl'

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Module A M'
inst✝² : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
⊢ IsLocalizedModule S ↑(IsScalarTower.toAlgHom R T (A ⊗[R] T))

Tactic:
rw [isLocalizedModule_iff_isBaseChange (S := S) (A := A)]

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Module A M'
inst✝² : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
⊢ IsBaseChange A ↑(IsScalarTower.toAlgHom R T (A ⊗[R] T))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 *
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) •
      mk m s =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2 • mk m s

Tactic:
← IsLocalization.mk'_mul,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ IsLocalization.mk' T ((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1)
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2) •
      mk m s =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2 • mk m s
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case W
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ CommRingCat

Tactic:
exact CommRingCat.of (A ⊗[R] B)

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

Goal state before:
pp: R S Rₘ Sₘ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing Rₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : CommRing S
inst✝³ : CommRing Sₘ
inst✝² : Algebra S Sₘ
f : R →+* S
fₘ : Rₘ →+* Sₘ
H : fₘ.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp f
M : Submonoid R
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
⊢ IsPushout (ofHom f) (ofHom (algebraMap R Rₘ)) (ofHom (algebraMap S Sₘ)) (ofHom fₘ)

Tactic:
algebraize [f, fₘ, fₘ.comp (algebraMap R Rₘ)]
  have : IsScalarTower R S Sₘ := .of_algebraMap_eq' H
  have : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ := ‹_›
  exact CommRingCat.isPushout_iff_isPushout.mpr (Algebra.isPushout_of_isLocalization M _ _ _)

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Comma

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (h.unit.app A))).pt ⟶ s.pt
x✝ : ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone (StructuredArrow.mk (h.unit.app A))).ι.app j ≫ m = s.ι.app j
⊢ m = StructuredArrow.homMk ((h.homEquiv A s.pt.right).symm s.pt.hom) ⋯

Tactic:
apply StructuredArrow.ext

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (h.unit.app A))).pt ⟶ s.pt
x✝ : ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone (StructuredArrow.mk (h.unit.app A))).ι.app j ≫ m = s.ι.app j
⊢ StructuredArrow.Hom.right m =
    StructuredArrow.Hom.right (StructuredArrow.homMk ((h.homEquiv A s.pt.right).symm s.pt.hom) ⋯)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
⊢ Function.Injective ⇑g

Tactic:
by
  intro a b hab
  obtain ⟨⟨x, m⟩, (hxm : m • a = f x)⟩ := IsLocalizedModule.surj S f a
  obtain ⟨⟨y, n⟩, (hym : n • b = f y)⟩ := IsLocalizedModule.surj S f b
  suffices h : g (f (n.val • x)) = g (f (m.val • y)) by
    apply H at h
    rw [map_smul, map_smul] at h
    rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]
  simp [← hxm, ← hym, hab, ← S.smul_def, ← mul_smul, mul_comm, ← mul_smul]

Goal state after: