-- 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:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul 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:
have : lift (s.snd ≫ fst _ _ ≫ A.inv) (s.fst ≫ fst _ _) ≫ A.mul =
    lift (s.snd ≫ snd _ _) (s.fst ≫ snd _ _ ≫ A.inv) ≫ A.mul := by
  rw [← assoc s.fst, eq_lift_inv_right, lift_lift_assoc, ← assoc s.snd, lift_inv_left_eq,
    lift_comp_fst_snd, lift_comp_fst_snd, s.condition]

Result:
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

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.X A.X A.X).hom ≫ A.X ◁ A.mul) ≫
      fst A.X A.X =
    s.snd ≫ fst 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
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 =
    (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

Tactic:
refine ChosenFiniteProducts.hom_ext _ _ (ChosenFiniteProducts.hom_ext _ _ ?_ ?_) ?_

Result:
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

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
⊢ (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

case refine_3
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 ≫ snd (A.X ⊗ 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 ≫
      snd (A.X ⊗ A.X) A.X

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.X A.X A.X).hom ≫ A.X ◁ A.mul =
      s.snd

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.X A.X A.X).hom ≫ A.X ◁ A.mul) ≫
      snd A.X A.X =
    s.snd ≫ snd A.X A.X

Proof state:
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),
    m ≫ A.mul ▷ A.X = s.fst →
      m ≫ (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul = s.snd →
        m =
          (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

Tactic:
intro s m hm₁ hm₂

Result:
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 =
    (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

Proof state:
case refine_3
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 ≫ snd (A.X ⊗ 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 ≫
      snd (A.X ⊗ A.X) A.X

Tactic:
simpa using hm₁ =≫ snd _ _

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
⊢ A.mul ▷ A.X ≫ A.mul = ((α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul) ≫ A.mul

Tactic:
simp

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
⊢ (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 h : m ≫ fst _ _ ≫ fst _ _ = s.snd ≫ fst _ _ := by simpa using 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
⊢ (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

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 ≫ 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

Tactic:
rw [← assoc s.fst, eq_lift_inv_right, lift_lift_assoc, ← assoc s.snd, lift_inv_left_eq,
  lift_comp_fst_snd, lift_comp_fst_snd, s.condition]

Result:
no goals