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

State before:
α α' β : Sort u_1
a : α
b : β
h : α = α'
⊢ HEq (cast h a) b = HEq a b
Tactic:
apply propext
State after:
case a
α α' β : Sort u_1
a : α
b : β
h : α = α'
⊢ HEq (cast h a) b ↔ HEq a b

State before:
case a
α α' β : Sort u_1
a : α
b : β
h : α = α'
⊢ HEq (cast h a) b ↔ HEq a b
Tactic:
constructor
<;> intro premise
State after:
case a.mp
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq (cast h a) b
⊢ HEq a b

case a.mpr
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq a b
⊢ HEq (cast h a) b

State before:
case a.mp
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq (cast h a) b
⊢ HEq a b

case a.mpr
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq a b
⊢ HEq (cast h a) b
Tactic:
. have : HEq a (cast h a) := HEq.symm $ cast_heq _ _
  apply HEq.trans this;
  assumption;
State after:
case a.mpr
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq a b
⊢ HEq (cast h a) b

State before:
case a.mpr
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq a b
⊢ HEq (cast h a) b
Tactic:
. apply HEq.trans _ premise;
  apply cast_heq;
State after:
no goals

State before:
case a.mp
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq (cast h a) b
⊢ HEq a b
Tactic:
have : HEq a (cast h a) := HEq.symm $ cast_heq _ _
State after:
case a.mp
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq (cast h a) b
this : HEq a (cast h a)
⊢ HEq a b

State before:
case a.mp
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq (cast h a) b
this : HEq a (cast h a)
⊢ HEq a b
Tactic:
apply HEq.trans this
State after:
case a.mp
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq (cast h a) b
this : HEq a (cast h a)
⊢ HEq (cast h a) b

State before:
case a.mp
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq (cast h a) b
this : HEq a (cast h a)
⊢ HEq (cast h a) b
Tactic:
assumption
State after:
no goals

State before:
case a.mpr
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq a b
⊢ HEq (cast h a) b
Tactic:
apply HEq.trans _ premise
State after:
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq a b
⊢ HEq (cast h a) a

State before:
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq a b
⊢ HEq (cast h a) a
Tactic:
apply cast_heq
State after:
no goals