internlm/Lean-Github huggingface dataset:
Theorem: List.mem_map
Proof state before:
case mp.tail.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h' : Mem b (map f xs)
a : α
ha : a ∈ xs ∧ f a = b
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
exact Exists.intro a (And.intro (Mem.tail _ ha.left) ha.right)
Proof state after:
no goals
Theorem: List.mem_map
Proof state before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h : ∃ a, a ∈ x :: xs ∧ f a = b
⊢ b ∈ map f (x :: xs)
Theorem: List.mem_map
Proof state before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h : ∃ a, a ∈ x :: xs ∧ f a = b
⊢ b ∈ map f (x :: xs)
Tactic:
cases h with | intro a ha =>
simp only [map]
cases ha.left with
| head => rw [ha.right]; constructor
| tail x h' =>
  have h_in_tail := ih.mpr (Exists.intro a ⟨h', ha.right⟩)
  exact Mem.tail _ h_in_tail
Proof state after:
no goals
Theorem: List.mem_map
Proof state before:
case mpr.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
⊢ b ∈ map f (x :: xs)
Tactic:
simp only [map]
Proof state after:
case mpr.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
⊢ b ∈ f x :: map f xs
Theorem: List.mem_map
Proof state before:
case mpr.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
⊢ b ∈ f x :: map f xs
Tactic:
cases ha.left with
| head => rw [ha.right]; constructor
| tail x h' =>
  have h_in_tail := ih.mpr (Exists.intro a ⟨h', ha.right⟩)
  exact Mem.tail _ h_in_tail
Proof state after:
no goals
Theorem: List.mem_map
Proof state before:
case mpr.intro.head
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
ha : x ∈ x :: xs ∧ f x = b
⊢ b ∈ f x :: map f xs
Tactic:
rw [ha.right]
Proof state after:
case mpr.intro.head
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
ha : x ∈ x :: xs ∧ f x = b
⊢ b ∈ b :: map f xs
Theorem: List.mem_map
Proof state before:
case mpr.intro.head
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
ha : x ∈ x :: xs ∧ f x = b
⊢ b ∈ b :: map f xs
Tactic:
constructor
Proof state after:
no goals
Theorem: List.mem_map
Proof state before:
case mpr.intro.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
h' : Mem a xs
⊢ b ∈ f x :: map f xs
Tactic:
have h_in_tail := ih.mpr (Exists.intro a ⟨h', ha.right⟩)
Proof state after:
case mpr.intro.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
h' : Mem a xs
h_in_tail : b ∈ map f xs
⊢ b ∈ f x :: map f xs
Theorem: List.mem_map
Proof state before:
case mpr.intro.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
h' : Mem a xs
h_in_tail : b ∈ map f xs
⊢ b ∈ f x :: map f xs
Tactic:
exact Mem.tail _ h_in_tail
Proof state after:
no goals
Theorem: List.map_fst_incrCounts_eq_map_fst
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
snd✝ : Nat
as : List (α × Nat)
⊢ map Prod.fst (incrCounts ((x, snd✝) :: as) x) = map Prod.fst ((x, snd✝) :: as)
Tactic:
simp only [map, incrCounts]
Proof state after:
no goals
Theorem: List.map_fst_incrCounts_eq_map_fst
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
h' : Mem x (map Prod.fst as)
ih : map Prod.fst (incrCounts as x) = map Prod.fst as
heq : a.fst = x
⊢ map Prod.fst (incrCounts (a :: as) x) = map Prod.fst (a :: as)
Tactic:
simp only [map, incrCounts, heq, ite_true, map]
Proof state after:
no goals
Theorem: List.map_fst_incrCounts_eq_map_fst
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
h' : Mem x (map Prod.fst as)
ih : map Prod.fst (incrCounts as x) = map Prod.fst as
hneq : ¬a.fst = x
⊢ map Prod.fst (incrCounts (a :: as) x) = map Prod.fst (a :: as)
Tactic:
simp only [hneq, ite_false, map, incrCounts]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
h' : Mem x (map Prod.fst as)
ih : map Prod.fst (incrCounts as x) = map Prod.fst as
hneq : ¬a.fst = x
⊢ a.fst :: map Prod.fst (incrCounts as x) = a.fst :: map Prod.fst as
Theorem: List.map_fst_incrCounts_eq_map_fst
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
h' : Mem x (map Prod.fst as)
ih : map Prod.fst (incrCounts as x) = map Prod.fst as
hneq : ¬a.fst = x
⊢ a.fst :: map Prod.fst (incrCounts as x) = a.fst :: map Prod.fst as
Tactic:
exact congrArg _ ih
Proof state after:
no goals
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ ∀ (as : List (α × Nat)), ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
Tactic:
intros as h
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
as : List (α × Nat)
h : ¬x ∈ map Prod.fst as
⊢ map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
as : List (α × Nat)
h : ¬x ∈ map Prod.fst as
⊢ map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
Tactic:
induction as with
| nil =>
  simp only [incrCounts, map, HAppend.hAppend, Append.append, List.append]
| cons a as ih =>
  simp only [map, incrCounts]
  cases Decidable.em (a.1 = x) with
  | inl heq =>
    apply absurd h
    apply not_not
    simp only [map, heq]
    apply List.Mem.head
  | inr hneq =>
    simp only [hneq, ite_false, map]
    apply congrArg
    apply ih
    . intros hneg
      apply h
      apply List.Mem.tail _ hneg
Proof state after:
no goals
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : ¬x ∈ map Prod.fst []
⊢ map Prod.fst (incrCounts [] x) = map Prod.fst [] ++ [x]
Tactic:
simp only [incrCounts, map, HAppend.hAppend, Append.append, List.append]
Proof state after:
no goals
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
⊢ map Prod.fst (incrCounts (a :: as) x) = map Prod.fst (a :: as) ++ [x]
Tactic:
simp only [map, incrCounts]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
⊢ map Prod.fst (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) =
    a.fst :: map Prod.fst as ++ [x]
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
⊢ map Prod.fst (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) =
    a.fst :: map Prod.fst as ++ [x]
Tactic:
cases Decidable.em (a.1 = x) with
| inl heq =>
  apply absurd h
  apply not_not
  simp only [map, heq]
  apply List.Mem.head
| inr hneq =>
  simp only [hneq, ite_false, map]
  apply congrArg
  apply ih
  . intros hneg
    apply h
    apply List.Mem.tail _ hneg
Proof state after:
no goals
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ map Prod.fst (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) =
    a.fst :: map Prod.fst as ++ [x]
Tactic:
apply absurd h
Proof state after:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ ¬¬x ∈ map Prod.fst (a :: as)
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ ¬¬x ∈ map Prod.fst (a :: as)
Tactic:
apply not_not
Proof state after:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ x ∈ map Prod.fst (a :: as)
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ x ∈ map Prod.fst (a :: as)
Tactic:
simp only [map, heq]
Proof state after:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ x ∈ x :: map Prod.fst as
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ x ∈ x :: map Prod.fst as
Tactic:
apply List.Mem.head
Proof state after:
no goals
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ map Prod.fst (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) =
    a.fst :: map Prod.fst as ++ [x]
Tactic:
simp only [hneq, ite_false, map]
Proof state after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ a.fst :: map Prod.fst (incrCounts as x) = a.fst :: map Prod.fst as ++ [x]
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ a.fst :: map Prod.fst (incrCounts as x) = a.fst :: map Prod.fst as ++ [x]
Tactic:
apply congrArg
Proof state after:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ map Prod.fst (incrCounts as x) = List.append (map Prod.fst as) [x]
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ map Prod.fst (incrCounts as x) = List.append (map Prod.fst as) [x]
Tactic:
apply ih
Proof state after:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ ¬x ∈ map Prod.fst as
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ ¬x ∈ map Prod.fst as
Tactic:
. intros hneg
  apply h
  apply List.Mem.tail _ hneg
Proof state after:
no goals
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ ¬x ∈ map Prod.fst as
Tactic:
intros hneg
Proof state after:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
hneg : x ∈ map Prod.fst as
⊢ False
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
hneg : x ∈ map Prod.fst as
⊢ False
Tactic:
apply h
Proof state after:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
hneg : x ∈ map Prod.fst as
⊢ x ∈ map Prod.fst (a :: as)
Theorem: List.map_fst_incrCounts_eq_cons_fst
Proof state before:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
hneg : x ∈ map Prod.fst as
⊢ x ∈ map Prod.fst (a :: as)
Tactic:
apply List.Mem.tail _ hneg
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ∨ x ∈ ys ↔ x ∈ xs ++ ys
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ∨ x ∈ ys → x ∈ xs ++ ys

case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
Theorem: List.mem_append_iff
Proof state before:
case mp
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ∨ x ∈ ys → x ∈ xs ++ ys

case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
Tactic:
. intros hf
  cases hf with
  | inl hxs => apply mem_append_front _ _ _ hxs
  | inr hys => apply mem_append_back _ _ _ hys
Proof state after:
case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
Theorem: List.mem_append_iff
Proof state before:
case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
Tactic:
. intros hb
  induction xs with
  | nil => exact Or.intro_right _ hb
  | cons z xs ih =>
    cases hb with
    | head _ => apply Or.intro_left _ (List.Mem.head _)
    | tail _ h' =>
      cases ys with
      | nil =>
        apply Or.intro_left
        apply List.Mem.tail
        simp at h'
        exact h'
      | cons y ys =>
        simp at h'
        cases ih h' with
        | inl hxxs =>
          apply Or.intro_left
          exact List.Mem.tail _ hxxs
        | inr hxys =>
          exact Or.intro_right _ hxys
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mp
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ∨ x ∈ ys → x ∈ xs ++ ys
Tactic:
intros hf
Proof state after:
case mp
α : Type u_1
x : α
xs ys : List α
hf : x ∈ xs ∨ x ∈ ys
⊢ x ∈ xs ++ ys
Theorem: List.mem_append_iff
Proof state before:
case mp
α : Type u_1
x : α
xs ys : List α
hf : x ∈ xs ∨ x ∈ ys
⊢ x ∈ xs ++ ys
Tactic:
cases hf with
| inl hxs => apply mem_append_front _ _ _ hxs
| inr hys => apply mem_append_back _ _ _ hys
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mp.inl
α : Type u_1
x : α
xs ys : List α
hxs : x ∈ xs
⊢ x ∈ xs ++ ys
Tactic:
apply mem_append_front _ _ _ hxs
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mp.inr
α : Type u_1
x : α
xs ys : List α
hys : x ∈ ys
⊢ x ∈ xs ++ ys
Tactic:
apply mem_append_back _ _ _ hys
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
Tactic:
intros hb
Proof state after:
case mpr
α : Type u_1
x : α
xs ys : List α
hb : x ∈ xs ++ ys
⊢ x ∈ xs ∨ x ∈ ys
Theorem: List.mem_append_iff
Proof state before:
case mpr
α : Type u_1
x : α
xs ys : List α
hb : x ∈ xs ++ ys
⊢ x ∈ xs ∨ x ∈ ys
Tactic:
induction xs with
| nil => exact Or.intro_right _ hb
| cons z xs ih =>
  cases hb with
  | head _ => apply Or.intro_left _ (List.Mem.head _)
  | tail _ h' =>
    cases ys with
    | nil =>
      apply Or.intro_left
      apply List.Mem.tail
      simp at h'
      exact h'
    | cons y ys =>
      simp at h'
      cases ih h' with
      | inl hxxs =>
        apply Or.intro_left
        exact List.Mem.tail _ hxxs
      | inr hxys =>
        exact Or.intro_right _ hxys
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mpr.nil
α : Type u_1
x : α
ys : List α
hb : x ∈ [] ++ ys
⊢ x ∈ [] ∨ x ∈ ys
Tactic:
exact Or.intro_right _ hb
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons
α : Type u_1
x : α
ys : List α
z : α
xs : List α
ih : x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
hb : x ∈ z :: xs ++ ys
⊢ x ∈ z :: xs ∨ x ∈ ys
Tactic:
cases hb with
| head _ => apply Or.intro_left _ (List.Mem.head _)
| tail _ h' =>
  cases ys with
  | nil =>
    apply Or.intro_left
    apply List.Mem.tail
    simp at h'
    exact h'
  | cons y ys =>
    simp at h'
    cases ih h' with
    | inl hxxs =>
      apply Or.intro_left
      exact List.Mem.tail _ hxxs
    | inr hxys =>
      exact Or.intro_right _ hxys
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.head
α : Type u_1
x : α
ys xs : List α
ih : x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
⊢ x ∈ x :: xs ∨ x ∈ ys
Tactic:
apply Or.intro_left _ (List.Mem.head _)
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.tail
α : Type u_1
x : α
ys : List α
z : α
xs : List α
ih : x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
h' : Mem x (List.append xs ys)
⊢ x ∈ z :: xs ∨ x ∈ ys
Tactic:
cases ys with
| nil =>
  apply Or.intro_left
  apply List.Mem.tail
  simp at h'
  exact h'
| cons y ys =>
  simp at h'
  cases ih h' with
  | inl hxxs =>
    apply Or.intro_left
    exact List.Mem.tail _ hxxs
  | inr hxys =>
    exact Or.intro_right _ hxys
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.tail.nil
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ x ∈ z :: xs ∨ x ∈ []
Tactic:
apply Or.intro_left
Proof state after:
case mpr.cons.tail.nil.h
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ x ∈ z :: xs
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.tail.nil.h
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ x ∈ z :: xs
Tactic:
apply List.Mem.tail
Proof state after:
case mpr.cons.tail.nil.h.a
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ Mem x xs
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.tail.nil.h.a
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ Mem x xs
Tactic:
simp at h'
Proof state after:
case mpr.cons.tail.nil.h.a
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x xs
⊢ Mem x xs
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.tail.nil.h.a
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x xs
⊢ Mem x xs
Tactic:
exact h'
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.tail.cons
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (List.append xs (y :: ys))
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
Tactic:
simp at h'
Proof state after:
case mpr.cons.tail.cons
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.tail.cons
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
Tactic:
cases ih h' with
| inl hxxs =>
  apply Or.intro_left
  exact List.Mem.tail _ hxxs
| inr hxys =>
  exact Or.intro_right _ hxys
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.tail.cons.inl
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
hxxs : x ∈ xs
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
Tactic:
apply Or.intro_left
Proof state after:
case mpr.cons.tail.cons.inl.h
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
hxxs : x ∈ xs
⊢ x ∈ z :: xs
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.tail.cons.inl.h
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
hxxs : x ∈ xs
⊢ x ∈ z :: xs
Tactic:
exact List.Mem.tail _ hxxs
Proof state after:
no goals
Theorem: List.mem_append_iff
Proof state before:
case mpr.cons.tail.cons.inr
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
hxys : x ∈ y :: ys
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
Tactic:
exact Or.intro_right _ hxys
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x y : α
as xs cs : List α
⊢ length (uniqueAux xs (cs ++ x :: (as ++ [y]))) = length (uniqueAux xs (cs ++ y :: x :: as))
Tactic:
induction xs generalizing cs with
| nil =>
  simp [uniqueAux]
  rw [←Nat.add_one,
      Nat.add_assoc,
      Nat.add_comm (length cs),
      ←Nat.add_assoc]
| cons z zs ih =>
  have rearrange_mem :
    (z ∈ cs ++ x :: (as ++ [y])) ↔ (z ∈ cs ++ y :: x :: as) := by
    apply Iff.intro
    . intros h
      cases mem_append_iff.mpr h with
      | inl hcs => exact List.mem_append_front _ _ _ hcs
      | inr hcons =>
        apply List.mem_append_back
        rw [←cons_append] at hcons
        cases mem_append_iff.mpr hcons with
        | inl hxas => exact List.Mem.tail _ hxas
        | inr hy =>
          cases hy with
          | tail _ _ => contradiction
          | head _ => exact List.Mem.head _
    . intros h
      cases mem_append_iff.mpr h with
      | inl hcs => exact List.mem_append_front _ _ _ hcs
      | inr hcons =>
        apply List.mem_append_back
        cases hcons with
        | head _ =>
          apply List.Mem.tail
          apply List.mem_append_back
          apply (List.mem_singleton_iff y y).mpr rfl
        | tail _ hcons' =>
          rw [←cons_append]
          exact List.mem_append_front _ _ _ hcons'
  simp only [uniqueAux]
  cases Decidable.em (z ∈ cs ++ x :: (as ++ [y])) with
  | inl hin =>
    simp only [hin, rearrange_mem.mp hin, ite_true]
    apply ih
  | inr hout =>
    simp only [hout, rearrange_mem.not_iff_not_of_iff.mp hout, ite_false]
    have rw_help (stuff) : (z :: (cs ++ stuff)) = ((z :: cs) ++ stuff) := rfl
    rw [rw_help, rw_help]
    apply ih
Proof state after:
no goals