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

State before:
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ cast h₂ f a' = cast ⋯ (f (cast h₁ a'))
Tactic:
apply eq_of_heq
State after:
case h
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq (cast h₂ f a') (cast ⋯ (f (cast h₁ a')))

State before:
case h
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq (cast h₂ f a') (cast ⋯ (f (cast h₁ a')))
Tactic:
rw [heq_cast_right]
State after:
case h
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq (cast h₂ f a') (f (cast h₁ a'))

State before:
case h
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq (cast h₂ f a') (f (cast h₁ a'))
Tactic:
apply hcongr
State after:
case h.H₁
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq (cast h₂ f) f

case h.H₂
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq a' (cast h₁ a')

case h.H₄
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ ∀ (a : α'), β' a = β (cast ?h.H₃ a)

case h.H₃
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ α' = α

State before:
case h.H₁
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq (cast h₂ f) f

case h.H₂
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq a' (cast h₁ a')

case h.H₄
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ ∀ (a : α'), β' a = β (cast ?h.H₃ a)

case h.H₃
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ α' = α
Tactic:
. apply cast_heq
State after:
case h.H₂
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq a' (cast h₁ a')

case h.H₄
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ ∀ (a : α'), β' a = β (cast ?h.H₃ a)

case h.H₃
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ α' = α

State before:
case h.H₂
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq a' (cast h₁ a')

case h.H₄
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ ∀ (a : α'), β' a = β (cast ?h.H₃ a)

case h.H₃
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ α' = α
Tactic:
. apply HEq.symm; apply cast_heq
State after:
case h.H₄
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ ∀ (a : α'), β' a = β (cast ?h.H₃ a)

case h.H₃
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ α' = α

State before:
case h.H₄
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ ∀ (a : α'), β' a = β (cast ?h.H₃ a)

case h.H₃
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ α' = α
Tactic:
. intro a'; apply Eq.symm; apply h₃
State after:
no goals

State before:
case h.H₁
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq (cast h₂ f) f
Tactic:
apply cast_heq
State after:
no goals

State before:
case h.H₂
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq a' (cast h₁ a')
Tactic:
apply HEq.symm
State after:
case h.H₂.h
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq (cast h₁ a') a'

State before:
case h.H₂.h
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ HEq (cast h₁ a') a'
Tactic:
apply cast_heq
State after:
no goals

State before:
case h.H₄
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a' : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
⊢ ∀ (a : α'), β' a = β (cast ?h.H₃ a)
Tactic:
intro a'
State after:
case h.H₄
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a'✝ : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
a' : α'
⊢ β' a' = β (cast ?h.H₃ a')

State before:
case h.H₄
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a'✝ : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
a' : α'
⊢ β' a' = β (cast ?h.H₃ a')
Tactic:
apply Eq.symm
State after:
case h.H₄.h
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a'✝ : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
a' : α'
⊢ β (cast ?h.H₃ a') = β' a'

State before:
case h.H₄.h
α α' : Sort u₁
β : α → Sort u₂
β' : α' → Sort u₂
f : (a : α) → β a
a'✝ : α'
h₁ : α' = α
h₂ : ((a : α) → β a) = ((a' : α') → β' a')
h₃ : ∀ (a' : α'), β (cast h₁ a') = β' a'
a' : α'
⊢ β (cast ?h.H₃ a') = β' a'
Tactic:
apply h₃
State after:
no goals