def etaStructAtom (e: Expr): MetaM (Option Expr) := do
  let (declName, declArgs) := e.getAppFnArgs
  match (← getEnv).find? declName with
  | ConstantInfo.ctorInfo ctorInfo =>
    match (← getEnv).find? ctorInfo.induct with
    | ConstantInfo.inductInfo indInfo =>
      if indInfo.ctors.length == 1 
        && ctorInfo.numFields > 0
        && declArgs.size == ctorInfo.numParams + ctorInfo.numFields then
        match declArgs.get? ctorInfo.numParams with
        | some (Expr.proj _ _ arg) =>
          if ←  isDefEq e arg then
            pure (some arg)
          else
            pure none
        | some a =>
          match (a).getAppArgs'.back? with
          | some arg =>
              if ←  isDefEq e arg then
                pure (some arg)
              else
                pure none
          | none => pure none
        | _ => pure none
      else
        pure none
    | _ => pure none
  | _ =>
    pure none


 def etaStruct (e: Expr): MetaM Expr := do
  Meta.transform e (post:= fun n => do
    match (← etaStructAtom n) with
    | some t => pure (TransformStep.done t)
    | none => pure TransformStep.continue 
  )

/--
`eta_struct at loc` applies eta reduction for structures to all sub-expressions at the given location.
This also exists as a `conv`-mode tactic.

For example, if `x` is a Prod, `Prod.mk x.1 x.2` becomes `x` after eta reduction for structures.
-/
elab (name := etaStructStx) "eta_struct" loc?:(ppSpace Parser.Tactic.location)? : tactic =>
  runDefeqTactic etaStruct loc? "eta_struct"

@[inherit_doc etaStructStx]
elab "eta_struct" : conv => runDefeqConvTactic etaStruct