[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
⊢ foldl (argAux r) o [] = none ↔ [] = [] ∧ o = none
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (foldl (argAux r) o (tl ++ [hd]) = none ↔ tl ++ [hd] = [] ∧ o = none)
[PROOFSTEP]
simp [argAux]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd : α
⊢ (foldl (fun a b => Option.rec (some b) (fun val => if r b val then some b else some val) a) o tl = none ↔
      tl = [] ∧ o = none) →
    ¬Option.rec (some hd) (fun val => if r hd val then some hd else some val)
          (foldl (fun a b => Option.rec (some b) (fun val => if r b val then some b else some val) a) o tl) =
        none
[PROOFSTEP]
cases foldl (argAux r) o tl
[GOAL]
case none
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd : α
⊢ (none = none ↔ tl = [] ∧ o = none) →
    ¬Option.rec (some hd) (fun val => if r hd val then some hd else some val) none = none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    ¬Option.rec (some hd) (fun val => if r hd val then some hd else some val) (some val✝) = none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd val✝ : α
⊢ (tl = [] → ¬o = none) → ¬(if r hd val✝ then some hd else some val✝) = none
[PROOFSTEP]
try split_ifs <;> simp
[GOAL]
case some
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd val✝ : α
⊢ (tl = [] → ¬o = none) → ¬(if r hd val✝ then some hd else some val✝) = none
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd val✝ : α
h✝ : r hd val✝
⊢ (tl = [] → ¬o = none) → ¬False
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd val✝ : α
h✝ : ¬r hd val✝
⊢ (tl = [] → ¬o = none) → ¬False
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a m : α
l : List α
⊢ ∀ (a m : α), m ∈ foldl (argAux r) (some a) [] → m ∈ [a]
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a m : α
l : List α
⊢ ∀ (l : List α) (a : α),
    (∀ (a m : α), m ∈ foldl (argAux r) (some a) l → m ∈ a :: l) →
      ∀ (a_2 m : α), m ∈ foldl (argAux r) (some a_2) (l ++ [a]) → m ∈ a_2 :: (l ++ [a])
[PROOFSTEP]
intro tl hd ih a m
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m : α
⊢ m ∈ foldl (argAux r) (some a) (tl ++ [hd]) → m ∈ a :: (tl ++ [hd])
[PROOFSTEP]
simp only [foldl_append, foldl_cons, foldl_nil, argAux]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m : α
⊢ m ∈
      Option.rec (some hd) (fun val => if r hd val then some hd else some val)
        (foldl (fun a b => Option.rec (some b) (fun val => if r b val then some b else some val) a) (some a) tl) →
    m ∈ a :: (tl ++ [hd])
[PROOFSTEP]
cases hf : foldl (argAux r) (some a) tl
[GOAL]
case none
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m : α
hf : foldl (argAux r) (some a) tl = none
⊢ m ∈ Option.rec (some hd) (fun val => if r hd val then some hd else some val) none → m ∈ a :: (tl ++ [hd])
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
case some
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
⊢ m ∈ Option.rec (some hd) (fun val => if r hd val then some hd else some val) (some val✝) → m ∈ a :: (tl ++ [hd])
[PROOFSTEP]
dsimp only
[GOAL]
case some
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
⊢ (m ∈ if r hd val✝ then some hd else some val✝) → m ∈ a :: (tl ++ [hd])
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : r hd val✝
⊢ m ∈ some hd → m ∈ a :: (tl ++ [hd])
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
case neg
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : ¬r hd val✝
⊢ m ∈ some val✝ → m ∈ a :: (tl ++ [hd])
[PROOFSTEP]
simp only [List.mem_cons] at ih
[GOAL]
case neg
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
l tl : List α
hd a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : ¬r hd val✝
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m = a ∨ m ∈ tl
⊢ m ∈ some val✝ → m ∈ a :: (tl ++ [hd])
[PROOFSTEP]
rcases ih _ _ hf with rfl | H
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a m✝ : α
l tl : List α
hd m val✝ : α
h✝ : ¬r hd val✝
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m = a ∨ m ∈ tl
hf : foldl (argAux r) (some val✝) tl = some val✝
⊢ m ∈ some val✝ → m ∈ val✝ :: (tl ++ [hd])
[PROOFSTEP]
simp (config := { contextual := true }) only [Option.mem_def, Option.some.injEq, find?, eq_comm, mem_cons, mem_append,
  mem_singleton, true_or, implies_true]
[GOAL]
case neg.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
l tl : List α
hd a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : ¬r hd val✝
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m = a ∨ m ∈ tl
H : val✝ ∈ tl
⊢ m ∈ some val✝ → m ∈ a :: (tl ++ [hd])
[PROOFSTEP]
simp (config := { contextual := true }) [@eq_comm _ _ m, H]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
hr₀ : Irreflexive r
hr₁ : Transitive r
⊢ ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m
[PROOFSTEP]
induction' l using List.reverseRecOn with tl a ih
[GOAL]
case H0
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
hr₀ : Irreflexive r
hr₁ : Transitive r
⊢ ∀ {a m : α} {o : Option α}, a ∈ [] → m ∈ foldl (argAux r) o [] → ¬r a m
[PROOFSTEP]
simp
[GOAL]
case H1
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a✝ m : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
⊢ ∀ {a_1 m : α} {o : Option α}, a_1 ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r a_1 m
[PROOFSTEP]
intro b m o hb ho
[GOAL]
case H1
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ foldl (argAux r) o (tl ++ [a])
⊢ ¬r b m
[PROOFSTEP]
rw [foldl_append, foldl_cons, foldl_nil, argAux] at ho
[GOAL]
case H1
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c => if r a c then some a else some c
⊢ ¬r b m
[PROOFSTEP]
cases' hf : foldl (argAux r) o tl with c
[GOAL]
case H1.none
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c => if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m
[PROOFSTEP]
rw [hf] at ho
[GOAL]
case H1.none
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn none (some a) fun c => if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m
[PROOFSTEP]
rw [foldl_argAux_eq_none] at hf
[GOAL]
case H1.none
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn none (some a) fun c => if r a c then some a else some c
hf : tl = [] ∧ o = none
⊢ ¬r b m
[PROOFSTEP]
simp_all [hf.1, hf.2, hr₀ _]
[GOAL]
case H1.some
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c => if r a c then some a else some c
c : α
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m
[PROOFSTEP]
rw [hf, Option.mem_def] at ho
[GOAL]
case H1.some
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
ho : (Option.casesOn (some c) (some a) fun c => if r a c then some a else some c) = some m
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m
[PROOFSTEP]
dsimp only at ho
[GOAL]
case H1.some
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
ho : (if r a c then some a else some c) = some m
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m
[PROOFSTEP]
split_ifs at ho  with hac
[GOAL]
case pos
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : r a c
ho : some a = some m
⊢ ¬r b m
[PROOFSTEP]
cases' mem_append.1 hb with h h
[GOAL]
case neg
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : ¬r a c
ho : some c = some m
⊢ ¬r b m
[PROOFSTEP]
cases' mem_append.1 hb with h h
[GOAL]
case pos.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : r a c
ho : some a = some m
h : b ∈ tl
⊢ ¬r b m
[PROOFSTEP]
injection ho with ho
[GOAL]
case pos.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : r a c
ho : some a = some m
h : b ∈ [a]
⊢ ¬r b m
[PROOFSTEP]
injection ho with ho
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : ¬r a c
ho : some c = some m
h : b ∈ tl
⊢ ¬r b m
[PROOFSTEP]
injection ho with ho
[GOAL]
case neg.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : ¬r a c
ho : some c = some m
h : b ∈ [a]
⊢ ¬r b m
[PROOFSTEP]
injection ho with ho
[GOAL]
case pos.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : r a c
h : b ∈ tl
ho : a = m
⊢ ¬r b m
[PROOFSTEP]
subst ho
[GOAL]
case pos.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : r a c
h : b ∈ [a]
ho : a = m
⊢ ¬r b m
[PROOFSTEP]
subst ho
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : ¬r a c
h : b ∈ tl
ho : c = m
⊢ ¬r b m
[PROOFSTEP]
subst ho
[GOAL]
case neg.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m✝ : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : ¬r a c
h : b ∈ [a]
ho : c = m
⊢ ¬r b m
[PROOFSTEP]
subst ho
[GOAL]
case pos.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : r a c
h : b ∈ tl
⊢ ¬r b a
[PROOFSTEP]
exact fun hba => ih h hf (hr₁ hba hac)
[GOAL]
case pos.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : r a c
h : b ∈ [a]
⊢ ¬r b a
[PROOFSTEP]
simp_all [hr₀ _]
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : ¬r a c
h : b ∈ tl
⊢ ¬r b c
[PROOFSTEP]
exact ih h hf
[GOAL]
case neg.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o✝ : Option α
a✝ m : α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : ¬r a c
h : b ∈ [a]
⊢ ¬r b c
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x x_1 => x < x_1
f✝ : α → β
l✝ : List α
o : Option α
a✝ m : α
f : α → β
a : α
l : List α
⊢ argmax f (l ++ [a]) = Option.casesOn (argmax f l) (some a) fun c => if f c < f a then some a else some c
[PROOFSTEP]
rw [argmax, argmax]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x x_1 => x < x_1
f✝ : α → β
l✝ : List α
o : Option α
a✝ m : α
f : α → β
a : α
l : List α
⊢ foldl (argAux fun b c => f c < f b) none (l ++ [a]) =
    Option.casesOn (foldl (argAux fun b c => f c < f b) none l) (some a) fun c => if f c < f a then some a else some c
[PROOFSTEP]
simp [argAux]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x x_1 => x < x_1
f : α → β
l : List α
o : Option α
a m✝ m : α
⊢ m ∈ argmax f [] → m ∈ []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x x_1 => x < x_1
f : α → β
l : List α
o : Option α
a m✝ hd : α
tl : List α
m : α
⊢ m ∈ argmax f (hd :: tl) → m ∈ hd :: tl
[PROOFSTEP]
simpa [argmax, argAux] using foldl_argAux_mem _ tl hd m
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x x_1 => x < x_1
f : α → β
l : List α
o : Option α
a m : α
⊢ argmax f l = none ↔ l = []
[PROOFSTEP]
simp [argmax]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
⊢ argmax f (a :: (hd ++ [tl])) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c => if f a < f c then some c else some a
[PROOFSTEP]
rw [← cons_append, argmax_concat, ih, argmax_concat]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
⊢ (Option.casesOn (Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a) (some tl)
      fun c => if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn (argmax f hd) (some tl) fun c => if f c < f tl then some tl else some c) (some a)
      fun c => if f a < f c then some c else some a
[PROOFSTEP]
cases' h : argmax f hd with m
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
h : argmax f hd = none
⊢ (Option.casesOn (Option.casesOn none (some a) fun c => if f a < f c then some c else some a) (some tl) fun c =>
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn none (some tl) fun c => if f c < f tl then some tl else some c) (some a) fun c =>
      if f a < f c then some c else some a
[PROOFSTEP]
simp [h]
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ (Option.casesOn (Option.casesOn (some m) (some a) fun c => if f a < f c then some c else some a) (some tl) fun c =>
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn (some m) (some tl) fun c => if f c < f tl then some tl else some c) (some a) fun c =>
      if f a < f c then some c else some a
[PROOFSTEP]
dsimp
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ Option.rec (some tl) (fun val => if f val < f tl then some tl else some val) (if f a < f m then some m else some a) =
    Option.rec (some a) (fun val => if f a < f val then some val else some a) (if f m < f tl then some tl else some m)
[PROOFSTEP]
rw [← apply_ite, ← apply_ite]
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ Option.rec (some tl) (fun val => if f val < f tl then some tl else some val) (some (if f a < f m then m else a)) =
    Option.rec (some a) (fun val => if f a < f val then some val else some a) (some (if f m < f tl then tl else m))
[PROOFSTEP]
dsimp
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ (if f (if f a < f m then m else a) < f tl then some tl else some (if f a < f m then m else a)) =
    if f a < f (if f m < f tl then tl else m) then some (if f m < f tl then tl else m) else some a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : f a < f m
h✝¹ : f m < f tl
h✝ : f a < f tl
⊢ some tl = some tl
[PROOFSTEP]
try rfl
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : f a < f m
h✝¹ : f m < f tl
h✝ : f a < f tl
⊢ some tl = some tl
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : f a < f m
h✝¹ : f m < f tl
h✝ : ¬f a < f tl
⊢ some tl = some a
[PROOFSTEP]
try rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : f a < f m
h✝¹ : f m < f tl
h✝ : ¬f a < f tl
⊢ some tl = some a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝¹ : f a < f m
h✝ : ¬f m < f tl
⊢ some m = some m
[PROOFSTEP]
try rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝¹ : f a < f m
h✝ : ¬f m < f tl
⊢ some m = some m
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : f a < f tl
h✝ : f m < f tl
⊢ some tl = some tl
[PROOFSTEP]
try rfl
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : f a < f tl
h✝ : f m < f tl
⊢ some tl = some tl
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : f a < f tl
h✝ : ¬f m < f tl
⊢ some tl = some a
[PROOFSTEP]
try rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : f a < f tl
h✝ : ¬f m < f tl
⊢ some tl = some a
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : ¬f a < f tl
h✝ : f m < f tl
⊢ some a = some a
[PROOFSTEP]
try rfl
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : ¬f a < f tl
h✝ : f m < f tl
⊢ some a = some a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : ¬f a < f tl
h✝ : ¬f m < f tl
⊢ some a = some a
[PROOFSTEP]
try rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : ¬f a < f tl
h✝ : ¬f m < f tl
⊢ some a = some a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : f a < f m
h✝¹ : f m < f tl
h✝ : ¬f a < f tl
⊢ some tl = some a
[PROOFSTEP]
exact absurd (lt_trans ‹f a < f m› ‹_›) ‹_›
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : f a < f tl
h✝ : ¬f m < f tl
⊢ some tl = some a
[PROOFSTEP]
cases (‹f a < f tl›.lt_or_lt _).elim ‹_› ‹_›
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m✝ : α
inst✝ : DecidableEq α
m : α
x✝³ : m ∈ argmax f []
x✝² : α
x✝¹ : x✝² ∈ []
x✝ : f m ≤ f x✝²
⊢ indexOf m [] ≤ indexOf x✝² []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m : α
hm : m ∈ argmax f (hd :: tl)
a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
⊢ indexOf m (hd :: tl) ≤ indexOf a (hd :: tl)
[PROOFSTEP]
simp only [indexOf_cons, argmax_cons, Option.mem_def] at hm ⊢
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (argmax f tl) = some m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
cases h : argmax f tl
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (argmax f tl) = some m
h : argmax f tl = none
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
rw [h] at hm
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) none = some m
h : argmax f tl = none
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
simp_all
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (argmax f tl) = some m
val✝ : α
h : argmax f tl = some val✝
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
rw [h] at hm
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val✝ : α
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (some val✝) = some m
h : argmax f tl = some val✝
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
dsimp only at hm
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
obtain ha | ha := ha
[GOAL]
case some.head
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
ham : f m ≤ f hd
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)
[PROOFSTEP]
split_ifs at hm
[GOAL]
case some.tail
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
a✝ : Mem a tl
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
split_ifs at hm
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : f hd < f val✝
hm : some val✝ = some m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)
[PROOFSTEP]
injection hm with hm
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : ¬f hd < f val✝
hm : some hd = some m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)
[PROOFSTEP]
injection hm with hm
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
hm : some val✝ = some m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
injection hm with hm
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
hm : some hd = some m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
injection hm with hm
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : f hd < f val✝
hm : val✝ = m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)
[PROOFSTEP]
subst hm
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : ¬f hd < f val✝
hm : hd = m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)
[PROOFSTEP]
subst hm
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
hm : val✝ = m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
subst hm
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
hm : hd = m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
subst hm
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : f hd < f val✝
ham : f val✝ ≤ f hd
⊢ (if val✝ = hd then 0 else Nat.succ (indexOf val✝ tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)
[PROOFSTEP]
cases not_le_of_lt ‹_› ‹_›
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : ¬f hd < f val✝
ham : f hd ≤ f hd
⊢ (if hd = hd then 0 else Nat.succ (indexOf hd tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)
[PROOFSTEP]
rw [if_pos rfl]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ (if val✝ = hd then 0 else Nat.succ (indexOf val✝ tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
rw [if_neg, if_neg]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ Nat.succ (indexOf val✝ tl) ≤ Nat.succ (indexOf a tl)
case pos.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬a = hd
case pos.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬val✝ = hd
[PROOFSTEP]
exact Nat.succ_le_succ (index_of_argmax h (by assumption) ham)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ a ∈ tl
[PROOFSTEP]
assumption
[GOAL]
case pos.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬a = hd
[PROOFSTEP]
exact ne_of_apply_ne f (lt_of_lt_of_le ‹_› ‹_›).ne'
[GOAL]
case pos.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬val✝ = hd
[PROOFSTEP]
exact ne_of_apply_ne _ ‹f hd < f _›.ne'
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else Nat.succ (indexOf hd tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
rw [if_pos rfl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ 0 ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l) → m ∈ argmax f l
[PROOFSTEP]
rintro ⟨hml, ham, hma⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
⊢ m ∈ argmax f l
[PROOFSTEP]
cases' harg : argmax f l with n
[GOAL]
case intro.intro.none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
harg : argmax f l = none
⊢ m ∈ none
[PROOFSTEP]
simp_all
[GOAL]
case intro.intro.some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
n : α
harg : argmax f l = some n
⊢ m ∈ some n
[PROOFSTEP]
have :=
  _root_.le_antisymm (hma n (argmax_mem harg) (le_of_mem_argmax hml harg))
    (index_of_argmax harg hml (ham _ (argmax_mem harg)))
[GOAL]
case intro.intro.some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
n : α
harg : argmax f l = some n
this : indexOf m l = indexOf n l
⊢ m ∈ some n
[PROOFSTEP]
rw [(indexOf_inj hml (argmax_mem harg)).1 this, Option.mem_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
l : List α
a m : α
ha : a ∈ l
⊢ ¬maximum l < ↑a
[PROOFSTEP]
cases h : l.maximum
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
l : List α
a m : α
ha : a ∈ l
h : maximum l = none
⊢ ¬none < ↑a
[PROOFSTEP]
simp_all
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
l : List α
a m : α
ha : a ∈ l
val✝ : α
h : maximum l = some val✝
⊢ ¬some val✝ < ↑a
[PROOFSTEP]
simp [WithBot.some_eq_coe, WithBot.coe_lt_coe, not_lt_maximum_of_mem ha h, not_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
⊢ maximum (l ++ [a]) = max (maximum l) ↑a
[PROOFSTEP]
simp only [maximum, argmax_concat, id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) (argmax (fun a => a) l) =
    max (argmax (fun a => a) l) ↑a
[PROOFSTEP]
cases h : argmax id l
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
h : argmax id l = none
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) none = max none ↑a
[PROOFSTEP]
exact (max_eq_right bot_le).symm
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
val✝ : α
h : argmax id l = some val✝
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) (some val✝) = max (some val✝) ↑a
[PROOFSTEP]
simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
⊢ maximum [a] = max (↑a) (maximum [])
[PROOFSTEP]
simp [@max_eq_left (WithBot α) _ _ _ bot_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l tl : List α
hd : α
ih : maximum (a :: tl) = max (↑a) (maximum tl)
⊢ maximum (a :: (tl ++ [hd])) = max (↑a) (maximum (tl ++ [hd]))
[PROOFSTEP]
rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
⊢ maximum l = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
[PROOFSTEP]
rw [maximum, ← WithBot.some_eq_coe, argmax_eq_some_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → indexOf m l ≤ indexOf a l) ↔
    m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
[PROOFSTEP]
simp only [id_eq, and_congr_right_iff, and_iff_left_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
⊢ m ∈ l → (∀ (a : α), a ∈ l → a ≤ m) → ∀ (a : α), a ∈ l → m ≤ a → indexOf m l ≤ indexOf a l
[PROOFSTEP]
intro _ h a hal hma
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a✝¹ m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
hal : a ∈ l
hma : m ≤ a
⊢ indexOf m l ≤ indexOf a l
[PROOFSTEP]
rw [_root_.le_antisymm hma (h a hal)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
⊢ ↑a ≤ maximum l ↔ ∃ b, b ∈ l ∧ a ≤ b
[PROOFSTEP]
induction l with
| nil => simp
| cons h t ih => simp [maximum_cons, ih]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
⊢ ↑a ≤ maximum l ↔ ∃ b, b ∈ l ∧ a ≤ b
[PROOFSTEP]
induction l with
| nil => simp
| cons h t ih => simp [maximum_cons, ih]
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
⊢ ↑a ≤ maximum [] ↔ ∃ b, b ∈ [] ∧ a ≤ b
[PROOFSTEP]

| nil => simp
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
⊢ ↑a ≤ maximum [] ↔ ∃ b, b ∈ [] ∧ a ≤ b
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m h : α
t : List α
ih : ↑a ≤ maximum t ↔ ∃ b, b ∈ t ∧ a ≤ b
⊢ ↑a ≤ maximum (h :: t) ↔ ∃ b, b ∈ h :: t ∧ a ≤ b
[PROOFSTEP]

| cons h t ih => simp [maximum_cons, ih]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m h : α
t : List α
ih : ↑a ≤ maximum t ↔ ∃ b, b ∈ t ∧ a ≤ b
⊢ ↑a ≤ maximum (h :: t) ↔ ∃ b, b ∈ h :: t ∧ a ≤ b
[PROOFSTEP]
simp [maximum_cons, ih]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
h : l ≠ []
head✝ : α
tail✝ : List α
x✝ : head✝ :: tail✝ ≠ []
⊢ maximum (head✝ :: tail✝) ≠ ⊥
[PROOFSTEP]
simp [maximum_cons]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
h : 0 < length l
head✝ : α
tail✝ : List α
x✝ : 0 < length (head✝ :: tail✝)
⊢ maximum (head✝ :: tail✝) ≠ ⊥
[PROOFSTEP]
simp [maximum_cons]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
h : a ∈ l
w : 0 < length l
⊢ a ≤ maximum_of_length_pos w
[PROOFSTEP]
simp [le_maximum_of_length_pos_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
h : a ∈ l
w : 0 < length l
⊢ ↑a ≤ maximum l
[PROOFSTEP]
exact le_maximum_of_mem' h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
i : ℕ
w : i < length l
h : optParam (0 < length l) (_ : 0 < length l)
⊢ l[i] ≤ maximum_of_length_pos h
[PROOFSTEP]
apply le_maximum_of_length_pos_of_mem
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
l : List α
a m : α
i : ℕ
w : i < length l
h : optParam (0 < length l) (_ : 0 < length l)
⊢ l[i] ∈ l
[PROOFSTEP]
exact get_mem l i w
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h : l ≠ []
⊢ ↑(foldr max ⊥ l) = maximum l
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝ : l ≠ []
h : [] ≠ []
⊢ ↑(foldr max ⊥ []) = maximum []
[PROOFSTEP]
contradiction
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h : hd :: tl ≠ []
⊢ ↑(foldr max ⊥ (hd :: tl)) = maximum (hd :: tl)
[PROOFSTEP]
rw [maximum_cons, foldr, WithBot.coe_max]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h : hd :: tl ≠ []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) (maximum tl)
[PROOFSTEP]
by_cases h : tl = []
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝¹ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h✝ : hd :: tl ≠ []
h : tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) (maximum tl)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝¹ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) (maximum tl)
[PROOFSTEP]
simp [IH h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝ l : List α
a : α
h : ∀ (x : α), x ∈ l → x ≤ a
⊢ foldr max ⊥ l ≤ a
[PROOFSTEP]
induction' l with y l IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝ l : List α
a : α
h✝ : ∀ (x : α), x ∈ l → x ≤ a
h : ∀ (x : α), x ∈ [] → x ≤ a
⊢ foldr max ⊥ [] ≤ a
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a : α
h✝ : ∀ (x : α), x ∈ l✝ → x ≤ a
y : α
l : List α
IH : (∀ (x : α), x ∈ l → x ≤ a) → foldr max ⊥ l ≤ a
h : ∀ (x : α), x ∈ y :: l → x ≤ a
⊢ foldr max ⊥ (y :: l) ≤ a
[PROOFSTEP]
simpa [h y (mem_cons_self _ _)] using IH fun x hx => h x <| mem_cons_of_mem _ hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝ l : List α
a x : α
hx : x ∈ l
h : a ≤ x
⊢ a ≤ foldr max ⊥ l
[PROOFSTEP]
induction' l with y l IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝ l : List α
a x : α
hx✝ : x ∈ l
h : a ≤ x
hx : x ∈ []
⊢ a ≤ foldr max ⊥ []
[PROOFSTEP]
exact absurd hx (not_mem_nil _)
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx✝ : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
hx : x ∈ y :: l
⊢ a ≤ foldr max ⊥ (y :: l)
[PROOFSTEP]
obtain hl | hl := hx
[GOAL]
case cons.head
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)
case cons.tail
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)
[PROOFSTEP]
simp only [foldr, foldr_cons]
[GOAL]
case cons.head
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ max x (foldr max ⊥ l)
[PROOFSTEP]
exact le_max_of_le_left h
[GOAL]
case cons.tail
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)
[PROOFSTEP]
exact le_max_of_le_right (IH (by assumption))
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ x ∈ l
[PROOFSTEP]
assumption


[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : α
as : List α
x : α
⊢ x ∈ List.insert a as ↔ x ∈ a :: as
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
as bs : List α
x : α
⊢ x ∈ as ∪ bs ↔ x ∈ as ++ bs
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
⊢ b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
[PROOFSTEP]
induction as with
| nil => simp [remove]
| cons a' as ih =>
  simp [remove]
  cases Decidable.em (a = a') with
  | inl h =>
    simp only [if_pos h, ih]
    exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
  | inr h =>
    simp [if_neg h, ih]
    constructor
    {focus
        intro h'
        cases h' with
        | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
        | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
    }
    intro ⟨h1, h2⟩
    cases h1 with
    | inl h1' => exact Or.inl h1'
    | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
⊢ b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
[PROOFSTEP]
induction as with
| nil => simp [remove]
| cons a' as ih =>
  simp [remove]
  cases Decidable.em (a = a') with
  | inl h =>
    simp only [if_pos h, ih]
    exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
  | inr h =>
    simp [if_neg h, ih]
    constructor
    {focus
        intro h'
        cases h' with
        | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
        | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
    }
    intro ⟨h1, h2⟩
    cases h1 with
    | inl h1' => exact Or.inl h1'
    | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case nil
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
⊢ b ∈ remove a [] ↔ b ∈ [] ∧ b ≠ a
[PROOFSTEP]

| nil => simp [remove]
[GOAL]
case nil
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
⊢ b ∈ remove a [] ↔ b ∈ [] ∧ b ≠ a
[PROOFSTEP]
simp [remove]
[GOAL]
case cons
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
⊢ b ∈ remove a (a' :: as) ↔ b ∈ a' :: as ∧ b ≠ a
[PROOFSTEP]

| cons a' as ih =>
  simp [remove]
  cases Decidable.em (a = a') with
  | inl h =>
    simp only [if_pos h, ih]
    exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
  | inr h =>
    simp [if_neg h, ih]
    constructor
    {focus
        intro h'
        cases h' with
        | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
        | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
    }
    intro ⟨h1, h2⟩
    cases h1 with
    | inl h1' => exact Or.inl h1'
    | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
⊢ b ∈ remove a (a' :: as) ↔ b ∈ a' :: as ∧ b ≠ a
[PROOFSTEP]
simp [remove]
[GOAL]
case cons
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
cases Decidable.em (a = a') with
| inl h =>
  simp only [if_pos h, ih]
  exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
| inr h =>
  simp [if_neg h, ih]
  constructor
  {focus
      intro h'
      cases h' with
      | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
      | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
  }
  intro ⟨h1, h2⟩
  cases h1 with
  | inl h1' => exact Or.inl h1'
  | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
x✝ : a = a' ∨ ¬a = a'
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
cases Decidable.em (a = a') with
| inl h =>
  simp only [if_pos h, ih]
  exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
| inr h =>
  simp [if_neg h, ih]
  constructor
  {focus
      intro h'
      cases h' with
      | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
      | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
  }
  intro ⟨h1, h2⟩
  cases h1 with
  | inl h1' => exact Or.inl h1'
  | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : a = a'
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]

| inl h =>
  simp only [if_pos h, ih]
  exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
[GOAL]
case cons.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : a = a'
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
simp only [if_pos h, ih]
[GOAL]
case cons.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : a = a'
⊢ b ∈ as ∧ b ≠ a ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
[GOAL]
case cons.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]

| inr h =>
  simp [if_neg h, ih]
  constructor
  {focus
      intro h'
      cases h' with
      | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
      | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
  }
  intro ⟨h1, h2⟩
  cases h1 with
  | inl h1' => exact Or.inl h1'
  | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
simp [if_neg h, ih]
[GOAL]
case cons.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
constructor
[GOAL]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a → (b = a' ∨ b ∈ as) ∧ ¬b = a
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a → b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
{focus
    intro h'
    cases h' with
    | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
    | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
}
[GOAL]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a → (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
focus
  intro h'
  cases h' with
  | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
  | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
[GOAL]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a → (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
intro h'
[GOAL]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h' : b = a' ∨ b ∈ as ∧ ¬b = a
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
cases h' with
| inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
| inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
[GOAL]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h' : b = a' ∨ b ∈ as ∧ ¬b = a
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
cases h' with
| inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
| inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
[GOAL]
case cons.inr.mp.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h₁ : b = a'
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]

| inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
[GOAL]
case cons.inr.mp.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h₁ : b = a'
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
[GOAL]
case cons.inr.mp.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h₁ : b ∈ as ∧ ¬b = a
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]

| inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
[GOAL]
case cons.inr.mp.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h₁ : b ∈ as ∧ ¬b = a
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
exact ⟨Or.inr h₁.1, h₁.2⟩
[GOAL]
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a → b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
intro ⟨h1, h2⟩
[GOAL]
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h1 : b = a' ∨ b ∈ as
h2 : ¬b = a
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
cases h1 with
| inl h1' => exact Or.inl h1'
| inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h1 : b = a' ∨ b ∈ as
h2 : ¬b = a
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
cases h1 with
| inl h1' => exact Or.inl h1'
| inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons.inr.mpr.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h2 : ¬b = a
h1' : b = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]

| inl h1' => exact Or.inl h1'
[GOAL]
case cons.inr.mpr.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h2 : ¬b = a
h1' : b = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
exact Or.inl h1'
[GOAL]
case cons.inr.mpr.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h2 : ¬b = a
h1' : b ∈ as
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]

| inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons.inr.mpr.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h2 : ¬b = a
h1' : b ∈ as
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
exact Or.inr ⟨h1', h2⟩
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
x✝ : ¬a ∈ []
⊢ remove a [] = []
[PROOFSTEP]
simp [remove]
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : ¬a ∈ a' :: as
⊢ remove a (a' :: as) = a' :: as
[PROOFSTEP]
have h1 : a ≠ a' := fun h' ↦ h (by rw [h']; apply mem_cons_self)
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : ¬a ∈ a' :: as
h' : a = a'
⊢ a ∈ a' :: as
[PROOFSTEP]
rw [h']
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : ¬a ∈ a' :: as
h' : a = a'
⊢ a' ∈ a' :: as
[PROOFSTEP]
apply mem_cons_self
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : ¬a ∈ a' :: as
h1 : a ≠ a'
⊢ remove a (a' :: as) = a' :: as
[PROOFSTEP]
have h2 : a ∉ as := fun h' ↦ h (mem_cons_of_mem _ h')
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : ¬a ∈ a' :: as
h1 : a ≠ a'
h2 : ¬a ∈ as
⊢ remove a (a' :: as) = a' :: as
[PROOFSTEP]
simp [remove, h1, remove_eq_of_not_mem h2]
[GOAL]
α : Type u_1
β : Sort ?u.19685
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
h : b ∈ remove a as
⊢ b ∈ as
[PROOFSTEP]
rw [mem_remove_iff] at h
[GOAL]
α : Type u_1
β : Sort ?u.19685
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
h : b ∈ as ∧ b ≠ a
⊢ b ∈ as
[PROOFSTEP]
exact
  h.1
    /- card -/
[GOAL]
α : Type u_1
β : Sort ?u.20767
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : a ∈ as
⊢ card (a :: as) = card as
[PROOFSTEP]
simp [card, h]
[GOAL]
α : Type u_1
β : Sort ?u.21944
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : ¬a ∈ as
⊢ card (a :: as) = card as + 1
[PROOFSTEP]
simp [card, h]
[GOAL]
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
⊢ card as ≤ card (a :: as)
[PROOFSTEP]
cases Decidable.em (a ∈ as) with
| inl h => simp [h, Nat.le_refl]
| inr h => simp [h, Nat.le_succ]
[GOAL]
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
x✝ : a ∈ as ∨ ¬a ∈ as
⊢ card as ≤ card (a :: as)
[PROOFSTEP]
cases Decidable.em (a ∈ as) with
| inl h => simp [h, Nat.le_refl]
| inr h => simp [h, Nat.le_succ]
[GOAL]
case inl
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : a ∈ as
⊢ card as ≤ card (a :: as)
[PROOFSTEP]

| inl h => simp [h, Nat.le_refl]
[GOAL]
case inl
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : a ∈ as
⊢ card as ≤ card (a :: as)
[PROOFSTEP]
simp [h, Nat.le_refl]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : ¬a ∈ as
⊢ card as ≤ card (a :: as)
[PROOFSTEP]

| inr h => simp [h, Nat.le_succ]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : ¬a ∈ as
⊢ card as ≤ card (a :: as)
[PROOFSTEP]
simp [h, Nat.le_succ]
[GOAL]
α : Type u_1
β : Sort ?u.25043
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : a ∈ as
⊢ card (List.insert a as) = card as
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Sort ?u.25854
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : ¬a ∈ as
⊢ card (List.insert a as) = card as + 1
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]
cases Decidable.em (a = a') with
| inl h' =>
  simp [remove, if_pos h']
  cases Decidable.em (a ∈ as) with
  | inl h'' =>
    have h₃ : a' ∈ as := h' ▸ h''
    simp [card_remove_of_mem h'', h₃]
  | inr h'' =>
    have h₃ : a' ∉ as := h' ▸ h''
    simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
| inr h' =>
  have h₃ : a ∈ as := (mem_cons.1 h).resolve_left h'
  simp [remove, h']
  cases Decidable.em (a' ∈ as) with
  | inl h'' =>
    have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
    simp [h'', this, card_remove_of_mem h₃]
  | inr h'' =>
    have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
    simp [h'', this, card_remove_of_mem h₃]
[GOAL]
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
x✝ : a = a' ∨ ¬a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]
cases Decidable.em (a = a') with
| inl h' =>
  simp [remove, if_pos h']
  cases Decidable.em (a ∈ as) with
  | inl h'' =>
    have h₃ : a' ∈ as := h' ▸ h''
    simp [card_remove_of_mem h'', h₃]
  | inr h'' =>
    have h₃ : a' ∉ as := h' ▸ h''
    simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
| inr h' =>
  have h₃ : a ∈ as := (mem_cons.1 h).resolve_left h'
  simp [remove, h']
  cases Decidable.em (a' ∈ as) with
  | inl h'' =>
    have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
    simp [h'', this, card_remove_of_mem h₃]
  | inr h'' =>
    have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
    simp [h'', this, card_remove_of_mem h₃]
[GOAL]
case inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]

| inl h' =>
  simp [remove, if_pos h']
  cases Decidable.em (a ∈ as) with
  | inl h'' =>
    have h₃ : a' ∈ as := h' ▸ h''
    simp [card_remove_of_mem h'', h₃]
  | inr h'' =>
    have h₃ : a' ∉ as := h' ▸ h''
    simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
[GOAL]
case inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]
simp [remove, if_pos h']
[GOAL]
case inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
⊢ card (a' :: as) = card (remove a as) + 1
[PROOFSTEP]
cases Decidable.em (a ∈ as) with
| inl h'' =>
  have h₃ : a' ∈ as := h' ▸ h''
  simp [card_remove_of_mem h'', h₃]
| inr h'' =>
  have h₃ : a' ∉ as := h' ▸ h''
  simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
[GOAL]
case inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
x✝ : a ∈ as ∨ ¬a ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
[PROOFSTEP]
cases Decidable.em (a ∈ as) with
| inl h'' =>
  have h₃ : a' ∈ as := h' ▸ h''
  simp [card_remove_of_mem h'', h₃]
| inr h'' =>
  have h₃ : a' ∉ as := h' ▸ h''
  simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
[GOAL]
case inl.inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : a ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
[PROOFSTEP]

| inl h'' =>
  have h₃ : a' ∈ as := h' ▸ h''
  simp [card_remove_of_mem h'', h₃]
[GOAL]
case inl.inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : a ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
[PROOFSTEP]
have h₃ : a' ∈ as := h' ▸ h''
[GOAL]
case inl.inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : a ∈ as
h₃ : a' ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
[PROOFSTEP]
simp [card_remove_of_mem h'', h₃]
[GOAL]
case inl.inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : ¬a ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
[PROOFSTEP]

| inr h'' =>
  have h₃ : a' ∉ as := h' ▸ h''
  simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
[GOAL]
case inl.inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : ¬a ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
[PROOFSTEP]
have h₃ : a' ∉ as := h' ▸ h''
[GOAL]
case inl.inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : ¬a ∈ as
h₃ : ¬a' ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
[PROOFSTEP]
simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
[GOAL]
case inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]

| inr h' =>
  have h₃ : a ∈ as := (mem_cons.1 h).resolve_left h'
  simp [remove, h']
  cases Decidable.em (a' ∈ as) with
  | inl h'' =>
    have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
    simp [h'', this, card_remove_of_mem h₃]
  | inr h'' =>
    have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
    simp [h'', this, card_remove_of_mem h₃]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]
have h₃ : a ∈ as := (mem_cons.1 h).resolve_left h'
[GOAL]
case inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]
simp [remove, h']
[GOAL]
case inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
[PROOFSTEP]
cases Decidable.em (a' ∈ as) with
| inl h'' =>
  have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
  simp [h'', this, card_remove_of_mem h₃]
| inr h'' =>
  have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
  simp [h'', this, card_remove_of_mem h₃]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
x✝ : a' ∈ as ∨ ¬a' ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
[PROOFSTEP]
cases Decidable.em (a' ∈ as) with
| inl h'' =>
  have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
  simp [h'', this, card_remove_of_mem h₃]
| inr h'' =>
  have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
  simp [h'', this, card_remove_of_mem h₃]
[GOAL]
case inr.inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
[PROOFSTEP]

| inl h'' =>
  have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
  simp [h'', this, card_remove_of_mem h₃]
[GOAL]
case inr.inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
[PROOFSTEP]
have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
[GOAL]
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
⊢ a' ∈ remove a as
[PROOFSTEP]
rw [mem_remove_iff]
[GOAL]
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
⊢ a' ∈ as ∧ a' ≠ a
[PROOFSTEP]
exact ⟨h'', Ne.symm h'⟩
[GOAL]
case inr.inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
this : a' ∈ remove a as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
[PROOFSTEP]
simp [h'', this, card_remove_of_mem h₃]
[GOAL]
case inr.inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : ¬a' ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
[PROOFSTEP]

| inr h'' =>
  have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
  simp [h'', this, card_remove_of_mem h₃]
[GOAL]
case inr.inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : ¬a' ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
[PROOFSTEP]
have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
[GOAL]
case inr.inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : ¬a' ∈ as
this : ¬a' ∈ remove a as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
[PROOFSTEP]
simp [h'', this, card_remove_of_mem h₃]
[GOAL]
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
bs : List α
x✝ : [] ⊆ bs
⊢ card [] ≤ card bs
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
cases Decidable.em (a ∈ as) with
| inl h' =>
  have hsub' : as ⊆ bs := fun _ xmem ↦ hsub (mem_cons_of_mem a xmem)
  simp [h', card_subset_le hsub']
| inr h' =>
  have : a ∈ bs := hsub (Mem.head ..)
  rw [card_cons_of_not_mem h', card_remove_of_mem this]
  apply Nat.add_le_add_right
  apply card_subset_le
  intro x xmem
  rw [mem_remove_iff]
  exact ⟨hsub (mem_cons_of_mem _ xmem), fun h ↦ h' (h ▸ xmem)⟩
[GOAL]
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
x✝ : a ∈ as ∨ ¬a ∈ as
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
cases Decidable.em (a ∈ as) with
| inl h' =>
  have hsub' : as ⊆ bs := fun _ xmem ↦ hsub (mem_cons_of_mem a xmem)
  simp [h', card_subset_le hsub']
| inr h' =>
  have : a ∈ bs := hsub (Mem.head ..)
  rw [card_cons_of_not_mem h', card_remove_of_mem this]
  apply Nat.add_le_add_right
  apply card_subset_le
  intro x xmem
  rw [mem_remove_iff]
  exact ⟨hsub (mem_cons_of_mem _ xmem), fun h ↦ h' (h ▸ xmem)⟩
[GOAL]
case inl
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : a ∈ as
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]

| inl h' =>
  have hsub' : as ⊆ bs := fun _ xmem ↦ hsub (mem_cons_of_mem a xmem)
  simp [h', card_subset_le hsub']
[GOAL]
case inl
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : a ∈ as
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
have hsub' : as ⊆ bs := fun _ xmem ↦ hsub (mem_cons_of_mem a xmem)
[GOAL]
case inl
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : a ∈ as
hsub' : as ⊆ bs
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
simp [h', card_subset_le hsub']
[GOAL]
case inr
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]

| inr h' =>
  have : a ∈ bs := hsub (Mem.head ..)
  rw [card_cons_of_not_mem h', card_remove_of_mem this]
  apply Nat.add_le_add_right
  apply card_subset_le
  intro x xmem
  rw [mem_remove_iff]
  exact ⟨hsub (mem_cons_of_mem _ xmem), fun h ↦ h' (h ▸ xmem)⟩
[GOAL]
case inr
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
have : a ∈ bs := hsub (Mem.head ..)
[GOAL]
case inr
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
rw [card_cons_of_not_mem h', card_remove_of_mem this]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card as + 1 ≤ card (remove a bs) + 1
[PROOFSTEP]
apply Nat.add_le_add_right
[GOAL]
case inr.h
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card as ≤ card (remove a bs)
[PROOFSTEP]
apply card_subset_le
[GOAL]
case inr.h.a
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ as ⊆ remove a bs
[PROOFSTEP]
intro x xmem
[GOAL]
case inr.h.a
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
x : α
xmem : x ∈ as
⊢ x ∈ remove a bs
[PROOFSTEP]
rw [mem_remove_iff]
[GOAL]
case inr.h.a
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
x : α
xmem : x ∈ as
⊢ x ∈ bs ∧ x ≠ a
[PROOFSTEP]
exact ⟨hsub (mem_cons_of_mem _ xmem), fun h ↦ h' (h ▸ xmem)⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
as : List α
⊢ card (map f as) ≤ card as
[PROOFSTEP]
induction as with
| nil => simp
| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    rw [map, card_cons_of_mem h]
    apply Nat.le_trans ih (card_le_card_cons ..)
  | inr h =>
    have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
    exact Nat.add_le_add_right ih _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
as : List α
⊢ card (map f as) ≤ card as
[PROOFSTEP]
induction as with
| nil => simp
| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    rw [map, card_cons_of_mem h]
    apply Nat.le_trans ih (card_le_card_cons ..)
  | inr h =>
    have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
    exact Nat.add_le_add_right ih _
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
⊢ card (map f []) ≤ card []
[PROOFSTEP]

| nil => simp
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
⊢ card (map f []) ≤ card []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]

| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    rw [map, card_cons_of_mem h]
    apply Nat.le_trans ih (card_le_card_cons ..)
  | inr h =>
    have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
    exact Nat.add_le_add_right ih _
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]
cases Decidable.em (f a ∈ map f as) with
| inl h =>
  rw [map, card_cons_of_mem h]
  apply Nat.le_trans ih (card_le_card_cons ..)
| inr h =>
  have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
  exact Nat.add_le_add_right ih _
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
x✝ : f a ∈ map f as ∨ ¬f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]
cases Decidable.em (f a ∈ map f as) with
| inl h =>
  rw [map, card_cons_of_mem h]
  apply Nat.le_trans ih (card_le_card_cons ..)
| inr h =>
  have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
  exact Nat.add_le_add_right ih _
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]

| inl h =>
  rw [map, card_cons_of_mem h]
  apply Nat.le_trans ih (card_le_card_cons ..)
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]
rw [map, card_cons_of_mem h]
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : f a ∈ map f as
⊢ card (map f as) ≤ card (a :: as)
[PROOFSTEP]
apply Nat.le_trans ih (card_le_card_cons ..)
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]

| inr h =>
  have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
  exact Nat.add_le_add_right ih _
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]
have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
this : ¬a ∈ as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]
rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
this : ¬a ∈ as
⊢ card (map f as) + 1 ≤ card as + 1
[PROOFSTEP]
exact Nat.add_le_add_right ih _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
as : List α
⊢ inj_on f as → card (map f as) = card as
[PROOFSTEP]
induction as with
| nil => simp
| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    intro inj_on'
    cases (exists_of_mem_map h) with
    | intro x hx =>
      have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
      have h1 : a ∈ as := this ▸ hx.1
      have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
      rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
  | inr h =>
    intro inj_on'
    have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
as : List α
⊢ inj_on f as → card (map f as) = card as
[PROOFSTEP]
induction as with
| nil => simp
| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    intro inj_on'
    cases (exists_of_mem_map h) with
    | intro x hx =>
      have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
      have h1 : a ∈ as := this ▸ hx.1
      have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
      rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
  | inr h =>
    intro inj_on'
    have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
⊢ inj_on f [] → card (map f []) = card []
[PROOFSTEP]

| nil => simp
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
⊢ inj_on f [] → card (map f []) = card []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]

| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    intro inj_on'
    cases (exists_of_mem_map h) with
    | intro x hx =>
      have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
      have h1 : a ∈ as := this ▸ hx.1
      have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
      rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
  | inr h =>
    intro inj_on'
    have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
cases Decidable.em (f a ∈ map f as) with
| inl h =>
  intro inj_on'
  cases (exists_of_mem_map h) with
  | intro x hx =>
    have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
    have h1 : a ∈ as := this ▸ hx.1
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
| inr h =>
  intro inj_on'
  have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
x✝ : f a ∈ map f as ∨ ¬f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
cases Decidable.em (f a ∈ map f as) with
| inl h =>
  intro inj_on'
  cases (exists_of_mem_map h) with
  | intro x hx =>
    have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
    have h1 : a ∈ as := this ▸ hx.1
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
| inr h =>
  intro inj_on'
  have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]

| inl h =>
  intro inj_on'
  cases (exists_of_mem_map h) with
  | intro x hx =>
    have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
    have h1 : a ∈ as := this ▸ hx.1
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
intro inj_on'
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
cases (exists_of_mem_map h) with
| intro x hx =>
  have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
  have h1 : a ∈ as := this ▸ hx.1
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x✝ : ∃ a_1, a_1 ∈ as ∧ f a_1 = f a
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
cases (exists_of_mem_map h) with
| intro x hx =>
  have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
  have h1 : a ∈ as := this ▸ hx.1
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
[GOAL]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]

| intro x hx =>
  have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
  have h1 : a ∈ as := this ▸ hx.1
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
[GOAL]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
[GOAL]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
have h1 : a ∈ as := this ▸ hx.1
[GOAL]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
h1 : a ∈ as
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
[GOAL]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
h1 : a ∈ as
h2 : inj_on f as
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]

| inr h =>
  intro inj_on'
  have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
intro inj_on'
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
h1 : ¬a ∈ as
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
h1 : ¬a ∈ as
h2 : inj_on f as
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝¹ : List α
x✝ : Disjoint [] x✝¹
⊢ card ([] ++ x✝¹) = card [] + card x✝¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
[PROOFSTEP]
have disj' : Disjoint as bs := fun _ h1 h2 ↦ disj (mem_cons_of_mem a h1) h2
[GOAL]
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
[PROOFSTEP]
cases Decidable.em (a ∈ as) with
| inl h => simp [h, card_append_disjoint disj']
| inr h =>
  have h1 : a ∉ bs := fun h' ↦ disj (mem_cons_self a as) h'
  simp [h, h1, card_append_disjoint disj']
  rw [Nat.add_right_comm]
[GOAL]
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
x✝ : a ∈ as ∨ ¬a ∈ as
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
[PROOFSTEP]
cases Decidable.em (a ∈ as) with
| inl h => simp [h, card_append_disjoint disj']
| inr h =>
  have h1 : a ∉ bs := fun h' ↦ disj (mem_cons_self a as) h'
  simp [h, h1, card_append_disjoint disj']
  rw [Nat.add_right_comm]
[GOAL]
case inl
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : a ∈ as
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
[PROOFSTEP]

| inl h => simp [h, card_append_disjoint disj']
[GOAL]
case inl
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : a ∈ as
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
[PROOFSTEP]
simp [h, card_append_disjoint disj']
[GOAL]
case inr
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : ¬a ∈ as
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
[PROOFSTEP]

| inr h =>
  have h1 : a ∉ bs := fun h' ↦ disj (mem_cons_self a as) h'
  simp [h, h1, card_append_disjoint disj']
  rw [Nat.add_right_comm]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : ¬a ∈ as
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
[PROOFSTEP]
have h1 : a ∉ bs := fun h' ↦ disj (mem_cons_self a as) h'
[GOAL]
case inr
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : ¬a ∈ as
h1 : ¬a ∈ bs
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
[PROOFSTEP]
simp [h, h1, card_append_disjoint disj']
[GOAL]
case inr
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : ¬a ∈ as
h1 : ¬a ∈ bs
⊢ card as + card bs + 1 = card as + 1 + card bs
[PROOFSTEP]
rw [Nat.add_right_comm]
[GOAL]
α : Type u_1
β : Sort ?u.54019
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
as bs : List α
h : Disjoint as bs
⊢ card (as ∪ bs) = card as + card bs
[PROOFSTEP]
rw [card_eq_of_equiv (union_equiv_append as bs), card_append_disjoint h]