internlm/Lean-Github huggingface dataset:
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons
α : Type u
β : Type v
a : α
l : List α
i j : Nat
hi : i < length (a :: l)
hj : j < length (a :: l)
h : (a :: l)[i] = (a :: l)[j]
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
⊢ i = j
Tactic:
cases i <;> cases j <;> dsimp at h
Proof state after:
case cons.cons.zero.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi hj : Nat.zero < length (a :: l)
h : a = a
⊢ Nat.zero = Nat.zero

case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝

case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.zero.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi hj : Nat.zero < length (a :: l)
h : a = a
⊢ Nat.zero = Nat.zero

case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝

case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Tactic:
. rfl
Proof state after:
case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝

case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝

case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Tactic:
. exfalso
  suffices a ∈ l from ha a this rfl
  exact List.mem_iff_get.mpr ⟨_, h.symm⟩
Proof state after:
case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Tactic:
. exfalso
  suffices a ∈ l from ha a this rfl
  exact List.mem_iff_get.mpr ⟨_, h⟩
Proof state after:
case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Tactic:
. exact congrArg Nat.succ <| IH _ _ h
Proof state after:
no goals
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.zero.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi hj : Nat.zero < length (a :: l)
h : a = a
⊢ Nat.zero = Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝
Tactic:
exfalso
Proof state after:
case cons.cons.zero.succ.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ False
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.zero.succ.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ False
Tactic:
suffices a ∈ l from ha a this rfl
Proof state after:
case cons.cons.zero.succ.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ a ∈ l
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.zero.succ.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ a ∈ l
Tactic:
exact List.mem_iff_get.mpr ⟨_, h.symm⟩
Proof state after:
no goals
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero
Tactic:
exfalso
Proof state after:
case cons.cons.succ.zero.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ False
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.succ.zero.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ False
Tactic:
suffices a ∈ l from ha a this rfl
Proof state after:
case cons.cons.succ.zero.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ a ∈ l
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.succ.zero.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ a ∈ l
Tactic:
exact List.mem_iff_get.mpr ⟨_, h⟩
Proof state after:
no goals
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Tactic:
exact congrArg Nat.succ <| IH _ _ h
Proof state after:
no goals
Theorem: List.Nodup.filter
Proof state before:
α : Type u
β : Type v
l : List α
nodup : Nodup l
p : α → Bool
⊢ Nodup (List.filter p l)
Tactic:
induction l with
| nil => exact .nil
| cons a l IH =>
  specialize IH nodup.tail
  dsimp [List.filter]
  cases p a <;> dsimp
  . exact IH
  . refine nodup_cons_of_notmem_nodup _ ?_ IH
    intro ha
    exact nodup.head <| l.filter_sublist.subset ha
Proof state after:
no goals
Theorem: List.Nodup.filter
Proof state before:
case nil
α : Type u
β : Type v
p : α → Bool
nodup : Nodup []
⊢ Nodup (List.filter p [])
Tactic:
exact .nil
Proof state after:
no goals
Theorem: List.Nodup.filter
Proof state before:
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
IH : Nodup l → Nodup (List.filter p l)
nodup : Nodup (a :: l)
⊢ Nodup (List.filter p (a :: l))
Tactic:
specialize IH nodup.tail
Proof state after:
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p (a :: l))
Theorem: List.Nodup.filter
Proof state before:
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p (a :: l))
Tactic:
dsimp [List.filter]
Proof state after:
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup
    (match p a with
    | true => a :: List.filter p l
    | false => List.filter p l)
Theorem: List.Nodup.filter
Proof state before:
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup
    (match p a with
    | true => a :: List.filter p l
    | false => List.filter p l)
Tactic:
cases p a <;> dsimp
Proof state after:
case cons.false
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p l)

case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)
Theorem: List.Nodup.filter
Proof state before:
case cons.false
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p l)

case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)
Tactic:
. exact IH
Proof state after:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)
Theorem: List.Nodup.filter
Proof state before:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)
Tactic:
. refine nodup_cons_of_notmem_nodup _ ?_ IH
  intro ha
  exact nodup.head <| l.filter_sublist.subset ha
Proof state after:
no goals
Theorem: List.Nodup.filter
Proof state before:
case cons.false
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p l)
Tactic:
exact IH
Proof state after:
no goals
Theorem: List.Nodup.filter
Proof state before:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)
Tactic:
refine nodup_cons_of_notmem_nodup _ ?_ IH
Proof state after:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ ¬a ∈ List.filter p l
Theorem: List.Nodup.filter
Proof state before:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ ¬a ∈ List.filter p l
Tactic:
intro ha
Proof state after:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
ha : a ∈ List.filter p l
⊢ False
Theorem: List.Nodup.filter
Proof state before:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
ha : a ∈ List.filter p l
⊢ False
Tactic:
exact nodup.head <| l.filter_sublist.subset ha
Proof state after:
no goals
Theorem: List.Nodup.map
Proof state before:
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ Nodup (List.map f l)
Tactic:
apply nodup_of_get_inj
Proof state after:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ ∀ (i j : Nat) (x : i < length (List.map f l)) (x_1 : j < length (List.map f l)),
    (List.map f l)[i] = (List.map f l)[j] → i = j
Theorem: List.Nodup.map
Proof state before:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ ∀ (i j : Nat) (x : i < length (List.map f l)) (x_1 : j < length (List.map f l)),
    (List.map f l)[i] = (List.map f l)[j] → i = j
Tactic:
intro i j hi hj
Proof state after:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
⊢ (List.map f l)[i] = (List.map f l)[j] → i = j
Theorem: List.Nodup.map
Proof state before:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
⊢ (List.map f l)[i] = (List.map f l)[j] → i = j
Tactic:
simp only [getElem_eq_get, get_map]
Proof state after:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
⊢ f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
      f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) }) →
    i = j
Theorem: List.Nodup.map
Proof state before:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
⊢ f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
      f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) }) →
    i = j
Tactic:
intro hfij
Proof state after:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
hfij :
  f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
    f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) })
⊢ i = j
Theorem: List.Nodup.map
Proof state before:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
hfij :
  f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
    f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) })
⊢ i = j
Tactic:
specialize hf _ _ hfij
Proof state after:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
hfij :
  f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
    f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) })
hf :
  get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) } =
    get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) }
⊢ i = j
Theorem: List.Nodup.map
Proof state before:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
hfij :
  f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
    f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) })
hf :
  get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) } =
    get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) }
⊢ i = j
Tactic:
exact nodup.get_inj i j hf
Proof state after:
no goals
Theorem: List.Nodup.pmap
Proof state before:
α : 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₂
⊢ Nodup (List.pmap f l h)
Tactic:
apply nodup_of_get_inj
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) (x : i < length (List.pmap f l h)) (x_1 : j < length (List.pmap f l h)),
    (List.pmap f l h)[i] = (List.pmap f l h)[j] → 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) (x : i < length (List.pmap f l h)) (x_1 : j < length (List.pmap f l h)),
    (List.pmap f l h)[i] = (List.pmap f l h)[j] → i = j
Tactic:
intro i j hi hj
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)
⊢ (List.pmap f l h)[i] = (List.pmap f l h)[j] → i = j