awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : 0 ≤ x
hy : 0 ≤ y
⊢ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) x hx / Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) y hy =
    Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) (x / y) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : { x : α // 0 ≤ x }
n : ℤ
⊢ (↑(a ^ n) : α) = (↑a : α) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
hx : 0 ≤ x
n : ℤ
⊢ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) x hx ^ n = Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) (x ^ n) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : { x : α // 0 ≤ x }
rw : 0 ≤ (↑q : α) * (↑a : α)
⊢ 0 ≤ q • (↑a : α)

Tactic:
rw [NNRat.smul_def]

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : { x : α // 0 ≤ x }
⊢ 0 ≤ (↑q : α) * (↑a : α)

Tactic:
mul_nonneg q.cast_nonneg a.2

Premises used: mul_nonneg, NNRat.cast_nonneg, Subtype.property
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : { x : α // 0 ≤ x }
⊢ 0 ≤ (↑q : α) * (↑a : α)

Tactic:
exact mul_nonneg q.cast_nonneg a.2

Premises used: mul_nonneg, NNRat.cast_nonneg, Subtype.property
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := α) (↑(↑q : { x : α // 0 ≤ x }) : α) (↑q : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := { x : α // 0 ≤ x }) (Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) (↑q : α) ⋯) (↑q : { x : α // 0 ≤ x })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
a : { x : α // 0 ≤ x }
⊢ (↑(q • a) : α) = q • (↑a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
rw : 0 ≤ (↑q : α) * a
⊢ 0 ≤ q • a

Tactic:
rw [NNRat.smul_def]

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ (↑q : α) * a

Tactic:
mul_nonneg q.cast_nonneg ha

Premises used: mul_nonneg, NNRat.cast_nonneg
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ (↑q : α) * a

Tactic:
exact mul_nonneg q.cast_nonneg ha

Premises used: mul_nonneg, NNRat.cast_nonneg
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ (↑(Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) (q • a) ⋯) : α) = q • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Floor
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : FloorSemiring α
a : { r : α // 0 ≤ r }
⊢ ⌊(↑a : α)⌋₊ = ⌊a⌋₊

Tactic:
rfl

Premises used: Nat.floor, rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Floor
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : FloorSemiring α
a : { r : α // 0 ≤ r }
⊢ ⌈(↑a : α)⌉₊ = ⌈a⌉₊

Tactic:
rfl

Premises used: Nat.ceil, rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Lattice
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := { x : α // a ≤ x }) ⊥ (Subtype.mk (p := fun (x : α) ↦ a ≤ x) a ⋯)

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Lattice
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : NoMaxOrder α
a : α
⊢ NoMaxOrder.{u_1} { x : α // a ≤ x }

Tactic:
inferInstanceAs <| NoMaxOrder (Ici a)

Premises used: _private.0.Nonneg.noMaxOrder._proof_1
-- Module: Mathlib.Algebra.Order.Nonneg.Lattice
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
a : α
⊢ DenselyOrdered.{u_1} { x : α // a ≤ x }

Tactic:
inferInstanceAs <| DenselyOrdered (Ici a)

Premises used: _private.0.Nonneg.instDenselyOrdered._proof_1
-- Module: Mathlib.Algebra.Order.Nonneg.Lattice
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
a : α
⊢ Eq.{u_1 + 1} (α := { x : α // a ≤ x })
    ((fun (t : Set (↑(Ici a) : Type u_1)) ↦
        (if ht : t.Nonempty ∧ BddAbove t ∧ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a) '' t) ∈ Ici a then
            Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a) '' t)) ⋯
          else default :
          (↑(Ici a) : Type u_1)))
      ∅)
    ⊥

Tactic:
simp [bot_eq]

Premises used: Nonneg.bot_eq
-- Module: Mathlib.Algebra.Order.Nonneg.Module
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : SMul R S
a : R≥0
x : S
⊢ (↑a : R) • x = a • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Module
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : SMul R S
a : R
ha : 0 ≤ a
x : S
⊢ Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) a ha • x = a • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Module
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : SMul R S
inst_4 : SMul R M
inst_5 : SMul S M
inst_6 : IsScalarTower R S M
⊢ IsScalarTower.{u_1, u_2, u_3} R≥0 S M

Tactic:
SMul.comp.isScalarTower ↑Nonneg.coeRingHom

Premises used: SMul.comp.isScalarTower, SMul.comp.smul, Nonneg.coeRingHom, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
⊢ IsOrderedAddMonoid.{u_1} { x : α // 0 ≤ x }

Tactic:
Function.Injective.isOrderedAddMonoid Subtype.val Nonneg.coe_add .rfl

Premises used: Iff.rfl, Nonneg.coe_add, Subtype.val, Function.Injective.isOrderedAddMonoid
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
⊢ IsOrderedCancelAddMonoid.{u_1} { x : α // 0 ≤ x }

Tactic:
Function.Injective.isOrderedCancelAddMonoid _ Nonneg.coe_add .rfl

Premises used: Iff.rfl, Nonneg.coe_add, Function.Injective.isOrderedCancelAddMonoid
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
⊢ IsOrderedRing.{u_1} { x : α // 0 ≤ x }

Tactic:
Function.Injective.isOrderedRing Subtype.val Nonneg.coe_zero Nonneg.coe_one Nonneg.coe_add
    Nonneg.coe_mul .rfl

Premises used: Iff.rfl, Nonneg.coe_add, Nonneg.coe_zero, Nonneg.coe_mul, Function.Injective.isOrderedRing, Subtype.val, Nonneg.coe_one
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
⊢ IsStrictOrderedRing.{u_1} { x : α // 0 ≤ x }

Tactic:
Function.Injective.isStrictOrderedRing Subtype.val Nonneg.coe_zero Nonneg.coe_one Nonneg.coe_add
    Nonneg.coe_mul .rfl .rfl

Premises used: Iff.rfl, Nonneg.coe_add, Nonneg.coe_zero, Nonneg.coe_mul, Function.Injective.isStrictOrderedRing, Subtype.val, Nonneg.coe_one
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
h : a ≤ b
⊢ (↑a : α) ≤ (↑b : α)

Tactic:
rw [← Subtype.coe_le_coe] at h

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
h : (↑a : α) ≤ (↑b : α)
obtain : ∀ (c : α) (hc : (↑b : α) = (↑a : α) + c), ∃ (c : { x : α // 0 ≤ x }), b = a + c
⊢ ∃ (c : { x : α // 0 ≤ x }), b = a + c

Tactic:
obtain ⟨c, hc⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
h : (↑a : α) ≤ (↑b : α)
c : α
hc : (↑b : α) = (↑a : α) + c
⊢ b = a + Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) c ⋯

Tactic:
simp [Subtype.ext_iff, hc]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
h : (↑a : α) ≤ (↑b : α)
c : α
hc : (↑b : α) = (↑a : α) + c
refine : 0 ≤ c
⊢ ∃ (c : { x : α // 0 ≤ x }), b = a + c

Tactic:
refine ⟨⟨c, ?_⟩, by simp [Subtype.ext_iff, hc]⟩
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
h : (↑a : α) ≤ (↑b : α)
c : α
hc : (↑b : α) = (↑a : α) + c
rw : ∀ (c : α) (h : (↑a : α) + 0 ≤ (↑a : α) + c) (hc : (↑b : α) = (↑a : α) + c), 0 ≤ c
⊢ 0 ≤ c

Tactic:
rw [← add_zero a.val, hc] at h

Premises used: add_zero, Subtype.val
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
c : α
h : (↑a : α) + 0 ≤ (↑a : α) + c
hc : (↑b : α) = (↑a : α) + c
⊢ 0 ≤ c

Tactic:
le_of_add_le_add_left h

Premises used: le_of_add_le_add_left
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
c : α
h : (↑a : α) + 0 ≤ (↑a : α) + c
hc : (↑b : α) = (↑a : α) + c
⊢ 0 ≤ c

Tactic:
exact le_of_add_le_add_left h

Premises used: le_of_add_le_add_left
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
⊢ Nontrivial.{u_1} { x : α // 0 ≤ x }

Tactic:
⟨⟨0, 1, fun h => zero_ne_one (congr_arg Subtype.val h)⟩⟩

Premises used: zero_ne_one, Nontrivial.mk, congr_arg, Exists.intro, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : AddGroup α
inst_2 : LinearOrder α
inst_3 : AddLeftMono α
have : ∀ (a : α) (ha : a ≠ 0), Nontrivial.{u_1} { x : α // 0 ≤ x }
⊢ Nontrivial.{u_1} { x : α // 0 ≤ x }

Tactic:
have ⟨a, ha⟩ := exists_ne (0 : α)
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : AddGroup α
inst_2 : LinearOrder α
inst_3 : AddLeftMono α
a : α
ha : a ≠ 0
inl : ∀ (lt : a < 0), Nontrivial.{u_1} { x : α // 0 ≤ x }
inr : ∀ (lt : 0 < a), Nontrivial.{u_1} { x : α // 0 ≤ x }
⊢ Nontrivial.{u_1} { x : α // 0 ≤ x }

Tactic:
obtain lt | lt := ha.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : AddGroup α
inst_2 : LinearOrder α
inst_3 : AddLeftMono α
a : α
ha : a ≠ 0
lt : a < 0
⊢ Nontrivial.{u_1} { x : α // 0 ≤ x }

Tactic:
⟨0, ⟨-a, neg_nonneg.mpr lt.le⟩, Subtype.coe_ne_coe.mp (neg_ne_zero.mpr ha).symm⟩

Premises used: Iff.mpr, LT.lt.le, Ne.symm, Nontrivial.mk, Subtype.mk, neg_nonneg, Exists.intro, Iff.mp, neg_ne_zero, OfNat.ofNat, Neg.neg, Subtype.coe_ne_coe
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : AddGroup α
inst_2 : LinearOrder α
inst_3 : AddLeftMono α
a : α
ha : a ≠ 0
lt : a < 0
⊢ Nontrivial.{u_1} { x : α // 0 ≤ x }

Tactic:
exact ⟨0, ⟨-a, neg_nonneg.mpr lt.le⟩, Subtype.coe_ne_coe.mp (neg_ne_zero.mpr ha).symm⟩
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : AddGroup α
inst_2 : LinearOrder α
inst_3 : AddLeftMono α
a : α
ha : a ≠ 0
lt : 0 < a
⊢ Nontrivial.{u_1} { x : α // 0 ≤ x }

Tactic:
⟨0, ⟨a, lt.le⟩, Subtype.coe_ne_coe.mp ha.symm⟩

Premises used: LT.lt.le, Ne.symm, Nontrivial.mk, Subtype.mk, Exists.intro, Iff.mp, OfNat.ofNat, Subtype.coe_ne_coe
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : AddGroup α
inst_2 : LinearOrder α
inst_3 : AddLeftMono α
a : α
ha : a ≠ 0
lt : 0 < a
⊢ Nontrivial.{u_1} { x : α // 0 ≤ x }

Tactic:
exact ⟨0, ⟨a, lt.le⟩, Subtype.coe_ne_coe.mp ha.symm⟩
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : NoZeroDivisors α
a : α
ha : 0 ≤ a
b : α
hb : 0 ≤ b
⊢ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a ha * Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) b hb = 0 →
    Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a ha = 0 ∨ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) b hb = 0

Tactic:
simp only [mk_mul_mk, mk_eq_zero, mul_eq_zero, imp_self]

Premises used: mul_eq_zero, Nonneg.mk_eq_zero, Nonneg.mk_mul_mk, imp_self
-- Module: Mathlib.Algebra.Order.Nonneg.Ring
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : 0 ≤ a
b : α
hb : 0 ≤ b
c : α
hc : 0 ≤ c
⊢ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a ha - Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) b hb ≤
      Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) c hc ↔
    Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a ha ≤
      Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) c hc + Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) b hb

Tactic:
simp only [sub_le_iff_le_add, Subtype.mk_le_mk, mk_sub_mk, mk_add_mk, toNonneg_le]

Premises used: Nonneg.toNonneg_le, Nonneg.mk_add_mk, Nonneg.mk_sub_mk, sub_le_iff_le_add, Subtype.mk_le_mk
-- Module: Mathlib.Algebra.Order.PUnit
Goal:
x x_1 : PUnit
h : x ≤ x_1
⊢ x_1 = x + unit

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Order.PUnit
Goal:
a b : PUnit
h : a ≤ b
c : PUnit
⊢ a + c ≤ a + c

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.PUnit
Goal:
⊢ ∀ ⦃x : PUnit.{1}⦄, x ≠ () → IsAddLeftRegular x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Pi
Goal:
I : Type u_1
α_1 : Type u_2
β : Type u_3
γ : Type u_4
f : I → Type u_5
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → LE (α i)
inst_1 : (i : ι) → Mul (α i)
inst_2 : ∀ (i : ι), ExistsMulOfLE.{u_7} (α i)
⊢ ExistsMulOfLE ((i : ι) → α i)

Tactic:
⟨fun h =>
    ⟨fun i => (exists_mul_of_le <| h i).choose,
      funext fun i => (exists_mul_of_le <| h i).choose_spec⟩⟩

Premises used: Exists.choose_spec, ExistsMulOfLE.mk, funext, Exists.intro, Exists.choose, ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : Preorder α
a : α
ha : 1 ≤ a
⊢ 1 ≤ const β a

Tactic:
fun _ => ha
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : Preorder α
a : α
ha : a ≤ 1
⊢ const β a ≤ 1

Tactic:
fun _ => ha
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : Preorder α
a : α
inst_2 : Nonempty β
⊢ 1 ≤ const β a ↔ 1 ≤ a

Tactic:
const_le_const

Premises used: Function.const_le_const
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : Preorder α
a : α
inst_2 : Nonempty β
⊢ 1 < const β a ↔ 1 < a

Tactic:
const_lt_const

Premises used: Function.const_lt_const
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : Preorder α
a : α
inst_2 : Nonempty β
⊢ const β a ≤ 1 ↔ a ≤ 1

Tactic:
const_le_const

Premises used: Function.const_le_const
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : Preorder α
a : α
inst_2 : Nonempty β
⊢ const β a < 1 ↔ a < 1

Tactic:
const_lt_const

Premises used: Function.const_lt_const
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : One γ
inst_1 : LE γ
f : α → β
g : α → γ
e : β → γ
hg : 1 ≤ g
he : 1 ≤ e
_b : β
⊢ 1 _b ≤ extend f g e _b

Tactic:
one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)

Premises used: Function.extend, Classical.choose, one_le_dite
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : One γ
inst_1 : LE γ
f : α → β
g : α → γ
e : β → γ
hg : 1 ≤ g
he : 1 ≤ e
_b : β
⊢ 1 _b ≤ extend f g e _b

Tactic:
exact one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)

Premises used: one_le_dite
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : One γ
inst_1 : LE γ
f : α → β
g : α → γ
e : β → γ
hg : 1 ≤ g
he : 1 ≤ e
_b : β
⊢ 1 _b ≤ extend f g e _b

Tactic:
classical exact one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)

Premises used: one_le_dite
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : One γ
inst_1 : LE γ
f : α → β
g : α → γ
e : β → γ
hg : g ≤ 1
he : e ≤ 1
_b : β
⊢ extend f g e _b ≤ 1 _b

Tactic:
dite_le_one (fun _ ↦ hg _) (fun _ ↦ he _)

Premises used: Function.extend, Classical.choose, dite_le_one
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : One γ
inst_1 : LE γ
f : α → β
g : α → γ
e : β → γ
hg : g ≤ 1
he : e ≤ 1
_b : β
⊢ extend f g e _b ≤ 1 _b

Tactic:
exact dite_le_one (fun _ ↦ hg _) (fun _ ↦ he _)

Premises used: dite_le_one
-- Module: Mathlib.Algebra.Order.Pi
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : One γ
inst_1 : LE γ
f : α → β
g : α → γ
e : β → γ
hg : g ≤ 1
he : e ≤ 1
_b : β
⊢ extend f g e _b ≤ 1 _b

Tactic:
classical exact dite_le_one (fun _ ↦ hg _) (fun _ ↦ he _)

Premises used: dite_le_one
-- Module: Mathlib.Algebra.Order.Pi
Goal:
ι : Type u_6
α : ι → Type u_7
inst : DecidableEq ι
inst_1 : (i : ι) → One (α i)
inst_2 : (i : ι) → Preorder (α i)
i : ι
a b : α i
⊢ mulSingle (M := α) i a ≤ mulSingle (M := α) i b ↔ a ≤ b

Tactic:
simp [mulSingle]

Premises used: Pi.mulSingle
-- Module: Mathlib.Algebra.Order.Pi
Goal:
ι : Type u_6
α : ι → Type u_7
inst : DecidableEq ι
inst_1 : (i : ι) → One (α i)
inst_2 : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ 1 ≤ mulSingle (M := α) i a ↔ 1 ≤ a

Tactic:
simp [mulSingle]

Premises used: Pi.mulSingle
-- Module: Mathlib.Algebra.Order.Pi
Goal:
ι : Type u_6
α : ι → Type u_7
inst : DecidableEq ι
inst_1 : (i : ι) → One (α i)
inst_2 : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ 1 < mulSingle (M := α) i a ↔ 1 < a

Tactic:
simp [mulSingle]

Premises used: Pi.mulSingle
-- Module: Mathlib.Algebra.Order.Pi
Goal:
ι : Type u_6
α : ι → Type u_7
inst : DecidableEq ι
inst_1 : (i : ι) → One (α i)
inst_2 : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ mulSingle (M := α) i a ≤ 1 ↔ a ≤ 1

Tactic:
simp [mulSingle]

Premises used: Pi.mulSingle
-- Module: Mathlib.Algebra.Order.Positive.Field
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : { x : K // 0 < x }
⊢ (↑x⁻¹ : K) = (↑x : K)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Positive.Field
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : { x : K // 0 < x }
n : ℤ
⊢ (↑(x ^ n) : K) = (↑x : K) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Positive.Ring
Goal:
M : Type u_1
inst : AddMonoid M
inst_1 : Preorder M
inst_2 : AddLeftStrictMono M
x y : { x : M // 0 < x }
⊢ (↑(x + y) : M) = (↑x : M) + (↑y : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Positive.Ring
Goal:
M : Type u_1
R : Type u_2
inst : AddMonoid M
inst_1 : Preorder M
inst_2 : AddLeftStrictMono M
⊢ AddLeftStrictMono.{u_1} { x : M // 0 < x }

Tactic:
⟨fun _ y z hyz => Subtype.coe_lt_coe.1 <| add_lt_add_right (show (y : M) < z from hyz) _⟩

Premises used: CovariantClass.mk, add_lt_add_right, Subtype.coe_lt_coe, Iff.mp, Subtype.val
-- Module: Mathlib.Algebra.Order.Positive.Ring
Goal:
M : Type u_1
R : Type u_2
inst : AddMonoid M
inst_1 : Preorder M
inst_2 : AddLeftStrictMono M
inst_3 : AddRightStrictMono M
⊢ AddRightStrictMono.{u_1} { x : M // 0 < x }

Tactic:
⟨fun _ y z hyz => Subtype.coe_lt_coe.1 <| add_lt_add_left (show (y : M) < z from hyz) _⟩

Premises used: CovariantClass.mk, add_lt_add_left, Subtype.coe_lt_coe, Iff.mp, Subtype.val
-- Module: Mathlib.Algebra.Order.Positive.Ring
Goal:
M : Type u_1
R : Type u_2
inst : AddMonoid M
inst_1 : Preorder M
inst_2 : AddLeftStrictMono M
inst_3 : AddLeftReflectLT M
⊢ AddLeftReflectLT.{u_1} { x : M // 0 < x }

Tactic:
⟨fun _ _ _ h => Subtype.coe_lt_coe.1 <| lt_of_add_lt_add_left h⟩

Premises used: Subtype.coe_lt_coe, ContravariantClass.mk, Iff.mp, lt_of_add_lt_add_left
-- Module: Mathlib.Algebra.Order.Positive.Ring
Goal:
M : Type u_1
R : Type u_2
inst : AddMonoid M
inst_1 : Preorder M
inst_2 : AddLeftStrictMono M
inst_3 : AddRightReflectLT M
⊢ AddRightReflectLT.{u_1} { x : M // 0 < x }

Tactic:
⟨fun _ _ _ h => Subtype.coe_lt_coe.1 <| lt_of_add_lt_add_right h⟩

Premises used: Subtype.coe_lt_coe, ContravariantClass.mk, Iff.mp, lt_of_add_lt_add_right
-- Module: Mathlib.Algebra.Order.Positive.Ring
Goal:
M : Type u_1
R : Type u_2
inst : AddMonoid M
inst_1 : PartialOrder M
inst_2 : AddLeftStrictMono M
⊢ AddLeftMono.{u_1} { x : M // 0 < x }

Tactic:
⟨@fun _ _ _ h₁ => StrictMono.monotone (fun _ _ h => add_lt_add_right h _) h₁⟩

Premises used: CovariantClass.mk, add_lt_add_right, StrictMono.monotone
-- Module: Mathlib.Algebra.Order.Positive.Ring
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
x y : { x : R // 0 < x }
⊢ (↑(x * y) : R) = (↑x : R) * (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Positive.Ring
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
x : { x : R // 0 < x }
n : ℕ
⊢ (↑(x ^ n) : R) = (↑x : R) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Positive.Ring
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
⊢ Eq.{u_2 + 1} (α := R) (↑1 : R) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
x : α
s : Set α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
⊢ x * sSup s = ⨆ y ∈ s, x * y

Tactic:
IsQuantale.mul_sSup_distrib _ _

Premises used: IsQuantale.mul_sSup_distrib
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
x : α
s : Set α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
⊢ sSup s * x = ⨆ y ∈ s, y * x

Tactic:
IsQuantale.sSup_mul_distrib _ _

Premises used: IsQuantale.sSup_mul_distrib
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
rw : x * sSup (Set.range fun (i : ι) ↦ f i) = ⨆ (i : ι), x * f i
rw₁ :
  Eq.{u_1 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ f i) y), x * y)
    (⨆ (i : ι), x * f i)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), x * f i) (⨆ (i : ι), x * f i)
⊢ x * ⨆ (i : ι), f i = ⨆ (i : ι), x * f i

Tactic:
rw [iSup, mul_sSup_distrib, iSup_range]

Premises used: iSup, iSup_range, mul_sSup_distrib
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
rw : sSup (Set.range fun (i : ι) ↦ f i) * x = ⨆ (i : ι), f i * x
rw₁ :
  Eq.{u_1 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ f i) y), y * x)
    (⨆ (i : ι), f i * x)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i * x) (⨆ (i : ι), f i * x)
⊢ (⨆ (i : ι), f i) * x = ⨆ (i : ι), f i * x

Tactic:
rw [iSup, sSup_mul_distrib, iSup_range]

Premises used: iSup, iSup_range, sSup_mul_distrib