mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
⊢ IsUnit a

Tactic:
rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
⊢ a ^ m ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m ↔ n ≤ m

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: m : ℕ
⊢ ↑(m + 1).toPNat' = if 0 < m + 1 then m + 1 else 1

Tactic:
by

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

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

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

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k

Tactic:
by

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

Goal state before:
pp: m k : ℕ+
⊢ m.div k = if ↑m % ↑k = 0 then (↑m / ↑k).pred else ↑m / ↑k

Tactic:
by

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

Goal state before:
pp: n : ℤ
hn : 0 < n
⊢ ↑↑n.natAbs.toPNat' = n

Tactic:
by

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

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ (a /. b).num ∣ a

Tactic:
by

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

Goal state before:
pp: a b : ℤ
⊢ ↑(a /. b).den ∣ b

Tactic:
by

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₂
h : ↑(n₁ /. ↑d₁) = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ ↑↑d₁ ≠ 0

Tactic:
by

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₂
h : ↑n₁ / ↑↑d₁ = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ ↑↑d₂ ≠ 0

Tactic:
by

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

Goal state before:
pp: case refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num /. ↑q.den = n /. d

Tactic:
rwa [num_divInt_den]

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

Goal state before:
pp: q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num * d = n * ↑q.den

Tactic:
by

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

Goal state before:
pp: q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ q.num ∣ n

Tactic:
by

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

Goal state before:
pp: q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ + q₂).den ∣ q₁.den.lcm q₂.den

Tactic:
by

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ - q₂).den ∣ q₁.den.lcm q₂.den

Tactic:
by

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).den ∣ q₁.den * q₂.den

Tactic:
by

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₂
h : ↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = ↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
⊢ { num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }

Tactic:
by

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).num = q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a b : ℤ
⊢ ↑(a /. b) = ↑a / ↑b

Tactic:
by

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
by

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

Goal state before:
pp: q : ℚ
n : ℤ
⊢ (q + ↑n).den = q.den

Tactic:
by

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

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (↑n + q).den = q.den

Tactic:
by

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

Goal state before:
pp: q : ℚ
n : ℤ
⊢ (q - ↑n).den = q.den

Tactic:
by

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

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (↑n - q).den = q.den

Tactic:
by

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
by

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.num * q₂.num = (q₁ * q₂).num * ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ IsSquare ↑n ↔ IsSquare n

Tactic:
by

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

Goal state before:
pp: z : ℤ
⊢ IsSquare ↑z ↔ IsSquare z

Tactic:
by

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

Goal state before:
pp: n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
⊢ mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
⊢ Injective NNRat.cast

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
q : ℚ≥0
⊢ ↑q = 0 ↔ q = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑a / ↑b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
a : α
⊢ Commute (↑q) a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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»
⊢ ((«$r», «$x») ::ᵣ []).eval = «$e»

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
⊢ ↑(divNat a b) = ↑a / ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q + r) = ↑q + ↑r

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q * r) = ↑q * ↑r

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
hq : ↑q.num ≠ 0
⊢ ↑q⁻¹ = (↑q)⁻¹

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n✝¹ num✝ n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsNNRat (NNRat.divNat ↑n✝¹ ↑n✝) num✝ denom✝

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑qi * ↑denom✝ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q / r) = ↑q / ↑r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑denom✝ * ↑qi = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝

Tactic:
simp only

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
r : ℚ
a : α
⊢ Commute (↑r) a

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ b ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionSemiring R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ≥0
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑qi * ↑denom✝ = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionSemiring R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ≥0
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑denom✝ * ↑qi = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionSemiring R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ≥0
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝

Tactic:
simp only

Goal state after:
R : Type u_1
inst✝¹ : DivisionSemiring R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ≥0
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionSemiring R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ≥0
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑qi * ↑denom✝ = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑denom✝ * ↑qi = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝

Tactic:
simp only

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsNNRat a n.succ d → IsNNRat a⁻¹ d n.succ

Tactic:
by

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

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ ↑b = ↑d * ↑k

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.ofNat n.succ) d → IsRat a⁻¹ (Int.ofNat d) n.succ

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.negOfNat n.succ) d → IsRat a⁻¹ (Int.negOfNat d) n.succ

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ ↑d ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑(mkRat a b) = ↑a / ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q + r) = ↑q + ↑r

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q : ℚ
⊢ ↑(-q) = -↑q

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p - q) = ↑p - ↑q

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ (-q)⁻¹ = -q⁻¹

Tactic:
by

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

Goal state before:
pp: a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
⊢ (↑a / ↑b).num = a

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p * q) = ↑p * ↑q

Tactic:
by

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

Goal state before:
pp: a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
⊢ ↑(↑a / ↑b).den = b

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q : ℚ
hq : ↑q.num ≠ 0
⊢ ↑q⁻¹ = (↑q)⁻¹

Tactic:
by

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

Goal state before:
pp: a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c ∧ b = d

Tactic:
by

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

Goal state before:
pp: n : ℤ
hn : ¬n = 0
⊢ ↑n ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p / q) = ↑p / ↑q

Tactic:
by

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

Goal state before:
pp: a b : ℤ
h : b ∣ a
⊢ ↑(a / b) = ↑a / ↑b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionSemiring α
inst✝¹ : DivisionSemiring β
inst✝ : RingHomClass F α β
f : F
q : ℚ≥0
⊢ f ↑q = ↑q

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
h1 : a.pow b = c
⊢ a.pow (2 * b) = c.mul c

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : FunLike F ℚ≥0 α
inst✝ : RingHomClass F ℚ≥0 α
f : F
q : ℚ≥0
⊢ f q = ↑q

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
h1 : a.pow b = c
⊢ a.pow (2 * b + 1) = c.mul (c.mul a)

Tactic:
by

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

Goal state before:
pp: m n : ℤ
hn : n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m

Tactic:
by

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

Goal state before:
pp: a : ℤ
ha0 : 0 < a
⊢ (↑a)⁻¹.num = 1

Tactic:
by

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

Goal state before:
pp: a : ℤ
ha0 : 0 < a
⊢ ↑(↑a)⁻¹.den = a

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionRing α
inst✝¹ : DivisionRing β
inst✝ : RingHomClass F α β
f : F
q : ℚ
⊢ f ↑q = ↑q

Tactic:
by

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

Goal state before:
pp: a : ℕ
ha0 : 0 < a
⊢ (↑a)⁻¹.den = a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_3
inst✝² : DivisionRing α
inst✝¹ : FunLike F ℚ α
inst✝ : RingHomClass F ℚ α
f : F
q : ℚ
⊢ f q = ↑q

Tactic:
by

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

Goal state before:
pp: a : ℕ
inst✝ : a.AtLeastTwo
⊢ (OfNat.ofNat a)⁻¹.num = 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : ℕ
inst✝ : a.AtLeastTwo
⊢ (OfNat.ofNat a)⁻¹.den = OfNat.ofNat a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℚ → Prop
h : ∀ (a b : ℤ), b ≠ 0 → p (↑a / ↑b)
q : ℚ
⊢ p q

Tactic:
by

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

Goal state before:
pp: p : ℚ → Prop
⊢ (∃ r, p r) ↔ ∃ a b, b ≠ 0 ∧ p (↑a / ↑b)

Tactic:
by

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

Goal state before:
pp: a✝¹ b✝¹ c : ℕ
a✝ b✝ : Q(ℕ)
depth : ℕ
a b₀ c₀ b : Q(ℕ)
p : Q(Prop)
hp : «$p» =Q («$a».pow «$b₀» = «$c₀»)
b' : ℕ := Expr.natLit! b
d : ℕ := depth >>> 1
hi : Q(ℕ)
⊢ «$p» =Q («$a».pow «$b₀» = «$c₀»)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f r = g r

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
h1 : a.pow b = c
⊢ (Int.ofNat a).pow b = Int.ofNat c

Tactic:
by

Goal state after: