-- Mathlib/Combinatorics/Quiver/Push.lean
theorem lift_comp : (of σ ⋙q lift σ φ τ h) = φ

Proof state:
case h_map.h
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)
X Y : V
f : X ⟶ Y
⊢ HEq (⋯.mpr (φ.map f)) (⋯ ▸ ⋯ ▸ φ.map f)

Tactic:
apply (cast_heq _ _).trans

Result:
case h_map.h
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)
X Y : V
f : X ⟶ Y
⊢ HEq (φ.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)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2471
γ✝ : Sort ?u.2473
β✝ : α✝ → γ✝ → Sort ?u.2475
a✝ a'✝ : α✝
p✝ : a✝ = a'✝
g✝ : γ✝
b✝ : β✝ a✝ g✝
⊢ HEq (p✝ ▸ b✝) b✝

Tactic:
subst_vars

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)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2471
γ✝ : Sort ?u.2473
β✝ : α✝ → γ✝ → Sort ?u.2475
a'✝ : α✝
g✝ : γ✝
b✝ : β✝ a'✝ g✝
⊢ HEq (⋯ ▸ b✝) b✝

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)
X Y : V
f : X ⟶ Y
⊢ (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
simp only [Prefunctor.comp_map]

Result:
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)
X Y : V
f : X ⟶ Y
⊢ (lift σ φ τ h).map ((of σ).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)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2471
γ✝ : Sort ?u.2473
β✝ : α✝ → γ✝ → Sort ?u.2475
a'✝ : α✝
g✝ : γ✝
b✝ : β✝ a'✝ g✝
⊢ HEq (⋯ ▸ b✝) b✝

Tactic:
rfl

Result:
no goals

Proof state:
case h_map.h
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)
X Y : V
f : X ⟶ Y
⊢ HEq ((lift σ φ τ h).map ((of σ).map f)) (⋯ ▸ ⋯ ▸ φ.map f)

Tactic:
iterate 2 apply (cast_heq _ _).trans

Result:
case h_map.h
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)
X Y : V
f : X ⟶ Y
⊢ HEq (φ.map f) (⋯ ▸ ⋯ ▸ φ.map f)

Proof state:
case h_map.h.h
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)
X Y : V
f : X ⟶ Y
⊢ HEq (⋯ ▸ φ.map f) (φ.map f)

Tactic:
have : ∀ {α γ} {β : α → γ → Sort _} {a a'} (p : a = a') g (b : β a g), HEq (p ▸ b) b := by
  intros
  subst_vars
  rfl

Result:
case h_map.h.h
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)
X Y : V
f : X ⟶ Y
this :
  ∀ {α : Sort ?u.2471} {γ : Sort ?u.2473} {β : α → γ → Sort ?u.2475} {a a' : α} (p : a = a') (g : γ) (b : β a g),
    HEq (p ▸ b) b
⊢ HEq (⋯ ▸ φ.map f) (φ.map f)

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)
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
rintro X Y f

Result:
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)
X Y : V
f : X ⟶ Y
⊢ (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

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)
X Y : V
f : X ⟶ Y
⊢ (lift σ φ τ h).map ((of σ).map f) = ⋯ ▸ ⋯ ▸ φ.map f

Tactic:
apply eq_of_heq

Result:
case h_map.h
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)
X Y : V
f : X ⟶ Y
⊢ HEq ((lift σ φ τ h).map ((of σ).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)
X Y : V
f : X ⟶ Y
⊢ ∀ {α : Sort ?u.2471} {γ : Sort ?u.2473} {β : α → γ → Sort ?u.2475} {a a' : α} (p : a = a') (g : γ) (b : β a g),
    HEq (p ▸ b) b

Tactic:
intros

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)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2471
γ✝ : Sort ?u.2473
β✝ : α✝ → γ✝ → Sort ?u.2475
a✝ a'✝ : α✝
p✝ : a✝ = a'✝
g✝ : γ✝
b✝ : β✝ a✝ g✝
⊢ HEq (p✝ ▸ b✝) b✝

Proof state:
case h_obj.h
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)
X : V
⊢ φ.obj X = (lift σ φ τ h).obj ((of σ).obj X)

Tactic:
exact h X

Result:
no goals

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)
X : V
⊢ (of σ ⋙q lift σ φ τ h).obj X = φ.obj X

Tactic:
simp only [Prefunctor.comp_obj]

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)
X : V
⊢ (lift σ φ τ h).obj ((of σ).obj X) = φ.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)
⊢ of σ ⋙q lift σ φ τ h = φ

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)
⊢ ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.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)
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Proof state:
case h_map.h.h
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)
X Y : V
f : X ⟶ Y
this :
  ∀ {α : Sort ?u.2471} {γ : Sort ?u.2473} {β : α → γ → Sort ?u.2475} {a a' : α} (p : a = a') (g : γ) (b : β a g),
    HEq (p ▸ b) b
⊢ HEq (⋯ ▸ φ.map f) (φ.map f)

Tactic:
apply this

Result:
no goals

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)
⊢ ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X

Tactic:
rintro 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)
X : V
⊢ (of σ ⋙q lift σ φ τ h).obj X = φ.obj X

Proof state:
case h_map.h
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)
X Y : V
f : X ⟶ Y
⊢ HEq (φ.map f) (⋯ ▸ ⋯ ▸ φ.map f)

Tactic:
apply HEq.symm

Result:
case h_map.h.h
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)
X Y : V
f : X ⟶ Y
⊢ HEq (⋯ ▸ ⋯ ▸ φ.map f) (φ.map f)