awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
hq : q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
simp [takeWhile, hp, hq, IH]

Premises used: List.takeWhile
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
hq : ¬q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
simp [takeWhile, hp, hq, IH]

Premises used: List.takeWhile
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p q : α → Bool
l : List α
nil : takeWhile p (takeWhile q []) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) []
cons :
  ∀ (hd : α) (tl : List α)
    (IH : takeWhile p (takeWhile q tl) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) tl),
    takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
⊢ takeWhile p (takeWhile q l) = takeWhile (fun (a : α) ↦ decide (p a = true ∧ q a = true)) l

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH => by_cases hp : p hd <;> by_cases hq : q hd <;> simp [takeWhile, hp, hq, IH]

Premises used: List.cons, List.takeWhile, List.nil
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
simp_rw : takeWhile (fun (a : α) ↦ decide (p a = true ∧ p a = true)) l = takeWhile p l
simp_rw₁ : takeWhile (fun (a : α) ↦ decide (p a = true)) l = takeWhile p l
⊢ takeWhile p (takeWhile p l) = takeWhile p l

Tactic:
simp_rw [takeWhile_takeWhile, and_self_iff, Bool.decide_coe]

Premises used: Bool.decide_coe, List.takeWhile_takeWhile, and_self_iff
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
induction : find? p [] = head? (dropWhile (fun (x : α) ↦ !p x) [])
cons :
  ∀ (head : α) (tail : List α),
    find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head? →
      find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
⊢ find? p l = (dropWhile (fun (x : α) ↦ !p x) l).head?

Tactic:
induction l
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ find? p [] = head? (dropWhile (fun (x : α) ↦ !p x) [])

Tactic:
simp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ find? p [] = head? (dropWhile (fun (x : α) ↦ !p x) [])

Tactic:
case nil => simp

Premises used: List.nil
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
⊢ let ph := p head;
  ph = p head

Tactic:
set ph := p head with phh
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
ph : Bool := p head
phh : ph = p head
false : ∀ (phh : Bool.false = p head), find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
true : ∀ (phh : Bool.true = p head), find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?
⊢ find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?

Tactic:
rcases ph with rfl | rfl

Premises used: rfl
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : false = p head
⊢ ¬p head = true

Tactic:
simp [phh.symm]

Premises used: Eq.symm
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : false = p head
⊢ ¬p head = true

Tactic:
have phh' : ¬(p head = true) := by simp [phh.symm]
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : Bool.false = p head
phh' : ¬p head = true
false : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
false₁ : (!p head) = true
⊢ find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?

Tactic:
rw [find?_cons_of_neg phh', dropWhile_cons_of_pos]

Premises used: List.dropWhile_cons_of_pos, List.find?_cons_of_neg
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?

Tactic:
hi
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?

Tactic:
exact hi
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ (!p head) = true

Tactic:
simpa using phh
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : Bool.true = p head
true : some head = (head :: tail).head?
true₁ : ¬(!p head) = Bool.true
⊢ find? p (head :: tail) = (dropWhile (fun (x : α) ↦ !p x) (head :: tail)).head?

Tactic:
rw [find?_cons_of_pos phh.symm, dropWhile_cons_of_neg]

Premises used: List.dropWhile_cons_of_neg, List.find?_cons_of_pos, Eq.symm
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : true = p head
⊢ some head = (head :: tail).head?

Tactic:
simp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun (x : α) ↦ !p x) tail).head?
phh : true = p head
⊢ ¬(!p head) = true

Tactic:
simpa using phh
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ find? (fun (x : α) ↦ !p x) l = (dropWhile (fun (x : α) ↦ !!p x) l).head?

Tactic:
l.find?_eq_head?_dropWhile_not ?_

Premises used: List.find?_eq_head?_dropWhile_not
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∀ (x : α), p x = !!p x
⊢ find? (fun (x : α) ↦ !p x) l = (dropWhile p l).head?

Tactic:
convert! l.find?_eq_head?_dropWhile_not ?_

Premises used: List.find?_eq_head?_dropWhile_not
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ p x = !!p x

Tactic:
simp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ p x = true
⊢ dropWhile (fun (x : α) ↦ !p x) l ≠ []

Tactic:
simpa using h
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ p x = true
rw : (dropWhile (fun (x : α) ↦ !p x) l).head? = some ((dropWhile (fun (x : α) ↦ !p x) l).head ⋯)
rw₁ : (dropWhile (fun (x : α) ↦ !p x) l).head ⋯ = (dropWhile (fun (x : α) ↦ !p x) l).head ⋯
rw₂ : dropWhile (fun (x : α) ↦ !p x) l ≠ []
rw₃ : (dropWhile (fun (x : α) ↦ !p x) l).head ⋯ = (dropWhile (fun (x : α) ↦ !p x) l).head ⋯
rw₄ : dropWhile (fun (x : α) ↦ !p x) l ≠ []
⊢ find? p l = some ((dropWhile (fun (x : α) ↦ !p x) l).head ⋯)

Tactic:
rw [l.find?_eq_head?_dropWhile_not p, ← head_eq_iff_head?_eq_some]

Premises used: List.head_eq_iff_head?_eq_some, List.find?_eq_head?_dropWhile_not
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ ¬p x = true
⊢ dropWhile p l ≠ []

Tactic:
simpa using h
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ ¬p x = true
⊢ find? (fun (x : α) ↦ !p x) l = some ((dropWhile (fun (x : α) ↦ !!p x) l).head ⋯)

Tactic:
l.find?_eq_head_dropWhile_not ?_

Premises used: List.find?_eq_head_dropWhile_not
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ ¬p x = true
h₁ : ∀ (x : α), p x = !!p x
convert_2 : ∃ (x : α), x ∈ l ∧ (!p x) = true
⊢ find? (fun (x : α) ↦ !p x) l = some ((dropWhile p l).head ⋯)

Tactic:
convert! l.find?_eq_head_dropWhile_not ?_

Premises used: List.find?_eq_head_dropWhile_not
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ ¬p x = true
x : α
⊢ p x = !!p x

Tactic:
simp
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
l : List α
h : ∃ (x : α), x ∈ l ∧ ¬p x = true
⊢ ∃ (x : α), x ∈ l ∧ (!p x) = true

Tactic:
simpa using h
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
n_1 n : ℕ
simp : ¬l.getD n 0 = 0 → n < l.length
⊢ n ∈ {i ∈ Finset.range l.length | l.getD i 0 ≠ 0} ↔ l.getD n 0 ≠ 0

Tactic:
simp only [Ne, Finset.mem_filter, Finset.mem_range, and_iff_right_iff_imp]

Premises used: Ne, Finset.mem_range, and_iff_right_iff_imp, Finset.mem_filter
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
n_1 n : ℕ
contrapose! : l.length ≤ n → l.getD n 0 = 0
⊢ ¬l.getD n 0 = 0 → n < l.length

Tactic:
contrapose!
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
n_1 n : ℕ
⊢ l.length ≤ n → l.getD n 0 = 0

Tactic:
getD_eq_default _ _

Premises used: List.getD_eq_default
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
n_1 n : ℕ
⊢ l.length ≤ n → l.getD n 0 = 0

Tactic:
exact getD_eq_default _ _

Premises used: List.getD_eq_default
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
⊢ Eq (α := (a : ℕ) → M) (⇑l.toFinsupp : (a : ℕ) → M) fun (x : ℕ) ↦ l.getD x 0

Tactic:
rfl

Premises used: Option.getD, List.getD, rfl
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
i : ℕ
⊢ (l.toFinsupp : (a : ℕ) → M) i = l.getD i 0

Tactic:
rfl

Premises used: Option.getD, List.getD, rfl
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
⊢ Finsupp.support l.toFinsupp = {i ∈ Finset.range l.length | l.getD i 0 ≠ 0}

Tactic:
rfl

Premises used: Finset.filter, rfl
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
⊢ Finsupp.support l.toFinsupp ⊆ Finset.range l.length

Tactic:
simp [List.toFinsupp_support]

Premises used: List.toFinsupp_support
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
n : ℕ
hn : n < l.length
⊢ (l.toFinsupp : (a : ℕ) → M) n = getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l n hn

Tactic:
getD_eq_getElem _ _ hn

