internlm/Lean-Github huggingface dataset:
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this✝ : n + 1 - k - 1 = n - k
this : succ (n - k - 1) = n - k
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k
Tactic:
rw [‹n+1-k-1=n-k›, ‹succ (n-k-1)=n-k›]
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this✝ : n + 1 - k - 1 = n - k
this : succ (n - k - 1) = n - k
⊢ (fun x => f (n - k) x >>= foldM.loop f (n + 1) k) = fun x => f (n - k) x >>= foldM.loop (f ∘ succ) n k
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this✝ : n + 1 - k - 1 = n - k
this : succ (n - k - 1) = n - k
⊢ (fun x => f (n - k) x >>= foldM.loop f (n + 1) k) = fun x => f (n - k) x >>= foldM.loop (f ∘ succ) n k
Tactic:
rw [h_ind (Nat.le_of_succ_le hk)]
Proof state after:
no goals
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
⊢ n + 1 - k - 1 = succ n - succ k
Tactic:
simp only [Nat.sub_sub]
Proof state after:
no goals
Theorem: Nat.foldM_succ_eq_foldM_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ foldM f init (n + 1) = foldM f init n >>= f n
Tactic:
induction n generalizing f init
Proof state after:
case zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldM f init (zero + 1) = foldM f init zero >>= f zero

case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n✝ : Nat
n_ih✝ : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n✝ + 1) = foldM f init n✝ >>= f n✝
f : Nat → α → m α
init : α
⊢ foldM f init (succ n✝ + 1) = foldM f init (succ n✝) >>= f (succ n✝)
Theorem: Nat.foldM_succ_eq_foldM_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldM f init (zero + 1) = foldM f init zero >>= f zero
Tactic:
case zero =>
  conv =>
    dsimp [foldM, foldM.loop]
    change f 0 init >>= pure = pure init >>= f 0
  simp only [pure_bind, bind_pure]
Proof state after:
no goals
Theorem: Nat.foldM_succ_eq_foldM_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ foldM f init (succ n + 1) = foldM f init (succ n) >>= f (succ n)
Tactic:
case succ n h_ind =>
  simp only [Nat.succ_eq_add_one]
  conv => lhs; rw [foldM_succ]; rhs; ext; rw [h_ind]
  conv => rhs; rw [foldM_succ]
  dsimp; rw [bind_assoc]
Proof state after:
no goals
Theorem: Nat.foldM_succ_eq_foldM_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldM f init (zero + 1) = foldM f init zero >>= f zero
Tactic:
conv =>
  dsimp [foldM, foldM.loop]
  change f 0 init >>= pure = pure init >>= f 0
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ f 0 init >>= pure = pure init >>= f 0
Theorem: Nat.foldM_succ_eq_foldM_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ f 0 init >>= pure = pure init >>= f 0
Tactic:
simp only [pure_bind, bind_pure]
Proof state after:
no goals
Theorem: Nat.foldM_succ_eq_foldM_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ foldM f init (succ n + 1) = foldM f init (succ n) >>= f (succ n)
Tactic:
simp only [Nat.succ_eq_add_one]
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ foldM f init (n + 1 + 1) = foldM f init (n + 1) >>= f (n + 1)
Theorem: Nat.foldM_succ_eq_foldM_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ foldM f init (n + 1 + 1) = foldM f init (n + 1) >>= f (n + 1)
Tactic:
conv => lhs; rw [foldM_succ]; rhs; ext; rw [h_ind]
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= (f ∘ succ) n) = foldM f init (n + 1) >>= f (n + 1)
Theorem: Nat.foldM_succ_eq_foldM_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= (f ∘ succ) n) = foldM f init (n + 1) >>= f (n + 1)
Tactic:
conv => rhs; rw [foldM_succ]
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= (f ∘ succ) n) =
    (do
        let x ← f 0 init
        foldM (f ∘ succ) x n) >>=
      f (n + 1)
Theorem: Nat.foldM_succ_eq_foldM_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= (f ∘ succ) n) =
    (do
        let x ← f 0 init
        foldM (f ∘ succ) x n) >>=
      f (n + 1)
Tactic:
dsimp
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= f (succ n)) =
    (do
        let x ← f 0 init
        foldM (f ∘ succ) x n) >>=
      f (n + 1)
Theorem: Nat.foldM_succ_eq_foldM_bind
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= f (succ n)) =
    (do
        let x ← f 0 init
        foldM (f ∘ succ) x n) >>=
      f (n + 1)
