awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
rw :
  (∀ (i j : ι),
      0 ≤
        (f j - f i) •
          HSub.hSub (α := βᵒᵈ) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)
            (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i)) ↔
    ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0
⊢ Monovary (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) ↔ ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0

Tactic:
rw [monovary_iff_forall_smul_nonneg]

Premises used: monovary_iff_forall_smul_nonneg
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
⊢ (∀ (i j : ι),
      0 ≤
        (f j - f i) •
          HSub.hSub (α := βᵒᵈ) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)
            (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i)) ↔
    ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
s : Set ι
i : ι
h : i ∈ s
j : ι
h_1 : j ∈ s
⊢ 0 ≤ (f j - f i) • (g j - g i) ↔ f i • g j + f j • g i ≤ f i • g i + f j • g j

Tactic:
simp [smul_sub, sub_smul, ← add_sub_right_comm, le_sub_iff_add_le, add_comm (f i • g i),
      add_comm (f i • g j)]

Premises used: sub_smul, add_sub_right_comm, add_comm, smul_sub, HSMul.hSMul, le_sub_iff_add_le
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
s : Set ι
rw :
  (∀ ⦃i : ι⦄,
      i ∈ s →
        ∀ ⦃j : ι⦄,
          j ∈ s →
            HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j) +
                HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) ≤
              HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) +
                HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)) ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
⊢ MonovaryOn (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) s ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
rw [monovaryOn_iff_smul_rearrangement]

Premises used: monovaryOn_iff_smul_rearrangement
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
s : Set ι
⊢ (∀ ⦃i : ι⦄,
      i ∈ s →
        ∀ ⦃j : ι⦄,
          j ∈ s →
            HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j) +
                HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) ≤
              HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) +
                HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)) ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
⊢ (∀ ⦃i : ι⦄,
      Membership.mem (γ := Set ι) Set.univ i →
        ∀ ⦃j : ι⦄, Membership.mem (γ := Set ι) Set.univ j → f i • g j + f j • g i ≤ f i • g i + f j • g j) ↔
    ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j

Tactic:
simp only [Set.mem_univ, forall_true_left]

Premises used: forall_true_left, Set.mem_univ
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
rw :
  (∀ (i j : ι),
      HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j) +
          HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) ≤
        HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) +
          HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)) ↔
    ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
⊢ Monovary (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) ↔
    ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
rw [monovary_iff_smul_rearrangement]

Premises used: monovary_iff_smul_rearrangement
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
⊢ (∀ (i j : ι),
      HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j) +
          HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) ≤
        HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) +
          HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)) ↔
    ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : ι → α
s : Set ι
⊢ MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)

Tactic:
simp only [smul_eq_mul, monovaryOn_iff_forall_smul_nonneg]

Premises used: monovaryOn_iff_forall_smul_nonneg, smul_eq_mul
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : ι → α
s : Set ι
⊢ AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0

Tactic:
simp only [smul_eq_mul, antivaryOn_iff_forall_smul_nonpos]

Premises used: smul_eq_mul, antivaryOn_iff_forall_smul_nonpos
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : ι → α
⊢ Monovary f g ↔ ∀ (i j : ι), 0 ≤ (f j - f i) * (g j - g i)

Tactic:
simp only [smul_eq_mul, monovary_iff_forall_smul_nonneg]

Premises used: monovary_iff_forall_smul_nonneg, smul_eq_mul
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : ι → α
⊢ Antivary f g ↔ ∀ (i j : ι), (f j - f i) * (g j - g i) ≤ 0

Tactic:
simp only [smul_eq_mul, antivary_iff_forall_smul_nonpos]

Premises used: smul_eq_mul, antivary_iff_forall_smul_nonpos
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : ι → α
s : Set ι
⊢ MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j

Tactic:
simp only [smul_eq_mul, monovaryOn_iff_smul_rearrangement]

Premises used: monovaryOn_iff_smul_rearrangement, smul_eq_mul
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : ι → α
s : Set ι
⊢ AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i

Tactic:
simp only [smul_eq_mul, antivaryOn_iff_smul_rearrangement]

Premises used: antivaryOn_iff_smul_rearrangement, smul_eq_mul
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : ι → α
⊢ Monovary f g ↔ ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j

Tactic:
simp only [smul_eq_mul, monovary_iff_smul_rearrangement]

Premises used: monovary_iff_smul_rearrangement, smul_eq_mul
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : ι → α
⊢ Antivary f g ↔ ∀ (i j : ι), f i * g i + f j * g j ≤ f i * g j + f j * g i

Tactic:
simp only [smul_eq_mul, antivary_iff_smul_rearrangement]

Premises used: antivary_iff_smul_rearrangement, smul_eq_mul
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
⊢ Eq.{u_1 + 1} (α := α) (↑0 : α) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
x : α
hx : 0 ≤ x
⊢ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) x hx = 0 ↔ x = 0

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : AddZeroClass α
inst_1 : Preorder α
inst_2 : AddLeftMono α
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.Basic
Goal:
α : Type u_1
inst : AddZeroClass α
inst_1 : Preorder α
inst_2 : AddLeftMono α
a b : { x : α // 0 ≤ x }
⊢ (↑(a + b) : α) = (↑a : α) + (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : Preorder α
inst_2 : AddLeftMono α
n : ℕ
x : α
hx : 0 ≤ x
⊢ n • Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) x hx = Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) (n • x) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : Preorder α
inst_2 : AddLeftMono α
n : ℕ
a : { x : α // 0 ≤ x }
⊢ (↑(n • a) : α) = n • (↑a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : LE α
inst_3 : ZeroLEOneClass α
⊢ Eq.{u_1 + 1} (α := α) (↑1 : α) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : LE α
inst_3 : ZeroLEOneClass α
x : α
hx : 0 ≤ x
⊢ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) x hx = 1 ↔ x = 1

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : Preorder α
inst_2 : PosMulMono α
a b : { x : α // 0 ≤ x }
⊢ (↑(a * b) : α) = (↑a : α) * (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : Preorder α
inst_2 : PosMulMono α
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.Basic
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : Preorder α
inst_2 : AddLeftMono α
n : ℕ
r : { x : α // 0 ≤ x }
⊢ (↑(n • r) : α) = n • (↑r : α)

Tactic:
Nonneg.coeAddMonoidHom.map_nsmul _ _

Premises used: AddMonoidHom.map_nsmul, Nonneg.coeAddMonoidHom
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : { x : α // 0 ≤ x }) : α) (↑n : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
n : ℕ
⊢ Eq.{u_1 + 1} (α := { x : α // 0 ≤ x }) (Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) (↑n : α) ⋯) (↑n : { x : α // 0 ≤ x })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
a : Eq.{u_1 + 1} (α := α) (↑↑0 : α) (↑0 : α)
⊢ Eq.{u_1 + 1} (α := { x : α // 0 ≤ x }) (↑0) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
⊢ Eq.{u_1 + 1} (α := α) (↑↑0 : α) (↑0 : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
x : ℕ
a : (↑↑(x + 1) : α) = (↑(HAdd.hAdd (α := { x : α // 0 ≤ x }) (↑x) 1) : α)
⊢ ↑(x + 1) = HAdd.hAdd (α := { x : α // 0 ≤ x }) (↑x) 1

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
x : ℕ
⊢ (↑↑(x + 1) : α) = (↑(HAdd.hAdd (α := { x : α // 0 ≤ x }) (↑x) 1) : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : PosMulMono α
a : { x : α // 0 ≤ x }
n : ℕ
⊢ (↑(a ^ n) : α) = (↑a : α) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : PosMulMono α
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.Basic
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
inst_4 : PosMulMono α
⊢ MonoidWithZero { x : α // 0 ≤ x }

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : SemilatticeSup α
a : α
⊢ (↑(toNonneg a) : α) = a ⊔ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : SemilatticeSup α
a : α
h : 0 ≤ a
⊢ toNonneg a = Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a h

Tactic:
simp [toNonneg, h]

Premises used: Nonneg.toNonneg
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : SemilatticeSup α
a : { x : α // 0 ≤ x }
⊢ toNonneg (↑a : α) = a

Tactic:
toNonneg_of_nonneg a.2

Premises used: Nonneg.toNonneg_of_nonneg, Subtype.property
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : SemilatticeSup α
a : α
b : { x : α // 0 ≤ x }
obtain :
  ∀ (b : α) (hb : 0 ≤ b),
    toNonneg a ≤ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) b hb ↔ a ≤ (↑(Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) b hb) : α)
⊢ toNonneg a ≤ b ↔ a ≤ (↑b : α)

Tactic:
obtain ⟨b, hb⟩ := b
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : SemilatticeSup α
a b : α
hb : 0 ≤ b
⊢ toNonneg a ≤ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) b hb ↔ a ≤ (↑(Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) b hb) : α)

Tactic:
simp [toNonneg, hb]

Premises used: Nonneg.toNonneg
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : SemilatticeSup α
inst_2 : Sub α
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 = toNonneg (x - y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : { x : α // 0 ≤ x }
b : α
obtain :
  ∀ (a : α) (ha : 0 ≤ a),
    Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a ha < toNonneg b ↔ (↑(Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a ha) : α) < b
⊢ a < toNonneg b ↔ (↑a : α) < b

Tactic:
obtain ⟨a, ha⟩ := a
-- Module: Mathlib.Algebra.Order.Nonneg.Basic
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
b a : α
ha : 0 ≤ a
⊢ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a ha < toNonneg b ↔ (↑(Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a ha) : α) < b

Tactic:
simp [toNonneg, ha.not_gt]

Premises used: LE.le.not_gt, Nonneg.toNonneg
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
rw : 0 ≤ HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
⊢ LE.le.{u_1} (α := α) 0 (↑q : α)

Tactic:
rw [cast_def]

Premises used: NNRat.cast_def
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
⊢ 0 ≤ HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)

Tactic:
div_nonneg q.num.cast_nonneg q.den.cast_nonneg

Premises used: Nat.cast_nonneg, NNRat.num, NNRat.den, div_nonneg
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
⊢ 0 ≤ HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)

Tactic:
exact div_nonneg q.num.cast_nonneg q.den.cast_nonneg

Premises used: div_nonneg
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
q : ℚ≥0
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 α
a : α
q : ℚ≥0
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 α
a : α
q : ℚ≥0
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
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 < r }
a :
  (↑(Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯ * Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯) : R) =
    (↑1 : R)
⊢ Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯ * Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯ = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 < r }
⊢ (↑(Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯ * Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯) : R) =
    (↑1 : R)

Tactic:
simp [r.2.ne']

Premises used: LT.lt.ne', Subtype.property
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 < r }
a :
  (↑(Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯ * Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯) : R) =
    (↑1 : R)
⊢ Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯ * Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯ = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 < r }
⊢ (↑(Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯ * Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯) : R) =
    (↑1 : R)

Tactic:
simp [r.2.ne']

Premises used: LT.lt.ne', Subtype.property
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 ≤ r }ˣ
huv :
  (↑(↑((fun (r : { r : R // 0 < r }) ↦
                ({ val := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯,
                    inv := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯, val_inv := ⋯, inv_val := ⋯ } :
                  { r : R // 0 ≤ r }ˣ))
              ((fun (r : { r : R // 0 ≤ r }ˣ) ↦
                  Subtype.mk (p := fun (r : R) ↦ 0 < r) (↑(↑r : { r : R // 0 ≤ r }) : R) ⋯)
                r)) :
          { r : R // 0 ≤ r }) :
      R) =
    (↑(↑r : { r : R // 0 ≤ r }) : R)
⊢ (fun (r : { r : R // 0 < r }) ↦
        ({ val := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯,
            inv := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯, val_inv := ⋯, inv_val := ⋯ } :
          { r : R // 0 ≤ r }ˣ))
      ((fun (r : { r : R // 0 ≤ r }ˣ) ↦ Subtype.mk (p := fun (r : R) ↦ 0 < r) (↑(↑r : { r : R // 0 ≤ r }) : R) ⋯) r) =
    r

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 ≤ r }ˣ
⊢ (↑(↑((fun (r : { r : R // 0 < r }) ↦
                ({ val := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯,
                    inv := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯, val_inv := ⋯, inv_val := ⋯ } :
                  { r : R // 0 ≤ r }ˣ))
              ((fun (r : { r : R // 0 ≤ r }ˣ) ↦
                  Subtype.mk (p := fun (r : R) ↦ 0 < r) (↑(↑r : { r : R // 0 ≤ r }) : R) ⋯)
                r)) :
          { r : R // 0 ≤ r }) :
      R) =
    (↑(↑r : { r : R // 0 ≤ r }) : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 < r }
a :
  (↑((fun (r : { r : R // 0 ≤ r }ˣ) ↦ Subtype.mk (p := fun (r : R) ↦ 0 < r) (↑(↑r : { r : R // 0 ≤ r }) : R) ⋯)
          ((fun (r : { r : R // 0 < r }) ↦
              ({ val := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯,
                  inv := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯, val_inv := ⋯, inv_val := ⋯ } :
                { r : R // 0 ≤ r }ˣ))
            r)) :
      R) =
    (↑r : R)
⊢ (fun (r : { r : R // 0 ≤ r }ˣ) ↦ Subtype.mk (p := fun (r : R) ↦ 0 < r) (↑(↑r : { r : R // 0 ≤ r }) : R) ⋯)
      ((fun (r : { r : R // 0 < r }) ↦
          ({ val := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯,
              inv := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯, val_inv := ⋯, inv_val := ⋯ } :
            { r : R // 0 ≤ r }ˣ))
        r) =
    r

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 < r }
⊢ (↑((fun (r : { r : R // 0 ≤ r }ˣ) ↦ Subtype.mk (p := fun (r : R) ↦ 0 < r) (↑(↑r : { r : R // 0 ≤ r }) : R) ⋯)
          ((fun (r : { r : R // 0 < r }) ↦
              ({ val := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯,
                  inv := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯, val_inv := ⋯, inv_val := ⋯ } :
                { r : R // 0 ≤ r }ˣ))
            r)) :
      R) =
    (↑r : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Nonneg.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : { x : α // 0 ≤ x }
⊢ (↑a⁻¹ : α) = (↑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 : α
hx : 0 ≤ x
⊢ (Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) x hx)⁻¹ = Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) x⁻¹ ⋯

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl