mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = g ≫ (PushoutCocone.mk h k comm).inr ≫ p

Tactic:
]

Goal state after:
case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = g ≫ (PushoutCocone.mk h k comm).inr ≫ p
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = (f ≫ h) ≫ p

Tactic:
]

Goal state after:
case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = (f ≫ h) ≫ p
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ ((pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ≫ pullback.snd f₃ f₄ =
    pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫
      pullback.snd f₃ f₄

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ ((pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ≫ pullback.snd f₃ f₄ =
    pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫
      pullback.snd f₃ f₄
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ =
    pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄ = pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
⊢ g₂ ≫ pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ =
    g₂ ≫ pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ g₄ ≫ pushout.inr g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) =
    g₄ ≫ pushout.inr g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasPullback f f
inst✝ : Mono f
⊢ IsIso (inv (fst f f))

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasPullback f f
inst✝ : Mono f
⊢ IsIso (inv (fst f f))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom =
    pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)

Tactic:
by
  trans f₁ ≫ l₁
  · congr 1
    exact
      (pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_hom _
        WalkingCospan.left
  · exact pushout.inl_desc _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
H : IsIso (diagonal f)
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝ = x✝

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} C₀
inst✝¹ : Category.{v_2, u_2} C
F : C₀ ⥤ C
X : C
inst✝ : F.Initial
Y : Over X
⊢ IsConnected (CostructuredArrow F Y.left)

Tactic:
]

Goal state after:
C₀ : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} C₀
inst✝¹ : Category.{v_2, u_2} C
F : C₀ ⥤ C
X : C
inst✝ : F.Initial
Y : Over X
⊢ IsConnected (CostructuredArrow F Y.left)
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X
⊢ Mono f

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X
⊢ Mono f
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
⊢ Mono f

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
⊢ Mono f
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
l' : Z ⟶ (IsPullback.cone h).pt
e : (l' ≫ (IsPullback.cone h).fst) ≫ f = (l' ≫ (IsPullback.cone h).snd) ≫ f
⊢ l' ≫ a = l' ≫ a

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso ((IsPullback.isLimit ⋯).conePointUniqueUpToIso (IsPullback.isLimit h)).inv

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso ((IsPullback.isLimit ⋯).conePointUniqueUpToIso (IsPullback.isLimit h)).inv
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄) = pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) =
    pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄ = pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso g
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ P (CommRingCat.Hom.hom f)

Tactic:
by
    convert! hP.1 (f ≫ g).hom (asIso g).symm.commRingCatIsoToRingEquiv H
    simp [← CommRingCat.hom_comp]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
⊢ P.IsStableUnderBaseChange

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
⊢ P.IsStableUnderBaseChange
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P (pullback.fst f g)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P (pullback.fst f g)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
⊢ P
      ((CommRingCat.Hom.hom e₂.toCommRingCatIso.hom).comp
        (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            {
              toFun := fun x ↦
                (CommRingCat.Hom.hom
                    (CommRingCat.ofHom
                      {
                        toFun :=
                          (↑((IsLocalization.toLocalizationMap (Submonoid.powers r) (Localization.Away r)).lift₀
                                ((algebraMap S (Localization.Away (f r))).comp f).toMonoidWithZeroHom ⋯)).toFun,
                        map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))
                  ((CommRingCat.Hom.hom e₁.toCommRingCatIso.hom) x),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))) =
    P (IsLocalization.Away.map R' S' f r)

Tactic:
]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
⊢ P
      ((CommRingCat.Hom.hom e₂.toCommRingCatIso.hom).comp
        (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            {
              toFun := fun x ↦
                (CommRingCat.Hom.hom
                    (CommRingCat.ofHom
                      {
                        toFun :=
                          (↑((IsLocalization.toLocalizationMap (Submonoid.powers r) (Localization.Away r)).lift₀
                                ((algebraMap S (Localization.Away (f r))).comp f).toMonoidWithZeroHom ⋯)).toFun,
                        map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))
                  ((CommRingCat.Hom.hom e₁.toCommRingCatIso.hom) x),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))) =
    P (IsLocalization.Away.map R' S' f r)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g], P g → ∃ T fst snd, IsPullback fst snd f g ∧ P fst
X Y S : C
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : P g
T : C
fst : T ⟶ X
snd : T ⟶ Y
h : IsPullback fst snd f g
hfst : P fst
⊢ P fst

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g], P g → ∃ T fst snd, IsPullback fst snd f g ∧ P fst
X Y S : C
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : P g
T : C
fst : T ⟶ X
snd : T ⟶ Y
h : IsPullback fst snd f g
hfst : P fst
⊢ P fst
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ f ≫ i = f ≫ i

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this✝ : HasPullbacksAlong (Over.mk f).hom
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))
⊢ P
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this✝ : HasPullbacksAlong (Over.mk f).hom
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))
⊢ P
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ g ≫ i = g ≫ i

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_3
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ diagonal i = diagonal i

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hf
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this✝ : HasPullbacksAlong (Over.mk f).hom
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))
⊢ P (Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)))

Tactic:
]

Goal state after:
case hf
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this✝ : HasPullbacksAlong (Over.mk f).hom
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))
⊢ P (Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)))
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hg
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this✝ : HasPullbacksAlong (Over.mk f).hom
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))
⊢ P (Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))

Tactic:
]

Goal state after:
case hg
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this✝ : HasPullbacksAlong (Over.mk f).hom
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))
⊢ P (Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))