internlm/Lean-Github huggingface dataset:
Theorem: List.mapM'_mem_inversion
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
b' : β
hb' : f a = some b'
bs' : List β
hbs' : mapM' f as = some bs'
hb : b ∈ b' :: bs'
⊢ b = b' ∨ b ∈ bs'
Tactic:
simpa using hb
Proof state after:
no goals
Theorem: List.mapM'_mem_inversion
Proof state before:
case cons.intro.intro.intro.intro.inl
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
bs' : List β
hbs' : mapM' f as = some bs'
hb' : f a = some b
hb : b ∈ b :: bs'
⊢ ∃ a, f a = some b
Tactic:
exact ⟨a, hb'⟩
Proof state after:
no goals
Theorem: List.mapM'_mem_inversion
Proof state before:
case cons.intro.intro.intro.intro.inr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
b' : β
hb' : f a = some b'
bs' : List β
hbs' : mapM' f as = some bs'
hb✝ : b ∈ b' :: bs'
hb : b ∈ bs'
⊢ ∃ a, f a = some b
Tactic:
exact ih hbs' hb
Proof state after:
no goals
Theorem: List.mapM'_eq_mapM'_of_eq
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
l : List α
hf : ∀ a ∈ l, f a = g a
⊢ mapM' f l = mapM' g l
Tactic:
induction' l with a as ih <;> simp
Proof state after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Theorem: List.mapM'_eq_mapM'_of_eq
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Tactic:
{ have : as.mapM' f = as.mapM' g := ih (fun a ha => hf a (by simp[ha]))
  have : f a = g a := hf a (by simp)
  simp[*] }
Proof state after:
no goals
Theorem: List.mapM'_eq_mapM'_of_eq
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Tactic:
have : as.mapM' f = as.mapM' g := ih (fun a ha => hf a (by simp[ha]))
Proof state after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this : mapM' f as = mapM' g as
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Theorem: List.mapM'_eq_mapM'_of_eq
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this : mapM' f as = mapM' g as
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Tactic:
have : f a = g a := hf a (by simp)
Proof state after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this✝ : mapM' f as = mapM' g as
this : f a = g a
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Theorem: List.mapM'_eq_mapM'_of_eq
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this✝ : mapM' f as = mapM' g as
this : f a = g a
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Tactic:
simp[*]
Proof state after:
no goals
Theorem: List.mapM'_eq_mapM'_of_eq
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a✝ : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a ∈ a✝ :: as, f a = g a
a : α
ha : a ∈ as
⊢ a ∈ a✝ :: as
Tactic:
simp[ha]
Proof state after:
no goals
Theorem: List.mapM'_eq_mapM'_of_eq
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this : mapM' f as = mapM' g as
⊢ a ∈ a :: as
Tactic:
simp
Proof state after:
no goals
Theorem: List.mapM'_option_map
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.164904 → Type ?u.164906
α : Type u_3
β : Type u_2
inst✝ : Monad m
γ : Type u_1
f : α → Option β
g : β → γ
as : List α
⊢ mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
Tactic:
induction' as with a as ih generalizing f g <;> simp[Option.pure_eq_some, Option.bind_eq_bind, Function.comp]
Proof state after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.164904 → Type ?u.164906
α : Type u_3
β : Type u_2
inst✝ : Monad m
γ : Type u_1
a : α
as : List α
ih :
  ∀ {f : α → Option β} {g : β → γ},
    mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
f : α → Option β
g : β → γ
⊢ ((Option.map g (f a)).bind fun __do_lift =>
      (mapM' (fun a => Option.map g (f a)) as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)) =
    Option.map (fun bs => map g bs)
      ((f a).bind fun __do_lift => (mapM' f as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1))
Theorem: List.mapM'_option_map
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.164904 → Type ?u.164906
α : Type u_3
β : Type u_2
inst✝ : Monad m
γ : Type u_1
a : α
as : List α
ih :
  ∀ {f : α → Option β} {g : β → γ},
    mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
f : α → Option β
g : β → γ
⊢ ((Option.map g (f a)).bind fun __do_lift =>
      (mapM' (fun a => Option.map g (f a)) as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)) =
    Option.map (fun bs => map g bs)
      ((f a).bind fun __do_lift => (mapM' f as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1))
Tactic:
{ simp[ih]
  rcases f a with (_ | b) <;> simp
  rcases mapM' f as with (_ | bs) <;> simp }
Proof state after:
no goals
Theorem: List.mapM'_option_map
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.164904 → Type ?u.164906
α : Type u_3
β : Type u_2
inst✝ : Monad m
γ : Type u_1
a : α
as : List α
ih :
  ∀ {f : α → Option β} {g : β → γ},
    mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
f : α → Option β
g : β → γ
⊢ ((Option.map g (f a)).bind fun __do_lift =>
      (mapM' (fun a => Option.map g (f a)) as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)) =
    Option.map (fun bs => map g bs)
      ((f a).bind fun __do_lift => (mapM' f as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1))
Tactic:
simp[ih]
Proof state after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.164904 → Type ?u.164906
α : Type u_3
β : Type u_2
inst✝ : Monad m
γ : Type u_1
a : α
as : List α
ih :
  ∀ {f : α → Option β} {g : β → γ},
    mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
f : α → Option β
g : β → γ
⊢ ((Option.map g (f a)).bind fun a =>
      (Option.map (fun bs => map g bs) (mapM' (fun a => f a) as)).bind fun a_1 => some (a :: a_1)) =
    Option.map (fun bs => map g bs)
      ((f a).bind fun __do_lift => (mapM' f as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1))
Theorem: List.mapM'_option_map
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.164904 → Type ?u.164906
α : Type u_3
β : Type u_2
inst✝ : Monad m
γ : Type u_1
a : α
as : List α
ih :
  ∀ {f : α → Option β} {g : β → γ},
    mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
f : α → Option β
g : β → γ
⊢ ((Option.map g (f a)).bind fun a =>
      (Option.map (fun bs => map g bs) (mapM' (fun a => f a) as)).bind fun a_1 => some (a :: a_1)) =
    Option.map (fun bs => map g bs)
      ((f a).bind fun __do_lift => (mapM' f as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1))
Tactic:
rcases f a with (_ | b) <;> simp
Proof state after:
case cons.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.164904 → Type ?u.164906
α : Type u_3
β : Type u_2
inst✝ : Monad m
γ : Type u_1
a : α
as : List α
ih :
  ∀ {f : α → Option β} {g : β → γ},
    mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
f : α → Option β
g : β → γ
b : β
⊢ ((Option.map (fun bs => map g bs) (mapM' (fun a => f a) as)).bind fun a => some (g b :: a)) =
    Option.map (fun bs => map g bs) ((mapM' f as).bind fun __do_lift => some (b :: __do_lift))
Theorem: List.mapM'_option_map
Proof state before:
case cons.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.164904 → Type ?u.164906
α : Type u_3
β : Type u_2
inst✝ : Monad m
γ : Type u_1
a : α
as : List α
ih :
  ∀ {f : α → Option β} {g : β → γ},
    mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
f : α → Option β
g : β → γ
b : β
⊢ ((Option.map (fun bs => map g bs) (mapM' (fun a => f a) as)).bind fun a => some (g b :: a)) =
    Option.map (fun bs => map g bs) ((mapM' f as).bind fun __do_lift => some (b :: __do_lift))
Tactic:
rcases mapM' f as with (_ | bs) <;> simp
Proof state after:
no goals
Theorem: List.mapM_eq_map
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.168328 → Type ?u.168330
α : Type u_1
β : Type u_2
inst✝ : Monad m
l : List α
f : α → β
⊢ mapM' (fun x => some (f x)) l = some (map f l)
Tactic:
induction l <;> simp[Option.pure_eq_some, Option.bind_eq_bind, Function.comp, *]
Proof state after:
no goals
Theorem: List.mapM_map
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.169273 → Type ?u.169275
α : Type u_2
β : Type u_3
inst✝ : Monad m
γ : Type u_1
as : List α
f : α → Option β
g : Option β → Option γ
⊢ mapM' g (map f as) = mapM' (g ∘ f) as
Tactic:
induction' as with a as ih <;> simp[Option.bind_eq_bind, Function.comp, *]
Proof state after:
no goals
Theorem: List.allSome_map_some
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.170951 → Type ?u.170953
α : Type u_1
β : Type u_2
inst✝ : Monad m
l : List α
f : α → β
⊢ (map (fun x => some (f x)) l).allSome' = some (map f l)
Tactic:
simp[allSome', mapM_map]
Proof state after:
no goals
Theorem: List.subset_of_eq
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171524 → Type ?u.171526
α : Type u_1
β : Type ?u.171532
inst✝ : Monad m
l₁ l₂ : List α
e : l₁ = l₂
⊢ l₁ ⊆ l₂
Tactic:
simp[e]
Proof state after:
no goals
Theorem: List.nil_iff
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
l : List α
⊢ l = [] ↔ ∀ (a : α), a ∉ l
Tactic:
induction l with
| nil => simp only [not_mem_nil, not_false_eq_true, implies_true];
| cons a _ _ =>
  simp_all only [mem_cons, not_or, false_iff, not_forall, not_and, not_not];
  use a;
  tauto;
Proof state after:
no goals
Theorem: List.nil_iff
Proof state before:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
⊢ [] = [] ↔ ∀ (a : α), a ∉ []
Tactic:
simp only [not_mem_nil, not_false_eq_true, implies_true]
Proof state after:
no goals
Theorem: List.nil_iff
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
a : α
tail✝ : List α
tail_ih✝ : tail✝ = [] ↔ ∀ (a : α), a ∉ tail✝
⊢ a :: tail✝ = [] ↔ ∀ (a_1 : α), a_1 ∉ a :: tail✝
Tactic:
simp_all only [mem_cons, not_or, false_iff, not_forall, not_and, not_not]
Proof state after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
a : α
tail✝ : List α
tail_ih✝ : tail✝ = [] ↔ ∀ (a : α), a ∉ tail✝
⊢ ∃ x, ¬x = a → x ∈ tail✝
Theorem: List.nil_iff
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
a : α
tail✝ : List α
tail_ih✝ : tail✝ = [] ↔ ∀ (a : α), a ∉ tail✝
⊢ ∃ x, ¬x = a → x ∈ tail✝
Tactic:
use a
Proof state after:
case h
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
a : α
tail✝ : List α
tail_ih✝ : tail✝ = [] ↔ ∀ (a : α), a ∉ tail✝
⊢ ¬a = a → a ∈ tail✝
Theorem: List.nil_iff
Proof state before:
case h
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
a : α
tail✝ : List α
tail_ih✝ : tail✝ = [] ↔ ∀ (a : α), a ∉ tail✝
⊢ ¬a = a → a ∈ tail✝
Tactic:
tauto
Proof state after:
no goals
Theorem: List.remove_nil
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.173581 → Type ?u.173583
α : Type u_1
β : Type ?u.173589
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
⊢ remove a [] = []
Tactic:
simp [List.remove]
Proof state after:
no goals
Theorem: List.eq_remove_cons
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.173910 → Type ?u.173912
α : Type u_1
β : Type ?u.173918
inst✝¹ : Monad m
inst✝ : DecidableEq α
q : α
l : List α
⊢ remove q (q :: l) = remove q l
Tactic:
induction l <;> simp_all [List.remove]
Proof state after:
no goals
Theorem: List.remove_singleton_of_ne
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.175397 → Type ?u.175399
α : Type u_1
β : Type ?u.175405
inst✝¹ : Monad m
inst✝ : DecidableEq α
p q : α
h : p ≠ q
⊢ remove q [p] = [p]
Tactic:
simp_all [List.remove, Ne.symm]
Proof state after:
no goals
Theorem: List.mem_remove_iff
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ remove a l ↔ b ∈ l ∧ b ≠ a
Tactic:
simp [List.remove, List.of_mem_filter]
Proof state after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ filter (fun x => !decide (x = a)) l ↔ b ∈ l ∧ ¬b = a
Theorem: List.mem_remove_iff
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ filter (fun x => !decide (x = a)) l ↔ b ∈ l ∧ ¬b = a
Tactic:
constructor
Proof state after:
case mp
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ filter (fun x => !decide (x = a)) l → b ∈ l ∧ ¬b = a

case mpr
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ l ∧ ¬b = a → b ∈ filter (fun x => !decide (x = a)) l
Theorem: List.mem_remove_iff
Proof state before:
case mp
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ filter (fun x => !decide (x = a)) l → b ∈ l ∧ ¬b = a

case mpr
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ l ∧ ¬b = a → b ∈ filter (fun x => !decide (x = a)) l
Tactic:
. intro h;
  exact ⟨mem_of_mem_filter h, by simpa using of_mem_filter h⟩;
Proof state after:
case mpr
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ l ∧ ¬b = a → b ∈ filter (fun x => !decide (x = a)) l
Theorem: List.mem_remove_iff
Proof state before:
case mpr
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ l ∧ ¬b = a → b ∈ filter (fun x => !decide (x = a)) l
Tactic:
. rintro ⟨h₁, h₂⟩;
  exact mem_filter_of_mem h₁ (by simpa using h₂);
Proof state after:
no goals
Theorem: List.mem_remove_iff
Proof state before:
case mp
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ filter (fun x => !decide (x = a)) l → b ∈ l ∧ ¬b = a
Tactic:
intro h
Proof state after:
case mp
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h : b ∈ filter (fun x => !decide (x = a)) l
⊢ b ∈ l ∧ ¬b = a
Theorem: List.mem_remove_iff
Proof state before:
case mp
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h : b ∈ filter (fun x => !decide (x = a)) l
⊢ b ∈ l ∧ ¬b = a
Tactic:
exact ⟨mem_of_mem_filter h, by simpa using of_mem_filter h⟩
Proof state after:
no goals
Theorem: List.mem_remove_iff
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h : b ∈ filter (fun x => !decide (x = a)) l
⊢ ¬b = a
Tactic:
simpa using of_mem_filter h
Proof state after:
no goals
Theorem: List.mem_remove_iff
Proof state before:
case mpr
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ l ∧ ¬b = a → b ∈ filter (fun x => !decide (x = a)) l
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case mpr.intro
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h₁ : b ∈ l
h₂ : ¬b = a
⊢ b ∈ filter (fun x => !decide (x = a)) l
Theorem: List.mem_remove_iff
Proof state before:
case mpr.intro
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h₁ : b ∈ l
h₂ : ¬b = a
⊢ b ∈ filter (fun x => !decide (x = a)) l
Tactic:
exact mem_filter_of_mem h₁ (by simpa using h₂)
Proof state after:
no goals
Theorem: List.mem_remove_iff
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h₁ : b ∈ l
h₂ : ¬b = a
⊢ (!decide (b = a)) = true
Tactic:
simpa using h₂
Proof state after:
no goals
Theorem: List.mem_of_mem_remove
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.180995 → Type ?u.180997
α : Type u_1
β : Type ?u.181003
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ remove a l
⊢ b ∈ l
Tactic:
rw [mem_remove_iff] at h
Proof state after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.180995 → Type ?u.180997
α : Type u_1
β : Type ?u.181003
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l ∧ b ≠ a
⊢ b ∈ l
Theorem: List.mem_of_mem_remove
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.180995 → Type ?u.180997
α : Type u_1
β : Type ?u.181003
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l ∧ b ≠ a
⊢ b ∈ l
Tactic:
exact h.1
Proof state after:
no goals
Theorem: List.remove_cons_self
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.181446 → Type ?u.181448
α : Type u_1
β : Type ?u.181454
inst✝¹ : Monad m
inst✝ : DecidableEq α
l : List α
a : α
⊢ remove a (a :: l) = remove a l
Tactic:
simp[remove]
Proof state after:
no goals
Theorem: List.remove_cons_of_ne
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.181909 → Type ?u.181911
α : Type u_1
β : Type ?u.181917
inst✝¹ : Monad m
inst✝ : DecidableEq α
l : List α
a b : α
ne : a ≠ b
⊢ remove b (a :: l) = a :: remove b l
Tactic:
simp_all [remove]
Proof state after:
no goals