awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
n : ℕ
zero : IsChain r (range 0) ↔ ∀ (m : ℕ), m < HSub.hSub (α := ℕ) 0 1 → r m m.succ
succ :
  ∀ (n : ℕ) (hn : IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ),
    IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m < n + 1 - 1 → r m m.succ
⊢ IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    simp only [range_succ, Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt] at hn ⊢
    cases n with
    | zero => simp
    | succ n =>
      simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]

Premises used: Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt, Nat.succ_eq_add_one, and_true, List.append_assoc, List.IsChain.singleton, List.nil_append, List.isChain_append_cons_cons, Nat.zero, Nat.add_lt_add_iff_right, Nat.succ, List.cons_append, Nat.forall_lt_succ_right, List.range_succ
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
n : ℕ
rw : (∀ (m : ℕ), m < n.succ - 1 → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
rw₁ : (∀ (m : ℕ), m < n + 1 - 1 → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
rw₂ rw₃ : (∀ (m : ℕ), m < n → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
⊢ IsChain r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
rw [isChain_range, succ_eq_add_one, Nat.add_one_sub_one]

Premises used: Nat.add_one_sub_one, Nat.succ_eq_add_one, List.isChain_range
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
n a : ℕ
rw : r a 0 → (IsChain r (0 :: map succ (range n)) ↔ IsChain r (0 :: map succ (range n)))
⊢ IsChain r (a :: range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
rw [range_succ_eq_map, isChain_cons_cons, and_congr_right_iff,
    ← isChain_range_succ, range_succ_eq_map]

Premises used: and_congr_right_iff, List.range_succ_eq_map, List.isChain_cons_cons, List.isChain_range_succ
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (IsChain r (0 :: map succ (range n)) ↔ IsChain r (0 :: map succ (range n)))

Tactic:
fun _ => Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (IsChain r (0 :: map succ (range n)) ↔ IsChain r (0 :: map succ (range n)))

Tactic:
exact fun _ => Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.List.Range
Goal:
⊢ Pairwise Disjoint (ranges [])

Tactic:
Pairwise.nil

Premises used: List.Pairwise.nil, List.ranges
-- Module: Mathlib.Data.List.Range
Goal:
⊢ Pairwise Disjoint (ranges [])

Tactic:
exact Pairwise.nil

Premises used: List.Pairwise.nil
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
cons :
  (∀ (a' : List ℕ),
      Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) a' → (range a).Disjoint a') ∧
    Pairwise (α := List ℕ) Disjoint (map (map fun (x : ℕ) ↦ a + x) l.ranges)
⊢ Pairwise Disjoint (a :: l).ranges

Tactic:
simp only [ranges, pairwise_cons]

Premises used: List.pairwise_cons, List.ranges
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
cons :
  ∀ (a' : List ℕ),
    Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) a' → (range a).Disjoint a'
cons₁ : Pairwise (α := List ℕ) Disjoint (map (map fun (x : ℕ) ↦ a + x) l.ranges)
⊢ (∀ (a' : List ℕ),
      Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) a' → (range a).Disjoint a') ∧
    Pairwise (α := List ℕ) Disjoint (map (map fun (x : ℕ) ↦ a + x) l.ranges)

Tactic:
constructor
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s : List ℕ
hs : Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) s
cons :
  ∀ (s' : List ℕ),
    s' ∈ l.ranges →
      ∀
        (hs :
          Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) (map (fun (x : ℕ) ↦ a + x) s')),
        (range a).Disjoint (map (fun (x : ℕ) ↦ a + x) s')
⊢ (range a).Disjoint s

Tactic:
obtain ⟨s', _, rfl⟩ := mem_map.mp hs

Premises used: Iff.mp, List.mem_map, rfl
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left : s' ∈ l.ranges
hs : Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) (map (fun (x : ℕ) ↦ a + x) s')
u : ℕ
hu : u ∈ range a
cons : (∃ (a_1 : ℕ), a_1 ∈ s' ∧ a + a_1 = u) → False
⊢ Membership.mem (γ := List ℕ) (map (fun (x : ℕ) ↦ a + x) s') u → False

Tactic:
rw [mem_map]

Premises used: List.mem_map
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left : s' ∈ l.ranges
hs : Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) (map (fun (x : ℕ) ↦ a + x) s')
u : ℕ
hu : u ∈ range a
⊢ u < a

Tactic:
rw [mem_range] at hu

Premises used: List.mem_range
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left : s' ∈ l.ranges
hs : Membership.mem (γ := List (List ℕ)) (map (map fun (x : ℕ) ↦ a + x) l.ranges) (map (fun (x : ℕ) ↦ a + x) s')
u : ℕ
hu : u < a
⊢ (∃ (a_1 : ℕ), a_1 ∈ s' ∧ a + a_1 = u) → False

Tactic:
lia
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
cons :
  Pairwise (fun (a_1 b : List ℕ) ↦ Disjoint (α := ℕ) (map (fun (x : ℕ) ↦ a + x) a_1) (map (fun (x : ℕ) ↦ a + x) b))
    l.ranges
⊢ Pairwise (α := List ℕ) Disjoint (map (map fun (x : ℕ) ↦ a + x) l.ranges)

Tactic:
rw [pairwise_map]

Premises used: List.pairwise_map
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
apply :
  ∀ {a_1 b : List ℕ}, a_1.Disjoint b → Disjoint (α := ℕ) (map (fun (x : ℕ) ↦ a + x) a_1) (map (fun (x : ℕ) ↦ a + x) b)
⊢ Pairwise (fun (a_1 b : List ℕ) ↦ Disjoint (α := ℕ) (map (fun (x : ℕ) ↦ a + x) a_1) (map (fun (x : ℕ) ↦ a + x) b))
    l.ranges

Tactic:
apply Pairwise.imp _ hl

Premises used: List.Pairwise.imp
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
hf : Function.Injective (β := ℕ) fun (x : ℕ) ↦ a + x
⊢ u.Disjoint v → Disjoint (α := ℕ) (map (fun (x : ℕ) ↦ a + x) u) (map (fun (x : ℕ) ↦ a + x) v)

Tactic:
apply disjoint_map

Premises used: List.disjoint_map
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
⊢ Function.Injective (β := ℕ) fun (x : ℕ) ↦ a + x

Tactic:
fun u v => Nat.add_left_cancel

Premises used: Nat.add_left_cancel, Function.Injective
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
⊢ Function.Injective (β := ℕ) fun (x : ℕ) ↦ a + x

Tactic:
exact fun u v => Nat.add_left_cancel

Premises used: Nat.add_left_cancel
-- Module: Mathlib.Data.List.Range
Goal:
l : List ℕ
nil : Pairwise Disjoint (ranges [])
cons : ∀ (a : ℕ) (l : List ℕ) (hl : Pairwise Disjoint l.ranges), Pairwise Disjoint (a :: l).ranges
⊢ Pairwise Disjoint l.ranges

Tactic:
induction l with
  | nil => exact Pairwise.nil
  | cons a l hl =>
    simp only [ranges, pairwise_cons]
    constructor
    · intro s hs
      obtain ⟨s', _, rfl⟩ := mem_map.mp hs
      intro u hu
      rw [mem_map]
      rw [mem_range] at hu
      lia
    · rw [pairwise_map]
      apply Pairwise.imp _ hl
      intro u v
      apply disjoint_map
      exact fun u v => Nat.add_left_cancel

Premises used: List.mem_range, List.pairwise_map, List.cons, List.pairwise_cons, List.Pairwise.nil, Nat.add_left_cancel, List.mem_map, List.ranges, List.disjoint_map, rfl, List.nil
-- Module: Mathlib.Data.List.Range
Goal:
⊢ map length (ranges []) = []

Tactic:
simp only [ranges, map_nil]

Premises used: List.ranges, List.map_nil
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
cons : map (Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x)) l.ranges = l
⊢ map length (a :: l).ranges = a :: l

Tactic:
simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]

Premises used: List.map_cons, List.length_range, List.map_map, List.cons.injEq, List.ranges, true_and
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
rw : map length l.ranges
| l

Tactic:
rw [← hl]
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
cons : map (Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x)) l.ranges = map length l.ranges
⊢ map (Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x)) l.ranges = l

Tactic:
conv_rhs => rw [← hl]
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
cons : ∀ (a_1 : List ℕ), a_1 ∈ l.ranges → Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x) a_1 = a_1.length
⊢ map (Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x)) l.ranges = map length l.ranges

Tactic:
apply map_congr_left

Premises used: List.map_congr_left
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
s : List ℕ
cons : s ∈ l.ranges → Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x) s = s.length
⊢ s ∈ l.ranges → Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x) s = s.length

Tactic:
_
-- Module: Mathlib.Data.List.Range
Goal:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
s : List ℕ
h : s ∈ l.ranges
⊢ Function.comp (β := List ℕ) length (map fun (x : ℕ) ↦ a + x) s = s.length

Tactic:
simp only [Function.comp_apply, length_map]

Premises used: List.length_map, Function.comp_apply
-- Module: Mathlib.Data.List.Range
Goal:
l : List ℕ
nil : map length (ranges []) = []
cons : ∀ (a : ℕ) (l : List ℕ) (hl : map length l.ranges = l), map length (a :: l).ranges = a :: l
⊢ map length l.ranges = l

Tactic:
induction l with
  | nil => simp only [ranges, map_nil]
  | cons a l hl => -- (a :: l)
    simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]
    conv_rhs => rw [← hl]
    apply map_congr_left
    intro s _
    simp only [Function.comp_apply, length_map]

Premises used: List.map_cons, List.length_range, List.map_congr_left, List.map_map, List.cons, List.cons.injEq, List.length_map, Function.comp_apply, List.ranges, true_and, List.map_nil, List.nil
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
x : α
l : List (Option α)
⊢ (some x :: l).reduceOption = x :: l.reduceOption

Tactic:
simp only [reduceOption, filterMap, id]

Premises used: id, List.reduceOption, List.filterMap
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
⊢ (none :: l).reduceOption = l.reduceOption

Tactic:
simp only [reduceOption, filterMap, id]

Premises used: id, List.reduceOption, List.filterMap
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) (reduceOption []) []

Tactic:
rfl

Premises used: List.filterMap, rfl
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ (map (Option.map f) []).reduceOption = map f (reduceOption [])

Tactic:
simp only [reduceOption_nil, map_nil]

Premises used: List.reduceOption_nil, List.map_nil
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
β : Type u_2
f : α → β
hd : Option α
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
cons : (map (Option.map f) (none :: tl)).reduceOption = map f (none :: tl).reduceOption
cons₁ : ∀ (val : α), (map (Option.map f) (some val :: tl)).reduceOption = map f (some val :: tl).reduceOption
⊢ (map (Option.map f) (hd :: tl)).reduceOption = map f (hd :: tl).reduceOption

Tactic:
cases hd
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
⊢ (map (Option.map f) (none :: tl)).reduceOption = map f (none :: tl).reduceOption

Tactic:
simpa [Option.map_some, map, eq_self_iff_true, reduceOption_cons_of_some] using hl

Premises used: List.map, Option.map_some, List.reduceOption_cons_of_some, eq_self_iff_true
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
val : α
⊢ (map (Option.map f) (some val :: tl)).reduceOption = map f (some val :: tl).reduceOption

Tactic:
simpa [Option.map_some, map, eq_self_iff_true, reduceOption_cons_of_some] using hl

Premises used: List.map, Option.map_some, List.reduceOption_cons_of_some, eq_self_iff_true
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
β : Type u_2
l : List (Option α)
f : α → β
nil : (map (Option.map f) []).reduceOption = map f (reduceOption [])
cons :
  ∀ (hd : Option α) (tl : List (Option α)) (hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption),
    (map (Option.map f) (hd :: tl)).reduceOption = map f (hd :: tl).reduceOption
⊢ (map (Option.map f) l).reduceOption = map f l.reduceOption

Tactic:
induction l with
  | nil => simp only [reduceOption_nil, map_nil]
  | cons hd tl hl =>
    cases hd <;> simpa [Option.map_some, map, eq_self_iff_true, reduceOption_cons_of_some] using hl

Premises used: List.map, List.cons, Option.map_some, List.reduceOption_cons_of_some, List.reduceOption_nil, eq_self_iff_true, List.map_nil, List.nil
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l l' : List (Option α)
⊢ (l ++ l').reduceOption = l.reduceOption ++ l'.reduceOption

Tactic:
filterMap_append

Premises used: List.filterMap_append
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
n : ℕ
rw rw₁ : Eq.{u_1 + 1} (α := List α) [] []
⊢ Eq.{u_1 + 1} (α := List α) (filterMap id (replicate n none)) []

Tactic:
rw [filterMap_replicate_of_none (id_def _)]

Premises used: id_def, List.filterMap_replicate_of_none
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
rw : (∀ (a : Option α), a ∈ l → id a = none) ↔ ∃ (n : ℕ), l = replicate n none
⊢ filterMap id l = [] ↔ ∃ (n : ℕ), l = replicate n none

Tactic:
rw [filterMap_eq_nil_iff]

Premises used: List.filterMap_eq_nil_iff
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
mp : (∀ (a : Option α), a ∈ l → id a = none) → ∃ (n : ℕ), l = replicate n none
mpr : (∃ (n : ℕ), l = replicate n none) → ∀ (a : Option α), a ∈ l → id a = none
⊢ (∀ (a : Option α), a ∈ l → id a = none) ↔ ∃ (n : ℕ), l = replicate n none

Tactic:
constructor
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
h : ∀ (a : Option α), a ∈ l → id a = none
⊢ ∃ (n : ℕ), l = replicate n none

Tactic:
⟨l.length, eq_replicate_of_mem h⟩

Premises used: List.eq_replicate_of_mem, Exists.intro, List.length
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
h : ∀ (a : Option α), a ∈ l → id a = none
⊢ ∃ (n : ℕ), l = replicate n none

Tactic:
exact ⟨l.length, eq_replicate_of_mem h⟩
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
⊢ (∃ (n : ℕ), l = replicate n none) → ∀ (a : Option α), a ∈ l → id a = none

Tactic:
grind
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
a : α
mp : filterMap id l = [a] → ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
mpr : (∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none) → filterMap id l = [a]
⊢ filterMap id l = [a] ↔ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none

Tactic:
constructor
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
a : α
h : filterMap id l = [a]
⊢ ∃ (l₁ : List (Option α)),
    ∃ (a_1 : Option α),
      ∃ (l₂ : List (Option α)),
        l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : Option α), x ∈ l₁ → id x = none) ∧ id a_1 = some a ∧ filterMap id l₂ = []

Tactic:
rw [filterMap_eq_cons_iff] at h

Premises used: List.filterMap_eq_cons_iff
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
a : α
h :
  ∃ (l₁ : List (Option α)),
    ∃ (a_1 : Option α),
      ∃ (l₂ : List (Option α)),
        l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : Option α), x ∈ l₁ → id x = none) ∧ id a_1 = some a ∧ filterMap id l₂ = []
mp :
  ∀ (l₁ l₂ : List (Option α)) (hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none) (hl₂ : filterMap id l₂ = [])
    (h : l = l₁ ++ some a :: l₂), ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
⊢ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none

Tactic:
obtain ⟨l₁, _, l₂, h, hl₁, ⟨⟩, hl₂⟩ := h
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : filterMap id l₂ = []
h : l = l₁ ++ some a :: l₂
⊢ ∀ (a : Option α), a ∈ l₂ → id a = none

Tactic:
rw [filterMap_eq_nil_iff] at hl₂

Premises used: List.filterMap_eq_nil_iff
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : filterMap id l₂ = []
h : l = l₁ ++ some a :: l₂
hl₃ : ∀ (a : Option α), a ∈ l₂ → id a = none
⊢ l = l₁ ++ some a :: l₂

Tactic:
rw [filterMap_eq_nil_iff] at hl₂

Premises used: List.filterMap_eq_nil_iff
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : ∀ (a : Option α), a ∈ l₂ → id a = none
h : l = l₁ ++ some a :: l₂
⊢ l₁ = replicate l₁.length none

Tactic:
apply eq_replicate_of_mem at hl₁

Premises used: List.eq_replicate_of_mem
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₂ : ∀ (a : Option α), a ∈ l₂ → id a = none
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
⊢ l₂ = replicate l₂.length none

Tactic:
apply eq_replicate_of_mem at hl₂

Premises used: List.eq_replicate_of_mem
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
mp :
  ∃ (m : ℕ),
    ∃ (n : ℕ),
      replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none
⊢ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none

Tactic:
rw [h, hl₁, hl₂]
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
w w₁ : ℕ
h₁ :
  replicate l₁.length none ++ some a :: replicate l₂.length none =
    replicate l₁.length none ++ some a :: replicate l₂.length none
⊢ ∃ (m : ℕ),
    ∃ (n : ℕ),
      replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none

Tactic:
use l₁.length, l₂.length

Premises used: List.length
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
a : α
w w_1 : ℕ
h : l = replicate w none ++ some a :: replicate w_1 none
⊢ filterMap id l = [a]

Tactic:
simp only [h, filterMap_append, filterMap_cons_some, filterMap_replicate_of_none, id_eq,
      nil_append, Option.some.injEq]

Premises used: Option.some.injEq, List.nil_append, List.filterMap_append, List.filterMap_replicate_of_none, List.filterMap_cons_some, id_eq
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l'₁ l'₂ : List α
⊢ filterMap id l = l'₁ ++ l'₂ ↔
    ∃ (l₁ : List (Option α)), ∃ (l₂ : List (Option α)), l = l₁ ++ l₂ ∧ filterMap id l₁ = l'₁ ∧ filterMap id l₂ = l'₂

Tactic:
filterMap_eq_append_iff

Premises used: List.filterMap_eq_append_iff
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l'₁ l'₂ : List α
⊢ filterMap id l = l'₁ ++ l'₂ ↔
    ∃ (l₁ : List (Option α)), ∃ (l₂ : List (Option α)), l = l₁ ++ l₂ ∧ filterMap id l₁ = l'₁ ∧ filterMap id l₂ = l'₂

Tactic:
exact filterMap_eq_append_iff

Premises used: List.filterMap_eq_append_iff
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
rw :
  l.reduceOption = l' ++ [a] ↔
    ∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
⊢ l.reduceOption = l'.concat a ↔
    ∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
rw [concat_eq_append]

Premises used: List.concat_eq_append
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
mp :
  l.reduceOption = l' ++ [a] →
    ∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
mpr :
  (∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []) →
    l.reduceOption = l' ++ [a]
⊢ l.reduceOption = l' ++ [a] ↔
    ∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
constructor
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : l.reduceOption = l' ++ [a]
⊢ ∃ (l₁ : List (Option α)), ∃ (l₂ : List (Option α)), l = l₁ ++ l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [a]

Tactic:
rw [reduceOption_eq_append_iff] at h

Premises used: List.reduceOption_eq_append_iff
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : ∃ (l₁ : List (Option α)), ∃ (l₂ : List (Option α)), l = l₁ ++ l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [a]
mp :
  ∀ (l₁ w : List (Option α)) (h : l = l₁ ++ w) (hl₁ : l₁.reduceOption = l') (hl₂ : w.reduceOption = [a]),
    ∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
⊢ ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
obtain ⟨l₁, _, h, hl₁, hl₂⟩ := h
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
hl₂ : w.reduceOption = [a]
⊢ ∃ (m : ℕ), ∃ (n : ℕ), w = replicate m none ++ some a :: replicate n none

Tactic:
rw [reduceOption_eq_singleton_iff] at hl₂

Premises used: List.reduceOption_eq_singleton_iff
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
hl₂ : ∃ (m : ℕ), ∃ (n : ℕ), w = replicate m none ++ some a :: replicate n none
mp :
  ∀ (m n : ℕ) (hl₂ : w = replicate m none ++ some a :: replicate n none),
    ∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
⊢ ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
obtain ⟨m, n, hl₂⟩ := hl₂
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w = replicate m none ++ some a :: replicate n none
h₁ :
  l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
⊢ ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
use l₁ ++ replicate m none, replicate n none

Premises used: List.replicate, Option.none