mathlib-initiative/mathlib-tactics huggingface dataset:
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:
]

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

Goal state before:
pp: case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ n ! = n !

Tactic:
]

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

Goal state before:
pp: case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Tactic:
]

Goal state after:
case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case pos
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ 0 = 0

Tactic:
]

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) ∧ f y ≤ f x + f (x / y)

Tactic:
]

Goal state after:
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) ∧ f y ≤ f x + f (x / y)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ (k - n) * k.descFactorial n ≤ (m - n) * m.descFactorial n

Tactic:
]

Goal state after:
case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ (k - n) * k.descFactorial n ≤ (m - n) * m.descFactorial n
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 : α
⊢ f (a / a) ≤ f a + f a

Tactic:
]

Goal state after:
ι : 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 : α
⊢ f (a / a) ≤ f a + f a
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
]

Goal state after:
n k : ℕ
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * n.descFactorial k
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
]

Goal state after:
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
]

Goal state after:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * n.descFactorial (k + 2)
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
]

Goal state after:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
]

Goal state after:
n k : ℕ
x✝ : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
]

Goal state after:
n k : ℕ
⊢ (n - k) * n.descFactorial k ≤ n * n ^ k
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1).ascFactorial n * n ! ≤ (n + n) ^ n * n !

Tactic:
]

Goal state after:
n : ℕ
⊢ (n + 1).ascFactorial n * n ! ≤ (n + n) ^ n * n !
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case succ
n : ℕ
⊢ (n + 1)! * 2 ^ (n + 1) ≤ (n + 1 + (n + 1))!

Tactic:
]

Goal state after:
case succ
n : ℕ
⊢ (n + 1)! * 2 ^ (n + 1) ≤ (n + 1 + (n + 1))!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k = if n < k then 0 else (n - k + 1).ascFactorialBinary k

Tactic:
]

Goal state after:
n k : ℕ
⊢ n.descFactorial k = if n < k then 0 else (n - k + 1).ascFactorialBinary k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case pos
n k : ℕ
h : n < k
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1 + k - 1).descFactorial k

Tactic:
]

Goal state after:
case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1 + k - 1).descFactorial k
Module: Mathlib.Data.Rat.Cast.Lemmas

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
⊢ ↑(↑q.num / ↑q.den).num / ↑(↑q.num / ↑q.den).den = ↑q.num / ↑q.den

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
⊢ ↑(↑q.num / ↑q.den).num / ↑(↑q.num / ↑q.den).den = ↑q.num / ↑q.den
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
hn : (↑q.num / ↑q.den).num = ↑q.num
hd : (↑q.num / ↑q.den).den = q.den
⊢ ↑q.num / ↑q.den = ↑q.num / ↑q.den

Tactic:
]

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

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

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

Tactic:
]

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

Goal state before:
pp: case inr.e_a
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ (↑q)⁻¹ = (↑q)⁻¹

Tactic:
]

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.num / ↑q.den = ↑q.num / ↑q.den

Tactic:
]

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✝
⊢ ↑(NNRat.divNat x✝¹ (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
x✝¹ x✝ num✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
eq : ↑(NNRat.divNat x✝¹ (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ ↑(NNRat.divNat x✝¹ (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
Module: Mathlib.Tactic.NormNum.OfScientific

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
a✝ n✝ : ℕ
⊢ ↑↑(↑a✝ * 10 ^ ↑n✝) = ↑(a✝ * 10 ^ n✝)
Module: Mathlib.Algebra.Order.Round

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

Tactic:
]

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if 2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 = (0 + 1) / 2

pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 2 * fract x ∈ Ico 0 1

pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1

Tactic:
]

Goal state after:
case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 = (0 + 1) / 2

case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 2 * fract x ∈ Ico 0 1

case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
H : ⌊2 * fract x⌋ = 1
h : fract x ≤ 0
⊢ 2 * 0 < 1

Tactic:
]

Goal state after:
case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
H : ⌊2 * fract x⌋ = 1
h : fract x ≤ 0
⊢ 2 * 0 < 1
Module: Mathlib.Data.PNat.Basic

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑m = 2 * x
⊢ round x = m / 2
Module: Mathlib.Algebra.Order.Round

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

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
hx' : 2 * x ∉ range Int.cast
⊢ (⌊2 * x⌋ + 1) / 2 = (⌊2 * x⌋ + 1) / 2

Tactic:
]

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

Goal state before:
pp: case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1

Tactic:
]

Goal state after:
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1
Module: Mathlib.Data.PNat.Basic

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

Tactic:
]

Goal state after:
a b : ℕ+
⊢ (if b < a then ↑a - ↑b else 1) ≤ ↑a
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
hab : a < b
⊢ ↑a ≤ if 1 < b then ↑b - ↑1 else 1

Tactic:
]

Goal state after:
a b : ℕ+
hab : a < b
⊢ ↑a ≤ if 1 < b then ↑b - ↑1 else 1
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y

Tactic:
]

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

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

Tactic:
]

Goal state after:
a b : ℕ+
h : a < b
⊢ ↑a + (↑b - ↑a) = ↑b
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:
]

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

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + -↑y) = round x - y
Module: Mathlib.Data.PNat.Basic

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

Tactic:
]

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

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

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

Tactic:
]

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

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 : ℤ
⊢ y + round x = y + round x

Tactic:
]

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 : ℕ
⊢ ↑y + round x = ↑y + round x

Tactic:
]

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

Goal state before:
pp: m k : ℕ+
h₀ : 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False

Tactic:
]

Goal state after:
m k : ℕ+
h₀ : 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
Module: Mathlib.Data.PNat.Basic

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

Tactic:
]

Goal state after:
m k : ℕ+
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m
Module: Mathlib.Data.PNat.Basic

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

Tactic:
]

Goal state after:
m k : ℕ+
⊢ ↑k * m.div k + ↑(m.mod k) = ↑m
Module: Mathlib.Data.PNat.Basic

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

Tactic:
]

Goal state after:
m k : ℕ+
⊢ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑m ∧ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑k
Module: Mathlib.Algebra.Order.Round

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

Tactic:
]

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

Goal state before:
pp: case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Tactic:
]

Goal state after:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
Module: Mathlib.Algebra.Order.Round

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

Tactic:
]

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 : ℤ
⊢ fract x ≤ |x - ↑z| ∨ 1 - fract x ≤ |x - ↑z|

Tactic:
]

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ fract x ≤ |x - ↑z| ∨ 1 - fract x ≤ |x - ↑z|
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(x - ↑z)

Tactic:
]

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(x - ↑z)
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ ↑k * n.succ = ↑k * n.succ

Tactic:
]

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

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

Tactic:
]

Goal state after:
k m : ℕ+
⊢ ↑k ∣ ↑m ↔ m.mod k = k
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: k m : ℕ+
⊢ ↑m % ↑k = 0 ↔ m.mod k = k

Tactic:
]

Goal state after:
k m : ℕ+
⊢ ↑m % ↑k = 0 ↔ m.mod k = k
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ ↑k = ↑k

Tactic:
]

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

Goal state before:
pp: case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑m % ↑k = ↑k
⊢ ↑m % ↑k = 0

Tactic:
]

Goal state after:
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑m % ↑k = ↑k
⊢ ↑m % ↑k = 0
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m n : ℕ+
⊢ n.mod m = m → m ≤ n

Tactic:
]

Goal state after:
m n : ℕ+
⊢ n.mod m = m → m ≤ n
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ↑⌊x⌋ ≤ ↑z - 1

Tactic:
]

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ↑⌊x⌋ ≤ ↑z - 1
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m n : ℕ+
h : n.mod m = m
⊢ n.mod m ≤ n

Tactic:
]

Goal state after:
m n : ℕ+
h : n.mod m = m
⊢ n.mod m ≤ n
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(fract x + ↑⌊x⌋ - ↑z)

Tactic:
rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel,
      le_sub_comm]

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ↑⌊x⌋ ≤ ↑z - 1
Module: Mathlib.Data.PNat.Basic

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

Tactic:
]

Goal state after:
m k : ℕ+
h : k ∣ m
⊢ ↑k * ↑(m.divExact k) = ↑m
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ x < ↑z

Tactic:
]

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ x < ↑z
Module: Mathlib.Data.PNat.Basic

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

Tactic:
]

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

Goal state before:
pp: n : ℕ+
a : ℕ
h : 0 ∣ ↑n
hzero : a = 0
⊢ False

Tactic:
]

Goal state after:
n : ℕ+
a : ℕ
h : 0 ∣ ↑n
hzero : a = 0
⊢ False
Module: Mathlib.Algebra.Order.Round

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

Tactic:
]

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (⌊2 * x⌋ + 1) / 2 = ⌊↑2 * (x + 1 / 2)⌋ / 2
Module: Mathlib.Algebra.Order.Round

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

Tactic:
]

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ min (↑(m % n) / ↑n) (1 - ↑(m % n) / ↑n) = min (↑(m % n) / ↑n) (1 - ↑(m % n) / ↑n)

Tactic:
]

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 - 1 < ↑⌊x + 1 / 2⌋

Tactic:
]

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ x + 1 / 2 - 1 < ↑⌊x + 1 / 2⌋
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
  rw [round_eq x, show x - 1 / 2 = x + 1 / 2 - 1 by linarith]
  exact Int.sub_one_lt_floor (x + 1 / 2)

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⌋ ≤ x + 1 / 2

Tactic:
]

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
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
⊢ 1 ≤ a ↔ 1 ≤ a

Tactic:
]

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
⊢ ↑z ≤ a ∧ a < ↑z + 1 ↔ ↑z ≤ a ∧ a < ↑z + 1

Tactic:
]

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

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

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

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

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 - ↑z ≤ a✝ ↔ ↑a - ↑z ≤ a✝

Tactic:
]

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

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

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a⌋ + ↑⌊b⌋ ≤ a + b
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:
]

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