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

State before:
α α' : Type u_1
β : Type (max u_1 u_2)
γ : Type u_2
a : γ → α
b : β
h : α = α'
⊢ HEq (fun x => cast h (a x)) b = HEq a b
Tactic:
apply propext
State after:
case a
α α' : Type u_1
β : Type (max u_1 u_2)
γ : Type u_2
a : γ → α
b : β
h : α = α'
⊢ HEq (fun x => cast h (a x)) b ↔ HEq a b

State before:
case a
α α' : Type u_1
β : Type (max u_1 u_2)
γ : Type u_2
a : γ → α
b : β
h : α = α'
⊢ HEq (fun x => cast h (a x)) b ↔ HEq a b
Tactic:
constructor
<;> intro premise
<;> cases premise
State after:
case a.mp.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq a fun x => cast h (a x)

case a.mpr.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a

State before:
case a.mp.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq a fun x => cast h (a x)

case a.mpr.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Tactic:
. apply HEq.symm; apply heq_fun_congr;
State after:
case a.mpr.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a

State before:
case a.mpr.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Tactic:
. apply heq_fun_congr;
State after:
no goals

State before:
case a.mp.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq a fun x => cast h (a x)
Tactic:
apply HEq.symm
State after:
case a.mp.refl.h
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a

State before:
case a.mp.refl.h
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Tactic:
apply heq_fun_congr
State after:
no goals

State before:
case a.mpr.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Tactic:
apply heq_fun_congr
State after:
no goals