mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α✝ : Type u₀
β✝ : Type u₁
x✝ : bicompr G F α✝ β✝
⊢ bimap id id x✝ = x✝

pp: case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u₀
β₀✝ β₁✝ β₂✝ : Type u₁
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : bicompr G F α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝

Tactic:
<;>

Goal state after:
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α✝ : Type u₀
β✝ : Type u₁
x✝ : bicompr G F α✝ β✝
⊢ bimap id id x✝ = x✝

case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u₀
β₀✝ β₁✝ β₂✝ : Type u₁
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : bicompr G F α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case empty
R : Type u
inst✝² : CommSemiring R
ι : Type u_3
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Submonoid R
a : ι → A
s : ι → ↥S
⊢ ∏ i ∈ ∅, mk (a i) (s i) = mk (∏ i ∈ ∅, a i) (∏ i ∈ ∅, s i)

pp: case cons
R : Type u
inst✝² : CommSemiring R
ι : Type u_3
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Submonoid R
a : ι → A
s : ι → ↥S
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∏ i ∈ s✝, mk (a i) (s i) = mk (∏ i ∈ s✝, a i) (∏ i ∈ s✝, s i)
⊢ ∏ i ∈ Finset.cons a✝¹ s✝ h✝, mk (a i) (s i) = mk (∏ i ∈ Finset.cons a✝¹ s✝ h✝, a i) (∏ i ∈ Finset.cons a✝¹ s✝ h✝, s i)

Tactic:
<;>

Goal state after:
case empty
R : Type u
inst✝² : CommSemiring R
ι : Type u_3
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Submonoid R
a : ι → A
s : ι → ↥S
⊢ ∏ i ∈ ∅, mk (a i) (s i) = mk (∏ i ∈ ∅, a i) (∏ i ∈ ∅, s i)

case cons
R : Type u
inst✝² : CommSemiring R
ι : Type u_3
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Submonoid R
a : ι → A
s : ι → ↥S
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∏ i ∈ s✝, mk (a i) (s i) = mk (∏ i ∈ s✝, a i) (∏ i ∈ s✝, s i)
⊢ ∏ i ∈ Finset.cons a✝¹ s✝ h✝, mk (a i) (s i) = mk (∏ i ∈ Finset.cons a✝¹ s✝ h✝, a i) (∏ i ∈ Finset.cons a✝¹ s✝ h✝, s i)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ IsLocalization.mk' T 1 1 • mk m s = mk m s

Tactic:
mk'_smul_mk,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ mk (1 • m) (1 * s) = mk m s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ IsLocalization.mk' T ((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1)
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2) •
      mk m s =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2 • mk m s

Tactic:
mk'_smul_mk,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ mk (((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1) • m)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s) =
    mk ((IsLocalization.sec S x).1 • (IsLocalization.sec S y).1 • m)
      ((IsLocalization.sec S x).2 * ((IsLocalization.sec S y).2 * s))
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x y : FreeRing α
⊢ toFreeCommRing (x - y) = toFreeCommRing x - toFreeCommRing y

Tactic:
map_sub

Goal state after:
α : Type u
x y : FreeRing α
⊢ toFreeCommRing x - toFreeCommRing y = toFreeCommRing x - toFreeCommRing y
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
            (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2) *
          ↑s)
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s) •
      mk m s =
    mk
      (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1 • m)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s))

Tactic:
mk'_smul_mk,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ mk
      ((((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
            (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2) *
          ↑s) •
        m)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s) =
    mk
      (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1 • m)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s))
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case hC
α : Type u
x✝ : ℤ
m✝ : α →₀ ℕ
⊢ MvPolynomial.coeff m✝
      ((((FreeCommRing.lift fun a ↦ MvPolynomial.X a).comp
              (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of)).comp
          MvPolynomial.C)
        x✝) =
    MvPolynomial.coeff m✝ (((RingHom.id (MvPolynomial α ℤ)).comp MvPolynomial.C) x✝)

pp: case hX
α : Type u
i✝ : α
m✝ : α →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((FreeCommRing.lift fun a ↦ MvPolynomial.X a).comp
          (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of))
        (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ ((RingHom.id (MvPolynomial α ℤ)) (MvPolynomial.X i✝))

Tactic:
<;>

Goal state after:
case hC
α : Type u
x✝ : ℤ
m✝ : α →₀ ℕ
⊢ MvPolynomial.coeff m✝
      ((((FreeCommRing.lift fun a ↦ MvPolynomial.X a).comp
              (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of)).comp
          MvPolynomial.C)
        x✝) =
    MvPolynomial.coeff m✝ (((RingHom.id (MvPolynomial α ℤ)).comp MvPolynomial.C) x✝)

case hX
α : Type u
i✝ : α
m✝ : α →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((FreeCommRing.lift fun a ↦ MvPolynomial.X a).comp
          (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of))
        (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ ((RingHom.id (MvPolynomial α ℤ)) (MvPolynomial.X i✝))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ IsLocalization.mk' T 0 1 • mk m s = 0

Tactic:
mk'_smul_mk,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ mk (0 • m) (1 * s) = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ IsLocalization.mk' T a s • mk 1 1 = mk ((algebraMap R A) a) s

Tactic:
mk'_smul_mk,

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ mk (a • 1) (s * 1) = mk ((algebraMap R A) a) s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
m : M
s : ↥S
⊢ IsLocalization.mk' T (r * (IsLocalization.sec S x).1) (IsLocalization.sec S x).2 • mk m s =
    r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 • mk m s

Tactic:
mk'_smul_mk,

Goal state after:
case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
m : M
s : ↥S
⊢ mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s) =
    r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 • mk m s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
m : M
s : ↥S
⊢ mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s) =
    r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 • mk m s

