internlm/Lean-Github huggingface dataset:
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]
ht' : ↑t.fst = ↑t.snd
⊢ False
Tactic:
cases t
Proof 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
Theorem: Permutation.inversionNum_add
Proof 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 *
Proof 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
Theorem: Permutation.inversionNum_add
Proof 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'
Proof 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
Theorem: Permutation.inversionNum_add
Proof 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
Proof state after:
no goals
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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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]
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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])
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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]
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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]
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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
Theorem: Permutation.inversionNum_add
Proof 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
Proof 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
Theorem: Permutation.inversionNum_add
Proof 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)
Proof state after:
no goals
Theorem: Permutation.Inversion.elim1
Proof state before:
n : Nat
α : Sort u
iv : Inversion 1
⊢ α
Tactic:
rcases iv with ⟨i,j,hlt,hinv⟩
Proof state after:
case mk
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : 1[↑i] > 1[↑j]
⊢ α
Theorem: Permutation.Inversion.elim1
Proof state before:
case mk
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : 1[↑i] > 1[↑j]
⊢ α
Tactic:
conv at hinv => simp only [get_one]
Proof state after:
case mk
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : { val := ↑i, isLt := (_ : ↑i < n) } > { val := ↑j, isLt := (_ : ↑j < n) }
⊢ α
Theorem: Permutation.Inversion.elim1
Proof state before:
case mk
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : { val := ↑i, isLt := (_ : ↑i < n) } > { val := ↑j, isLt := (_ : ↑j < n) }
⊢ α
Tactic:
exfalso
Proof state after:
case mk.h
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : { val := ↑i, isLt := (_ : ↑i < n) } > { val := ↑j, isLt := (_ : ↑j < n) }
⊢ False
Theorem: Permutation.Inversion.elim1
Proof state before:
case mk.h
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : { val := ↑i, isLt := (_ : ↑i < n) } > { val := ↑j, isLt := (_ : ↑j < n) }
⊢ False
Tactic:
exact Nat.lt_asymm hlt hinv
Proof state after:
no goals
Theorem: Permutation.inversions_one
Proof state before:
n : Nat
⊢ inversions 1 = #[]
Tactic:
apply Array.ext'
Proof state after:
case h
n : Nat
⊢ (inversions 1).data = #[].data
Theorem: Permutation.inversions_one
Proof state before:
case h
n : Nat
⊢ (inversions 1).data = #[].data
Tactic:
generalize (inversions 1).data = l
Proof state after:
case h
n : Nat
l : List (Inversion 1)
⊢ l = #[].data
Theorem: Permutation.inversions_one
Proof state before:
case h
n : Nat
l : List (Inversion 1)
⊢ l = #[].data
Tactic:
cases l with
| nil => rfl
| cons iv l => exact iv.elim1
Proof state after:
no goals
Theorem: Permutation.inversions_one
Proof state before:
case h.nil
n : Nat
⊢ [] = #[].data
Tactic:
rfl
Proof state after:
no goals
Theorem: Permutation.inversions_one
Proof state before:
case h.cons
n : Nat
iv : Inversion 1
l : List (Inversion 1)
⊢ iv :: l = #[].data
Tactic:
exact iv.elim1
Proof state after:
no goals
Theorem: Permutation.inversionNum_one
Proof state before:
n : Nat
⊢ inversionNum 1 = 0
Tactic:
rewrite [inversionNum_eq_card_inversion]
Proof state after:
n : Nat
⊢ BishopFin.card (Inversion 1) = 0
Theorem: Permutation.inversionNum_one
Proof state before:
n : Nat
⊢ BishopFin.card (Inversion 1) = 0
Tactic:
show (inversions 1).toList.length = 0
Proof state after:
n : Nat
⊢ List.length (Array.toList (inversions 1)) = 0
Theorem: Permutation.inversionNum_one
Proof state before:
n : Nat
⊢ List.length (Array.toList (inversions 1)) = 0
Tactic:
rewrite [inversions_one]
Proof state after:
n : Nat
⊢ List.length (Array.toList #[]) = 0
Theorem: Permutation.inversionNum_one
Proof state before:
n : Nat
⊢ List.length (Array.toList #[]) = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Permutation.Inversion.nonempty_transpos
Proof state before:
n : Nat
i j : Fin n
h : i ≠ j
⊢ Nonempty (Inversion (transpos i j))
Tactic:
cases Nat.lt_or_ge i.1 j.1 with
| inl hlt => exact ⟨transposInversion i j hlt⟩
| inr hge =>
  rewrite [transpos_comm]
  refine ⟨transposInversion j i ?_⟩
  exact Nat.lt_of_le_of_ne hge fun hcntr =>
    h <| Fin.eq_of_val_eq hcntr.symm
Proof state after:
no goals
Theorem: Permutation.Inversion.nonempty_transpos
Proof state before:
case inl
n : Nat
i j : Fin n
h : i ≠ j
hlt : ↑i < ↑j
⊢ Nonempty (Inversion (transpos i j))
Tactic:
exact ⟨transposInversion i j hlt⟩
Proof state after:
no goals
Theorem: Permutation.Inversion.nonempty_transpos
Proof state before:
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ Nonempty (Inversion (transpos i j))
Tactic:
rewrite [transpos_comm]
Proof state after:
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ Nonempty (Inversion (transpos j i))
Theorem: Permutation.Inversion.nonempty_transpos
Proof state before:
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ Nonempty (Inversion (transpos j i))
Tactic:
refine ⟨transposInversion j i ?_⟩
Proof state after:
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ ↑j < ↑i
Theorem: Permutation.Inversion.nonempty_transpos
Proof state before:
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ ↑j < ↑i
Tactic:
exact Nat.lt_of_le_of_ne hge fun hcntr =>
  h <| Fin.eq_of_val_eq hcntr.symm
Proof state after:
no goals
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
n i : Nat
h : i + 1 < n
iv : Inversion (transposAdj i h)
⊢ iv = transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
cases iv.fst_eq_or_snd_eq_of_transpos i.lt_succ_self
<;> cases iv <;> rename_i k l hlt hinv heq <;> cases heq
<;> simp only [transposAdj, get_transpos, if_pos] at hinv
Proof state after:
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  (if i + 1 = i then { val := i, isLt := (_ : i < n) } else { val := i + 1, isLt := h }) >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑l then { val := i + 1, isLt := h }
      else
        { val := ↑l,
          isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i + 1 = ↑k then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑k then { val := i + 1, isLt := h }
      else
        { val := ↑k,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  (if i + 1 = i then { val := i, isLt := (_ : i < n) } else { val := i + 1, isLt := h }) >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑l then { val := i + 1, isLt := h }
      else
        { val := ↑l,
          isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i + 1 = ↑k then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑k then { val := i + 1, isLt := h }
      else
        { val := ↑k,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
. simp only [i.succ_ne_self, Nat.ne_of_lt (a:=i) (b:=l.1) hlt, if_neg] at hinv
  if hil : i+1 = l.1 then
    have : ⟨i+1,h⟩ = l := Fin.eq_of_val_eq hil
    cases this; rfl
  else
    exfalso
    conv at hinv => simp only [hil, if_neg]; change i+1 > l.1
    exact Nat.not_le_of_lt hinv hlt
Proof state after:
case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i + 1 = ↑k then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑k then { val := i + 1, isLt := h }
      else
        { val := ↑k,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i + 1 = ↑k then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑k then { val := i + 1, isLt := h }
      else
        { val := ↑k,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
. simp only [Ne.symm <| Nat.ne_of_lt (a:=k.1) (b:=i+1) hlt, if_neg] at hinv
  if hik : i = k.1 then
    have : ⟨i, Nat.lt_of_succ_lt h⟩ = k := Fin.eq_of_val_eq hik
    cases this; rfl
  else
    exfalso
    conv at hinv => simp only [hik, if_neg]; change k.1 > i
    exact Nat.not_le_of_lt hlt hinv
Proof state after:
no goals
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  (if i + 1 = i then { val := i, isLt := (_ : i < n) } else { val := i + 1, isLt := h }) >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑l then { val := i + 1, isLt := h }
      else
        { val := ↑l,
          isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
simp only [i.succ_ne_self, Nat.ne_of_lt (a:=i) (b:=l.1) hlt, if_neg] at hinv
Proof state after:
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
if hil : i+1 = l.1 then
  have : ⟨i+1,h⟩ = l := Fin.eq_of_val_eq hil
  cases this; rfl
else
  exfalso
  conv at hinv => simp only [hil, if_neg]; change i+1 > l.1
  exact Nat.not_le_of_lt hinv hlt
Proof state after:
no goals
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
hil : i + 1 = ↑l
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
have : ⟨i+1,h⟩ = l := Fin.eq_of_val_eq hil
Proof state after:
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
hil : i + 1 = ↑l
this : { val := i + 1, isLt := h } = l
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
hil : i + 1 = ↑l
this : { val := i + 1, isLt := h } = l
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
cases this
Proof state after:
case refl
n i : Nat
h : i + 1 < n
hlt : { val := i, isLt := (_ : i < n) } < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑{ val := i + 1, isLt := h } then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑{ val := i + 1, isLt := h },
        isLt :=
          (_ :
            (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h })
              ↑{ val := i + 1, isLt := h }) }
hil : i + 1 = ↑{ val := i + 1, isLt := h }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)