mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
⊢ reverseBraiding C = i.toBraidedCategory

Tactic:
dsimp only [reverseBraiding]
  congr
  funext X Y
  exact Iso.ext (braiding_swap_eq_inv_braiding Y X).symm

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d c : RingCon M
x✝ y✝ : M
f✝ : M →+* P
f : c.Quotient →+* P
x y : M
h : c x y
⊢ f ↑x = f ↑y

Tactic:
rw [c.eq.2 h]

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

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + (g (m₁ <• r₂) + f r₁ * g m₂) = f (r₁ * r₂) + (g m₁ * f r₂ + f r₁ * g m₂)

Tactic:
hgf

Goal state after:
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + (g m₁ * f r₂ + f r₁ * g m₂) = f (r₁ * r₂) + (g m₁ * f r₂ + f r₁ * g m₂)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑M₁
ihx : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝
ihy : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) (x✝ + y✝) = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) (x✝ + y✝)

Tactic:
erw [LinearMap.map_add, LinearMap.map_add]; grind

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

Goal state before:
pp: case tmul
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
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s' : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
⊢ (Hom.hom (Counit.map f)) (s' ⊗ₜ[R] (ConcreteCategory.hom g) y) = (Hom.hom g) ((Hom.hom (Counit.map f)) (s' ⊗ₜ[R] y))

Tactic:
erw [Counit.map_hom_apply]

Goal state after:
case tmul
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
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s' : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s' ⊗ₜ[R] (ConcreteCategory.hom g) y) =
    (Hom.hom g) ((Hom.hom (Counit.map f)) (s' ⊗ₜ[R] y))
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯ =
    Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
      Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯

Tactic:
ext : 2

Goal state after:
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
          Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯))
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ ((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
      Under.homMk
        (ofHom
          (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
        ⋯ =
    Under.homMk
        (ofHom
          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
        ⋯ ≫
      (𝟭 (Under R)).map f

Tactic:
ext : 2

Goal state after:
R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ Hom.hom
      (Under.Hom.right
        (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
          Under.homMk
            (ofHom
              (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
            ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk
            (ofHom
              (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
            ⋯ ≫
          (𝟭 (Under R)).map f))
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:
ext : 2

Goal state after:
R : CommRingCat
G : CommMonCat
⊢ Hom.hom
      (Under.Hom.right
        (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))) =
    Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case e_a.e_6
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
⊢ x ^ Exists.choose ⋯ = ↑(IsLocalization.sec (Submonoid.powers x) s).2

Tactic:
exact (IsLocalization.sec (Submonoid.powers x) s).2.property.choose_spec

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

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
n : ℕ
a : R
hn : s * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) (a * ↑u ^ n)

Tactic:
simp [mul_pow, ← mul_assoc, hn]

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

Goal state before:
pp: case refine_1
S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
s : S
⊢ ∃ n a, (algebraMap S T) s * (algebraMap S T) r ^ n = (algebraMap S T) a

Tactic:
exact ⟨0, by simp⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
le : N ≤ Ring.jacobson R • N
⊢ N = ⊥

Tactic:
contrapose! le

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
le : N ≠ ⊥
⊢ ¬N ≤ Ring.jacobson R • N
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
⊢ x ∈ 𝔪₀

Tactic:
have I𝔪₀ : I ≤ 𝔪₀ := fun i iI =>
      𝔪_mem.left (I.mul_mem_right _ iI)

Goal state after:
case neg
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
⊢ x ∈ 𝔪₀
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.jacobson = ⊥
⊢ I.jacobson = I

Tactic:
replace h := congr_arg (comap (Ideal.Quotient.mk I)) h

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : comap (Quotient.mk I) ⊥.jacobson = comap (Quotient.mk I) ⊥
⊢ I.jacobson = I
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
⊢ (((Functor.const J).obj (F.1 i)).map f ≫
      if h : k = i then eqToHom ⋯ else (H k h).from (((Functor.const J).obj (F.1 i)).obj k)) =
    (if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j)) ≫ F.map f

Tactic:
split_ifs with h h_1 h_1

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map f

case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) = eqToHom ⋯ ≫ F.map f

case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) =
    (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ ⇑((map S) l) =
    ⇑(IsLocalizedModule.iso S g₂).symm ∘ ⇑((IsLocalizedModule.map S g₁ g₂) l) ∘ ⇑(IsLocalizedModule.iso S g₁)

Tactic:
rw [← LinearMap.coe_restrictScalars R, restrictScalars_map_eq _ g₁ g₂ l]

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ ⇑(↑(IsLocalizedModule.iso S g₂).symm ∘ₗ (IsLocalizedModule.map S g₁ g₂) l ∘ₗ ↑(IsLocalizedModule.iso S g₁)) =
    ⇑(IsLocalizedModule.iso S g₂).symm ∘ ⇑((IsLocalizedModule.map S g₁ g₂) l) ∘ ⇑(IsLocalizedModule.iso S g₁)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk.mk.mk
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
⊢ mk a₁ s₁ * (mk a₂ s₂ + mk a₃ s₃) = mk (a₁ * a₂) (s₁ * s₂) + mk (a₁ * a₃) (s₁ * s₃)

Tactic:
mk_add_mk,

Goal state after:
case mk.mk.mk
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
⊢ mk a₁ s₁ * mk (s₃ • a₂ + s₂ • a₃) (s₂ * s₃) = mk (a₁ * a₂) (s₁ * s₂) + mk (a₁ * a₃) (s₁ * s₃)
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:
← Iso.eq_comp_inv,

Goal state after:
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' =
    (g' ≫ pushout.inr f (g ≫ g')) ≫ (pushoutLeftPushoutInrIso f g g').inv
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk.mk.mk
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
⊢ (mk a₁ s₁ + mk a₂ s₂) * mk a₃ s₃ = mk (a₁ * a₃) (s₁ * s₃) + mk (a₂ * a₃) (s₂ * s₃)

Tactic:
mk_add_mk,

Goal state after:
case mk.mk.mk
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
⊢ mk (s₂ • a₁ + s₁ • a₂) (s₁ * s₂) * mk a₃ s₃ = mk (a₁ * a₃) (s₁ * s₃) + mk (a₂ * a₃) (s₂ * s₃)
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
f' : Y ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout f' (pushout.inl f g)
⊢ f' ≫ pushout.inl f' (pushout.inl f g) ≫ (pushoutRightPushoutInlIso f g f').hom = f' ≫ pushout.inl (f ≫ f') g

Tactic:
inl_pushoutRightPushoutInlIso_hom

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout f' (pushout.inl f g)
⊢ f' ≫ pushout.inl (f ≫ f') g = f' ≫ pushout.inl (f ≫ f') g
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
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • (mk m s + mk n t) =
    mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s) +
      mk ((IsLocalization.sec S x).1 • n) ((IsLocalization.sec S x).2 * t)

Tactic:
mk_add_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
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • mk (t • m + s • n) (s * t) =
    mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s) +
      mk ((IsLocalization.sec S x).1 • n) ((IsLocalization.sec S x).2 * 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
⊢ (x + y) • mk m s =
    mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s) +
      mk ((IsLocalization.sec S y).1 • m) ((IsLocalization.sec S y).2 * s)

Tactic:
mk_add_mk,

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
⊢ (x + y) • mk m s =
    mk
      (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1 • m)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s))
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 m₁ t₁ + mk m₂ t₂).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
    (mk m₁ t₁).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ + (mk m₂ t₂).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯

Tactic:
mk_add_mk,

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₂)).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
    (mk m₁ t₁).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ + (mk m₂ t₂).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯
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 m₁ (t₁ * s) + mk m₂ (t₂ * s)

Tactic:
mk_add_mk,

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.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_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
⊢ lift' S g h (mk a b + mk a' b') = lift' S g h (mk a b) + lift' S g h (mk a' b')

Tactic:
mk_add_mk,

Goal state after:
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
⊢ lift' S g h (mk (b' • a + b • a') (b * b')) = lift' S g h (mk a b) + lift' S g h (mk a' b')
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case eq
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom =
    ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom

Tactic:
· ext r
    trans algebraMap R (A ⊗[R] B) r
    · exact Algebra.TensorProduct.includeLeft.commutes (R := R) r
    · exact (Algebra.TensorProduct.includeRight.commutes (R := R) r).symm

Goal state after:
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
R₀ : Type u_6
inst✝⁵ : SMul R₀ R
inst✝⁴ : SMul R₀ M
inst✝³ : SMul R₀ M'
inst✝² : IsScalarTower R₀ R R
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsScalarTower R₀ R M'
r : R₀
m : M
s : ↥S
⊢ mk' f (r • m) s = r • mk' f m s

Tactic:
delta mk'
  rw [← LocalizedModule.smul'_mk, LinearMap.map_smul_of_tower]

Goal state after:
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
s₁ s₂ : ↥S
⊢ mk' f (s₁ • m) (s₁ * s₂) = mk' f m s₂

Tactic:
by
  delta mk'
  rw [LocalizedModule.mk_cancel_common_left]

Goal state after: