awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
p : ℤ
hp : Even p
a : α
inl : ∀ (h : |a| = a), |a| ^ p = a ^ p
inr : ∀ (h : |a| = -a), |a| ^ p = a ^ p
⊢ |a| ^ p = a ^ p

Tactic:
rcases abs_choice a with h | h

Premises used: abs_choice
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
p : ℤ
hp : Even p
a : α
h : |a| = a
⊢ |a| ^ p = a ^ p

Tactic:
simp only [h, hp.neg_zpow _]

Premises used: Even.neg_zpow
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
p : ℤ
hp : Even p
a : α
h : |a| = -a
⊢ |a| ^ p = a ^ p

Tactic:
simp only [h, hp.neg_zpow _]

Premises used: Even.neg_zpow
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : ofNat m ≠ 0
simp : ∀ (hn : ¬m = 0), a ^ m = b ^ m ↔ a = b ∨ a = -b ∧ Even m
⊢ a ^ ofNat m = b ^ ofNat m ↔ a = b ∨ a = -b ∧ Even (ofNat m)

Tactic:
simp only [Int.ofNat_eq_natCast, ne_eq, Nat.cast_eq_zero, zpow_natCast, Int.even_coe_nat] at *

Premises used: zpow_natCast, Int.ofNat_eq_natCast, ne_eq, Nat.cast_eq_zero, Int.even_coe_nat
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : ¬m = 0
⊢ a ^ m = b ^ m ↔ a = b ∨ a = -b ∧ Even m

Tactic:
pow_eq_pow_iff_of_ne_zero hn

Premises used: pow_eq_pow_iff_of_ne_zero
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : ¬m = 0
⊢ a ^ m = b ^ m ↔ a = b ∨ a = -b ∧ Even m

Tactic:
exact pow_eq_pow_iff_of_ne_zero hn

Premises used: pow_eq_pow_iff_of_ne_zero
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : -[m+1] ≠ 0
simp : ∀ (hn : ¬m.succ = 0), a ^ m.succ = b ^ m.succ ↔ a = b ∨ a = -b ∧ Even m.succ
⊢ a ^ -[m+1] = b ^ -[m+1] ↔ a = b ∨ a = -b ∧ Even -[m+1]

Tactic:
simp only [← neg_ofNat_succ, ne_eq, neg_eq_zero, Nat.cast_eq_zero, zpow_neg, zpow_natCast,
      inv_inj, even_neg, Int.even_coe_nat] at *

Premises used: zpow_natCast, neg_eq_zero, ne_eq, Int.neg_ofNat_succ, inv_inj, Nat.cast_eq_zero, zpow_neg, even_neg, Int.even_coe_nat
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : ¬m.succ = 0
⊢ a ^ m.succ = b ^ m.succ ↔ a = b ∨ a = -b ∧ Even m.succ

Tactic:
pow_eq_pow_iff_of_ne_zero hn

Premises used: pow_eq_pow_iff_of_ne_zero
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : ¬m.succ = 0
⊢ a ^ m.succ = b ^ m.succ ↔ a = b ∨ a = -b ∧ Even m.succ

Tactic:
exact pow_eq_pow_iff_of_ne_zero hn

Premises used: pow_eq_pow_iff_of_ne_zero
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
inl : HPow.hPow (β := ℤ) a 0 = HPow.hPow (β := ℤ) b 0 ↔ Eq (α := ℤ) 0 0 ∨ a = b ∨ a = -b ∧ Even (α := ℤ) 0
inr : ∀ (hn : n ≠ 0), a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ HPow.hPow (β := ℤ) a 0 = HPow.hPow (β := ℤ) b 0 ↔ Eq (α := ℤ) 0 0 ∨ a = b ∨ a = -b ∧ Even (α := ℤ) 0

Tactic:
simp [zpow_eq_zpow_iff_of_ne_zero₀, *]

Premises used: zpow_eq_zpow_iff_of_ne_zero₀
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
simp [zpow_eq_zpow_iff_of_ne_zero₀, *]

Premises used: zpow_eq_zpow_iff_of_ne_zero₀
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n

Tactic:
simp [← zpow_eq_zpow_iff_of_ne_zero₀ hn]

Premises used: zpow_eq_zpow_iff_of_ne_zero₀
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
⊢ a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

Tactic:
simp [← zpow_eq_zpow_iff_cases₀]

Premises used: zpow_eq_zpow_iff_cases₀
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
hb : b ≠ 0
m : ℕ
⊢ a ^ ofNat m = -b ^ ofNat m ↔ a = -b ∧ Odd (ofNat m)

Tactic:
simp [pow_eq_neg_pow_iff, hb]

Premises used: pow_eq_neg_pow_iff
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
hb : b ≠ 0
m : ℕ
simp : a = -b ∧ Odd m.succ ↔ a = -b ∧ Odd (α := ℤ) (-(↑m.succ : ℤ))
⊢ a ^ -[m+1] = -b ^ -[m+1] ↔ a = -b ∧ Odd -[m+1]

Tactic:
simp only [← neg_ofNat_succ, zpow_neg, ← inv_neg, pow_eq_neg_pow_iff hb, inv_inj,
      zpow_natCast]

Premises used: zpow_natCast, pow_eq_neg_pow_iff, inv_neg, Int.neg_ofNat_succ, inv_inj, zpow_neg
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
hb : b ≠ 0
m : ℕ
⊢ a = -b ∧ Odd m.succ ↔ a = -b ∧ Odd (α := ℤ) (-(↑m.succ : ℤ))

Tactic:
simp [parity_simps]
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n

Tactic:
simpa using zpow_eq_neg_zpow_iff₀ (α := α) one_ne_zero

Premises used: zpow_eq_neg_zpow_iff₀, one_ne_zero
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
H : 1 < a
n : ℕ
⊢ (↑n : α) ≤ (a ^ n - 1) / (a - 1)

Tactic:
(le_div_iff₀ (sub_pos.2 H)).2 <|
    le_sub_left_of_add_le <| one_add_mul_sub_le_pow ((neg_le_self zero_le_one).trans H.le) _

Premises used: Iff.mpr, sub_pos, one_add_mul_sub_le_pow, LT.lt.le, neg_le_self, zero_le_one, le_sub_left_of_add_le, LE.le.trans, le_div_iff₀
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
H : 1 < a
n : ℕ
⊢ (↑n : α) ≤ a ^ n / (a - 1)

Tactic:
(n.cast_le_pow_sub_div_sub H).trans <|
    div_le_div_of_nonneg_right (sub_le_self _ zero_le_one) (sub_nonneg.2 H.le)

Premises used: Iff.mpr, div_le_div_of_nonneg_right, LT.lt.le, Nat.cast_le_pow_sub_div_sub, zero_le_one, sub_le_self, LE.le.trans, sub_nonneg
-- Module: Mathlib.Algebra.Order.Field.Subfield
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
s : Subfield K
⊢ IsStrictOrderedRing.{u_1} ↥s

Tactic:
Function.Injective.isStrictOrderedRing
    Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) .rfl .rfl

Premises used: Iff.rfl, Function.Injective.isStrictOrderedRing, Subtype.val, rfl
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
a n : ℕ
h : 0 ≤ a
rw : n ≤ id a ↔ n ≤ a
rw₁ rw₂ : n ≤ a ↔ n ≤ a
⊢ n ≤ id a ↔ (↑n : ℕ) ≤ a

Tactic:
rw [Nat.cast_id, id_def]

Premises used: Nat.cast_id, id_def
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
n a : ℕ
rw : id n ≤ a ↔ n ≤ a
rw₁ rw₂ : n ≤ a ↔ n ≤ a
⊢ id n ≤ a ↔ n ≤ (↑a : ℕ)

Tactic:
rw [Nat.cast_id, id_def]

Premises used: Nat.cast_id, id_def
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
⊢ floor = id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
⊢ ceil = id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ (↑n : α) ≤ a

Tactic:
FloorSemiring.gc_floor ha

Premises used: Nat.floor, FloorSemiring.gc_floor
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : FloorSemiring α
a : α
n : ℕ
inst_3 : IsOrderedRing α
h : (↑n : α) ≤ a
⊢ n ≤ ⌊a⌋₊

Tactic:
(le_floor_iff <| n.cast_nonneg.trans h).2 h

Premises used: Iff.mpr, Nat.cast_nonneg, Nat.le_floor_iff, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : FloorSemiring α
⊢ GaloisConnection.{u_2, 0} (α := α) ceil Nat.cast

Tactic:
FloorSemiring.gc_ceil

Premises used: FloorSemiring.gc_ceil, Nat.ceil
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : FloorSemiring α
a : α
n : ℕ
⊢ ⌈a⌉₊ ≤ n ↔ a ≤ (↑n : α)

Tactic:
gc_ceil_coe _ _

Premises used: Nat.gc_ceil_coe
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : FloorSemiring α
a : α
n : ℕ
⊢ NeZero.{u_2} (R := α) 1

Tactic:
⟨fun h ↦ not_succ_le_self ⌊(0 : α)⌋₊ <|
    (le_floor_iff (le_refl 0)).mpr (eq_zero_of_zero_eq_one h.symm _).le⟩

Premises used: Iff.mpr, le_refl, NeZero.mk, Eq.le, Nat.le_floor_iff, Nat.cast, eq_zero_of_zero_eq_one, Nat.floor, OfNat.ofNat, Eq.symm, Nat.succ, Nat.not_succ_le_self
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : FloorSemiring α
a : α
n : ℕ
⊢ Nontrivial α

Tactic:
NeZero.nontrivial 1

Premises used: NeZero.nontrivial, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : FloorSemiring α
a : α
n : ℕ
⊢ n < ⌈a⌉₊ ↔ (↑n : α) < a

Tactic:
lt_iff_lt_of_le_iff_le ceil_le

Premises used: lt_iff_lt_of_le_iff_le, Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : FloorSemiring α
a : α
rw : (↑0 : α) < a ↔ 0 < a
rw₁ rw₂ : 0 < a ↔ 0 < a
⊢ 0 < ⌈a⌉₊ ↔ 0 < a

Tactic:
rw [lt_ceil, cast_zero]

Premises used: Nat.lt_ceil, Nat.cast_zero
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
rw : a ≤ b ↔ a ≤ id b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ (↑a : ℤ) ≤ b ↔ a ≤ id b

Tactic:
rw [Int.cast_id, id_def]

Premises used: id_def, Int.cast_id
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
rw : id a ≤ b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ id a ≤ b ↔ a ≤ (↑b : ℤ)

Tactic:
rw [Int.cast_id, id_def]

Premises used: id_def, Int.cast_id
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
floor : α → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
a : α
z : ℤ
rw : -z ≤ floor (-a) ↔ a ≤ (↑z : α)
rw₁ : (↑(-z) : α) ≤ -a ↔ a ≤ (↑z : α)
rw₂ : -(↑z : α) ≤ -a ↔ a ≤ (↑z : α)
rw₃ rw₄ : a ≤ (↑z : α) ↔ a ≤ (↑z : α)
⊢ (fun (a : α) ↦ -floor (-a)) a ≤ z ↔ a ≤ (↑z : α)

Tactic:
rw [neg_le, ← gc_coe_floor, Int.cast_neg, neg_le_neg_iff]

Premises used: Int.cast_neg, neg_le, neg_le_neg_iff
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
ceil : α → ℤ
gc_ceil_coe : GaloisConnection ceil Int.cast
a : ℤ
z : α
rw : (↑a : α) ≤ z ↔ ceil (-z) ≤ -a
rw₁ : (↑a : α) ≤ z ↔ -z ≤ (↑(-a) : α)
rw₂ : (↑a : α) ≤ z ↔ -z ≤ -(↑a : α)
rw₃ rw₄ : (↑a : α) ≤ z ↔ (↑a : α) ≤ z
⊢ (↑a : α) ≤ z ↔ a ≤ (fun (a : α) ↦ -ceil (-a)) z

Tactic:
rw [le_neg, gc_ceil_coe, Int.cast_neg, neg_le_neg_iff]

Premises used: Int.cast_neg, le_neg, neg_le_neg_iff
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
x : α
below : ∃ (n : ℤ), (↑n : α) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : α)
n : { x_1 : ℤ // x ≤ (↑x_1 : α) } := indefiniteDescription (fun (x_1 : ℤ) ↦ x ≤ (↑x_1 : α)) above
refine : ∀ (m : ℤ) (hm : (fun (x_1 : ℤ) ↦ (↑x_1 : α) ≤ x) m), m ≤ (↑n : ℤ)
⊢ { n : ℤ // (↑n : α) ≤ x ∧ ∀ (m : ℤ), (↑m : α) ≤ x → m ≤ n }

Tactic:
refine Int.greatestOfBdd (P := (· ≤ x)) n.1 (fun m hm ↦ ?_) below

Premises used: Int.greatestOfBdd, Subtype.val
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
x : α
below : ∃ (n : ℤ), (↑n : α) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : α)
n : { x_1 : ℤ // x ≤ (↑x_1 : α) } := indefiniteDescription (fun (x_1 : ℤ) ↦ x ≤ (↑x_1 : α)) above
m : ℤ
hm : (fun (x_1 : ℤ) ↦ (↑x_1 : α) ≤ x) m
rw : LE.le.{u_4} (α := α) (↑m : α) (↑(↑n : ℤ) : α)
⊢ m ≤ (↑n : ℤ)

Tactic:
rw [← Int.cast_le (R := α)]

Premises used: Int.cast_le
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
x : α
below : ∃ (n : ℤ), (↑n : α) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : α)
n : { x_1 : ℤ // x ≤ (↑x_1 : α) } := indefiniteDescription (fun (x_1 : ℤ) ↦ x ≤ (↑x_1 : α)) above
m : ℤ
hm : (fun (x_1 : ℤ) ↦ (↑x_1 : α) ≤ x) m
⊢ LE.le.{u_4} (α := α) (↑m : α) (↑(↑n : ℤ) : α)

Tactic:
hm.trans n.2

Premises used: LE.le.trans, Subtype.property
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
x : α
below : ∃ (n : ℤ), (↑n : α) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : α)
n : { x_1 : ℤ // x ≤ (↑x_1 : α) } := indefiniteDescription (fun (x_1 : ℤ) ↦ x ≤ (↑x_1 : α)) above
m : ℤ
hm : (fun (x_1 : ℤ) ↦ (↑x_1 : α) ≤ x) m
⊢ LE.le.{u_4} (α := α) (↑m : α) (↑(↑n : ℤ) : α)

Tactic:
exact hm.trans n.2

Premises used: LE.le.trans, Subtype.property
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_4
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
x : α
below : ∃ (n : ℤ), (↑n : α) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : α)
⊢ ∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ (↑z : α) ≤ x

Tactic:
⟨_, fun n ↦ ⟨?_, (floorAux below above).2.2 _⟩⟩

Premises used: _private.0.floorAux, And.right, Iff.intro, Exists.intro, Subtype.property
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_4
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
x : α
below : ∃ (n : ℤ), (↑n : α) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : α)
refine : ∀ (n : ℤ), n ≤ (↑(floorAux below above) : ℤ) → (↑n : α) ≤ x
⊢ ∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ (↑z : α) ≤ x

Tactic:
refine ⟨_, fun n ↦ ⟨?_, (floorAux below above).2.2 _⟩⟩
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_4
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
x : α
below : ∃ (n : ℤ), (↑n : α) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : α)
n : ℤ
rw : LE.le.{u_4} (α := α) (↑n : α) (↑(↑(floorAux below above) : ℤ) : α) → (↑n : α) ≤ x
⊢ n ≤ (↑(floorAux below above) : ℤ) → (↑n : α) ≤ x

Tactic:
rw [← Int.cast_le (R := α)]

Premises used: Int.cast_le
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_4
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
x : α
below : ∃ (n : ℤ), (↑n : α) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : α)
n : ℤ
⊢ LE.le.{u_4} (α := α) (↑n : α) (↑(↑(floorAux below above) : ℤ) : α) → (↑n : α) ≤ x

Tactic:
le_trans' (floorAux below above).2.1

Premises used: _private.0.floorAux, And.left, le_trans', Subtype.property
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_4
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
x : α
below : ∃ (n : ℤ), (↑n : α) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : α)
n : ℤ
⊢ LE.le.{u_4} (α := α) (↑n : α) (↑(↑(floorAux below above) : ℤ) : α) → (↑n : α) ≤ x

Tactic:
exact le_trans' (floorAux below above).2.1

Premises used: _private.0.floorAux, And.left, le_trans', Subtype.property
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
bounded : ∀ (x : α), ∃ (n : ℕ), x ≤ (↑n : α)
x : α
obtain : ∀ (n : ℕ) (hn : -x ≤ (↑n : α)), ∃ (n : ℤ), (↑n : α) ≤ x
⊢ ∃ (n : ℤ), (↑n : α) ≤ x

