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

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]
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]

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]
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]

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]
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]

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]
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]

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]
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]

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]
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]

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]
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])

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 ?_ ?_)
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]

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]
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]

State before:
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 =>
    rhs; rw [and_assoc]
    conv => rhs; rw [and_comm]
    rw [← and_assoc]
  refine and_congr_left' ?_
  refine and_congr_right ?_
  intro ht
  simp only [Nat.not_lt_eq, Nat.le_iff_lt_or_eq]
  apply Iff.symm; apply or_iff_left
  intro hyt
  exact Nat.lt_irrefl _ <| (y.get_inj _ _ <| Fin.eq_of_val_eq hyt) ▸ ht
State after:
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]

State before:
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:
. let swap : Fin n × Fin n → Fin n × Fin n :=
    fun t => ⟨t.2, t.1⟩
  have : ∀ t, swap (swap t) = t := fun | .mk i j => rfl
  conv =>
    lhs; rw [BishopFin.count_eq_count_invimage_of_inv swap swap this this]
  dsimp only [Function.comp]
  apply BishopFin.count_congr; intro t
  conv => lhs; rw [and_comm]
  refine and_congr_left ?_
  intro ht
  rewrite [Nat.not_lt_eq, Nat.le_iff_lt_or_eq]
  apply or_iff_left
  intro ht'; cases t; dsimp at *
  cases Fin.eq_of_val_eq ht'; exact Nat.lt_irrefl _ ht.1
State after:
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]

State before:
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
  rewrite [← and_assoc]
  apply and_congr_right
  intro ht
  rewrite [Nat.not_lt_eq, Nat.le_iff_lt_or_eq]
  apply or_iff_left
  intro hxyt
  have : t.1.1 = t.2.1 := (x*y).get_inj _ _ <| Fin.eq_of_val_eq hxyt
  exact Nat.lt_irrefl _ (this ▸ ht.1)
State after:
no goals

