internlm/Lean-Github huggingface dataset:
Theorem: Stream'.dropEveryNth_two_eq_even
Proof state before:
case hg
α : Type u_1
σ : Stream' α
⊢ ∀ (a : Stream' α × ℕ) (a' : Stream' α),
    (match a with
      | (σ, n) => σ = a' ∧ n = 0) →
      match
        match a with
        | (σ, 0) => (tail (tail σ), 0)
        | (σ, Nat.succ m) => (tail σ, m) with
      | (σ, n) => σ = tail (tail a') ∧ n = 0
Tactic:
rintro ⟨σ, n⟩ σ' ⟨⟨⟩, ⟨⟩⟩
Proof state after:
case hg.mk.intro.refl.refl
α : Type u_1
σ✝ σ : Stream' α
⊢ match
    match (σ, 0) with
    | (σ, 0) => (tail (tail σ), 0)
    | (σ, Nat.succ m) => (tail σ, m) with
  | (σ_1, n) => σ_1 = tail (tail σ) ∧ n = 0
Theorem: Stream'.dropEveryNth_two_eq_even
Proof state before:
case hg.mk.intro.refl.refl
α : Type u_1
σ✝ σ : Stream' α
⊢ match
    match (σ, 0) with
    | (σ, 0) => (tail (tail σ), 0)
    | (σ, Nat.succ m) => (tail σ, m) with
  | (σ_1, n) => σ_1 = tail (tail σ) ∧ n = 0
Tactic:
simp [tail, nth]
Proof state after:
no goals
Theorem: Stream'.dropEveryNth_two_eq_even
Proof state before:
case a
α : Type u_1
σ : Stream' α
⊢ match (σ, 0) with
  | (σ_1, n) => σ_1 = σ ∧ n = 0
Tactic:
exact ⟨rfl, rfl⟩
Proof state after:
no goals
Theorem: Stream'.dropEveryNth_two_eq_mul_two
Proof state before:
α : Type u_1
σ✝ σ : Stream' α
⊢ dropEveryNth 2 σ = fun i => σ (i * 2)
Tactic:
rw [dropEveryNth_two_eq_even, even_eq_mul_two]
Proof state after:
no goals
Theorem: Stream'.corec_sub_corec
Proof state before:
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁ : α₁
x₂ : α₂
inst✝ : Sub β
⊢ (fun i => Sub.sub (corec f₁ g₁ x₁ i) (corec f₂ g₂ x₂ i)) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂)
Tactic:
funext i
Proof state after:
case h
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁ : α₁
x₂ : α₂
inst✝ : Sub β
i : ℕ
⊢ Sub.sub (corec f₁ g₁ x₁ i) (corec f₂ g₂ x₂ i) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) i
Theorem: Stream'.corec_sub_corec
Proof state before:
case h
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁ : α₁
x₂ : α₂
inst✝ : Sub β
i : ℕ
⊢ Sub.sub (corec f₁ g₁ x₁ i) (corec f₂ g₂ x₂ i) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) i
Tactic:
induction' i with i ih generalizing x₁ x₂
Proof state after:
case h.zero
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁✝ : α₁
x₂✝ : α₂
inst✝ : Sub β
x₁ : α₁
x₂ : α₂
⊢ Sub.sub (corec f₁ g₁ x₁ Nat.zero) (corec f₂ g₂ x₂ Nat.zero) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) Nat.zero

case h.succ
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁✝ : α₁
x₂✝ : α₂
inst✝ : Sub β
i : ℕ
ih :
  ∀ {x₁ : α₁} {x₂ : α₂},
    Sub.sub (corec f₁ g₁ x₁ i) (corec f₂ g₂ x₂ i) =
      corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) i
x₁ : α₁
x₂ : α₂
⊢ Sub.sub (corec f₁ g₁ x₁ (Nat.succ i)) (corec f₂ g₂ x₂ (Nat.succ i)) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) (Nat.succ i)
Theorem: Stream'.corec_sub_corec
Proof state before:
case h.zero
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁✝ : α₁
x₂✝ : α₂
inst✝ : Sub β
x₁ : α₁
x₂ : α₂
⊢ Sub.sub (corec f₁ g₁ x₁ Nat.zero) (corec f₂ g₂ x₂ Nat.zero) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: Stream'.corec_sub_corec
Proof state before:
case h.succ
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁✝ : α₁
x₂✝ : α₂
inst✝ : Sub β
i : ℕ
ih :
  ∀ {x₁ : α₁} {x₂ : α₂},
    Sub.sub (corec f₁ g₁ x₁ i) (corec f₂ g₂ x₂ i) =
      corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) i
x₁ : α₁
x₂ : α₂
⊢ Sub.sub (corec f₁ g₁ x₁ (Nat.succ i)) (corec f₂ g₂ x₂ (Nat.succ i)) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) (Nat.succ i)
Tactic:
simp [corec_succ, ih]
Proof state after:
no goals
Theorem: procedure_two_eq_squares
Proof state before:
⊢ sum (dropEveryNth 2 pnats) = powers 2
Tactic:
funext i
Proof state after:
case h
i : ℕ
⊢ sum (dropEveryNth 2 pnats) i = powers 2 i
Theorem: procedure_two_eq_squares
Proof state before:
case h
i : ℕ
⊢ sum (dropEveryNth 2 pnats) i = powers 2 i
Tactic:
simp [dropEveryNth_two_eq_mul_two, powers, pnats]
Proof state after:
case h
i : ℕ
⊢ sum (fun i => i * 2 + 1) i = (i + 1) ^ 2
Theorem: procedure_two_eq_squares
Proof state before:
case h
i : ℕ
⊢ sum (fun i => i * 2 + 1) i = (i + 1) ^ 2
Tactic:
induction' i with i ih
Proof state after:
case h.zero

⊢ sum (fun i => i * 2 + 1) Nat.zero = (Nat.zero + 1) ^ 2

case h.succ
i : ℕ
ih : sum (fun i => i * 2 + 1) i = (i + 1) ^ 2
⊢ sum (fun i => i * 2 + 1) (Nat.succ i) = (Nat.succ i + 1) ^ 2
Theorem: procedure_two_eq_squares
Proof state before:
case h.zero

⊢ sum (fun i => i * 2 + 1) Nat.zero = (Nat.zero + 1) ^ 2
Tactic:
rfl
Proof state after:
no goals
Theorem: procedure_two_eq_squares
Proof state before:
case h.succ
i : ℕ
ih : sum (fun i => i * 2 + 1) i = (i + 1) ^ 2
⊢ sum (fun i => i * 2 + 1) (Nat.succ i) = (Nat.succ i + 1) ^ 2
Tactic:
simp only [sum_succ, ih, pow_two, (show Nat.succ i = i + 1 from rfl)]
Proof state after:
case h.succ
i : ℕ
ih : sum (fun i => i * 2 + 1) i = (i + 1) ^ 2
⊢ (i + 1) * (i + 1) + ((i + 1) * 2 + 1) = (i + 1 + 1) * (i + 1 + 1)
Theorem: procedure_two_eq_squares
Proof state before:
case h.succ
i : ℕ
ih : sum (fun i => i * 2 + 1) i = (i + 1) ^ 2
⊢ (i + 1) * (i + 1) + ((i + 1) * 2 + 1) = (i + 1 + 1) * (i + 1 + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: sumDrop_two
Proof state before:
⊢ sumDrop 2 pnats = powers 2
Tactic:
simp only [sumDrop]
Proof state after:
⊢ sum (dropEveryNth (1 + 1) pnats) = powers 2
Theorem: sumDrop_two
Proof state before:
⊢ sum (dropEveryNth (1 + 1) pnats) = powers 2
Tactic:
rw [procedure_two_eq_squares]
Proof state after:
no goals
Theorem: Nat.not_dvd_of_mod_neq_zero
Proof state before:
a b : ℕ
⊢ a % b ≠ 0 → ¬b ∣ a
Tactic:
rw [Nat.dvd_iff_mod_eq_zero]
Proof state after:
a b : ℕ
⊢ a % b ≠ 0 → ¬a % b = 0
Theorem: Nat.not_dvd_of_mod_neq_zero
Proof state before:
a b : ℕ
⊢ a % b ≠ 0 → ¬a % b = 0
Tactic:
exact id
Proof state after:
no goals
Theorem: dropEveryNth_three_eq_fun
Proof state before:
α✝ : Type u_1
σ : Stream' α✝
⊢ dropEveryNth 3 σ = fun i => σ (i + i / 2)
Tactic:
rw [dropEveryNth, fun_to_corec fun i => σ (i + i/2)]
Proof state after:
α✝ : Type u_1
σ : Stream' α✝
⊢ corec
      (fun x =>
        match x with
        | (σ, snd) => head σ)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), 3 - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, 3 - 2) =
    corec (fun i => σ (i + i / 2)) (fun x => x + 1) 0
Theorem: dropEveryNth_three_eq_fun
Proof state before:
α✝ : Type u_1
σ : Stream' α✝
⊢ corec
      (fun x =>
        match x with
        | (σ, snd) => head σ)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), 3 - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, 3 - 2) =
    corec (fun i => σ (i + i / 2)) (fun x => x + 1) 0
Tactic:
apply corec_bisim (fun ⟨σ', c⟩ i => σ' = (σ.drop <| i + i/2) 
  ∧ c = (i+1) % 2)
Proof state after:
case hf
α✝ : Type u_1
σ : Stream' α✝
⊢ ∀ (a : Stream' α✝ × ℕ) (a' : ℕ),
    (match a with
      | (σ', c) => σ' = drop (a' + a' / 2) σ ∧ c = (a' + 1) % 2) →
      (match a with
        | (σ, snd) => head σ) =
        σ (a' + a' / 2)

case hg
α✝ : Type u_1
σ : Stream' α✝
⊢ ∀ (a : Stream' α✝ × ℕ) (a' : ℕ),
    (match a with
      | (σ', c) => σ' = drop (a' + a' / 2) σ ∧ c = (a' + 1) % 2) →
      match
        match a with
        | (σ, 0) => (tail (tail σ), 3 - 2)
        | (σ, Nat.succ m) => (tail σ, m) with
      | (σ', c) => σ' = drop (a' + 1 + (a' + 1) / 2) σ ∧ c = (a' + 1 + 1) % 2

case a
α✝ : Type u_1
σ : Stream' α✝
⊢ match (σ, 3 - 2) with
  | (σ', c) => σ' = drop (0 + 0 / 2) σ ∧ c = (0 + 1) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hf
α✝ : Type u_1
σ : Stream' α✝
⊢ ∀ (a : Stream' α✝ × ℕ) (a' : ℕ),
    (match a with
      | (σ', c) => σ' = drop (a' + a' / 2) σ ∧ c = (a' + 1) % 2) →
      (match a with
        | (σ, snd) => head σ) =
        σ (a' + a' / 2)
Tactic:
rintro ⟨_, _⟩ i ⟨⟨⟩, ⟨⟩⟩
Proof state after:
case hf.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
    | (σ, snd) => head σ) =
    σ (i + i / 2)
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hf.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
    | (σ, snd) => head σ) =
    σ (i + i / 2)
Tactic:
simp only [head, nth, drop, zero_add]
Proof state after:
no goals
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg
α✝ : Type u_1
σ : Stream' α✝
⊢ ∀ (a : Stream' α✝ × ℕ) (a' : ℕ),
    (match a with
      | (σ', c) => σ' = drop (a' + a' / 2) σ ∧ c = (a' + 1) % 2) →
      match
        match a with
        | (σ, 0) => (tail (tail σ), 3 - 2)
        | (σ, Nat.succ m) => (tail σ, m) with
      | (σ', c) => σ' = drop (a' + 1 + (a' + 1) / 2) σ ∧ c = (a' + 1 + 1) % 2
Tactic:
rintro ⟨_, _⟩ i ⟨⟨⟩, ⟨⟩⟩
Proof state after:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ match
    match (drop (i + i / 2) σ, (i + 1) % 2) with
    | (σ, 0) => (tail (tail σ), 3 - 2)
    | (σ, Nat.succ m) => (tail σ, m) with
  | (σ', c) => σ' = drop (i + 1 + (i + 1) / 2) σ ∧ c = (i + 1 + 1) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ match
    match (drop (i + i / 2) σ, (i + 1) % 2) with
    | (σ, 0) => (tail (tail σ), 3 - 2)
    | (σ, Nat.succ m) => (tail σ, m) with
  | (σ', c) => σ' = drop (i + 1 + (i + 1) / 2) σ ∧ c = (i + 1 + 1) % 2
Tactic:
simp
Proof state after:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (i + 1 + 1) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (i + 1 + 1) % 2
Tactic:
rw [Nat.add_mod (i+1) 1]
Proof state after:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      ((i + 1) % 2 + 1 % 2) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      ((i + 1) % 2 + 1 % 2) % 2
Tactic:
cases h : (i+1)%2
Proof state after:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
⊢ (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.zero + 1 % 2) % 2

case hg.mk.intro.refl.refl.succ
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ (match (drop (i + i / 2) σ, Nat.succ n✝) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.succ n✝) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.succ n✝ + 1 % 2) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
⊢ (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.zero + 1 % 2) % 2
Tactic:
have hdvd : 2 ∣ i+1 := Nat.dvd_of_mod_eq_zero h
Proof state after:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
⊢ (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.zero + 1 % 2) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
⊢ (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.zero + 1 % 2) % 2
Tactic:
simp [tail, drop, nth, Nat.succ_div_of_dvd hdvd]
Proof state after:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
⊢ (fun i_1 => σ (i_1 + 1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i / 2 + 1)))
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
⊢ (fun i_1 => σ (i_1 + 1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i / 2 + 1)))
Tactic:
funext j
Proof state after:
case hg.mk.intro.refl.refl.zero.h
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
j : ℕ
⊢ σ (j + 1 + 1 + (i + i / 2)) = σ (j + (i + 1 + (i / 2 + 1)))
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.zero.h
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
j : ℕ
⊢ σ (j + 1 + 1 + (i + i / 2)) = σ (j + (i + 1 + (i / 2 + 1)))
Tactic:
congr 1
Proof state after:
case hg.mk.intro.refl.refl.zero.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
j : ℕ
⊢ j + 1 + 1 + (i + i / 2) = j + (i + 1 + (i / 2 + 1))
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.zero.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
j : ℕ
⊢ j + 1 + 1 + (i + i / 2) = j + (i + 1 + (i / 2 + 1))
Tactic:
ring
Proof state after:
no goals
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ (match (drop (i + i / 2) σ, Nat.succ n✝) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.succ n✝) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.succ n✝ + 1 % 2) % 2
Tactic:
simp [tail, drop, nth]
Proof state after:
case hg.mk.intro.refl.refl.succ
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ ((fun i_1 => σ (i_1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i + 1) / 2))) ∧ n✝ = (Nat.succ n✝ + 1) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ ((fun i_1 => σ (i_1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i + 1) / 2))) ∧ n✝ = (Nat.succ n✝ + 1) % 2
Tactic:
constructor
Proof state after:
case hg.mk.intro.refl.refl.succ.left
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ (fun i_1 => σ (i_1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i + 1) / 2))

case hg.mk.intro.refl.refl.succ.right
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ.left
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ (fun i_1 => σ (i_1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i + 1) / 2))
Tactic:
funext j
Proof state after:
case hg.mk.intro.refl.refl.succ.left.h
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ σ (j + 1 + (i + i / 2)) = σ (j + (i + 1 + (i + 1) / 2))
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ.left.h
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ σ (j + 1 + (i + i / 2)) = σ (j + (i + 1 + (i + 1) / 2))
Tactic:
congr 1
Proof state after:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ j + 1 + (i + i / 2) = j + (i + 1 + (i + 1) / 2)
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ j + 1 + (i + i / 2) = j + (i + 1 + (i + 1) / 2)
Tactic:
have hdvd : ¬2 ∣ i+1 := by
  apply Nat.not_dvd_of_mod_neq_zero 
  intro h'
  rw [h] at h'
  contradiction
Proof state after:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
hdvd : ¬2 ∣ i + 1
⊢ j + 1 + (i + i / 2) = j + (i + 1 + (i + 1) / 2)
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
hdvd : ¬2 ∣ i + 1
⊢ j + 1 + (i + i / 2) = j + (i + 1 + (i + 1) / 2)
Tactic:
rw [Nat.succ_div_of_not_dvd hdvd]
Proof state after:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
hdvd : ¬2 ∣ i + 1
⊢ j + 1 + (i + i / 2) = j + (i + 1 + i / 2)
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
hdvd : ¬2 ∣ i + 1
⊢ j + 1 + (i + i / 2) = j + (i + 1 + i / 2)
Tactic:
ring
Proof state after:
no goals
Theorem: dropEveryNth_three_eq_fun
Proof state before:
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ ¬2 ∣ i + 1
Tactic:
apply Nat.not_dvd_of_mod_neq_zero
Proof state after:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ (i + 1) % 2 ≠ 0
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ (i + 1) % 2 ≠ 0
Tactic:
intro h'
Proof state after:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
h' : (i + 1) % 2 = 0
⊢ False
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
h' : (i + 1) % 2 = 0
⊢ False
Tactic:
rw [h] at h'
Proof state after:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
h' : Nat.succ n✝ = 0
⊢ False
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
h' : Nat.succ n✝ = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ.right
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Tactic:
cases' Nat.mod_two_eq_zero_or_one (i + 1) with h' h'
<;> rw [h'] at h
Proof state after:
case hg.mk.intro.refl.refl.succ.right.inl
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : 0 = Nat.succ n✝
h' : (i + 1) % 2 = 0
⊢ n✝ = (Nat.succ n✝ + 1) % 2

case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : 1 = Nat.succ n✝
h' : (i + 1) % 2 = 1
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ.right.inl
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : 0 = Nat.succ n✝
h' : (i + 1) % 2 = 0
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Tactic:
contradiction
Proof state after:
no goals
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : 1 = Nat.succ n✝
h' : (i + 1) % 2 = 1
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Tactic:
simp at h
Proof state after:
case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h' : (i + 1) % 2 = 1
h : 0 = n✝
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h' : (i + 1) % 2 = 1
h : 0 = n✝
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Tactic:
rw[←h]
Proof state after:
case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h' : (i + 1) % 2 = 1
h : 0 = n✝
⊢ 0 = (Nat.succ 0 + 1) % 2
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h' : (i + 1) % 2 = 1
h : 0 = n✝
⊢ 0 = (Nat.succ 0 + 1) % 2
Tactic:
rfl
Proof state after:
no goals
Theorem: dropEveryNth_three_eq_fun
Proof state before:
case a
α✝ : Type u_1
σ : Stream' α✝
⊢ match (σ, 3 - 2) with
  | (σ', c) => σ' = drop (0 + 0 / 2) σ ∧ c = (0 + 1) % 2
Tactic:
exact ⟨rfl, rfl⟩
Proof state after:
no goals
Theorem: dropEveryNth_eq_fun
Proof state before:
n : ℕ
α✝ : Type u_1
σ : Stream' α✝
⊢ dropEveryNth (n + 1) σ = fun i => σ (i + i / n)
Tactic:
rw [dropEveryNth, fun_to_corec fun i => σ (i + i/n)]
Proof state after:
n : ℕ
α✝ : Type u_1
σ : Stream' α✝
⊢ corec
      (fun x =>
        match x with
        | (σ, snd) => head σ)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), n + 1 - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, n + 1 - 2) =
    corec (fun i => σ (i + i / n)) (fun x => x + 1) 0
Theorem: Nat.mul_div
Proof state before:
a b : ℕ
hb : 0 < b
⊢ a * b / b = a
Tactic:
have hb' : b ≠ 0 := by 
  rintro ⟨⟩; contradiction
Proof state after:
a b : ℕ
hb : 0 < b
hb' : b ≠ 0
⊢ a * b / b = a
Theorem: Nat.mul_div
Proof state before:
a b : ℕ
hb : 0 < b
hb' : b ≠ 0
⊢ a * b / b = a
Tactic:
induction a generalizing b
<;> simp [Nat.succ_mul, Nat.add_div hb, hb', *]
Proof state after:
no goals
Theorem: Nat.mul_div
Proof state before:
a b : ℕ
hb : 0 < b
⊢ b ≠ 0
Tactic:
rintro ⟨⟩
Proof state after:
case refl
a : ℕ
hb : 0 < 0
⊢ False
Theorem: Nat.mul_div
Proof state before:
case refl
a : ℕ
hb : 0 < 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: sum_eq_three_even
Proof state before:
j : ℕ
⊢ sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j ^ 2 + j) + 1
Tactic:
simp [pow_two]
Proof state after:
j : ℕ
⊢ sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
Theorem: sum_eq_three_even
Proof state before:
j : ℕ
⊢ sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
Tactic:
induction' j with j ih
Proof state after:
case zero

⊢ sum (fun i => i + i / 2 + 1) (Nat.zero + Nat.zero) = 3 * (Nat.zero * Nat.zero + Nat.zero) + 1

case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
⊢ sum (fun i => i + i / 2 + 1) (Nat.succ j + Nat.succ j) = 3 * (Nat.succ j * Nat.succ j + Nat.succ j) + 1