Unfolding structure definition

Stream: Is there code for X?

[Jasper Robb]

I would like to be able to unfold the definition of structures in my proofs, but I can't find any nice built-in way of accomplishing this. The best I've found is to write a lemma showing equivalence between a structure type and an explicit unpacking of the structure. #mwe:

def TypeEven : Type :=
  {n : ℕ // ∃ k, n = 2*k}

structure TypeEven' : Type :=
  val' : ℕ
  isEven : ∃ k, val' = 2 * k

def TypeEven_equiv : TypeEven ≃ TypeEven' where
  toFun := fun ⟨n, hn⟩ ↦ ⟨n, hn⟩
  invFun := fun ⟨n, hn⟩ ↦ ⟨n, hn⟩
  left_inv := by
    simp only [Function.LeftInverse]
    exact fun x ↦ rfl
  right_inv := by simp [Function.RightInverse, Function.LeftInverse]

theorem min_TypeEven : (⨅ x : TypeEven, x.val) = (⨅ y : TypeEven', y.val') := by
  simp only [← TypeEven_equiv.symm.iInf_comp]
  rfl

Surely there is a better way to accomplish this kind of proof.

[Kyle Miller]

Which direction do you want to do? Are you starting from TypeEven', or from TypeEven?

[Jasper Robb]

I'm just trying to unwrap the structure TypeEven'. Essentially I want to manipulate a structure in the same way you can manipulate product and dependent product types in a proof.

[Kyle Miller]

Could you give an #mwe that shows how you use this unpacking? I see how you use TypeEven_equiv in min_TypeEven, but I imagine you want to fully eliminate TypeEven.