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

State before:
α : Type u
n m : ℕ
α✝ : Type u_1
xs : List (BinTree α✝)
a : BinTree α✝
rt : IsRankedTree n m xs
ha : IsBinTree a
hrank : a.rank = m
⊢ IsRankedTree n (m + 1) (xs ++ [a])
Tactic:
induction xs generalizing n
State after:
case nil
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
n : ℕ
rt : IsRankedTree n m []
⊢ IsRankedTree n (m + 1) ([] ++ [a])

case cons
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
tail_ih✝ : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
rt : IsRankedTree n m (head✝ :: tail✝)
⊢ IsRankedTree n (m + 1) (head✝ :: tail✝ ++ [a])

State before:
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
n : ℕ
rt : IsRankedTree n m []
⊢ IsRankedTree n (m + 1) ([] ++ [a])
Tactic:
case nil =>
  simp
  cases rt
  constructor
  . assumption
  . constructor
  . assumption
State after:
no goals

State before:
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
rt : IsRankedTree n m (head✝ :: tail✝)
⊢ IsRankedTree n (m + 1) (head✝ :: tail✝ ++ [a])
Tactic:
case cons _ _ ih =>
  cases rt
  constructor
  . assumption
  . apply ih
    assumption
  . assumption
State after:
no goals

State before:
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
n : ℕ
rt : IsRankedTree n m []
⊢ IsRankedTree n (m + 1) ([] ++ [a])
Tactic:
simp
State after:
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
n : ℕ
rt : IsRankedTree n m []
⊢ IsRankedTree n (m + 1) [a]

State before:
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
n : ℕ
rt : IsRankedTree n m []
⊢ IsRankedTree n (m + 1) [a]
Tactic:
cases rt
State after:
case nil
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsRankedTree m (m + 1) [a]

State before:
case nil
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsRankedTree m (m + 1) [a]
Tactic:
constructor
State after:
case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ a.rank = m

case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsRankedTree (m + 1) (m + 1) []

case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsBinTree a

State before:
case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ a.rank = m

case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsRankedTree (m + 1) (m + 1) []

case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsBinTree a
Tactic:
. assumption
State after:
case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsRankedTree (m + 1) (m + 1) []

case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsBinTree a

State before:
case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsRankedTree (m + 1) (m + 1) []

case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsBinTree a
Tactic:
. constructor
State after:
case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsBinTree a

State before:
case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsBinTree a
Tactic:
. assumption
State after:
no goals

State before:
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
rt : IsRankedTree n m (head✝ :: tail✝)
⊢ IsRankedTree n (m + 1) (head✝ :: tail✝ ++ [a])
Tactic:
cases rt
State after:
case cons
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsRankedTree n (m + 1) (head✝ :: tail✝ ++ [a])

State before:
case cons
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsRankedTree n (m + 1) (head✝ :: tail✝ ++ [a])
Tactic:
constructor
State after:
case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ head✝.rank = n

case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsRankedTree (n + 1) (m + 1) (List.append tail✝ [a])

case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsBinTree head✝

State before:
case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ head✝.rank = n

case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsRankedTree (n + 1) (m + 1) (List.append tail✝ [a])

case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsBinTree head✝
Tactic:
. assumption
State after:
case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsRankedTree (n + 1) (m + 1) (List.append tail✝ [a])

case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsBinTree head✝

State before:
case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsRankedTree (n + 1) (m + 1) (List.append tail✝ [a])

case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsBinTree head✝
Tactic:
. apply ih
  assumption
State after:
case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsBinTree head✝

State before:
case cons.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsBinTree head✝
Tactic:
. assumption
State after:
no goals