internlm/Lean-Github huggingface dataset:
Theorem: List.Nodup.pmap
Proof state before:
case h
α : Type u
β : Type v
p : α → Prop
l : List α
nodup : Nodup l
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ l → p a
f_inj : ∀ (a₁ a₂ : α) (h₁ : p a₁) (h₂ : p a₂), f a₁ h₁ = f a₂ h₂ → a₁ = a₂
i j : Nat
hi : i < length (List.pmap f l h)
hj : j < length (List.pmap f l h)
⊢ (List.pmap f l h)[i] = (List.pmap f l h)[j] → i = j
Tactic:
simp only [getElem_eq_get, get_pmap]
Proof state after:
case h
α : Type u
β : Type v
p : α → Prop
l : List α
nodup : Nodup l
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ l → p a
f_inj : ∀ (a₁ a₂ : α) (h₁ : p a₁) (h₂ : p a₂), f a₁ h₁ = f a₂ h₂ → a₁ = a₂
i j : Nat
hi : i < length (List.pmap f l h)
hj : j < length (List.pmap f l h)
⊢ f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))
        (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))) =
      f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj }))
        (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj }))) →
    i = j
Theorem: List.Nodup.pmap
Proof state before:
case h
α : Type u
β : Type v
p : α → Prop
l : List α
nodup : Nodup l
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ l → p a
f_inj : ∀ (a₁ a₂ : α) (h₁ : p a₁) (h₂ : p a₂), f a₁ h₁ = f a₂ h₂ → a₁ = a₂
i j : Nat
hi : i < length (List.pmap f l h)
hj : j < length (List.pmap f l h)
⊢ f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))
        (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))) =
      f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj }))
        (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj }))) →
    i = j
Tactic:
intro hfij
Proof state after:
case h
α : Type u
β : Type v
p : α → Prop
l : List α
nodup : Nodup l
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ l → p a
f_inj : ∀ (a₁ a₂ : α) (h₁ : p a₁) (h₂ : p a₂), f a₁ h₁ = f a₂ h₂ → a₁ = a₂
i j : Nat
hi : i < length (List.pmap f l h)
hj : j < length (List.pmap f l h)
hfij :
  f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))
      (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))) =
    f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj }))
      (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj })))
⊢ i = j
Theorem: List.Nodup.pmap
Proof state before:
case h
α : Type u
β : Type v
p : α → Prop
l : List α
nodup : Nodup l
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ l → p a
f_inj : ∀ (a₁ a₂ : α) (h₁ : p a₁) (h₂ : p a₂), f a₁ h₁ = f a₂ h₂ → a₁ = a₂
i j : Nat
hi : i < length (List.pmap f l h)
hj : j < length (List.pmap f l h)
hfij :
  f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))
      (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))) =
    f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj }))
      (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj })))
⊢ i = j
Tactic:
specialize f_inj _ _ _ _ hfij
Proof state after:
case h
α : Type u
β : Type v
p : α → Prop
l : List α
nodup : Nodup l
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ l → p a
i j : Nat
hi : i < length (List.pmap f l h)
hj : j < length (List.pmap f l h)
hfij :
  f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))
      (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))) =
    f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj }))
      (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj })))
f_inj :
  get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }) =
    get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj })
⊢ i = j
Theorem: List.Nodup.pmap
Proof state before:
case h
α : Type u
β : Type v
p : α → Prop
l : List α
nodup : Nodup l
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ l → p a
i j : Nat
hi : i < length (List.pmap f l h)
hj : j < length (List.pmap f l h)
hfij :
  f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))
      (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))) =
    f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj }))
      (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj })))
f_inj :
  get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }) =
    get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj })
⊢ i = j
Tactic:
exact nodup.get_inj i j f_inj
Proof state after:
no goals
Theorem: List.Nodup.append
Proof state before:
α : Type u
β : Type v
l l' : List α
nodup : Nodup l
nodup' : Nodup l'
h : ∀ (a : α), a ∈ l → ¬a ∈ l'
⊢ Nodup (l ++ l')
Tactic:
induction l with
| nil => exact nodup'
| cons a l IH =>
  specialize IH nodup.tail fun a ha =>
    h a <| mem_cons_of_mem _ ha
  refine nodup_cons_of_notmem_nodup a ?_ IH
  simp only [append_eq, mem_append, not_or]
  exact ⟨nodup.head, h a <| l.mem_cons_self a⟩
Proof state after:
no goals
Theorem: List.Nodup.append
Proof state before:
case nil
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
nodup : Nodup []
h : ∀ (a : α), a ∈ [] → ¬a ∈ l'
⊢ Nodup ([] ++ l')
Tactic:
exact nodup'
Proof state after:
no goals
Theorem: List.Nodup.append
Proof state before:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
IH : Nodup l → (∀ (a : α), a ∈ l → ¬a ∈ l') → Nodup (l ++ l')
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
⊢ Nodup (a :: l ++ l')
Tactic:
specialize IH nodup.tail fun a ha =>
  h a <| mem_cons_of_mem _ ha
Proof state after:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ Nodup (a :: l ++ l')
Theorem: List.Nodup.append
Proof state before:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ Nodup (a :: l ++ l')
Tactic:
refine nodup_cons_of_notmem_nodup a ?_ IH
Proof state after:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ ¬a ∈ List.append l l'
Theorem: List.Nodup.append
Proof state before:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ ¬a ∈ List.append l l'
Tactic:
simp only [append_eq, mem_append, not_or]
Proof state after:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ ¬a ∈ l ∧ ¬a ∈ l'
Theorem: List.Nodup.append
Proof state before:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ ¬a ∈ l ∧ ¬a ∈ l'
Tactic:
exact ⟨nodup.head, h a <| l.mem_cons_self a⟩
Proof state after:
no goals
Theorem: List.Nodup.product
Proof state before:
α : Type u
β : Type v
la : List α
lb : List β
la_nodup : Nodup la
lb_nodup : Nodup lb
⊢ Nodup (List.product la lb)
Tactic:
induction la with
| nil => exact .nil
| cons a la IH =>
  specialize IH la_nodup.tail
  conv =>
    arg 1
    dsimp [List.product, List.bind]
    change lb.map (Prod.mk a) ++ la.product lb
  refine Nodup.append ?_ IH ?_
  . apply lb_nodup.map
    intro b₁ b₂; exact congrArg Prod.snd
  . intro x
    let ⟨_,b⟩ := x
    simp only [mem_map, Prod.mk.injEq, exists_eq_right_right, and_imp, pair_mem_product]
    intro _ ha h; cases ha
    exact la_nodup.head h.1
Proof state after:
no goals
Theorem: List.Nodup.product
Proof state before:
case nil
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
la_nodup : Nodup []
⊢ Nodup (List.product [] lb)
Tactic:
exact .nil
Proof state after:
no goals
Theorem: List.Nodup.product
Proof state before:
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
IH : Nodup la → Nodup (List.product la lb)
la_nodup : Nodup (a :: la)
⊢ Nodup (List.product (a :: la) lb)
Tactic:
specialize IH la_nodup.tail
Proof state after:
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.product (a :: la) lb)
Theorem: List.Nodup.product
Proof state before:
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.product (a :: la) lb)
Tactic:
conv =>
  arg 1
  dsimp [List.product, List.bind]
  change lb.map (Prod.mk a) ++ la.product lb
Proof state after:
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb ++ List.product la lb)
Theorem: List.Nodup.product
Proof state before:
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb ++ List.product la lb)
Tactic:
refine Nodup.append ?_ IH ?_
Proof state after:
case cons.refine_1
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb)

case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb
Theorem: List.Nodup.product
Proof state before:
case cons.refine_1
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb)

case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb
Tactic:
. apply lb_nodup.map
  intro b₁ b₂; exact congrArg Prod.snd
Proof state after:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb
Theorem: List.Nodup.product
Proof state before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb
Tactic:
. intro x
  let ⟨_,b⟩ := x
  simp only [mem_map, Prod.mk.injEq, exists_eq_right_right, and_imp, pair_mem_product]
  intro _ ha h; cases ha
  exact la_nodup.head h.1
Proof state after:
no goals
Theorem: List.Nodup.product
Proof state before:
case cons.refine_1
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb)
Tactic:
apply lb_nodup.map
Proof state after:
case cons.refine_1.hf
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a₁ a₂ : β), (a, a₁) = (a, a₂) → a₁ = a₂
Theorem: List.Nodup.product
Proof state before:
case cons.refine_1.hf
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a₁ a₂ : β), (a, a₁) = (a, a₂) → a₁ = a₂
Tactic:
intro b₁ b₂
Proof state after:
case cons.refine_1.hf
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
b₁ b₂ : β
⊢ (a, b₁) = (a, b₂) → b₁ = b₂
Theorem: List.Nodup.product
Proof state before:
case cons.refine_1.hf
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
b₁ b₂ : β
⊢ (a, b₁) = (a, b₂) → b₁ = b₂
Tactic:
exact congrArg Prod.snd
Proof state after:
no goals
Theorem: List.Nodup.product
Proof state before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb
Tactic:
intro x
Proof state after:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
⊢ x ∈ List.map (Prod.mk a) lb → ¬x ∈ List.product la lb
Theorem: List.Nodup.product
Proof state before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
⊢ x ∈ List.map (Prod.mk a) lb → ¬x ∈ List.product la lb
Tactic:
let ⟨_,b⟩ := x
Proof state after:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
⊢ (fst✝, b) ∈ List.map (Prod.mk a) lb → ¬(fst✝, b) ∈ List.product la lb
Theorem: List.Nodup.product
Proof state before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
⊢ (fst✝, b) ∈ List.map (Prod.mk a) lb → ¬(fst✝, b) ∈ List.product la lb
Tactic:
simp only [mem_map, Prod.mk.injEq, exists_eq_right_right, and_imp, pair_mem_product]
Proof state after:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
⊢ b ∈ lb → a = fst✝ → ¬(fst✝ ∈ la ∧ b ∈ lb)
Theorem: List.Nodup.product
Proof state before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
⊢ b ∈ lb → a = fst✝ → ¬(fst✝ ∈ la ∧ b ∈ lb)
Tactic:
intro _ ha h
Proof state after:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
a✝ : b ∈ lb
ha : a = fst✝
h : fst✝ ∈ la ∧ b ∈ lb
⊢ False
Theorem: List.Nodup.product
Proof state before:
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
fst✝ : α
b : β
a✝ : b ∈ lb
ha : a = fst✝
h : fst✝ ∈ la ∧ b ∈ lb
⊢ False
Tactic:
cases ha
Proof state after:
case cons.refine_2.refl
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
b : β
a✝ : b ∈ lb
h : a ∈ la ∧ b ∈ lb
⊢ False
Theorem: List.Nodup.product
Proof state before:
case cons.refine_2.refl
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
b : β
a✝ : b ∈ lb
h : a ∈ la ∧ b ∈ lb
⊢ False
Tactic:
exact la_nodup.head h.1
Proof state after:
no goals
Theorem: List.countP_erase_true
Proof state before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
ha : a ∈ []
⊢ countP p [] = countP p (List.erase [] a) + 1
Tactic:
cases ha
Proof state after:
no goals
Theorem: List.countP_erase_true
Proof state before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
⊢ countP p (a' :: l) = countP p (List.erase (a' :: l) a) + 1
Tactic:
rewrite [List.erase_cons]
Proof state after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a) + 1
Theorem: List.countP_erase_true
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : a' = a
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a) + 1
Tactic:
cases h
Proof state after:
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a :: l
⊢ countP p (a :: l) = countP p (if a = a then l else a :: List.erase l a) + 1
Theorem: List.countP_erase_true
Proof state before:
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a :: l
⊢ countP p (a :: l) = countP p (if a = a then l else a :: List.erase l a) + 1
Tactic:
simp only [if_pos, countP_cons, if_pos hp]
Proof state after:
no goals
Theorem: List.countP_erase_true
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a) + 1
Tactic:
simp only [countP_cons, if_neg h]
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ (countP p l + if p a' = true then 1 else 0) = (countP p (List.erase l a) + if p a' = true then 1 else 0) + 1
Theorem: List.countP_erase_true
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ (countP p l + if p a' = true then 1 else 0) = (countP p (List.erase l a) + if p a' = true then 1 else 0) + 1
Tactic:
rewrite [Nat.add_assoc, Nat.add_comm _ 1, ← Nat.add_assoc]
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ (countP p l + if p a' = true then 1 else 0) = countP p (List.erase l a) + 1 + if p a' = true then 1 else 0
Theorem: List.countP_erase_true
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ countP p l = countP p (List.erase l a) + 1
Tactic:
exact IH <| (mem_cons.mp ha).resolve_left (Ne.symm h)
Proof state after:
no goals
Theorem: List.countP_erase_false
Proof state before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
ha : a ∈ []
⊢ countP p [] = countP p (List.erase [] a)
Tactic:
cases ha
Proof state after:
no goals
Theorem: List.countP_erase_false
Proof state before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
ha : a ∈ a' :: l
⊢ countP p (a' :: l) = countP p (List.erase (a' :: l) a)
Tactic:
rewrite [List.erase_cons]
Proof state after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
ha : a ∈ a' :: l
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a)
Theorem: List.countP_erase_false
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
ha : a ∈ a' :: l
h : a' = a
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a)
Tactic:
cases h
Proof state after:
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
ha : a ∈ a :: l
⊢ countP p (a :: l) = countP p (if a = a then l else a :: List.erase l a)
Theorem: List.countP_erase_false
Proof state before:
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
ha : a ∈ a :: l
⊢ countP p (a :: l) = countP p (if a = a then l else a :: List.erase l a)
Tactic:
simp only [if_true, countP_cons, hp, if_neg, Nat.add_zero]
Proof state after:
no goals
Theorem: List.countP_erase_false
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
ha : a ∈ a' :: l
h : ¬a' = a
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a)
Tactic:
simp only [countP_cons, if_neg h]
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
ha : a ∈ a' :: l
h : ¬a' = a
⊢ (countP p l + if p a' = true then 1 else 0) = countP p (List.erase l a) + if p a' = true then 1 else 0
Theorem: List.countP_erase_false
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
ha : a ∈ a' :: l
h : ¬a' = a
⊢ countP p l = countP p (List.erase l a)
Tactic:
exact IH <| (mem_cons.mp ha).resolve_left (Ne.symm h)
Proof state after:
no goals
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
α : Type u
β : Type v
p : α → Bool
l : List α
hp : ∀ (a b : α), p a = true → p b = true → a = b
hl : Nodup l
⊢ countP p l ≤ 1
Tactic:
induction l with
| nil => exact .step .refl
| cons a l IH =>
  simp only [countP_cons]
  cases Nat.eq_or_lt_of_le (IH hl.tail) with
  | inl hone =>
    have ⟨b,hb⟩:= (countP_pos p).mp (trans Nat.zero_lt_one hone.symm)
    rewrite [hone, Nat.add_comm]
    apply Nat.succ_le_succ
    if hpa : p a = true then
      have : a = b := hp _ _ hpa hb.2
      cases this
      exact absurd hb.1 hl.head
    else
      rewrite [if_neg hpa]; exact .refl
  | inr hlt =>
    have := Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hlt)
    rewrite [this, Nat.zero_add]
    cases p a <;> decide
Proof state after:
no goals
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case nil
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
hl : Nodup []
⊢ countP p [] ≤ 1
Tactic:
exact .step .refl
Proof state after:
no goals
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case cons
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
⊢ countP p (a :: l) ≤ 1
Tactic:
simp only [countP_cons]
Proof state after:
case cons
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Theorem: List.countP_le_one_of_unique_nodup
Proof state before:
case cons
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Tactic:
cases Nat.eq_or_lt_of_le (IH hl.tail) with
| inl hone =>
  have ⟨b,hb⟩:= (countP_pos p).mp (trans Nat.zero_lt_one hone.symm)
  rewrite [hone, Nat.add_comm]
  apply Nat.succ_le_succ
  if hpa : p a = true then
    have : a = b := hp _ _ hpa hb.2
    cases this
    exact absurd hb.1 hl.head
  else
    rewrite [if_neg hpa]; exact .refl
| inr hlt =>
  have := Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hlt)
  rewrite [this, Nat.zero_add]
  cases p a <;> decide
Proof state after:
no goals