Theorem: Nat.Arith₁.sqrt (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
i : Fin n
⊢ Arith₁ fun v => (v.get i).sqrt
Tactic:
have := ArithPart₁.implicit_fun i (fun _ x => x * x) ((mul 0 1).comp₂ _ head head)
State after:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
⊢ Arith₁ fun v => (v.get i).sqrt

State before:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
⊢ ∀ (i_1 : Vector ℕ n),
    (rfind fun x =>
        Part.some (decide ((fun x x => x * x) i_1 x ≤ i_1.get i ∧ i_1.get i < (fun x x => x * x) i_1 (x + 1)))) =
      (↑fun v => (v.get i).sqrt) i_1
Tactic:
intro v
State after:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))) =
    (↑fun v => (v.get i).sqrt) v

State before:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))) =
    (↑fun v => (v.get i).sqrt) v
Tactic:
simp only [Bool.decide_and, PFun.coe_val, eq_some_iff, mem_rfind, mem_some_iff]
State after:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ true =
      (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
        decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1))) ∧
    ∀ {m : ℕ}, m < (v.get i).sqrt → false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))

State before:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ true =
      (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
        decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1))) ∧
    ∀ {m : ℕ}, m < (v.get i).sqrt → false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))
Tactic:
constructor
State after:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ true =
    (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
      decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)))

case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ ∀ {m : ℕ}, m < (v.get i).sqrt → false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))

State before:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ true =
    (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
      decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)))
Tactic:
symm
State after:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
      decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1))) =
    true

State before:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
      decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1))) =
    true
Tactic:
simp
State after:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (v.get i).sqrt * (v.get i).sqrt ≤ v.get i ∧ v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)

State before:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (v.get i).sqrt * (v.get i).sqrt ≤ v.get i ∧ v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)
Tactic:
constructor
State after:
case left.left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (v.get i).sqrt * (v.get i).sqrt ≤ v.get i

case left.right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)

State before:
case left.left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (v.get i).sqrt * (v.get i).sqrt ≤ v.get i
Tactic:
exact sqrt_le (Vector.get v i)
State after:
no goals

State before:
case left.right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)
Tactic:
exact lt_succ_sqrt (Vector.get v i)
State after:
no goals

State before:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ ∀ {m : ℕ}, m < (v.get i).sqrt → false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))
Tactic:
intro m hm
State after:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))

State before:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))
Tactic:
symm
State after:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1))) = false

State before:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1))) = false
Tactic:
simp only [Bool.and_eq_false_eq_eq_false_or_eq_false, decide_eq_false_iff_not, not_le, not_lt]
State after:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ v.get i < m * m ∨ (m + 1) * (m + 1) ≤ v.get i

State before:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ v.get i < m * m ∨ (m + 1) * (m + 1) ≤ v.get i
Tactic:
right
State after:
case right.h
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ (m + 1) * (m + 1) ≤ v.get i

State before:
case right.h
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ (m + 1) * (m + 1) ≤ v.get i
Tactic:
exact Iff.mp le_sqrt hm
State after:
no goals