internlm/Lean-Github huggingface dataset:
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this :
  OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Tactic:
rw [this] at bound
Proof state after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      ((OneHom.toFun (↑↑inclusion) a -
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
            OneHom.toFun (↑↑inclusion) b) *
        sorryAx ℂ true) <
    1
this :
  OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      ((OneHom.toFun (↑↑inclusion) a -
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
            OneHom.toFun (↑↑inclusion) b) *
        sorryAx ℂ true) <
    1
this :
  OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Tactic:
clear this
Proof state after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      ((OneHom.toFun (↑↑inclusion) a -
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
            OneHom.toFun (↑↑inclusion) b) *
        sorryAx ℂ true) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      ((OneHom.toFun (↑↑inclusion) a -
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
            OneHom.toFun (↑↑inclusion) b) *
        sorryAx ℂ true) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Tactic:
rw [normSq_mul] at bound
Proof state after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
        (OneHom.toFun (↑↑inclusion) a -
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
            OneHom.toFun (↑↑inclusion) b) *
      ↑normSq (sorryAx ℂ true) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
this : ↑normSq (OneHom.toFun (↑↑inclusion) (mod a b)) < ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (mod a b) < natNorm b
Tactic:
simp only [natNorm_coe] at this
Proof state after:
a b c : ℤω
h : b ≠ 0
this : ↑(natNorm (mod a b)) < ↑(natNorm b)
⊢ natNorm (mod a b) < natNorm b
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
this : ↑(natNorm (mod a b)) < ↑(natNorm b)
⊢ natNorm (mod a b) < natNorm b
Tactic:
exact_mod_cast this
Proof state after:
no goals
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
Tactic:
ring_nf
Proof state after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹ -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) a * sorryAx ℂ true -
      OneHom.toFun (↑↑inclusion) b *
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
        sorryAx ℂ true
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹ -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) a * sorryAx ℂ true -
      OneHom.toFun (↑↑inclusion) b *
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
        sorryAx ℂ true
Tactic:
have : (b : ℂ) * (b : ℂ)⁻¹ = 1 := by
  apply mul_inv_cancel
  simpa [coe_eq_zero] using h
Proof state after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹ -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) a * sorryAx ℂ true -
      OneHom.toFun (↑↑inclusion) b *
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
        sorryAx ℂ true
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹ -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) a * sorryAx ℂ true -
      OneHom.toFun (↑↑inclusion) b *
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
        sorryAx ℂ true
Tactic:
congr
Proof state after:
case e_a.e_a
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ (OneHom.toFun (↑↑inclusion) b)⁻¹ = sorryAx ℂ true

case e_a
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) b *
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
      sorryAx ℂ true
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
Tactic:
apply mul_inv_cancel
Proof state after:
case h
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) b ≠ 0
Theorem: ℤω.normSq_mod_lt
Proof state before:
case h
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) b ≠ 0
Tactic:
simpa [coe_eq_zero] using h
Proof state after:
no goals
Theorem: ℤω.my_quotient_zero
Proof state before:
a b c : ℤω
⊢ div a 0 = 0
Tactic:
unfold div
Proof state after:
a b c : ℤω
⊢ nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
Theorem: ℤω.my_quotient_zero
Proof state before:
a b c : ℤω
⊢ nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
Tactic:
have : ((0 : ℤω) : ℂ) = 0 := my_map_zero
Proof state after:
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
Theorem: ℤω.my_quotient_zero
Proof state before:
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
Tactic:
rw [this, div_zero]
Proof state after:
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤω 0 = 0
Theorem: ℤω.my_quotient_zero
Proof state before:
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤω 0 = 0
Tactic:
unfold nearestℤω
Proof state after:
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ (let y := round (2 * rt3⁻¹ * 0.im);
    { x := round (0.re + 2⁻¹ * ↑y), y := y }) =
    0
Theorem: ℤω.my_quotient_zero
Proof state before:
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ (let y := round (2 * rt3⁻¹ * 0.im);
    { x := round (0.re + 2⁻¹ * ↑y), y := y }) =
    0
Tactic:
ext <;> dsimp <;> simp only [MulZeroClass.mul_zero, round_zero, algebraMap.coe_zero, add_zero]
Proof state after:
case x
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ round (0 + 2⁻¹ * ↑0) = 0.x
Theorem: ℤω.my_quotient_zero
Proof state before:
case x
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ round (0 + 2⁻¹ * ↑0) = 0.x
Tactic:
simp only [cast_zero, mul_zero, add_zero, round_zero]
Proof state after:
no goals
Theorem: project.IsHeap_empty
Proof state before:
α : Type u
⊢ IsHeap empty
Tactic:
constructor
Proof state after:
no goals
Theorem: project.IsMinHeap_empty
Proof state before:
α : Type u
le : α → α → Bool
⊢ IsMinHeap le empty
Tactic:
constructor
Proof state after:
no goals
Theorem: project.singleton_IsHeap
Proof state before:
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeap (singleton a)
Tactic:
constructor
Proof state after:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ 0 < { val := a, rank := 1, children := heap [] }.rank

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsBinTree { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []
Theorem: project.singleton_IsHeap
Proof state before:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ 0 < { val := a, rank := 1, children := heap [] }.rank

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsBinTree { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []
Tactic:
. dsimp
  decide
Proof state after:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsBinTree { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []
Theorem: project.singleton_IsHeap
Proof state before:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsBinTree { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []
Tactic:
. constructor
  dsimp
  constructor
Proof state after:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []
Theorem: project.singleton_IsHeap
Proof state before:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []
Tactic:
. constructor
Proof state after:
no goals
Theorem: project.singleton_IsMinHeap
Proof state before:
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsMinHeap le (singleton a)
Tactic:
constructor
Proof state after:
case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsSearchTree le { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsMinHeap le (heap [])
Theorem: project.singleton_IsMinHeap
Proof state before:
case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsSearchTree le { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsMinHeap le (heap [])
Tactic:
. constructor
  dsimp
  constructor
Proof state after:
case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsMinHeap le (heap [])
Theorem: project.singleton_IsMinHeap
Proof state before:
case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsMinHeap le (heap [])
Tactic:
. constructor
Proof state after:
no goals
Theorem: project.IsRankedTree_append
Proof 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
Proof 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])
Theorem: project.IsRankedTree_append
Proof 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
Proof state after:
no goals
Theorem: project.IsRankedTree_append
Proof 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
Proof state after:
no goals
Theorem: project.IsRankedTree_append
Proof 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
Proof 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]
Theorem: project.IsRankedTree_append
Proof 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
Proof state after:
case nil
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsRankedTree m (m + 1) [a]
Theorem: project.IsRankedTree_append
Proof 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
Proof 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
Theorem: project.IsRankedTree_append
Proof 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
Proof 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
Theorem: project.IsRankedTree_append
Proof 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
Proof state after:
case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsBinTree a
Theorem: project.IsRankedTree_append
Proof state before:
case nil.a
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsBinTree a
Tactic:
. assumption
Proof state after:
no goals
Theorem: project.IsRankedTree_append
Proof 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
Proof 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])
Theorem: project.IsRankedTree_append
Proof 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
Proof 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✝
Theorem: project.IsRankedTree_append
Proof 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
Proof 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✝
Theorem: project.IsRankedTree_append
Proof 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
Proof 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✝
Theorem: project.IsRankedTree_append
Proof 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
Proof state after:
no goals