Tactic:
rw [bind_assoc]
Proof state after:
no goals
Theorem: Nat.fold_eq_foldM
Proof state before:
α : Type u
f : Nat → α → α
init : α
n : Nat
⊢ fold f n init = foldM f init n
Tactic:
induction n
Proof state after:
case zero
α : Type u
f : Nat → α → α
init : α
⊢ fold f zero init = foldM f init zero

case succ
α : Type u
f : Nat → α → α
init : α
n✝ : Nat
n_ih✝ : fold f n✝ init = foldM f init n✝
⊢ fold f (succ n✝) init = foldM f init (succ n✝)
Theorem: Nat.fold_eq_foldM
Proof state before:
α : Type u
f : Nat → α → α
init : α
⊢ fold f zero init = foldM f init zero
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.fold_eq_foldM
Proof state before:
α : Type u
f : Nat → α → α
init : α
n : Nat
h_ind : fold f n init = foldM f init n
⊢ fold f (succ n) init = foldM f init (succ n)
Tactic:
case succ n h_ind =>
  rw [foldM_succ_eq_foldM_bind, ←h_ind]; rfl
Proof state after:
no goals
Theorem: Nat.fold_eq_foldM
Proof state before:
α : Type u
f : Nat → α → α
init : α
⊢ fold f zero init = foldM f init zero
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.fold_eq_foldM
Proof state before:
α : Type u
f : Nat → α → α
init : α
n : Nat
h_ind : fold f n init = foldM f init n
⊢ fold f (succ n) init = foldM f init (succ n)
Tactic:
rw [foldM_succ_eq_foldM_bind, ←h_ind]
Proof state after:
α : Type u
f : Nat → α → α
init : α
n : Nat
h_ind : fold f n init = foldM f init n
⊢ fold f (succ n) init = fold f n init >>= f n
Theorem: Nat.fold_eq_foldM
Proof state before:
α : Type u
f : Nat → α → α
init : α
n : Nat
h_ind : fold f n init = foldM f init n
⊢ fold f (succ n) init = fold f n init >>= f n
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.fold_hom
Proof state before:
α : Type u
β : Type v
f : α → β
g₁ : Nat → α → α
g₂ : Nat → β → β
n✝ : Nat
init : α
hf✝ : ∀ (i : Nat) (a : α), i < n✝ → g₂ i (f a) = f (g₁ i a)
n : Nat
IH : (∀ (i : Nat) (a : α), i < n → g₂ i (f a) = f (g₁ i a)) → fold g₂ n (f init) = f (fold g₁ n init)
hf : ∀ (i : Nat) (a : α), i < succ n → g₂ i (f a) = f (g₁ i a)
⊢ fold g₂ (succ n) (f init) = f (fold g₁ (succ n) init)
Tactic:
dsimp [Nat.fold]
Proof state after:
α : Type u
β : Type v
f : α → β
g₁ : Nat → α → α
g₂ : Nat → β → β
n✝ : Nat
init : α
hf✝ : ∀ (i : Nat) (a : α), i < n✝ → g₂ i (f a) = f (g₁ i a)
n : Nat
IH : (∀ (i : Nat) (a : α), i < n → g₂ i (f a) = f (g₁ i a)) → fold g₂ n (f init) = f (fold g₁ n init)
hf : ∀ (i : Nat) (a : α), i < succ n → g₂ i (f a) = f (g₁ i a)
⊢ g₂ n (fold g₂ n (f init)) = f (g₁ n (fold g₁ n init))
Theorem: Nat.fold_hom
Proof state before:
α : Type u
β : Type v
f : α → β
g₁ : Nat → α → α
g₂ : Nat → β → β
n✝ : Nat
init : α
hf✝ : ∀ (i : Nat) (a : α), i < n✝ → g₂ i (f a) = f (g₁ i a)
n : Nat
IH : (∀ (i : Nat) (a : α), i < n → g₂ i (f a) = f (g₁ i a)) → fold g₂ n (f init) = f (fold g₁ n init)
hf : ∀ (i : Nat) (a : α), i < succ n → g₂ i (f a) = f (g₁ i a)
⊢ g₂ n (fold g₂ n (f init)) = f (g₁ n (fold g₁ n init))
Tactic:
have IH := IH λ i a h => hf i a (trans h n.lt_succ_self)
Proof state after:
α : Type u
β : Type v
f : α → β
g₁ : Nat → α → α
g₂ : Nat → β → β
n✝ : Nat
init : α
hf✝ : ∀ (i : Nat) (a : α), i < n✝ → g₂ i (f a) = f (g₁ i a)
n : Nat
IH✝ : (∀ (i : Nat) (a : α), i < n → g₂ i (f a) = f (g₁ i a)) → fold g₂ n (f init) = f (fold g₁ n init)
hf : ∀ (i : Nat) (a : α), i < succ n → g₂ i (f a) = f (g₁ i a)
IH : fold g₂ n (f init) = f (fold g₁ n init)
⊢ g₂ n (fold g₂ n (f init)) = f (g₁ n (fold g₁ n init))
Theorem: Nat.fold_hom
Proof state before:
α : Type u
β : Type v
f : α → β
g₁ : Nat → α → α
g₂ : Nat → β → β
n✝ : Nat
init : α
hf✝ : ∀ (i : Nat) (a : α), i < n✝ → g₂ i (f a) = f (g₁ i a)
n : Nat
IH✝ : (∀ (i : Nat) (a : α), i < n → g₂ i (f a) = f (g₁ i a)) → fold g₂ n (f init) = f (fold g₁ n init)
hf : ∀ (i : Nat) (a : α), i < succ n → g₂ i (f a) = f (g₁ i a)
IH : fold g₂ n (f init) = f (fold g₁ n init)
⊢ g₂ n (fold g₂ n (f init)) = f (g₁ n (fold g₁ n init))
Tactic:
rw [IH, hf n _ n.lt_succ_self]
Proof state after:
no goals
Theorem: Nat.foldRev_succ
Proof state before:
α : Type u_1
f : Nat → α → α
n : Nat
init : α
⊢ foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
Tactic:
induction n generalizing f init with
| zero => rfl
| succ n IH =>
  unfold foldRev; simp only [Nat.add, Nat.succ_eq_add_one]
  rewrite [IH]; rfl
Proof state after:
no goals
Theorem: Nat.foldRev_succ
Proof state before:
case zero
α : Type u_1
f : Nat → α → α
init : α
⊢ foldRev f (zero + 1) init = f 0 (foldRev (f ∘ succ) zero init)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.foldRev_succ
Proof state before:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (succ n + 1) init = f 0 (foldRev (f ∘ succ) (succ n) init)
Tactic:
unfold foldRev
Proof state after:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (Nat.add (succ n) 0) (f (Nat.add (succ n) 0) init) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))
Theorem: Nat.foldRev_succ
Proof state before:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (Nat.add (succ n) 0) (f (Nat.add (succ n) 0) init) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))
Tactic:
simp only [Nat.add, Nat.succ_eq_add_one]
Proof state after:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (n + 1) (f (n + 1) init) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))
Theorem: Nat.foldRev_succ
Proof state before:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (n + 1) (f (n + 1) init) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))
Tactic:
rewrite [IH]
Proof state after:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ f 0 (foldRev (f ∘ succ) n (f (n + 1) init)) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))
Theorem: Nat.foldRev_succ
Proof state before:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ f 0 (foldRev (f ∘ succ) n (f (n + 1) init)) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.foldRev_induction
Proof state before:
α : Type u_1
motive : Nat → α → Prop
f : Nat → α → α
n : Nat
init : α
hinit : motive n init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (foldRev f n init)
Tactic:
induction n generalizing f init motive with
| zero => exact hinit
| succ n IH =>
  rewrite [foldRev_succ]
  apply hsucc
  exact @IH (motive ∘ succ) (f ∘ succ) init hinit (fun k => hsucc (k+1))
Proof state after:
no goals
Theorem: Nat.foldRev_induction
Proof state before:
case zero
α : Type u_1
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive zero init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (foldRev f zero init)
Tactic:
exact hinit
Proof state after:
no goals
Theorem: Nat.foldRev_induction
Proof state before:
case succ
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (foldRev f (succ n) init)
Tactic:
rewrite [foldRev_succ]
Proof state after:
case succ
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (f 0 (foldRev (f ∘ succ) n init))
Theorem: Nat.foldRev_induction
Proof state before:
case succ
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (f 0 (foldRev (f ∘ succ) n init))
Tactic:
apply hsucc
Proof state after:
case succ.a
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive (0 + 1) (foldRev (f ∘ succ) n init)
Theorem: Nat.foldRev_induction
Proof state before:
case succ.a
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive (0 + 1) (foldRev (f ∘ succ) n init)
Tactic:
exact @IH (motive ∘ succ) (f ∘ succ) init hinit (fun k => hsucc (k+1))
Proof state after:
no goals
Theorem: Nat.shiftRight_le_self
Proof state before:
n k : Nat
⊢ n >>> k ≤ n
Tactic:
induction k
Proof state after:
case zero
n : Nat
⊢ n >>> zero ≤ n

case succ
n n✝ : Nat
n_ih✝ : n >>> n✝ ≤ n
⊢ n >>> succ n✝ ≤ n
Theorem: Nat.shiftRight_le_self
Proof state before:
n : Nat
⊢ n >>> zero ≤ n
Tactic:
case zero => exact Nat.le.refl
Proof state after:
no goals
Theorem: Nat.shiftRight_le_self
Proof state before:
n k : Nat
h_ind : n >>> k ≤ n
⊢ n >>> succ k ≤ n
Tactic:
case succ k h_ind=>
  conv => lhs; change (n >>> k) / 2
  calc
    (n >>> k) / 2 ≤ n >>> k := Nat.div_le_self _ 2
    _             ≤ n := h_ind
Proof state after:
no goals
Theorem: Nat.shiftRight_le_self
Proof state before:
n : Nat
⊢ n >>> zero ≤ n
Tactic:
exact Nat.le.refl
Proof state after:
no goals
Theorem: Nat.shiftRight_le_self
Proof state before:
n k : Nat
h_ind : n >>> k ≤ n
⊢ n >>> succ k ≤ n
Tactic:
conv => lhs; change (n >>> k) / 2
Proof state after:
n k : Nat
h_ind : n >>> k ≤ n
⊢ n >>> k / 2 ≤ n
Theorem: Nat.shiftRight_le_self
Proof state before:
n k : Nat
h_ind : n >>> k ≤ n
⊢ n >>> k / 2 ≤ n
Tactic:
calc
  (n >>> k) / 2 ≤ n >>> k := Nat.div_le_self _ 2
  _             ≤ n := h_ind
Proof state after:
no goals
Theorem: Nat.shiftRight_lt
Proof state before:
n k : Nat
⊢ n ≠ 0 → k > 0 → shiftRight n k < n
Tactic:
intro hn hk
Proof state after:
n k : Nat
hn : n ≠ 0
hk : k > 0
⊢ shiftRight n k < n
Theorem: Nat.shiftRight_lt
Proof state before:
n k : Nat
hn : n ≠ 0
hk : k > 0
⊢ shiftRight n k < n
Tactic:
induction k
Proof state after:
case zero
n : Nat
hn : n ≠ 0
hk : zero > 0
⊢ shiftRight n zero < n

case succ
n : Nat
hn : n ≠ 0
n✝ : Nat
n_ih✝ : n✝ > 0 → shiftRight n n✝ < n
hk : succ n✝ > 0
⊢ shiftRight n (succ n✝) < n
Theorem: Nat.shiftRight_lt
Proof state before:
n : Nat
hn : n ≠ 0
hk : zero > 0
⊢ shiftRight n zero < n
Tactic:
case zero => exact absurd hk (Nat.lt_irrefl 0)
Proof state after:
no goals
Theorem: Nat.shiftRight_lt
Proof state before:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n (succ k) < n
Tactic:
case succ k h_ind =>
  unfold shiftRight
  cases Nat.eq_zero_or_pos k
  case inl h =>
    cases h; dsimp [shiftRight]
    exact Nat.div_lt_self (Nat.zero_lt_of_ne_zero hn) (Nat.lt_succ_self 1)
  case inr h =>
    calc
      shiftRight n k / 2
        ≤ shiftRight n k := Nat.div_le_self _ _
      _ < n := h_ind h
Proof state after:
no goals
Theorem: Nat.shiftRight_lt
Proof state before:
n : Nat
hn : n ≠ 0
hk : zero > 0
⊢ shiftRight n zero < n
Tactic:
exact absurd hk (Nat.lt_irrefl 0)
Proof state after:
no goals
Theorem: Nat.shiftRight_lt
Proof state before:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n (succ k) < n
Tactic:
unfold shiftRight
Proof state after:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n k / 2 < n
Theorem: Nat.shiftRight_lt
Proof state before:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n k / 2 < n
Tactic:
cases Nat.eq_zero_or_pos k
Proof state after:
case inl
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
h✝ : k = 0
⊢ shiftRight n k / 2 < n

