internlm/Lean-Github huggingface dataset:
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
case hi.h₂.left
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ true = decide (Nat.bit b n ≠ 0)

case hi.h₂.right
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)
Tactic:
exact Eq.symm (decide_eq_true λ h ↦ absurd ((Nat.bit_eq_zero.mp h).right.symm.trans (hn (Nat.bit_eq_zero.mp h).left)) Bool.noConfusion)
Proof state after:
case hi.h₂.right
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
case hi.h₂.right
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)
Tactic:
cases b <;> simp [-Nat.bit_false, -Nat.bit_true, Nat.bit_mod_two, Nat.bit_div_2]
Proof state after:
case hi.h₂.right.false
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → false = true
⊢ encodeList (Nat.bits n) = encode n

case hi.h₂.right.true
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → true = true
⊢ encodeList (Nat.bits n) = encode n
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
case hi.h₂.right.false
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → false = true
⊢ encodeList (Nat.bits n) = encode n

case hi.h₂.right.true
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → true = true
⊢ encodeList (Nat.bits n) = encode n
Tactic:
rfl
Proof state after:
case hi.h₂.right.true
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → true = true
⊢ encodeList (Nat.bits n) = encode n
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
case hi.h₂.right.true
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → true = true
⊢ encodeList (Nat.bits n) = encode n
Tactic:
rfl
Proof state after:
no goals
Theorem: HMem.Encoding.decode_succ
Proof state before:
hd tl : Memory
⊢ decode ℕ (Memory.mk true hd tl) = Option.map (fun n => 2 * n + Bool.toNat (Memory.getv hd)) (decode ℕ tl)
Tactic:
simp [decode_nat]
Proof state after:
hd tl : Memory
⊢ Option.map (Nat.ofBits ∘ fun b => Memory.getv hd :: b) (decode (List Bool) tl) =
    Option.map ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) (decode (List Bool) tl)
Theorem: HMem.Encoding.decode_succ
Proof state before:
hd tl : Memory
⊢ Option.map (Nat.ofBits ∘ fun b => Memory.getv hd :: b) (decode (List Bool) tl) =
    Option.map ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) (decode (List Bool) tl)
Tactic:
apply congrArg₂ Option.map _ rfl
Proof state after:
hd tl : Memory
⊢ (Nat.ofBits ∘ fun b => Memory.getv hd :: b) = (fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits
Theorem: HMem.Encoding.decode_succ
Proof state before:
hd tl : Memory
⊢ (Nat.ofBits ∘ fun b => Memory.getv hd :: b) = (fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits
Tactic:
apply funext
Proof state after:
case h
hd tl : Memory
⊢ ∀ (x : List Bool),
    (Nat.ofBits ∘ fun b => Memory.getv hd :: b) x = ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) x
Theorem: HMem.Encoding.decode_succ
Proof state before:
case h
hd tl : Memory
⊢ ∀ (x : List Bool),
    (Nat.ofBits ∘ fun b => Memory.getv hd :: b) x = ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) x
Tactic:
intro xs
Proof state after:
case h
hd tl : Memory
xs : List Bool
⊢ (Nat.ofBits ∘ fun b => Memory.getv hd :: b) xs = ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) xs
Theorem: HMem.Encoding.decode_succ
Proof state before:
case h
hd tl : Memory
xs : List Bool
⊢ (Nat.ofBits ∘ fun b => Memory.getv hd :: b) xs = ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) xs
Tactic:
simp [Nat.ofBits]
Proof state after:
case h
hd tl : Memory
xs : List Bool
⊢ Nat.bit (Memory.getv hd) (Nat.ofBits xs) = 2 * Nat.ofBits xs + Bool.toNat (Memory.getv hd)
Theorem: HMem.Encoding.decode_succ
Proof state before:
case h
hd tl : Memory
xs : List Bool
⊢ Nat.bit (Memory.getv hd) (Nat.ofBits xs) = 2 * Nat.ofBits xs + Bool.toNat (Memory.getv hd)
Tactic:
match HMem.Memory.getv hd with
| true => simp [← Nat.two_mul]
| false => simp [← Nat.two_mul]
Proof state after:
no goals
Theorem: HMem.Encoding.decode_succ
Proof state before:
hd tl : Memory
xs : List Bool
⊢ Nat.bit true (Nat.ofBits xs) = 2 * Nat.ofBits xs + Bool.toNat true
Tactic:
simp [← Nat.two_mul]
Proof state after:
no goals
Theorem: HMem.Encoding.decode_succ
Proof state before:
hd tl : Memory
xs : List Bool
⊢ Nat.bit false (Nat.ofBits xs) = 2 * Nat.ofBits xs + Bool.toNat false
Tactic:
simp [← Nat.two_mul]
Proof state after:
no goals
Theorem: HMem.Memory.canonical_congr
Proof state before:
v₀ : Bool
lhs₀ rhs₀ t₁ : Tree Bool
hv : Tree.getOrElse 1 (Tree.node v₀ lhs₀ rhs₀) false = Tree.getOrElse 1 t₁ false
hl : canonical (Tree.left (Tree.node v₀ lhs₀ rhs₀)) = canonical (Tree.left t₁)
hr : canonical (Tree.right (Tree.node v₀ lhs₀ rhs₀)) = canonical (Tree.right t₁)
h₀ : canonical (Tree.node v₀ lhs₀ rhs₀) = Tree.nil
h₁ : canonical t₁ = Tree.node (Tree.getOrElse 1 t₁ false) (canonical (Tree.left t₁)) (canonical (Tree.right t₁))
⊢ canonical (Tree.node v₀ lhs₀ rhs₀) = canonical t₁
Tactic:
apply absurd (h₁.symm.trans (canonical_nil
    (hv.symm.trans (canonical_getOrElse.symm.trans (congrArg (λ t ↦ Tree.getOrElse 1 t false) h₀)))
    (hl.symm.trans (canonical_left.trans (congrArg _ h₀)))
    (hr.symm.trans (canonical_right.trans (congrArg _ h₀)))))
  Tree.noConfusion
Proof state after:
no goals
Theorem: Option.filter_eq_some'
Proof state before:
α : Type u_1
f : α → Bool
b✝ b : α
⊢ Option.filter f (some b) = some b✝ ↔ some b = some b✝ ∧ f b✝ = true
Tactic:
simpa [Option.filter, And.comm (a := Eq b _)] using λ heq ↦ heq ▸ ⟨id, id⟩
Proof state after:
no goals
Theorem: Option.forall_mem_filter
Proof state before:
α : Type u_1
f : α → Bool
o : Option α
p : α → Prop
⊢ (∀ y ∈ Option.filter f o, p y) ↔ ∀ x ∈ o, f x = true → p x
Tactic:
simp
Proof state after:
no goals
Theorem: Option.forall_mem_bind
Proof state before:
α : Type u_1
β : Type u_2
f : α → Option β
o : Option α
p : β → Prop
⊢ (∀ y ∈ Option.bind o f, p y) ↔ ∀ x ∈ o, ∀ y ∈ f x, p y
Tactic:
simpa using ⟨ λ h _ hx _ ↦ h _ _ hx, λ h _ _ hx ↦ h _ hx _ ⟩
Proof state after:
no goals
Theorem: HMem.Trace.TracedProgram.sound_subroutine_arg
Proof state before:
α : Type u_2
inst✝¹ : Complexity.Coding α Memory
β : Type u_3
inst✝ : Complexity.Encoding β Memory
f : α → β
γ : Type u_1
δ : Type
enγ : Complexity.Coding γ Memory
enδ : Complexity.Encoding δ Memory
fs : γ → δ
hc : Complexity.Computable Encoding.Model fs
size : α → ℕ
a : α
dst src : Source
next : TracedProgram
m : Memory
h : sound f size a (subroutine dst src fs next) m
x✝ : γ
hm : Memory.getms m src = Complexity.encode x✝
right✝ : sound f size a next (Memory.setms m dst (Complexity.encode (fs x✝)))
⊢ Memory.getms m src =
    Complexity.encode
      (Option.get (Complexity.decode γ (Memory.getms m src))
        (_ : Option.isSome (Complexity.decode γ (Memory.getms m src)) = true))
Tactic:
simp only [hm, Complexity.decode_inv, Option.get_some]
Proof state after:
no goals
Theorem: HMem.Trace.TracedProgram.sound_subroutine_next
Proof state before:
α : Type u_2
inst✝¹ : Complexity.Coding α Memory
β : Type u_3
inst✝ : Complexity.Encoding β Memory
f : α → β
γ : Type u_1
δ : Type
enγ : Complexity.Coding γ Memory
enδ : Complexity.Encoding δ Memory
fs : γ → δ
hc : Complexity.Computable Encoding.Model fs
size : α → ℕ
a : α
dst src : Source
next : TracedProgram
m : Memory
h✝ : sound f size a (subroutine dst src fs next) m
x✝ : γ
hm : Memory.getms m src = Complexity.encode x✝
h : sound f size a next (Memory.setms m dst (Complexity.encode (fs x✝)))
⊢ sound f size a next
    (Memory.setms m dst
      (Complexity.encode
        (fs
          (Option.get (Complexity.decode γ (Memory.getms m src))
            (_ : Option.isSome (Complexity.decode γ (Memory.getms m src)) = true)))))
Tactic:
simpa only [hm, Complexity.decode_inv, Option.get_some] using h
Proof state after:
no goals
Theorem: HMem.Trace.TracedProgram.sound_recurse_arg
Proof state before:
α : Type u_2
inst✝¹ : Complexity.Coding α Memory
β : Type u_3
inst✝ : Complexity.Encoding β Memory
f : α → β
γ : Type ?u.37426
δ : Type
enγ : Complexity.Coding γ Memory
enδ : Complexity.Encoding δ Memory
fs : γ → δ
hc : Complexity.Computable Encoding.Model fs
size : α → ℕ
a : α
dst src : Source
next : TracedProgram
m : Memory
h : sound f size a (recurse dst src next) m
x✝ : α
hm : Memory.getms m src = Complexity.encode x✝
left✝ : size x✝ < size a
right✝ : sound f size a next (Memory.setms m dst (Complexity.encode (f x✝)))
⊢ Memory.getms m src =
    Complexity.encode
      (Option.get (Complexity.decode α (Memory.getms m src))
        (_ : Option.isSome (Complexity.decode α (Memory.getms m src)) = true))
Tactic:
simp only [hm, Complexity.decode_inv, Option.get_some]
Proof state after:
no goals
Theorem: HMem.Trace.TracedProgram.sound_recurse_size
Proof state before:
α : Type u_2
inst✝¹ : Complexity.Coding α Memory
β : Type u_3
inst✝ : Complexity.Encoding β Memory
f : α → β
γ : Type ?u.39174
δ : Type
enγ : Complexity.Coding γ Memory
enδ : Complexity.Encoding δ Memory
fs : γ → δ
hc : Complexity.Computable Encoding.Model fs
size : α → ℕ
a : α
dst src : Source
next : TracedProgram
m : Memory
h : sound f size a (recurse dst src next) m
x✝ : α
hm : Memory.getms m src = Complexity.encode x✝
hs : size x✝ < size a
right✝ : sound f size a next (Memory.setms m dst (Complexity.encode (f x✝)))
⊢ size
      (Option.get (Complexity.decode α (Memory.getms m src))
        (_ : Option.isSome (Complexity.decode α (Memory.getms m src)) = true)) <
    size a
Tactic:
simpa only [hm, Complexity.decode_inv, Option.get_some] using hs
Proof state after:
no goals
Theorem: HMem.Trace.TracedProgram.sound_recurse_next
Proof state before:
α : Type u_2
inst✝¹ : Complexity.Coding α Memory
β : Type u_3
inst✝ : Complexity.Encoding β Memory
f : α → β
γ : Type ?u.40501
δ : Type
enγ : Complexity.Coding γ Memory
enδ : Complexity.Encoding δ Memory
fs : γ → δ
hc : Complexity.Computable Encoding.Model fs
size : α → ℕ
a : α
dst src : Source
next : TracedProgram
m : Memory
h✝ : sound f size a (recurse dst src next) m
x✝ : α
hm : Memory.getms m src = Complexity.encode x✝
left✝ : size x✝ < size a
h : sound f size a next (Memory.setms m dst (Complexity.encode (f x✝)))
⊢ sound f size a next
    (Memory.setms m dst
      (Complexity.encode
        (f
          (Option.get (Complexity.decode α (Memory.getms m src))
            (_ : Option.isSome (Complexity.decode α (Memory.getms m src)) = true)))))
Tactic:
simpa only [hm, Complexity.decode_inv, Option.get_some] using h
Proof state after:
no goals
Theorem: Complexity.CostFunction.flatMap_none
Proof state before:
α : Type u_3
β : Type u_2
θ : Type u_1
inst✝ : Zero θ
f : α → Option β
a : α
h : f a = none
g : CostFunction β θ
⊢ flatMap f g a = 0
Tactic:
simp[flatMap, h]
Proof state after:
no goals
Theorem: Complexity.CostFunction.flatMap_some
Proof state before:
α : Type u_3
β : Type u_2
θ : Type u_1
inst✝ : Zero θ
f : α → Option β
a : α
b : β
h : f a = some b
g : CostFunction β θ
⊢ flatMap f g a = g b
Tactic:
simp[flatMap, h]
Proof state after:
no goals
Theorem: List.cons_append_inj
Proof state before:
α : Type u_1
a : α
x y z : List α
⊢ a :: (y ++ x) = z ++ x ↔ a :: y = z
Tactic:
simp [-List.cons_append, (List.cons_append _ _ _).symm]
Proof state after:
no goals
Theorem: List.cons₂_append_inj
Proof state before:
α : Type u_1
a b : α
x y z : List α
⊢ a :: b :: (y ++ x) = z ++ x ↔ a :: b :: y = z
Tactic:
simp [-List.cons_append, (List.cons_append _ _ _).symm]
Proof state after:
no goals
Theorem: Nat.bit_div_2
Proof state before:
b : Bool
n : ℕ
⊢ bit b n / 2 = n
Tactic:
set_option linter.deprecated false in
cases b <;> dsimp [bit, bit0, bit1] <;> omega
Proof state after:
no goals
Theorem: Nat.bit_div_2
Proof state before:
b : Bool
n : ℕ
⊢ bit b n / 2 = n
Tactic:
cases b <;> dsimp [bit, bit0, bit1] <;> omega
Proof state after:
no goals
Theorem: Nat.pred_lt_iff
Proof state before:
n : ℕ
⊢ n - 1 < n ↔ n ≠ 0
Tactic:
cases n <;> simp
Proof state after:
no goals
Theorem: Nat.size_div2
Proof state before:
n : ℕ
⊢ size (n / 2) = size n - 1
Tactic:
induction n using Nat.binaryRec' with
| z => rfl
| _ _ _ h =>
  rw [bit_div_2, size_bit]
  apply Eq.symm
  apply Nat.pred_succ
  apply bit_ne_zero_iff.mpr h
Proof state after:
no goals
Theorem: Nat.size_div2
Proof state before:
case z

⊢ size (0 / 2) = size 0 - 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.size_div2
Proof state before:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ size (bit b✝ n✝ / 2) = size (bit b✝ n✝) - 1
Tactic:
rw [bit_div_2, size_bit]
Proof state after:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ size n✝ = succ (size n✝) - 1

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0
Theorem: Nat.size_div2
Proof state before:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ size n✝ = succ (size n✝) - 1

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0
Tactic:
apply Eq.symm
Proof state after:
case f.h
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ succ (size n✝) - 1 = size n✝

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0
Theorem: Nat.size_div2
Proof state before:
case f.h
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ succ (size n✝) - 1 = size n✝

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0
Tactic:
apply Nat.pred_succ
Proof state after:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0
Theorem: Nat.size_div2
Proof state before:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0
Tactic:
apply bit_ne_zero_iff.mpr h
Proof state after:
no goals
Theorem: Nat.mod_mul
Proof state before:
a b c : ℕ
⊢ a % (b * c) = b * (a / b % c) + a % b
Tactic:
match b with
| 0 => simp
| b + 1 =>
  match c with
  | 0 => simp[Nat.div_add_mod]
  | c + 1 =>
    apply Eq.trans
    apply congrArg₂ _ (Nat.div_add_mod a (b + 1)).symm rfl
    apply Eq.trans
    apply Nat.add_mod
    apply Eq.trans
    exact congrArg₂ _ (congrArg₂ _ (Nat.mul_mod_mul_left _ _ _) (Nat.mod_eq_of_lt (lt_of_lt_of_le (Nat.mod_lt _ (Nat.zero_lt_succ _)) (Nat.le_mul_of_pos_right (Nat.zero_lt_succ _))))) rfl
    apply Nat.mod_eq_of_lt
    apply Nat.lt_of_succ_le
    apply le_trans
    apply Nat.succ_le_succ
    apply add_le_add
    apply Nat.mul_le_mul_left
    apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
    apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
    simp [Nat.succ_eq_add_one, left_distrib, right_distrib, ← add_assoc]
Proof state after:
no goals
Theorem: Nat.mod_mul
Proof state before:
a b c : ℕ
⊢ a % (0 * c) = 0 * (a / 0 % c) + a % 0
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.mod_mul
Proof state before:
a b✝ c b : ℕ
⊢ a % ((b + 1) * c) = (b + 1) * (a / (b + 1) % c) + a % (b + 1)
Tactic:
match c with
| 0 => simp[Nat.div_add_mod]
| c + 1 =>
  apply Eq.trans
  apply congrArg₂ _ (Nat.div_add_mod a (b + 1)).symm rfl
  apply Eq.trans
  apply Nat.add_mod
  apply Eq.trans
  exact congrArg₂ _ (congrArg₂ _ (Nat.mul_mod_mul_left _ _ _) (Nat.mod_eq_of_lt (lt_of_lt_of_le (Nat.mod_lt _ (Nat.zero_lt_succ _)) (Nat.le_mul_of_pos_right (Nat.zero_lt_succ _))))) rfl
  apply Nat.mod_eq_of_lt
  apply Nat.lt_of_succ_le
  apply le_trans
  apply Nat.succ_le_succ
  apply add_le_add
  apply Nat.mul_le_mul_left
  apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
  apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
  simp [Nat.succ_eq_add_one, left_distrib, right_distrib, ← add_assoc]
Proof state after:
no goals
Theorem: Nat.mod_mul
Proof state before:
a b✝ c b : ℕ
⊢ a % ((b + 1) * 0) = (b + 1) * (a / (b + 1) % 0) + a % (b + 1)
Tactic:
simp[Nat.div_add_mod]
Proof state after:
no goals
Theorem: Nat.mod_mul
Proof state before:
a b✝ c✝ b c : ℕ
⊢ a % ((b + 1) * (c + 1)) = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Tactic:
apply Eq.trans
Proof state after:
case h₁
a b✝ c✝ b c : ℕ
⊢ a % ((b + 1) * (c + 1)) = ?b

case h₂
a b✝ c✝ b c : ℕ
⊢ ?b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case b
a b✝ c✝ b c : ℕ
⊢ ℕ
Theorem: Nat.mod_mul
Proof state before:
case h₁
a b✝ c✝ b c : ℕ
⊢ a % ((b + 1) * (c + 1)) = ?b

case h₂
a b✝ c✝ b c : ℕ
⊢ ?b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case b
a b✝ c✝ b c : ℕ
⊢ ℕ
Tactic:
apply congrArg₂ _ (Nat.div_add_mod a (b + 1)).symm rfl
Proof state after:
case h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Theorem: Nat.mod_mul
Proof state before:
case h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Tactic:
apply Eq.trans
Proof state after:
case h₂.h₁
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) = ?h₂.b

case h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ?h₂.b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case h₂.b
a b✝ c✝ b c : ℕ
⊢ ℕ
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₁
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) = ?h₂.b

case h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ?h₂.b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case h₂.b
a b✝ c✝ b c : ℕ
⊢ ℕ
Tactic:
apply Nat.add_mod
Proof state after:
case h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) % ((b + 1) * (c + 1)) + a % (b + 1) % ((b + 1) * (c + 1))) % ((b + 1) * (c + 1)) =
    (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) % ((b + 1) * (c + 1)) + a % (b + 1) % ((b + 1) * (c + 1))) % ((b + 1) * (c + 1)) =
    (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Tactic:
apply Eq.trans
Proof state after:
case h₂.h₂.h₁
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) % ((b + 1) * (c + 1)) + a % (b + 1) % ((b + 1) * (c + 1))) % ((b + 1) * (c + 1)) = ?h₂.h₂.b

case h₂.h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ?h₂.h₂.b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case h₂.h₂.b
a b✝ c✝ b c : ℕ
⊢ ℕ
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂.h₁
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) % ((b + 1) * (c + 1)) + a % (b + 1) % ((b + 1) * (c + 1))) % ((b + 1) * (c + 1)) = ?h₂.h₂.b

case h₂.h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ?h₂.h₂.b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case h₂.h₂.b
a b✝ c✝ b c : ℕ
⊢ ℕ
Tactic:
exact congrArg₂ _ (congrArg₂ _ (Nat.mul_mod_mul_left _ _ _) (Nat.mod_eq_of_lt (lt_of_lt_of_le (Nat.mod_lt _ (Nat.zero_lt_succ _)) (Nat.le_mul_of_pos_right (Nat.zero_lt_succ _))))) rfl
Proof state after:
case h₂.h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) =
    (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) =
    (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Tactic:
apply Nat.mod_eq_of_lt
Proof state after:
case h₂.h₂.h₂.h
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1) < (b + 1) * (c + 1)
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂.h₂.h
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1) < (b + 1) * (c + 1)
Tactic:
apply Nat.lt_of_succ_le
Proof state after:
case h₂.h₂.h₂.h.h
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) ≤ (b + 1) * (c + 1)
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂.h₂.h.h
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) ≤ (b + 1) * (c + 1)
Tactic:
apply le_trans
Proof state after:
case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) ≤ ?h₂.h₂.h₂.h.h.b

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ ?h₂.h₂.h₂.h.h.b ≤ (b + 1) * (c + 1)

case h₂.h₂.h₂.h.h.b
a b✝ c✝ b c : ℕ
⊢ ℕ
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) ≤ ?h₂.h₂.h₂.h.h.b

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ ?h₂.h₂.h₂.h.h.b ≤ (b + 1) * (c + 1)

case h₂.h₂.h₂.h.h.b
a b✝ c✝ b c : ℕ
⊢ ℕ
Tactic:
apply Nat.succ_le_succ
Proof state after:
case h₂.h₂.h₂.h.h.a.a
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.m

case h₂.h₂.h₂.h.h.a.m
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ?h₂.h₂.h₂.h.h.a.m ≤ (b + 1) * (c + 1)
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂.h₂.h.h.a.a
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.m

case h₂.h₂.h₂.h.h.a.m
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ?h₂.h₂.h₂.h.h.a.m ≤ (b + 1) * (c + 1)
Tactic:
apply add_le_add
Proof state after:
case h₂.h₂.h₂.h.h.a.a.h₁
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) ≤ ?h₂.h₂.h₂.h.h.a.a.b

case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.b
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ (?h₂.h₂.h₂.h.h.a.a.b + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂.h₂.h.h.a.a.h₁
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) ≤ ?h₂.h₂.h₂.h.h.a.a.b

case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.b
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ (?h₂.h₂.h₂.h.h.a.a.b + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)
Tactic:
apply Nat.mul_le_mul_left
Proof state after:
case h₂.h₂.h₂.h.h.a.a.h₁.h
a b✝ c✝ b c : ℕ
⊢ a / (b + 1) % (c + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.h₁.m

case h₂.h₂.h₂.h.h.a.a.h₁.m
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * ?h₂.h₂.h₂.h.h.a.a.h₁.m + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂.h₂.h.h.a.a.h₁.h
a b✝ c✝ b c : ℕ
⊢ a / (b + 1) % (c + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.h₁.m

case h₂.h₂.h₂.h.h.a.a.h₁.m
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * ?h₂.h₂.h₂.h.h.a.a.h₁.m + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)
Tactic:
apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
Proof state after:
case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * c + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * c + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)
Tactic:
apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
Proof state after:
case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * c + b) ≤ (b + 1) * (c + 1)
Theorem: Nat.mod_mul
Proof state before:
case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * c + b) ≤ (b + 1) * (c + 1)
Tactic:
simp [Nat.succ_eq_add_one, left_distrib, right_distrib, ← add_assoc]
Proof state after:
no goals