internlm/Lean-Github huggingface dataset:
Theorem: Permutation.nodup_inversions
Proof state before:
case right.inl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
iv : Inversion x
hmem : iv ∈ ivs'
⊢ ↑iv.snd = k ∧ ↑iv.fst < l → ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
exact And.imp_right Nat.le.step
Proof state after:
no goals
Theorem: Permutation.nodup_inversions
Proof state before:
case right.inr
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
iv : Inversion x
heq :
  iv =
    { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
      lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
      inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
cases heq
Proof state after:
case right.inr.refl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ↑{ fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
            lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
            inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }.snd <
      k ∨
    ↑{ fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
              lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
              inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }.snd =
        k ∧
      ↑{ fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
              lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
              inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }.fst <
        l + 1
Theorem: Permutation.nodup_inversions
Proof state before:
case right.inr.refl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ↑{ fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
            lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
            inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }.snd <
      k ∨
    ↑{ fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
              lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
              inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }.snd =
        k ∧
      ↑{ fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
              lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
              inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }.fst <
        l + 1
Tactic:
dsimp
Proof state after:
case right.inr.refl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ k < k ∨ k = k ∧ l < l + 1
Theorem: Permutation.nodup_inversions
Proof state before:
case right.inr.refl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ k < k ∨ k = k ∧ l < l + 1
Tactic:
exact Or.inr ⟨rfl, l.lt_succ_self⟩
Proof state after:
no goals
Theorem: Permutation.nodup_inversions
Proof state before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
⊢ Array.Nodup
      (if h : x[l] > x[k] then
        Array.push ivs'
          { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
            lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
            inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
      else ivs') ∧
    ∀ (iv : Inversion x),
      (iv ∈
          if h : x[l] > x[k] then
            Array.push ivs'
              { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
                lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
                inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
          else ivs') →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
simp only [dif_neg hx]
Proof state after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
⊢ Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Theorem: Permutation.nodup_inversions
Proof state before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
⊢ Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
apply And.intro ivs'_nodup
Proof state after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
⊢ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Theorem: Permutation.nodup_inversions
Proof state before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
⊢ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
intro iv hiv
Proof state after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Theorem: Permutation.nodup_inversions
Proof state before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
specialize ivs'_lt iv hiv
Proof state after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
ivs'_lt : ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Theorem: Permutation.nodup_inversions
Proof state before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
ivs'_lt : ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
refine Or.imp_right ?_ ivs'_lt
Proof state after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
ivs'_lt : ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ ↑iv.snd = k ∧ ↑iv.fst < l → ↑iv.snd = k ∧ ↑iv.fst < l + 1
Theorem: Permutation.nodup_inversions
Proof state before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
ivs'_lt : ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ ↑iv.snd = k ∧ ↑iv.fst < l → ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
exact And.imp_right Nat.le.step
Proof state after:
no goals
Theorem: Permutation.inversions_size_eq_card
Proof state before:
n : Nat
x : Permutation n
⊢ List.length (inversions x).data = List.length (Array.toList (inversions x))
Tactic:
rw [Array.toList_eq]
Proof state after:
no goals
Theorem: Permutation.Inversion.card_eq
Proof state before:
n : Nat
x : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]
Tactic:
rewrite [BishopFin.count_eq_card]
Proof state after:
n : Nat
x : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.card { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }
Theorem: Permutation.Inversion.card_eq
Proof state before:
n : Nat
x : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.card { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }
Tactic:
refine BishopFin.card_eq_card_of_bij ?_ ?_ ?_
Proof state after:
case refine_1
n : Nat
x : Permutation n
⊢ Inversion x → { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }

case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }), ∃ a, ?refine_1 a = b

case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x), ?refine_1 a₁ = ?refine_1 a₂ → a₁ = a₂
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_1
n : Nat
x : Permutation n
⊢ Inversion x → { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }

case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }), ∃ a, ?refine_1 a = b

case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x), ?refine_1 a₁ = ?refine_1 a₂ → a₁ = a₂
Tactic:
. exact fun iv => ⟨⟨iv.1,iv.2⟩, iv.3, iv.4⟩
Proof state after:
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }),
    ∃ a,
      { val := (a.fst, a.snd),
          property :=
            (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
        b

case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }),
    ∃ a,
      { val := (a.fst, a.snd),
          property :=
            (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
        b

case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂
Tactic:
. intro t; exact ⟨⟨t.1.1, t.1.2, t.2.1, t.2.2⟩, rfl⟩
Proof state after:
case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂
Tactic:
. intro iv₁ iv₂
  simp only [Subtype.mk.injEq, Prod.mk.injEq, and_imp]
  intro hfst hsnd
  cases iv₁; cases iv₂; cases hfst; cases hsnd; rfl
Proof state after:
no goals
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_1
n : Nat
x : Permutation n
⊢ Inversion x → { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }
Tactic:
exact fun iv => ⟨⟨iv.1,iv.2⟩, iv.3, iv.4⟩
Proof state after:
no goals
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }),
    ∃ a,
      { val := (a.fst, a.snd),
          property :=
            (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
        b
Tactic:
intro t
Proof state after:
case refine_2
n : Nat
x : Permutation n
t : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }
⊢ ∃ a,
    { val := (a.fst, a.snd),
        property :=
          (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
      t
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_2
n : Nat
x : Permutation n
t : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }
⊢ ∃ a,
    { val := (a.fst, a.snd),
        property :=
          (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
      t
Tactic:
exact ⟨⟨t.1.1, t.1.2, t.2.1, t.2.2⟩, rfl⟩
Proof state after:
no goals
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂
Tactic:
intro iv₁ iv₂
Proof state after:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ { val := (iv₁.fst, iv₁.snd),
        property :=
          (_ :
            ↑(iv₁.fst, iv₁.snd).fst < ↑(iv₁.fst, iv₁.snd).snd ∧
              ↑x[↑(iv₁.fst, iv₁.snd).fst] > ↑x[↑(iv₁.fst, iv₁.snd).snd]) } =
      { val := (iv₂.fst, iv₂.snd),
        property :=
          (_ :
            ↑(iv₂.fst, iv₂.snd).fst < ↑(iv₂.fst, iv₂.snd).snd ∧
              ↑x[↑(iv₂.fst, iv₂.snd).fst] > ↑x[↑(iv₂.fst, iv₂.snd).snd]) } →
    iv₁ = iv₂
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ { val := (iv₁.fst, iv₁.snd),
        property :=
          (_ :
            ↑(iv₁.fst, iv₁.snd).fst < ↑(iv₁.fst, iv₁.snd).snd ∧
              ↑x[↑(iv₁.fst, iv₁.snd).fst] > ↑x[↑(iv₁.fst, iv₁.snd).snd]) } =
      { val := (iv₂.fst, iv₂.snd),
        property :=
          (_ :
            ↑(iv₂.fst, iv₂.snd).fst < ↑(iv₂.fst, iv₂.snd).snd ∧
              ↑x[↑(iv₂.fst, iv₂.snd).fst] > ↑x[↑(iv₂.fst, iv₂.snd).snd]) } →
    iv₁ = iv₂
Tactic:
simp only [Subtype.mk.injEq, Prod.mk.injEq, and_imp]
Proof state after:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ iv₁.fst = iv₂.fst → iv₁.snd = iv₂.snd → iv₁ = iv₂
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ iv₁.fst = iv₂.fst → iv₁.snd = iv₂.snd → iv₁ = iv₂
Tactic:
intro hfst hsnd
Proof state after:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
hfst : iv₁.fst = iv₂.fst
hsnd : iv₁.snd = iv₂.snd
⊢ iv₁ = iv₂
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
hfst : iv₁.fst = iv₂.fst
hsnd : iv₁.snd = iv₂.snd
⊢ iv₁ = iv₂
Tactic:
cases iv₁
Proof state after:
case refine_3.mk
n : Nat
x : Permutation n
iv₂ : Inversion x
fst✝ snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hfst : { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.fst = iv₂.fst
hsnd : { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd = iv₂.snd
⊢ { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ } = iv₂
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_3.mk
n : Nat
x : Permutation n
iv₂ : Inversion x
fst✝ snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hfst : { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.fst = iv₂.fst
hsnd : { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd = iv₂.snd
⊢ { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ } = iv₂
Tactic:
cases iv₂
Proof state after:
case refine_3.mk.mk
n : Nat
x : Permutation n
fst✝¹ snd✝¹ : Fin n
lt✝¹ : fst✝¹ < snd✝¹
inverted✝¹ : x[↑fst✝¹] > x[↑snd✝¹]
fst✝ snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hfst :
  { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.fst =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.fst
hsnd :
  { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.snd =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_3.mk.mk
n : Nat
x : Permutation n
fst✝¹ snd✝¹ : Fin n
lt✝¹ : fst✝¹ < snd✝¹
inverted✝¹ : x[↑fst✝¹] > x[↑snd✝¹]
fst✝ snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hfst :
  { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.fst =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.fst
hsnd :
  { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.snd =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }
Tactic:
cases hfst
Proof state after:
case refine_3.mk.mk.refl
n : Nat
x : Permutation n
fst✝ snd✝¹ : Fin n
lt✝¹ : fst✝ < snd✝¹
inverted✝¹ : x[↑fst✝] > x[↑snd✝¹]
snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hsnd :
  { fst := fst✝, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.snd =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_3.mk.mk.refl
n : Nat
x : Permutation n
fst✝ snd✝¹ : Fin n
lt✝¹ : fst✝ < snd✝¹
inverted✝¹ : x[↑fst✝] > x[↑snd✝¹]
snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hsnd :
  { fst := fst✝, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.snd =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }
Tactic:
cases hsnd
Proof state after:
case refine_3.mk.mk.refl.refl
n : Nat
x : Permutation n
fst✝ snd✝ : Fin n
lt✝¹ : fst✝ < snd✝
inverted✝¹ : x[↑fst✝] > x[↑snd✝]
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
⊢ { fst := fst✝, snd := snd✝, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }
Theorem: Permutation.Inversion.card_eq
Proof state before:
case refine_3.mk.mk.refl.refl
n : Nat
x : Permutation n
fst✝ snd✝ : Fin n
lt✝¹ : fst✝ < snd✝
inverted✝¹ : x[↑fst✝] > x[↑snd✝]
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
⊢ { fst := fst✝, snd := snd✝, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }
Tactic:
rfl
Proof state after:
no goals
Theorem: Permutation.Inversion.card_eq_of_mul
Proof state before:
n : Nat
x y : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]
Tactic:
rewrite [Inversion.card_eq x]
Proof state after:
n : Nat
x y : Permutation n
⊢ (BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]) =
    BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]
Theorem: Permutation.Inversion.card_eq_of_mul
Proof state before:
n : Nat
x y : Permutation n
⊢ (BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]) =
    BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]
Tactic:
simp only [get_mul]
Proof state after:
n : Nat
x y : Permutation n
⊢ (BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]) =
    BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑x[↑y[↑t.fst]] > ↑x[↑y[↑t.snd]]
Theorem: Permutation.Inversion.card_eq_of_mul
Proof state before:
n : Nat
x y : Permutation n
⊢ (BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]) =
    BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑x[↑y[↑t.fst]] > ↑x[↑y[↑t.snd]]
Tactic:
refine BishopFin.count_eq_count_invimage_of_inv (Prod.map y.toFun y.toFun) (Prod.map y.inv.toFun y.inv.toFun) ?_ ?_
Proof state after:
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