mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ f (↑(b * b') • a) = ↑b • f (b' • a)

Tactic:
]

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
⊢ f (↑(b * b') • a) = ↑b • f (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' • f (b • a')

Tactic:
]

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' • f (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:
]

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 : R
x : LocalizedModule S M
a : M
b : ↥S
⊢ r • ↑⋯.unit⁻¹ (f a) = r • ↑⋯.unit⁻¹ (f a)

Tactic:
]

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
M'' : Type u_4
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid M''
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module A M'
inst✝⁵ : IsLocalization S A
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
inst✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
r : R
x : LocalizedModule S M
⊢ fromLocalizedModule' S f (r • x) = fromLocalizedModule' S f (r • x)

Tactic:
]

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

Goal state before:
pp: case h.h
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑b • f a' = ↑b' • f a
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'

Tactic:
]

Goal state after:
case h.h
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑b • f a' = ↑b' • f a
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: 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
r : R
⊢ (ConcreteCategory.hom h) ((algebraMap R A) r ⊗ₜ[R] 1) =
    (ConcreteCategory.hom (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h)) ((algebraMap R A) r)

Tactic:
]

Goal state after:
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
r : R
⊢ (ConcreteCategory.hom h) ((algebraMap R A) r ⊗ₜ[R] 1) =
    (ConcreteCategory.hom (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h)) ((algebraMap R A) r)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: 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
r : R
⊢ (↑↑(Hom.hom h)).toFun ((algebraMap R (A ⊗[R] B)) r) = (algebraMap R ↑s.pt) r

Tactic:
change h (algebraMap R A r ⊗ₜ[R] 1) = s.inl (algebraMap R A r)
          rw [← eq1]
          simp only [pushoutCocone_pt, coe_of]
          rfl

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

Goal state before:
pp: case h.h
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑b • f a' = ↑b' • f a
⊢ ↑b' • f a = ↑b' • f a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom =
    (tensorProdObjIsoPushoutObj S A).inv ≫
      (tensorProdObjIsoPushoutObj S A).hom ≫
        Under.homMk
          (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
            (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
          ⋯

Tactic:
]

Goal state after:
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom =
    (tensorProdObjIsoPushoutObj S A).inv ≫
      (tensorProdObjIsoPushoutObj S A).hom ≫
        Under.homMk
          (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
            (pushout.inr B.hom (ofHom (algebraMap ↑R ↑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_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
m : M
s : ↥S
eq1 : (m, s).2 • x = f (m, s).1
⊢ ↑(m, s).2 • x = ↑s • x

Tactic:
]

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'
⊢ m = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)

Tactic:
]

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'
⊢ m = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: 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' := ⋯ }
this : h' = Algebra.TensorProduct.productMap f' g'
x : ↑(pushoutCocone R A B).pt
⊢ (Algebra.TensorProduct.productMap f' g') x = (Algebra.TensorProduct.productMap f' g') x

Tactic:
]

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'
a : M
b : ↥S
eq1 : b • m = f a
⊢ ⋯.choose.2 • f a = ⋯.choose.2 • f a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: case h₀
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv =
    (pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫
            (tensorProdObjIsoPushoutObj S A).hom ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                  (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
                ⋯)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv

Tactic:
]

Goal state after:
case h₀
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv =
    (pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫
            (tensorProdObjIsoPushoutObj S A).hom ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                  (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
                ⋯)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv
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
⊢ LocalizedModule.mk ?a ?b = LocalizedModule.mk m 1

pp: case 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
m : M
⊢ M

pp: case b
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

pp: case eq1
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
⊢ ?b • f m = f ?a

Tactic:
]

Goal state after:
case eq1
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
⊢ 1 • f m = f m
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv =
    (pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫
            (tensorProdObjIsoPushoutObj S A).hom ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                  (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
                ⋯)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv

Tactic:
]

Goal state after:
case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv =
    (pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫
            (tensorProdObjIsoPushoutObj S A).hom ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                  (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
                ⋯)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv
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
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
⊢ g = g

Tactic:
]

Goal state after:
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) = (Hom.hom h) (a ⊗ₜ[R] b)

Tactic:
]

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 h) (a ⊗ₜ[R] b)
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ ((pushout f).obj x).hom ≫ Hom.right u

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ ((pushout f).obj x).hom ≫ Hom.right u
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
⊢ ∀ {X Y : Under R} (f : X ⟶ Y),
    (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S Y).hom =
      (tensorProdObjIsoPushoutObj S X).hom ≫ (Under.pushout (ofHom (algebraMap ↑R ↑S))).map f

Tactic:
by
    intro A B f
    dsimp
    rw [← cancel_epi (tensorProdObjIsoPushoutObj S A).inv]
    ext : 1
    apply pushout.hom_ext
    · rw [← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right]
      ext x
      simp [mkUnder_right]
    · rw [← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right]
      ext (x : S)
      simp [mkUnder_right]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ (f ≫ pushout.inr x.hom f) ≫ Hom.right u = (f ≫ pushout.inr x.hom f) ≫ Hom.right u

Tactic:
]

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
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ l = l

pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ (l ∘ₗ ↑(iso S f)) ∘ₗ LocalizedModule.mkLinearMap S M = g

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ (l ∘ₗ ↑(iso S f)) ∘ₗ LocalizedModule.mkLinearMap S M = g
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
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ l ∘ₗ ↑(iso S f) ∘ₗ LocalizedModule.mkLinearMap S M = l ∘ₗ f

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ l ∘ₗ ↑(iso S f) ∘ₗ LocalizedModule.mkLinearMap S M = l ∘ₗ f
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
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ ?l = k

pp: case l
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ M' →ₗ[R] M''

pp: case hl
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ ?l ∘ₗ f = k ∘ₗ f

Tactic:
]

Goal state after:
case hl
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ k ∘ₗ f = k ∘ₗ f
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
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
this : initial.to B' = g'
⊢ g'.right = g

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
this : initial.to B' = g'
⊢ g'.right = g