internlm/Lean-Github huggingface dataset:
Theorem: P_goes_down
Proof state before:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
Proof state after:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases em (isAtomic α) <;> cases em (isStar α)
Proof state after:
case inl.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inl.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
all_goals (simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
(simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
Proof state after:
case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
try linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ = β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
subst γ_in
Proof state after:
γ α : Program
αs : List Program
ℓ : TP (α;'γ)
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram γ
Theorem: P_goes_down
Proof state before:
γ α : Program
αs : List Program
ℓ : TP (α;'γ)
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram γ
Tactic:
linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases em ([] ∈ P α ℓ)
Proof state after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
h✝ : [] ∉ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
Proof state after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IH := P_goes_down γ_in δ_in
Proof state after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases em (isAtomic β) <;> cases em (isStar β)
Proof state after:
case inl.inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inl.inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
all_goals (simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
(simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
Proof state after:
case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
try linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
h✝ : [] ∉ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : (δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases δ_in
Proof state after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
h✝ : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
h✝ : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inl δ_in =>
  have IH := P_goes_down γ_in δ_in
  cases em (isAtomic α) <;> cases em (isStar α)
  all_goals (simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inr δ_in =>
  have IH := P_goes_down γ_in δ_in
  cases em (isAtomic β) <;> cases em (isStar β)
  all_goals (simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IH := P_goes_down γ_in δ_in
Proof state after:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases em (isAtomic α) <;> cases em (isStar α)
Proof state after:
case inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
all_goals (simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
(simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
Proof state after:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
try linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IH := P_goes_down γ_in δ_in
Proof state after:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β