awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : Nonempty ι
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
have intro : ∀ (ε : (i : ι) → α) (hε : ∀ (i : ι), 0 < ε i) (hxε : ∀ (i : ι), x i + ε i = y i),
  ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Tactic: choose ε hε hxε using fun i => exists_pos_add_of_lt' (h i)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : Nonempty ι
ε : (i : ι) → α
hε : ∀ (i : ι), 0 < ε i
hxε : ∀ (i : ι), x i + ε i = y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
have intro : ∀ (h : ∀ (i : ι), x i < (x + ε) i) (hxε : ∀ (i : ι), x i + ε i = (x + ε) i),
  ∃ (ε_1 : α), 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
Tactic: obtain rfl : x + ε = y := funext hxε
Cleared hypotheses: y, h, hxε
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x : ι → α
val : Fintype ι
h_1 : Nonempty ι
ε : (i : ι) → α
hε : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
⊢ ∃ (ε_1 : α), 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
have hε₁ : 0 < Finset.inf' Finset.univ sorry ε
Tactic: have hε : 0 < Finset.univ.inf' Finset.univ_nonempty ε := (Finset.lt_inf'_iff _).2 fun i _ => hε _
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x : ι → α
val : Fintype ι
h_1 : Nonempty ι
ε : (i : ι) → α
hε_1 : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
hε : 0 < Finset.inf' Finset.univ ⋯ ε
⊢ ∃ (ε_1 : α), 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
have intro : ∀ (δ : α) (hδ : 0 < δ) (hδε : δ < Finset.inf' Finset.univ sorry ε), ∃ (ε_1 : α), 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
Tactic: obtain ⟨δ, hδ, hδε⟩ := exists_between hε
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℤ
hn : Even n
a : α
⊢ 0 ≤ a ^ n
have obtain : ∀ (k : ℤ), 0 ≤ a ^ (k + k)
Tactic: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ (k + k)
have rw : 0 ≤ a ^ k * a ^ k
Tactic: rw [zpow_add' (by simp [em'])]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Even n
h : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0
have obtain : ∀ (k : ℤ) (h : k + k ≠ 0), 0 < a ^ (k + k) ↔ a ≠ 0
Tactic: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, hn, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
have rw : 0 < a ^ k * a ^ k ↔ a ≠ 0
Tactic: rw [zpow_add' (by simp [em']), mul_self_pos, zpow_ne_zero_iff (by simpa using h)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
rw : 0 < a ^ k * a ^ k ↔ a ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
have rw₁ : a ^ k ≠ 0 ↔ a ≠ 0
Tactic: rw [zpow_add' (by simp [em']), mul_self_pos, zpow_ne_zero_iff (by simpa using h)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
rw : 0 < a ^ k * a ^ k ↔ a ≠ 0
rw₁ : a ^ k ≠ 0 ↔ a ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
have rw₂ : a ≠ 0 ↔ a ≠ 0
Tactic: rw [zpow_add' (by simp [em']), mul_self_pos, zpow_ne_zero_iff (by simpa using h)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0
have refine : ∀ (ha : a < 0), a ^ n < 0
Tactic: refine ⟨lt_imp_lt_of_le_imp_le (zpow_nonneg · _), fun ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
ha : a < 0
⊢ a ^ n < 0
have obtain : ∀ (k : ℤ), a ^ (2 * k + 1) < 0
Tactic: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k + 1) < 0
have rw : a ^ (2 * k) * a < 0
Tactic: rw [zpow_add_one₀ ha.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0
have rw : n ≠ 0
Tactic: rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.zpow_neg_iff, zpow_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
p : ℤ
hp : Even p
a : α
⊢ |a| ^ p = a ^ p
have inl : ∀ (h : |a| = a), |a| ^ p = a ^ p
Tactic: rcases abs_choice a with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
p : ℤ
hp : Even p
a : α
inl : ∀ (h : |a| = a), |a| ^ p = a ^ p
⊢ |a| ^ p = a ^ p
have inr : ∀ (h : |a| = -a), |a| ^ p = a ^ p
Tactic: rcases abs_choice a with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : ofNat m ≠ 0
⊢ a ^ ofNat m = b ^ ofNat m ↔ a = b ∨ a = -b ∧ Even (ofNat m)
have simp : ∀ (hn : ¬m = 0), a ^ m = b ^ m ↔ a = b ∨ a = -b ∧ Even m
Tactic: simp only [Int.ofNat_eq_natCast, ne_eq, Nat.cast_eq_zero, zpow_natCast, Int.even_coe_nat] at *
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : -[m+1] ≠ 0
⊢ a ^ -[m+1] = b ^ -[m+1] ↔ a = b ∨ a = -b ∧ Even -[m+1]
have simp : ∀ (hn : ¬m.succ = 0), a ^ m.succ = b ^ m.succ ↔ a = b ∨ a = -b ∧ Even m.succ
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 *
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
have inl : HPow.hPow (β := ℤ) a 0 = HPow.hPow (β := ℤ) b 0 ↔ Eq (α := ℤ) 0 0 ∨ a = b ∨ a = -b ∧ Even (α := ℤ) 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
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
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
have inr : ∀ (hn : n ≠ 0), a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Power (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
n : ℤ
hb : b ≠ 0
m : ℕ
⊢ a ^ -[m+1] = -b ^ -[m+1] ↔ a = -b ∧ Odd -[m+1]
have simp : a = -b ∧ Odd m.succ ↔ a = -b ∧ Odd (α := ℤ) (-(↑m.succ : ℤ))
Tactic: simp only [← neg_ofNat_succ, zpow_neg, ← inv_neg, pow_eq_neg_pow_iff hb, inv_inj,
      zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
a n : ℕ
h : 0 ≤ a
⊢ n ≤ id a ↔ (↑n : ℕ) ≤ a
have rw : n ≤ id a ↔ n ≤ a
Tactic: rw [Nat.cast_id, id_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
a n : ℕ
h : 0 ≤ a
rw : n ≤ id a ↔ n ≤ a
⊢ n ≤ id a ↔ (↑n : ℕ) ≤ a
have rw₁ : n ≤ a ↔ n ≤ a
Tactic: rw [Nat.cast_id, id_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
n a : ℕ
⊢ id n ≤ a ↔ n ≤ (↑a : ℕ)
have rw : id n ≤ a ↔ n ≤ a
Tactic: rw [Nat.cast_id, id_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
n a : ℕ
rw : id n ≤ a ↔ n ≤ a
⊢ id n ≤ a ↔ n ≤ (↑a : ℕ)
have rw₁ : n ≤ a ↔ n ≤ a
Tactic: rw [Nat.cast_id, id_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : FloorSemiring α
a : α
⊢ 0 < ⌈a⌉₊ ↔ 0 < a
have rw : (↑0 : α) < a ↔ 0 < a
Tactic: rw [lt_ceil, cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : FloorSemiring α
a : α
rw : (↑0 : α) < a ↔ 0 < a
⊢ 0 < ⌈a⌉₊ ↔ 0 < a
have rw₁ : 0 < a ↔ 0 < a
Tactic: rw [lt_ceil, cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
⊢ (↑a : ℤ) ≤ b ↔ a ≤ id b
have rw : a ≤ b ↔ a ≤ id b
Tactic: rw [Int.cast_id, id_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
rw : a ≤ b ↔ a ≤ id b
⊢ (↑a : ℤ) ≤ b ↔ a ≤ id b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [Int.cast_id, id_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
⊢ id a ≤ b ↔ a ≤ (↑b : ℤ)
have rw : id a ≤ b ↔ a ≤ b
Tactic: rw [Int.cast_id, id_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
rw : id a ≤ b ↔ a ≤ b
⊢ id a ≤ b ↔ a ≤ (↑b : ℤ)
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [Int.cast_id, id_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : ℤ
⊢ (fun (a : α) ↦ -floor (-a)) a ≤ z ↔ a ≤ (↑z : α)
have rw : -z ≤ floor (-a) ↔ a ≤ (↑z : α)
Tactic: rw [neg_le, ← gc_coe_floor, Int.cast_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : α)
⊢ (fun (a : α) ↦ -floor (-a)) a ≤ z ↔ a ≤ (↑z : α)
have rw₁ : (↑(-z) : α) ≤ -a ↔ a ≤ (↑z : α)
Tactic: rw [neg_le, ← gc_coe_floor, Int.cast_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : α)
⊢ (fun (a : α) ↦ -floor (-a)) a ≤ z ↔ a ≤ (↑z : α)
have rw₂ : -(↑z : α) ≤ -a ↔ a ≤ (↑z : α)
Tactic: rw [neg_le, ← gc_coe_floor, Int.cast_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : α)
⊢ (fun (a : α) ↦ -floor (-a)) a ≤ z ↔ a ≤ (↑z : α)
have rw₃ : a ≤ (↑z : α) ↔ a ≤ (↑z : α)
Tactic: rw [neg_le, ← gc_coe_floor, Int.cast_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : α
⊢ (↑a : α) ≤ z ↔ a ≤ (fun (a : α) ↦ -ceil (-a)) z
have rw : (↑a : α) ≤ z ↔ ceil (-z) ≤ -a
Tactic: rw [le_neg, gc_ceil_coe, Int.cast_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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
⊢ (↑a : α) ≤ z ↔ a ≤ (fun (a : α) ↦ -ceil (-a)) z
have rw₁ : (↑a : α) ≤ z ↔ -z ≤ (↑(-a) : α)
Tactic: rw [le_neg, gc_ceil_coe, Int.cast_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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) : α)
⊢ (↑a : α) ≤ z ↔ a ≤ (fun (a : α) ↦ -ceil (-a)) z
have rw₂ : (↑a : α) ≤ z ↔ -z ≤ -(↑a : α)
Tactic: rw [le_neg, gc_ceil_coe, Int.cast_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : α)
⊢ (↑a : α) ≤ z ↔ a ≤ (fun (a : α) ↦ -ceil (-a)) z
have rw₃ : (↑a : α) ≤ z ↔ (↑a : α) ≤ z
Tactic: rw [le_neg, gc_ceil_coe, Int.cast_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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
⊢ { n : ℤ // (↑n : α) ≤ x ∧ ∀ (m : ℤ), (↑m : α) ≤ x → m ≤ n }
have refine : ∀ (m : ℤ) (hm : (fun (x_1 : ℤ) ↦ (↑x_1 : α) ≤ x) m), m ≤ (↑n : ℤ)
Tactic: refine Int.greatestOfBdd (P := (· ≤ x)) n.1 (fun m hm ↦ ?_) below
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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
⊢ m ≤ (↑n : ℤ)
have rw : LE.le.{u_4} (α := α) (↑m : α) (↑(↑n : ℤ) : α)
Tactic: rw [← Int.cast_le (R := α)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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
have refine : ∀ (n : ℤ), n ≤ (↑(floorAux below above) : ℤ) → (↑n : α) ≤ x
Tactic: refine ⟨_, fun n ↦ ⟨?_, (floorAux below above).2.2 _⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
α : Type u_4
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
x : α
below : ∃ (n : ℤ), (↑n : α) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : α)
n : ℤ
⊢ n ≤ (↑(floorAux below above) : ℤ) → (↑n : α) ≤ x
have rw : LE.le.{u_4} (α := α) (↑n : α) (↑(↑(floorAux below above) : ℤ) : α) → (↑n : α) ≤ x
Tactic: rw [← Int.cast_le (R := α)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : ℤ), (↑n : α) ≤ x
have obtain : ∀ (n : ℕ) (hn : -x ≤ (↑n : α)), ∃ (n : ℤ), (↑n : α) ≤ x
Tactic: obtain ⟨n, hn⟩ := bounded (-x)
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : ℤ), (↑n : α) ≤ x
have h : (↑(-(↑n : ℤ)) : α) ≤ x
Tactic: use -n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : ℤ), x ≤ (↑n : α)
have obtain : ∀ (n : ℕ) (hn : x ≤ (↑n : α)), ∃ (n : ℤ), x ≤ (↑n : α)
Tactic: obtain ⟨n, hn⟩ := bounded x
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : α)
⊢ ∃ (n : ℤ), x ≤ (↑n : α)
have h : x ≤ (↑(↑n : ℤ) : α)
Tactic: use n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
⊢ 0 ≤ ⌊a⌋ ↔ 0 ≤ a
have rw : (↑0 : α) ≤ a ↔ 0 ≤ a
Tactic: rw [le_floor, Int.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
rw : (↑0 : α) ≤ a ↔ 0 ≤ a
⊢ 0 ≤ ⌊a⌋ ↔ 0 ≤ a
have rw₁ : 0 ≤ a ↔ 0 ≤ a
Tactic: rw [le_floor, Int.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
inst_3 : IsOrderedRing α
ha : a ≤ 0
⊢ ⌊a⌋ ≤ 0
have rw : LE.le.{u_2} (α := α) (↑⌊a⌋ : α) 0
Tactic: rw [← @cast_le α, Int.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
⊢ 0 < ⌈a⌉ ↔ 0 < a
have rw : (↑0 : α) < a ↔ 0 < a
Tactic: rw [lt_ceil, cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
rw : (↑0 : α) < a ↔ 0 < a
⊢ 0 < ⌈a⌉ ↔ 0 < a
have rw₁ : 0 < a ↔ 0 < a
Tactic: rw [lt_ceil, cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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
⊢ n ≤ ⌊a⌋.toNat ↔ (↑n : α) ≤ a
have rw : (↑n : ℤ) ≤ ⌊a⌋ ↔ (↑n : α) ≤ a
Tactic: rw [Int.le_toNat (Int.floor_nonneg.2 ha), Int.le_floor, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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
⊢ n ≤ ⌊a⌋.toNat ↔ (↑n : α) ≤ a
have rw₁ : (↑(↑n : ℤ) : α) ≤ a ↔ (↑n : α) ≤ a
Tactic: rw [Int.le_toNat (Int.floor_nonneg.2 ha), Int.le_floor, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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
⊢ n ≤ ⌊a⌋.toNat ↔ (↑n : α) ≤ a
have rw₂ : (↑n : α) ≤ a ↔ (↑n : α) ≤ a
Tactic: rw [Int.le_toNat (Int.floor_nonneg.2 ha), Int.le_floor, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
inst_3 : FloorRing α
a : α
n : ℕ
⊢ (fun (a : α) ↦ ⌈a⌉.toNat) a ≤ n ↔ a ≤ (↑n : α)
have rw : ⌈a⌉ ≤ (↑n : ℤ) ↔ a ≤ (↑n : α)
Tactic: rw [Int.toNat_le, Int.ceil_le, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : α)
⊢ (fun (a : α) ↦ ⌈a⌉.toNat) a ≤ n ↔ a ≤ (↑n : α)
have rw₁ : a ≤ (↑(↑n : ℤ) : α) ↔ a ≤ (↑n : α)
Tactic: rw [Int.toNat_le, Int.ceil_le, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Defs (goal)
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 : α)
⊢ (fun (a : α) ↦ ⌈a⌉.toNat) a ≤ n ↔ a ≤ (↑n : α)
have rw₂ : a ≤ (↑n : α) ↔ a ≤ (↑n : α)
Tactic: rw [Int.toNat_le, Int.ceil_le, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : PosSMulReflectLE α β
inst_6 : FloorDiv α β
inst_7 : CeilDiv α β
a : α
b : β
⊢ @FloorDiv.floorDiv _ _ inst SemilatticeInf.toPartialOrder inst_2 inst_3 inst_4 _ b a ≤
    @CeilDiv.ceilDiv _ _ inst SemilatticeInf.toPartialOrder inst_2 inst_3 inst_4 _ b a
have inl : ∀ (ha : a ≤ 0),
  @FloorDiv.floorDiv _ _ inst SemilatticeInf.toPartialOrder inst_2 inst_3 inst_4 _ b a ≤
    @CeilDiv.ceilDiv _ _ inst SemilatticeInf.toPartialOrder inst_2 inst_3 inst_4 _ b a
Tactic: obtain ha | ha := le_or_gt a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : PosSMulReflectLE α β
inst_6 : FloorDiv α β
inst_7 : CeilDiv α β
a : α
b : β
inl :
  ∀ (ha : a ≤ 0),
    @FloorDiv.floorDiv _ _ inst SemilatticeInf.toPartialOrder inst_2 inst_3 inst_4 _ b a ≤
      @CeilDiv.ceilDiv _ _ inst SemilatticeInf.toPartialOrder inst_2 inst_3 inst_4 _ b a
⊢ @FloorDiv.floorDiv _ _ inst SemilatticeInf.toPartialOrder inst_2 inst_3 inst_4 _ b a ≤
    @CeilDiv.ceilDiv _ _ inst SemilatticeInf.toPartialOrder inst_2 inst_3 inst_4 _ b a
have inr : ∀ (ha : 0 < a),
  @FloorDiv.floorDiv _ _ inst SemilatticeInf.toPartialOrder inst_2 inst_3 inst_4 _ b a ≤
    @CeilDiv.ceilDiv _ _ inst SemilatticeInf.toPartialOrder inst_2 inst_3 inst_4 _ b a
Tactic: obtain ha | ha := le_or_gt a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : a ≤ 0
b : ℕ
⊢ b / a = 0
have rw : b / 0 = 0
Tactic: rw [ha.antisymm <| zero_le _, Nat.div_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : a ≤ 0
b : ℕ
rw : b / 0 = 0
⊢ b / a = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [ha.antisymm <| zero_le _, Nat.div_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : a ≤ 0
b : ℕ
⊢ (b + a - 1) / a = 0
have simp_rw : (b + 0 - 1) / 0 = 0
Tactic: simp_rw [ha.antisymm <| zero_le _, Nat.div_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
⊢ (0 + a - 1) / a = 0
have zero : (HAdd.hAdd (α := ℕ) 0 0 - 1) / 0 = 0
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 0 - 1) / 0 = 0
⊢ (0 + a - 1) / a = 0
have succ : ∀ (n : ℕ), (0 + (n + 1) - 1) / (n + 1) = 0
Tactic: cases a
Cleared hypotheses: a