[GOAL]
α α' : Sort u
β β' : Sort v
h : α = α'
h' : α' → β = β'
⊢ (α → β) = (α' → β')
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Sort u
β β' : Sort v
h' : α → β = β'
⊢ (α → β) = (α → β')
[PROOFSTEP]
show (∀ (x : α), (fun _ => β) x) = _
[GOAL]
case refl
α : Sort u
β β' : Sort v
h' : α → β = β'
⊢ ((x : α) → (fun x => β) x) = (α → β')
[PROOFSTEP]
rw [funext h']
[GOAL]
α✝ : Sort u_1
x y : α✝
p : HEq x y → Prop
h : ∀ (he : x = y), p (_ : HEq x y)
he : HEq x y
⊢ p he
[PROOFSTEP]
cases he
[GOAL]
case refl
α✝ : Sort u_1
x : α✝
p : HEq x x → Prop
h : ∀ (he : x = x), p (_ : HEq x x)
⊢ p (_ : HEq x x)
[PROOFSTEP]
exact h rfl
[GOAL]
x y : Prop
p : x = y → Prop
h : ∀ (he : x ↔ y), p (_ : x = y)
he : x = y
⊢ p he
[PROOFSTEP]
cases he
[GOAL]
case refl
x : Prop
p : x = x → Prop
h : ∀ (he : x ↔ x), p (_ : x = x)
⊢ p (_ : x = x)
[PROOFSTEP]
exact h Iff.rfl
