Theorem: SciLean.isomorph.funext (SciLean/Core/Objects/IsomorphicType.lean)

State before:
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
⊢ isomorph tag f = isomorph tag g → f = g
Tactic:
intro h
State after:
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
⊢ f = g

State before:
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
⊢ f = g
Tactic:
funext _
State after:
case h
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
x✝ : α
⊢ f x✝ = g x✝

State before:
case h
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
x✝ : α
⊢ f x✝ = g x✝
Tactic:
apply ext tag
State after:
case h.a
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
x✝ : α
⊢ (IsomorphicType.equiv tag) (f x✝) = (IsomorphicType.equiv tag) (g x✝)

State before:
case h.a
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
x✝ : α
⊢ (IsomorphicType.equiv tag) (f x✝) = (IsomorphicType.equiv tag) (g x✝)
Tactic:
simp[app tag,h]
State after:
no goals