internlm/Lean-Github huggingface dataset:
Theorem: Permutation.Inversion.card_eq_of_mul
Proof state before:
case refine_1
n : Nat
x y : Permutation n
⊢ ∀ (b : Fin n × Fin n), Prod.map (toFun (inv y)) (toFun (inv y)) (Prod.map (toFun y) (toFun y) b) = b

case refine_2
n : Nat
x y : Permutation n
⊢ ∀ (a : Fin n × Fin n), Prod.map (toFun y) (toFun y) (Prod.map (toFun (inv y)) (toFun (inv y)) a) = a
Tactic:
. simp only [Prod.map, toFun_inv_toFun, implies_true]
Proof state after:
case refine_2
n : Nat
x y : Permutation n
⊢ ∀ (a : Fin n × Fin n), Prod.map (toFun y) (toFun y) (Prod.map (toFun (inv y)) (toFun (inv y)) a) = a
Theorem: Permutation.Inversion.card_eq_of_mul
Proof state before:
case refine_2
n : Nat
x y : Permutation n
⊢ ∀ (a : Fin n × Fin n), Prod.map (toFun y) (toFun y) (Prod.map (toFun (inv y)) (toFun (inv y)) a) = a
Tactic:
. simp only [Prod.map, toFun_toFun_inv, implies_true]
Proof state after:
no goals
Theorem: Permutation.Inversion.card_eq_of_mul
Proof state before:
case refine_1
n : Nat
x y : Permutation n
⊢ ∀ (b : Fin n × Fin n), Prod.map (toFun (inv y)) (toFun (inv y)) (Prod.map (toFun y) (toFun y) b) = b
Tactic:
simp only [Prod.map, toFun_inv_toFun, implies_true]
Proof state after:
no goals
Theorem: Permutation.Inversion.card_eq_of_mul
Proof state before:
case refine_2
n : Nat
x y : Permutation n
⊢ ∀ (a : Fin n × Fin n), Prod.map (toFun y) (toFun y) (Prod.map (toFun (inv y)) (toFun (inv y)) a) = a
Tactic:
simp only [Prod.map, toFun_toFun_inv, implies_true]
Proof state after:
no goals
Theorem: Permutation.inversionNum_eq_card_inversion
Proof state before:
n : Nat
x : Permutation n
⊢ inversionNum x = BishopFin.card (Inversion x)
Tactic:
rewrite [← inversions_size_eq_card]
Proof state after:
n : Nat
x : Permutation n
⊢ inversionNum x = Array.size (inversions x)
Theorem: Permutation.inversionNum_eq_card_inversion
Proof state before:
n : Nat
x : Permutation n
⊢ inversionNum x = Array.size (inversions x)
Tactic:
dsimp [inversionNum, inversions]
Proof 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)
        #[])
Theorem: Permutation.inversionNum_eq_card_inversion
Proof 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
Proof 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)
        #[])
Theorem: Permutation.inversionNum_eq_card_inversion
Proof 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
Proof 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)
Theorem: Permutation.inversionNum_eq_card_inversion
Proof 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 _
Proof 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✝)
Theorem: Permutation.inversionNum_eq_card_inversion
Proof 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
Proof 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)
Theorem: Permutation.inversionNum_eq_card_inversion
Proof 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'
Proof 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')
Theorem: Permutation.inversionNum_eq_card_inversion
Proof 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]
Proof state after:
no goals
Theorem: Permutation.inversionNum_eq_card_inversion
Proof 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]
Proof state after:
no goals
Theorem: Permutation.inversionNum_eq_card_inversion
Proof 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]
Proof state after:
no goals
Theorem: Permutation.inversionNum_add
Proof state before:
n : Nat
x y : Permutation n
⊢ inversionNum x + inversionNum y =
    inversionNum (x * y) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
simp only [inversionNum_eq_card_inversion]
Proof state after:
n : Nat
x y : Permutation n
⊢ BishopFin.card (Inversion x) + BishopFin.card (Inversion y) =
    BishopFin.card (Inversion (x * y)) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Theorem: Permutation.inversionNum_add
Proof state before:
n : Nat
x y : Permutation n
⊢ BishopFin.card (Inversion x) + BishopFin.card (Inversion y) =
    BishopFin.card (Inversion (x * y)) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
conv =>
  lhs; lhs; rw [Inversion.card_eq_of_mul x y]
  rw [BishopFin.count_split fun t => t.1.1 < t.2.1]
Proof state after:
n : Nat
x y : Permutation n
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
      BishopFin.card (Inversion y) =
    BishopFin.card (Inversion (x * y)) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Theorem: Permutation.inversionNum_add
Proof state before:
n : Nat
x y : Permutation n
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
      BishopFin.card (Inversion y) =
    BishopFin.card (Inversion (x * y)) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
conv =>
  lhs; rhs; rw [Inversion.card_eq]
  rw [BishopFin.count_split fun t => (x * y)[t.1.1].1 > (x * y)[t.2.1].1]
Proof state after:
n : Nat
x y : Permutation n
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
      ((BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.card (Inversion (x * y)) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Theorem: Permutation.inversionNum_add
Proof state before:
n : Nat
x y : Permutation n
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
      ((BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.card (Inversion (x * y)) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
have : ∀ (a b c d : Nat), (a + b) + (c + d) = (a + c) + (b + d) :=
  fun a b c d => by
    conv => lhs; rw [Nat.add_assoc, ← Nat.add_assoc b, Nat.add_comm b c, Nat.add_assoc c, ← Nat.add_assoc a]
Proof state after:
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
      ((BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.card (Inversion (x * y)) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Theorem: Permutation.inversionNum_add
Proof state before:
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
      ((BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.card (Inversion (x * y)) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
conv => lhs; rw [this]
Proof state after:
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) +
      ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.card (Inversion (x * y)) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Theorem: Permutation.inversionNum_add
Proof state before:
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) +
      ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.card (Inversion (x * y)) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
conv =>
  rhs; lhs; rw [Inversion.card_eq]
  rw [BishopFin.count_split fun t => y[t.1.1].1 < y[t.2.1].1]
Proof state after:
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) +
      ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    ((BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑y[↑a.fst] < ↑y[↑a.snd]) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Theorem: Permutation.inversionNum_add
Proof state before:
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) +
      ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    ((BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑y[↑a.fst] < ↑y[↑a.snd]) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]) +
      2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
conv =>
  rhs; rhs; rw [Nat.two_mul]
Proof state after:
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) +
      ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    ((BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑y[↑a.fst] < ↑y[↑a.snd]) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]) +
      ((BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]) +
        BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd])
Theorem: Permutation.inversionNum_add
Proof state before:
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) +
      ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    ((BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑y[↑a.fst] < ↑y[↑a.snd]) +
        BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]) +
      ((BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]) +
        BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd])
Tactic:
refine congrArg₂ HAdd.hAdd (congrArg₂ HAdd.hAdd ?_ ?_) (congrArg₂ HAdd.hAdd ?_ ?_)
Proof state after:
case refine_1
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) =
    BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑y[↑a.fst] < ↑y[↑a.snd]

case refine_2
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]

case refine_3
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

case refine_4
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Theorem: Permutation.inversionNum_add
Proof state before:
case refine_1
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) =
    BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑y[↑a.fst] < ↑y[↑a.snd]

case refine_2
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]

case refine_3
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

case refine_4
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
. apply BishopFin.count_congr; intro t
  conv => lhs; rw [and_comm]
  conv => rhs; rw [and_assoc]; rhs; rw [and_comm]
Proof state after:
case refine_2
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]

case refine_3
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

case refine_4
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]