Tactic:
obtain ⟨n, hn⟩ := bounded (-x)

Premises used: Neg.neg
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
bounded : ∀ (x : α), ∃ (n : ℕ), x ≤ (↑n : α)
x : α
n : ℕ
hn : -x ≤ (↑n : α)
h : (↑(-(↑n : ℤ)) : α) ≤ x
⊢ ∃ (n : ℤ), (↑n : α) ≤ x

Tactic:
use -n
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
bounded : ∀ (x : α), ∃ (n : ℕ), x ≤ (↑n : α)
x : α
n : ℕ
hn : -x ≤ (↑n : α)
⊢ (↑(-(↑n : ℤ)) : α) ≤ x

Tactic:
simpa [neg_le]

Premises used: neg_le
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
bounded : ∀ (x : α), ∃ (n : ℕ), x ≤ (↑n : α)
below : ∀ (x : α), ∃ (n : ℤ), (↑n : α) ≤ x
x : α
obtain : ∀ (n : ℕ) (hn : x ≤ (↑n : α)), ∃ (n : ℤ), x ≤ (↑n : α)
⊢ ∃ (n : ℤ), x ≤ (↑n : α)

Tactic:
obtain ⟨n, hn⟩ := bounded x
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
bounded : ∀ (x : α), ∃ (n : ℕ), x ≤ (↑n : α)
below : ∀ (x : α), ∃ (n : ℤ), (↑n : α) ≤ x
x : α
n : ℕ
hn : x ≤ (↑n : α)
h : x ≤ (↑(↑n : ℤ) : α)
⊢ ∃ (n : ℤ), x ≤ (↑n : α)

Tactic:
use n
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
bounded : ∀ (x : α), ∃ (n : ℕ), x ≤ (↑n : α)
below : ∀ (x : α), ∃ (n : ℤ), (↑n : α) ≤ x
x : α
n : ℕ
hn : x ≤ (↑n : α)
⊢ x ≤ (↑(↑n : ℤ) : α)

Tactic:
exact_mod_cast hn
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
x : ℤ
⊢ fract x = 0 x

Tactic:
simp [fract]

Premises used: Int.fract
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
⊢ @FloorRing.floor = @floor

Tactic:
rfl

Premises used: Int.floor, rfl
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
⊢ @FloorRing.ceil = @ceil

Tactic:
rfl

Premises used: Int.ceil, rfl
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
z : ℤ
a b : α
⊢ NeZero.{u_2} (R := α) 1

Tactic:
⟨fun h ↦ (Int.lt_succ ⌊(0 : α)⌋).not_ge <|
    (FloorRing.gc_coe_floor _ _).mp (eq_zero_of_zero_eq_one h.symm _).le⟩

Premises used: Int.cast, NeZero.mk, Int.floor, Int.lt_succ, Eq.le, eq_zero_of_zero_eq_one, HAdd.hAdd, Iff.mp, FloorRing.gc_coe_floor, LT.lt.not_ge, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
z : ℤ
a b : α
⊢ Nontrivial α

Tactic:
NeZero.nontrivial 1

Premises used: NeZero.nontrivial, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
⊢ GaloisConnection.{0, u_2} (β := α) Int.cast floor

Tactic:
FloorRing.gc_coe_floor

Premises used: Int.floor, FloorRing.gc_coe_floor
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
z : ℤ
a : α
⊢ z ≤ ⌊a⌋ ↔ (↑z : α) ≤ a

Tactic:
(gc_coe_floor z a).symm

Premises used: Int.gc_coe_floor, Iff.symm
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
z : ℤ
a : α
⊢ ⌊a⌋ < z ↔ a < (↑z : α)

Tactic:
lt_iff_lt_of_le_iff_le le_floor

Premises used: Int.le_floor, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
⊢ (↑⌊a⌋ : α) ≤ a

Tactic:
gc_coe_floor.l_u_le a

Premises used: Int.gc_coe_floor, GaloisConnection.l_u_le
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
rw : (↑0 : α) ≤ a ↔ 0 ≤ a
rw₁ rw₂ : 0 ≤ a ↔ 0 ≤ a
⊢ 0 ≤ ⌊a⌋ ↔ 0 ≤ a

Tactic:
rw [le_floor, Int.cast_zero]

Premises used: Int.cast_zero, Int.le_floor
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
inst_3 : IsOrderedRing α
ha : a ≤ 0
rw : LE.le.{u_2} (α := α) (↑⌊a⌋ : α) 0
⊢ ⌊a⌋ ≤ 0

Tactic:
rw [← @cast_le α, Int.cast_zero]

Premises used: Int.cast_le, Int.cast_zero
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
inst_3 : IsOrderedRing α
ha : a ≤ 0
⊢ LE.le.{u_2} (α := α) (↑⌊a⌋ : α) 0

Tactic:
(floor_le a).trans ha

Premises used: Int.floor_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
inst_3 : IsOrderedRing α
ha : a ≤ 0
⊢ LE.le.{u_2} (α := α) (↑⌊a⌋ : α) 0

Tactic:
exact (floor_le a).trans ha

Premises used: Int.floor_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
⊢ GaloisConnection.{u_2, 0} (α := α) ceil Int.cast

Tactic:
FloorRing.gc_ceil_coe

Premises used: FloorRing.gc_ceil_coe, Int.ceil
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
z : ℤ
a : α
⊢ ⌈a⌉ ≤ z ↔ a ≤ (↑z : α)

Tactic:
gc_ceil_coe a z

Premises used: Int.gc_ceil_coe
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
z : ℤ
a : α
⊢ z < ⌈a⌉ ↔ (↑z : α) < a

Tactic:
lt_iff_lt_of_le_iff_le ceil_le

Premises used: Int.ceil_le, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
⊢ a ≤ (↑⌈a⌉ : α)

Tactic:
gc_ceil_coe.le_u_l a

Premises used: GaloisConnection.le_u_l, Int.gc_ceil_coe
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
inst_3 : IsOrderedRing α
ha : 0 ≤ a
⊢ 0 ≤ ⌈a⌉

Tactic:
mod_cast ha.trans (le_ceil a)

Premises used: Int.cast, congrArg, Int.cast_zero, Int.le_ceil, cast, LE.le, Int.cast_le._simp_1, congrFun', Nat.cast_zero, LE.le.trans, Int.ceil, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
rw : (↑0 : α) < a ↔ 0 < a
rw₁ rw₂ : 0 < a ↔ 0 < a
⊢ 0 < ⌈a⌉ ↔ 0 < a

Tactic:
rw [lt_ceil, cast_zero]

Premises used: Int.lt_ceil, Int.cast_zero
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
inst_3 : FloorRing α
a : α
n : ℕ
ha : 0 ≤ a
rw : (↑n : ℤ) ≤ ⌊a⌋ ↔ (↑n : α) ≤ a
rw₁ : (↑(↑n : ℤ) : α) ≤ a ↔ (↑n : α) ≤ a
rw₂ rw₃ : (↑n : α) ≤ a ↔ (↑n : α) ≤ a
⊢ n ≤ ⌊a⌋.toNat ↔ (↑n : α) ≤ a

Tactic:
rw [Int.le_toNat (Int.floor_nonneg.2 ha), Int.le_floor, Int.cast_natCast]

Premises used: Iff.mpr, Int.cast_natCast, Int.le_toNat, Int.floor_nonneg, Int.le_floor
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
inst_3 : FloorRing α
a : α
n : ℕ
rw : ⌈a⌉ ≤ (↑n : ℤ) ↔ a ≤ (↑n : α)
rw₁ : a ≤ (↑(↑n : ℤ) : α) ↔ a ≤ (↑n : α)
rw₂ rw₃ : a ≤ (↑n : α) ↔ a ≤ (↑n : α)
⊢ (fun (a : α) ↦ ⌈a⌉.toNat) a ≤ n ↔ a ≤ (↑n : α)

Tactic:
rw [Int.toNat_le, Int.ceil_le, Int.cast_natCast]

Premises used: Int.cast_natCast, Int.ceil_le, Int.toNat_le
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
inst_3 : FloorRing α
a : α
⊢ ⌊a⌋.toNat = ⌊a⌋₊

Tactic:
rfl

Premises used: Nat.floor, Int.toNat, rfl
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
inst_3 : FloorRing α
a : α
⊢ ⌈a⌉.toNat = ⌈a⌉₊

Tactic:
rfl

Premises used: Nat.ceil, Int.toNat, rfl