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

State before:
α₁ α₂ : Sort u
β₁ : α₁ → Sort u_1
β₂ : α₂ → Sort u_1
f₁ : (x : α₁) → β₁ x
f₂ : (x : α₂) → β₂ x
type_eq_α : α₁ = α₂
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast type_eq_α a)
⊢ (∀ (x : α₁), HEq (f₁ x) (f₂ (cast type_eq_α x))) → HEq f₁ f₂
Tactic:
cases type_eq_α
State after:
case refl
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
⊢ (∀ (x : α₁), HEq (f₁ x) (f₂ (cast ⋯ x))) → HEq f₁ f₂

State before:
case refl
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
⊢ (∀ (x : α₁), HEq (f₁ x) (f₂ (cast ⋯ x))) → HEq f₁ f₂
Tactic:
apply HEq.funext
State after:
case refl.type_eq
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
⊢ (fun x => β₁ x) = fun x => β₂ (cast ⋯ x)

State before:
case refl.type_eq
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
⊢ (fun x => β₁ x) = fun x => β₂ (cast ⋯ x)
Tactic:
funext x
State after:
case refl.type_eq.h
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
x : α₁
⊢ β₁ x = β₂ (cast ⋯ x)

State before:
case refl.type_eq.h
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
x : α₁
⊢ β₁ x = β₂ (cast ⋯ x)
Tactic:
apply type_eq_β
State after:
no goals