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

Goal state before:
pp: case inl.intro
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
hn : n < l₂.length
hnm : l₂[n] = l₁[m]
⊢ l₁ ~ l₂ ↔ l₁ ~ l₂

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
]

Goal state after:
case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
⊢ l₁ ~ l₂ ↔ l₁ ~ l₂

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ y ∈ l

Tactic:
]

Goal state after:
α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ y ∈ l
Module: Mathlib.Data.List.Basic

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

Tactic:
]

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 Forall₂ r) ∘r Perm) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d

Tactic:
]

Goal state after:
α : 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 Forall₂ r) ∘r Perm) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ f x✝ (f y✝ (foldr f b l₂✝)) = f x✝ (f y✝ (foldr f b l₂✝))

Tactic:
]

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
  refine ⟨fun p => ?_, fun e => e ▸ Perm.refl _⟩
  rcases o₁ with - | a <;> rcases o₂ with - | b; · rfl
  · cases p.length_eq
  · cases p.length_eq
  · exact Option.mem_toList.1 (p.symm.subset <| by simp)

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
⊢ (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:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (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]
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✝ ∈ l → x✝ = b ∨ x✝ = a

Tactic:
]

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

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ (∃ a b, l = [a, b]) ↔ l = [l.head h, l.getLast h]

Tactic:
]

Goal state after:
α : Type u
l : List α
h : l ≠ []
⊢ (∃ a b, l = [a, b]) ↔ l = [l.head h, l.getLast h]
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' ↔ (fun x1 x2 ↦ x1 ~ map f x2) (map f l) l'

Tactic:
]

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]

pp: α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x ∈ {y}

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x ∈ {y}
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x = y

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x = y
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
⊢ ∀ (x : α), x ∈ l → f x ~ g x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a ~ g a
⊢ ∀ (x : α), x ∈ l → f x ~ g x
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
⊢ foldr (fun x y ↦ f (f₁ x) (f₂ x) * y) 1 l = foldr (fun x y ↦ f (f₁ x) (f₂ x) * y) 1 l

Tactic:
]

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 = (map (⇑g ∘ f) L).prod

Tactic:
]

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

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

Tactic:
]

Goal state after:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l
⊢ flatMap f l ++ g a ++ flatMap g l ~ g a ++ flatMap f l ++ flatMap g l
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 L).prod * [L[i]].prod = (take i L).prod * L[i]

Tactic:
]

Goal state after:
M : Type u_4
inst✝ : Monoid M
L : List M
i : ℕ
p : i < L.length
⊢ (take i L).prod * [L[i]].prod = (take i L).prod * L[i]
Module: Mathlib.Data.List.Basic

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
l : List α
a : α
⊢ [a].reverse ++ l.reverse = a :: l.reverse
Module: Mathlib.Data.List.Basic

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

Tactic:
]

Goal state after:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ a :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = a :: b :: l
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z :: l).prod

Tactic:
]

Goal state after:
case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z :: l).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z * l.prod)

Tactic:
]

Goal state after:
case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z * l.prod)
Module: Mathlib.Data.List.Basic

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

Tactic:
]

Goal state after:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l
Module: Mathlib.Data.List.Basic

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

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * 0) = zpow' (zpow' a m) 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * 0) = zpow' (zpow' a m) 0
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)).prod * f n = (map f (range n)).prod * f n

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : m = 0
⊢ zpow' a (0 * n) = zpow' (zpow' a 0) n

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : m = 0
⊢ zpow' a (0 * n) = zpow' (zpow' a 0) n
Module: Mathlib.Data.List.Basic

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

Tactic:
]

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

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

pp: case hn
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ a ^ ↑n = a ^ n

case hn
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
]

Goal state after:
M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (0 :: map Nat.succ (range n))).prod = f 0 * (map (fun i ↦ f i.succ) (range n)).prod
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
⊢ n = n

Tactic:
]

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
⊢ d⁻¹ = d⁻¹

Tactic:
]

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
⊢ n / d = n / d

Tactic:
]

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:
rw [h, hn, hd]

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

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

Tactic:
]

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
⊢ D * f = D * f

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
h' : l.head! ∈ l
⊢ l.head! ∈ l
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
]

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 < x ^ r

Tactic:
]

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 < x ^ r
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 b (b :: l) = 0

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf b (b :: l) = 0
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → a' ∈ [] → f a' = 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)

Tactic:
]

Goal state after:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
]

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

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

Tactic:
]

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
⊢ l.eval = l.eval

Tactic:
]

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
⊢ idxOf a l < (take n l).length ↔ idxOf a l < n

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : ℕ
l : List α
ha : a ∈ l
⊢ idxOf a l < (take n l).length ↔ idxOf a l < n
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 = l.prod

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.length - 1 ≤ idxOf (l.getLast hl) l
⊢ ¬l.length - 1 ≤ idxOf (l.getLast hl) l
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
⊢ l.eval = l.eval

Tactic:
]

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 * (l.eval * zpow' (n, e).2 (n, e).1) = L.eval * (l.eval * zpow' (n, e).2 (n, e).1)

Tactic:
]

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 = L.eval * l₀.eval

Tactic:
]

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
⊢ a' ∈ take i l

Tactic:
]

Goal state after:
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
⊢ a' ∈ take i l
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.prod = l.prod

Tactic:
]

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 * zpow' (n, e).2 (n, e).1 * l.eval = L.eval * l.eval * zpow' (n, e).2 (n, e).1

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ L.eval * zpow' (n, e).2 (n, e).1 * l.eval = L.eval * l.eval * zpow' (n, e).2 (n, e).1
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 + -n, e) ::ᵣ l').eval = l'.eval

Tactic:
]

Goal state after:
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 + -n, e) ::ᵣ l').eval = l'.eval
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
⊢ l.eval⁻¹ = l⁻¹.eval

Tactic:
eval_inv

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
x : M
h : x = l.eval
⊢ l.eval⁻¹ = l.eval⁻¹
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
⊢ l.eval⁻¹ = l.eval⁻¹

Tactic:
]

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

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

Tactic:
]

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
⊢ (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod = (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod

Tactic:
]

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
h : idxOf x l = idxOf y l
⊢ l[idxOf x l] = y

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
h : idxOf x l = idxOf y l
⊢ l[idxOf x l] = y
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
]

Goal state after:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod
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
⊢ zpow' l.eval r = zpow' l.eval r

Tactic:
]

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
⊢ l.eval ^ r = zpow' l.eval ↑r

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ l.eval ^ r = zpow' l.eval ↑r
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
⊢ l.eval ^ r = l.eval ^ r

Tactic:
]

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 (fun a ↦ if p a then f a else f a) l).prod = (map f l).prod

Tactic:
]

Goal state after:
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α → M
l : List α
⊢ (map (fun a ↦ if p a then f a else f a) l).prod = (map f l).prod
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
⊢ t'.eval * zpow' (r, x).2 (r, x).1 = t'.eval * zpow' (r, x).2 (r, x).1

Tactic:
]

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

Goal state before:
pp: M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take i L').prod * L[i] = (take i L').prod * L'[i]
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Tactic:
]

Goal state after:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take i L').prod * L[i] = (take i L').prod * L'[i]
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : Group G
⊢ ∀ (L : List G), L.reverse.prod = (map (fun x ↦ x⁻¹) L).prod⁻¹

Tactic:
by
  simp [prod_inv_reverse]

Goal state after: