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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
l : List α
i✝ : ℕ
a✝ : γ
⊢ (map g (map f l))[i✝]? = some a✝ ↔ (map g (map f l))[i✝]? = some a✝

Tactic:
]

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 : f x = f y
hxys : map f xs = map f ys
⊢ y :: ys = y :: ys

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
refine ⟨fun h x => ?_, (·.list_map)⟩

Goal state after:
α : Type u
β : Type v
f : α → β
h : Surjective (map f)
x : β
⊢ ∃ a, f a = x
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate l.length b₂
⊢ b₁ = b₂

Tactic:
]

Goal state after:
α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate l.length b₂
⊢ b₁ = b₂
Module: Mathlib.Data.List.Basic

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

Tactic:
]

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

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

Tactic:
]

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 β
⊢ a = a

Tactic:
]

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

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

Tactic:
]

Goal state after:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x ↦ if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
Module: Mathlib.Data.List.Basic

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

Tactic:
]

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

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

Tactic:
]

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

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:
induction l <;> simp [*]

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
⊢ a = a

Tactic:
]

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

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

Tactic:
]

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₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } (c /. d) = f₁ a b c d /. f₂ a b c d

Tactic:
]

Goal state after:
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₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } (c /. d) = f₁ a b c d /. f₂ a b c d
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₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ }
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } (c /. d) = f₁ a b c d /. f₂ a b c d

Tactic:
rw [mk_eq_divInt] at ha

Goal state after:
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₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } (c /. d) = f₁ a b c d /. f₂ a b c d
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₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
    f₁ a b c d /. f₂ a b c d

Tactic:
]

Goal state after:
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₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
    f₁ a b c d /. f₂ a b c d
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:
]

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

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₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d

Tactic:
]

Goal state after:
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₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
⊢ -q = -q

Tactic:
]

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₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)

Tactic:
]

Goal state after:
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₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)
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₁
⊢ normalize
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.num *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.num)
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.den *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.den)
      ⋯ =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Tactic:
]

Goal state after:
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₁
⊢ normalize
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.num *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.num)
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.den *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.den)
      ⋯ =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }
Module: Mathlib.Data.Rat.Defs

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
induction l <;> simp [*]

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

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

Tactic:
]

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.natAbs ^ n).Coprime (den ^ n)

Tactic:
]

Goal state after:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num.natAbs ^ n).Coprime (den ^ n)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ↑b /. a = ↑b /. a

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: q r : ℚ
⊢ q / r = q / r

Tactic:
]

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

Goal state before:
pp: ⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: ⊢ 1 ≠ 0

pp: ⊢ 1 ≠ 0

Tactic:
]

Goal state after:
⊢ 1 ≠ 0

⊢ 1 ≠ 0
Module: Mathlib.Data.Rat.Defs

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ -(↑(↑x✝¹ + 1) * x✝) = -(↑↑x✝¹.succ * x✝)

Tactic:
]

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ -(↑(↑x✝¹ + 1) * x✝) = -(↑↑x✝¹.succ * x✝)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
]

Goal state after:
case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + L.length ≤ j + L.sum
Module: Mathlib.Data.Rat.Defs

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

Tactic:
]

Goal state after:
a b c : ℤ
h : ¬c = 0
⊢ (a + b) * (c * c) = (a * c + b * c) * c
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 α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ f a == f x) l) = map f (eraseP ((fun x ↦ f a == x) ∘ f) l)

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ f a == f x) l) = map f (eraseP ((fun x ↦ f a == x) ∘ f) l)
Module: Mathlib.Data.Rat.Defs

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

Tactic:
]

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

Goal state after:
case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. 0) = n /. 0
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. d = n /. d

Tactic:
]

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

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

Tactic:
]

Goal state after:
q : ℚ
hq : q.den = 1
⊢ q.num /. 1 = q.num /. ↑1
Module: Mathlib.Data.Rat.Defs

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

Tactic:
]

Goal state after:
q : ℚ
h : q.den = 1
⊢ q = ↑q.num
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a✝ b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C (↑n / ↑↑d)

Tactic:
]

Goal state after:
q a✝ b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C (↑n / ↑↑d)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a✝ b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C (↑n / ↑↑d)

Tactic:
exact div n d nz red

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ Forall p l → q x ∧ Forall q l

Tactic:
]

Goal state after:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ Forall p l → q x ∧ Forall q l
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f l) ↔ Forall (p ∘ f) l

Tactic:
induction l <;> simp [*]

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

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℚ
⊢ x✝ ^ x✝¹ * x✝ = x✝ ^ x✝¹ * x✝

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: r : ℚ
⊢ r = r

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ a' ∈ t

Tactic:
]

Goal state after:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ a' ∈ t
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ (pmap (fun a x ↦ f a) s ⋯).Disjoint (pmap (fun a x ↦ f a) t ⋯)

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ (pmap (fun a x ↦ f a) s ⋯).Disjoint (pmap (fun a x ↦ f a) t ⋯)
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: q : ℚ
this : ↑q.den ≠ 0
⊢ q.num /. 1 = q.num /. 1

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ if s = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Tactic:
]

Goal state after:
m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ if s = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case false
m e : ℕ
⊢ 0 ≤ ↑(m * 10 ^ e)

Tactic:
]

Goal state after:
case false
m e : ℕ
⊢ 0 ≤ ↑(m * 10 ^ e)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ 0 ≤ c /. d - a /. b ↔ 0 ≤ c * b - a * d

Tactic:
]

Goal state after:
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ 0 ≤ c /. d - a /. b ↔ 0 ≤ c * b - a * d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: q : ℚ
⊢ { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.num = |q.num|

Tactic:
]

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

Goal state before:
pp: q : ℚ
⊢ { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.den = q.den

Tactic:
]

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

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

Tactic:
]

Goal state after:
q : ℚ≥0
⊢ ↑q = ↑(↑q).num / ↑(↑q).den
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ ↑a.den /. a.num

Tactic:
]

Goal state after:
a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ ↑a.den /. a.num
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ q.den = q.den

pp: q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num

Tactic:
]

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ q⁻¹.num = q.den

Tactic:
rw [inv_def, divNat, num, coe_mk, Rat.divInt_ofNat, ← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq),
    Int.natAbs_natCast]

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ { num := ↑q.den, den := q.num, den_nz := ⋯, reduced := ?m.26 }.den = q.num

pp: q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num

Tactic:
]

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
⊢ ↑↑(↑q).num.natAbs / ↑q.den = ↑q

Tactic:
]

Goal state after:
q : ℚ≥0
⊢ ↑↑(↑q).num.natAbs / ↑q.den = ↑q
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑(if b = true then NNRat.divNat m (10 ^ d) else ↑(m * 10 ^ d))

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑(if b = true then NNRat.divNat m (10 ^ d) else ↑(m * 10 ^ d))
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ mkRat (↑(OfNat.ofNat m)) (10 ^ OfNat.ofNat d) = Rat.divInt ↑m ↑(10 ^ d)

Tactic:
]

Goal state after:
case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ mkRat (↑(OfNat.ofNat m)) (10 ^ OfNat.ofNat d) = Rat.divInt ↑m ↑(10 ^ d)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ≥0
h : q ≤ p
⊢ ↑q ≤ ↑p

Tactic:
]

Goal state after:
p q : ℚ≥0
h : q ≤ p
⊢ ↑q ≤ ↑p
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑(OfNat.ofNat m * 10 ^ OfNat.ofNat d) = ↑(m * 10 ^ d)

Tactic:
]

Goal state after:
case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑(OfNat.ofNat m * 10 ^ OfNat.ofNat d) = ↑(m * 10 ^ d)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p : ℚ
q : ℚ≥0
hp : 0 ≤ p
⊢ ↑q ≤ p ↔ ↑q ≤ p

Tactic:
]

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

Goal state before:
pp: q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ q < ↑p ↔ q < ↑p

Tactic:
]

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

Goal state before:
pp: case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ 0 = 0

Tactic:
]

Goal state after: