mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
⊢ IsPullback (t ≫ fstfi) sndsndfgr f (rY ≫ g)

Tactic:
ht₁

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
⊢ IsPullback (fstsndfgr ≫ fstfg) sndsndfgr f (rY ≫ g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
⊢ f ≫ e₂.hom ≫ inl' = e₁.hom ≫ g' ≫ inr'

Tactic:
← comminl,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
⊢ f ≫ inl ≫ e₄.hom = e₁.hom ≫ g' ≫ inr'
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
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ (↑a.2 * v) • a.1 = (↑u * ↑a.2) • b.1

Tactic:
mul_smul,

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ ↑a.2 • v • a.1 = (↑u * ↑a.2) • b.1
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
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ ↑a.2 • u • b.1 = (↑a.2 * ↑u) • b.1

Tactic:
mul_smul,

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ ↑a.2 • u • b.1 = ↑a.2 • ↑u • b.1
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
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ (u * a.2) • b.1 = (↑u * ↑b.2) • a.1 ∧ ↑(u * a.2) * ↑b.2 = ↑u * ↑b.2 * ↑a.2

Tactic:
mul_smul,

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • a.2 • b.1 = (↑u * ↑b.2) • a.1 ∧ ↑(u * a.2) * ↑b.2 = ↑u * ↑b.2 * ↑a.2
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
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • b.2 • a.1 = (↑u * ↑b.2) • a.1 ∧ ↑(u * a.2) * ↑b.2 = ↑u * ↑b.2 * ↑a.2

Tactic:
mul_smul,

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • b.2 • a.1 = ↑u • ↑b.2 • a.1 ∧ ↑(u * a.2) * ↑b.2 = ↑u * ↑b.2 * ↑a.2
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: 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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ ∃ u,
    u •
        (((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
          (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1) =
      u •
        ((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
          ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1)

Tactic:
use 1

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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ 1 •
      (((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
        (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1) =
    1 •
      ((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
        ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case zero
R : Type u
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a : A
s : ↥S
⊢ mk a s ^ 0 = mk (a ^ 0) (s ^ 0)

Tactic:
rw [pow_zero, pow_zero, pow_zero, OreLocalization.one_def]

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

Goal state before:
pp: 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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ ∃ u,
    u • (s₁ * s₂ * (s₁ * s₃)) • (a₁ * (s₃ • a₂ + s₂ • a₃)) =
      u • (s₁ * (s₂ * s₃)) • ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃))

Tactic:
use 1

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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ 1 • (s₁ * s₂ * (s₁ * s₃)) • (a₁ * (s₃ • a₂ + s₂ • a₃)) =
    1 • (s₁ * (s₂ * s₃)) • ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout (pushout.inr f g) g'
⊢ pushout.inr f g ≫ pushout.inl (pushout.inr f g) g' ≫ (pushoutLeftPushoutInrIso f g g').hom =
    g' ≫ pushout.inr f (g ≫ g')

Tactic:
by
  rw [← Category.assoc, ← Iso.eq_comp_inv, Category.assoc, inr_pushoutLeftPushoutInrIso_inv,
    pushout.condition]

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

Goal state before:
pp: 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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ ∃ u,
    u • (s₁ * s₃ * (s₂ * s₃)) • ((s₂ • a₁ + s₁ • a₂) * a₃) =
      u • (s₁ * s₂ * s₃) • ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃))

Tactic:
use 1

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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ 1 • (s₁ * s₃ * (s₂ * s₃)) • ((s₂ • a₁ + s₁ • a₂) * a₃) =
    1 • (s₁ * s₂ * s₃) • ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃))
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : α → R
F : Multiplicative (Multiset α) →* R
x : Multiplicative (Multiset α)
F' : Multiset α →+ Additive R := MonoidHom.toAdditiveRight F
x' : Multiset α := Multiplicative.toAdd x
⊢ (Multiset.map (fun x ↦ F' x) (Multiset.map (fun x ↦ {x}) x')).sum = F' x'

Tactic:
← AddMonoidHom.map_multiset_sum

Goal state after:
α : Type u
R : Type v
inst✝ : CommRing R
f : α → R
F : Multiplicative (Multiset α) →* R
x : Multiplicative (Multiset α)
F' : Multiset α →+ Additive R := MonoidHom.toAdditiveRight F
x' : Multiset α := Multiplicative.toAdd x
⊢ F' (Multiset.map (fun x ↦ {x}) x').sum = F' x'
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_1
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) 1 = ↑n

Tactic:
use 1

Goal state after:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ (lift fun a ↦ if a ∈ s then 0 else X) 1 = ↑1
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
this : ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (of p) = ↑n
⊢ p ∈ s

Tactic:
lift_of

Goal state after:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
this : ∃ n, (if p ∈ s then 0 else X) = ↑n
⊢ p ∈ s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ mk (r • m) s = mk n t ↔ mk m s = Localization.mk 1 ⟨r, hr⟩ • mk n t

Tactic:
mk_smul_mk,

Goal state after:
case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ mk (r • m) s = mk n t ↔ mk m s = mk (1 • n) (⟨r, hr⟩ * t)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h.mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
⊢ a • (⟨r, hr⟩ * t) • m = a • s • n

Tactic:
mul_smul,

Goal state after:
case h.h.mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
⊢ a • ⟨r, hr⟩ • t • m = a • s • n
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (⟨r, hr⟩ * t) • m = a • s • n
⊢ a • t • r • m = a • (t * ⟨r, hr⟩) • m

Tactic:
mul_smul,

Goal state after:
case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (⟨r, hr⟩ * t) • m = a • s • n
⊢ a • t • r • m = a • t • ⟨r, hr⟩ • m
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: 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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
p : LocalizedModule S M
x✝² x✝¹ : M × ↥S
a : M
b : ↥S
a' : M
b' : ↥S
x✝ : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ c • ((a', b').2 * s) • (a, b).1 = c • ((a, b).2 * s) • (a', b').1

Tactic:
mul_smul,

Goal state after:
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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
p : LocalizedModule S M
x✝² x✝¹ : M × ↥S
a : M
b : ↥S
a' : M
b' : ↥S
x✝ : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ c • (a', b').2 • s • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: 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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
p : LocalizedModule S M
x✝² x✝¹ : M × ↥S
a : M
b : ↥S
a' : M
b' : ↥S
x✝ : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ c • (a', b').2 • s • (a, b).1 = c • ((a, b).2 * s) • (a', b').1

Tactic:
mul_smul,

Goal state after:
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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
p : LocalizedModule S M
x✝² x✝¹ : M × ↥S
a : M
b : ↥S
a' : M
b' : ↥S
x✝ : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ c • (a', b').2 • s • (a, b).1 = c • (a, b).2 • s • (a', b').1
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: 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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
⊢ mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = mk ((t₂ * s) • m₁ + (t₁ * s) • m₂) (t₁ * s * (t₂ * s))

Tactic:
mul_smul,

Goal state after:
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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
⊢ mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = mk (t₂ • s • m₁ + t₁ • s • m₂) (t₁ * s * (t₂ * s))
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
⊢ f.inv.app X ≫ M.δ.app X = N.δ.app X ≫ f.inv.app (N.obj X) ≫ M.map (f.inv.app X)

Tactic:
rw [← NatIso.cancel_natIso_hom_left f]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
⊢ f.hom.app X ≫ f.inv.app X ≫ M.δ.app X = f.hom.app X ≫ N.δ.app X ≫ f.inv.app (N.obj X) ≫ M.map (f.inv.app X)
Module: Mathlib.CategoryTheory.Adjunction.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : (F.op ⋙ (cones J D).obj K).obj X
j j' : J
f : j ⟶ j'
⊢ (unop ((const J).op.obj X)).map f ≫ (adj.homEquiv (unop X) (K.obj j')) (t.app j') =
    (adj.homEquiv ((unop ((const J).op.obj X)).obj j) (K.obj j')) (t.app j ≫ K.map f)

Tactic:
← t.naturality,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : (F.op ⋙ (cones J D).obj K).obj X
j j' : J
f : j ⟶ j'
⊢ (unop ((const J).op.obj X)).map f ≫ (adj.homEquiv (unop X) (K.obj j')) (t.app j') =
    (adj.homEquiv ((unop ((const J).op.obj X)).obj j) (K.obj j'))
      ((unop ((const J).op.obj (F.op.obj X))).map f ≫ t.app j')
Module: Mathlib.CategoryTheory.Adjunction.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : ((cones J C).obj (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
⊢ (unop ((const J).op.obj (F.op.obj X))).map f ≫ (adj.homEquiv (unop X) (K.obj j')).symm (t.app j') =
    (adj.homEquiv (unop X) (K.obj j')).symm (t.app j ≫ G.map (K.map f))

Tactic:
← t.naturality,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : ((cones J C).obj (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
⊢ (unop ((const J).op.obj (F.op.obj X))).map f ≫ (adj.homEquiv (unop X) (K.obj j')).symm (t.app j') =
    (adj.homEquiv (unop X) (K.obj j')).symm ((unop ((const J).op.obj X)).map f ≫ t.app j')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ (↑b * ↑b') • g a = ↑b • b' • g a

Tactic:
mul_smul,

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑b • ↑b' • g a = ↑b • b' • g a
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ (↑b' * ↑b) • g a' = ↑b' • g (b • a')

Tactic:
mul_smul,

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑b' • ↑b • g a' = ↑b' • g (b • a')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ (↑b' * ↑b) • f a' = ↑b' • b • f a'

Tactic:
mul_smul,

Goal state after:
case e_a
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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑b' • ↑b • f a' = ↑b' • b • f a'
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
m : M'
a : M
b : ↥S
eq1 : b • m = f a
⊢ (⋯.choose.2 * b) • m = ⋯.choose.2 • f a

Tactic:
mul_smul,

Goal state after:
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
m : M'
a : M
b : ↥S
eq1 : b • m = f a
⊢ ⋯.choose.2 • b • m = ⋯.choose.2 • f a
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right.right
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
h' : A ⊗[R] B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
a : A
b : B
⊢ h' (a ⊗ₜ[R] b) = (Algebra.TensorProduct.productMap f' g') (a ⊗ₜ[R] b)

Tactic:
simp only [f', g', ← eq1, pushoutCocone_pt, ← eq2, AlgHom.toRingHom_eq_coe,
      Algebra.TensorProduct.productMap_apply_tmul, AlgHom.coe_mk]

Goal state after:
case property.right.right
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
h' : A ⊗[R] B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
a : A
b : B
⊢ h' (a ⊗ₜ[R] b) =
    (Hom.hom (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h)) a *
      (Hom.hom (ofHom ↑Algebra.TensorProduct.includeRight ≫ h)) b