case inr
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
h✝ : k > 0
⊢ shiftRight n k / 2 < n
Theorem: Nat.shiftRight_lt
Proof state before:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
h : k = 0
⊢ shiftRight n k / 2 < n
Tactic:
case inl h =>
  cases h; dsimp [shiftRight]
  exact Nat.div_lt_self (Nat.zero_lt_of_ne_zero hn) (Nat.lt_succ_self 1)
Proof state after:
no goals
Theorem: Nat.shiftRight_lt
Proof state before:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
h : k > 0
⊢ shiftRight n k / 2 < n
Tactic:
case inr h =>
  calc
    shiftRight n k / 2
      ≤ shiftRight n k := Nat.div_le_self _ _
    _ < n := h_ind h
Proof state after:
no goals
Theorem: Nat.shiftRight_lt
Proof state before:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
h : k = 0
⊢ shiftRight n k / 2 < n
Tactic:
cases h
Proof state after:
case refl
n : Nat
hn : n ≠ 0
h_ind : 0 > 0 → shiftRight n 0 < n
hk : succ 0 > 0
⊢ shiftRight n 0 / 2 < n
Theorem: Nat.shiftRight_lt
Proof state before:
case refl
n : Nat
hn : n ≠ 0
h_ind : 0 > 0 → shiftRight n 0 < n
hk : succ 0 > 0
⊢ shiftRight n 0 / 2 < n
Tactic:
dsimp [shiftRight]
Proof state after:
case refl
n : Nat
hn : n ≠ 0
h_ind : 0 > 0 → shiftRight n 0 < n
hk : succ 0 > 0
⊢ n / 2 < n
Theorem: Nat.shiftRight_lt
Proof state before:
case refl
n : Nat
hn : n ≠ 0
h_ind : 0 > 0 → shiftRight n 0 < n
hk : succ 0 > 0
⊢ n / 2 < n
Tactic:
exact Nat.div_lt_self (Nat.zero_lt_of_ne_zero hn) (Nat.lt_succ_self 1)
Proof state after:
no goals
Theorem: Nat.shiftRight_lt
Proof state before:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
h : k > 0
⊢ shiftRight n k / 2 < n
Tactic:
calc
  shiftRight n k / 2
    ≤ shiftRight n k := Nat.div_le_self _ _
  _ < n := h_ind h
Proof state after:
no goals
Theorem: FreeCMonoid.eq
Proof state before:
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar yvar : KVChain LT.lt fun x => valType
h : { vars := xvar }.vars = { vars := yvar }.vars
⊢ { vars := xvar } = { vars := yvar }
Tactic:
simp at h
Proof state after:
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar yvar : KVChain LT.lt fun x => valType
h : xvar = yvar
⊢ { vars := xvar } = { vars := yvar }
Theorem: FreeCMonoid.eq
Proof state before:
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar yvar : KVChain LT.lt fun x => valType
h : xvar = yvar
⊢ { vars := xvar } = { vars := yvar }
Tactic:
cases h
Proof state after:
case refl
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar : KVChain LT.lt fun x => valType
⊢ { vars := xvar } = { vars := xvar }
Theorem: FreeCMonoid.eq
Proof state before:
case refl
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar : KVChain LT.lt fun x => valType
⊢ { vars := xvar } = { vars := xvar }
Tactic:
rfl
Proof state after:
no goals
Theorem: FreeCMonoid.one_mul
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars : KVChain LT.lt fun x => valType
⊢ 1 * { vars := xvars } = { vars := xvars }
Tactic:
dsimp [OfNat.ofNat, HMul.hMul, Mul.mul]
Proof state after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars : KVChain LT.lt fun x => valType
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) KVChain.nil xvars } = { vars := xvars }
Theorem: FreeCMonoid.one_mul
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars : KVChain LT.lt fun x => valType
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) KVChain.nil xvars } = { vars := xvars }
Tactic:
rw [KVChain.nil_mergeWith]
Proof state after:
no goals
Theorem: FreeCMonoid.mul_one
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars : KVChain LT.lt fun x => valType
⊢ { vars := xvars } * 1 = { vars := xvars }
Tactic:
dsimp [OfNat.ofNat, HMul.hMul, Mul.mul]
Proof state after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars : KVChain LT.lt fun x => valType
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xvars KVChain.nil } = { vars := xvars }
Theorem: FreeCMonoid.mul_one
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars : KVChain LT.lt fun x => valType
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xvars KVChain.nil } = { vars := xvars }
Tactic:
rw [KVChain.mergeWith_nil]
Proof state after:
no goals