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

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

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

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

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

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

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

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

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

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

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

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

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