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

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

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 j : ℕ
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ j < l.length

Tactic:
by

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
⊢ L = L'

Tactic:
by

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

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

Goal state before:
pp: α : Type u
l : List α
i j : ℕ
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ (l.set i a)[j] = l[j]

Tactic:
by

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

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

Tactic:
by

Goal state after:
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

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

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map g ∘ map f = map (g ∘ f)

Tactic:
by

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

Goal state before:
pp: G : Type u_7
inst✝ : Group G
n : ℕ
f : ℕ → G
⊢ (map (fun k ↦ f k / f (k + 1)) (range n)).prod = f 0 / f n

Tactic:
by

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

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
⊢ map f (map g []) = []

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
⊢ ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
x : β
xs : List β
⊢ map f (map g (x :: xs)) = x :: xs

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse (map f) (map g)
x : β
⊢ f (g x) = x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : map f (x :: xs) = map f (y :: ys)
⊢ x :: xs = y :: ys

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
this : [x] = [y]
⊢ x = y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Injective (map f) ↔ Injective f

Tactic:
by

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
⊢ (map (fun k ↦ f (k + 1) / f k) (range n)).prod = f n / f 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Surjective (map f) ↔ Surjective f

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Bijective (map f) ↔ Bijective f

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) l
⊢ b₁ = b₂

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l = [] ∨ ∃ L b, l = L ++ [b]

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f g : α → β → α
a : α
l : List β
H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b
⊢ foldl f a l = foldl g a l

Tactic:
by

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ (L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f g : α → β → β
b : β
l : List α
H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
⊢ foldr f b l = foldr g b l

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : β → α → β
b : β
x : α
xs : List α
⊢ foldl f b (xs ++ [x]) = f (foldl f b xs) x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β → β
b : β
x : α
xs : List α
⊢ foldr f b (xs ++ [x]) = foldr f (f x b) xs

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β → α
a : α
hf : ∀ (b : β), f a b = a
b : β
l : List β
⊢ foldl f a (b :: l) = a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β → β
b : β
hf : ∀ (a : α), f a b = b
a : α
l : List α
⊢ foldr f b (a :: l) = b

Tactic:
by

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

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
a : α
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) 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 : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
a : α
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Tactic:
by

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

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

Goal state before:
pp: α : Type u
l : List (α → α)
f : α → α
hl : ∀ (f : α → α), f ∈ l → Injective f
hf : Injective f
⊢ Injective (foldl comp f l)

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Semiring α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : AddLeftMono α
inst✝ : PosMulMono α
⊢ MonoidWithZero { x // 0 ≤ x }

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : SemilatticeSup α
a : α
h : 0 ≤ a
⊢ toNonneg a = ⟨a, h⟩

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : SemilatticeSup α
a : α
b : { x // 0 ≤ x }
⊢ toNonneg a ≤ b ↔ a ≤ ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : { x // 0 ≤ x }
b : α
⊢ a < toNonneg b ↔ ↑a < b

Tactic:
by

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

Goal state before:
pp: L : List ℕ
⊢ L.headI + L.tail.sum = L.sum

Tactic:
by

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

Goal state before:
pp: α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
by

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

Goal state before:
pp: L : List ℕ
⊢ L.tail.sum = L.sum - L.headI

Tactic:
by

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

Goal state before:
pp: G : Type u_7
inst✝ : DivInvMonoid G
a b : G
l : List G
⊢ (a :: b :: l).alternatingProd = a / b * l.alternatingProd

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l : List α
⊢ foldrM f b l = foldr (fun a mb ↦ mb >>= f a) (pure b) l

Tactic:
by

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
⊢ [a].alternatingProd = a * [].alternatingProd⁻¹

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ { num := 0, den := d, den_nz := h, reduced := w } = 0

Tactic:
by

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

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a /. b = 0 ↔ a = 0

Tactic:
by

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a b : G
l : List G
⊢ (a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹

Tactic:
by

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (a :: l).alternatingProd = a / l.alternatingProd

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l : List α
⊢ foldlM f b l =
    foldl
      (fun mb a ↦ do
        let b ← mb
        f b a)
      (pure b) l

Tactic:
by

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

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ l.sum % n = (map (fun x ↦ x % n) l).sum % n

Tactic:
by

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

Goal state before:
pp: f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
⊢ f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
f : α → Bool
⊢ l.length = (filter f l).length + (filter (fun x ↦ !f x) l).length

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ -q = -q.num /. ↑q.den

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
l : List α
⊢ filterMap f l = flatMap (fun a ↦ (f a).toList) l

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
l : List α
⊢ filterMap f l = flatMap (fun a ↦ (f a).toList) l

Tactic:
by
  induction l with | nil => ?_ | cons a l ih => ?_ <;> simp [filterMap_cons]
  rcases f a <;> simp [ih]

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

Goal state before:
pp: q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁ * n₂).natAbs.Coprime (d₁ * d₂)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f g : α → Option β
l : List α
h : ∀ (x : α), x ∈ l → f x = g x
⊢ filterMap f l = filterMap g l

Tactic:
by

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

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ l.prod % n = (map (fun x ↦ x % n) l).prod % n

Tactic:
by

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

Goal state before:
pp: l : List ℤ
n : ℤ
⊢ l.sum % n = (map (fun x ↦ x % n) l).sum % n

Tactic:
by

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

Goal state before:
pp: n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ { num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ } * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ } =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
h : filterMap f (a :: l) = map g (a :: l)
⊢ (filterMap f l).length = l.length + 1

Tactic:
by

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

Goal state before:
pp: l : List ℤ
n : ℤ
⊢ l.prod % n = (map (fun x ↦ x % n) l).prod % n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: q : ℚ
n : ℕ
⊢ q ^ n = mkRat (q.num ^ n) (q.den ^ n)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
g : α → β
l : List α
h : ∀ (x : α), x ∈ l → f x = some (g x)
⊢ ∀ (x : α), x ∈ l → f x = (some ∘ g) x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
⊢ filterMap (fun x ↦ none) l = []

Tactic:
by

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

Goal state before:
pp: q : ℚ
n : ℕ
⊢ q ^ n = q.num ^ n /. ↑q.den ^ n

Tactic:
by

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

Goal state before:
pp: q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ den ^ n ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
⊢ filter p l = foldr (fun a out ↦ bif p a then a :: out else out) [] l

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p l <+ filter q l

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Bool
f : α → β
hf : Injective f
l : List α
inst✝ : DecidablePred fun b ↦ ∃ a, p a = true ∧ f a = b
⊢ map f (filter p l) = filter (fun b ↦ decide (∃ a, p a = true ∧ f a = b)) (map f l)

Tactic:
by

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

Goal state before:
pp: q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num ^ n).natAbs.Coprime (den ^ n)

Tactic:
by

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ (mkRat a b)⁻¹ = ↑b /. a

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
p : { a // a ∈ l } → Bool
inst✝ : DecidableEq α
⊢ filter p l.attach = map (Subtype.map id ⋯) (filter (fun x ↦ decide (∃ h, p ⟨x, h⟩ = true)) l).attach

Tactic:
by

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

Goal state before:
pp: n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ / (n₂ /. d₂) = n₁ * d₂ /. (d₁ * n₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
L : List (List α)
i : ℕ
⊢ take (take i (map length L)).sum L.flatten = (take i L).flatten

Tactic:
by

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

Goal state before:
pp: q r : ℚ
⊢ q / r = q.num * ↑r.den /. (↑q.den * r.num)

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ n /. 1 = ↑n

Tactic:
by

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

Goal state before:
pp: ⊢ 1 /. 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map (fun a ↦ ↑a) (map (Subtype.map id ⋯) (filter p l).attach)

Tactic:
by

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ 1 ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u
p q : α → Bool
l : List α
⊢ filter p (filter q l) = filter q (filter p l)

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ filter (fun x ↦ true) l = l

Tactic:
by

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

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

Goal state before:
pp: α : Type u
l : List α
⊢ filter (fun x ↦ false) l = []

Tactic:
by

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

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
⊢ (eraseP p l).length + 1 = l.length

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑x✝¹.succ • x✝ = ↑x✝¹ • x✝ + x✝

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.erase a).length + 1 = l.length

Tactic:
by

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

Goal state before:
pp: α : Type u_2
L : List (List α)
i : ℕ
⊢ drop (take i (map length L)).sum L.flatten = (drop i L).flatten

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ Int.negSucc x✝¹ • x✝ = -(↑x✝¹.succ • x✝)

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ AddGroup ℚ

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ AddCommMonoid ℚ

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ AddMonoid ℚ

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ AddLeftCancelSemigroup ℚ

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ AddRightCancelSemigroup ℚ

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ AddCommSemigroup ℚ

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ AddSemigroup ℚ

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ Monoid ℚ

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ CommSemigroup ℚ

Tactic:
by

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

Goal state before:
pp: q a b c : ℚ
⊢ Semigroup ℚ

Tactic:
by

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

Goal state before:
pp: q : ℚ
hq : q.num = 0
⊢ q = 0

Tactic:
by

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

Goal state before:
pp: q : ℚ
x✝ : q = 0
⊢ q.num = 0

Tactic:
by

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

Goal state before:
pp: q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : n = 0
⊢ q = 0

Tactic:
by

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

Goal state before:
pp: q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : d = 0
⊢ q = 0

Tactic:
by

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

Goal state before:
pp: a b c : ℤ
h : c = 0
⊢ (a + b) /. c = a /. c + b /. c

Tactic:
by

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

Goal state before:
pp: a b c : ℤ
h : ¬c = 0
⊢ (a + b) /. c = a /. c + b /. c

Tactic:
by

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

Goal state before:
pp: n d : ℤ
⊢ ↑n / ↑d = n /. d

Tactic:
by

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

Goal state before:
pp: L : List ℕ
h : ∀ (i : ℕ), i ∈ L → 1 ≤ i
⊢ L.length ≤ L.sum

Tactic:
by

Goal state after:
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 α
⊢ map f (l.erase a) = (map f l).erase (f a)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: q : ℚ
hq : q.den = 1
⊢ ↑q.num = q

Tactic:
by

Goal state after:
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
l₁ l₂ : List α
⊢ map f (foldl List.erase l₁ l₂) = foldl (fun l a ↦ l.erase (f a)) (map f l₁) l₂

Tactic:
by

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

Goal state before:
pp: q : ℚ
h : q.isInt = true
⊢ q = ↑q.num

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
l : List ι
i : ℕ
h : i < l.length
⊢ (l.eraseIdx i).length + 1 = l.length

Tactic:
by

Goal state after:
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
l₁ l₂ : List α
⊢ map f (l₁.diff l₂) = (map f l₁).diff (map f l₂)

Tactic:
by

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

Goal state after: