internlm/Lean-Github huggingface dataset:
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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)
Proof state after:
no goals
Theorem: Permutation.inversionNum_add
Proof 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]
Proof state after:
no goals
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]
Tactic:
apply BishopFin.count_congr
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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]
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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]
Proof state after:
no goals
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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]
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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' ?_
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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 ?_
Proof 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])
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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]
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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
Theorem: Permutation.inversionNum_add
Proof 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
Proof state after:
no goals
Theorem: Permutation.inversionNum_add
Proof 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⟩
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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]
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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]
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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]
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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 ?_
Proof 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)
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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
Theorem: Permutation.inversionNum_add
Proof 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]
Proof 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
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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
Theorem: Permutation.inversionNum_add
Proof 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'
Proof 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