Theorem: Schema.retypedFromSubschema_preserves_names (Table/SchemaFunctions.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
⊢ names (retypedFromSubschema ({ fst := (nm, τ), snd := pf } :: rs)) = names ((fst✝, snd✝) :: ss)
Tactic:
simp only [retypedFromSubschema]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
⊢ names (retypedFromSubschema (map (fun x => { fst := x.fst, snd := hasRetypedName x.snd }) rs)) =
    names ((fst✝, snd✝) :: ss)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
⊢ names (retypedFromSubschema (map (fun x => { fst := x.fst, snd := hasRetypedName x.snd }) rs)) =
    names ((fst✝, snd✝) :: ss)
Tactic:
have := retypedFromSubschema_preserves_names (Schema.retypeColumn _ pf τ)
  (Schema.map (fun ⟨h, pf⟩ => ⟨h, hasRetypedName pf⟩) rs)
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
this :
  names
      (retypedFromSubschema
        (map
          (fun x =>
            match x with
            | { fst := h, snd := pf_1 } => { fst := h, snd := hasRetypedName pf_1 })
          rs)) =
    names (retypeColumn ((fst✝, snd✝) :: ss) pf τ)
⊢ names (retypedFromSubschema (map (fun x => { fst := x.fst, snd := hasRetypedName x.snd }) rs)) =
    names ((fst✝, snd✝) :: ss)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
this :
  names
      (retypedFromSubschema
        (map
          (fun x =>
            match x with
            | { fst := h, snd := pf_1 } => { fst := h, snd := hasRetypedName pf_1 })
          rs)) =
    names (retypeColumn ((fst✝, snd✝) :: ss) pf τ)
⊢ names (retypedFromSubschema (map (fun x => { fst := x.fst, snd := hasRetypedName x.snd }) rs)) =
    names ((fst✝, snd✝) :: ss)
Tactic:
rw [this]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
this :
  names
      (retypedFromSubschema
        (map
          (fun x =>
            match x with
            | { fst := h, snd := pf_1 } => { fst := h, snd := hasRetypedName pf_1 })
          rs)) =
    names (retypeColumn ((fst✝, snd✝) :: ss) pf τ)
⊢ names (retypeColumn ((fst✝, snd✝) :: ss) pf τ) = names ((fst✝, snd✝) :: ss)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
this :
  names
      (retypedFromSubschema
        (map
          (fun x =>
            match x with
            | { fst := h, snd := pf_1 } => { fst := h, snd := hasRetypedName pf_1 })
          rs)) =
    names (retypeColumn ((fst✝, snd✝) :: ss) pf τ)
⊢ names (retypeColumn ((fst✝, snd✝) :: ss) pf τ) = names ((fst✝, snd✝) :: ss)
Tactic:
simp only [retypeColumn_preserves_names]
State after:
no goals