mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case fst
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
fx : (A ⟶ R) × (σ → ↑R)
x✝ : ↑A
⊢ (Hom.hom
        ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i)))
            ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)) fx)).1)
      x✝ =
    (Hom.hom fx.1) x✝

pp: case snd
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
fx : (A ⟶ R) × (σ → ↑R)
x✝ : σ
⊢ ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i)))
          ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)) fx)).2
      x✝ =
    fx.2 x✝

Tactic:
<;>

Goal state after:
case fst
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
fx : (A ⟶ R) × (σ → ↑R)
x✝ : ↑A
⊢ (Hom.hom
        ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i)))
            ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)) fx)).1)
      x✝ =
    (Hom.hom fx.1) x✝

case snd
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
fx : (A ⟶ R) × (σ → ↑R)
x✝ : σ
⊢ ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i)))
          ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)) fx)).2
      x✝ =
    fx.2 x✝
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
⊢ (R.tensorProd S).map ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ (R.tensorProd S).map f =
    (R.tensorProd S).map ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ (R.tensorProd S).map g

Tactic:
by
    rw [← Functor.map_comp, equalizer_comp, Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : PullbackCone f g
a : c₁ ⟶ c₂
⊢ Over.homMk a.hom ⋯ ≫ (BinaryFan.mk (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)).π.app { as := WalkingPair.left } =
    (BinaryFan.mk (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯)).π.app { as := WalkingPair.left }

pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : PullbackCone f g
a : c₁ ⟶ c₂
⊢ Over.homMk a.hom ⋯ ≫ (BinaryFan.mk (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)).π.app { as := WalkingPair.right } =
    (BinaryFan.mk (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯)).π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : PullbackCone f g
a : c₁ ⟶ c₂
⊢ Over.homMk a.hom ⋯ ≫ (BinaryFan.mk (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)).π.app { as := WalkingPair.left } =
    (BinaryFan.mk (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯)).π.app { as := WalkingPair.left }

case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : PullbackCone f g
a : c₁ ⟶ c₂
⊢ Over.homMk a.hom ⋯ ≫ (BinaryFan.mk (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)).π.app { as := WalkingPair.right } =
    (BinaryFan.mk (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯)).π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Over.Hom.left a.hom ≫ (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app none =
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app none

pp: case some.left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Over.Hom.left a.hom ≫
      (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app (some WalkingPair.left) =
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app (some WalkingPair.left)

pp: case some.right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Over.Hom.left a.hom ≫
      (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app (some WalkingPair.right) =
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app (some WalkingPair.right)

Tactic:
<;>

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Over.Hom.left a.hom ≫ (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app none =
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app none

case some.left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Over.Hom.left a.hom ≫
      (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app (some WalkingPair.left) =
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app (some WalkingPair.left)

case some.right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Over.Hom.left a.hom ≫
      (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app (some WalkingPair.right) =
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.left } =
    (pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.left }

pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.right } =
    (pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.left } =
    (pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.left }

case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.right } =
    (pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.left }) =
    Over.Hom.left ((pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.left })

pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.right }) =
    Over.Hom.left ((pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.right })

Tactic:
<;>

Goal state after:
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.left }) =
    Over.Hom.left ((pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.left })

case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.right }) =
    Over.Hom.left ((pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.right })
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : PushoutCocone f g
a : c₁ ⟶ c₂
⊢ (BinaryCofan.mk (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯)).ι.app { as := WalkingPair.left } ≫
      Under.homMk a.hom ⋯ =
    (BinaryCofan.mk (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)).ι.app { as := WalkingPair.left }

pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : PushoutCocone f g
a : c₁ ⟶ c₂
⊢ (BinaryCofan.mk (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯)).ι.app { as := WalkingPair.right } ≫
      Under.homMk a.hom ⋯ =
    (BinaryCofan.mk (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)).ι.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : PushoutCocone f g
a : c₁ ⟶ c₂
⊢ (BinaryCofan.mk (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯)).ι.app { as := WalkingPair.left } ≫
      Under.homMk a.hom ⋯ =
    (BinaryCofan.mk (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)).ι.app { as := WalkingPair.left }

