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

Goal state before:
pp: n k : ℕ
h : k.succ ≤ n.succ
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !

Tactic:
by

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

Goal state before:
pp: F : Type u_2
β : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
f : F
α : Type u_7
inst✝² : FunLike F α β
inst✝¹ : CommGroup α
inst✝ : GroupSeminormClass F α β
x y : α
⊢ f (x⁻¹ * y) = f (x * y⁻¹)

Tactic:
by

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

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f x ≤ f y + f (y / x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k m n : ℕ
hkm : k ≤ m
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
by

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

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommGroup β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ |f x - f y| ≤ f (x / y)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ n.descFactorial k = n ! / (n - k)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k m : ℕ
h : k ≤ m
⊢ k.descFactorial n ≤ m.descFactorial n

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommMonoid β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
a : α
⊢ 0 ≤ 2 • f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1 - 0) ^ 0 ≤ n.descFactorial 0

Tactic:
by

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

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupNormClass F α β
f : F
x : α
⊢ x = 1 → f x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ n.descFactorial (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
h : 0 + 2 ≤ n
⊢ n - (0 + 1) < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) ^ (0 + 2) < n.descFactorial (0 + 2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < n.descFactorial (k + 1 + 2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 0 → 0 ≤ n → (n + 1 - 0) ^ 0 < n.descFactorial 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 1 → 1 ≤ n → (n + 1 - 1) ^ 1 < n.descFactorial 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
x✝ : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n + 1 - (k + 2)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n.descFactorial 0 ≤ n ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial (k + 1) ≤ n ^ (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 2 ≤ 0 → n.descFactorial 0 < n ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 2 ≤ 1 → n.descFactorial 1 < n ^ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n - (k + 1) < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 2) < n ^ (k + 2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (2 * n)! ≤ (2 * n) ^ n * n !

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 2 ^ n * n ! ≤ (2 * n)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: ⊢ ascFactorial = ascFactorialBinary

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: ⊢ factorial = factorialBinarySplitting

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: ⊢ descFactorial = descFactorialBinary

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑(p ^ n) = ↑p ^ n

Tactic:
rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑(p ^ n) = ↑p ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹

Tactic:
by

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
⊢ ↑↑q = ↑q

Tactic:
by

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
m : ℕ
s : Bool
e : ℕ
⊢ ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑(q ^ n) = ↑q ^ n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
z : ℤ
hq : ↑q.num ≠ 0
⊢ ↑(q ^ z) = ↑q ^ z

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ 0 ≤ q.num

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ ↑⟨q, h⟩ = ↑q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
x✝¹ x✝ num✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
eq : ↑(NNRat.divNat x✝¹ (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ OfScientific.ofScientific x✝¹ true x✝ = ↑num✝ * ⅟↑denom✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a✝ n✝ : ℕ
⊢ OfScientific.ofScientific (↑a✝) false ↑n✝ = ↑(a✝ * 10 ^ n✝)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
this : fract x < 1
⊢ fract x ∈ Ico 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌊2 * fract x⌋ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
H : ⌊2 * fract x⌋ = 1
this : 0 < fract x
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round x = (⌊2 * x⌋ + 1) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
⊢ round 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
⊢ round 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n : ℕ
⊢ round ↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n : ℤ
⊢ round ↑n = n

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑(m + m) = 2 * x
⊢ 2 * ↑m = 2 * x

Tactic:
by

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

Goal state before:
pp: p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
⊢ p a

Tactic:
by

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

Goal state before:
pp: p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
h : 0 < 0
⊢ ¬0 < 0

Tactic:
by

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

Goal state before:
pp: n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
⊢ p n

Tactic:
by

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

Goal state before:
pp: n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
⊢ (n + 1).recOn one succ = succ n (n.recOn one succ)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
⊢ round x = ⌈2 * x⌉ / 2

Tactic:
by

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

Goal state before:
pp: n : ℕ+
⊢ n ≤ 1 ↔ n = 1

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ ↑(a - b) = if b < a then ↑a - ↑b else 1

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ a - b ≤ a

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
hab : a < b
⊢ a ≤ b - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑y) = round x + y

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
h : a < b
⊢ ↑(a + (b - a)) = ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a + 1) = round a + 1

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
h : b < a
⊢ a - b + b = a

Tactic:
by

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

Goal state before:
pp: n : ℕ
property✝ : 0 < n + 2
x✝ : ⟨n + 2, property✝⟩ ≠ 1
⊢ 0 < n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x - ↑y) = round x - y

Tactic:
by

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

Goal state before:
pp: k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑(k.modDivAux 0 (q + 1)).1 + ↑k * (k.modDivAux 0 (q + 1)).2 = 0 + ↑k * (q + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a - 1) = round a - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (↑y + x) = y + round x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (↑y + x) = ↑y + round x

Tactic:
by

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

Goal state before:
pp: m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)

Tactic:
by

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

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
by

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

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) + m.div k * ↑k = ↑m

