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

State before:
n : ℕ
i j : Fin n
⊢ Arith₁ fun v => (v.get i).pair (v.get j)
Tactic:
have := if_pos (lt i j)
  ((add 0 1).comp₂ _ (mul j j) (proj i))
  ((add 0 1).comp₂ _ ((add 0 1).comp₂ _ (mul i i) (proj i)) (proj j))
State after:
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
⊢ Arith₁ fun v => (v.get i).pair (v.get j)

State before:
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
⊢ Arith₁ fun v => (v.get i).pair (v.get j)
Tactic:
exact this.of_eq <| by
  intro v; simp[pair]
State after:
no goals

State before:
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
⊢ ∀ (i_1 : Vector ℕ n),
    (if 0 < (i_1.get i).isLtNat (i_1.get j) then i_1.get j * i_1.get j + i_1.get i
      else i_1.get i * i_1.get i + i_1.get i + i_1.get j) =
      (i_1.get i).pair (i_1.get j)
Tactic:
intro v
State after:
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
v : Vector ℕ n
⊢ (if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j) =
    (v.get i).pair (v.get j)

State before:
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
v : Vector ℕ n
⊢ (if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j) =
    (v.get i).pair (v.get j)
Tactic:
simp[pair]
State after:
no goals