mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i ↦ f i) ↔ x✝ ∈ range fun i ↦ ↑(f i)

Tactic:
;

Goal state after:
case e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i ↦ f i) ↔ x✝ ∈ range fun i ↦ ↑(f i)
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ≥0
⊢ 0 ≤ ↑q.num / ↑q.den

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ≥0
⊢ 0 ≤ ↑q.num / ↑q.den
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑(⟨↑r, ⋯⟩ * ⟨(↑r)⁻¹, ⋯⟩) = ↑1

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑(⟨↑r, ⋯⟩ * ⟨(↑r)⁻¹, ⋯⟩) = ↑1
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑(⟨(↑r)⁻¹, ⋯⟩ * ⟨↑r, ⋯⟩) = ↑1

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑(⟨(↑r)⁻¹, ⋯⟩ * ⟨↑r, ⋯⟩) = ↑1
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 ≤ r }ˣ
⊢ ↑↑((fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) ((fun r ↦ ⟨↑↑r, ⋯⟩) r)) = ↑↑r

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 ≤ r }ˣ
⊢ ↑↑((fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) ((fun r ↦ ⟨↑↑r, ⋯⟩) r)) = ↑↑r
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑((fun r ↦ ⟨↑↑r, ⋯⟩) ((fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) r)) = ↑r

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑((fun r ↦ ⟨↑↑r, ⋯⟩) ((fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) r)) = ↑r
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : { x // 0 ≤ x }
⊢ 0 ≤ ↑q * ↑a

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : { x // 0 ≤ x }
⊢ 0 ≤ ↑q * ↑a
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a
Module: Mathlib.Tactic.NormNum.Eq

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : CharZero α
num✝¹ num✝ denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul denom✝ = num✝.mul denom✝¹) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : CharZero α
num✝¹ num✝ denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul denom✝ = num✝.mul denom✝¹) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹
Module: Mathlib.Tactic.NormNum.Eq

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ a / ↑b' = ↑q

Tactic:
;

Goal state after:
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ a / ↑b' = ↑q
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
⊢ a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
⊢ a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x a : ι
⊢ a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x a : ι
⊢ a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ 1 x = 1

Tactic:
;

Goal state after:
case neg
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ 1 x = 1
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
hf : Injective f
x : ι
hx : x ∈ mulSupport g
⊢ f x ∈ mulSupport (extend f g 1)

Tactic:
;

Goal state after:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
hf : Injective f
x : ι
hx : x ∈ mulSupport g
⊢ f x ∈ mulSupport (extend f g 1)
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
c : M
hc : c ≠ 1
x : ι
⊢ (x ∈ mulSupport fun x ↦ c) ↔ x ∈ univ

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
c : M
hc : c ≠ 1
x : ι
⊢ (x ∈ mulSupport fun x ↦ c) ↔ x ∈ univ
Module: Mathlib.Data.Int.Cast.Field

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
k : ℤ
hn : ↑0 ≠ 0
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
k : ℤ
hn : ↑0 ≠ 0
⊢ False
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
;

Goal state after:
$u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
;

Goal state after:
$u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ max a 1 = (fun x1 x2 ↦ max x1 x2) 1 a

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ max a 1 = (fun x1 x2 ↦ max x1 x2) 1 a
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : 1 < a
⊢ a⁺ᵐ = a

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : 1 < a
⊢ a⁺ᵐ = a
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ max a⁻¹ 1 = (fun x1 x2 ↦ max x1 x2) 1 a⁻¹

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ max a⁻¹ 1 = (fun x1 x2 ↦ max x1 x2) 1 a⁻¹
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: ⊢ ascFactorial 0 (succ 0) = 0

Tactic:
by
    rw [ascFactorial_succ, ascFactorial_zero, Nat.zero_add, Nat.zero_mul]

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

Goal state before:
pp: n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1) ^ 1 < (n + 1).ascFactorial 1

Tactic:
;

Goal state after:
n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1) ^ 1 < (n + 1).ascFactorial 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1).ascFactorial 1 < (n + 1) ^ 1

Tactic:
;

Goal state after:
n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1).ascFactorial 1 < (n + 1) ^ 1
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
apply Nat.mul_le_mul_left

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

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
n : ℕ
hn : n ≠ 0
a✝ : 2 ≤ 1
⊢ n.descFactorial 1 < n ^ 1
Module: Mathlib.Data.PNat.Basic

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

Tactic:
by
  rw [natPred, add_tsub_cancel_iff_le.mpr <| show 1 ≤ (n : ℕ) from n.2]

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:
← round_sub_intCast a 1,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a - 1) = round (a - ↑1)
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: 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.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n
Module: Mathlib.Algebra.Order.Floor.Ring

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

Tactic:
;

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a b : R
⊢ a + b - ↑⌊a + b⌋ - (a - ↑⌊a⌋) - (b - ↑⌊b⌋) = ↑(⌊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 : R
⊢ 0 ≤ fract a ∧ fract a < 1

Tactic:
;

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ 0 ≤ fract a ∧ fract a < 1
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 - ↑⌊a⌋ = b - ↑⌊b⌋
⊢ 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
h : a - ↑⌊a⌋ = b - ↑⌊b⌋
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ fract a * ↑0 - fract (a * ↑0) = ↑0

Tactic:
;

Goal state after:
case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ fract a * ↑0 - fract (a * ↑0) = ↑0
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
s : Set R
⊢ fract ⁻¹' s = ⋃ m, (fun x ↦ x - ↑m) ⁻¹' (s ∩ Ico 0 1)

Tactic:
by
  ext x
  simp only [mem_preimage, mem_iUnion, mem_inter_iff]
  refine ⟨fun h => ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, ?_⟩
  rintro ⟨m, hms, hm0, hm1⟩
  obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩
  exact hms

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
s : Set R
x : R
⊢ (∃ x_1 ∈ s, fract x_1 = x) ↔ ∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1

Tactic:
;

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ (∃ x_1 ∈ s, fract x_1 = x) ↔ ∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌊↑m⌋ m

Tactic:
;

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌊↑m⌋ m
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌊↑m⌋ m

Tactic:
;

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌊↑m⌋ m
Module: Mathlib.Tactic.Positivity.Basic

Goal state before:
pp: a : ℤ
ha : 0 < a
⊢ 0 < 1

Tactic:
;

Goal state after:
a : ℤ
ha : 0 < a
⊢ 0 < 1
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌈↑m⌉ m

Tactic:
;

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌈↑m⌉ m
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌈↑m⌉ m

Tactic:
;

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌈↑m⌉ m
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
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - ↑⌈a⌉

Tactic:
rw [this, ← self_sub_fract]
    abel

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat (fract ↑m) 0

Tactic:
;

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat (fract ↑m) 0
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsNat (fract ↑m) 0

Tactic:
;

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsNat (fract ↑m) 0
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat (round ↑m) m

Tactic:
;

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat (round ↑m) m
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case hbc
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ a < ↑⌊a⌋ + 1

Tactic:
;

Goal state after:
case hbc
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ a < ↑⌊a⌋ + 1
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt (round ↑m) m

Tactic:
;

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt (round ↑m) m
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < 1
hn0 : n = 0
⊢ False

Tactic:
;

Goal state after:
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < 1
hn0 : n = 0
⊢ False
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ 0 < b

Tactic:
;

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ 0 < b
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: case h
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : n < 0
⊢ n + 1 ≤ 0

Tactic:
;

Goal state after:
case h
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : n < 0
⊢ n + 1 ≤ 0
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0

Tactic:
;

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ l ∈ Icc l (l + a)

Tactic:
;

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ l ∈ Icc l (l + a)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋

Tactic:
;

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