internlm/Lean-Github huggingface dataset:
Theorem: heq_cast_left
Proof state before:
case a
α α' β : Sort u_1
a : α
b : β
h : α = α'
⊢ HEq (cast h a) b ↔ HEq a b
Tactic:
constructor
<;> intro premise
Proof 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
Theorem: heq_cast_left
Proof 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;
Proof state after:
case a.mpr
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq a b
⊢ HEq (cast h a) b
Theorem: heq_cast_left
Proof 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;
Proof state after:
no goals
Theorem: heq_cast_left
Proof 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 _ _
Proof 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
Theorem: heq_cast_left
Proof 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
Proof 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
Theorem: heq_cast_left
Proof 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
Proof state after:
no goals
Theorem: heq_cast_left
Proof 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
Proof state after:
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq a b
⊢ HEq (cast h a) a
Theorem: heq_cast_left
Proof state before:
α α' β : Sort u_1
a : α
b : β
h : α = α'
premise : HEq a b
⊢ HEq (cast h a) a
Tactic:
apply cast_heq
Proof state after:
no goals
Theorem: heq_cast_right
Proof state before:
α β β' : Sort u_1
a : α
b : β
h : β = β'
⊢ HEq a (cast h b) = HEq a b
Tactic:
apply propext
Proof state after:
case a
α β β' : Sort u_1
a : α
b : β
h : β = β'
⊢ HEq a (cast h b) ↔ HEq a b
Theorem: heq_cast_right
Proof state before:
case a
α β β' : Sort u_1
a : α
b : β
h : β = β'
⊢ HEq a (cast h b) ↔ HEq a b
Tactic:
constructor
<;> intro premise
Proof 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)
Theorem: heq_cast_right
Proof 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;
Proof state after:
case a.mpr
α β β' : Sort u_1
a : α
b : β
h : β = β'
premise : HEq a b
⊢ HEq a (cast h b)
Theorem: heq_cast_right
Proof 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;
Proof state after:
no goals
Theorem: heq_cast_right
Proof 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 _ _
Proof 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
Theorem: heq_cast_right
Proof 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
Proof 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)
Theorem: heq_cast_right
Proof 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
Proof state after:
no goals
Theorem: heq_cast_right
Proof 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
Proof state after:
case a.mpr
α β β' : Sort u_1
a : α
b : β
h : β = β'
premise : HEq a b
⊢ HEq b (cast h b)
Theorem: heq_cast_right
Proof state before:
case a.mpr
α β β' : Sort u_1
a : α
b : β
h : β = β'
premise : HEq a b
⊢ HEq b (cast h b)
Tactic:
apply HEq.symm
Proof state after:
case a.mpr.h
α β β' : Sort u_1
a : α
b : β
h : β = β'
premise : HEq a b
⊢ HEq (cast h b) b
Theorem: heq_cast_right
Proof 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
Proof state after:
no goals
Theorem: heq_fun_congr
Proof state before:
α α' : Sort u_1
γ : Sort u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
γ : Sort u_2
a : γ → α
⊢ HEq (fun x => cast ⋯ (a x)) a
Theorem: heq_fun_congr
Proof state before:
case refl
α : Sort u_1
γ : Sort u_2
a : γ → α
⊢ HEq (fun x => cast ⋯ (a x)) a
Tactic:
simp only [cast_eq, heq_eq_eq]
Proof state after:
no goals
Theorem: heq_cast_left_fun
Proof 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
Proof 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
Theorem: heq_cast_left_fun
Proof 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
Proof 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
Theorem: heq_cast_left_fun
Proof 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;
Proof state after:
case a.mpr.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Theorem: heq_cast_left_fun
Proof 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;
Proof state after:
no goals
Theorem: heq_cast_left_fun
Proof 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
Proof state after:
case a.mp.refl.h
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Theorem: heq_cast_left_fun
Proof 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
Proof state after:
no goals
Theorem: heq_cast_left_fun
Proof 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
Proof state after:
no goals
Theorem: heq_cast_right_fun
Proof state before:
α α' : Type u_1
β : Type (max u_1 u_2)
γ : Type u_2
a : γ → α
b : β
h : α = α'
⊢ (HEq b fun x => cast h (a x)) = HEq b a
Tactic:
apply propext
Proof state after:
case a
α α' : Type u_1
β : Type (max u_1 u_2)
γ : Type u_2
a : γ → α
b : β
h : α = α'
⊢ (HEq b fun x => cast h (a x)) ↔ HEq b a
Theorem: heq_cast_right_fun
Proof state before:
case a
α α' : Type u_1
β : Type (max u_1 u_2)
γ : Type u_2
a : γ → α
b : β
h : α = α'
⊢ (HEq b fun x => cast h (a x)) ↔ HEq b a
Tactic:
constructor
<;> intro premise
<;> cases premise
Proof state after:
case a.mp.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a

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

case a.mpr.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq a fun x => cast h (a x)
Tactic:
. apply heq_fun_congr;
Proof state after:
case a.mpr.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq a fun x => cast h (a x)
Theorem: heq_cast_right_fun
Proof state before:
case a.mpr.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq a fun x => cast h (a x)
Tactic:
. apply HEq.symm; apply heq_fun_congr;
Proof state after:
no goals
Theorem: heq_cast_right_fun
Proof state before:
case a.mp.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Tactic:
apply heq_fun_congr
Proof state after:
no goals
Theorem: heq_cast_right_fun
Proof state before:
case a.mpr.refl
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq a fun x => cast h (a x)
Tactic:
apply HEq.symm
Proof state after:
case a.mpr.refl.h
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Theorem: heq_cast_right_fun
Proof state before:
case a.mpr.refl.h
α α' : Type u_1
γ : Type u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Tactic:
apply heq_fun_congr
Proof state after:
no goals
Theorem: hcongr_fun
Proof state before:
α : Sort u_1
P P' : α → Sort u_2
f : (a : α) → P a
f' : (a : α) → P' a
a : α
H₁ : HEq f f'
H₂ : P = P'
⊢ HEq (f a) (f' a)
Tactic:
cases H₂
Proof state after:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
f' : (a : α) → P a
H₁ : HEq f f'
⊢ HEq (f a) (f' a)
Theorem: hcongr_fun
Proof state before:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
f' : (a : α) → P a
H₁ : HEq f f'
⊢ HEq (f a) (f' a)
Tactic:
cases H₁
Proof state after:
case refl.refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
⊢ HEq (f a) (f a)
Theorem: hcongr_fun
Proof state before:
case refl.refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
⊢ HEq (f a) (f a)
Tactic:
apply HEq.rfl
Proof state after:
no goals
Theorem: hcongr
Proof state before:
α α' : Sort u_1
P : α → Sort u_2
P' : α' → Sort u_2
f : (a : α) → P a
f' : (a' : α') → P' a'
a : α
a' : α'
H₁ : HEq f f'
H₂ : HEq a a'
H₃ : α = α'
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
⊢ HEq (f a) (f' a')
Tactic:
cases H₂
Proof state after:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
⊢ HEq (f a) (f' a)
Theorem: hcongr
Proof state before:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
⊢ HEq (f a) (f' a)
Tactic:
apply hcongr_fun _ H₁
Proof state after:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
⊢ (fun a => P a) = fun a => P' a
Theorem: hcongr
Proof state before:
case refl
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
⊢ (fun a => P a) = fun a => P' a
Tactic:
funext a
Proof state after:
case refl.h
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a✝ : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
a : α
⊢ P a = P' a
Theorem: hcongr
Proof state before:
case refl.h
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a✝ : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃ a)
a : α
⊢ P a = P' a
Tactic:
simp [cast_eq] at H₃
Proof state after:
case refl.h
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a✝ : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃✝ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃✝ a)
a : α
H₃ : True
⊢ P a = P' a
Theorem: hcongr
Proof state before:
case refl.h
α : Sort u_1
P : α → Sort u_2
f : (a : α) → P a
a✝ : α
P' : α → Sort u_2
f' : (a' : α) → P' a'
H₁ : HEq f f'
H₃✝ : α = α
H₄ : ∀ (a : α), P a = P' (cast H₃✝ a)
a : α
H₃ : True
⊢ P a = P' a
Tactic:
apply H₄
Proof state after:
no goals
Theorem: heq_of_eq'
Proof state before:
α β : Sort u_1
a : α
b : β
h : β = α
⊢ a = cast h b → HEq a b
Tactic:
intro eq
Proof state after:
α β : Sort u_1
a : α
b : β
h : β = α
eq : a = cast h b
⊢ HEq a b
Theorem: heq_of_eq'
Proof state before:
α β : Sort u_1
a : α
b : β
h : β = α
eq : a = cast h b
⊢ HEq a b
Tactic:
cases eq
Proof state after:
case refl
α β : Sort u_1
b : β
h : β = α
⊢ HEq (cast h b) b
Theorem: heq_of_eq'
Proof state before:
case refl
α β : Sort u_1
b : β
h : β = α
⊢ HEq (cast h b) b
Tactic:
apply cast_heq
Proof state after:
no goals
Theorem: heq_of_eq_left'
Proof state before:
α β : Sort u_1
a : α
b : β
h : α = β
⊢ cast h a = b → HEq a b
Tactic:
intro eq
Proof state after:
α β : Sort u_1
a : α
b : β
h : α = β
eq : cast h a = b
⊢ HEq a b
Theorem: heq_of_eq_left'
Proof state before:
α β : Sort u_1
a : α
b : β
h : α = β
eq : cast h a = b
⊢ HEq a b
Tactic:
apply HEq.symm
Proof state after:
case h
α β : Sort u_1
a : α
b : β
h : α = β
eq : cast h a = b
⊢ HEq b a
Theorem: heq_of_eq_left'
Proof state before:
case h
α β : Sort u_1
a : α
b : β
h : α = β
eq : cast h a = b
⊢ HEq b a
Tactic:
apply heq_of_eq' h eq.symm
Proof state after:
no goals
Theorem: cast_arg
Proof 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
Proof 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')))
Theorem: cast_arg
Proof 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]
Proof 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'))
Theorem: cast_arg
Proof 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
Proof 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'
⊢ α' = α
Theorem: cast_arg
Proof 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
Proof 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'
⊢ α' = α
Theorem: cast_arg
Proof 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
Proof 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'
⊢ α' = α
Theorem: cast_arg
Proof 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₃
Proof state after:
no goals
Theorem: cast_arg
Proof 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
Proof state after:
no goals
Theorem: cast_arg
Proof 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
Proof 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'
Theorem: cast_arg
Proof 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
Proof state after:
no goals
Theorem: cast_arg
Proof 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'
Proof 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')
Theorem: cast_arg
Proof 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
Proof 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'
Theorem: cast_arg
Proof 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₃
Proof state after:
no goals
Theorem: cast_arg'
Proof state before:
α : Sort u₁
β β' : α → Sort u₂
f : (a : α) → β a
a : α
h₁ : ((a : α) → β a) = ((a : α) → β' a)
h₂ : ∀ (a : α), β a = β' a
⊢ cast h₁ f a = cast ⋯ (f a)
Tactic:
apply cast_arg
Proof state after:
case h₁
α : Sort u₁
β β' : α → Sort u₂
f : (a : α) → β a
a : α
h₁ : ((a : α) → β a) = ((a : α) → β' a)
h₂ : ∀ (a : α), β a = β' a
⊢ α = α
Theorem: cast_arg'
Proof state before:
case h₁
α : Sort u₁
β β' : α → Sort u₂
f : (a : α) → β a
a : α
h₁ : ((a : α) → β a) = ((a : α) → β' a)
h₂ : ∀ (a : α), β a = β' a
⊢ α = α
Tactic:
rfl
Proof state after:
no goals
Theorem: cast_fun_arg
Proof state before:
α β : Sort u_1
γ : Sort u_2
h : α = β
f : β → γ
⊢ HEq (fun a => f (cast h a)) f
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
γ : Sort u_2
f : α → γ
⊢ HEq (fun a => f (cast ⋯ a)) f
Theorem: cast_fun_arg
Proof state before:
case refl
α : Sort u_1
γ : Sort u_2
f : α → γ
⊢ HEq (fun a => f (cast ⋯ a)) f
Tactic:
simp only [cast_eq, heq_eq_eq]
Proof state after:
no goals
Theorem: HEq.funext
Proof 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
Proof state after:
case refl
α : Sort u
β₁ : α → Sort u_1
f₁ f₂ : (x : α) → β₁ x
⊢ (∀ (x : α), HEq (f₁ x) (f₂ x)) → HEq f₁ f₂
Theorem: HEq.funext
Proof 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
Proof state after:
case refl
α : Sort u
β₁ : α → Sort u_1
f₁ f₂ : (x : α) → β₁ x
h : ∀ (x : α), HEq (f₁ x) (f₂ x)
⊢ HEq f₁ f₂
Theorem: HEq.funext
Proof 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
Proof state after:
case refl.h
α : Sort u
β₁ : α → Sort u_1
f₁ f₂ : (x : α) → β₁ x
h : ∀ (x : α), HEq (f₁ x) (f₂ x)
⊢ f₁ = f₂
Theorem: HEq.funext
Proof 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
Proof 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
Theorem: HEq.funext
Proof 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
Proof state after:
no goals
Theorem: HEq.funext'
Proof state before:
α₁ α₂ : Sort u
β₁ : α₁ → Sort u_1
β₂ : α₂ → Sort u_1
f₁ : (x : α₁) → β₁ x
f₂ : (x : α₂) → β₂ x
type_eq_α : α₁ = α₂
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast type_eq_α a)
⊢ (∀ (x : α₁), HEq (f₁ x) (f₂ (cast type_eq_α x))) → HEq f₁ f₂
Tactic:
cases type_eq_α
Proof state after:
case refl
α₁ : Sort u
β₁ : α₁ → Sort u_1
f₁ : (x : α₁) → β₁ x
β₂ : α₁ → Sort u_1
f₂ : (x : α₁) → β₂ x
type_eq_β : ∀ (a : α₁), β₁ a = β₂ (cast ⋯ a)
⊢ (∀ (x : α₁), HEq (f₁ x) (f₂ (cast ⋯ x))) → HEq f₁ f₂