Theorem: Permutation.inversionNum_eq_card_inversion (Fifteen/Data/Permutation/Inversion.lean)

State before:
n : Nat
x : Permutation n
⊢ inversionNum x = BishopFin.card (Inversion x)
Tactic:
rewrite [← inversions_size_eq_card]
State after:
n : Nat
x : Permutation n
⊢ inversionNum x = Array.size (inversions x)

State before:
n : Nat
x : Permutation n
⊢ inversionNum x = Array.size (inversions x)
Tactic:
dsimp [inversionNum, inversions]
State after:
n : Nat
x : Permutation n
⊢ Nat.fold' n (fun j => Nat.fold' ↑j fun i k => if x[↑i] > x[↑j] then k + 1 else k) 0 =
    Array.size
      (Nat.fold' n
        (fun j =>
          Nat.fold' ↑j fun i ivs =>
            if h : x[↑i] > x[↑j] then
              Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
            else ivs)
        #[])

State before:
n : Nat
x : Permutation n
⊢ Nat.fold' n (fun j => Nat.fold' ↑j fun i k => if x[↑i] > x[↑j] then k + 1 else k) 0 =
    Array.size
      (Nat.fold' n
        (fun j =>
          Nat.fold' ↑j fun i ivs =>
            if h : x[↑i] > x[↑j] then
              Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
            else ivs)
        #[])
Tactic:
conv => lhs; pattern 0; change (#[] : Array x.Inversion).size
State after:
n : Nat
x : Permutation n
⊢ Nat.fold' n (fun j => Nat.fold' ↑j fun i k => if x[↑i] > x[↑j] then k + 1 else k) (Array.size #[]) =
    Array.size
      (Nat.fold' n
        (fun j =>
          Nat.fold' ↑j fun i ivs =>
            if h : x[↑i] > x[↑j] then
              Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
            else ivs)
        #[])

State before:
n : Nat
x : Permutation n
⊢ Nat.fold' n (fun j => Nat.fold' ↑j fun i k => if x[↑i] > x[↑j] then k + 1 else k) (Array.size #[]) =
    Array.size
      (Nat.fold' n
        (fun j =>
          Nat.fold' ↑j fun i ivs =>
            if h : x[↑i] > x[↑j] then
              Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
            else ivs)
        #[])
Tactic:
apply Nat.fold'_hom
State after:
case H
n : Nat
x : Permutation n
⊢ ∀ (i : Fin n) (a : Array (Inversion x)),
    Nat.fold' (↑i) (fun i_1 k => if x[↑i_1] > x[↑i] then k + 1 else k) (Array.size a) =
      Array.size
        (Nat.fold' (↑i)
          (fun i_1 ivs =>
            if h : x[↑i_1] > x[↑i] then
              Array.push ivs { fst := Fin.castLE (_ : ↑i ≤ n) i_1, snd := i, lt := (_ : ↑i_1 < ↑i), inverted := h }
            else ivs)
          a)

State before:
case H
n : Nat
x : Permutation n
⊢ ∀ (i : Fin n) (a : Array (Inversion x)),
    Nat.fold' (↑i) (fun i_1 k => if x[↑i_1] > x[↑i] then k + 1 else k) (Array.size a) =
      Array.size
        (Nat.fold' (↑i)
          (fun i_1 ivs =>
            if h : x[↑i_1] > x[↑i] then
              Array.push ivs { fst := Fin.castLE (_ : ↑i ≤ n) i_1, snd := i, lt := (_ : ↑i_1 < ↑i), inverted := h }
            else ivs)
          a)
Tactic:
intro j _
State after:
case H
n : Nat
x : Permutation n
j : Fin n
a✝ : Array (Inversion x)
⊢ Nat.fold' (↑j) (fun i k => if x[↑i] > x[↑j] then k + 1 else k) (Array.size a✝) =
    Array.size
      (Nat.fold' (↑j)
        (fun i ivs =>
          if h : x[↑i] > x[↑j] then
            Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
          else ivs)
        a✝)

State before:
case H
n : Nat
x : Permutation n
j : Fin n
a✝ : Array (Inversion x)
⊢ Nat.fold' (↑j) (fun i k => if x[↑i] > x[↑j] then k + 1 else k) (Array.size a✝) =
    Array.size
      (Nat.fold' (↑j)
        (fun i ivs =>
          if h : x[↑i] > x[↑j] then
            Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
          else ivs)
        a✝)
Tactic:
apply Nat.fold'_hom
State after:
case H.H
n : Nat
x : Permutation n
j : Fin n
a✝ : Array (Inversion x)
⊢ ∀ (i : Fin ↑j) (a : Array (Inversion x)),
    (if x[↑i] > x[↑j] then Array.size a + 1 else Array.size a) =
      Array.size
        (if h : x[↑i] > x[↑j] then
          Array.push a { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
        else a)

State before:
case H.H
n : Nat
x : Permutation n
j : Fin n
a✝ : Array (Inversion x)
⊢ ∀ (i : Fin ↑j) (a : Array (Inversion x)),
    (if x[↑i] > x[↑j] then Array.size a + 1 else Array.size a) =
      Array.size
        (if h : x[↑i] > x[↑j] then
          Array.push a { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
        else a)
Tactic:
intro i ivs'
State after:
case H.H
n : Nat
x : Permutation n
j : Fin n
a✝ : Array (Inversion x)
i : Fin ↑j
ivs' : Array (Inversion x)
⊢ (if x[↑i] > x[↑j] then Array.size ivs' + 1 else Array.size ivs') =
    Array.size
      (if h : x[↑i] > x[↑j] then
        Array.push ivs' { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
      else ivs')

State before:
case H.H
n : Nat
x : Permutation n
j : Fin n
a✝ : Array (Inversion x)
i : Fin ↑j
ivs' : Array (Inversion x)
⊢ (if x[↑i] > x[↑j] then Array.size ivs' + 1 else Array.size ivs') =
    Array.size
      (if h : x[↑i] > x[↑j] then
        Array.push ivs' { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
      else ivs')
Tactic:
if hx : x[i.1]'(Nat.lt_trans i.2 j.2) > x[j.1] then
  simp only [hx, if_pos, dif_pos, Array.size_push]
else
  simp only [hx, if_neg, dif_neg]
State after:
no goals

State before:
n : Nat
x : Permutation n
j : Fin n
a✝ : Array (Inversion x)
i : Fin ↑j
ivs' : Array (Inversion x)
hx : x[↑i] > x[↑j]
⊢ (if x[↑i] > x[↑j] then Array.size ivs' + 1 else Array.size ivs') =
    Array.size
      (if h : x[↑i] > x[↑j] then
        Array.push ivs' { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
      else ivs')
Tactic:
simp only [hx, if_pos, dif_pos, Array.size_push]
State after:
no goals

State before:
n : Nat
x : Permutation n
j : Fin n
a✝ : Array (Inversion x)
i : Fin ↑j
ivs' : Array (Inversion x)
hx : ¬x[↑i] > x[↑j]
⊢ (if x[↑i] > x[↑j] then Array.size ivs' + 1 else Array.size ivs') =
    Array.size
      (if h : x[↑i] > x[↑j] then
        Array.push ivs' { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
      else ivs')
Tactic:
simp only [hx, if_neg, dif_neg]
State after:
no goals