Tactic:
by

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

Goal state before:
pp: m k : ℕ+
⊢ m.div k * ↑k + ↑(m.mod k) = ↑m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 1 - fract x ≤ fract x
⊢ 0 < fract x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(round x)| = min (fract x) (1 - fract x)

Tactic:
by

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

Goal state before:
pp: m k : ℕ+
⊢ m.mod k ≤ m ∧ m.mod k ≤ k

Tactic:
by

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

Goal state before:
pp: k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ a ≠ 0

Tactic:
by

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

Goal state before:
pp: k m : ℕ+
⊢ k ∣ m ↔ ↑k ∣ ↑m

Tactic:
by

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

Goal state before:
pp: k m : ℕ+
⊢ k ∣ m ↔ m.mod k = k

Tactic:
by

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

Goal state before:
pp: m n : ℕ+
⊢ m ∣ n → m ≤ n

Tactic:
by

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

Goal state before:
pp: m k : ℕ+
h : k ∣ m
⊢ k * m.divExact k = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ |x - ↑(round x)| ≤ |x - ↑z|

Tactic:
by

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

Goal state before:
pp: n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ 0 < a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round x = ⌊x + 1 / 2⌋

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
n : ℤ
⊢ round x = n ↔ x ∈ Ico (↑n - 1 / 2) (↑n + 1 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
⊢ round 2⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.PNat

Goal state before:
pp: n : ℕ+
n' : ℕ
k : ℕ+
k' : ℕ
h1 : CSLiftVal n n'
h2 : CSLiftVal k k'
⊢ n' + k' = CSLift.lift (n + k)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.PNat

Goal state before:
pp: n : ℕ+
n' : ℕ
k : ℕ+
k' : ℕ
h1 : CSLiftVal n n'
h2 : CSLiftVal k k'
⊢ n' * k' = CSLift.lift (n * k)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.PNat

Goal state before:
pp: n : ℕ+
n' k : ℕ
h1 : CSLiftVal n n'
⊢ n' ^ k = CSLift.lift (n ^ k)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
a b : R
⊢ a * -b = -(a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ Nat.rawCast 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ Nat.rawCast 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝ : Ring R
⊢ (Int.negOfNat n).rawCast = -n.rawCast

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: n d : ℕ
R : Type u_2
inst✝ : DivisionSemiring R
⊢ NNRat.rawCast n d = n.rawCast / d.rawCast

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: n d : ℕ
R : Type u_2
inst✝ : DivisionRing R
⊢ Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
⊢ round (-2⁻¹) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round x = 0 ↔ x ∈ Ico (-(1 / 2)) (1 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(round x)| ≤ 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
⊢ 0 < ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ x - 1 / 2 < ↑(round x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ ↑(round x) ≤ x + 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : LinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ round (f a) = round a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ ⌊a⌋ ≤ -1 ↔ a < 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ a < ↑⌊a⌋ + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ 0 < ⌊a⌋ ↔ 1 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ ⌊a⌋ = 0 ↔ a ∈ Ico 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z a : ℤ
⊢ a ≤ ⌊↑z⌋ ↔ a ≤ z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : ℤ
⊢ a ≤ ⌊↑n⌋ ↔ a ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ ⌊0⌋ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ ⌊1⌋ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a✝ : R
z a : ℤ
⊢ a ≤ ⌊a✝ + ↑z⌋ ↔ a ≤ ⌊a✝⌋ + z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ⌊a + 1⌋ = ⌊a⌋ + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z : ℤ
a : R
⊢ ⌊↑z + a⌋ = z + ⌊a⌋

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌊a + ↑n⌋ = ⌊a⌋ + ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : R
⊢ ⌊↑n + a⌋ = ↑n + ⌊a⌋

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ ⌊a - ↑z⌋ = ⌊a + ↑(-z)⌋

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌊a - ↑n⌋ = ⌊a⌋ - ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
h0 : b ≤ a
⊢ ↑⌊a⌋ + 1 - ↑⌊b⌋ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
⊢ |a - b| < 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ↑⌊a⌋ = a ↔ a ∈ range Int.cast

Tactic:
by

Goal state after: