mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
a : α
ha : a ∈ l
ha' : a ≠ l.getLast ⋯
⊢ a ∈ l.dropLast

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ zpow' a ↑n = a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
a d : α
ha : a ∈ l
ha' : a ≠ l.getLastD d
⊢ a ≠ l.getLast ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
a : α
ha : a ∈ l
ha' : some a ≠ l.getLast?
⊢ a ≠ l.getLast ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n.succ)).prod = f 0 * (map (fun i ↦ f i.succ) (range n)).prod

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l : List α
⊢ l.head! = l.head?.getD default

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Semiring M
x₁ x₂ X₁ X₂ Y y a : M
h₁ : x₁ = a * X₁
h₂ : x₂ = a * X₂
H_atom : X₁ + X₂ = Y
hy : a * Y = y
⊢ x₁ + x₂ = y

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Ring M
x₁ x₂ X₁ X₂ Y y a : M
h₁ : x₁ = a * X₁
h₂ : x₂ = a * X₂
H_atom : X₁ - X₂ = Y
hy : a * Y = y
⊢ x₁ - x₂ = y

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
x a : α
l : List α
h : x ∈ (a :: l).head?
⊢ a :: l = x :: (a :: l).tail

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : DivInvOneMonoid M
l l_n n : M
h : l = l_n / 1
hn : l_n = n
⊢ l = n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : DivInvOneMonoid M
l l_d d : M
h : l = 1 / l_d
hn : l_d = d
⊢ l = d⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Div M
l l_n l_d n d : M
h : l = l_n / l_d
hn : l_n = n
hd : l_d = d
⊢ l = n / d

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
hl : ∀ (x : M), x ∈ l → x = 1
⊢ l.prod = 1

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
⊢ a = D * f

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : L ≠ 0
⊢ (e₁ = e₂) = (f₁ = f₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
h : l.prod ≠ 1
⊢ ∃ x, x ∈ l ∧ x ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
t s : List α
h : s ≠ []
⊢ (s ++ t).head! = s.head!

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
s t : List α
x : α
h : x ∈ s.head?
⊢ x ∈ (s ++ t).head?

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a : α
l : List α
h : l ≠ []
⊢ (l ++ [a]).tail = l.tail ++ [a]

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : MonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : PosMulMono M
inst✝ : PosMulReflectLE M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : 0 < L
⊢ (e₁ ≤ e₂) = (f₁ ≤ f₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a : α
h : a ∈ [].head?
⊢ a :: [].tail = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
⊢ b = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
⊢ a :: (b :: l).tail = b :: l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
h : [] ≠ []
⊢ [].head! ∈ [].head?

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : MonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : PosMulStrictMono M
inst✝ : PosMulReflectLT M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : 0 < L
⊢ (e₁ < e₂) = (f₁ < f₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
⊢ l.head! ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
i : Fin l.length
⊢ l[i]?.isSome = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
i : Fin l.length
⊢ l.get i = l[i]?.get ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
p : α → Prop
⊢ (∃ x, x ∈ l ∧ p x) ↔ ∃ i x, p l[i]

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
p : ℤ × M
l : NF M
⊢ (p ::ᵣ l).eval = l.eval * zpow' p.2 p.1

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
p : α → Prop
⊢ (∀ (x : α), x ∈ l → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p l[i]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
⊢ (Surjective fun n ↦ l[n]?) ↔ ∀ (x : α), x ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
i : ℕ
h : i < l.tail.length
⊢ i + 1 < l.length

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
⊢ ((r, x) ::ᵣ l).eval ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
i : ℕ
h : i < l.tail.length
h' : i + 1 < l.length
⊢ l.tail.get ⟨i, h⟩ = l.get ⟨i + 1, h'⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
k : ℕ
l : List α
h : k ≠ 0
hk : k < l.length
⊢ l[k] ∈ l.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
a b : α
⊢ a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 <
    (fun x ↦
        match x with
        | (r, x) => zpow' x r)
      (r, x)

Tactic:
simp only

Goal state after:
M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 < zpow' x r
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
l : List M
a : M
inst✝ : DecidableEq M
ha : a ∈ l
comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x
⊢ a * (l.erase a).prod = l.prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ l <+ [a] ↔ l = [] ∨ l = [a]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf a (b :: l) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 < ((r, x) ::ᵣ l).eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
h : b ≠ a
⊢ idxOf a (b :: l) = (idxOf a l).succ

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ idxOf a l = l.length ↔ ¬a ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
x : M
⊢ x = eval [(1, x)]

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval * (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ idxOf a l = 0 ↔ l = [] ∨ l.head? = some a

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l ≠ []
a : α
⊢ idxOf a l = 0 ↔ l.head hl = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : a ∈ l₁
⊢ idxOf a (l₁ ++ l₂) = idxOf a l₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : ¬a ∈ l₁
⊢ idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
⊢ idxOf a l₁ ≤ idxOf a l₂

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval * l₂.eval = l.eval
⊢ ((r₁, x) ::ᵣ l₁).eval * ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
ha : a ∈ l₁
⊢ idxOf a l₁ = idxOf a l₂

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : (a₁ ::ᵣ l₁).eval * l₂.eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
⊢ a ∈ l₁ ↔ idxOf a l₂ < l₁.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <:+ l₂
a : α
⊢ idxOf a l₂ ≤ l₂.length - l₁.length + idxOf a l₁

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval * l₂.eval = l.eval
⊢ x₁ * x₂ = l.eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <:+ l₂
a : α
⊢ idxOf a l₂ + l₁.length ≤ idxOf a l₁ + l₂.length

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
l : List α
a : α
f : α → M
hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1
⊢ (map f l).prod = f a ^ count a l

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval / (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
l : List α
a : α
f : α → M
hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1
⊢ (map f l).prod = f a ^ count a l

Tactic:
by
  induction l generalizing a with
  | nil => rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
  | cons a' as h =>
    specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
    rw [List.map_cons, List.prod_cons, count_cons, h]
    simp only [beq_iff_eq]
    split_ifs with ha'
    · rw [ha', _root_.pow_succ']
    · rw [hf a' ha' mem_cons_self, one_mul, add_zero]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
l : List M
inst✝ : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1
⊢ l.prod = (map id l).prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : ℕ
l : List α
ha : a ∈ l
⊢ a ∈ take n l ↔ idxOf a l < n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval / l₂.eval = l.eval
⊢ ((r₁, x) ::ᵣ l₁).eval / ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l
⊢ a ∈ l.dropLast ↔ idxOf a l < l.length - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l.dropLast
⊢ idxOf a l + 1 < l.length

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : (a₁ ::ᵣ l₁).eval / l₂.eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval / l₂.eval = l.eval
⊢ x₁ / x₂ = l.eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.getLast hl ∈ l.dropLast
⊢ l.length - 1 ≤ idxOf (l.getLast hl) l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
h : l.length - 1 < l.length
⊢ l ≠ []

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
a : M
i : ℕ
hlen : i ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute a a'
⊢ (l.insertIdx i a).prod = a * l.prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?
⊢ l₁ = l₂

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ L.eval * ((n, e) ::ᵣ l).eval = ((n, e) ::ᵣ l').eval

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
⊢ i ≤ (l.eraseIdx i).length

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
e : M
L l l' l₀ : NF M
h : L.eval * l.eval = l'.eval
h' : ((0, e) ::ᵣ l).eval = l₀.eval
⊢ L.eval * l₀.eval = ((0, e) ::ᵣ l').eval

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
a' : M
a'_mem : a' ∈ take i (l.eraseIdx i)
⊢ a' ∈ take i l

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
⊢ l[i] * (l.eraseIdx i).prod = l.prod

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ ((n, e) ::ᵣ L).eval * l.eval = ((n, e) ::ᵣ l').eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
he : e ≠ 0
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ ((n, e) ::ᵣ L).eval * ((-n, e) ::ᵣ l).eval = l'.eval

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝² : Monoid M
inst✝¹ : BEq M
inst✝ : LawfulBEq M
l : List M
⊢ (filter (fun x ↦ x != 1) l).prod = l.prod

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ ((n, e) ::ᵣ t).eval = ((n, e) ::ᵣ t_n).eval / t_d.eval

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h : a ∈ b :: l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
ys : List M
⊢ [].prod * ys.prod = (zipWith (fun x1 x2 ↦ x1 * x2) [] ys).prod * (drop ys.length []).prod * (drop [].length ys).prod

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ ((-n, e) ::ᵣ t).eval = t_n.eval / ((n, e) ::ᵣ t_d).eval

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
xs : List M
⊢ xs.prod * [].prod = (zipWith (fun x1 x2 ↦ x1 * x2) xs []).prod * (drop [].length xs).prod * (drop xs.length []).prod

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ ((0, e) ::ᵣ t).eval = ((1, e) ::ᵣ t_n).eval / ((1, e) ::ᵣ t_d).eval

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ l⁻¹.eval = l.eval⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝ : Inhabited α
hl : l₁.length = l₂.length
h : ∀ (n : ℕ), l₁[n]! = l₂[n]!
n : ℕ
h₁ : n < l₁.length
h₂ : n < l₂.length
⊢ l₁[n] = l₂[n]

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ 1 / l.eval = l⁻¹.eval

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ (x :: xs).prod * (y :: ys).prod =
    (zipWith (fun x1 x2 ↦ x1 * x2) (x :: xs) (y :: ys)).prod * (drop (y :: ys).length (x :: xs)).prod *
      (drop (x :: xs).length (y :: ys)).prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : idxOf a l < l.length
⊢ l.get ⟨idxOf a l, h⟩ = a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
x : M
h : x = l.eval
⊢ x⁻¹ = l⁻¹.eval

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ l.prod * l'.prod = (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ l[idxOf a l]? = some a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
⊢ (l ^ r).eval = zpow' l.eval r

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
⊢ idxOf x l = idxOf y l ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ x ^ r = (l ^ r).eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
n : Fin l.reverse.length
hn' : l.length - 1 - ↑n < l.length
⊢ l.reverse.get n = l.get ⟨l.length - 1 - ↑n, hn'⟩

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ x ^ r = (l ^ r).eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
h : l.length = 1
⊢ 0 < l.length

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r : ℤ
hr : r = 0
x : M
hx : x ≠ 0
l : NF M
⊢ ((r, x) ::ᵣ l).eval = l.eval

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
h : l.length = 1
⊢ l.length = [l.get ⟨0, ⋯⟩].length

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
l : List α
⊢ (map (fun a ↦ if p a then f a else g a) l).prod =
    (map f (filter (fun b ↦ decide (p b)) l)).prod * (map g (filter (fun a ↦ decide ¬p a) l)).prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
h : l.length = 1
⊢ ∀ (n : ℕ) (h₁ : n < l.length) (h₂ : n < [l.get ⟨0, ⋯⟩].length), l.get ⟨n, h₁⟩ = [l.get ⟨0, ⋯⟩].get ⟨n, h₂⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α → M
l : List α
⊢ (map f (filter (fun b ↦ decide (p b)) l)).prod * (map f (filter (fun x ↦ decide ¬p x) l)).prod = (map f l).prod

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r : ℤ
x : M
t t' l' : NF M
h : t.eval = t'.eval
h' : ((r, x) ::ᵣ t').eval = l'.eval
⊢ ((r, x) ::ᵣ t).eval = l'.eval

Tactic:
by

Goal state after: