internlm/Lean-Github huggingface dataset:
Theorem: List.sup_ofFn
Proof state before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ f 0 ⊔ (ofFn fun i => f i.succ).sup = Finset.univ.sup f
Tactic:
{ simp[ih]
  have : (Finset.univ : Finset (Fin (n + 1))) = insert 0 ((Finset.univ : Finset (Fin n)).image Fin.succ) := by
    ext i; simp
  rw[this, Finset.sup_insert]; simp
  have : Finset.sup Finset.univ (fun i => f (Fin.succ i)) = Finset.sup {0}ᶜ f := by
    simpa[Function.comp] using Eq.symm <| Finset.sup_image (Finset.univ : Finset (Fin n)) Fin.succ f
  rw[this] }
Proof state after:
no goals
Theorem: List.sup_ofFn
Proof state before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ f 0 ⊔ (ofFn fun i => f i.succ).sup = Finset.univ.sup f
Tactic:
simp[ih]
Proof state after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = Finset.univ.sup f
Theorem: List.sup_ofFn
Proof state before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = Finset.univ.sup f
Tactic:
have : (Finset.univ : Finset (Fin (n + 1))) = insert 0 ((Finset.univ : Finset (Fin n)).image Fin.succ) := by
  ext i; simp
Proof state after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = Finset.univ.sup f
Theorem: List.sup_ofFn
Proof state before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = Finset.univ.sup f
Tactic:
rw[this, Finset.sup_insert]
Proof state after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ (Finset.image Fin.succ Finset.univ).sup f
Theorem: List.sup_ofFn
Proof state before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ (Finset.image Fin.succ Finset.univ).sup f
Tactic:
simp
Proof state after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ {0}ᶜ.sup f
Theorem: List.sup_ofFn
Proof state before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ {0}ᶜ.sup f
Tactic:
have : Finset.sup Finset.univ (fun i => f (Fin.succ i)) = Finset.sup {0}ᶜ f := by
  simpa[Function.comp] using Eq.symm <| Finset.sup_image (Finset.univ : Finset (Fin n)) Fin.succ f
Proof state after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this✝ : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
this : (Finset.univ.sup fun i => f i.succ) = {0}ᶜ.sup f
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ {0}ᶜ.sup f
Theorem: List.sup_ofFn
Proof state before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this✝ : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
this : (Finset.univ.sup fun i => f i.succ) = {0}ᶜ.sup f
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ {0}ᶜ.sup f
Tactic:
rw[this]
Proof state after:
no goals
Theorem: List.sup_ofFn
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
Tactic:
ext i
Proof state after:
case a
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
i : Fin (n + 1)
⊢ i ∈ Finset.univ ↔ i ∈ insert 0 (Finset.image Fin.succ Finset.univ)
Theorem: List.sup_ofFn
Proof state before:
case a
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
i : Fin (n + 1)
⊢ i ∈ Finset.univ ↔ i ∈ insert 0 (Finset.image Fin.succ Finset.univ)
Tactic:
simp
Proof state after:
no goals
Theorem: List.sup_ofFn
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (Finset.univ.sup fun i => f i.succ) = {0}ᶜ.sup f
Tactic:
simpa[Function.comp] using Eq.symm <| Finset.sup_image (Finset.univ : Finset (Fin n)) Fin.succ f
Proof state after:
no goals
Theorem: List.ofFn_get_eq_map_cast
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
⊢ (ofFn fun i => g (as.get (Fin.cast h i))) = map g as
Tactic:
ext i b
Proof state after:
case a.a
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
⊢ b ∈ (ofFn fun i => g (as.get (Fin.cast h i))).get? i ↔ b ∈ (map g as).get? i
Theorem: List.ofFn_get_eq_map_cast
Proof state before:
case a.a
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
⊢ b ∈ (ofFn fun i => g (as.get (Fin.cast h i))).get? i ↔ b ∈ (map g as).get? i
Tactic:
simp
Proof state after:
case a.a
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Theorem: List.ofFn_get_eq_map_cast
Proof state before:
case a.a
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Tactic:
by_cases hi : i < n
Proof state after:
case pos
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b

case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Theorem: List.ofFn_get_eq_map_cast
Proof state before:
case pos
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b

case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Tactic:
{ simp[hi, List.ofFnNthVal, List.get?_eq_get (h ▸ hi)] }
Proof state after:
case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Theorem: List.ofFn_get_eq_map_cast
Proof state before:
case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Tactic:
{ simp[hi, List.ofFnNthVal, List.get?_len_le (le_of_not_lt $ h ▸ hi)] }
Proof state after:
no goals
Theorem: List.ofFn_get_eq_map_cast
Proof state before:
case pos
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Tactic:
simp[hi, List.ofFnNthVal, List.get?_eq_get (h ▸ hi)]
Proof state after:
no goals
Theorem: List.ofFn_get_eq_map_cast
Proof state before:
case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Tactic:
simp[hi, List.ofFnNthVal, List.get?_len_le (le_of_not_lt $ h ▸ hi)]
Proof state after:
no goals
Theorem: List.take_map_range
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n m : ℕ
f : ℕ → α
⊢ take m (map f (range n)) = map f (range (min n m))
Tactic:
induction' m with m ih
Proof state after:
case zero
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
⊢ take 0 (map f (range n)) = map f (range (min n 0))

case succ
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
⊢ take (m + 1) (map f (range n)) = map f (range (min n (m + 1)))
Theorem: List.take_map_range
Proof state before:
case zero
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
⊢ take 0 (map f (range n)) = map f (range (min n 0))
Tactic:
simp
Proof state after:
no goals
Theorem: List.take_map_range
Proof state before:
case succ
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
⊢ take (m + 1) (map f (range n)) = map f (range (min n (m + 1)))
Tactic:
simp[take_succ, ih]
Proof state after:
case succ
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
⊢ map f (range (min n m)) ++ (Option.map f ((range n).get? m)).toList = map f (range (min n (m + 1)))
Theorem: List.take_map_range
Proof state before:
case succ
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
⊢ map f (range (min n m)) ++ (Option.map f ((range n).get? m)).toList = map f (range (min n (m + 1)))
Tactic:
rcases hm : ((range n).get? m) with (_ | i) <;> simp
Proof state after:
case succ.none
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
⊢ map f (range (min n m)) = map f (range (min n (m + 1)))

case succ.some
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
⊢ map f (range (min n m)) ++ [f i] = map f (range (min n (m + 1)))
Theorem: List.take_map_range
Proof state before:
case succ.none
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
⊢ map f (range (min n m)) = map f (range (min n (m + 1)))
Tactic:
have : n ≤ m := by simpa using get?_eq_none.mp hm
Proof state after:
case succ.none
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
this : n ≤ m
⊢ map f (range (min n m)) = map f (range (min n (m + 1)))
Theorem: List.take_map_range
Proof state before:
case succ.none
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
this : n ≤ m
⊢ map f (range (min n m)) = map f (range (min n (m + 1)))
Tactic:
simp[Nat.min_eq_left this, Nat.min_eq_left (Nat.le_step this)]
Proof state after:
no goals
Theorem: List.take_map_range
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
⊢ n ≤ m
Tactic:
simpa using get?_eq_none.mp hm
Proof state after:
no goals
Theorem: List.take_map_range
Proof state before:
case succ.some
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
⊢ map f (range (min n m)) ++ [f i] = map f (range (min n (m + 1)))
Tactic:
have : m < n ∧ m = i := by simpa using get?_eq_some.mp hm
Proof state after:
case succ.some
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
this : m < n ∧ m = i
⊢ map f (range (min n m)) ++ [f i] = map f (range (min n (m + 1)))
Theorem: List.take_map_range
Proof state before:
case succ.some
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
this : m < n ∧ m = i
⊢ map f (range (min n m)) ++ [f i] = map f (range (min n (m + 1)))
Tactic:
rcases this with ⟨lt, rfl⟩
Proof state after:
case succ.some.intro
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
lt : m < n
hm : (range n).get? m = some m
⊢ map f (range (min n m)) ++ [f m] = map f (range (min n (m + 1)))
Theorem: List.take_map_range
Proof state before:
case succ.some.intro
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
lt : m < n
hm : (range n).get? m = some m
⊢ map f (range (min n m)) ++ [f m] = map f (range (min n (m + 1)))
Tactic:
simp[Nat.min_eq_right lt, Nat.min_eq_right (le_of_lt lt), range_succ]
Proof state after:
no goals
Theorem: List.take_map_range
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
⊢ m < n ∧ m = i
Tactic:
simpa using get?_eq_some.mp hm
Proof state after:
no goals
Theorem: List.bind_toList_some
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
⊢ (bs.bind fun i => (f i).toList) = map g bs
Tactic:
have : bs.bind (fun i => (f i).toList) = bs.bind (pure ∘ g) :=
  List.bind_congr (by simp; intro m hm; simp[h _ hm])
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
this : (bs.bind fun i => (f i).toList) = bs.bind (pure ∘ g)
⊢ (bs.bind fun i => (f i).toList) = map g bs
Theorem: List.bind_toList_some
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
this : (bs.bind fun i => (f i).toList) = bs.bind (pure ∘ g)
⊢ (bs.bind fun i => (f i).toList) = map g bs
Tactic:
rw[this, List.bind_pure_eq_map]
Proof state after:
no goals
Theorem: List.bind_toList_some
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
⊢ ∀ x ∈ bs, (f x).toList = (pure ∘ g) x
Tactic:
simp
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
⊢ ∀ x ∈ bs, f x = some (g x)
Theorem: List.bind_toList_some
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
⊢ ∀ x ∈ bs, f x = some (g x)
Tactic:
intro m hm
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
m : β
hm : m ∈ bs
⊢ f m = some (g m)
Theorem: List.bind_toList_some
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
m : β
hm : m ∈ bs
⊢ f m = some (g m)
Tactic:
simp[h _ hm]
Proof state after:
no goals
Theorem: List.mapM'_eq_none_iff
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
l : List α
⊢ mapM' f l = none ↔ ∃ a ∈ l, f a = none
Tactic:
induction' l with a l ih <;> simp[Option.bind_eq_bind]
Proof state after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) ↔ f a = none ∨ ∃ a ∈ l, f a = none
Theorem: List.mapM'_eq_none_iff
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) ↔ f a = none ∨ ∃ a ∈ l, f a = none
Tactic:
{ constructor
  { intros H
    rcases hb : f a with (_ | b); { simp }
    rcases hbs : mapM' f l with (_ | bs)
    { exact Or.inr (ih.mp hbs) }
    { have : False := by simpa[Option.pure_eq_some] using (H b hb) bs hbs
      contradiction } }
  { rintro (h | h)
    { simp[h] }
    { have := ih.mpr h; simp[this] } } }
Proof state after:
no goals
Theorem: List.mapM'_eq_none_iff
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) ↔ f a = none ∨ ∃ a ∈ l, f a = none
Tactic:
constructor
Proof state after:
case cons.mp
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) → f a = none ∨ ∃ a ∈ l, f a = none

case cons.mpr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (f a = none ∨ ∃ a ∈ l, f a = none) → ∀ (a_2 : β), f a = some a_2 → ∀ (a : List β), ¬mapM' f l = some a
Theorem: List.mapM'_eq_none_iff
Proof state before:
case cons.mp
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) → f a = none ∨ ∃ a ∈ l, f a = none

case cons.mpr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (f a = none ∨ ∃ a ∈ l, f a = none) → ∀ (a_2 : β), f a = some a_2 → ∀ (a : List β), ¬mapM' f l = some a
Tactic:
{ intros H
  rcases hb : f a with (_ | b); { simp }
  rcases hbs : mapM' f l with (_ | bs)
  { exact Or.inr (ih.mp hbs) }
  { have : False := by simpa[Option.pure_eq_some] using (H b hb) bs hbs
    contradiction } }
Proof state after:
case cons.mpr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (f a = none ∨ ∃ a ∈ l, f a = none) → ∀ (a_2 : β), f a = some a_2 → ∀ (a : List β), ¬mapM' f l = some a
Theorem: List.mapM'_eq_none_iff
Proof state before:
case cons.mpr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (f a = none ∨ ∃ a ∈ l, f a = none) → ∀ (a_2 : β), f a = some a_2 → ∀ (a : List β), ¬mapM' f l = some a
Tactic:
{ rintro (h | h)
  { simp[h] }
  { have := ih.mpr h; simp[this] } }
Proof state after:
no goals
Theorem: List.mapM'_eq_none_iff
Proof state before:
case cons.mp
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) → f a = none ∨ ∃ a ∈ l, f a = none
Tactic:
intros H
Proof state after:
case cons.mp
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
⊢ f a = none ∨ ∃ a ∈ l, f a = none