Tactic:
mk'_smul_mk,

Goal state after:
case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
m : M
s : ↥S
⊢ mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s) =
    r • mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (b' • a) = ↑⋯.unit⁻¹ (g (↑(b * b') • a))

pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (b • a') = ↑⋯.unit⁻¹ (↑(b * b') • g a')

Tactic:
<;>

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (b' • a) = ↑⋯.unit⁻¹ (g (↑(b * b') • a))

case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (b • a') = ↑⋯.unit⁻¹ (↑(b * b') • g a')
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case left
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
⊢ (A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
      ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom =
    s.ι.app { as := WalkingPair.left }

pp: case right
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
⊢ (A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
      ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom =
    s.ι.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
⊢ (A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
      ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom =
    s.ι.app { as := WalkingPair.left }

case right
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
⊢ (A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
      ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom =
    s.ι.app { as := WalkingPair.right }
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case left
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
a : ↑((pair A B).obj { as := WalkingPair.left })
⊢ (Hom.hom
        ((A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
          ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom))
      a =
    (Hom.hom (s.ι.app { as := WalkingPair.left })) a

pp: case right
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
a : ↑((pair A B).obj { as := WalkingPair.right })
⊢ (Hom.hom
        ((A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
          ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom))
      a =
    (Hom.hom (s.ι.app { as := WalkingPair.right })) a

Tactic:
<;>

Goal state after:
case left
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
a : ↑((pair A B).obj { as := WalkingPair.left })
⊢ (Hom.hom
        ((A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
          ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom))
      a =
    (Hom.hom (s.ι.app { as := WalkingPair.left })) a

case right
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
a : ↑((pair A B).obj { as := WalkingPair.right })
⊢ (Hom.hom
        ((A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
          ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom))
      a =
    (Hom.hom (s.ι.app { as := WalkingPair.right })) a
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
⊢ Function.Surjective (Function.uncurry (mk' f))

Tactic:
intro x
  obtain ⟨⟨m, s⟩, e : s • x = f m⟩ := IsLocalizedModule.surj S f x
  exact ⟨⟨m, s⟩, mk'_eq_iff.mpr e.symm⟩

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case left
A B : CommRingCat
c : Cone (pair A B)
x✝ : ↑c.pt
⊢ (Hom.hom
        (ofHom ((Hom.hom (c.π.app { as := WalkingPair.left })).prod (Hom.hom (c.π.app { as := WalkingPair.right }))) ≫
          (A.prodFan B).π.app { as := WalkingPair.left }))
      x✝ =
    (Hom.hom (c.π.app { as := WalkingPair.left })) x✝

pp: case right
A B : CommRingCat
c : Cone (pair A B)
x✝ : ↑c.pt
⊢ (Hom.hom
        (ofHom ((Hom.hom (c.π.app { as := WalkingPair.left })).prod (Hom.hom (c.π.app { as := WalkingPair.right }))) ≫
          (A.prodFan B).π.app { as := WalkingPair.right }))
      x✝ =
    (Hom.hom (c.π.app { as := WalkingPair.right })) x✝

Tactic:
<;>

Goal state after:
case left
A B : CommRingCat
c : Cone (pair A B)
x✝ : ↑c.pt
⊢ (Hom.hom
        (ofHom ((Hom.hom (c.π.app { as := WalkingPair.left })).prod (Hom.hom (c.π.app { as := WalkingPair.right }))) ≫
          (A.prodFan B).π.app { as := WalkingPair.left }))
      x✝ =
    (Hom.hom (c.π.app { as := WalkingPair.left })) x✝

case right
A B : CommRingCat
c : Cone (pair A B)
x✝ : ↑c.pt
⊢ (Hom.hom
        (ofHom ((Hom.hom (c.π.app { as := WalkingPair.left })).prod (Hom.hom (c.π.app { as := WalkingPair.right }))) ≫
          (A.prodFan B).π.app { as := WalkingPair.right }))
      x✝ =
    (Hom.hom (c.π.app { as := WalkingPair.right })) x✝
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case left
A B : CommRingCat
c : Cone (pair A B)
x✝ : ↑c.pt
⊢ (Hom.hom (ofHom ((Hom.hom (BinaryFan.fst c)).prod (Hom.hom (BinaryFan.snd c))) ≫ (A.prodFan B).fst)) x✝ =
    (Hom.hom (BinaryFan.fst c)) x✝

pp: case right
A B : CommRingCat
c : Cone (pair A B)
x✝ : ↑c.pt
⊢ (Hom.hom (ofHom ((Hom.hom (BinaryFan.fst c)).prod (Hom.hom (BinaryFan.snd c))) ≫ (A.prodFan B).snd)) x✝ =
    (Hom.hom (BinaryFan.snd c)) x✝

Tactic:
<;>

Goal state after:
case left
A B : CommRingCat
c : Cone (pair A B)
x✝ : ↑c.pt
⊢ (Hom.hom (ofHom ((Hom.hom (BinaryFan.fst c)).prod (Hom.hom (BinaryFan.snd c))) ≫ (A.prodFan B).fst)) x✝ =
    (Hom.hom (BinaryFan.fst c)) x✝

case right
A B : CommRingCat
c : Cone (pair A B)
x✝ : ↑c.pt
⊢ (Hom.hom (ofHom ((Hom.hom (BinaryFan.fst c)).prod (Hom.hom (BinaryFan.snd c))) ≫ (A.prodFan B).snd)) x✝ =
    (Hom.hom (BinaryFan.snd c)) x✝
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv

Tactic:
rw [F'.mapCompIso_inv, ← LaxFunctor.mapComp_naturality_right, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_1.refine_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ ((binaryProductFunctor.obj X).map x✝ ≫
        ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom) ≫
      prod.fst =
    (((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
        (prod.functor.obj X).map x✝) ≫
      prod.fst

pp: case h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ ((binaryProductFunctor.obj X).map x✝ ≫
        ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom) ≫
      prod.snd =
    (((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
        (prod.functor.obj X).map x✝) ≫
      prod.snd

Tactic:
<;>

Goal state after:
case refine_1.refine_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ ((binaryProductFunctor.obj X).map x✝ ≫
        ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom) ≫
      prod.fst =
    (((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
        (prod.functor.obj X).map x✝) ≫
      prod.fst

case h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ ((binaryProductFunctor.obj X).map x✝ ≫
        ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom) ≫
      prod.snd =
    (((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
        (prod.functor.obj X).map x✝) ≫
      prod.snd
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_1.refine_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (↾fun x ↦ (x.1, (ConcreteCategory.hom x✝) x.2)) ≫ ↾_root_.Prod.fst = ↾_root_.Prod.fst

pp: case h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (↾fun x ↦ (x.1, (ConcreteCategory.hom x✝) x.2)) ≫ ↾_root_.Prod.snd = ↾_root_.Prod.snd ≫ x✝

Tactic:
<;>

Goal state after:
case refine_1.refine_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (↾fun x ↦ (x.1, (ConcreteCategory.hom x✝) x.2)) ≫ ↾_root_.Prod.fst = ↾_root_.Prod.fst

case h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (↾fun x ↦ (x.1, (ConcreteCategory.hom x✝) x.2)) ≫ ↾_root_.Prod.snd = ↾_root_.Prod.snd ≫ x✝
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_2.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
            (NatIso.ofComponents
                (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm)
                ⋯).hom).app
        x✝ ≫
      prod.fst =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
                ⋯).hom ≫
            prod.functor.map x✝¹).app
        x✝ ≫
      prod.fst

pp: case h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
            (NatIso.ofComponents
                (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm)
                ⋯).hom).app
        x✝ ≫
      prod.snd =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
                ⋯).hom ≫
            prod.functor.map x✝¹).app
        x✝ ≫
      prod.snd

Tactic:
<;>

Goal state after:
case refine_2.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
            (NatIso.ofComponents
                (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm)
                ⋯).hom).app
        x✝ ≫
      prod.fst =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
                ⋯).hom ≫
            prod.functor.map x✝¹).app
        x✝ ≫
      prod.fst

case h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
            (NatIso.ofComponents
                (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm)
                ⋯).hom).app
        x✝ ≫
      prod.snd =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
                ⋯).hom ≫
            prod.functor.map x✝¹).app
        x✝ ≫
      prod.snd
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_2.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y✝ x✝) (↾_root_.Prod.fst ≫ x✝¹) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.fst =
    ↾_root_.Prod.fst ≫ x✝¹

pp: case h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y✝ x✝) (↾_root_.Prod.fst ≫ x✝¹) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.snd =
    ↾_root_.Prod.snd

Tactic:
<;>

Goal state after:
case refine_2.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y✝ x✝) (↾_root_.Prod.fst ≫ x✝¹) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.fst =
    ↾_root_.Prod.fst ≫ x✝¹

case h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y✝ x✝) (↾_root_.Prod.fst ≫ x✝¹) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.snd =
    ↾_root_.Prod.snd