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

Goal state before:
pp: α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : n + k + 1 < (l.insertIdx n x).length
⊢ (l.insertIdx n x)[n + k + 1] = l[n + k]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ |1 / a| = 1 / |a|

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : n + k + 1 < (l.insertIdx n x).length
⊢ (l.insertIdx n x).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
⊢ Injective fun l ↦ l.insertIdx n x

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
x : α
i j : ℕ
h : i ≤ j
⊢ (take i (l.insertIdx j x)).length = (take i l).length

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
x : α
i j : ℕ
h : i ≤ j
⊢ ∀ (i_1 : ℕ) (h₁ : i_1 < (take i (l.insertIdx j x)).length) (h₂ : i_1 < (take i l).length),
    (take i (l.insertIdx j x))[i_1] = (take i l)[i_1]

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
i j : ℕ
h : i ≤ j
⊢ (take i (l.eraseIdx j)).length = (take i l).length

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
i j : ℕ
h : i ≤ j
⊢ ∀ (i_1 : ℕ) (h₁ : i_1 < (take i (l.eraseIdx j)).length) (h₂ : i_1 < (take i l).length),
    (take i (l.eraseIdx j))[i_1] = (take i l)[i_1]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ ¬q b = true

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : (R ⇒ fun x1 x2 ↦ x1 ↔ x2) (fun x ↦ p x = true) fun x ↦ q x = true
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P (filterMap f (a :: as)) (filterMap g (b :: bs))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * a * b = 2 * a * b * (ε * ε⁻¹)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * (a * (b * (ε * ε⁻¹))) = 2 * (ε * (a * (b * ε⁻¹)))

Tactic:
mul_comm ε,

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * (a * (b * (ε⁻¹ * ε))) = 2 * (a * (b * ε⁻¹) * ε)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * a * b * (ε * ε⁻¹) = 2 * (ε * a) * b * ε⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * (ε * a) * b * ε⁻¹ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ l.set n a ~ a :: l.eraseIdx n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.length
⊢ l[n] :: l.eraseIdx n ~ l

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹ = ε * a ^ 2 + ε⁻¹ * b ^ 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m ≤ l₁.length
hn : n ≤ l₂.length
a : α
⊢ l₁.insertIdx m a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
a b c : List α
⊢ SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → α
l₁ : List γ
l₂ : List β
⊢ SublistForall₂ R (map f l₁) l₂ ↔ SublistForall₂ (fun c b ↦ R (f c) b) l₁ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
⊢ 2 * a * b ≤ ε * a ^ 2 + ε⁻¹ * b ^ 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun a c ↦ R a (f c)) l₁ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ Perm ∘r Perm = Perm

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
by

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

Goal state before:
pp: α : Type u
a b c : α
⊢ a ∈ [b, c] ↔ a = b ∨ a = c

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
hf : Involutive f
x : α
l : List α
⊢ (∃ y, y ∈ l ∧ f y = x) → f x ∈ l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
v : List β
hlu : l ~ u
huv : Forall₂ r u v
⊢ (Forall₂ r ∘r Perm) l v

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
hf : Involutive f
a : α
l : List α
⊢ a ∈ map f l ↔ f a ∈ l

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
l : List α
⊢ l.length = n + 1 ↔ ∃ h t, h :: t = l ∧ t.length = n

Tactic:
by

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

Goal state before:
pp: α : Type u
h : Injective length
x y : α
this : [x] = [y]
⊢ x = y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ Forall₂ r ∘r Perm = Perm ∘r Forall₂ r

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ((fun x1 x2 ↦ x1 = map f x2) ∘r fun x1 x2 ↦ x1 ~ x2) = fun x1 x2 ↦ x1 ~ map f x2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
hr : RightUnique r
a : List α
b : List β
h₁ : Forall₂ r a b
c : List α
d : List β
h₂ : Forall₂ r c d
h : a ~ c
this : (flip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a : α
⊢ count a l = count a (filter (fun b ↦ decide (P b)) l) + count a (filter (fun x ↦ decide ¬P x) l)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
⊢ ∀ (b : β), foldr f b l₁ = foldr f b l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ b ∈ (some b).toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
o₁ o₂ : Option α
⊢ o₁.toList ~ o₂.toList ↔ o₁ = o₂

Tactic:
by

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
x : M
xs : List M
hl : x :: xs ≠ []
⊢ (map (⇑f) (x :: xs)).prod = f (x :: xs).prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
this : l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
by

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
⊢ (map (⇑f) l).prod = f l.prod

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ Injective length ↔ Subsingleton α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
x✝ : α
⊢ x✝ ∈ l → x✝ = b ∨ x✝ = a ↔ x✝ ≠ b → x✝ ≠ a → ¬x✝ ∈ l

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ l.length = 2 ↔ l = [l.head h, l.getLast h]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl : l ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) l).prod = f (map f₁ l).prod (map f₂ l).prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
⊢ map f l ~ map f l' ↔ Relation.Comp (fun x1 x2 ↦ x1 = map f x2) (fun x1 x2 ↦ x1 ~ x2) (map f l) l'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
⊢ Relation.Comp (fun x1 x2 ↦ x1 = map f x2) (fun x1 x2 ↦ x1 ~ x2) (map f l) l' ↔ l ~ l'

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ ∀ (a : M) (b : N) (i : ι), f (f₁ i * a) (f₂ i * b) = f (f₁ i) (f₂ i) * f a b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ {x, y} = [x, y]

