Theorem: SciLean.structExt (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
x x' : X
⊢ (∀ (i : I), structProj x i = structProj x' i) → x = x'
Tactic:
intro h
State after:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ x = x'

State before:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ x = x'
Tactic:
rw[← structMake_structProj (I:=I) x]
State after:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ (structMake fun i => structProj x i) = x'

State before:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ (structMake fun i => structProj x i) = x'
Tactic:
rw[← structMake_structProj (I:=I) x']
State after:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ (structMake fun i => structProj x i) = structMake fun i => structProj x' i

State before:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ (structMake fun i => structProj x i) = structMake fun i => structProj x' i
Tactic:
simp[h]
State after:
no goals