Theorem: List.countP_le_one_of_unique_nodup (Fifteen/Data/List/Basic.lean)

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
State after:
no goals

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
State after:
no goals

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]
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

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
State after:
no goals

State before:
case cons.inl
α : 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)
hone : countP p l = 1
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Tactic:
have ⟨b,hb⟩:= (countP_pos p).mp (trans Nat.zero_lt_one hone.symm)
State after:
case cons.inl
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1

State before:
case cons.inl
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Tactic:
rewrite [hone, Nat.add_comm]
State after:
case cons.inl
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (if p a = true then 1 else 0) + 1 ≤ 1

State before:
case cons.inl
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (if p a = true then 1 else 0) + 1 ≤ 1
Tactic:
apply Nat.succ_le_succ
State after:
case cons.inl.a
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (if p a = true then 1 else 0) ≤ 0

State before:
case cons.inl.a
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (if p a = true then 1 else 0) ≤ 0
Tactic:
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
State after:
no goals

State before:
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : p a = true
⊢ (if p a = true then 1 else 0) ≤ 0
Tactic:
have : a = b := hp _ _ hpa hb.2
State after:
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : p a = true
this : a = b
⊢ (if p a = true then 1 else 0) ≤ 0

State before:
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : p a = true
this : a = b
⊢ (if p a = true then 1 else 0) ≤ 0
Tactic:
cases this
State after:
case refl
α : 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)
hone : countP p l = 1
hpa : p a = true
hb : a ∈ l ∧ p a = true
⊢ (if p a = true then 1 else 0) ≤ 0

State before:
case refl
α : 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)
hone : countP p l = 1
hpa : p a = true
hb : a ∈ l ∧ p a = true
⊢ (if p a = true then 1 else 0) ≤ 0
Tactic:
exact absurd hb.1 hl.head
State after:
no goals

State before:
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : ¬p a = true
⊢ (if p a = true then 1 else 0) ≤ 0
Tactic:
rewrite [if_neg hpa]
State after:
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : ¬p a = true
⊢ 0 ≤ 0

State before:
α : 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)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
hpa : ¬p a = true
⊢ 0 ≤ 0
Tactic:
exact .refl
State after:
no goals

State before:
case cons.inr
α : 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)
hlt : countP p l < 1
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Tactic:
have := Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hlt)
State after:
case cons.inr
α : 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)
hlt : countP p l < 1
this : countP p l = 0
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1

State before:
case cons.inr
α : 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)
hlt : countP p l < 1
this : countP p l = 0
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
Tactic:
rewrite [this, Nat.zero_add]
State after:
case cons.inr
α : 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)
hlt : countP p l < 1
this : countP p l = 0
⊢ (if p a = true then 1 else 0) ≤ 1

State before:
case cons.inr
α : 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)
hlt : countP p l < 1
this : countP p l = 0
⊢ (if p a = true then 1 else 0) ≤ 1
Tactic:
cases p a <;> decide
State after:
no goals