How to simplify this proof on inductive type structure?

Stream: general

[Török Edwin]

Hi, I am new to Lean.

I wrote this proof to familiarise myself with it.

It feels like it should be possible to simplify the proof. Am I missing some annotations, or existing proofs from Lean/Mathlib? The property is very "structural", so I'm hoping some of the autogenerated theorems about the inductive type could help here.

import Mathlib

set_option linter.missingDocs false

variable (α) [BEq α]
in

@[aesop safe constructors]
inductive Expr
| C : α -> Expr
| Plus: Expr -> Expr -> Expr
deriving BEq, DecidableEq, Repr, Inhabited, LawfulTraversable

variable {α}

namespace Expr

@[simp]
abbrev contains (s a : Expr α) :=
  s = a ∨ match s with
  | Plus x y => contains x a ∨ contains y a
  | _ => false

instance instMembership : Membership (Expr α) (Expr α) where
  mem := contains

@[simp]
lemma x_in_app_x_y {x y : Expr α} : contains (Plus x y) x := by
  induction x <;> tauto

@[simp]
lemma x_in_app_y_x_z {x y z : Expr α} : contains (Plus (Plus y x) z) x := by
  induction x <;> tauto

@[simp]
lemma x_contains_x {x : Expr α} : contains x x := by
  unfold contains
  simp_all only [Bool.false_eq_true, true_or]

lemma contains_sizeof :
  ∀ (s a : Expr α), contains s a ->
  sizeOf s >= sizeOf a := by
  intro s a h
  simp_all only [ge_iff_le]
  induction s with
  | C _ => simp_all
  | Plus x y h1 h2 =>
    simp_all only [contains, Plus.sizeOf_spec]
    cases h with
    | inl h_1 =>
      subst h_1
      simp_all
    | inr h_2 =>
      cases h_2 with
      | inl h_3 =>
        simp_all only [forall_const]
        bound
      | inr h_3 =>
        simp_all only [forall_const]
        bound

lemma sizeof_contains :
  ∀ (s a : Expr α), sizeOf s < sizeOf a -> ¬ contains s a := by
    intro s a a_1
    apply Aesop.BuiltinRules.not_intro
    intro a_2
    apply contains_sizeof at a_2
    bound

theorem x_ne_x_contains {x y z : Expr α} :
  (contains y x ∨ contains z x) ->
  ¬ x = Plus y z := by
  induction x with
  | C _ => simp_all
  | Plus t u h1 h2 =>
    intros h3
    simp_all only [Plus.injEq, not_and]
    intro h4
    subst h4
    simp_all only [x_contains_x, true_or, forall_const]
    apply Aesop.BuiltinRules.not_intro
    intro a
    subst a
    simp_all only [x_contains_x, or_true, forall_const]
    cases h3 with
    | inl h =>
      apply sizeof_contains at h
      · assumption
      · simp_all only [Plus.sizeOf_spec]
        bound
    | inr h_1 =>
      apply sizeof_contains at h_1
      · assumption
      · simp_all only [Plus.sizeOf_spec]
        bound


end Expr

[Kenny Lau]

congrats on writing your first lean code!
some issues:

1. your instMembership is the wrong way
2. you might want to define contains inductively
3. you might also want to define your own size function instead of relying on the built in sizeOf
4. and also maybe you won't even need to reason about size in the first place
5. you can prove your last theorem using size