case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : PushoutCocone f g
a : c₁ ⟶ c₂
⊢ (BinaryCofan.mk (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯)).ι.app { as := WalkingPair.right } ≫
      Under.homMk a.hom ⋯ =
    (BinaryCofan.mk (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)).ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app none ≫ Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app none

pp: case some.left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app (some WalkingPair.left) ≫
      Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app (some WalkingPair.left)

pp: case some.right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app (some WalkingPair.right) ≫
      Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app (some WalkingPair.right)

Tactic:
<;>

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app none ≫ Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app none

case some.left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app (some WalkingPair.left) ≫
      Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app (some WalkingPair.left)

case some.right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app (some WalkingPair.right) ≫
      Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ c.ι.app { as := WalkingPair.left } ≫ Under.homMk m ⋯ =
    (pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.left }

pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ c.ι.app { as := WalkingPair.right } ≫ Under.homMk m ⋯ =
    (pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ c.ι.app { as := WalkingPair.left } ≫ Under.homMk m ⋯ =
    (pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.left }

case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ c.ι.app { as := WalkingPair.right } ≫ Under.homMk m ⋯ =
    (pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Under.Hom.right (c.ι.app { as := WalkingPair.left } ≫ Under.homMk m ⋯) =
    Under.Hom.right ((pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.left })

pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Under.Hom.right (c.ι.app { as := WalkingPair.right } ≫ Under.homMk m ⋯) =
    Under.Hom.right ((pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.right })

Tactic:
<;>

Goal state after:
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Under.Hom.right (c.ι.app { as := WalkingPair.left } ≫ Under.homMk m ⋯) =
    Under.Hom.right ((pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.left })

case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Under.Hom.right (c.ι.app { as := WalkingPair.right } ≫ Under.homMk m ⋯) =
    Under.Hom.right ((pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.right })
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
⊢ ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π.app none =
    { hom := 𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt,
          inv := 𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π.app none

pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
j : J
⊢ ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π.app (some j) =
    { hom := 𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt,
          inv := 𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π.app (some j)

Tactic:
<;>

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
⊢ ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π.app none =
    { hom := 𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt,
          inv := 𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π.app none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
j : J
⊢ ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π.app (some j) =
    { hom := 𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt,
          inv := 𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π.app (some j)
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))

Tactic:
let ι : R.mkUnder (AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
    (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder

Goal state after:
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case h₀
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
⊢ ((𝟭 (P.Over Q X)).map g ≫ Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj B).left) B.hom ⋯) ⋯ ⋯).left ≫
      pullback.fst ((map Q hPf).obj B).hom f =
    (Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯) ⋯ ⋯ ≫
          (map Q hPf ⋙ pullback P Q f).map g).left ≫
      pullback.fst ((map Q hPf).obj B).hom f

pp: case h₁
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
⊢ ((𝟭 (P.Over Q X)).map g ≫ Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj B).left) B.hom ⋯) ⋯ ⋯).left ≫
      pullback.snd ((map Q hPf).obj B).hom f =
    (Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯) ⋯ ⋯ ≫
          (map Q hPf ⋙ pullback P Q f).map g).left ≫
      pullback.snd ((map Q hPf).obj B).hom f

Tactic:
<;>

Goal state after:
case h₀
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
⊢ ((𝟭 (P.Over Q X)).map g ≫ Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj B).left) B.hom ⋯) ⋯ ⋯).left ≫
      pullback.fst ((map Q hPf).obj B).hom f =
    (Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯) ⋯ ⋯ ≫
          (map Q hPf ⋙ pullback P Q f).map g).left ≫
      pullback.fst ((map Q hPf).obj B).hom f

case h₁
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
⊢ ((𝟭 (P.Over Q X)).map g ≫ Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj B).left) B.hom ⋯) ⋯ ⋯).left ≫
      pullback.snd ((map Q hPf).obj B).hom f =
    (Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯) ⋯ ⋯ ≫
          (map Q hPf ⋙ pullback P Q f).map g).left ≫
      pullback.snd ((map Q hPf).obj B).hom f