Theorem: Nat.split_eq (GMLInit/Data/Nat/Coding/Prod.lean)

State before:
case zero

⊢ (split 0).fst.tri + ↑(split 0).snd = 0
Tactic:
rfl
State after:
no goals

State before:
case succ
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (n + 1).split.fst.tri + ↑(n + 1).split.snd = n + 1
Tactic:
symmetry
State after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n + 1 = (n + 1).split.fst.tri + ↑(n + 1).split.snd

State before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n + 1 = (n + 1).split.fst.tri + ↑(n + 1).split.snd
Tactic:
transitivity (tri (split n).fst + ((split n).snd + 1))
State after:
case left
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n + 1 = n.split.fst.tri + (↑n.split.snd + 1)

case right
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n.split.fst.tri + (↑n.split.snd + 1) = (n + 1).split.fst.tri + ↑(n + 1).split.snd

State before:
case left
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n + 1 = n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
rw [←Nat.add_assoc (tri (split n).fst) (split n).snd 1, H]
State after:
no goals

State before:
case right
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n.split.fst.tri + (↑n.split.snd + 1) = (n + 1).split.fst.tri + ↑(n + 1).split.snd
Tactic:
symmetry
State after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (n + 1).split.fst.tri + ↑(n + 1).split.snd = n.split.fst.tri + (↑n.split.snd + 1)

State before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (n + 1).split.fst.tri + ↑(n + 1).split.snd = n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
simp only [split]
State after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)

State before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
split
State after:
case isTrue
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)

case isFalse
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)

State before:
case isTrue
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)

case isFalse
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
next h =>
  dsimp only [Nat.add_eq] at h ⊢
  rw [dif_pos h]
State after:
case isFalse
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)

State before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h : ↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
dsimp only [Nat.add_eq] at h ⊢
State after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h : ↑n.split.2 < n.split.fst
⊢ n.split.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)

State before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h : ↑n.split.2 < n.split.fst
⊢ n.split.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
rw [dif_pos h]
State after:
no goals

State before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h : ¬↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
have h : ¬((split n).snd.val < (split n).fst) := h
State after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)

State before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
heq : ↑n.split.snd = n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
rw [dif_neg h, ←Nat.add_assoc, heq]
State after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
heq : ↑n.split.snd = n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri + ↑⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.snd = n.split.fst.tri + n.split.fst + 1

State before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
heq : ↑n.split.snd = n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri + ↑⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.snd = n.split.fst.tri + n.split.fst + 1
Tactic:
rfl
State after:
no goals

State before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ ↑n.split.snd = n.split.fst
Tactic:
apply Nat.le_antisymm
State after:
case h₁
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ ↑n.split.snd ≤ n.split.fst

case h₂
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ n.split.fst ≤ ↑n.split.snd

State before:
case h₁
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ ↑n.split.snd ≤ n.split.fst
Tactic:
exact Nat.le_of_lt_succ (split n).snd.isLt
State after:
no goals

State before:
case h₂
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ n.split.fst ≤ ↑n.split.snd
Tactic:
exact Nat.le_of_not_gt h
State after:
no goals