Premises used: Option.getD, List.getD, List.getD_eq_getElem
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
n : Fin l.length
⊢ (l.toFinsupp : (a : ℕ) → M) (↑n : ℕ) =
    getElem (valid := fun (xs : List M) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l n ⋯

Tactic:
getD_eq_getElem _ _ n.isLt

Premises used: Option.getD, Fin.isLt, List.getD, List.getD_eq_getElem
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
l : List M
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
n : ℕ
hn : l.length ≤ n
⊢ Eq (α := M) ((l.toFinsupp : (a : ℕ) → M) n : M) (0 : M)

Tactic:
getD_eq_default _ _ hn

Premises used: Option.getD, List.getD, List.getD_eq_default
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
inst_1 : DecidablePred fun (i : ℕ) ↦ Ne.{u_1 + 1} (α := M) (getD [] i 0) 0
h : ∀ (a : ℕ), Eq.{u_1 + 1} (α := M) ((toFinsupp [] : (a : ℕ) → M) a : M) ((0 : (a : ℕ) → M) a : M)
⊢ Eq.{u_1 + 1} (α := ℕ →₀ M) (toFinsupp []) 0

Tactic:
ext
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
inst_1 : DecidablePred fun (i : ℕ) ↦ Ne.{u_1 + 1} (α := M) (getD [] i 0) 0
a : ℕ
⊢ Eq.{u_1 + 1} (α := M) ((toFinsupp [] : (a : ℕ) → M) a : M) ((0 : (a : ℕ) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
x : M
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ [x].getD x_1 0 ≠ 0
h : Eq (α := M) (([x].toFinsupp : (a : ℕ) → M) 0 : M) ((Finsupp.single 0 x : (a : ℕ) → M) 0 : M)
h₁ : ∀ (n : ℕ), Eq (α := M) (([x].toFinsupp : (a : ℕ) → M) (n + 1) : M) ((Finsupp.single 0 x : (a : ℕ) → M) (n + 1) : M)
⊢ Eq (α := ℕ →₀ M) [x].toFinsupp (Finsupp.single 0 x)

Tactic:
ext ⟨_ | i⟩
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
x : M
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ [x].getD x_1 0 ≠ 0
⊢ Eq (α := M) (([x].toFinsupp : (a : ℕ) → M) 0 : M) ((Finsupp.single 0 x : (a : ℕ) → M) 0 : M)

Tactic:
simp
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
M : Type u_1
inst : Zero M
x : M
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ [x].getD x_1 0 ≠ 0
n : ℕ
⊢ Eq (α := M) (([x].toFinsupp : (a : ℕ) → M) (n + 1) : M) ((Finsupp.single 0 x : (a : ℕ) → M) (n + 1) : M)

Tactic:
simp
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
h :
  ∀ (n : ℕ),
    Eq (α := R) (((l₁ ++ l₂).toFinsupp : (a : ℕ) → R) n : R)
      ((HAdd.hAdd (α := ℕ →₀ R) l₁.toFinsupp (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) :
            (a : ℕ) → R)
          n :
        R)
⊢ (l₁ ++ l₂).toFinsupp =
    HAdd.hAdd (α := ℕ →₀ R) l₁.toFinsupp (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp)

Tactic:
ext n
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
n : ℕ
h :
  (l₁ ++ l₂).getD n 0 =
    HAdd.hAdd (β := R) (l₁.getD n 0) ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) n : R)
⊢ Eq (α := R) (((l₁ ++ l₂).toFinsupp : (a : ℕ) → R) n : R)
    ((HAdd.hAdd (α := ℕ →₀ R) l₁.toFinsupp (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) : (a : ℕ) → R)
        n :
      R)

Tactic:
simp only [toFinsupp_apply, Finsupp.add_apply]

Premises used: Finsupp.add_apply, List.toFinsupp_apply
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
n : ℕ
h : n < l₁.length
h₁ : n ∉ Set.range (ι := ℕ) (⇑(addLeftEmbedding l₁.length) : (a : ℕ) → ℕ)
⊢ (l₁ ++ l₂).getD n 0 =
    HAdd.hAdd (β := R) (l₁.getD n 0) ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) n : R)

Tactic:
rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]

Premises used: List.getD_append, Finsupp.embDomain_notin_range, add_zero
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
k : ℕ
h : l₁.length + k < l₁.length
⊢ False

Tactic:
lia
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
n : ℕ
h : l₁.length ≤ n
h₁ :
  ∀ (k : ℕ) (h : l₁.length ≤ l₁.length + k),
    (l₁ ++ l₂).getD (l₁.length + k) 0 =
      HAdd.hAdd (β := R) (l₁.getD (l₁.length + k) 0)
        ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) (l₁.length + k) : R)
⊢ (l₁ ++ l₂).getD n 0 =
    HAdd.hAdd (β := R) (l₁.getD n 0) ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) n : R)

Tactic:
rcases Nat.exists_eq_add_of_le h with ⟨k, rfl⟩

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
k : ℕ
h : l₁.length ≤ l₁.length + k
h₁ : l₂.getD k 0 = (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) (l₁.length + k)
⊢ (l₁ ++ l₂).getD (l₁.length + k) 0 =
    HAdd.hAdd (β := R) (l₁.getD (l₁.length + k) 0)
      ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) (l₁.length + k) : R)

