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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
⊢ c.unop.op.π = c.π

Tactic:
simp [Fork.op_π, Cofork.unop_ι]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_3
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (x y : RXn),
    x ∈ adjoin R (Set.range MvPolynomial.X) →
      y ∈ adjoin R (Set.range MvPolynomial.X) →
        x ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
          y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
            x + y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid

Tactic:
intro _ _ _ _ h₁ h₂

Goal state after:
case refine_3
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x✝ y✝ : RXn
hx✝ : x✝ ∈ adjoin R (Set.range MvPolynomial.X)
hy✝ : y✝ ∈ adjoin R (Set.range MvPolynomial.X)
h₁ : x✝ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
h₂ : y✝ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
⊢ x✝ + y✝ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: 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
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ g ≫ k ≫ hr.left = g ≫ k ≫ hr.right

Tactic:
← Category.assoc,

Goal state after:
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
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (g ≫ k) ≫ hr.left = g ≫ k ≫ hr.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: 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
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = g ≫ k ≫ hr.right

Tactic:
← Category.assoc,

Goal state after:
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
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = (g ≫ k) ≫ hr.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: 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
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right

Tactic:
← Category.assoc,

Goal state after:
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
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Initial
inst✝ : (F ⋙ G).Initial
⊢ G.Initial

Tactic:
by
  suffices Final G.op from initial_of_final_op _
  have : Final (F.op ⋙ G.op) := show Final (F ⋙ G).op from inferInstance
  exact final_of_final_comp F.op G.op

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ z ≫ v ≫ h.left = z ≫ v ≫ h.right

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (z ≫ v) ≫ h.left = z ≫ v ≫ h.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = z ≫ v ≫ h.right

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (z ≫ v) ≫ h.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ Ideal.comap ↑f ⊥ = Ideal.map (↑g) (Ideal.comap ↑(f.comp g) ⊥)

Tactic:
AlgHom.comp_toRingHom

Goal state after:
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ Ideal.comap ↑f ⊥ = Ideal.map (↑g) (Ideal.comap ((↑f).comp ↑g) ⊥)
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: 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)
⊢ gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π

Tactic:
← Category.assoc,

Goal state after:
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)
⊢ (gr.left ≫ f) ≫ s.π = gr.right ≫ f ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: 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)
⊢ (gr.left ≫ f) ≫ s.π = gr.right ≫ f ≫ s.π

Tactic:
← Category.assoc,

Goal state after:
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)
⊢ (gr.left ≫ f) ≫ s.π = (gr.right ≫ f) ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ s.fst ≫ pullback.fst f g ≫ f = s.snd ≫ pullback.fst f g ≫ f

Tactic:
← Category.assoc,

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (s.fst ≫ pullback.fst f g) ≫ f = (s.snd ≫ pullback.fst f g) ≫ f
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
⊢ g ≫ (PushoutCocone.mk h k comm).inr ≫ m = g ≫ (PushoutCocone.mk h k comm).inr ≫ p

Tactic:
← Category.assoc,

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
⊢ (g ≫ (PushoutCocone.mk h k comm).inr) ≫ 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 = g ≫ (PushoutCocone.mk h k comm).inr ≫ p

Tactic:
← Category.assoc,

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.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₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv =
    pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄

Tactic:
← Category.assoc,

Goal state after:
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₄)) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv =
    pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
⊢ P f'

Tactic:
let e := sq.flip.isoPushout

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
⊢ P f'
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
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) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫
      snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i) =
    fst f g

Tactic:
rw [Iso.inv_comp_eq]
  simp

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
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) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫
      snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i) =
    snd f g

Tactic:
rw [Iso.inv_comp_eq]
  simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
⊢ ∀ (f g : Arrow C) (x : f ≅ g), W.limitsOfShape J f.hom → W.limitsOfShape J g.hom

Tactic:
by
    rintro ⟨_, _, f⟩ ⟨Y₁, Y₂, g⟩ e ⟨X₁, X₂, c₁, c₂, h₁, h₂, f, hf⟩
    let e₁ := Arrow.leftFunc.mapIso e
    let e₂ := Arrow.rightFunc.mapIso e
    have fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift (Cone.mk _ (c₁.π ≫ f)) :=
      e.inv.w.symm
    let c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const _).map e₁.inv ≫ c₁.π }
    let c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const _).map e₂.inv ≫ c₂.π }
    have h₁' : IsLimit c₁' := IsLimit.ofIsoLimit h₁ (Cone.ext e₁)
    have h₂' : IsLimit c₂' := IsLimit.ofIsoLimit h₂ (Cone.ext e₂)
    obtain hg : h₂'.lift (Cone.mk _ (c₁'.π ≫ f)) = g :=
      h₂'.hom_ext (fun j ↦ by
        rw [h₂'.fac]
        simp [reassoc_of% fac, c₁', c₂'])
    rw [← hg]
    exact ⟨_, _, _, _, h₁', _, _, hf⟩

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
this : (↑e.symm).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S)
⊢ P (algebraMap R S)

Tactic:
apply h₂ hQ

Goal state after:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := ⋯
this : (↑e.symm).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S)
⊢ P (algebraMap R' (R' ⊗[R] S))
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), α ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
this✝² : HasLimit X₁
this✝¹ : HasLimit X₂
this✝ : HasProduct fun j ↦ X₁.obj { as := j }
this : HasProduct fun j ↦ X₂.obj { as := j }
⊢ W α

Tactic:
have hf' := hW _ _ φ (fun j => hf (Discrete.mk j))

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), α ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
this✝² : HasLimit X₁
this✝¹ : HasLimit X₂
this✝ : HasProduct fun j ↦ X₁.obj { as := j }
this : HasProduct fun j ↦ X₂.obj { as := j }
hf' : W (Limits.Pi.map φ)
⊢ W α
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
this✝² : HasColimit X₁
this✝¹ : HasColimit X₂
this✝ : HasCoproduct fun j ↦ X₁.obj { as := j }
this : HasCoproduct fun j ↦ X₂.obj { as := j }
⊢ W α

Tactic:
have hf' := hW _ _ φ (fun j => hf (Discrete.mk j))

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
this✝² : HasColimit X₁
this✝¹ : HasColimit X₂
this✝ : HasCoproduct fun j ↦ X₁.obj { as := j }
this : HasCoproduct fun j ↦ X₂.obj { as := j }
hf' : W (Limits.Sigma.map φ)
⊢ W α
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
this✝² : HasColimit X₁
this✝¹ : HasColimit X₂
this✝ : HasCoproduct fun j ↦ X₁.obj { as := j }
this : HasCoproduct fun j ↦ X₂.obj { as := j }
hf' : W (Limits.Sigma.map φ)
⊢ W α

Tactic:
refine (W.arrow_mk_iso_iff ?_).1 hf'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
this✝² : HasColimit X₁
this✝¹ : HasColimit X₂
this✝ : HasCoproduct fun j ↦ X₁.obj { as := j }
this : HasCoproduct fun j ↦ X₂.obj { as := j }
hf' : W (Limits.Sigma.map φ)
⊢ Arrow.mk (Limits.Sigma.map φ) ≅ Arrow.mk α
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape Jᵒᵖ
⊢ P.op.IsClosedUnderLimitsOfShape J

Tactic:
← isClosedUnderColimitsOfShape_op_iff_op

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape Jᵒᵖ
⊢ P.IsClosedUnderColimitsOfShape Jᵒᵖ
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst : HasPullback f g], P (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
⊢ P f'

Tactic:
have := h.hasPullback

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst : HasPullback f g], P (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
this : HasPullback i₂ g
⊢ P f'