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

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

State before:
case refl
α : Sort u
β₁ : α → Sort u_1
f₁ f₂ : (x : α) → β₁ x
⊢ (∀ (x : α), HEq (f₁ x) (f₂ x)) → HEq f₁ f₂
Tactic:
intro h
State after:
case refl
α : Sort u
β₁ : α → Sort u_1
f₁ f₂ : (x : α) → β₁ x
h : ∀ (x : α), HEq (f₁ x) (f₂ x)
⊢ HEq f₁ f₂

State before:
case refl
α : Sort u
β₁ : α → Sort u_1
f₁ f₂ : (x : α) → β₁ x
h : ∀ (x : α), HEq (f₁ x) (f₂ x)
⊢ HEq f₁ f₂
Tactic:
apply heq_of_eq
State after:
case refl.h
α : Sort u
β₁ : α → Sort u_1
f₁ f₂ : (x : α) → β₁ x
h : ∀ (x : α), HEq (f₁ x) (f₂ x)
⊢ f₁ = f₂

State before:
case refl.h
α : Sort u
β₁ : α → Sort u_1
f₁ f₂ : (x : α) → β₁ x
h : ∀ (x : α), HEq (f₁ x) (f₂ x)
⊢ f₁ = f₂
Tactic:
funext a
State after:
case refl.h.h
α : Sort u
β₁ : α → Sort u_1
f₁ f₂ : (x : α) → β₁ x
h : ∀ (x : α), HEq (f₁ x) (f₂ x)
a : α
⊢ f₁ a = f₂ a

State before:
case refl.h.h
α : Sort u
β₁ : α → Sort u_1
f₁ f₂ : (x : α) → β₁ x
h : ∀ (x : α), HEq (f₁ x) (f₂ x)
a : α
⊢ f₁ a = f₂ a
Tactic:
apply eq_of_heq <| h a
State after:
no goals