Tactic:
rw [getD_append_right _ _ _ _ h, Nat.add_sub_cancel_left, getD_eq_default _ _ h, zero_add]

Premises used: List.getD_append_right, Nat.add_sub_cancel_left, zero_add, List.getD_eq_default
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
k : ℕ
h : l₁.length ≤ l₁.length + k
⊢ l₂.getD k 0 = (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) (l₁.length + k)

Tactic:
Eq.symm (Finsupp.embDomain_apply_self _ _ _)

Premises used: Finsupp.embDomain_apply_self, Eq.symm
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
k : ℕ
h : l₁.length ≤ l₁.length + k
⊢ l₂.getD k 0 = (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) (l₁.length + k)

Tactic:
exact Eq.symm (Finsupp.embDomain_apply_self _ _ _)

Premises used: Finsupp.embDomain_apply_self, Eq.symm
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
n : ℕ
⊢ n < l₁.length ∨ l₁.length ≤ n

Tactic:
cases lt_or_ge n l₁.length with
  | inl h =>
    rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
    rintro ⟨k, rfl : length l₁ + k = n⟩
    lia
  | inr h =>
    rcases Nat.exists_eq_add_of_le h with ⟨k, rfl⟩
    rw [getD_append_right _ _ _ _ h, Nat.add_sub_cancel_left, getD_eq_default _ _ h, zero_add]
    exact Eq.symm (Finsupp.embDomain_apply_self _ _ _)

Premises used: Nat.add_sub_cancel_left, zero_add, Finsupp.embDomain_apply_self, Finsupp.embDomain_notin_range, lt_or_ge, add_zero, Eq.symm, List.length, rfl
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
⊢ ([x] ++ xs).toFinsupp =
    HAdd.hAdd (α := ℕ →₀ R) [x].toFinsupp (Finsupp.embDomain (addLeftEmbedding [x].length) xs.toFinsupp)

Tactic:
toFinsupp_append [x] xs

Premises used: List.cons, List.toFinsupp_append, List.nil
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
h : Eq (α := ℕ →₀ R) (Finsupp.single 0 x) [x].toFinsupp
h₁ : addRightEmbedding 1 = addLeftEmbedding [x].length
⊢ (x :: xs).toFinsupp =
    HAdd.hAdd (α := ℕ →₀ R) (Finsupp.single 0 x) (Finsupp.embDomain (addRightEmbedding 1) xs.toFinsupp)

Tactic:
convert! toFinsupp_append [x] xs using 3

Premises used: List.cons, List.toFinsupp_append, List.nil
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
⊢ Eq (α := ℕ →₀ R) (Finsupp.single 0 x) [x].toFinsupp

Tactic:
(toFinsupp_singleton x).symm

Premises used: List.toFinsupp_singleton, Eq.symm
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
⊢ Eq (α := ℕ →₀ R) (Finsupp.single 0 x) [x].toFinsupp

Tactic:
exact (toFinsupp_singleton x).symm

Premises used: List.toFinsupp_singleton, Eq.symm
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
h :
  ∀ (n : ℕ), Eq (α := ℕ) ((addRightEmbedding 1 : (a : ℕ) → ℕ) n : ℕ) ((addLeftEmbedding [x].length : (a : ℕ) → ℕ) n : ℕ)
⊢ addRightEmbedding 1 = addLeftEmbedding [x].length

Tactic:
ext n
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
n : ℕ
⊢ Eq (α := ℕ) ((addRightEmbedding 1 : (a : ℕ) → ℕ) n : ℕ) ((addLeftEmbedding [x].length : (a : ℕ) → ℕ) n : ℕ)

Tactic:
add_comm n 1

Premises used: add_comm, OfNat.ofNat
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
n : ℕ
⊢ Eq (α := ℕ) ((addRightEmbedding 1 : (a : ℕ) → ℕ) n : ℕ) ((addLeftEmbedding [x].length : (a : ℕ) → ℕ) n : ℕ)

Tactic:
exact add_comm n 1

Premises used: add_comm, OfNat.ofNat
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
h : Eq (α := ℕ →₀ R) (Finsupp.single 0 x) [x].toFinsupp
h₁ h₂ : addRightEmbedding 1 = addLeftEmbedding [x].length
⊢ (x :: xs).toFinsupp =
    HAdd.hAdd (α := ℕ →₀ R) (Finsupp.single 0 x) (Finsupp.embDomain (addRightEmbedding 1) xs.toFinsupp)

Tactic:
classical
    convert! toFinsupp_append [x] xs using 3
    · exact (toFinsupp_singleton x).symm
    · ext n
      exact add_comm n 1