State before:
n : Nat
x y : Permutation n
a b c d : Nat
⊢ a + b + (c + d) = a + c + (b + d)
Tactic:
conv => lhs; rw [Nat.add_assoc, ← Nat.add_assoc b, Nat.add_comm b c, Nat.add_assoc c, ← Nat.add_assoc a]
State after:
no goals

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]
Tactic:
apply BishopFin.count_congr
State after:
case refine_1.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ∀ (a : Fin n × Fin n),
    (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd ↔
      (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑y[↑a.fst] < ↑y[↑a.snd]

State before:
case refine_1.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ∀ (a : Fin n × Fin n),
    (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd ↔
      (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑y[↑a.fst] < ↑y[↑a.snd]
Tactic:
intro t
State after:
case refine_1.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ↑t.fst < ↑t.snd ↔
    (↑t.fst < ↑t.snd ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ↑y[↑t.fst] < ↑y[↑t.snd]

State before:
case refine_1.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ↑t.fst < ↑t.snd ↔
    (↑t.fst < ↑t.snd ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ↑y[↑t.fst] < ↑y[↑t.snd]
Tactic:
conv => lhs; rw [and_comm]
State after:
case refine_1.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    (↑t.fst < ↑t.snd ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ↑y[↑t.fst] < ↑y[↑t.snd]

State before:
case refine_1.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    (↑t.fst < ↑t.snd ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ↑y[↑t.fst] < ↑y[↑t.snd]
Tactic:
conv => rhs; rw [and_assoc]; rhs; rw [and_comm]
State after:
no goals

State before:
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]
Tactic:
apply BishopFin.count_congr
State after:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ∀ (a : Fin n × Fin n),
    (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd] ↔
      (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]

State before:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ∀ (a : Fin n × Fin n),
    (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd] ↔
      (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]
Tactic:
intro t
State after:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    (↑t.fst < ↑t.snd ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ¬↑y[↑t.fst] < ↑y[↑t.snd]

State before:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    (↑t.fst < ↑t.snd ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ¬↑y[↑t.fst] < ↑y[↑t.snd]
Tactic:
conv =>
  rhs; rw [and_assoc]
  conv => rhs; rw [and_comm]
  rw [← and_assoc]
State after:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    (↑t.fst < ↑t.snd ∧ ¬↑y[↑t.fst] < ↑y[↑t.snd]) ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]

State before:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    (↑t.fst < ↑t.snd ∧ ¬↑y[↑t.fst] < ↑y[↑t.snd]) ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]
Tactic:
refine and_congr_left' ?_
State after:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ↔ ↑t.fst < ↑t.snd ∧ ¬↑y[↑t.fst] < ↑y[↑t.snd]

State before:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ↔ ↑t.fst < ↑t.snd ∧ ¬↑y[↑t.fst] < ↑y[↑t.snd]
Tactic:
refine and_congr_right ?_
State after:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ ↑t.fst < ↑t.snd → (↑y[↑t.fst] > ↑y[↑t.snd] ↔ ¬↑y[↑t.fst] < ↑y[↑t.snd])

State before:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ ↑t.fst < ↑t.snd → (↑y[↑t.fst] > ↑y[↑t.snd] ↔ ¬↑y[↑t.fst] < ↑y[↑t.snd])
Tactic:
intro ht
State after:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
⊢ ↑y[↑t.fst] > ↑y[↑t.snd] ↔ ¬↑y[↑t.fst] < ↑y[↑t.snd]

State before:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
⊢ ↑y[↑t.fst] > ↑y[↑t.snd] ↔ ¬↑y[↑t.fst] < ↑y[↑t.snd]
Tactic:
simp only [Nat.not_lt_eq, Nat.le_iff_lt_or_eq]
State after:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
⊢ ↑y[↑t.fst] > ↑y[↑t.snd] ↔ ↑y[↑t.snd] < ↑y[↑t.fst] ∨ ↑y[↑t.snd] = ↑y[↑t.fst]

State before:
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
⊢ ↑y[↑t.fst] > ↑y[↑t.snd] ↔ ↑y[↑t.snd] < ↑y[↑t.fst] ∨ ↑y[↑t.snd] = ↑y[↑t.fst]
Tactic:
apply Iff.symm
State after:
case refine_2.h.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
⊢ ↑y[↑t.snd] < ↑y[↑t.fst] ∨ ↑y[↑t.snd] = ↑y[↑t.fst] ↔ ↑y[↑t.fst] > ↑y[↑t.snd]

State before:
case refine_2.h.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
⊢ ↑y[↑t.snd] < ↑y[↑t.fst] ∨ ↑y[↑t.snd] = ↑y[↑t.fst] ↔ ↑y[↑t.fst] > ↑y[↑t.snd]
Tactic:
apply or_iff_left
State after:
case refine_2.h.h.hb
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
⊢ ¬↑y[↑t.snd] = ↑y[↑t.fst]

State before:
case refine_2.h.h.hb
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
⊢ ¬↑y[↑t.snd] = ↑y[↑t.fst]
Tactic:
intro hyt
State after:
case refine_2.h.h.hb
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
hyt : ↑y[↑t.snd] = ↑y[↑t.fst]
⊢ False

State before:
case refine_2.h.h.hb
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
hyt : ↑y[↑t.snd] = ↑y[↑t.fst]
⊢ False
Tactic:
exact Nat.lt_irrefl _ <| (y.get_inj _ _ <| Fin.eq_of_val_eq hyt) ▸ ht
State after:
no goals

State before:
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]
Tactic:
let swap : Fin n × Fin n → Fin n × Fin n :=
  fun t => ⟨t.2, t.1⟩
State after:
case refine_3
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
⊢ (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]

State before:
case refine_3
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
⊢ (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]
Tactic:
have : ∀ t, swap (swap t) = t := fun | .mk i j => rfl
State after:
case refine_3
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
⊢ (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]

State before:
case refine_3
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
⊢ (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]
Tactic:
conv =>
  lhs; rw [BishopFin.count_eq_count_invimage_of_inv swap swap this this]
State after:
case refine_3
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
⊢ BishopFin.count
      ((fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) ∘ swap) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

State before:
case refine_3
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
⊢ BishopFin.count
      ((fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) ∘ swap) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
dsimp only [Function.comp]
State after:
case refine_3
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
⊢ (BishopFin.count fun x_1 =>
      (↑y[↑x_1.snd] < ↑y[↑x_1.fst] ∧ ↑(x * y)[↑x_1.snd] > ↑(x * y)[↑x_1.fst]) ∧ ¬↑x_1.snd < ↑x_1.fst) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

State before:
case refine_3
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
⊢ (BishopFin.count fun x_1 =>
      (↑y[↑x_1.snd] < ↑y[↑x_1.fst] ∧ ↑(x * y)[↑x_1.snd] > ↑(x * y)[↑x_1.fst]) ∧ ¬↑x_1.snd < ↑x_1.fst) =
    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
State after:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
⊢ ∀ (a : Fin n × Fin n),
    (↑y[↑a.snd] < ↑y[↑a.fst] ∧ ↑(x * y)[↑a.snd] > ↑(x * y)[↑a.fst]) ∧ ¬↑a.snd < ↑a.fst ↔
      ↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] < ↑(x * y)[↑a.snd]

State before:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
⊢ ∀ (a : Fin n × Fin n),
    (↑y[↑a.snd] < ↑y[↑a.fst] ∧ ↑(x * y)[↑a.snd] > ↑(x * y)[↑a.fst]) ∧ ¬↑a.snd < ↑a.fst ↔
      ↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] < ↑(x * y)[↑a.snd]
Tactic:
intro t
State after:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
⊢ (↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst]) ∧ ¬↑t.snd < ↑t.fst ↔
    ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

State before:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
⊢ (↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst]) ∧ ¬↑t.snd < ↑t.fst ↔
    ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
conv => lhs; rw [and_comm]
State after:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
⊢ ¬↑t.snd < ↑t.fst ∧ ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst] ↔
    ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

State before:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
⊢ ¬↑t.snd < ↑t.fst ∧ ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst] ↔
    ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
refine and_congr_left ?_
State after:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
⊢ ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst] → (¬↑t.snd < ↑t.fst ↔ ↑t.fst < ↑t.snd)

State before:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
⊢ ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst] → (¬↑t.snd < ↑t.fst ↔ ↑t.fst < ↑t.snd)
Tactic:
intro ht
State after:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
ht : ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst]
⊢ ¬↑t.snd < ↑t.fst ↔ ↑t.fst < ↑t.snd

State before:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
ht : ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst]
⊢ ¬↑t.snd < ↑t.fst ↔ ↑t.fst < ↑t.snd
Tactic:
rewrite [Nat.not_lt_eq, Nat.le_iff_lt_or_eq]
State after:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
ht : ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst]
⊢ ↑t.fst < ↑t.snd ∨ ↑t.fst = ↑t.snd ↔ ↑t.fst < ↑t.snd

State before:
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
ht : ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst]
⊢ ↑t.fst < ↑t.snd ∨ ↑t.fst = ↑t.snd ↔ ↑t.fst < ↑t.snd
Tactic:
apply or_iff_left
State after:
case refine_3.h.hb
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
ht : ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst]
⊢ ¬↑t.fst = ↑t.snd

State before:
case refine_3.h.hb
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
ht : ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst]
⊢ ¬↑t.fst = ↑t.snd
Tactic:
intro ht'
State after:
case refine_3.h.hb
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
ht : ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst]
ht' : ↑t.fst = ↑t.snd
⊢ False

State before:
case refine_3.h.hb
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
ht : ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst]
ht' : ↑t.fst = ↑t.snd
⊢ False
Tactic:
cases t
State after:
case refine_3.h.hb.mk
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
fst✝ snd✝ : Fin n
ht : ↑y[↑(fst✝, snd✝).snd] < ↑y[↑(fst✝, snd✝).fst] ∧ ↑(x * y)[↑(fst✝, snd✝).snd] > ↑(x * y)[↑(fst✝, snd✝).fst]
ht' : ↑(fst✝, snd✝).fst = ↑(fst✝, snd✝).snd
⊢ False

State before:
case refine_3.h.hb.mk
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
fst✝ snd✝ : Fin n
ht : ↑y[↑(fst✝, snd✝).snd] < ↑y[↑(fst✝, snd✝).fst] ∧ ↑(x * y)[↑(fst✝, snd✝).snd] > ↑(x * y)[↑(fst✝, snd✝).fst]
ht' : ↑(fst✝, snd✝).fst = ↑(fst✝, snd✝).snd
⊢ False
Tactic:
dsimp at *
State after:
case refine_3.h.hb.mk
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), (t.fst, t.snd) = t
fst✝ snd✝ : Fin n
ht : ↑y[↑snd✝] < ↑y[↑fst✝] ∧ ↑(x * y)[↑snd✝] > ↑(x * y)[↑fst✝]
ht' : ↑fst✝ = ↑snd✝
⊢ False

