internlm/Lean-Github huggingface dataset:
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_pos hx, Array.nodup_push, Array.mem_push, ivs'_nodup, true_and]
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]
⊢ ¬{ 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 }]) } ∈
        ivs' ∧
    ∀ (iv : Inversion x),
      iv ∈ ivs' ∨
          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
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]
⊢ ¬{ 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 }]) } ∈
        ivs' ∧
    ∀ (iv : Inversion x),
      iv ∈ ivs' ∨
          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:
constructor
Proof state after:
case left
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 }]) } ∈
      ivs'

case right
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 =
          { 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
Theorem: Permutation.nodup_inversions
Proof state before:
case left
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 }]) } ∈
      ivs'

case right
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 =
          { 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:
. intro h
  specialize ivs'_lt _ h; dsimp at ivs'_lt
  refine ivs'_lt.elim ?_ ?_
  . exact Nat.lt_irrefl k
  . intro h; exact Nat.lt_irrefl l h.2
Proof state after:
case right
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 =
          { 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
Theorem: Permutation.nodup_inversions
Proof state before:
case right
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 =
          { 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:
. intro iv hiv
  cases hiv with
  | inl hmem =>
    refine Or.imp_right ?_ <| ivs'_lt iv hmem
    exact And.imp_right Nat.le.step
  | inr heq =>
    cases heq; dsimp
    exact Or.inr ⟨rfl, l.lt_succ_self⟩
Proof state after:
no goals
Theorem: Permutation.nodup_inversions
Proof state before:
case left
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 }]) } ∈
      ivs'
Tactic:
intro h
Proof state after:
case left
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]
h :
  { 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 }]) } ∈
    ivs'
⊢ False
Theorem: Permutation.nodup_inversions
Proof state before:
case left
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]
h :
  { 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 }]) } ∈
    ivs'
⊢ False
Tactic:
specialize ivs'_lt _ h
Proof state after:
case left
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt :
  ↑{ 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
⊢ False
Theorem: Permutation.nodup_inversions
Proof state before:
case left
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt :
  ↑{ 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
⊢ False
Tactic:
dsimp at ivs'_lt
Proof state after:
case left
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ False
Theorem: Permutation.nodup_inversions
Proof state before:
case left
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ False
Tactic:
refine ivs'_lt.elim ?_ ?_
Proof state after:
case left.refine_1
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k < k → False

case left.refine_2
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k = k ∧ l < l → False
Theorem: Permutation.nodup_inversions
Proof state before:
case left.refine_1
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k < k → False

case left.refine_2
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k = k ∧ l < l → False
Tactic:
. exact Nat.lt_irrefl k
Proof state after:
case left.refine_2
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k = k ∧ l < l → False
Theorem: Permutation.nodup_inversions
Proof state before:
case left.refine_2
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k = k ∧ l < l → False
Tactic:
. intro h; exact Nat.lt_irrefl l h.2
Proof state after:
no goals
Theorem: Permutation.nodup_inversions
Proof state before:
case left.refine_1
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k < k → False
Tactic:
exact Nat.lt_irrefl k
Proof state after:
no goals
Theorem: Permutation.nodup_inversions
Proof state before:
case left.refine_2
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]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k = k ∧ l < l → False
Tactic:
intro h
Proof state after:
case left.refine_2
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]
h✝ :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
h : k = k ∧ l < l
⊢ False
Theorem: Permutation.nodup_inversions
Proof state before:
case left.refine_2
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]
h✝ :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
h : k = k ∧ l < l
⊢ False
Tactic:
exact Nat.lt_irrefl l h.2
Proof state after:
no goals
Theorem: Permutation.nodup_inversions
Proof state before:
case right
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 =
          { 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:
intro iv hiv
Proof state after:
case right
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 =
      { 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
Theorem: Permutation.nodup_inversions
Proof state before:
case right
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 =
      { 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 hiv with
| inl hmem =>
  refine Or.imp_right ?_ <| ivs'_lt iv hmem
  exact And.imp_right Nat.le.step
| inr heq =>
  cases heq; dsimp
  exact Or.inr ⟨rfl, l.lt_succ_self⟩
Proof state after:
no goals
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.snd = k ∧ ↑iv.fst < l + 1
Tactic:
refine Or.imp_right ?_ <| ivs'_lt iv hmem
Proof state after:
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