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

State before:
n : ℕ
i : Fin n
⊢ Arith₁ fun v => (v.get i).unpair.2
Tactic:
have hf : Arith₁ (fun v => isLtNat (v.get i - (v.get i).sqrt * (v.get i).sqrt) (v.get i).sqrt) :=
  (lt 0 1).comp₂ _
    ((Arith₁.sub 0 1).comp₂ _ (proj i) ((mul 0 1).comp₂ _ (Arith₁.sqrt i) (Arith₁.sqrt i)))
    (Arith₁.sqrt i)
State after:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2

State before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2
Tactic:
have hg : Arith₁ (fun v => sqrt (v.get i)) := Arith₁.sqrt i
State after:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2

State before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2
Tactic:
have hh : Arith₁ (fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt) :=
  (sub 0 1).comp₂ _ ((sub 0 1).comp₂ _ (proj i) ((mul 0 1).comp₂ _ (Arith₁.sqrt i) (Arith₁.sqrt i))) (Arith₁.sqrt i)
State after:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2

State before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2
Tactic:
have := if_pos hf hg hh
State after:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2

State before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2
Tactic:
exact this.of_eq <| by
  intro v; simp[unpair]
  by_cases v.get i - (v.get i).sqrt * (v.get i).sqrt < sqrt (v.get i) <;> simp[*]
State after:
no goals

State before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
⊢ ∀ (i_1 : Vector ℕ n),
    (if 0 < (i_1.get i - (i_1.get i).sqrt * (i_1.get i).sqrt).isLtNat (i_1.get i).sqrt then (i_1.get i).sqrt
      else i_1.get i - (i_1.get i).sqrt * (i_1.get i).sqrt - (i_1.get i).sqrt) =
      (i_1.get i).unpair.2
Tactic:
intro v
State after:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
v : Vector ℕ n
⊢ (if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt) =
    (v.get i).unpair.2

State before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
v : Vector ℕ n
⊢ (if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt) =
    (v.get i).unpair.2
Tactic:
simp[unpair]
State after:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
v : Vector ℕ n
⊢ (if v.get i - (v.get i).sqrt * (v.get i).sqrt < (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt) =
    (if v.get i - (v.get i).sqrt * (v.get i).sqrt < (v.get i).sqrt then
        (v.get i - (v.get i).sqrt * (v.get i).sqrt, (v.get i).sqrt)
      else ((v.get i).sqrt, v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt)).2

State before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
v : Vector ℕ n
⊢ (if v.get i - (v.get i).sqrt * (v.get i).sqrt < (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt) =
    (if v.get i - (v.get i).sqrt * (v.get i).sqrt < (v.get i).sqrt then
        (v.get i - (v.get i).sqrt * (v.get i).sqrt, (v.get i).sqrt)
      else ((v.get i).sqrt, v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt)).2
Tactic:
by_cases v.get i - (v.get i).sqrt * (v.get i).sqrt < sqrt (v.get i) <;> simp[*]
State after:
no goals