Theorem: SciLean.StructType.structProj_structMake (SciLean/Data/StructType/Basic.lean)

State before:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
f : (i : I) → XI i
i : I
⊢ structProj (structMake f) i = f i
Tactic:
apply congr_fun
State after:
case h
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
f : (i : I) → XI i
i : I
⊢ structProj (structMake f) = fun i => f i

State before:
case h
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
f : (i : I) → XI i
i : I
⊢ structProj (structMake f) = fun i => f i
Tactic:
apply left_inv
State after:
no goals