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
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
⊢ { l //
    l ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).pt},
          m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd = s.snd → m = l }

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
⊢ ∀
    (s :
      PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
        (hT.from ((pair X Y).obj { as := WalkingPair.right }))),
    BinaryFan.IsLimit.lift hc s.fst s.snd ≫ c.fst = s.fst

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
⊢ ∀
    (s :
      PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
        (hT.from ((pair X Y).obj { as := WalkingPair.right }))),
    BinaryFan.IsLimit.lift hc s.fst s.snd ≫ c.snd = s.snd

Tactic:
by

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'
⊢ IsLocalizedModule S f ↔ IsBaseChange A f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
s : ↥S
⊢ (equivTensorProduct S M).symm (Localization.mk r s ⊗ₜ[R] x) = r • mk x s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (equivTensorProduct S M).symm (1 ⊗ₜ[R] x) = mk x 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
s : ↥S
⊢ (equivTensorProduct S M) (mk x s) = Localization.mk 1 s ⊗ₜ[R] x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
s :
  PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
    (hT.from ((pair X Y).obj { as := WalkingPair.right }))
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
h₁ : m ≫ c.fst = s.fst
h₂ : m ≫ c.snd = s.snd
⊢ m = BinaryFan.IsLimit.lift hc s.fst s.snd

Tactic:
by

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

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

Tactic:
by

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
w : fst ≫ f = snd ≫ g
hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : T ⟶ P⦄, φ ≫ fst = φ' ≫ fst → φ ≫ snd = φ' ≫ snd → φ = φ'
exists_lift : ∀ ⦃T : C⦄ (a : T ⟶ X) (b : T ⟶ Y), a ≫ f = b ≫ g → ∃ l, l ≫ fst = a ∧ l ≫ snd = b
⊢ Nonempty (IsLimit (PullbackCone.mk fst snd w))

Tactic:
by

Goal state after:
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 sndsndfgr sndfi rZ

Tactic:
by

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 Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst✝³ : HasPullback i g
h : U ⟶ pullback i g
inst✝² : HasPullback f g
inst✝¹ : HasPullback (pullback.snd f g) (h ≫ pullback.snd i g)
inst✝ : HasPullback f i
⊢ (h ≫ pullback.snd i g) ≫ g = (h ≫ pullback.fst i g) ≫ i

Tactic:
simp [pullback.condition]

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 Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst✝³ : HasPullback i g
h : U ⟶ pullback i g
inst✝² : HasPullback f g
inst✝¹ : HasPullback (pullback.snd f g) (h ≫ pullback.snd i g)
inst✝ : HasPullback f i
⊢ (h ≫ pullback.snd i g) ≫ g = (h ≫ pullback.fst i g) ≫ i

Tactic:
by

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_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₂
a : A
x✝¹ : M₁
x✝ : M₂
⊢ (a • x✝¹) ⊗ₜ[R] x✝ = x✝¹ ⊗ₜ[R] (a • x✝)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst✝³ : HasPullback i g
h : U ⟶ pullback i g
inst✝² : HasPullback f g
inst✝¹ : HasPullback (pullback.snd f g) (h ≫ pullback.snd i g)
inst✝ : HasPullback f i
⊢ (h ≫ pullback.snd i g) ≫ g = (h ≫ pullback.fst i g) ≫ i

Tactic:
simp [pullback.condition]

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₂.pasteHoriz t₁ hi₂)
⊢ IsLimit t₁

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst✝³ : HasPullback i g
h : U ⟶ pullback i g
inst✝² : HasPullback f g
inst✝¹ : HasPullback (pullback.snd f g) (h ≫ pullback.snd i g)
inst✝ : HasPullback f i
⊢ (h ≫ pullback.snd i g) ≫ g = (h ≫ pullback.fst i g) ≫ i

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst✝³ : HasPullback i g
h : U ⟶ pullback i g
inst✝² : HasPullback f g
inst✝¹ : HasPullback (pullback.snd f g) (h ≫ pullback.snd i g)
inst✝ : HasPullback f i
⊢ pullback.map (pullback.snd f g) (h ≫ pullback.snd i g) f i (pullback.fst f g) (h ≫ pullback.fst i g) g ⋯ ⋯ ≫
      pullback.fst f i =
    pullback.fst (pullback.snd f g) (h ≫ pullback.snd i g) ≫ pullback.fst f g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst✝³ : HasPullback i g
h : U ⟶ pullback i g
inst✝² : HasPullback f g
inst✝¹ : HasPullback (pullback.snd f g) (h ≫ pullback.snd i g)
inst✝ : HasPullback f i
⊢ pullback.map (pullback.snd f g) (h ≫ pullback.snd i g) f i (pullback.fst f g) (h ≫ pullback.fst i g) g ⋯ ⋯ ≫
      pullback.snd f i =
    pullback.snd (pullback.snd f g) (h ≫ pullback.snd i g) ≫ h ≫ pullback.fst i g

Tactic:
by

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 : C
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ ∀ (j : Discrete WalkingPair),
    c.ι.app j ≫ (Iso.refl c.pt).hom =
      (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι.app j

Tactic:
by

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₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone i₂ f₂
hi₂ : i₂ = t₁.snd
⊢ (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.snd ≫ f₂ ≫ f₁

Tactic:
by

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'
⊢ f' ≫ inl' = g' ≫ inr'

Tactic:
by

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₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone «i₂» f₂
hi₂ : «i₂» = t₁.snd
⊢ (t₁.pasteVert t₂ hi₂).flip.fst = (Iso.refl (t₁.pasteVert t₂ hi₂).flip.pt).hom ≫ (t₁.flip.pasteHoriz t₂.flip hi₂).fst

Tactic:
by

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₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone «i₂» f₂
hi₂ : «i₂» = t₁.snd
⊢ (t₁.pasteVert t₂ hi₂).flip.snd = (Iso.refl (t₁.pasteVert t₂ hi₂).flip.pt).hom ≫ (t₁.flip.pasteHoriz t₂.flip hi₂).snd

Tactic:
by

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₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone «i₂» f₂
hi₂ : «i₂» = t₁.snd
H₁ : IsLimit t₁
H₂ : IsLimit t₂
⊢ IsLimit (t₁.pasteVert t₂ hi₂)

Tactic:
by

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
⊢ i₁ ≫ t₁.inl ≫ t₂.inl = (f₁ ≫ f₂) ≫ t₂.inr

Tactic:
by

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'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
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₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
⊢ IsLocalizedModule S (TensorProduct.map f g)

Tactic:
by

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
⊢ IsLocalization (algebraMapSubmonoid T S) B ↔ IsPushout R T A B

Tactic:
by

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

Goal state before:
pp: M : Type u_7
N : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_9
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
⊢ map f (IsUnit.submonoid M) ≤ IsUnit.submonoid N

Tactic:
by

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

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
⊢ algebraMapSubmonoid S (IsUnit.submonoid R) ≤ IsUnit.submonoid S

Tactic:
by

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
T : Type u_5
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra A T
inst✝ : IsScalarTower R A T
H : Function.Bijective ⇑(algebraMap R A)
⊢ IsPushout R T A T

Tactic:
by

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
T : Type u_5
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra A T
inst✝ : IsScalarTower R A T
H : Function.Bijective ⇑(algebraMap A T)
⊢ IsLocalization (algebraMapSubmonoid A (IsUnit.submonoid R)) T

Tactic:
by

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
T : Type u_5
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra A T
inst✝ : IsScalarTower R A T
H : Function.Bijective ⇑(algebraMap A T)
⊢ IsPushout R A R T

Tactic:
by

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₂)
⊢ i₁ ≫ s.inl = f₁ ≫ f₂ ≫ s.inr

Tactic:
by

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 : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ IsPushout f' g' inl' inr'

Tactic:
by

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
this : IsLocalizedModule S (↑e'.symm ∘ₗ Finsupp.mapRange.linearMap f)
⊢ IsLocalizedModule S (Finsupp.mapRange.linearMap f)

Tactic:
by

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
⊢ «i₂» ≫ l₁ = f₂ ≫ s.inr

Tactic:
by

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
inst : Epi g
W : C
fst' snd' : P ⟶ W
heq : inl ≫ fst' = inl ≫ snd'
⊢ inr ≫ fst' = inr ≫ snd'

Tactic:
by

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
inst : Epi g
⊢ Epi inl

Tactic:
by

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
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inl ≫ l₂ = s.inl

Tactic:
by

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
inst : IsIso g
⊢ IsIso inl

Tactic:
by

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₃₂
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₂₁
⊢ h₁₁ ≫ v₁₃ = v₁₁ ≫ v₂₁ ≫ h₃₁

Tactic:
by

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
a : α
m : M
b : α
this : (if a = b then f m else 0) = e (1 ⊗ₜ[R] if a = b then m else 0)
⊢ e
      (((finsuppRight R R (Localization S) M α) (((↑e'.symm ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ Finsupp.lsingle a) m))
        b) =
    e (((finsuppRight R R (Localization S) M α) (((mk R (Localization S) (α →₀ M)) 1 ∘ₗ Finsupp.lsingle a) m)) b)

Tactic:
by

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₂₁
⊢ h₁₁ ≫ h₁₂ ≫ v₁₃ = v₁₁ ≫ h₂₃

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
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₂₁
⊢ h₁₂ ≫ v₁₃ = v₁₂ ≫ t.desc (h₁₂ ≫ v₁₃) h₂₃ ⋯

Tactic:
by

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
inst✝¹ : Epi f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g), inr ≫ inv inr ≫ s.inr = s.inr

Tactic:
by

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
inst✝¹ : Epi f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g) (m : P ⟶ s.pt), inl ≫ m = s.inl → inr ≫ m = s.inr → m = inv inr ≫ s.inr

Tactic:
by

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
inst✝¹ : Epi f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ IsColimit sq.cocone

Tactic:
by

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 : C
f : Z ⟶ X
⊢ 𝟙 Z ≫ f = f ≫ 𝟙 X

Tactic:
by

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 : C
f : Z ⟶ X
⊢ f ≫ 𝟙 X = 𝟙 Z ≫ f

Tactic:
by

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 : C
f : X ⟶ Z
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
by

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 : C
f : X ⟶ Z
⊢ 𝟙 X ≫ f = f ≫ 𝟙 Z

Tactic:
by

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
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₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl
hm₂ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr
⊢ t₂.inr ≫ m = t₂.inr ≫ l₂

Tactic:
by

Goal state after: