mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.Result

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
num : ℕ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑num * ⅟↑1 = ↑num

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Result

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a✝ denom✝ : ℕ
inv : Invertible ↑denom✝
⊢ ↑(Int.ofNat a✝) * ⅟↑denom✝ = ↑a✝ * ⅟↑denom✝

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Result

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ : ℕ
⊢ 1 * ↑1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Result

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ : ℕ
⊢ ↑1 * 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Result

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ : ℕ
⊢ ↑n✝ = ↑n✝ * ⅟↑1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Result

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ denom✝ : ℕ
inv : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑(Int.ofNat num✝) * ⅟↑denom✝

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Result

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ : ℤ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑num✝ * ⅟↑1 = ↑num✝

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Result

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ 1 * ↑1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Result

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑1 * 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Result

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑n✝ = ↑n✝ * ⅟↑1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: a✝ : ℕ
⊢ (↑(Int.negOfNat a✝)).natAbs = ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ ↑↑m = ↑m

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
l : List ι
⊢ (map (fun x ↦ 1) l).prod = 1

Tactic:
induction l with simp [*]

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

Goal state before:
pp: case nil
M : Type u_2
inst✝ : MulOneClass M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
hl : [] ≠ []
base : ∀ (x : M), x ∈ [] → p x
⊢ p [].prod

Tactic:
simp at hl

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

Goal state before:
pp: case e'_3
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ = 1 / a ^ n

Tactic:
simp

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

Goal state before:
pp: case e'_4
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ m)⁻¹ = 1 / a ^ m

Tactic:
simp

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

Goal state before:
pp: case e'_3
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ n)⁻¹ = 1 / a ^ n

Tactic:
simp

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

Goal state before:
pp: case e'_4
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ m)⁻¹ = 1 / a ^ m

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: n✝ : ℕ
⊢ (↑n✝).succ = ↑n✝.succ

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: n✝¹ n✝ : ℕ
⊢ ↑n✝¹ - ↑n✝ = ↑(n✝¹.sub n✝)

Tactic:
simp

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ [l[n]] = [l.get ⟨n, h⟩]

Tactic:
simp

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

Goal state before:
pp: α : Type u
l : List α
i : ℕ
h : i < l.length
⊢ take i l ++ [l[i]] = take (i + 1) l

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
Rₐ : α → α → Prop
⊢ Forall₂ Rₐ [] [] ↔ ∀ (x : α), x ∈ [] → Rₐ x x

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

pp: case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a / 0 < 1 ↔ 0 < 0 ∧ a < 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 < a

pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

Tactic:
· simp [hb, hb.not_gt, hb.ne, div_lt_one_of_neg]

Goal state after:
case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a / 0 < 1 ↔ 0 < 0 ∧ a < 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 < a

case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
l₂ : List β
h₁ : (a :: l₁).length = l₂.length
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ (a :: l₁).zip l₂ → R a_1 b
⊢ Forall₂ R (a :: l₁) l₂

Tactic:
| cons a l₁ IH =>

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

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Tactic:
simp [hb, hb.not_gt, div_le_one, hb.ne.symm]

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

Goal state before:
pp: case zero.nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
hl : ∀ (x : α), x ∈ [] → p x
⊢ (pmap f [] hl).insertIdx 0 (f a ha) = pmap f ([].insertIdx 0 a) ⋯

Tactic:
simp

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

Goal state before:
pp: case zero.cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
head✝ : α
tail✝ : List α
hl : ∀ (x : α), x ∈ head✝ :: tail✝ → p x
⊢ (pmap f (head✝ :: tail✝) hl).insertIdx 0 (f a ha) = pmap f ((head✝ :: tail✝).insertIdx 0 a) ⋯

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case mpr.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
hl1 : Forall₂ R l₁ l₁✝
⊢ SublistForall₂ R l₁ (a✝¹ :: l₂✝)

Tactic:
exact SublistForall₂.cons_right (ih hl1)

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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 L).prod * [L[i]].prod = (take i L).prod * L[i]

Tactic:
simp

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:
simp

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

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
h : (head✝ :: tail✝).prod ≠ 1
⊢ 0 < (head✝ :: tail✝).length

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case nil
M : Type u_4
inst✝ : Monoid M
⊢ [][0]?.getD 1 * [].tail.prod = [].prod

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
⊢ (head✝ :: tail✝)[0]?.getD 1 * (head✝ :: tail✝).tail.prod = (head✝ :: tail✝).prod

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case nil
M : Type u_4
inst✝ : Monoid M
y : M
h : ∀ (x : M), x ∈ [] → Commute y x
⊢ Commute y [].prod

Tactic:
simp

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

Tactic:
simp

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:
induction l with
  | nil => rfl
  | cons i l hil =>
    rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]

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:
simp

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:
simp

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:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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:
simp only [eval_cons, h, div_eq_mul_inv, mul_inv, ← zpow'_neg, ← add_neg_cancel (1:ℤ), zpow'_add]
  ac_rfl

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:
simp

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

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

Tactic:
simp

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:
simp

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
  rw [eval_pow, hx]
  rw [zpow'_ofNat _ hr]

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

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

Tactic:
simp

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

Goal state before:
pp: G : Type u_7
inst✝ : Group G
head✝ : G
tail✝ : List G
x✝ : 0 < (head✝ :: tail✝).length
⊢ (drop (0 + 1) (head✝ :: tail✝)).prod = (head✝ :: tail✝)[0]⁻¹ * (drop 0 (head✝ :: tail✝)).prod

Tactic:
simp

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

Goal state before:
pp: K : Type u_8
inst✝ : DivisionCommMonoid K
⊢ [].prod⁻¹ = (map (fun x ↦ x⁻¹) []).prod

Tactic:
simp

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

Goal state before:
pp: case nil
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a : A
⊢ (map (fun x ↦ if x = a then f x else g x) []).prod = (f a / g a) ^ count a [] * (map g []).prod

Tactic:
simp

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

Goal state before:
pp: α : Type u
l : List α
⊢ (foldl (fun t h ↦ h :: t) [] l).reverse = l

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
⊢ ↑↑0 = ↑0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
x✝ : ℕ
⊢ ↑↑(x✝ + 1) = ↑(↑x✝ + 1)

Tactic:
simp

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

Goal state before:
pp: case nil
⊢ [].headI + [].tail.sum = [].sum

Tactic:
simp

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

Goal state before:
pp: case cons
head✝ : ℕ
tail✝ : List ℕ
⊢ (head✝ :: tail✝).headI + (head✝ :: tail✝).tail.sum = (head✝ :: tail✝).sum

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
⊢ ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b []) =
      foldl
        (fun mb a ↦ do
          let b ← mb
          f b a)
        mb []

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u
β : Type v
f : α → Option β
g : α → β
⊢ filterMap f [] = map g [] → ∀ (x : α), x ∈ [] → f x = some (g x)

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_2
i : ℕ
⊢ take (take i (map length [])).sum [].flatten = (take i []).flatten

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_2
i : ℕ
⊢ drop (take i (map length [])).sum [].flatten = (drop i []).flatten

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q✝ a b c : ℚ
n : ℕ
q : ℚ
⊢ (↑↑n + ↑1) * q = n • q + q

Tactic:
Rat.add_mul,

Goal state after:
q✝ a b c : ℚ
n : ℕ
q : ℚ
⊢ ↑↑n * q + ↑1 * q = n • q + q
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
⊢ (fun x ↦ a == x) = fun x ↦ f a == f x

Tactic:
ext b

Goal state after:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
b : α
⊢ (a == b) = (f a == f b)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
h : ∀ (i : ℕ), i ∈ [] → 1 ≤ i
⊢ [].length ≤ [].sum

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. 0) = n /. 0

Tactic:
simp

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

Goal state before:
pp: case nil
ι : Type u_1
inst✝¹ : BEq ι
inst✝ : LawfulBEq ι
i : ℕ
hi : i < [].length
⊢ [].erase [][i] ~ [].eraseIdx i

Tactic:
simp

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

Goal state before:
pp: α : Type u
p : α → Prop
ys✝ : List α
⊢ Forall p ([] ++ ys✝) ↔ Forall p [] ∧ Forall p ys✝

Tactic:
simp

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

Goal state before:
pp: α : Type u
l : List α
i : Fin l.attach.length
⊢ ↑(l.attach.get i) = l.get ⟨↑i, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: case zero
a : ℕ
⊢ range' a 0 0 = replicate 0 a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case inl
a : ℤ
ha : a ≤ 0
⊢ mkRat a 0 ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b < ↑c / ↑d ↔ a * d < c * b

Tactic:
by
  simp only [lt_iff_le_not_ge]
  apply and_congr
  · simp [div_def', Rat.divInt_le_divInt b_pos d_pos]
  · simp [div_def', Rat.divInt_le_divInt d_pos b_pos]

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: ⊢ ↑0⁻¹ = ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (n * a) (d * a) = divNat n d

Tactic:
ext; push_cast; exact Rat.divInt_mul_right (mod_cast ha)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 = 0 * 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a : α
u : αˣ
⊢ a = ↑u * (↑u⁻¹ * a)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
⊢ a * 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b

Tactic:
apply Units.mul_left_dvd

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a : α
inst✝ : Subsingleton αˣ
d : α
⊢ a = a * 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Subsingleton αˣ
c d : α
⊢ 0 = 0 * c

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝ : GroupWithZero α
m : α
h : m = 0 → 0 = 0
⊢ 0 = m * (m⁻¹ * 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ ⟨n, hn⟩ ≤ ⟨k, hk⟩ ↔ n ≤ k

Tactic:
simp

Goal state after:
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ ⟨n, hn⟩ < ⟨k, hk⟩ ↔ n < k

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑d ∣ a * ↑d

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.den ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₂.den ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑(n₁ * ↑d₂) = ↑(n₂ * ↑d₁)
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
Int.cast_inj,

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : n₁ * ↑d₂ = n₂ * ↑d₁
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den

Tactic:
apply dvd_mul_of_dvd_right

Goal state after:
case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ ↑q₂.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₂.num * ↑q₁.den

Tactic:
apply dvd_mul_of_dvd_right

Goal state after:
case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ ↑q₁.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ (q * q).num = q.num * q.num

Tactic:
by
  rw [mul_num, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]
  exact (q.reduced.mul_right q.reduced).mul_left (q.reduced.mul_right q.reduced)

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
n✝ : ℤ
⊢ ↑↑n✝ = ↑n✝

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ (↑n.succ * ⅟↑d)⁻¹ = ↑d * ⅟↑n.succ

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ = ↑(Int.ofNat d) * ⅟↑n.succ

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
⊢ (↑1)⁻¹ = ↑1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
⊢ (↑0)⁻¹ = ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
⊢ (↑(Int.negOfNat 1))⁻¹ = ↑(Int.negOfNat 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case pos
⊢ ↑(0 / 0) = ↑0 / ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℤ
⊢ (↑a)⁻¹.num = a.sign

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℕ
⊢ (↑a)⁻¹.num = (↑a).sign

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℤ
⊢ (↑a)⁻¹.den = if a = 0 then 1 else a.natAbs

Tactic:
simp

Goal state after: