mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Nonneg.Basic

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
⊢ ↑↑0 = ↑0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (foldl comp f (lh :: lt))

Tactic:
| cons lh lt l_ih =>

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

Goal state after:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
x✝ : ℕ
⊢ ↑↑(x✝ + 1) = ↑(↑x✝ + 1)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: case e_den
d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ d = 1

Tactic:
;

Goal state after:
case e_den
d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ d = 1
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₂
x : ℚ
ha : a /. b = x
⊢ f x (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₂
x : ℚ
ha : a /. b = x
⊢ f x (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:
;

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 = { 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
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₁
x : ℚ
hc : c /. d = x
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } x = 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₁
x : ℚ
hc : c /. d = x
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } x = 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 = { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ }
⊢ 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 = { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ }
⊢ 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.Data.List.Basic

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

Tactic:
;

Goal state after:
case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
head✝ : α
tail✝ : List α
l_ih :
  ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b tail✝) =
      foldl
        (fun mb a ↦ do
          let b ← mb
          f b a)
        mb tail✝
mb✝ : m β
⊢ (do
      let b ← mb✝
      foldlM f b (head✝ :: tail✝)) =
    foldl
      (fun mb a ↦ do
        let b ← mb
        f b a)
      mb✝ (head✝ :: tail✝)
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.List.Basic

Goal state before:
pp: case cons
α : Type u
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : filter p tail✝ = foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
⊢ (match p head✝ with
    | true => head✝ :: foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
    | false => foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝) =
    bif p head✝ then head✝ :: foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
    else foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝

Tactic:
;

Goal state after:
case cons
α : Type u
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : filter p tail✝ = foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
⊢ (match p head✝ with
    | true => head✝ :: foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
    | false => foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝) =
    bif p head✝ then head✝ :: foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
    else foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
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: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑↑x✝¹.succ * x✝ = ↑↑x✝¹ * x✝ + x✝

Tactic:
;

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑↑x✝¹.succ * x✝ = ↑↑x✝¹ * x✝ + x✝
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.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 α
b : α
⊢ (a == b) = (f a == f b)

Tactic:
;

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.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: case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d

Tactic:
rw [hd]

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: 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.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: q : ℚ≥0
⊢ ↑q⁻¹ = ↑(divNat q.den q.num)

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: a : ℚ≥0
⊢ ↑(a ^ 0) = ↑1

Tactic:
;

Goal state after:
a : ℚ≥0
⊢ ↑(a ^ 0) = ↑1
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: n : ℕ
a : ℚ≥0
⊢ ↑(a ^ ↑n.succ) = ↑(a ^ ↑n * a)

Tactic:
;

Goal state after:
n : ℕ
a : ℚ≥0
⊢ ↑(a ^ ↑n.succ) = ↑(a ^ ↑n * a)
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: n : ℕ
a : ℚ≥0
⊢ ↑(a ^ Int.negSucc n) = ↑(a ^ ↑n.succ)⁻¹

Tactic:
;

Goal state after:
n : ℕ
a : ℚ≥0
⊢ ↑(a ^ Int.negSucc n) = ↑(a ^ ↑n.succ)⁻¹
Module: Mathlib.Algebra.Field.Rat

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

Tactic:
;

Goal state after:
⊢ ↑0⁻¹ = ↑0
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
h : q ≠ 0
⊢ ↑(q * q⁻¹) = ↑1

Tactic:
;

Goal state after:
q : ℚ≥0
h : q ≠ 0
⊢ ↑(q * q⁻¹) = ↑1
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n : ℕ
⊢ ↑n = ↑↑n

Tactic:
;

Goal state after:
n : ℕ
⊢ ↑n = ↑↑n
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p * q).toNNRat = ↑(p.toNNRat * q.toNNRat)

Tactic:
;

Goal state after:
case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p * q).toNNRat = ↑(p.toNNRat * q.toNNRat)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p : ℚ≥0
⊢ p.num = p.num ∧ p.den = p.den

Tactic:
;

Goal state after:
p : ℚ≥0
⊢ p.num = p.num ∧ p.den = p.den
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ ↑(divNat n₁ d₁) = ↑(divNat n₂ d₂) ↔ n₁ * d₂ = n₂ * d₁

Tactic:
;

Goal state after:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ ↑(divNat n₁ d₁) = ↑(divNat n₂ d₂) ↔ n₁ * d₂ = n₂ * d₁
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ ↑n₁ * ↑d₂ = ↑n₂ * ↑d₁ ↔ n₁ * d₂ = n₂ * d₁

Tactic:
;

Goal state after:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ ↑n₁ * ↑d₂ = ↑n₂ * ↑d₁ ↔ n₁ * d₂ = n₂ * d₁
Module: Mathlib.Data.NNRat.Defs

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

Tactic:
;

Goal state after:
q : ℚ≥0
⊢ ↑(divNat q.num q.den) = mkRat (↑q).num (↑q).den
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
⊢ ↑(divNat n₁ d₁ * divNat n₂ d₂) = ↑(divNat (n₁ * n₂) (d₁ * d₂))

Tactic:
;

Goal state after:
n₁ n₂ d₁ d₂ : ℕ
⊢ ↑(divNat n₁ d₁ * divNat n₂ d₂) = ↑(divNat (n₁ * n₂) (d₁ * d₂))
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
⊢ Rat.divInt ↑n₁ ↑d₁ * Rat.divInt ↑n₂ ↑d₂ = Rat.divInt (↑n₁ * ↑n₂) (↑d₁ * ↑d₂)

Tactic:
;

Goal state after:
n₁ n₂ d₁ d₂ : ℕ
⊢ Rat.divInt ↑n₁ ↑d₁ * Rat.divInt ↑n₂ ↑d₂ = Rat.divInt (↑n₁ * ↑n₂) (↑d₁ * ↑d₂)
Module: Mathlib.Data.NNRat.Defs

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

Tactic:
;

Goal state after:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ ↑(divNat (a * n) (a * d)) = ↑(divNat n d)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑a * ↑n) (↑a * ↑d) = Rat.divInt ↑n ↑d

Tactic:
;

Goal state after:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑a * ↑n) (↑a * ↑d) = Rat.divInt ↑n ↑d
Module: Mathlib.Data.NNRat.Defs

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

Tactic:
;

Goal state after:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ ↑(divNat (n * a) (d * a)) = ↑(divNat n d)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑n * ↑a) (↑d * ↑a) = Rat.divInt ↑n ↑d

Tactic:
;

Goal state after:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑n * ↑a) (↑d * ↑a) = Rat.divInt ↑n ↑d
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q✝ : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C (divNat q.num q.den)

Tactic:
;

Goal state after:
p q✝ : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C (divNat q.num q.den)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q r : ℚ≥0
⊢ ↑(q + r) = ↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den))

Tactic:
;

Goal state after:
q r : ℚ≥0
⊢ ↑(q + r) = ↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den))
Module: Mathlib.Data.NNRat.Defs

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

Tactic:
;

Goal state after:
q r : ℚ≥0
⊢ ↑(q * r) = ↑(divNat (q.num * r.num) (q.den * r.den))
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ≥0
⊢ (↑p).num * ↑(↑q).den < (↑q).num * ↑(↑p).den ↔ p.num * q.den < q.num * p.den

Tactic:
;

Goal state after:
p q : ℚ≥0
⊢ (↑p).num * ↑(↑q).den < (↑q).num * ↑(↑p).den ↔ p.num * q.den < q.num * p.den
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ≥0
⊢ (↑p).num * ↑(↑q).den ≤ (↑q).num * ↑(↑p).den ↔ p.num * q.den ≤ q.num * p.den

Tactic:
;

Goal state after:
p q : ℚ≥0
⊢ (↑p).num * ↑(↑q).den ≤ (↑q).num * ↑(↑p).den ↔ p.num * q.den ≤ q.num * p.den
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
h : IsRelPrime 0 0
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
h : IsRelPrime 0 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
hx : 0 ∣ x
hy : 0 ∣ y
h : ¬IsUnit 0
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
hx : 0 ∣ x
hy : 0 ∣ y
h : ¬IsUnit 0
⊢ False
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x z d : α
h : IsRelPrime (x * d) z
⊢ IsRelPrime x z

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x z d : α
h : IsRelPrime (x * d) z
⊢ IsRelPrime x z
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
hm : IsPrimal 0
⊢ IsPrimal (0 * n)

pp: case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
⊢ IsPrimal (m * n)

Tactic:
;

Goal state after:
case inl
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
hm : IsPrimal 0
⊢ IsPrimal (0 * n)

case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
⊢ IsPrimal (m * n)
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ y * x ∣ z

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ y * x ∣ z
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime y x
H2 : IsRelPrime z x
⊢ IsRelPrime (y * z) x

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime y x
H2 : IsRelPrime z x
⊢ IsRelPrime (y * z) x
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n

Tactic:
refine ⟨m⁻¹ * n, ?_⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ n = m * (m⁻¹ * n)
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
;

Goal state after:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
this : a.natAbs * d = n.natAbs * b.natAbs
⊢ n.natAbs ∣ a.natAbs * d
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b

pp: case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b

Tactic:
;

Goal state after:
case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b

case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b
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:
;

Goal state after:
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
Module: Mathlib.Tactic.FieldSimp

Goal state before:
pp: «$v» : Level
«$M» : Type v
«$iM» : CommGroupWithZero «$M»
«$r» : ℤ
«$x» : «$M»
$snd✝ : ℕ
«$e» : «$M»
«$pf» : zpow' «$x» «$r» = «$e»
⊢ NF.eval [] * zpow' («$r», «$x»).2 («$r», «$x»).1 = «$e»

Tactic:
;

Goal state after:
«$v» : Level
«$M» : Type v
«$iM» : CommGroupWithZero «$M»
«$r» : ℤ
«$x» : «$M»
$snd✝ : ℕ
«$e» : «$M»
«$pf» : zpow' «$x» «$r» = «$e»
⊢ NF.eval [] * zpow' («$r», «$x»).2 («$r», «$x»).1 = «$e»
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb : ↑0 ≠ 0
e : divNat a 0 = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ False

Tactic:
;

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
a d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb : ↑0 ≠ 0
e : divNat a 0 = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ False
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝

Tactic:
;

Goal state after:
n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