Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env (FOL/MM0/MM0.lean)

State before:
E : Env
d : Definition
h1 : E.WellFormed
h2 : d ∈ E
⊢ IsMetaVarOrAllDefInEnv E d.F
Tactic:
induction E
State after:
case nil
d : Definition
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ IsMetaVarOrAllDefInEnv [] d.F

case cons
d head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Env.WellFormed tail✝ → d ∈ tail✝ → IsMetaVarOrAllDefInEnv tail✝ d.F
h1 : Env.WellFormed (head✝ :: tail✝)
h2 : d ∈ head✝ :: tail✝
⊢ IsMetaVarOrAllDefInEnv (head✝ :: tail✝) d.F

State before:
d : Definition
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ IsMetaVarOrAllDefInEnv [] d.F
Tactic:
case nil =>
  simp at h2
State after:
no goals

State before:
d : Definition
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ IsMetaVarOrAllDefInEnv [] d.F
Tactic:
simp at h2
State after:
no goals

State before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Tactic:
unfold Env.WellFormed at h1
State after:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d ∈ hd :: tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F

State before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d ∈ hd :: tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Tactic:
simp at h2
State after:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
h2 : d = hd ∨ d ∈ tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F

State before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
h2 : d = hd ∨ d ∈ tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Tactic:
cases h1
State after:
case intro
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
left✝ : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
right✝ : IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F

State before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right : IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Tactic:
cases h1_right
State after:
case intro
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
left✝ : IsMetaVarOrAllDefInEnv tl hd.F
right✝ : Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F

State before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Tactic:
apply concat_env_preserves_is_meta_var_or_all_def_in_env tl (hd :: tl)
State after:
case h1
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ ∃ E1, hd :: tl = E1 ++ tl

case h2
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv tl d.F

State before:
case h1
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ ∃ E1, hd :: tl = E1 ++ tl
Tactic:
apply Exists.intro [hd]
State after:
case h1
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ hd :: tl = [hd] ++ tl

State before:
case h1
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ hd :: tl = [hd] ++ tl
Tactic:
simp
State after:
no goals

State before:
case h2
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
cases h2
State after:
case h2.inl
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
h✝ : d = hd
⊢ IsMetaVarOrAllDefInEnv tl d.F

case h2.inr
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
h✝ : d ∈ tl
⊢ IsMetaVarOrAllDefInEnv tl d.F

State before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : d = hd
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
case _ c1 =>
  subst c1
  exact h1_right_left
State after:
no goals

State before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : d ∈ tl
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
case _ c1 =>
  exact ih h1_right_right c1
State after:
no goals

State before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : d = hd
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
subst c1
State after:
d : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_right_right : Env.WellFormed tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
⊢ IsMetaVarOrAllDefInEnv tl d.F

State before:
d : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_right_right : Env.WellFormed tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
exact h1_right_left
State after:
no goals

State before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : d ∈ tl
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
exact ih h1_right_right c1
State after:
no goals