mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ m = hc.desc (PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ m = hc.desc (PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: 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✝ : BraidedCategory C
⊢ (ρ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: 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
⊢ t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ i₂ ≫ g₂

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: 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₁
s : PullbackCone (g₁ ≫ g₂) i₃
⊢ s.fst ≫ g₁ ≫ g₂ = s.fst ≫ g₁ ≫ g₂

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: 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₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
⊢ l₂ ≫ t₂.fst = l₂ ≫ t₂.fst

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ snd ≫ g ≫ e₄.hom = snd ≫ g ≫ e₄.hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ fst = fst

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ snd = snd

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case 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₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ s.fst ≫ g₁ = s.fst ≫ g₁

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : IsIso g
this : HasPullback f g
⊢ IsIso (h.isoPullback.hom ≫ pullback.fst f g)

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : IsIso g
this : HasPullback f g
⊢ IsIso (h.isoPullback.hom ≫ pullback.fst f g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
h₁₃ : X₁₁ ⟶ X₁₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
⊢ v₁₁ ≫ h₂₁ ≫ h₂₂ = v₁₁ ≫ h₂₁ ≫ h₂₂

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₃₁ : X₁₁ ⟶ X₃₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁
t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁
⊢ v₃₁ ≫ h₃₁ = v₃₁ ≫ h₃₁

Tactic:
]

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'
inst✝ : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x✝³ : AddCommMonoid Q
x✝² : Module R Q
x✝¹ : Module A Q
x✝ : IsScalarTower R A Q
g : M →ₗ[R] Q
s : ↥S
⊢ IsUnit ((Algebra.lsmul R R Q) ((algebraMap R A) ↑s))

Tactic:
]

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'
inst✝ : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x✝³ : AddCommMonoid Q
x✝² : Module R Q
x✝¹ : Module A Q
x✝ : IsScalarTower R A Q
g : M →ₗ[R] Q
s : ↥S
⊢ IsUnit ((Algebra.lsmul R R Q) ((algebraMap R A) ↑s))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: 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₂
⊢ s.snd ≫ i₂ ≫ g₂ = s.snd ≫ i₂ ≫ g₂

Tactic:
]

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'
h : IsBaseChange A f
this✝ : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x✝ : M
⊢ f x✝ = f x✝

Tactic:
]

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
⊢ IsBaseChange A ↑(IsScalarTower.toAlgHom R T (A ⊗[R] T))

Tactic:
]

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.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_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (algebraMap R A) ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = (algebraMap R A) ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)

Tactic:
]

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_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (algebraMap R A) ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = (algebraMap R A) ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)
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 (fstsndfgr ≫ fstfg) sndsndfgr f (rY ≫ g)

Tactic:
]

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.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₂ ⟶ X₁
f₂ : X₃ ⟶ X₂
i₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone i₂ f₂
hi₂ : i₂ = t₁.snd
⊢ t₂.fst ≫ i₂ ≫ f₁ = t₂.fst ≫ i₂ ≫ f₁

Tactic:
]

Goal state after:
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'
⊢ g ≫ inr ≫ e₄.hom = g ≫ inr ≫ e₄.hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone i₂ f₂
hi₂ : i₂ = t₁.inr
⊢ f₁ ≫ i₂ ≫ t₂.inl = f₁ ≫ i₂ ≫ t₂.inl

Tactic:
]

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
T : Type u_5
B : Type u_6
inst✝⁷ : CommSemiring T
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra T B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R T B
inst✝ : IsScalarTower R A B
⊢ IsLocalizedModule S (IsScalarTower.toAlgHom R T B).toLinearMap ↔
    IsBaseChange A (IsScalarTower.toAlgHom R T B).toLinearMap

Tactic:
]

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
T : Type u_5
B : Type u_6
inst✝⁷ : CommSemiring T
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra T B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R T B
inst✝ : IsScalarTower R A B
⊢ IsLocalizedModule S (IsScalarTower.toAlgHom R T B).toLinearMap ↔
    IsBaseChange A (IsScalarTower.toAlgHom R T B).toLinearMap
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
T : Type u_5
B : Type u_6
inst✝⁷ : CommSemiring T
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra T B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R T B
inst✝ : IsScalarTower R A B
⊢ IsLocalizedModule S (IsScalarTower.toAlgHom R T B).toLinearMap ↔
    IsLocalizedModule S (IsScalarTower.toAlgHom R T B).toLinearMap

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
⊢ f₁ ≫ f₂ ≫ s.inr = f₁ ≫ f₂ ≫ s.inr

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
⊢ t₁.inr ≫ l₁ = t₁.inr ≫ l₁

Tactic:
]

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
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
⊢ IsBaseChange (Localization S) (↑e'.symm ∘ₗ Finsupp.mapRange.linearMap f)

Tactic:
]

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
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
⊢ IsBaseChange (Localization S) (↑e'.symm ∘ₗ Finsupp.mapRange.linearMap f)
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
inst : IsIso g
this : HasPushout f g
⊢ IsIso (pushout.inl f g ≫ h.isoPushout.inv)

Tactic:
]

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
inst : IsIso g
this : HasPushout f g
⊢ IsIso (pushout.inl f g ≫ h.isoPushout.inv)
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
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₂ ⟶ X₃₂
v₂₁ : X₂₁ ⟶ X₃₁
s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ v₁₁ ≫ v₂₁ ≫ h₃₁ = v₁₁ ≫ v₂₁ ≫ h₃₁

Tactic:
]

Goal state after:
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
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₃ : X₂₁ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ v₁₁ ≫ h₂₃ = v₁₁ ≫ h₂₃

Tactic:
]

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
B : Type u_6
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : CommSemiring B
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T B
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : IsScalarTower R T B
inst✝⁴ : IsScalarTower R A B
S : Submonoid A
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
g : M →ₗ[A] M'
h✝ : IsLocalizedModule S g
Aₚ : Type u_2 := Localization S
this✝¹ : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
this✝ : IsScalarTower A Aₚ M'
h : IsBaseChange Aₚ g
this : IsScalarTower R Aₚ M'
⊢ IsBaseChange Aₚ ((AlgebraTensorModule.rTensor R N) g)

Tactic:
]

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
B : Type u_6
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : CommSemiring B
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T B
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : IsScalarTower R T B
inst✝⁴ : IsScalarTower R A B
S : Submonoid A
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
g : M →ₗ[A] M'
h✝ : IsLocalizedModule S g
Aₚ : Type u_2 := Localization S
this✝¹ : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
this✝ : IsScalarTower A Aₚ M'
h : IsBaseChange Aₚ g
this : IsScalarTower R Aₚ M'
⊢ IsBaseChange Aₚ ((AlgebraTensorModule.rTensor R N) g)
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:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R 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'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ (AlgebraTensorModule.rTensor R P) g ∘ₗ (AlgebraTensorModule.lTensor A M) f =
    (AlgebraTensorModule.lTensor A M') f ∘ₗ (AlgebraTensorModule.rTensor R N) g

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R 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'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ (AlgebraTensorModule.rTensor R P) g ∘ₗ (AlgebraTensorModule.lTensor A M) f =
    (AlgebraTensorModule.lTensor A M') f ∘ₗ (AlgebraTensorModule.rTensor R N) g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case h₀
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
⊢ t₁.inl ≫ l₁ = t₁.inl ≫ l₁

Tactic:
]

Goal state after: