internlm/Lean-Github huggingface dataset:
Theorem: Nat.ball_pos_iff
Proof state before:
case intro.inr
p : ℕ → ℕ
m : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) m ↔ ∀ m_1 < m, 0 < p m_1
hn : 0 < p m
hp : ∀ m_1 < m, 0 < p m_1
hm : m ≤ m
⊢ 0 < p m
Tactic:
exact hn
Proof state after:
no goals
Theorem: Nat.ball_pos_iff
Proof state before:
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ (∀ m ≤ n, 0 < p m) → 0 < p n ∧ ∀ m < n, 0 < p m
Tactic:
intro h
Proof state after:
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
h : ∀ m ≤ n, 0 < p m
⊢ 0 < p n ∧ ∀ m < n, 0 < p m
Theorem: Nat.ball_pos_iff
Proof state before:
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
h : ∀ m ≤ n, 0 < p m
⊢ 0 < p n ∧ ∀ m < n, 0 < p m
Tactic:
exact ⟨h n (Nat.le_refl n), fun m hm => h m (le_of_lt hm)⟩
Proof state after:
no goals
Theorem: Nat.ball_eq_zero_iff
Proof state before:
p : ℕ → ℕ
n : ℕ
⊢ n.ball p = 0 ↔ ∃ m < n, p m = 0
Tactic:
simpa[-ball_pos_iff] using not_iff_not.mpr (ball_pos_iff (p := p) (n := n))
Proof state after:
no goals
Theorem: Nat.ball_pos_iff_eq_one
Proof state before:
p : ℕ → ℕ
n : ℕ
⊢ n.ball p = 1 ↔ 0 < n.ball p
Tactic:
induction' n with n _ <;> simp[ball, Nat.lt_succ_iff] at*
Proof state after:
case succ
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1 ↔ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
Theorem: Nat.ball_pos_iff_eq_one
Proof state before:
case succ
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1 ↔ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
Tactic:
constructor
Proof state after:
case succ.mp
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1 → 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n

case succ.mpr
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n → (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1
Theorem: Nat.ball_pos_iff_eq_one
Proof state before:
case succ.mp
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1 → 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
Tactic:
intro h
Proof state after:
case succ.mp
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
h : (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
Theorem: Nat.ball_pos_iff_eq_one
Proof state before:
case succ.mp
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
h : (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
Tactic:
simpa using pos_of_eq_one h
Proof state after:
no goals
Theorem: Nat.ball_pos_iff_eq_one
Proof state before:
case succ.mpr
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n → (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1
Tactic:
intro h
Proof state after:
case succ.mpr
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
h : 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1
Theorem: Nat.ball_pos_iff_eq_one
Proof state before:
case succ.mpr
p : ℕ → ℕ
n : ℕ
a✝ : rec 1 (fun n ih => (p n).pos.and ih) n = 1 ↔ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
h : 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n
⊢ (p n).pos.and (rec 1 (fun n ih => (p n).pos.and ih) n) = 1
Tactic:
simpa[and_eq_one] using h
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n : ℕ
f : Vector ℕ n →. ℕ
hf : ArithPart₁ f
⊢ Partrec' f
Tactic:
induction hf
Proof state after:
case zero
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 0

case one
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 1

case add
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => v.get i✝ + v.get j✝

case mul
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => v.get i✝ * v.get j✝

case proj
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ : Fin n✝
⊢ Partrec' ↑fun v => v.get i✝

case equal
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => (v.get i✝).isEqNat (v.get j✝)

case lt
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => (v.get i✝).isLtNat (v.get j✝)

case comp
n : ℕ
f : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
g✝ : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : ArithPart₁ f✝
a✝ : ∀ (i : Fin n✝), ArithPart₁ (g✝ i)
a_ih✝¹ : Partrec' f✝
a_ih✝ : ∀ (i : Fin n✝), Partrec' (g✝ i)
⊢ Partrec' fun v => (mOfFn fun i => g✝ i v) >>= f✝

case rfind
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ (n✝ + 1) → ℕ
a✝ : ArithPart₁ ↑f✝
a_ih✝ : Partrec' ↑f✝
⊢ Partrec' fun v => Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 0
Tactic:
case zero => exact Partrec'.of_part (Partrec.const' 0)
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 1
Tactic:
case one  => exact Partrec'.of_part (Partrec.const' 1)
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => v.get i + v.get j
Tactic:
case add n i j =>
  exact (Partrec'.of_part ((Primrec.nat_add.comp
    (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
    (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j))).to_comp.partrec))
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => v.get i * v.get j
Tactic:
case mul n i j =>
  exact (Partrec'.of_part ((Primrec.nat_mul.comp
    (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
    (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j))).to_comp.partrec))
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i : Fin n
⊢ Partrec' ↑fun v => v.get i
Tactic:
case proj n i =>
  exact Partrec'.of_part
    (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i)).to_comp.partrec
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)
Tactic:
case equal n i j =>
  have : Primrec (fun (v : Vector ℕ n) => if v.get i = v.get j then 1 else 0) :=
    Primrec.ite
      (Primrec.eq.comp
        (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
        (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j)))
      (_root_.Primrec.const 1)
      (_root_.Primrec.const 0)
  exact Partrec'.of_part this.to_comp.partrec
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => (v.get i).isLtNat (v.get j)
Tactic:
case lt n i j =>
  have : Primrec (fun (v : Vector ℕ n) => if v.get i < v.get j then 1 else 0) :=
    Primrec.ite
      (Primrec.nat_lt.comp
        (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
        (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j)))
      (_root_.Primrec.const 1)
      (_root_.Primrec.const 0)
  exact Partrec'.of_part this.to_comp.partrec
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
a✝¹ : ArithPart₁ f
a✝ : ∀ (i : Fin n), ArithPart₁ (g i)
hf : Partrec' f
hg : ∀ (i : Fin n), Partrec' (g i)
⊢ Partrec' fun v => (mOfFn fun i => g i v) >>= f
Tactic:
case comp m n f g _ _ hf hg =>
  exact Partrec'.comp g hf hg
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : ArithPart₁ ↑f
hf : Partrec' ↑f
⊢ Partrec' fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
case rfind f _ hf =>
  exact Partrec'.rfind hf
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 0
Tactic:
exact Partrec'.of_part (Partrec.const' 0)
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 1
Tactic:
exact Partrec'.of_part (Partrec.const' 1)
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => v.get i + v.get j
Tactic:
exact (Partrec'.of_part ((Primrec.nat_add.comp
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j))).to_comp.partrec))
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => v.get i * v.get j
Tactic:
exact (Partrec'.of_part ((Primrec.nat_mul.comp
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j))).to_comp.partrec))
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i : Fin n
⊢ Partrec' ↑fun v => v.get i
Tactic:
exact Partrec'.of_part
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i)).to_comp.partrec
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)
Tactic:
have : Primrec (fun (v : Vector ℕ n) => if v.get i = v.get j then 1 else 0) :=
  Primrec.ite
    (Primrec.eq.comp
      (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
      (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j)))
    (_root_.Primrec.const 1)
    (_root_.Primrec.const 0)
Proof state after:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
this : Primrec fun v => if v.get i = v.get j then 1 else 0
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
this : Primrec fun v => if v.get i = v.get j then 1 else 0
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)
Tactic:
exact Partrec'.of_part this.to_comp.partrec
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => (v.get i).isLtNat (v.get j)
Tactic:
have : Primrec (fun (v : Vector ℕ n) => if v.get i < v.get j then 1 else 0) :=
  Primrec.ite
    (Primrec.nat_lt.comp
      (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
      (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j)))
    (_root_.Primrec.const 1)
    (_root_.Primrec.const 0)
Proof state after:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
this : Primrec fun v => if v.get i < v.get j then 1 else 0
⊢ Partrec' ↑fun v => (v.get i).isLtNat (v.get j)
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
this : Primrec fun v => if v.get i < v.get j then 1 else 0
⊢ Partrec' ↑fun v => (v.get i).isLtNat (v.get j)
Tactic:
exact Partrec'.of_part this.to_comp.partrec
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
a✝¹ : ArithPart₁ f
a✝ : ∀ (i : Fin n), ArithPart₁ (g i)
hf : Partrec' f
hg : ∀ (i : Fin n), Partrec' (g i)
⊢ Partrec' fun v => (mOfFn fun i => g i v) >>= f
Tactic:
exact Partrec'.comp g hf hg
Proof state after:
no goals
Theorem: Nat.ArithPart₁.to_partrec'
Proof state before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : ArithPart₁ ↑f
hf : Partrec' ↑f
⊢ Partrec' fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
exact Partrec'.rfind hf
Proof state after:
no goals
Theorem: Nat.ArithPart₁.bind
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
i : Fin n.succ
⊢ ArithPart₁ ((g :> fun i v => ↑(Option.some (v.get i))) i)
Tactic:
cases i using Fin.cases <;> simp[*]
Proof state after:
case succ
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
i✝ : Fin n
⊢ ArithPart₁ fun v => Part.some (v.get i✝)
Theorem: Nat.ArithPart₁.bind
Proof state before:
case succ
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
i✝ : Fin n
⊢ ArithPart₁ fun v => Part.some (v.get i✝)
Tactic:
exact proj _
Proof state after:
no goals
Theorem: Nat.ArithPart₁.bind
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
⊢ ∀ (i : Vector ℕ n),
    (do
        let v ← mOfFn fun i_1 => (g :> fun i v => ↑(Option.some (v.get i))) i_1 i
        f v.tail v.head) =
      (g i).bind (f i)
Tactic:
intro v
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ (do
      let v ← mOfFn fun i => (g :> fun i v => ↑(Option.some (v.get i))) i v
      f v.tail v.head) =
    (g v).bind (f v)
Theorem: Nat.ArithPart₁.bind
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ (do
      let v ← mOfFn fun i => (g :> fun i v => ↑(Option.some (v.get i))) i v
      f v.tail v.head) =
    (g v).bind (f v)
Tactic:
simp
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)
Theorem: Nat.ArithPart₁.bind
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)
Tactic:
rcases Part.eq_none_or_eq_some (g v) with (hgv | ⟨x, hgv⟩)
Proof state after:
case inl
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
hgv : g v = Part.none
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)

case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)
Theorem: Nat.ArithPart₁.bind
Proof state before:
case inl
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
hgv : g v = Part.none
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)
Tactic:
simp[hgv, mOfFn]
Proof state after:
no goals
Theorem: Nat.ArithPart₁.bind
Proof state before:
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)
Tactic:
simp[hgv, Matrix.comp_vecCons']
Proof state after:
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = f v x
Theorem: Nat.ArithPart₁.bind
Proof state before:
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = f v x
Tactic:
have : mOfFn (fun i => (g :> fun j v => Part.some $ v.get j) i v) = pure (Vector.ofFn (x :> fun j => v.get j)) := by
  rw[←Vector.mOfFn_pure]; apply congr_arg
  funext i; cases i using Fin.cases <;> simp[hgv]
Proof state after:
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
this : (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = pure (ofFn (x :> fun j => v.get j))
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = f v x
Theorem: Nat.ArithPart₁.bind
Proof state before:
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
this : (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = pure (ofFn (x :> fun j => v.get j))
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = f v x
Tactic:
simp[this]
Proof state after:
no goals
Theorem: Nat.ArithPart₁.bind
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = pure (ofFn (x :> fun j => v.get j))
Tactic:
rw[←Vector.mOfFn_pure]
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = mOfFn fun i => pure ((x :> fun j => v.get j) i)
Theorem: Nat.ArithPart₁.bind
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = mOfFn fun i => pure ((x :> fun j => v.get j) i)
Tactic:
apply congr_arg
Proof state after:
case h
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ (fun i => (g :> fun j v => Part.some (v.get j)) i v) = fun i => pure ((x :> fun j => v.get j) i)
Theorem: Nat.ArithPart₁.bind
Proof state before:
case h
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ (fun i => (g :> fun j v => Part.some (v.get j)) i v) = fun i => pure ((x :> fun j => v.get j) i)
Tactic:
funext i
Proof state after:
case h.h
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
i : Fin n.succ
⊢ (g :> fun j v => Part.some (v.get j)) i v = pure ((x :> fun j => v.get j) i)
Theorem: Nat.ArithPart₁.bind
Proof state before:
case h.h
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
i : Fin n.succ
⊢ (g :> fun j v => Part.some (v.get j)) i v = pure ((x :> fun j => v.get j) i)
Tactic:
cases i using Fin.cases <;> simp[hgv]
Proof state after:
no goals
Theorem: Nat.ArithPart₁.map
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
⊢ ∀ (i : Vector ℕ (n + 1)), (↑fun v => f v.tail v.head) i = (fun x x_1 => Part.some (f x x_1)) i.tail i.head
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.ArithPart₁.map
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
⊢ ∀ (i : Vector ℕ n), ((g i).bind fun x => Part.some (f i x)) = Part.map (f i) (g i)
Tactic:
intro v
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ ((g v).bind fun x => Part.some (f v x)) = Part.map (f v) (g v)
Theorem: Nat.ArithPart₁.map
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ ((g v).bind fun x => Part.some (f v x)) = Part.map (f v) (g v)
Tactic:
rcases Part.eq_none_or_eq_some (g v) with (_ | ⟨x, _⟩) <;> simp[*]
Proof state after:
no goals
Theorem: Nat.ArithPart₁.comp₁
Proof state before:
f : ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0)
n : ℕ
g : Vector ℕ n → ℕ
hg : Arith₁ g
⊢ ∀ (i : Vector ℕ n),
    (do
        let v ← mOfFn fun i_1 => ↑g i
        f (v.get 0)) =
      f (g i)
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.ArithPart₁.comp₂
Proof state before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i✝ : Fin (succ 0).succ
i : Fin 1
⊢ ArithPart₁ (![↑g, ↑h] i.succ)
Tactic:
simpa using hh
Proof state after:
no goals
Theorem: Nat.ArithPart₁.comp₂
Proof state before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
⊢ ∀ (i : Vector ℕ n),
    (do
        let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
        f (v.get 0) (v.get 1)) =
      f (g i) (h i)
Tactic:
intro i
Proof state after:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ (do
      let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
      f (v.get 0) (v.get 1)) =
    f (g i) (h i)
Theorem: Nat.ArithPart₁.comp₂
Proof state before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ (do
      let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
      f (v.get 0) (v.get 1)) =
    f (g i) (h i)
Tactic:
have : (fun j => (![↑g, h] : Fin 2 → Vector ℕ n →. ℕ) j i) = (fun j => pure (![g i, h i] j)) := by
  funext j; cases j using Fin.cases <;> simp[Fin.eq_zero]
Proof state after:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
this : (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
⊢ (do
      let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
      f (v.get 0) (v.get 1)) =
    f (g i) (h i)
Theorem: Nat.ArithPart₁.comp₂
Proof state before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
this : (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
⊢ (do
      let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
      f (v.get 0) (v.get 1)) =
    f (g i) (h i)
Tactic:
simp[Matrix.comp_vecCons']
Proof state after:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
this : (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
⊢ ((mOfFn fun i_1 => ![↑g, ↑h] i_1 i).bind fun v => f v.head (v.get 1)) = f (g i) (h i)
Theorem: Nat.ArithPart₁.comp₂
Proof state before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
this : (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
⊢ ((mOfFn fun i_1 => ![↑g, ↑h] i_1 i).bind fun v => f v.head (v.get 1)) = f (g i) (h i)
Tactic:
simp[this]
Proof state after:
no goals