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

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

State before:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
⊢ HEq (f a) (f' a)
Tactic:
apply hcongr_fun _ H₁
State after:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
⊢ (fun a => P a) = fun a => P' a

State before:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
⊢ (fun a => P a) = fun a => P' a
Tactic:
funext a
State after:
case refl.h
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a✝ : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
a : α
⊢ P a = P' a

State before:
case refl.h
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a✝ : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
a : α
⊢ P a = P' a
Tactic:
simp [cast_eq] at H₃
State after:
case refl.h
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a✝ : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃✝ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃✝ a)
a : α
H₃ : True
⊢ P a = P' a

State before:
case refl.h
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a✝ : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃✝ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃✝ a)
a : α
H₃ : True
⊢ P a = P' a
Tactic:
apply H₄
State after:
no goals