State before:
case refine_3.h.hb.mk
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), (t.fst, t.snd) = t
fst✝ snd✝ : Fin n
ht : ↑y[↑snd✝] < ↑y[↑fst✝] ∧ ↑(x * y)[↑snd✝] > ↑(x * y)[↑fst✝]
ht' : ↑fst✝ = ↑snd✝
⊢ False
Tactic:
cases Fin.eq_of_val_eq ht'
State after:
case refine_3.h.hb.mk.refl
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), (t.fst, t.snd) = t
fst✝ : Fin n
ht : ↑y[↑fst✝] < ↑y[↑fst✝] ∧ ↑(x * y)[↑fst✝] > ↑(x * y)[↑fst✝]
ht' : ↑fst✝ = ↑fst✝
⊢ False

State before:
case refine_3.h.hb.mk.refl
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), (t.fst, t.snd) = t
fst✝ : Fin n
ht : ↑y[↑fst✝] < ↑y[↑fst✝] ∧ ↑(x * y)[↑fst✝] > ↑(x * y)[↑fst✝]
ht' : ↑fst✝ = ↑fst✝
⊢ False
Tactic:
exact Nat.lt_irrefl _ ht.1
State after:
no goals

State before:
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
State after:
case refine_4.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ∀ (a : Fin n × Fin n),
    (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd] ↔
      ↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] < ↑(x * y)[↑a.snd]

State before:
case refine_4.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ∀ (a : Fin n × Fin n),
    (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd] ↔
      ↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] < ↑(x * y)[↑a.snd]
Tactic:
intro t
State after:
case refine_4.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ¬↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

State before:
case refine_4.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ¬↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
rewrite [← and_assoc]
State after:
case refine_4.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ¬↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

State before:
case refine_4.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ¬↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
apply and_congr_right
State after:
case refine_4.h.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] →
    (¬↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd])

State before:
case refine_4.h.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] →
    (¬↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd])
Tactic:
intro ht
State after:
case refine_4.h.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]
⊢ ¬↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

State before:
case refine_4.h.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]
⊢ ¬↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
rewrite [Nat.not_lt_eq, Nat.le_iff_lt_or_eq]
State after:
case refine_4.h.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]
⊢ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd] ∨ ↑(x * y)[↑t.fst] = ↑(x * y)[↑t.snd] ↔ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]

State before:
case refine_4.h.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]
⊢ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd] ∨ ↑(x * y)[↑t.fst] = ↑(x * y)[↑t.snd] ↔ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
Tactic:
apply or_iff_left
State after:
case refine_4.h.h.hb
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]
⊢ ¬↑(x * y)[↑t.fst] = ↑(x * y)[↑t.snd]

State before:
case refine_4.h.h.hb
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]
⊢ ¬↑(x * y)[↑t.fst] = ↑(x * y)[↑t.snd]
Tactic:
intro hxyt
State after:
case refine_4.h.h.hb
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]
hxyt : ↑(x * y)[↑t.fst] = ↑(x * y)[↑t.snd]
⊢ False

State before:
case refine_4.h.h.hb
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]
hxyt : ↑(x * y)[↑t.fst] = ↑(x * y)[↑t.snd]
⊢ False
Tactic:
have : t.1.1 = t.2.1 := (x*y).get_inj _ _ <| Fin.eq_of_val_eq hxyt
State after:
case refine_4.h.h.hb
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]
hxyt : ↑(x * y)[↑t.fst] = ↑(x * y)[↑t.snd]
this : ↑t.fst = ↑t.snd
⊢ False

State before:
case refine_4.h.h.hb
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]
hxyt : ↑(x * y)[↑t.fst] = ↑(x * y)[↑t.snd]
this : ↑t.fst = ↑t.snd
⊢ False
Tactic:
exact Nat.lt_irrefl _ (this ▸ ht.1)
State after:
no goals