internlm/Lean-Github huggingface dataset:
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
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)
Tactic:
rfl
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:
exfalso
Proof state after:
case h
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
⊢ False
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
case h
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
⊢ False
Tactic:
conv at hinv => simp only [hil, if_neg]; change i+1 > l.1
Proof state after:
case h
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 : i + 1 > ↑l
hil : ¬i + 1 = ↑l
⊢ False
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
case h
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 : i + 1 > ↑l
hil : ¬i + 1 = ↑l
⊢ False
Tactic:
exact Nat.not_le_of_lt hinv hlt
Proof state after:
no goals
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
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 = ↑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 = ↑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:
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:
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 = ↑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) }
hik : i = ↑k
⊢ { 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:
have : ⟨i, Nat.lt_of_succ_lt h⟩ = k := Fin.eq_of_val_eq hik
Proof state after:
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 = ↑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) }
hik : i = ↑k
this : { val := i, isLt := (_ : i < n) } = k
⊢ { 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:
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 = ↑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) }
hik : i = ↑k
this : { val := i, isLt := (_ : i < n) } = k
⊢ { 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:
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 :
  (if i = ↑{ val := i, isLt := (_ : i < n) } then { val := i + 1, isLt := h }
    else
      { val := ↑{ val := i, isLt := (_ : i < n) },
        isLt :=
          (_ :
            (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h })
              ↑{ val := i, isLt := (_ : i < n) }) }) >
    { val := i, isLt := (_ : i < n) }
hik : i = ↑{ val := i, isLt := (_ : i < n) }
⊢ { 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)
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
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 :
  (if i = ↑{ val := i, isLt := (_ : i < n) } then { val := i + 1, isLt := h }
    else
      { val := ↑{ val := i, isLt := (_ : i < n) },
        isLt :=
          (_ :
            (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h })
              ↑{ val := i, isLt := (_ : i < n) }) }) >
    { val := i, isLt := (_ : i < n) }
hik : i = ↑{ val := i, isLt := (_ : i < n) }
⊢ { 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)
Tactic:
rfl
Proof state after:
no goals
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
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 = ↑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) }
hik : ¬i = ↑k
⊢ { 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:
exfalso
Proof state after:
case h
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 = ↑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) }
hik : ¬i = ↑k
⊢ False
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
case h
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 = ↑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) }
hik : ¬i = ↑k
⊢ False
Tactic:
conv at hinv => simp only [hik, if_neg]; change k.1 > i
Proof state after:
case h
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 : ↑k > i
hik : ¬i = ↑k
⊢ False
Theorem: Permutation.Inversion.eq_transpos_adj
Proof state before:
case h
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 : ↑k > i
hik : ¬i = ↑k
⊢ False
Tactic:
exact Nat.not_le_of_lt hlt hinv
Proof state after:
no goals
Theorem: Permutation.inversionNum_transposAdj
Proof state before:
n i : Nat
h : i + 1 < n
⊢ inversionNum (transposAdj i h) = 1
Tactic:
rewrite [inversionNum_eq_card_inversion]
Proof state after:
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) = 1
Theorem: Permutation.inversionNum_transposAdj
Proof state before:
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) = 1
Tactic:
refine Nat.le_antisymm ?le ?ge
Proof state after:
case le
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) ≤ 1

case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))
Theorem: Permutation.inversionNum_transposAdj
Proof state before:
case le
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) ≤ 1

case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))
Tactic:
. exact BishopFin.card_subsingleton
Proof state after:
case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))
Theorem: Permutation.inversionNum_transposAdj
Proof state before:
case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))
Tactic:
. exact BishopFin.card_nonempty
Proof state after:
no goals
Theorem: Permutation.inversionNum_transposAdj
Proof state before:
case le
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) ≤ 1
Tactic:
exact BishopFin.card_subsingleton
Proof state after:
no goals
Theorem: Permutation.inversionNum_transposAdj
Proof state before:
case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))
Tactic:
exact BishopFin.card_nonempty
Proof state after:
no goals
Theorem: List.get_take
Proof state before:
α : Type u
β : Type v
l : List α
n i : Nat
hi : i < length (take n l)
hi' : i < length l
⊢ get (take n l) { val := i, isLt := hi } = get l { val := i, isLt := hi' }
Tactic:
rw [get_of_eq (l.take_append_drop n).symm, get_append_left]
Proof state after:
no goals
Theorem: List.length_pmap
Proof state before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
⊢ length (pmap f l h) = length l
Tactic:
induction l with
| nil => rfl
| cons a l IH => dsimp [pmap]; rw [IH]
Proof state after:
no goals
Theorem: List.length_pmap
Proof state before:
case nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ [] → p a
⊢ length (pmap f [] h) = length []
Tactic:
rfl
Proof state after:
no goals
Theorem: List.length_pmap
Proof state before:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ (h : ∀ (a : α), a ∈ l → p a), length (pmap f l h) = length l
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ length (pmap f (a :: l) h) = length (a :: l)
Tactic:
dsimp [pmap]
Proof state after:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ (h : ∀ (a : α), a ∈ l → p a), length (pmap f l h) = length l
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ Nat.succ (length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) = Nat.succ (length l)
Theorem: List.length_pmap
Proof state before:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ (h : ∀ (a : α), a ∈ l → p a), length (pmap f l h) = length l
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ Nat.succ (length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) = Nat.succ (length l)
Tactic:
rw [IH]
Proof state after:
no goals
Theorem: List.Nodup.length_le_of_subset
Proof state before:
α : Type u
β : Type v
l l₁ : List α
nodup : Nodup l
h : l ⊆ l₁
⊢ length l ≤ length l₁
Tactic:
induction l generalizing l₁ with
| nil => exact l₁.length.zero_le
| cons a l IH =>
  have .cons nodup_head (nodup_tail : l.Nodup) := nodup
  let ⟨ha,hl⟩ := cons_subset.mp h
  clear nodup h
  have ⟨l₁', l₁'', hl₁⟩ := mem_iff_append.mp ha
  cases hl₁; clear ha
  have : l ⊆ l₁' ++ l₁'' := fun b hb => 
    match mem_append.mp (hl hb) with
    | .inl hb => mem_append.mpr <| Or.inl hb
    | .inr hb => mem_append.mpr <| Or.inr <|
      match hb with
      | .head _ => absurd rfl <| nodup_head b ‹b ∈ l›
      | .tail _ h => h
  specialize IH nodup_tail this
  simp only [length_append, length_cons] at IH ⊢
  exact Nat.succ_le_succ IH
Proof state after:
no goals
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case nil
α : Type u
β : Type v
l₁ : List α
nodup : Nodup []
h : [] ⊆ l₁
⊢ length [] ≤ length l₁
Tactic:
exact l₁.length.zero_le
Proof state after:
no goals
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup : Nodup (a :: l)
h : a :: l ⊆ l₁
⊢ length (a :: l) ≤ length l₁
Tactic:
have .cons nodup_head (nodup_tail : l.Nodup) := nodup
Proof state after:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup : Nodup (a :: l)
h : a :: l ⊆ l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ length (a :: l) ≤ length l₁
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup : Nodup (a :: l)
h : a :: l ⊆ l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ length (a :: l) ≤ length l₁
Tactic:
let ⟨ha,hl⟩ := cons_subset.mp h
Proof state after:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup : Nodup (a :: l)
h : a :: l ⊆ l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
⊢ length (a :: l) ≤ length l₁
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup : Nodup (a :: l)
h : a :: l ⊆ l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
⊢ length (a :: l) ≤ length l₁
Tactic:
clear nodup h
Proof state after:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
⊢ length (a :: l) ≤ length l₁
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
⊢ length (a :: l) ≤ length l₁
Tactic:
have ⟨l₁', l₁'', hl₁⟩ := mem_iff_append.mp ha
Proof state after:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
l₁' l₁'' : List α
hl₁ : l₁ = l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length l₁
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
l₁' l₁'' : List α
hl₁ : l₁ = l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length l₁
Tactic:
cases hl₁
Proof state after:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
ha : a ∈ l₁' ++ a :: l₁''
hl : l ⊆ l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
ha : a ∈ l₁' ++ a :: l₁''
hl : l ⊆ l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Tactic:
clear ha
Proof state after:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Tactic:
have : l ⊆ l₁' ++ l₁'' := fun b hb => 
  match mem_append.mp (hl hb) with
  | .inl hb => mem_append.mpr <| Or.inl hb
  | .inr hb => mem_append.mpr <| Or.inr <|
    match hb with
    | .head _ => absurd rfl <| nodup_head b ‹b ∈ l›
    | .tail _ h => h
Proof state after:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Tactic:
specialize IH nodup_tail this
Proof state after:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
IH : length l ≤ length (l₁' ++ l₁'')
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
IH : length l ≤ length (l₁' ++ l₁'')
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Tactic:
simp only [length_append, length_cons] at IH ⊢
Proof state after:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
IH : length l ≤ length l₁' + length l₁''
⊢ Nat.succ (length l) ≤ length l₁' + Nat.succ (length l₁'')
Theorem: List.Nodup.length_le_of_subset
Proof state before:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
IH : length l ≤ length l₁' + length l₁''
⊢ Nat.succ (length l) ≤ length l₁' + Nat.succ (length l₁'')
Tactic:
exact Nat.succ_le_succ IH
Proof state after:
no goals
Theorem: List.mem_cons_iff_of_mem
Proof state before:
α : Type u
β : Type v
l : List α
a b : α
hb : b ∈ l
⊢ a ∈ b :: l ↔ a ∈ l
Tactic:
simp only [mem_cons, or_iff_right_iff_imp]
Proof state after:
α : Type u
β : Type v
l : List α
a b : α
hb : b ∈ l
⊢ a = b → a ∈ l
Theorem: List.mem_cons_iff_of_mem
Proof state before:
α : Type u
β : Type v
l : List α
a b : α
hb : b ∈ l
⊢ a = b → a ∈ l
Tactic:
intro heq
Proof state after:
α : Type u
β : Type v
l : List α
a b : α
hb : b ∈ l
heq : a = b
⊢ a ∈ l
Theorem: List.mem_cons_iff_of_mem
Proof state before:
α : Type u
β : Type v
l : List α
a b : α
hb : b ∈ l
heq : a = b
⊢ a ∈ l
Tactic:
exact heq ▸ hb
Proof state after:
no goals
Theorem: List.getElem_mem
Proof state before:
α : Type u
β : Type v
l : List α
i : Nat
hi : i < length l
⊢ l[i] ∈ l
Tactic:
rewrite [getElem_eq_get]
Proof state after:
α : Type u
β : Type v
l : List α
i : Nat
hi : i < length l
⊢ get l { val := i, isLt := hi } ∈ l
Theorem: List.getElem_mem
Proof state before:
α : Type u
β : Type v
l : List α
i : Nat
hi : i < length l
⊢ get l { val := i, isLt := hi } ∈ l
Tactic:
exact l.get_mem i hi
Proof state after:
no goals
Theorem: List.get_pmap
Proof state before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
i : Fin (length (pmap f l h))
⊢ get (pmap f l h) i =
    f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
      (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
Tactic:
induction l with
| nil => exact i.elim0
| cons a l IH =>
  let ⟨i,hi⟩ := i
  cases i <;> dsimp; rfl
  exact IH _ _
Proof state after:
no goals