-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem isPullback (A : Grp_ C) :
    IsPullback (A.mul ▷ A.X) ((α_ A.X A.X A.X).hom ≫ (A.X ◁ A.mul)) A.mul A.mul where
  w

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
m : s.pt ⟶ (A.X ⊗ A.X) ⊗ A.X
hm₁ : m ≫ A.mul ▷ A.X = s.fst
hm₂ : m ≫ (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul = s.snd
h : m ≫ fst (A.X ⊗ A.X) A.X ≫ fst A.X A.X = s.snd ≫ fst A.X A.X
this : (m ≫ A.mul ▷ A.X) ≫ fst A.X A.X = s.fst ≫ fst A.X A.X
⊢ (m ≫ fst (A.X ⊗ A.X) A.X) ≫ snd A.X A.X =
    ((fun s =>
            lift (lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul))
              (s.fst ≫ snd A.X A.X))
          s ≫
        fst (A.X ⊗ A.X) A.X) ≫
      snd A.X A.X

Tactic:
simp only [assoc, whiskerRight_fst, lift_fst, lift_snd] at this ⊢

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
m : s.pt ⟶ (A.X ⊗ A.X) ⊗ A.X
hm₁ : m ≫ A.mul ▷ A.X = s.fst
hm₂ : m ≫ (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul = s.snd
h : m ≫ fst (A.X ⊗ A.X) A.X ≫ fst A.X A.X = s.snd ≫ fst A.X A.X
this : m ≫ fst (A.X ⊗ A.X) A.X ≫ A.mul = s.fst ≫ fst A.X A.X
⊢ m ≫ fst (A.X ⊗ A.X) A.X ≫ snd A.X A.X = lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
m : s.pt ⟶ (A.X ⊗ A.X) ⊗ A.X
hm₁ : m ≫ A.mul ▷ A.X = s.fst
hm₂ : m ≫ (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul = s.snd
⊢ (m ≫ fst (A.X ⊗ A.X) A.X) ≫ fst A.X A.X =
    ((fun s =>
            lift (lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul))
              (s.fst ≫ snd A.X A.X))
          s ≫
        fst (A.X ⊗ A.X) A.X) ≫
      fst A.X A.X

Tactic:
simpa using hm₂ =≫ fst _ _

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
this :
  lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul =
    lift (s.snd ≫ snd A.X A.X) (s.fst ≫ snd A.X A.X ≫ A.inv) ≫ A.mul
⊢ lift (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul) (s.fst ≫ snd A.X A.X) ≫ A.mul =
    s.snd ≫ snd A.X A.X

Tactic:
rw [this, lift_lift_assoc, ← assoc, lift_comp_inv_left, lift_comp_one_right]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
⊢ ((fun s =>
            lift (lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul))
              (s.fst ≫ snd A.X A.X))
          s ≫
        A.mul ▷ A.X) ≫
      fst A.X A.X =
    s.fst ≫ fst A.X A.X

Tactic:
simp only [lift_whiskerRight, lift_fst]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
⊢ lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul) ≫ A.mul =
    s.fst ≫ fst A.X A.X

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
m : s.pt ⟶ (A.X ⊗ A.X) ⊗ A.X
hm₁ : m ≫ A.mul ▷ A.X = s.fst
hm₂ : m ≫ (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul = s.snd
h : m ≫ fst (A.X ⊗ A.X) A.X ≫ fst A.X A.X = s.snd ≫ fst A.X A.X
this : lift (s.snd ≫ fst A.X A.X) (m ≫ fst (A.X ⊗ A.X) A.X ≫ snd A.X A.X) ≫ A.mul = s.fst ≫ fst A.X A.X
⊢ m ≫ fst (A.X ⊗ A.X) A.X ≫ snd A.X A.X = lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul

Tactic:
rwa [← assoc s.snd, eq_lift_inv_left]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
⊢ ((fun s =>
            lift (lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul))
              (s.fst ≫ snd A.X A.X))
          s ≫
        A.mul ▷ A.X) ≫
      snd A.X A.X =
    s.fst ≫ snd A.X A.X

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
⊢ lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul) ≫ A.mul =
    s.fst ≫ fst A.X A.X

Tactic:
rw [← lift_lift_assoc, ← assoc, lift_comp_inv_right, lift_comp_one_left]

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
m : s.pt ⟶ (A.X ⊗ A.X) ⊗ A.X
hm₁ : m ≫ A.mul ▷ A.X = s.fst
hm₂ : m ≫ (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul = s.snd
h : m ≫ fst (A.X ⊗ A.X) A.X ≫ fst A.X A.X = s.snd ≫ fst A.X A.X
this : m ≫ fst (A.X ⊗ A.X) A.X ≫ A.mul = s.fst ≫ fst A.X A.X
⊢ m ≫ fst (A.X ⊗ A.X) A.X ≫ snd A.X A.X = lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul

Tactic:
rw [← assoc, ← lift_comp_fst_snd (m ≫ _), assoc, assoc, h] at this

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
m : s.pt ⟶ (A.X ⊗ A.X) ⊗ A.X
hm₁ : m ≫ A.mul ▷ A.X = s.fst
hm₂ : m ≫ (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul = s.snd
h : m ≫ fst (A.X ⊗ A.X) A.X ≫ fst A.X A.X = s.snd ≫ fst A.X A.X
this : lift (s.snd ≫ fst A.X A.X) (m ≫ fst (A.X ⊗ A.X) A.X ≫ snd A.X A.X) ≫ A.mul = s.fst ≫ fst A.X A.X
⊢ m ≫ fst (A.X ⊗ A.X) A.X ≫ snd A.X A.X = lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
⊢ ∀ (s : PullbackCone A.mul A.mul),
    (fun s =>
            lift (lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul))
              (s.fst ≫ snd A.X A.X))
          s ≫
        A.mul ▷ A.X =
      s.fst

Tactic:
refine fun s => ChosenFiniteProducts.hom_ext _ _ ?_ (by simp)

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
⊢ ((fun s =>
            lift (lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul))
              (s.fst ≫ snd A.X A.X))
          s ≫
        A.mul ▷ A.X) ≫
      fst A.X A.X =
    s.fst ≫ fst A.X A.X

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
m : s.pt ⟶ (A.X ⊗ A.X) ⊗ A.X
hm₁ : m ≫ A.mul ▷ A.X = s.fst
hm₂ : m ≫ (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul = s.snd
h : m ≫ fst (A.X ⊗ A.X) A.X ≫ fst A.X A.X = s.snd ≫ fst A.X A.X
⊢ (m ≫ fst (A.X ⊗ A.X) A.X) ≫ snd A.X A.X =
    ((fun s =>
            lift (lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul))
              (s.fst ≫ snd A.X A.X))
          s ≫
        fst (A.X ⊗ A.X) A.X) ≫
      snd A.X A.X

Tactic:
have := hm₁ =≫ fst _ _

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
m : s.pt ⟶ (A.X ⊗ A.X) ⊗ A.X
hm₁ : m ≫ A.mul ▷ A.X = s.fst
hm₂ : m ≫ (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul = s.snd
h : m ≫ fst (A.X ⊗ A.X) A.X ≫ fst A.X A.X = s.snd ≫ fst A.X A.X
this : (m ≫ A.mul ▷ A.X) ≫ fst A.X A.X = s.fst ≫ fst A.X A.X
⊢ (m ≫ fst (A.X ⊗ A.X) A.X) ≫ snd A.X A.X =
    ((fun s =>
            lift (lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul))
              (s.fst ≫ snd A.X A.X))
          s ≫
        fst (A.X ⊗ A.X) A.X) ≫
      snd A.X A.X