-- Mathlib/Combinatorics/Quiver/Push.lean
theorem lift_unique (Φ : Push σ ⥤q W') (Φ₀ : Φ.obj = τ) (Φcomp : (of σ ⋙q Φ) = φ) :
    Φ = lift σ φ τ h

Proof state:
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn ⋯
        (Eq.recOn ⋯
          ({ obj := τ,
                map :=
                  @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }.map
            f))

Tactic:
rintro _ _ ⟨⟩

Result:
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
⊢ Φ.map (PushQuiver.arrow f✝) =
    Eq.recOn ⋯
      (Eq.recOn ⋯
        ({ obj := τ,
              map :=
                @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }.map
          (PushQuiver.arrow f✝)))

Proof state:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X = τ X

Tactic:
rw [Φ₀]

Result:
no goals

Proof state:
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) =
    Eq.recOn ⋯
      (Eq.recOn ⋯
        ({ obj := Φ.obj,
              map :=
                @PushQuiver.rec V inst✝¹ W σ (fun X Y x => Φ.obj X ⟶ Φ.obj Y) fun X Y f =>
                  id (⋯.mpr (⋯.mpr ((of σ ⋙q Φ).map f))) }.map
          (PushQuiver.arrow f✝)))

Tactic:
simp only [Prefunctor.comp_map, cast_eq]

Result:
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) = id (⋯.mpr (⋯.mpr (Φ.map ((of σ).map f✝))))

Proof state:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X : Push σ),
    Φ.obj X =
      { obj := τ,
            map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }.obj
        X

Tactic:
intro X

Result:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X =
    { obj := τ,
          map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }.obj
      X

Proof state:
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ Φ =
    { obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }

Tactic:
fapply Prefunctor.ext

Result:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X : Push σ),
    Φ.obj X =
      { obj := τ,
            map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }.obj
        X

case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn ⋯
        (Eq.recOn ⋯
          ({ obj := τ,
                map :=
                  @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }.map
            f))

Proof state:
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ Φ = lift σ φ τ h

Tactic:
dsimp only [of, lift]

Result:
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ Φ =
    { obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }

Proof state:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X =
    { obj := τ,
          map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }.obj
      X

Tactic:
simp only

Result:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X = τ X

Proof state:
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
⊢ Φ.map (PushQuiver.arrow f✝) =
    Eq.recOn ⋯
      (Eq.recOn ⋯
        ({ obj := τ,
              map :=
                @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }.map
          (PushQuiver.arrow f✝)))

Tactic:
subst_vars

Result:
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) =
    Eq.recOn ⋯
      (Eq.recOn ⋯
        ({ obj := Φ.obj,
              map :=
                @PushQuiver.rec V inst✝¹ W σ (fun X Y x => Φ.obj X ⟶ Φ.obj Y) fun X Y f =>
                  id (⋯.mpr (⋯.mpr ((of σ ⋙q Φ).map f))) }.map
          (PushQuiver.arrow f✝)))

Proof state:
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) = id (⋯.mpr (⋯.mpr (Φ.map ((of σ).map f✝))))

Tactic:
rfl

Result:
no goals