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

Goal state before:
pp: case refine_1.h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ coprod.inl ≫ (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ coprod.desc s.inr (coprod.inr ≫ s.inl) =
    coprod.inl ≫ s.inl

pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ coprod.inr ≫ (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ coprod.desc s.inr (coprod.inr ≫ s.inl) =
    coprod.inr ≫ s.inl

Tactic:
·

Goal state after:
case refine_1.h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ coprod.inl ≫ (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ coprod.desc s.inr (coprod.inr ≫ s.inl) =
    coprod.inl ≫ s.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ coprod.inr ≫ (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ coprod.desc s.inr (coprod.inr ≫ s.inl) =
    coprod.inr ≫ s.inl

Tactic:
·

Goal state after:
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ coprod.inr ≫ (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ coprod.desc s.inr (coprod.inr ≫ s.inl) =
    coprod.inr ≫ s.inl
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
⊢ (OreLocalization.oreEqv S M) a b → r S M a b

pp: case mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
⊢ r S M a b → (OreLocalization.oreEqv S M) a b

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
⊢ (OreLocalization.oreEqv S M) a b → r S M a b
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ coprod.desc s.inr (coprod.inr ≫ s.inl) = s.inr

pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ ∀ {m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt},
    (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl →
      (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr → m = coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ coprod.desc s.inr (coprod.inr ≫ s.inl) = s.inr
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 ≫ t₂.inl ≫ m = t₁.inl ≫ t₂.inl ≫ l₂

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₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂

Tactic:
·

Goal state after:
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 ≫ t₂.inl ≫ m = t₁.inl ≫ t₂.inl ≫ l₂
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
⊢ r S M a b → (OreLocalization.oreEqv S M) a b

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
⊢ r S M a b → (OreLocalization.oreEqv S M) a b
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ ∀ {m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt},
    (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl →
      (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr → m = coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
·

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ ∀ {m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt},
    (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl →
      (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr → m = coprod.desc s.inr (coprod.inr ≫ s.inl)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3.h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : B ⨿ X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ coprod.inl ≫ m = coprod.inl ≫ coprod.desc s.inr (coprod.inr ≫ s.inl)

pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : B ⨿ X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ coprod.inr ≫ m = coprod.inr ≫ coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
·

Goal state after:
case refine_3.h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : B ⨿ X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ coprod.inl ≫ m = coprod.inl ≫ coprod.desc s.inr (coprod.inr ≫ s.inl)
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₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂

Tactic:
·

Goal state after:
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₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : B ⨿ X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ coprod.inr ≫ m = coprod.inr ≫ coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
·

Goal state after:
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : B ⨿ X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ coprod.inr ≫ m = coprod.inr ≫ coprod.desc s.inr (coprod.inr ≫ s.inl)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case lift
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ (s : Fork g g') → s.pt ⟶ (Fork.ofι f ⋯).pt

pp: case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g'), ?lift s ≫ (Fork.ofι f ⋯).ι = s.ι

pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f ⋯).pt), m ≫ (Fork.ofι f ⋯).ι = s.ι → m = ?lift s

Tactic:
·

Goal state after:
case lift
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ (s : Fork g g') → s.pt ⟶ (Fork.ofι f ⋯).pt
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g'), H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ (Fork.ofι f ⋯).ι = s.ι

pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f ⋯).pt),
    m ≫ (Fork.ofι f ⋯).ι = s.ι → m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)

Tactic:
·

Goal state after:
case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g'), H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ (Fork.ofι f ⋯).ι = s.ι
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
⊢ (tensorLeftAlgEquiv M S) (1 ⊗ₜ[R] IsLocalization.mk' (Localization M) x y) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
      (IsLocalization.mk' (Localization M) x y)

Tactic:
let : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra

Goal state after:
R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
⊢ (tensorLeftAlgEquiv M S) (1 ⊗ₜ[R] IsLocalization.mk' (Localization M) x y) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
      (IsLocalization.mk' (Localization M) x y)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f ⋯).pt),
    m ≫ (Fork.ofι f ⋯).ι = s.ι → m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)

Tactic:
·

Goal state after:
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f ⋯).pt),
    m ≫ (Fork.ofι f ⋯).ι = s.ι → m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_1
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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
⊢ t₂.inl ≫ l = s.inl

pp: case refine_2
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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
⊢ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l

Tactic:
·

Goal state after:
case refine_1
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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
⊢ t₂.inl ≫ l = s.inl
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
s : ↥S
⊢ mk 0 s = 0

Tactic:
simp [mk]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
s : ↥S
⊢ mk (-m) s = -mk m s

Tactic:
simp [mk]

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

Goal state before:
pp: case refine_2
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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
⊢ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l

Tactic:
·

Goal state after:
case refine_2
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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
⊢ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case desc
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ (s : Cofork f f') → (Cofork.ofπ g ⋯).pt ⟶ s.pt

pp: case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f'), (Cofork.ofπ g ⋯).π ≫ ?desc s = s.π

pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt), (Cofork.ofπ g ⋯).π ≫ m = s.π → m = ?desc s

Tactic:
·

Goal state after:
case desc
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ (s : Cofork f f') → (Cofork.ofπ g ⋯).pt ⟶ s.pt
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f'), (Cofork.ofπ g ⋯).π ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π

pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt),
    (Cofork.ofπ g ⋯).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
·

Goal state after:
case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f'), (Cofork.ofπ g ⋯).π ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt),
    (Cofork.ofπ g ⋯).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
·

Goal state after:
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt),
    (Cofork.ofπ g ⋯).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_2.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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inl ≫ m = (t₁.pasteHoriz t₂ hi₂).inl ≫ l

pp: case refine_2.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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inr ≫ m = (t₁.pasteHoriz t₂ hi₂).inr ≫ l

Tactic:
·

Goal state after:
case refine_2.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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inl ≫ m = (t₁.pasteHoriz t₂ hi₂).inl ≫ l
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_2.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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inr ≫ m = (t₁.pasteHoriz t₂ hi₂).inr ≫ l

Tactic:
·

Goal state after:
case refine_2.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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inr ≫ m = (t₁.pasteHoriz t₂ hi₂).inr ≫ l
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt ≅ ⋯.cone.pt

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left =
    Iso.hom ?refine_1 ≫ ⋯.cone.π.app WalkingCospan.left

pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
    Iso.hom ?refine_1 ≫ ⋯.cone.π.app WalkingCospan.right

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt ≅ ⋯.cone.pt
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left =
    (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt).hom ≫
      ⋯.cone.π.app WalkingCospan.left

pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
    (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt).hom ≫
      ⋯.cone.π.app WalkingCospan.right

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left =
    (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt).hom ≫
      ⋯.cone.π.app WalkingCospan.left