awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Floor.Defs
Goal:
⊢ floor = Int.toNat

Tactic:
rfl

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

Tactic:
rfl

Premises used: Nat.ceil, Int.toNat, Int.ceil, rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
a : α
ha : 0 < a
⊢ GaloisConnection (fun (x : β) ↦ a • x) fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a

Tactic:
FloorDiv.floorDiv_gc ha

Premises used: FloorDiv.floorDiv_gc
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
a : α
b c : β
ha : 0 < a
⊢ c ≤ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ b a ↔ a • c ≤ b

Tactic:
(gc_floorDiv_smul ha _ _).symm

Premises used: gc_floorDiv_smul, Iff.symm
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
a : α
ha : a ≤ 0
b : β
⊢ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ b a = 0

Tactic:
FloorDiv.floorDiv_nonpos ha _

Premises used: FloorDiv.floorDiv_nonpos
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
b : β
⊢ @FloorDiv.floorDiv.{u_2, u_3} α _ inst inst_1 inst_2 inst_3 inst_4 _ b 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
a : α
⊢ Eq.{u_3 + 1} (α := β) (@FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ 0 a) 0

Tactic:
FloorDiv.zero_floorDiv _

Premises used: FloorDiv.zero_floorDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
a : α
b : β
ha : 0 < a
⊢ a • @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ b a ≤ b

Tactic:
(le_floorDiv_iff_smul_le ha).1 le_rfl

Premises used: le_rfl, Iff.mp, le_floorDiv_iff_smul_le
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
a : α
ha : 0 < a
⊢ GaloisConnection (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) fun (x : β) ↦ a • x

Tactic:
CeilDiv.ceilDiv_gc ha

Premises used: CeilDiv.ceilDiv_gc
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
a : α
b c : β
ha : 0 < a
⊢ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ b a ≤ c ↔ b ≤ a • c

Tactic:
gc_smul_ceilDiv ha _ _

Premises used: gc_smul_ceilDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
a : α
ha : a ≤ 0
b : β
⊢ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ b a = 0

Tactic:
CeilDiv.ceilDiv_nonpos ha _

Premises used: CeilDiv.ceilDiv_nonpos
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
b : β
⊢ @CeilDiv.ceilDiv.{u_2, u_3} α _ inst inst_1 inst_2 inst_3 inst_4 _ b 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
a : α
⊢ Eq.{u_3 + 1} (α := β) (@CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ 0 a) 0

Tactic:
CeilDiv.zero_ceilDiv _

Premises used: CeilDiv.zero_ceilDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
a : α
b : β
ha : 0 < a
⊢ b ≤ a • @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ b a

Tactic:
(ceilDiv_le_iff_le_smul ha).1 le_rfl

Premises used: ceilDiv_le_iff_le_smul, le_rfl, Iff.mp
-- Module: Mathlib.Algebra.Order.Floor.Div
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
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
⊢ @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

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Div
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 : β
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:
simp [ha]
-- Module: Mathlib.Algebra.Order.Floor.Div
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 : β
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:
le_of_smul_le_smul_left ((smul_floorDiv_le ha).trans <| le_smul_ceilDiv ha) ha

Premises used: le_of_smul_le_smul_left, smul_floorDiv_le, LE.le.trans, le_smul_ceilDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
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 : β
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:
exact le_of_smul_le_smul_left ((smul_floorDiv_le ha).trans <| le_smul_ceilDiv ha) ha

Premises used: le_of_smul_le_smul_left, smul_floorDiv_le, LE.le.trans, le_smul_ceilDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : MulActionWithZero α β
inst_5 : FloorDiv α β
inst_6 : IsOrderedRing α
inst_7 : Nontrivial α
b c : β
⊢ c ≤
      @FloorDiv.floorDiv.{u_2, u_3} α _ NonUnitalNonAssocSemiring.toAddCommMonoid inst_1 inst_2 inst_3
        (@SMulWithZero.toSMulZeroClass _ _ MulZeroClass.toZero _ _) _ b 1 ↔
    c ≤ b

Tactic:
simp [zero_lt_one' α]

Premises used: zero_lt_one'
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : MulActionWithZero α β
inst_5 : FloorDiv α β
a : α
inst_6 : PosSMulMono α β
inst_7 : PosSMulReflectLE α β
ha : 0 < a
b : β
⊢ ∀ (c : β),
    c ≤
        @FloorDiv.floorDiv _ _ NonUnitalNonAssocSemiring.toAddCommMonoid inst_1 inst_2 inst_3
          (@SMulWithZero.toSMulZeroClass _ _ MulZeroClass.toZero _ _) _ (a • b) a ↔
      c ≤ b

Tactic:
simp [smul_le_smul_iff_of_pos_left, ha]

Premises used: smul_le_smul_iff_of_pos_left
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : MulActionWithZero α β
inst_5 : CeilDiv α β
inst_6 : IsOrderedRing α
inst_7 : Nontrivial α
b c : β
⊢ @CeilDiv.ceilDiv.{u_2, u_3} α _ NonUnitalNonAssocSemiring.toAddCommMonoid inst_1 inst_2 inst_3
        (@SMulWithZero.toSMulZeroClass _ _ MulZeroClass.toZero _ _) _ b 1 ≤
      c ↔
    b ≤ c

Tactic:
simp [zero_lt_one' α]

Premises used: zero_lt_one'
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : MulActionWithZero α β
inst_5 : CeilDiv α β
a : α
inst_6 : PosSMulMono α β
inst_7 : PosSMulReflectLE α β
ha : 0 < a
b : β
⊢ ∀ (c : β),
    @CeilDiv.ceilDiv _ _ NonUnitalNonAssocSemiring.toAddCommMonoid inst_1 inst_2 inst_3
          (@SMulWithZero.toSMulZeroClass _ _ MulZeroClass.toZero _ _) _ (a • b) a ≤
        c ↔
      b ≤ c

Tactic:
simp [smul_le_smul_iff_of_pos_left, ha]

Premises used: smul_le_smul_iff_of_pos_left
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : FloorDiv α α
a : α
ha : 0 < a
⊢ GaloisConnection (fun (x : α) ↦ a * x) fun (x : α) ↦
    @FloorDiv.floorDiv _ _ NonUnitalNonAssocSemiring.toAddCommMonoid inst_1 NonUnitalNonAssocSemiring.toAddCommMonoid
      inst_1 DistribSMul.toSMulZeroClass _ x a

Tactic:
gc_floorDiv_smul ha

Premises used: gc_floorDiv_smul
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : FloorDiv α α
a b c : α
ha : 0 < a
⊢ c ≤
      @FloorDiv.floorDiv _ _ NonUnitalNonAssocSemiring.toAddCommMonoid inst_1 NonUnitalNonAssocSemiring.toAddCommMonoid
        inst_1 DistribSMul.toSMulZeroClass _ b a ↔
    a • c ≤ b

Tactic:
le_floorDiv_iff_smul_le ha

Premises used: le_floorDiv_iff_smul_le
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : CeilDiv α α
a : α
ha : 0 < a
⊢ GaloisConnection
    (fun (x : α) ↦
      @CeilDiv.ceilDiv _ _ NonUnitalNonAssocSemiring.toAddCommMonoid inst_1 NonUnitalNonAssocSemiring.toAddCommMonoid
        inst_1 DistribSMul.toSMulZeroClass _ x a)
    fun (x : α) ↦ a * x

Tactic:
gc_smul_ceilDiv ha

Premises used: gc_smul_ceilDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
α : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : CeilDiv α α
a b c : α
ha : 0 < a
⊢ @CeilDiv.ceilDiv _ _ NonUnitalNonAssocSemiring.toAddCommMonoid inst_1 NonUnitalNonAssocSemiring.toAddCommMonoid inst_1
        DistribSMul.toSMulZeroClass _ b a ≤
      c ↔
    b ≤ a * c

Tactic:
ceilDiv_le_iff_le_smul ha

Premises used: ceilDiv_le_iff_le_smul
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : 0 < a
⊢ GaloisConnection (fun (x : ℕ) ↦ a • x) fun (x : ℕ) ↦ x / a

Tactic:
simpa [mul_comm] using Nat.galoisConnection_mul_div ha

Premises used: Nat.galoisConnection_mul_div, mul_comm
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : a ≤ 0
b : ℕ
rw : b / 0 = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ b / a = 0

Tactic:
rw [ha.antisymm <| zero_le _, Nat.div_zero]

Premises used: Nat.zero_le, LE.le.antisymm, Nat.div_zero
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : 0 < a
b c : ℕ
⊢ (fun (x : ℕ) ↦ (x + a - 1) / a) b ≤ c ↔ b ≤ (fun (x : ℕ) ↦ a • x) c

Tactic:
simp [div_le_iff_le_mul_add_pred ha, add_assoc, tsub_add_cancel_of_le <| succ_le_iff.2 ha]

Premises used: Iff.mpr, add_assoc, tsub_add_cancel_of_le, Nat.div_le_iff_le_mul_add_pred, Nat.succ_le_iff
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : a ≤ 0
b : ℕ
simp_rw : (b + 0 - 1) / 0 = 0
⊢ (b + a - 1) / a = 0

Tactic:
simp_rw [ha.antisymm <| zero_le _, Nat.div_zero]

Premises used: Nat.zero_le, LE.le.antisymm, Nat.div_zero
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 0 - 1) / 0 = 0
succ : ∀ (n : ℕ), (0 + (n + 1) - 1) / (n + 1) = 0
⊢ (0 + a - 1) / a = 0

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
⊢ (HAdd.hAdd (α := ℕ) 0 0 - 1) / 0 = 0

Tactic:
simp [Nat.div_eq_zero_iff]

Premises used: Nat.div_eq_zero_iff
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
n : ℕ
⊢ (0 + (n + 1) - 1) / (n + 1) = 0

Tactic:
simp [Nat.div_eq_zero_iff]

Premises used: Nat.div_eq_zero_iff
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
a b : ℕ
⊢ @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder instAddCommMonoid instPartialOrder
      DistribSMul.toSMulZeroClass _ a b =
    a / b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
a b : ℕ
⊢ @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder instAddCommMonoid instPartialOrder DistribSMul.toSMulZeroClass
      _ a b =
    (a + b - 1) / b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → FloorDiv.{u_2, u_4} α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
h : ∀ (i : ι), @FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a = 0 i
⊢ Eq (α := (i : ι) → π i) (fun (i : ι) ↦ @FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a)
    0

Tactic:
ext i
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → FloorDiv.{u_2, u_4} α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
i : ι
⊢ @FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a = 0 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
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → FloorDiv.{u_2, u_4} α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
i : ι
⊢ @FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a = 0 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
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → FloorDiv.{u_2, u_4} α (π i)
a : α
h :
  ∀ (i : ι),
    Eq.{u_4 + 1} (α := π i) (@FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (0 i) a) (0 i)
⊢ Eq (α := (i : ι) → π i) (fun (i : ι) ↦ @FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (0 i) a)
    0

Tactic:
ext i
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → FloorDiv.{u_2, u_4} α (π i)
a : α
i : ι
⊢ Eq.{u_4 + 1} (α := π i) (@FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (0 i) a) (0 i)

Tactic:
zero_floorDiv a

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

Tactic:
exact zero_floorDiv a

Premises used: zero_floorDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → FloorDiv.{u_2, u_4} α (π i)
f : (i : ι) → π i
a : α
⊢ @FloorDiv.floorDiv _ _ inst inst_1 (addCommMonoid (f := π)) (partialOrder (π := π)) (smulZeroClass (f := π) α) _ f a =
    fun (i : ι) ↦ @FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → FloorDiv.{u_2, u_4} α (π i)
f : (i : ι) → π i
a : α
i : ι
⊢ @FloorDiv.floorDiv _ _ inst inst_1 (addCommMonoid (f := π)) (partialOrder (π := π)) (smulZeroClass (f := π) α) _ f a
      i =
    @FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → CeilDiv.{u_2, u_4} α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
h : ∀ (i : ι), @CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a = 0 i
⊢ Eq (α := (i : ι) → π i) (fun (i : ι) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a) 0

Tactic:
ext i
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → CeilDiv.{u_2, u_4} α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
i : ι
⊢ @CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a = 0 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
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → CeilDiv.{u_2, u_4} α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
i : ι
⊢ @CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a = 0 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
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → CeilDiv.{u_2, u_4} α (π i)
a : α
h :
  ∀ (x : ι), Eq.{u_4 + 1} (α := π x) (@CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 x) (inst_3 x) (inst_4 x) _ (0 x) a) (0 x)
⊢ Eq (α := (i : ι) → π i) (fun (i : ι) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (0 i) a) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → CeilDiv.{u_2, u_4} α (π i)
a : α
x : ι
⊢ Eq.{u_4 + 1} (α := π x) (@CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 x) (inst_3 x) (inst_4 x) _ (0 x) a) (0 x)

Tactic:
zero_ceilDiv _

Premises used: zero_ceilDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → CeilDiv.{u_2, u_4} α (π i)
a : α
x : ι
⊢ Eq.{u_4 + 1} (α := π x) (@CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 x) (inst_3 x) (inst_4 x) _ (0 x) a) (0 x)

Tactic:
exact zero_ceilDiv _

Premises used: zero_ceilDiv
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → CeilDiv.{u_2, u_4} α (π i)
f : (i : ι) → π i
a : α
⊢ @CeilDiv.ceilDiv _ _ inst inst_1 (addCommMonoid (f := π)) (partialOrder (π := π)) (smulZeroClass (f := π) α) _ f a =
    fun (i : ι) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Div
Goal:
ι : Type u_1
α : Type u_2
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → CeilDiv.{u_2, u_4} α (π i)
f : (i : ι) → π i
a : α
i : ι
⊢ @CeilDiv.ceilDiv _ _ inst inst_1 (addCommMonoid (f := π)) (partialOrder (π := π)) (smulZeroClass (f := π) α) _ f a i =
    @CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f 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_1 : ι →₀ β
a _a : α
ha : 0 < _a
f _g : ι →₀ β
i : ι
⊢ LE.le.{u_3} (α := β) (((fun (x : ι →₀ β) ↦ _a • x) f : (a : ι) → β) i : β) ((_g : (a : ι) → β) i : β) ↔
    LE.le.{u_3} (α := β) ((f : (a : ι) → β) i : β)
      (((fun (x : ι →₀ β) ↦
                (mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x _a) ⋯ x : ι →₀ β))
              _g :
            (a : ι) → β)
          i :
        β)

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

Premises used: Finsupp.mapRange_apply, Finsupp.coe_smul, gc_floorDiv_smul, 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 : FloorDiv α β
f_1 : ι →₀ β
a_1 a : α
ha : a ≤ 0
f : ι →₀ β
h :
  ∀ (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 : β)
⊢ Eq (α := ι →₀ β) (mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f) 0

Tactic:
ext i