Theorem: hcongr_fun (Qpf/Util/HEq.lean)

State before:
α : Sort u_1
P P' : α → Sort u_2
f : (a : α) → P a
f' : (a : α) → P' a
a : α
H₁ : HEq f f'
H₂ : P = P'
⊢ HEq (f a) (f' a)
Tactic:
cases H₂
State after:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
f' : (a : α) → P a
H₁ : HEq f f'
⊢ HEq (f a) (f' a)

State before:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
f' : (a : α) → P a
H₁ : HEq f f'
⊢ HEq (f a) (f' a)
Tactic:
cases H₁
State after:
case refl.refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
⊢ HEq (f a) (f a)

State before:
case refl.refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
⊢ HEq (f a) (f a)
Tactic:
apply HEq.rfl
State after:
no goals