Theorem: project.IsMinTree_append (Project/Main.lean)

State before:
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
xs : List (BinTree α✝)
a : BinTree α✝
h : IsMinTree le m xs
ha : IsSearchTree le a
hba : le m a.val = true
⊢ IsMinTree le m (xs ++ [a])
Tactic:
induction xs with
| nil =>
  simp
  constructor <;> assumption
| cons _ _ ih => 
  cases h
  constructor
  . assumption
  . simp
    apply ih
    assumption
  . assumption
State after:
no goals

State before:
case nil
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
h : IsMinTree le m []
⊢ IsMinTree le m ([] ++ [a])
Tactic:
simp
State after:
case nil
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
h : IsMinTree le m []
⊢ IsMinTree le m [a]

State before:
case nil
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
h : IsMinTree le m []
⊢ IsMinTree le m [a]
Tactic:
constructor <;> assumption
State after:
no goals

State before:
case cons
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
h : IsMinTree le m (head✝ :: tail✝)
⊢ IsMinTree le m (head✝ :: tail✝ ++ [a])
Tactic:
cases h
State after:
case cons.cons
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (head✝ :: tail✝ ++ [a])

State before:
case cons.cons
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (head✝ :: tail✝ ++ [a])
Tactic:
constructor
State after:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ le m head✝.val = true

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (List.append tail✝ [a])

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝

State before:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ le m head✝.val = true

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (List.append tail✝ [a])

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝
Tactic:
. assumption
State after:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (List.append tail✝ [a])

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝

State before:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (List.append tail✝ [a])

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝
Tactic:
. simp
  apply ih
  assumption
State after:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝

State before:
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝
Tactic:
. assumption
State after:
no goals