Theorem: cast_arg' (Qpf/Util/HEq.lean)

State before:
α : Sort u₁
β β' : α → Sort u₂
f : (a : α) → β a
a : α
h₁ : ((a : α) → β a) = ((a : α) → β' a)
h₂ : ∀ (a : α), β a = β' a
⊢ cast h₁ f a = cast ⋯ (f a)
Tactic:
apply cast_arg
State after:
case h₁
α : Sort u₁
β β' : α → Sort u₂
f : (a : α) → β a
a : α
h₁ : ((a : α) → β a) = ((a : α) → β' a)
h₂ : ∀ (a : α), β a = β' a
⊢ α = α

State before:
case h₁
α : Sort u₁
β β' : α → Sort u₂
f : (a : α) → β a
a : α
h₁ : ((a : α) → β a) = ((a : α) → β' a)
h₂ : ∀ (a : α), β a = β' a
⊢ α = α
Tactic:
rfl
State after:
no goals