awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f_1 : ι →₀ β
a_1 a : α
ha : a ≤ 0
f : ι →₀ β
i : ι
⊢ Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f : (a : ι) → β) i : β)
    ((0 : (a : ι) → β) i : β)

Tactic:
floorDiv_of_nonpos ha _

Premises used: floorDiv_of_nonpos
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f_1 : ι →₀ β
a_1 a : α
ha : a ≤ 0
f : ι →₀ β
i : ι
⊢ Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f : (a : ι) → β) i : β)
    ((0 : (a : ι) → β) i : β)

Tactic:
exact floorDiv_of_nonpos ha _

Premises used: floorDiv_of_nonpos
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f : ι →₀ β
a_1 a : α
h :
  ∀ (a_2 : ι),
    Eq.{u_3 + 1} (α := β)
      ((mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ 0 : (a : ι) → β) a_2 :
        β)
      ((0 : (a : ι) → β) a_2 : β)
⊢ Eq (α := ι →₀ β) (mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ 0) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f : ι →₀ β
a_1 a : α
a_2 : ι
⊢ Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ 0 : (a : ι) → β) a_2 : β)
    ((0 : (a : ι) → β) a_2 : β)

Tactic:
zero_floorDiv _

Premises used: zero_floorDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f : ι →₀ β
a_1 a : α
a_2 : ι
⊢ Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ 0 : (a : ι) → β) a_2 : β)
    ((0 : (a : ι) → β) a_2 : β)

Tactic:
exact zero_floorDiv _

Premises used: zero_floorDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f : ι →₀ β
a : α
⊢ @FloorDiv.floorDiv _ _ inst inst_1 instAddCommMonoid partialorder smulZeroClass _ f a =
    mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f : ι →₀ β
a : α
⊢ Eq (α := (a : ι) → β)
    (⇑(@FloorDiv.floorDiv _ _ inst inst_1 instAddCommMonoid partialorder smulZeroClass _ f a) : (a : ι) → β)
    fun (i : ι) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ ((f : (a : ι) → β) i) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f : ι →₀ β
a : α
i : ι
⊢ Eq.{u_3 + 1} (α := β)
    ((@FloorDiv.floorDiv _ _ inst inst_1 instAddCommMonoid partialorder smulZeroClass _ f a : (a : ι) → β) i : β)
    (@FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ ((f : (a : ι) → β) i) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f : ι →₀ β
a : α
⊢ (@FloorDiv.floorDiv _ _ inst inst_1 instAddCommMonoid partialorder smulZeroClass _ f a).support ⊆ f.support

Tactic:
simp +contextual [Finset.subset_iff, not_imp_not]

Premises used: Finset.subset_iff, not_imp_not
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f_1 : ι →₀ β
a _a : α
ha : 0 < _a
f _g : ι →₀ β
i : ι
⊢ LE.le.{u_3} (α := β)
      (((fun (x : ι →₀ β) ↦
                (mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x _a) ⋯ x : ι →₀ β))
              f :
            (a : ι) → β)
          i :
        β)
      ((_g : (a : ι) → β) i : β) ↔
    LE.le.{u_3} (α := β) ((f : (a : ι) → β) i : β) (((fun (x : ι →₀ β) ↦ _a • x) _g : (a : ι) → β) i : β)

Tactic:
simpa only [coe_smul, Pi.smul_apply, mapRange_apply] using gc_smul_ceilDiv ha (f i) _

Premises used: Finsupp.mapRange_apply, Finsupp.coe_smul, gc_smul_ceilDiv, DFunLike.coe, Pi.smul_apply
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f_1 : ι →₀ β
a_1 a : α
ha : a ≤ 0
f : ι →₀ β
h :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α := β)
      ((mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f : (a : ι) → β) i : β)
      ((0 : (a : ι) → β) i : β)
⊢ Eq (α := ι →₀ β) (mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f) 0

Tactic:
ext i
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f_1 : ι →₀ β
a_1 a : α
ha : a ≤ 0
f : ι →₀ β
i : ι
⊢ Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f : (a : ι) → β) i : β)
    ((0 : (a : ι) → β) i : β)

Tactic:
ceilDiv_of_nonpos ha _

Premises used: ceilDiv_of_nonpos
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f_1 : ι →₀ β
a_1 a : α
ha : a ≤ 0
f : ι →₀ β
i : ι
⊢ Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f : (a : ι) → β) i : β)
    ((0 : (a : ι) → β) i : β)

Tactic:
exact ceilDiv_of_nonpos ha _

Premises used: ceilDiv_of_nonpos
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f : ι →₀ β
a_1 a : α
h :
  ∀ (a_2 : ι),
    Eq.{u_3 + 1} (α := β)
      ((mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ 0 : (a : ι) → β) a_2 : β)
      ((0 : (a : ι) → β) a_2 : β)
⊢ Eq (α := ι →₀ β) (mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ 0) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f : ι →₀ β
a_1 a : α
a_2 : ι
⊢ Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ 0 : (a : ι) → β) a_2 : β)
    ((0 : (a : ι) → β) a_2 : β)

Tactic:
zero_ceilDiv _

Premises used: zero_ceilDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f : ι →₀ β
a_1 a : α
a_2 : ι
⊢ Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ 0 : (a : ι) → β) a_2 : β)
    ((0 : (a : ι) → β) a_2 : β)

Tactic:
exact zero_ceilDiv _

Premises used: zero_ceilDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f : ι →₀ β
a : α
⊢ @CeilDiv.ceilDiv _ _ inst inst_1 instAddCommMonoid partialorder smulZeroClass _ f a =
    mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f : ι →₀ β
a : α
⊢ Eq (α := (a : ι) → β)
    (⇑(@CeilDiv.ceilDiv _ _ inst inst_1 instAddCommMonoid partialorder smulZeroClass _ f a) : (a : ι) → β) fun (i : ι) ↦
    @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ ((f : (a : ι) → β) i) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f : ι →₀ β
a : α
i : ι
⊢ Eq.{u_3 + 1} (α := β)
    ((@CeilDiv.ceilDiv _ _ inst inst_1 instAddCommMonoid partialorder smulZeroClass _ f a : (a : ι) → β) i : β)
    (@CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ ((f : (a : ι) → β) i) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f : ι →₀ β
a : α
⊢ (@CeilDiv.ceilDiv _ _ inst inst_1 instAddCommMonoid partialorder smulZeroClass _ f a).support ⊆ f.support

Tactic:
simp +contextual [Finset.subset_iff, not_imp_not]

Premises used: Finset.subset_iff, not_imp_not
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌊∞⌋ₑ = ⊤

Tactic:
rfl

Premises used: ENat.floor, rfl
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌈∞⌉ₑ = ⊤

Tactic:
rfl

Premises used: ENat.ceil, rfl
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
⊢ ⌊(↑r : ℝ≥0∞)⌋ₑ = (↑⌊r⌋₊ : ℕ∞)

Tactic:
rfl

Premises used: ENat.floor, rfl
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
⊢ ⌈(↑r : ℝ≥0∞)⌉ₑ = (↑⌈r⌉₊ : ℕ∞)

Tactic:
rfl

Premises used: ENat.ceil, rfl
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
top : ⌊∞⌋ₑ = ⊤ ↔ Eq (α := ℝ≥0∞) ∞ ∞
coe : ∀ (x : ℝ≥0), ⌊(↑x : ℝ≥0∞)⌋ₑ = ⊤ ↔ (↑x : ℝ≥0∞) = ∞
⊢ ⌊r⌋ₑ = ⊤ ↔ r = ∞

Tactic:
cases r
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌊∞⌋ₑ = ⊤ ↔ Eq (α := ℝ≥0∞) ∞ ∞

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0
⊢ ⌊(↑x : ℝ≥0∞)⌋ₑ = ⊤ ↔ (↑x : ℝ≥0∞) = ∞

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
top : ⌈∞⌉ₑ = ⊤ ↔ Eq (α := ℝ≥0∞) ∞ ∞
coe : ∀ (x : ℝ≥0), ⌈(↑x : ℝ≥0∞)⌉ₑ = ⊤ ↔ (↑x : ℝ≥0∞) = ∞
⊢ ⌈r⌉ₑ = ⊤ ↔ r = ∞

Tactic:
cases r
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌈∞⌉ₑ = ⊤ ↔ Eq (α := ℝ≥0∞) ∞ ∞

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0
⊢ ⌈(↑x : ℝ≥0∞)⌉ₑ = ⊤ ↔ (↑x : ℝ≥0∞) = ∞

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
top : ⌊∞⌋ₑ < ⊤ ↔ LT.lt (α := ℝ≥0∞) ∞ ∞
coe : ∀ (x : ℝ≥0), ⌊(↑x : ℝ≥0∞)⌋ₑ < ⊤ ↔ (↑x : ℝ≥0∞) < ∞
⊢ ⌊r⌋ₑ < ⊤ ↔ r < ∞

Tactic:
cases r
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌊∞⌋ₑ < ⊤ ↔ LT.lt (α := ℝ≥0∞) ∞ ∞

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0
⊢ ⌊(↑x : ℝ≥0∞)⌋ₑ < ⊤ ↔ (↑x : ℝ≥0∞) < ∞

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
top : ⌈∞⌉ₑ < ⊤ ↔ LT.lt (α := ℝ≥0∞) ∞ ∞
coe : ∀ (x : ℝ≥0), ⌈(↑x : ℝ≥0∞)⌉ₑ < ⊤ ↔ (↑x : ℝ≥0∞) < ∞
⊢ ⌈r⌉ₑ < ⊤ ↔ r < ∞

Tactic:
cases r
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌈∞⌉ₑ < ⊤ ↔ LT.lt (α := ℝ≥0∞) ∞ ∞

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0
⊢ ⌈(↑x : ℝ≥0∞)⌉ₑ < ⊤ ↔ (↑x : ℝ≥0∞) < ∞

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
top : n ≤ ⌊∞⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ ∞
coe : ∀ (x : ℝ≥0), n ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
⊢ n ≤ ⌊r⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ r

Tactic:
cases r
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ∞
top : ⊤ ≤ ⌊∞⌋ₑ ↔ (↑⊤ : ℝ≥0∞) ≤ ∞
top₁ : ∀ (a : ℕ), (↑a : ℕ∞) ≤ ⌊∞⌋ₑ ↔ (↑(↑a : ℕ∞) : ℝ≥0∞) ≤ ∞
⊢ n ≤ ⌊∞⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ ∞

Tactic:
cases n
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ∞
x : ℝ≥0
coe : ⊤ ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑⊤ : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
coe₁ : ∀ (a : ℕ), (↑a : ℕ∞) ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑(↑a : ℕ∞) : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
⊢ n ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)

Tactic:
cases n
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⊤ ≤ ⌊∞⌋ₑ ↔ (↑⊤ : ℝ≥0∞) ≤ ∞

Tactic:
simp [Nat.le_floor_iff]

Premises used: Nat.le_floor_iff
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a : ℕ
⊢ (↑a : ℕ∞) ≤ ⌊∞⌋ₑ ↔ (↑(↑a : ℕ∞) : ℝ≥0∞) ≤ ∞

Tactic:
simp [Nat.le_floor_iff]

Premises used: Nat.le_floor_iff
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0
⊢ ⊤ ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑⊤ : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)

Tactic:
simp [Nat.le_floor_iff]

Premises used: Nat.le_floor_iff
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0
a : ℕ
⊢ (↑a : ℕ∞) ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑(↑a : ℕ∞) : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)

Tactic:
simp [Nat.le_floor_iff]

Premises used: Nat.le_floor_iff
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
top : ⌈∞⌉ₑ ≤ n ↔ ∞ ≤ (↑n : ℝ≥0∞)
coe : ∀ (x : ℝ≥0), ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ n ↔ (↑x : ℝ≥0∞) ≤ (↑n : ℝ≥0∞)
⊢ ⌈r⌉ₑ ≤ n ↔ r ≤ (↑n : ℝ≥0∞)

Tactic:
cases r
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ∞
top : ⌈∞⌉ₑ ≤ ⊤ ↔ ∞ ≤ (↑⊤ : ℝ≥0∞)
top₁ : ∀ (a : ℕ), ⌈∞⌉ₑ ≤ (↑a : ℕ∞) ↔ ∞ ≤ (↑(↑a : ℕ∞) : ℝ≥0∞)
⊢ ⌈∞⌉ₑ ≤ n ↔ ∞ ≤ (↑n : ℝ≥0∞)

Tactic:
cases n
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ∞
x : ℝ≥0
coe : ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ ⊤ ↔ (↑x : ℝ≥0∞) ≤ (↑⊤ : ℝ≥0∞)
coe₁ : ∀ (a : ℕ), ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ (↑a : ℕ∞) ↔ (↑x : ℝ≥0∞) ≤ (↑(↑a : ℕ∞) : ℝ≥0∞)
⊢ ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ n ↔ (↑x : ℝ≥0∞) ≤ (↑n : ℝ≥0∞)

Tactic:
cases n
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌈∞⌉ₑ ≤ ⊤ ↔ ∞ ≤ (↑⊤ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a : ℕ
⊢ ⌈∞⌉ₑ ≤ (↑a : ℕ∞) ↔ ∞ ≤ (↑(↑a : ℕ∞) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0
⊢ ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ ⊤ ↔ (↑x : ℝ≥0∞) ≤ (↑⊤ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0
a : ℕ
⊢ ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ (↑a : ℕ∞) ↔ (↑x : ℝ≥0∞) ≤ (↑(↑a : ℕ∞) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
⊢ ⌊r⌋ₑ < n ↔ r < (↑n : ℝ≥0∞)

Tactic:
lt_iff_lt_of_le_iff_le le_floor

Premises used: ENat.le_floor, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
⊢ n < ⌈r⌉ₑ ↔ (↑n : ℝ≥0∞) < r

Tactic:
lt_iff_lt_of_le_iff_le ceil_le

Premises used: ENat.ceil_le, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ GaloisConnection toENNReal floor

Tactic:
fun _ _ ↦ le_floor.symm

Premises used: ENat.le_floor, Iff.symm, GaloisConnection
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ GaloisConnection ceil toENNReal

Tactic:
fun _ _ ↦ ceil_le

Premises used: ENat.ceil_le, GaloisConnection
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
⊢ (↑⌊r⌋ₑ : ℝ≥0∞) ≤ r

Tactic:
le_floor.1 le_rfl

Premises used: le_rfl, ENat.le_floor, Iff.mp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
⊢ r ≤ (↑⌈r⌉ₑ : ℝ≥0∞)

Tactic:
ceil_le.1 le_rfl

Premises used: le_rfl, ENat.ceil_le, Iff.mp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
hn : n ≠ ⊤
⊢ ⌊r⌋ₑ ≤ n ↔ r < (↑n : ℝ≥0∞) + 1

Tactic:
simp [← lt_add_one_iff hn]

Premises used: ENat.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
hn₀ : n ≠ 0
hn : n ≠ ⊤
⊢ n ≠ ⊤

Tactic:
hn
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
hn₀ : n ≠ 0
hn : n ≠ ⊤
lift : ∀ (n : ℕ) (hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0), (↑n : ℕ∞) ≤ ⌈r⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < r
⊢ n ≤ ⌈r⌉ₑ ↔ (↑n : ℝ≥0∞) - 1 < r

Tactic:
lift n to ℕ using hn
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
top : (↑n : ℕ∞) ≤ ⌈∞⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < ∞
coe : ∀ (x : ℝ≥0), (↑n : ℕ∞) ≤ ⌈(↑x : ℝ≥0∞)⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < (↑x : ℝ≥0∞)
⊢ (↑n : ℕ∞) ≤ ⌈r⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < r

Tactic:
cases r
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
top : HSub.hSub (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 < ∞
⊢ (↑n : ℕ∞) ≤ ⌈∞⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < ∞

Tactic:
simp only [ceil_top, le_top, toENNReal_coe, true_iff]

Premises used: ENat.ceil_top, true_iff, le_top, ENat.toENNReal_coe
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
top : LT.lt (α := ℝ≥0∞) (↑(n - 1) : ℝ≥0∞) ∞
⊢ HSub.hSub (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 < ∞

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
⊢ LT.lt (α := ℝ≥0∞) (↑(n - 1) : ℝ≥0∞) ∞

Tactic:
ENNReal.coe_lt_top

Premises used: ENNReal.ofNNReal, WithTop.some, ENNReal.coe_lt_top
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
⊢ LT.lt (α := ℝ≥0∞) (↑(n - 1) : ℝ≥0∞) ∞

Tactic:
exact ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
x : ℝ≥0
coe : ∀ (hn₀ : ¬n = 0), n ≤ ⌈x⌉₊ ↔ HSub.hSub (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 < (↑x : ℝ≥0∞)
⊢ (↑n : ℕ∞) ≤ ⌈(↑x : ℝ≥0∞)⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < (↑x : ℝ≥0∞)

Tactic:
simp only [ne_eq, Nat.cast_eq_zero, ceil_coe, Nat.cast_le, toENNReal_coe] at hn₀ ⊢

Premises used: ne_eq, Nat.cast_eq_zero, ENat.toENNReal_coe, Nat.cast_le, ENat.ceil_coe
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
x : ℝ≥0
hn₀ : ¬n = 0
coe : n ≤ ⌈x⌉₊ ↔ (↑(n - 1) : ℝ≥0) < x
⊢ n ≤ ⌈x⌉₊ ↔ HSub.hSub (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 < (↑x : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
x : ℝ≥0
hn₀ : ¬n = 0
coe : 1 ≤ n
⊢ n ≤ ⌈x⌉₊ ↔ (↑(n - 1) : ℝ≥0) < x

Tactic:
rw [← Nat.add_one_le_ceil_iff, Nat.sub_add_cancel]

Premises used: Nat.sub_add_cancel, Nat.add_one_le_ceil_iff
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
x : ℝ≥0
hn₀ : ¬n = 0
⊢ 1 ≤ n

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
hn : n ≠ ⊤
⊢ n < ⌊r⌋ₑ ↔ (↑n : ℝ≥0∞) + 1 ≤ r

Tactic:
simp [← add_one_le_iff hn]

Premises used: ENat.add_one_le_iff
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
hn₀ : n ≠ 0
hn : n ≠ ⊤
⊢ ⌈r⌉ₑ < n ↔ r ≤ (↑n : ℝ≥0∞) - 1

Tactic:
simpa using (le_ceil hn₀ hn).not

Premises used: Iff.not, ENat.le_ceil
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r s : ℝ≥0∞
hrs : r ≤ s
⊢ ⌊r⌋ₑ ≤ ⌊s⌋ₑ

Tactic:
simpa using hrs.trans' floor_le_self

Premises used: ENat.floor_le_self, LE.le.trans'
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r s : ℝ≥0∞
hrs : r ≤ s
⊢ ⌈r⌉ₑ ≤ ⌈s⌉ₑ

Tactic:
simpa using hrs.trans le_ceil_self

Premises used: ENat.le_ceil_self, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r s : ℝ≥0∞
hrs : r ≤ s
⊢ ⌊r⌋ₑ ≤ ⌊s⌋ₑ

Tactic:
floor_mono hrs

Premises used: ENat.floor_mono
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r s : ℝ≥0∞
hrs : r ≤ s
⊢ ⌈r⌉ₑ ≤ ⌈s⌉ₑ

Tactic:
ceil_mono hrs

Premises used: ENat.ceil_mono
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n r : ℕ∞
⊢ r ≤ ⌊(↑n : ℝ≥0∞)⌋ₑ ↔ r ≤ n

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n r : ℕ∞
⊢ ⌈(↑n : ℝ≥0∞)⌉ₑ ≤ r ↔ n ≤ r

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌊0⌋ₑ = 0

Tactic:
simpa using floor_natCast 0

Premises used: OfNat.ofNat, ENat.floor_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌈0⌉ₑ = 0

Tactic:
simpa using ceil_natCast 0

Premises used: ENat.ceil_natCast, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌊1⌋ₑ = 1

Tactic:
simpa using floor_natCast 1

Premises used: OfNat.ofNat, ENat.floor_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌈1⌉ₑ = 1

Tactic:
simpa using ceil_natCast 1

Premises used: ENat.ceil_natCast, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ ⌊OfNat.ofNat n⌋ₑ = OfNat.ofNat n

Tactic:
ENat.floor_natCast n

Premises used: WithTop.map, ENat.toENNReal, Nat.cast, WithTop.some, ENat.map, ENat.floor_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ ⌈OfNat.ofNat n⌉ₑ = OfNat.ofNat n

Tactic:
ENat.ceil_natCast n

Premises used: WithTop.map, ENat.toENNReal, Nat.cast, WithTop.some, ENat.map, ENat.ceil_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
⊢ 0 < ⌊r⌋ₑ ↔ 1 ≤ r

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
⊢ 0 < ⌈r⌉ₑ ↔ 0 < r

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
⊢ ⌊r⌋ₑ = 0 ↔ r < 1

Tactic:
simp [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
⊢ ⌈r⌉ₑ = 0 ↔ r = 0

Tactic:
simpa using ceil_le (n := 0)

Premises used: ENat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
⊢ ⌈(↑r : ℝ≥0∞)⌉ₑ ≤ ⌊(↑r : ℝ≥0∞)⌋ₑ + 1

Tactic:
simpa using mod_cast Nat.ceil_le_floor_add_one r

Premises used: Nat.ceil_le_floor_add_one
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r s : ℝ≥0∞
hrs : r < s
⊢ ⌊r⌋ₑ < ⌈s⌉ₑ

Tactic:
floor_lt.2 <| hrs.trans_le le_ceil_self

Premises used: Iff.mpr, ENat.le_ceil_self, LT.lt.trans_le, ENat.floor_lt
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r s : ℝ≥0∞
h : ∀ (n : ℕ∞), (↑n : ℝ≥0∞) ≤ r ↔ (↑n : ℝ≥0∞) ≤ s
⊢ ∀ (c : ℕ∞), c ≤ ⌊r⌋ₑ ↔ c ≤ ⌊s⌋ₑ

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r s : ℝ≥0∞
h : ∀ (n : ℕ∞), r ≤ (↑n : ℝ≥0∞) ↔ s ≤ (↑n : ℝ≥0∞)
⊢ ∀ (c : ℕ∞), ⌈r⌉ₑ ≤ c ↔ ⌈s⌉ₑ ≤ c

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℕ∞
⊢ ⌊∞ + (↑x : ℝ≥0∞)⌋ₑ = ⌊∞⌋ₑ + x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0∞
⊢ ⌊x + (↑⊤ : ℝ≥0∞)⌋ₑ = ⌊x⌋ₑ + ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
norm_cast : ⌊r + (↑n : ℝ≥0)⌋₊ = ⌊r⌋₊ + n
⊢ ⌊(↑(r + (↑n : ℝ≥0)) : ℝ≥0∞)⌋ₑ = (↑(⌊r⌋₊ + n) : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌊r + (↑n : ℝ≥0)⌋₊ = ⌊r⌋₊ + n

Tactic:
n.floor_add_natCast zero_le

Premises used: zero_le, Nat.floor_add_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌊r + (↑n : ℝ≥0)⌋₊ = ⌊r⌋₊ + n

Tactic:
exact n.floor_add_natCast zero_le

Premises used: zero_le, Nat.floor_add_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℕ∞
⊢ ⌈∞ + (↑x : ℝ≥0∞)⌉ₑ = ⌈∞⌉ₑ + x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0∞
⊢ ⌈x + (↑⊤ : ℝ≥0∞)⌉ₑ = ⌈x⌉ₑ + ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
norm_cast : ⌈r + (↑n : ℝ≥0)⌉₊ = ⌈r⌉₊ + n
⊢ ⌈(↑(r + (↑n : ℝ≥0)) : ℝ≥0∞)⌉ₑ = (↑(⌈r⌉₊ + n) : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌈r + (↑n : ℝ≥0)⌉₊ = ⌈r⌉₊ + n

Tactic:
Nat.ceil_add_natCast zero_le _

Premises used: zero_le, Nat.ceil_add_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌈r + (↑n : ℝ≥0)⌉₊ = ⌈r⌉₊ + n

Tactic:
exact Nat.ceil_add_natCast zero_le _

Premises used: zero_le, Nat.ceil_add_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
⊢ ⌊(↑n : ℝ≥0∞) + r⌋ₑ = n + ⌊r⌋ₑ

Tactic:
simp [add_comm, floor_add_toENNReal]

Premises used: add_comm, ENat.floor_add_toENNReal