Tactic:
by

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

Goal state before:
pp: α : Type u
p : α → Prop
a : α
l : List α
⊢ (∃ x, x ∈ a :: l ∧ p x) → p a ∨ ∃ x, x ∈ l ∧ p x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a ~ g a
⊢ Forall₂ (fun x1 x2 ↦ x1 ~ x2) (List.map f l) (List.map g l)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) l).prod = f (map f₁ l).prod (map f₂ l).prod

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
L : List ι
f : ι → M
G : Type u_8
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
⊢ (map (⇑g ∘ f) L).prod = g (map f L).prod

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 : ℕ
⊢ (take i L).prod * (drop i L).prod = L.prod

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f g : α → List β
⊢ flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β
g : α → List β
⊢ map f l ++ flatMap g l ~ flatMap (fun x ↦ f x :: g x) l

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
⊢ [] = replicate [].length a ↔ ∀ (b : α), b ∈ [] → b = a

Tactic:
by

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

Goal state before:
pp: α : Type u
a b : α
l : List α
⊢ b :: l = replicate (b :: l).length a ↔ ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = a

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 : ℕ
p : i < L.length
⊢ (take (i + 1) L).prod = (take i L).prod * L[i]

Tactic:
by

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

Goal state before:
pp: α : Type u
m n : ℕ
a : α
⊢ replicate (m + n) a = replicate m a ++ replicate n a

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
L : List α
⊢ L ⊆ [a] ↔ ∃ n, L = replicate n a

Tactic:
by

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

Goal state before:
pp: α : Type u
a b : α
⊢ replicate 0 a = replicate 0 b ↔ 0 = 0 ∨ a = b

Tactic:
by

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

Goal state before:
pp: α : Type u
a b : α
n : ℕ
⊢ a = b ↔ n + 1 = 0 ∨ a = b

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
⊢ 0 < L.length

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
a : M
⊢ ((x :: xs).set 0 a).prod =
    ((take 0 (x :: xs)).prod * if 0 < (x :: xs).length then a else 1) * (drop (0 + 1) (x :: xs)).prod

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.head? = l.head?

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
i : ℕ
a : M
⊢ ((x :: xs).set (i + 1) a).prod =
    ((take (i + 1) (x :: xs)).prod * if i + 1 < (x :: xs).length then a else 1) * (drop (i + 1 + 1) (x :: xs)).prod

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.getLast? = l.getLast?

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
⊢ x ∈ pure y ↔ x = y

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
x✝¹ : ℕ
x✝ : M
⊢ ([].set x✝¹ x✝).prod = ((take x✝¹ []).prod * if x✝¹ < [].length then x✝ else 1) * (drop (x✝¹ + 1) []).prod

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (a :: l).reverse = l.reverse.concat a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ l.concat a = (a :: l.reverse).reverse

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
l₁ l₂ : List α
⊢ map f (l₁.reverseAux l₂) = (map f l₁).reverseAux (map f l₂)

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (l ++ [a]).getLast ⋯ = a

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
⊢ l[0]?.getD 1 * l.tail.prod = l.prod

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₂ ≠ []
⊢ (l₁ ++ l₂).getLast ⋯ = l₂.getLast h

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₂ : List α
a : α
l : List α
⊢ l.concat a ≠ []

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (l.concat a).getLast ⋯ = a

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : Inhabited M
l : List M
h : l ≠ []
⊢ l.headI * l.tail.prod = l.prod

Tactic:
by

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

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

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.Tactic.FieldSimp.Lemmas

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
n : ℤ
⊢ zpow' 0 n = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h₁ : l₁ ≠ []
h₂ : l₂ ≠ []
h₃ : l₁ = l₂
⊢ l₁.getLast h₁ = l₂.getLast h₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
⊢ zpow' a n = 0 ↔ a = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
m : ℕ
a : α
⊢ (replicate (m + 1) a).getLast ⋯ = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
n : ℤ
⊢ zpow' 1 n = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 1 = a

Tactic:
by

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

Goal state before:
pp: α : Type u
x : α
hx : x ∈ [].getLast?
⊢ ∃ h, x = [].getLast h

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
y : M
h : ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y l.prod

Tactic:
by

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

Goal state before:
pp: α : Type u
a x : α
hx : x ∈ [a].getLast?
⊢ ∃ h, x = [a].getLast h

Tactic:
by

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

Goal state before:
pp: α : Type u
a b : α
l : List α
x : α
hx : x ∈ (a :: b :: l).getLast?
⊢ ∃ h, x = (a :: b :: l).getLast h

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
x✝ : x ∈ [].getLast?
⊢ x ∈ [y].getLast?

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 0 = a / a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
ha : a ≠ 0
⊢ zpow' a 0 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
⊢ zpow' a (-n) = (zpow' a n)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u
a b : α
l : List α
c : α
hc : c ∈ (a :: b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
⊢ [].getLastI = [].getLast?.getD default

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
head✝¹ head✝ c : α
l : List α
⊢ (head✝¹ :: head✝ :: c :: l).getLastI = (head✝¹ :: head✝ :: c :: l).getLast?.getD default

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 = (map f (range n)).prod * f n

Tactic:
by

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

Goal state before:
pp: α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ : List α
hl₂ : [] ≠ []
⊢ (l₁ ++ []).getLast? = [].getLast?

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
x : α
h : x ∈ l₂.getLast?
⊢ x ∈ (l₁ ++ l₂).getLast?

Tactic:
by

Goal state after: