awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ (some y).isSome = true

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ (some y).isSome = true

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
mp : dlookup (β := β) x (s₂.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y

Tactic:
left
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
mp mp₁ : some y = some y
⊢ dlookup (β := β) x (s₂.entries (β := β)) = some y

Tactic:
rw [h'.2]

Premises used: And.right
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' :
  dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
mpr :
  ∀ (h' : dlookup (β := β) x (s₂.entries (β := β)) = some y),
    dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
      ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
mpr₁ :
  ∀ (h' : ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y),
    dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
      ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y

Tactic:
rcases h' with h' | h'
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
mpr : ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y

Tactic:
right
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
⊢ ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y

Tactic:
⟨?_, h'⟩

Premises used: And.intro
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
mpr : ¬x ∈ s₁.entries (β := β).keys (β := β)
⊢ ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y

Tactic:
refine ⟨?_, h'⟩
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
h'' : x ∈ s₁.entries (β := β).keys (β := β)
mpr : x ∈ s₂.keys (β := β)
⊢ False

Tactic:
apply h _ h''
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
h'' : x ∈ s₁.entries (β := β).keys (β := β)
mpr : (some y).isSome = true
⊢ x ∈ s₂.keys (β := β)

Tactic:
rw [keys, ← List.dlookup_isSome, h']

Premises used: List.dlookup_isSome, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
h'' : x ∈ s₁.entries (β := β).keys (β := β)
⊢ (some y).isSome = true

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
h'' : x ∈ s₁.entries (β := β).keys (β := β)
⊢ (some y).isSome = true

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
mpr : dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y

Tactic:
left
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
mpr mpr₁ : some y = some y
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y

Tactic:
rw [h'.2]

Premises used: And.right
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
⊢ Injective (cons a)

Tactic:
fun _ _ => tail_eq_of_cons_eq

Premises used: List.tail_eq_of_cons_eq, Function.Injective
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
⊢ Injective (β := List α) fun (a : α) ↦ [a]

Tactic:
fun _ _ h => (cons_eq_cons.1 h).1

Premises used: And.left, List.cons_eq_cons, Iff.mp, Function.Injective
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
a : α
⊢ Eq (α := Set α) {x : α | x ∈ a :: l} (insert a {x : α | x ∈ l})

Tactic:
Set.ext fun _ => mem_cons

Premises used: Set.ext, List.mem_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
pos : ∀ (hab : a = b), a = b ∨ a ≠ b ∧ a ∈ l
neg : ∀ (hab : ¬a = b), a = b ∨ a ≠ b ∧ a ∈ l
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
by_cases hab : a = b
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
Or.inl hab

Premises used: Or.inl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
exact Or.inl hab

Premises used: Or.inl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
((List.mem_cons.1 h).elim Or.inl (fun h => Or.inr ⟨hab, h⟩))

Premises used: And.intro, Iff.mp, Or.inl, List.mem_cons, Or.elim, Or.inr
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
exact ((List.mem_cons.1 h).elim Or.inl (fun h => Or.inr ⟨hab, h⟩))

Premises used: Iff.mp, Or.inl, List.mem_cons, Or.elim, Or.inr
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b c : α
rw : a = b ∨ a ∈ [c] ↔ a = b ∨ a = c
rw₁ rw₂ : a = b ∨ a = c ↔ a = b ∨ a = c
⊢ a ∈ [b, c] ↔ a = b ∨ a = c

Tactic:
rw [mem_cons, mem_singleton]

Premises used: List.mem_singleton, List.mem_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
H : Injective f
a : α
l : List α
⊢ f a ∈ map f l ↔ a ∈ l

Tactic:
⟨fun m => let ⟨_, m', e⟩ := exists_of_mem_map m; H e ▸ m', mem_map_of_mem⟩

Premises used: Membership.mem, Eq.rec, List.exists_of_mem_map, Iff.intro, List.mem_map_of_mem, _private.0.List.mem_map_of_injective.match_1
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h rwa rwa₁ rwa₂ rwa₃ : y ∈ l
⊢ f (f y) ∈ l

Tactic:
rwa [hf y]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
f : α → α
hf : Involutive f
a : α
l : List α
rw : (∃ (a_1 : α), a_1 ∈ l ∧ f a_1 = a) ↔ f a ∈ l
rw₁ rw₂ : f a ∈ l ↔ f a ∈ l
⊢ a ∈ map f l ↔ f a ∈ l

Tactic:
rw [mem_map, hf.exists_mem_and_apply_eq_iff]

Premises used: Function.Involutive.exists_mem_and_apply_eq_iff, List.mem_map
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
⊢ 0 < l.length ↔ l ≠ []

Tactic:
⟨ne_nil_of_length_pos, length_pos_of_ne_nil⟩

Premises used: List.ne_nil_of_length_pos, Iff.intro, List.length_pos_of_ne_nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
n : ℕ
l : List α
⊢ l.length = n + 1 ↔ ∃ (h : α), ∃ (t : List α), h :: t = l ∧ t.length = n

Tactic:
grind [cases List]

Premises used: List
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
mp : Injective.{u + 1, 1} (α := List α) length → Subsingleton α
mpr : Subsingleton α → Injective.{u + 1, 1} (α := List α) length
⊢ Injective.{u + 1, 1} (α := List α) length ↔ Subsingleton α

Tactic:
constructor
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
h : Injective.{u + 1, 1} (α := List α) length
⊢ Subsingleton α

Tactic:
⟨fun x y => ?_⟩

Premises used: Subsingleton.intro
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
h : Injective.{u + 1, 1} (α := List α) length
mp : ∀ (x y : α), x = y
⊢ Subsingleton α

Tactic:
refine ⟨fun x y => ?_⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
h : Injective.{u + 1, 1} (α := List α) length
x y : α
this : [x] = [y]
⊢ x = y

Tactic:
simpa using this
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
h : Injective.{u + 1, 1} (α := List α) length
x y : α
mp : [x] = [y]
⊢ x = y

Tactic:
suffices [x] = [y] by simpa using this
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
h : Injective.{u + 1, 1} (α := List α) length
x y : α
mp : [x].length = [y].length
⊢ [x] = [y]

Tactic:
apply h
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
h : Injective.{u + 1, 1} (α := List α) length
x y : α
⊢ [x].length = [y].length

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
hα : Subsingleton α
l1 l2 : List α
hl : l1.length = l2.length
mpr : ∀ ⦃l2 : List α⦄ (hl : length.{u} (α := α) [] = l2.length), [] = l2
mpr₁ :
  ∀ (head : α) (tail : List α),
    (∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2) →
      ∀ ⦃l2 : List α⦄ (hl : (head :: tail).length = l2.length), head :: tail = l2
⊢ l1 = l2

Tactic:
induction l1 generalizing l2
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
hα : Subsingleton α
l2 : List α
hl : length.{u} (α := α) [] = l2.length
mpr : ∀ (hl : length.{u} (α := α) [] = length.{u} (α := α) []), Eq.{u + 1} (α := List α) [] []
mpr₁ : ∀ (head : α) (tail : List α) (hl : length.{u} (α := α) [] = (head :: tail).length), [] = head :: tail
⊢ [] = l2

Tactic:
cases l2
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
tail_ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
l2 : List α
hl : (head :: tail).length = l2.length
mpr : ∀ (hl : (head :: tail).length = length.{u} (α := α) []), head :: tail = []
mpr₁ :
  ∀ (head_1 : α) (tail_1 : List α) (hl : (head :: tail).length = (head_1 :: tail_1).length),
    head :: tail = head_1 :: tail_1
⊢ head :: tail = l2

Tactic:
cases l2
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
hα : Subsingleton α
hl : length.{u} (α := α) [] = length.{u} (α := α) []
⊢ Eq.{u + 1} (α := List α) [] []

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
hl : length.{u} (α := α) [] = (head :: tail).length
⊢ [] = head :: tail

Tactic:
cases hl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
tail_ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
hl : (head :: tail).length = length.{u} (α := α) []
⊢ head :: tail = []

Tactic:
cases hl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
head_1 : α
tail_1 : List α
hl : (head :: tail).length = (head_1 :: tail_1).length
e_head : head = head_1
e_tail : tail = tail_1
⊢ head :: tail = head_1 :: tail_1

Tactic:
congr
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
head_1 : α
tail_1 : List α
hl : (head :: tail).length = (head_1 :: tail_1).length
⊢ head = head_1

Tactic:
subsingleton
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
head_1 : α
tail_1 : List α
hl : (head :: tail).length = (head_1 :: tail_1).length
e_tail : tail.length = tail_1.length
⊢ tail = tail_1

Tactic:
apply ih
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
head_1 : α
tail_1 : List α
hl : (head :: tail).length = (head_1 :: tail_1).length
⊢ tail.length = tail_1.length

Tactic:
simpa using hl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Subsingleton α
⊢ Injective.{u + 1, 1} (α := List α) length

Tactic:
length_injective_iff.mpr inferInstance

Premises used: Iff.mpr, inferInstance, List.length_injective_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
⊢ l.length = 2 ↔ ∃ (a : α), ∃ (b : α), l = [a, b]

Tactic:
⟨fun _ => let [a, b] := l; ⟨a, b, rfl⟩, fun ⟨_, _, e⟩ => e ▸ rfl⟩

Premises used: _private.0.List.length_eq_two.match_1, Exists, Eq.rec, List.cons, Iff.intro, Exists.intro, OfNat.ofNat, Eq.symm, Eq, List.length, rfl, _private.0.List.length_eq_two.match_2, List.nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : l ≠ []
rw : (∃ (a : α), ∃ (b : α), l = [a, b]) ↔ l = [l.head h, l.getLast h]
⊢ l.length = 2 ↔ l = [l.head h, l.getLast h]

Tactic:
rw [length_eq_two]

Premises used: List.length_eq_two
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : l ≠ []
⊢ (∃ (a : α), ∃ (b : α), l = [a, b]) ↔ l = [l.head h, l.getLast h]

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
⊢ l.length = 3 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), l = [a, b, c]

Tactic:
⟨fun _ => let [a, b, c] := l; ⟨a, b, c, rfl⟩, fun ⟨_, _, _, e⟩ => e ▸ rfl⟩

Premises used: _private.0.List.length_eq_three.match_2, Exists, Eq.rec, _private.0.List.length_eq_three.match_1, List.cons, Iff.intro, Exists.intro, OfNat.ofNat, Eq.symm, Eq, List.length, rfl, List.nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
⊢ l.length = 4 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), ∃ (d : α), l = [a, b, c, d]

Tactic:
⟨fun _ => let [a, b, c, d] := l; ⟨a, b, c, d, rfl⟩, fun ⟨_, _, _, _, e⟩ => e ▸ rfl⟩

Premises used: _private.0.List.length_eq_four.match_1, Exists, Eq.rec, List.cons, Iff.intro, Exists.intro, OfNat.ofNat, Eq.symm, Eq, List.length, rfl, _private.0.List.length_eq_four.match_2, List.nil
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l l₁ l₂ : List α
inst : DecidableEq α
⊢ LawfulSingleton α (List α)

Tactic:
{ insert_empty_eq := fun x =>
      show (if x ∈ ([] : List α) then [] else [x]) = [x] from if_neg not_mem_nil }

Premises used: LawfulSingleton.mk, if_neg, List.not_mem_nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x : α
⊢ {x} = [x]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : DecidableEq α
x : α
l : List α
h : ¬x ∈ l
⊢ insert x l = x :: l

Tactic:
insert_of_not_mem h

Premises used: List.insert_of_not_mem
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : DecidableEq α
x : α
l : List α
h : x ∈ l
⊢ insert x l = l

Tactic:
insert_of_mem h

Premises used: List.insert_of_mem
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : DecidableEq α
x y : α
h : x ≠ y
rw : ¬Membership.mem (γ := List α) {y} x
⊢ {x, y} = [x, y]

Tactic:
rw [insert_neg, singleton_eq]

Premises used: List.singleton_eq, List.insert_neg
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : DecidableEq α
x y : α
h : x ≠ y
rwa : ¬x ∈ [y]
rwa₁ rwa₂ rwa₃ rwa₄ : ¬x = y
⊢ ¬Membership.mem (γ := List α) {y} x

Tactic:
rwa [singleton_eq, mem_singleton]

Premises used: List.singleton_eq, List.mem_singleton
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
a : α
l : List α
h : ∀ (x : α), x ∈ a :: l → p x
⊢ ∀ (x : α), x ∈ l → p x

Tactic:
(forall_mem_cons.1 h).2

Premises used: And.right, List.forall_mem_cons, Iff.mp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
a : α
l : List α
h : p a
⊢ ∃ (x : α), x ∈ a :: l ∧ p x

Tactic:
⟨a, mem_cons_self, h⟩

Premises used: And.intro, Exists.intro, List.mem_cons_self
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
a : α
l : List α
⊢ (∃ (x : α), x ∈ l ∧ p x) → ∃ (x : α), x ∈ a :: l ∧ p x

Tactic:
fun ⟨x, xl, px⟩ => ⟨x, mem_cons_of_mem _ xl, px⟩

Premises used: List.mem_cons_of_mem, Membership.mem, Exists, List.cons, And, _private.0.List.exists_mem_cons_of_exists.match_1, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
a : α
l : List α
⊢ (∃ (x : α), x ∈ a :: l ∧ p x) → p a ∨ ∃ (x : α), x ∈ l ∧ p x

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Prop
a : α
l : List α
⊢ (∃ (x : α), x ∈ a :: l ∧ p x) ↔ p a ∨ ∃ (x : α), x ∈ l ∧ p x

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
l m : List α
ainm : a ∈ m
lsubm : l ⊆ m
⊢ a :: l ⊆ m

Tactic:
cons_subset.2 ⟨ainm, lsubm⟩

Premises used: Iff.mpr, List.cons_subset, And.intro
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ l : List α
l₁subl : l₁ ⊆ l
l₂subl : l₂ ⊆ l
⊢ l₁ ++ l₂ ⊆ l

Tactic:
fun _ h ↦ (mem_append.1 h).elim (@l₁subl _) (@l₂subl _)

Premises used: List.Subset, List.mem_append, Iff.mp, Or.elim
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂

Tactic:
⟨?_, map_subset f⟩

Premises used: Iff.intro, List.map_subset
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
refine : map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂
⊢ map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂

Tactic:
refine ⟨?_, map_subset f⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
rcases : ∀ (x' : α) (hx' : x' ∈ l₂) (hxx' : f x' = f x), x ∈ l₂
⊢ x ∈ l₂

Tactic:
rcases mem_map.1 (h2 (mem_map_of_mem hx)) with ⟨x', hx', hxx'⟩

Premises used: Iff.mp, List.mem_map_of_mem, List.mem_map
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
x' : α
hx' : x' ∈ l₂
hxx' : f x' = f x
⊢ x ∈ l₂

Tactic:
cases h hxx'
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
x' : α
hx' : x' ∈ l₂
hxx' : f x' = f x
hx'₁ : x ∈ l₂
⊢ f x = f x

Tactic:
cases h hxx'
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
hx' : x ∈ l₂
hxx' : f x = f x
⊢ x ∈ l₂

Tactic:
hx'
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
hx' : x ∈ l₂
hxx' : f x = f x
⊢ x ∈ l₂

Tactic:
exact hx'
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l l₁ : List α
h : l ⊆ l₁
a : α
ha : ¬a ∈ l₁
⊢ ¬a ∈ l

Tactic:
(ha <| h ·)

Premises used: Not
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
L₁ L₂ : List α
⊢ L₁.append L₂ = L₁ ++ L₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
s : List α
⊢ Injective (β := List α) fun (t : List α) ↦ s ++ t

Tactic:
fun _ _ ↦ append_cancel_left

Premises used: List.append_cancel_left, Function.Injective
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
t : List α
⊢ Injective (β := List α) fun (s : List α) ↦ s ++ t

Tactic:
fun _ _ ↦ append_cancel_right

Premises used: List.append_cancel_right, Function.Injective
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
⊢ [] = replicate (length.{u} (α := α) []) a ↔ ∀ (b : α), Membership.mem (γ := List α) [] b → b = a

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
l : List α
⊢ b :: l = replicate (b :: l).length a ↔ ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = a

Tactic:
simp [eq_replicate_length, replicate_succ]

Premises used: List.replicate_succ
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
m n : ℕ
a : α
rw rw₁ : replicate (m + n) a = replicate (m + n) a
⊢ replicate (m + n) a = replicate m a ++ replicate n a

Tactic:
rw [replicate_append_replicate]

Premises used: List.replicate_append_replicate
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
n : ℕ
a : α
⊢ replicate n a ⊆ [a]

Tactic:
fun _ h =>
  mem_singleton.2 (eq_of_mem_replicate h)

Premises used: Iff.mpr, List.Subset, List.mem_singleton, List.eq_of_mem_replicate
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
L : List α
⊢ L ⊆ [a] ↔ ∃ (n : ℕ), L = replicate n a

Tactic:
simp only [eq_replicate_iff, subset_def, mem_singleton, exists_eq_left']

Premises used: List.subset_def, exists_eq_left', List.mem_singleton, List.eq_replicate_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
n : ℕ
hn : n ≠ 0
⊢ Injective.{u + 1, u + 1} (α := α) (replicate n)

Tactic:
fun _ _ h => (eq_replicate_iff.1 h).2 _ <| mem_replicate.2 ⟨hn, rfl⟩

Premises used: Iff.mpr, And.right, And.intro, Iff.mp, List.mem_replicate, List.eq_replicate_iff, Function.Injective, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
n : ℕ
hn : n ≠ 0
⊢ replicate n a = replicate n b ↔ a = b

Tactic:
(replicate_right_injective hn).eq_iff

Premises used: Function.Injective.eq_iff, List.replicate_right_injective
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
⊢ replicate 0 a = replicate 0 b ↔ Eq (α := ℕ) 0 0 ∨ a = b

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
n : ℕ
⊢ a = b ↔ n + 1 = 0 ∨ a = b

Tactic:
simp only [n.succ_ne_zero, false_or]

Premises used: false_or, Nat.succ_ne_zero
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
⊢ Injective.{1, u + 1} (β := List α) fun (x : ℕ) ↦ replicate x a

Tactic:
LeftInverse.injective (length_replicate (n := ·))

Premises used: Function.LeftInverse.injective, List.length_replicate
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
n m : ℕ
⊢ replicate n a = replicate m a ↔ n = m

Tactic:
(replicate_left_injective a).eq_iff

Premises used: Function.Injective.eq_iff, List.replicate_left_injective
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
obtain : ∀ (n : ℕ) (h : n.succ ≠ 0), (replicate n.succ l).flatten.head? = l.head?
⊢ (replicate n l).flatten.head? = l.head?

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
n : ℕ
h : n.succ ≠ 0
nil : Eq.{u + 1} (α := Option α) (head? (flatten (replicate n.succ []))) (head? [])
cons :
  ∀ (head : α) (tail : List α),
    (replicate n.succ tail).flatten.head? = tail.head? →
      (replicate n.succ (head :: tail)).flatten.head? = (head :: tail).head?
⊢ (replicate n.succ l).flatten.head? = l.head?

Tactic:
induction l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
n : ℕ
h : n.succ ≠ 0
⊢ Eq.{u + 1} (α := Option α) (head? (flatten (replicate n.succ []))) (head? [])

Tactic:
simp [replicate]

Premises used: List.replicate
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
n : ℕ
h : n.succ ≠ 0
head : α
tail : List α
tail_ih : (replicate n.succ tail).flatten.head? = tail.head?
⊢ (replicate n.succ (head :: tail)).flatten.head? = (head :: tail).head?

Tactic:
simp [replicate]

Premises used: List.replicate