Consistent checks ensure refinement

theorem consistent_checks_ensure_refinement {schema : Schema} {req : Request} {es : Entities} {preq : PartialRequest} {pes : PartialEntities} :  isValidAndConsistent schema req es preq pes = .ok () → RequestAndEntitiesRefine req es preq pes:= by  intro h  simp only [isValidAndConsistent] at h  split at h <;> try cases h  rcases do_eq_ok₂ h with ⟨h₁, h₂⟩  simp only [RequestAndEntitiesRefine]  constructor  case _ =>    simp only [RequestRefines]    simp only [      isValidAndConsistent.requestIsConsistent,      Bool.or_eq_true,      Bool.not_eq_eq_eq_not,      Bool.not_true,      Bool.and_eq_true,      decide_eq_true_eq    ] at h₁    split at h₁ <;> simp at h₁    rcases h₁ with ⟨h₁₁, h₁₂, h₁₃, h₁₄⟩    -- Extract type equalities from requestMatchesEnvironment and schema.environment?    rename_i env heq h_guard    simp only [not_or, Bool.not_eq_false] at h_guard    have h_rm := h_guard.2    simp only [requestMatchesEnvironment, instanceOfRequestType, instanceOfEntityType,      Bool.and_eq_true, beq_iff_eq] at h_rm    refine ⟨      partial_is_valid_rfl _ _ _ decide_eq_implies_eq h₁₁,      h₁₂,      partial_is_valid_rfl _ _ _ decide_eq_implies_eq h₁₃,      partial_is_valid_rfl _ _ _ decide_eq_implies_eq h₁₄,      ?_, ?_⟩    all_goals {      unfold Schema.environment? at heq      cases h_find : schema.acts.find? preq.action      · simp [h_find] at heq      · simp only [h_find, Option.bind_some_fun] at heq        split at heq <;> simp at heq        rw [← heq] at h_rm        simp_all    }   case _ =>    simp [      isValidAndConsistent.envIsWellFormed,      bind, Except.bind,    ] at h₂    split at h₂ <;> simp at h₂    rename_i h₃    replace h₂ := h₃    simp [isValidAndConsistent.entitiesIsConsistent] at h₂    split at h₂ <;> simp at h₂    simp [isValidAndConsistent.entitiesMatch] at h₂    simp [EntitiesRefine]    intro uid data₂ hᵢ    replace hᵢ := Data.Map.find?_mem_toList hᵢ    simp [Data.Map.toList] at hᵢ    specialize h₂ uid data₂ hᵢ    split at h₂ <;> simp at h₂    rcases h₂ with ⟨⟨h₂₁, h₂₂⟩, h₂₃⟩    rename_i data₁ heq    exists data₁    constructor    exact heq    constructor    exact partial_is_valid_rfl (fun x => decide (x = data₁.attrs)) (fun x => x = data₁.attrs) data₂.attrs decide_eq_implies_eq h₂₁    constructor    exact partial_is_valid_rfl (fun x => decide (x = data₁.ancestors)) (fun x => x = data₁.ancestors) data₂.ancestors decide_eq_implies_eq h₂₂    exact partial_is_valid_rfl (fun x => decide (x = data₁.tags)) (fun x => x = data₁.tags) data₂.tags decide_eq_implies_eq h₂₃