awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
s : Set ι
f : ι → α
g₁ g₂ : ι → β
h₁ : AntivaryOn f g₁ s
h₂ : AntivaryOn f g₂ s
⊢ AntivaryOn f (g₁ * g₂) s

Tactic:
fun _i hi _j hj hij ↦ (lt_or_lt_of_mul_lt_mul hij).elim (h₁ hi hj) <| h₂ hi hj

Premises used: lt_or_lt_of_mul_lt_mul, AntivaryOn, Or.elim
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
s : Set ι
f : ι → α
g₁ g₂ : ι → β
h₁ : MonovaryOn f g₁ s
h₂ : AntivaryOn f g₂ s
⊢ MonovaryOn f (g₁ / g₂) s

Tactic:
fun _i hi _j hj hij ↦ (lt_or_lt_of_div_lt_div hij).elim (h₁ hi hj) <| h₂ hj hi

Premises used: MonovaryOn, Or.elim, lt_or_lt_of_div_lt_div
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
s : Set ι
f : ι → α
g₁ g₂ : ι → β
h₁ : AntivaryOn f g₁ s
h₂ : MonovaryOn f g₂ s
⊢ AntivaryOn f (g₁ / g₂) s

Tactic:
fun _i hi _j hj hij ↦ (lt_or_lt_of_div_lt_div hij).elim (h₁ hi hj) <| h₂ hj hi

Premises used: AntivaryOn, Or.elim, lt_or_lt_of_div_lt_div
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g s
n : ℕ
⊢ MonovaryOn f (g ^ n) s

Tactic:
fun _i hi _j hj hij ↦ hfg hi hj <| lt_of_pow_lt_pow_left' _ hij

Premises used: MonovaryOn, lt_of_pow_lt_pow_left'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g s
n : ℕ
⊢ AntivaryOn f (g ^ n) s

Tactic:
fun _i hi _j hj hij ↦ hfg hi hj <| lt_of_pow_lt_pow_left' _ hij

Premises used: AntivaryOn, lt_of_pow_lt_pow_left'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
f : ι → α
g₁ g₂ : ι → β
h₁ : Monovary f g₁
h₂ : Monovary f g₂
⊢ Monovary f (g₁ * g₂)

Tactic:
fun _i _j hij ↦ (lt_or_lt_of_mul_lt_mul hij).elim (fun h ↦ h₁ h) fun h ↦ h₂ h

Premises used: Monovary, lt_or_lt_of_mul_lt_mul, Or.elim
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
f : ι → α
g₁ g₂ : ι → β
h₁ : Antivary f g₁
h₂ : Antivary f g₂
⊢ Antivary f (g₁ * g₂)

Tactic:
fun _i _j hij ↦ (lt_or_lt_of_mul_lt_mul hij).elim (fun h ↦ h₁ h) fun h ↦ h₂ h

Premises used: Antivary, lt_or_lt_of_mul_lt_mul, Or.elim
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
f : ι → α
g₁ g₂ : ι → β
h₁ : Monovary f g₁
h₂ : Antivary f g₂
⊢ Monovary f (g₁ / g₂)

Tactic:
fun _i _j hij ↦ (lt_or_lt_of_div_lt_div hij).elim (fun h ↦ h₁ h) fun h ↦ h₂ h

Premises used: Monovary, Or.elim, lt_or_lt_of_div_lt_div
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
f : ι → α
g₁ g₂ : ι → β
h₁ : Antivary f g₁
h₂ : Monovary f g₂
⊢ Antivary f (g₁ / g₂)

Tactic:
fun _i _j hij ↦ (lt_or_lt_of_div_lt_div hij).elim (fun h ↦ h₁ h) fun h ↦ h₂ h

Premises used: Antivary, Or.elim, lt_or_lt_of_div_lt_div
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
f : ι → α
g : ι → β
hfg : Monovary f g
n : ℕ
⊢ Monovary f (g ^ n)

Tactic:
fun _i _j hij ↦ hfg <| lt_of_pow_lt_pow_left' _ hij

Premises used: Monovary, lt_of_pow_lt_pow_left'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
f : ι → α
g : ι → β
hfg : Antivary f g
n : ℕ
⊢ Antivary f (g ^ n)

Tactic:
fun _i _j hij ↦ hfg <| lt_of_pow_lt_pow_left' _ hij

Premises used: Antivary, lt_of_pow_lt_pow_left'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : PartialOrder β
s : Set ι
f₁ f₂ : ι → α
g : ι → β
hf₁ : ∀ (i : ι), i ∈ s → 0 ≤ f₁ i
hf₂ : ∀ (i : ι), i ∈ s → 0 ≤ f₂ i
h₁ : MonovaryOn f₁ g s
h₂ : MonovaryOn f₂ g s
⊢ MonovaryOn (f₁ * f₂) g s

Tactic:
fun _i hi _j hj hij ↦ mul_le_mul (h₁ hi hj hij) (h₂ hi hj hij) (hf₂ _ hi) (hf₁ _ hj)

Premises used: MonovaryOn, mul_le_mul
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : PartialOrder β
s : Set ι
f₁ f₂ : ι → α
g : ι → β
hf₁ : ∀ (i : ι), i ∈ s → 0 ≤ f₁ i
hf₂ : ∀ (i : ι), i ∈ s → 0 ≤ f₂ i
h₁ : AntivaryOn f₁ g s
h₂ : AntivaryOn f₂ g s
⊢ AntivaryOn (f₁ * f₂) g s

Tactic:
fun _i hi _j hj hij ↦ mul_le_mul (h₁ hi hj hij) (h₂ hi hj hij) (hf₂ _ hj) (hf₁ _ hi)

Premises used: AntivaryOn, mul_le_mul
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : PartialOrder β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hfg : MonovaryOn f g s
n : ℕ
⊢ MonovaryOn (f ^ n) g s

Tactic:
fun _i hi _j hj hij ↦ pow_le_pow_left₀ (hf _ hi) (hfg hi hj hij) _

Premises used: pow_le_pow_left₀, MonovaryOn
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : PartialOrder β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hfg : AntivaryOn f g s
n : ℕ
⊢ AntivaryOn (f ^ n) g s

Tactic:
fun _i hi _j hj hij ↦ pow_le_pow_left₀ (hf _ hj) (hfg hi hj hij) _

Premises used: pow_le_pow_left₀, AntivaryOn
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : PartialOrder β
f₁ f₂ : ι → α
g : ι → β
hf₁ : 0 ≤ f₁
hf₂ : 0 ≤ f₂
h₁ : Monovary f₁ g
h₂ : Monovary f₂ g
⊢ Monovary (f₁ * f₂) g

Tactic:
fun _i _j hij ↦ mul_le_mul (h₁ hij) (h₂ hij) (hf₂ _) (hf₁ _)

Premises used: Monovary, mul_le_mul
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : PartialOrder β
f₁ f₂ : ι → α
g : ι → β
hf₁ : 0 ≤ f₁
hf₂ : 0 ≤ f₂
h₁ : Antivary f₁ g
h₂ : Antivary f₂ g
⊢ Antivary (f₁ * f₂) g

Tactic:
fun _i _j hij ↦ mul_le_mul (h₁ hij) (h₂ hij) (hf₂ _) (hf₁ _)

Premises used: Antivary, mul_le_mul
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : PartialOrder β
f : ι → α
g : ι → β
hf : 0 ≤ f
hfg : Monovary f g
n : ℕ
⊢ Monovary (f ^ n) g

Tactic:
fun _i _j hij ↦ pow_le_pow_left₀ (hf _) (hfg hij) _

Premises used: Monovary, pow_le_pow_left₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : PartialOrder β
f : ι → α
g : ι → β
hf : 0 ≤ f
hfg : Antivary f g
n : ℕ
⊢ Antivary (f ^ n) g

Tactic:
fun _i _j hij ↦ pow_le_pow_left₀ (hf _) (hfg hij) _

Premises used: Antivary, pow_le_pow_left₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g₁ g₂ : ι → β
hg₁ : ∀ (i : ι), i ∈ s → 0 ≤ g₁ i
hg₂ : ∀ (i : ι), i ∈ s → 0 ≤ g₂ i
h₁ : MonovaryOn f g₁ s
h₂ : MonovaryOn f g₂ s
⊢ MonovaryOn f (g₁ * g₂) s

Tactic:
(h₁.symm.mul_left₀ hg₁ hg₂ h₂.symm).symm

Premises used: MonovaryOn.symm, MonovaryOn.mul_left₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g₁ g₂ : ι → β
hg₁ : ∀ (i : ι), i ∈ s → 0 ≤ g₁ i
hg₂ : ∀ (i : ι), i ∈ s → 0 ≤ g₂ i
h₁ : AntivaryOn f g₁ s
h₂ : AntivaryOn f g₂ s
⊢ AntivaryOn f (g₁ * g₂) s

Tactic:
(h₁.symm.mul_left₀ hg₁ hg₂ h₂.symm).symm

Premises used: AntivaryOn.mul_left₀, AntivaryOn.symm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hfg : MonovaryOn f g s
n : ℕ
⊢ MonovaryOn f (g ^ n) s

Tactic:
(hfg.symm.pow_left₀ hg _).symm

Premises used: MonovaryOn.symm, MonovaryOn.pow_left₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hfg : AntivaryOn f g s
n : ℕ
⊢ AntivaryOn f (g ^ n) s

Tactic:
(hfg.symm.pow_left₀ hg _).symm

Premises used: AntivaryOn.pow_left₀, AntivaryOn.symm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f : ι → α
g₁ g₂ : ι → β
hg₁ : 0 ≤ g₁
hg₂ : 0 ≤ g₂
h₁ : Monovary f g₁
h₂ : Monovary f g₂
⊢ Monovary f (g₁ * g₂)

Tactic:
(h₁.symm.mul_left₀ hg₁ hg₂ h₂.symm).symm

Premises used: Monovary.symm, Monovary.mul_left₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f : ι → α
g₁ g₂ : ι → β
hg₁ : 0 ≤ g₁
hg₂ : 0 ≤ g₂
h₁ : Antivary f g₁
h₂ : Antivary f g₂
⊢ Antivary f (g₁ * g₂)

Tactic:
(h₁.symm.mul_left₀ hg₁ hg₂ h₂.symm).symm

Premises used: Antivary.mul_left₀, Antivary.symm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f : ι → α
g : ι → β
hg : 0 ≤ g
hfg : Monovary f g
n : ℕ
⊢ Monovary f (g ^ n)

Tactic:
(hfg.symm.pow_left₀ hg _).symm

Premises used: Monovary.pow_left₀, Monovary.symm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f : ι → α
g : ι → β
hg : 0 ≤ g
hfg : Antivary f g
n : ℕ
⊢ Antivary f (g ^ n)

Tactic:
(hfg.symm.pow_left₀ hg _).symm

Premises used: Antivary.pow_left₀, Antivary.symm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : LinearOrder β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
⊢ MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s

Tactic:
forall₅_congr fun _i hi _j hj _ ↦ inv_le_inv₀ (hf _ hi) (hf _ hj)

Premises used: forall₅_congr, MonovaryOn, AntivaryOn, inv_le_inv₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : LinearOrder β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
⊢ AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s

Tactic:
forall₅_congr fun _i hi _j hj _ ↦ inv_le_inv₀ (hf _ hj) (hf _ hi)

Premises used: forall₅_congr, MonovaryOn, AntivaryOn, inv_le_inv₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : LinearOrder β
f : ι → α
g : ι → β
hf : StrongLT (π := fun (i : ι) ↦ α) 0 f
⊢ Monovary f⁻¹ g ↔ Antivary f g

Tactic:
forall₃_congr fun _i _j _ ↦ inv_le_inv₀ (hf _) (hf _)

Premises used: Monovary, Antivary, forall₃_congr, inv_le_inv₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : LinearOrder β
f : ι → α
g : ι → β
hf : StrongLT (π := fun (i : ι) ↦ α) 0 f
⊢ Antivary f⁻¹ g ↔ Monovary f g

Tactic:
forall₃_congr fun _i _j _ ↦ inv_le_inv₀ (hf _) (hf _)

Premises used: Monovary, Antivary, forall₃_congr, inv_le_inv₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : LinearOrder β
s : Set ι
f₁ f₂ : ι → α
g : ι → β
hf₁ : ∀ (i : ι), i ∈ s → 0 ≤ f₁ i
hf₂ : ∀ (i : ι), i ∈ s → 0 < f₂ i
h₁ : MonovaryOn f₁ g s
h₂ : AntivaryOn f₂ g s
⊢ MonovaryOn (f₁ / f₂) g s

Tactic:
fun _i hi _j hj hij ↦ div_le_div₀ (hf₁ _ hj) (h₁ hi hj hij) (hf₂ _ hj) <| h₂ hi hj hij

Premises used: div_le_div₀, MonovaryOn
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : LinearOrder β
s : Set ι
f₁ f₂ : ι → α
g : ι → β
hf₁ : ∀ (i : ι), i ∈ s → 0 ≤ f₁ i
hf₂ : ∀ (i : ι), i ∈ s → 0 < f₂ i
h₁ : AntivaryOn f₁ g s
h₂ : MonovaryOn f₂ g s
⊢ AntivaryOn (f₁ / f₂) g s

Tactic:
fun _i hi _j hj hij ↦ div_le_div₀ (hf₁ _ hi) (h₁ hi hj hij) (hf₂ _ hi) <| h₂ hi hj hij

Premises used: div_le_div₀, AntivaryOn
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : LinearOrder β
f₁ f₂ : ι → α
g : ι → β
hf₁ : 0 ≤ f₁
hf₂ : StrongLT (π := fun (i : ι) ↦ α) 0 f₂
h₁ : Monovary f₁ g
h₂ : Antivary f₂ g
⊢ Monovary (f₁ / f₂) g

Tactic:
fun _i _j hij ↦ div_le_div₀ (hf₁ _) (h₁ hij) (hf₂ _) <| h₂ hij

Premises used: div_le_div₀, Monovary
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : LinearOrder β
f₁ f₂ : ι → α
g : ι → β
hf₁ : 0 ≤ f₁
hf₂ : StrongLT (π := fun (i : ι) ↦ α) 0 f₂
h₁ : Antivary f₁ g
h₂ : Monovary f₂ g
⊢ Antivary (f₁ / f₂) g

Tactic:
fun _i _j hij ↦ div_le_div₀ (hf₁ _) (h₁ hij) (hf₂ _) <| h₂ hij

Premises used: div_le_div₀, Antivary
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semifield β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hg : ∀ (i : ι), i ∈ s → 0 < g i
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
⊢ g⁻¹ j < g⁻¹ i → f j ≤ f i ↔ g i < g j → f j ≤ f i

Tactic:
simp [inv_lt_inv₀ (hg _ hj) (hg _ hi)]

Premises used: inv_lt_inv₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semifield β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hg : ∀ (i : ι), i ∈ s → 0 < g i
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
⊢ g⁻¹ j < g⁻¹ i → f i ≤ f j ↔ g i < g j → f i ≤ f j

Tactic:
simp [inv_lt_inv₀ (hg _ hj) (hg _ hi)]

Premises used: inv_lt_inv₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semifield β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f : ι → α
g : ι → β
hg : StrongLT (π := fun (i : ι) ↦ β) 0 g
i j : ι
⊢ g⁻¹ j < g⁻¹ i → f j ≤ f i ↔ g i < g j → f j ≤ f i

Tactic:
simp [inv_lt_inv₀ (hg _) (hg _)]

Premises used: inv_lt_inv₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semifield β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f : ι → α
g : ι → β
hg : StrongLT (π := fun (i : ι) ↦ β) 0 g
i j : ι
⊢ g⁻¹ j < g⁻¹ i → f i ≤ f j ↔ g i < g j → f i ≤ f j

Tactic:
simp [inv_lt_inv₀ (hg _) (hg _)]

Premises used: inv_lt_inv₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semifield β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g₁ g₂ : ι → β
hg₁ : ∀ (i : ι), i ∈ s → 0 ≤ g₁ i
hg₂ : ∀ (i : ι), i ∈ s → 0 < g₂ i
h₁ : MonovaryOn f g₁ s
h₂ : AntivaryOn f g₂ s
⊢ MonovaryOn f (g₁ / g₂) s

Tactic:
(h₁.symm.div_left₀ hg₁ hg₂ h₂.symm).symm

Premises used: MonovaryOn.symm, MonovaryOn.div_left₀, AntivaryOn.symm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semifield β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g₁ g₂ : ι → β
hg₁ : ∀ (i : ι), i ∈ s → 0 ≤ g₁ i
hg₂ : ∀ (i : ι), i ∈ s → 0 < g₂ i
h₁ : AntivaryOn f g₁ s
h₂ : MonovaryOn f g₂ s
⊢ AntivaryOn f (g₁ / g₂) s

Tactic:
(h₁.symm.div_left₀ hg₁ hg₂ h₂.symm).symm

Premises used: MonovaryOn.symm, AntivaryOn.div_left₀, AntivaryOn.symm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semifield β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f : ι → α
g₁ g₂ : ι → β
hg₁ : 0 ≤ g₁
hg₂ : StrongLT (π := fun (i : ι) ↦ β) 0 g₂
h₁ : Monovary f g₁
h₂ : Antivary f g₂
⊢ Monovary f (g₁ / g₂)

Tactic:
(h₁.symm.div_left₀ hg₁ hg₂ h₂.symm).symm

Premises used: Monovary.div_left₀, Monovary.symm, Antivary.symm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : Semifield β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f : ι → α
g₁ g₂ : ι → β
hg₁ : 0 ≤ g₁
hg₂ : StrongLT (π := fun (i : ι) ↦ β) 0 g₂
h₁ : Antivary f g₁
h₂ : Monovary f g₂
⊢ Antivary f (g₁ / g₂)

Tactic:
(h₁.symm.div_left₀ hg₁ hg₂ h₂.symm).symm

Premises used: Monovary.symm, Antivary.div_left₀, Antivary.symm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
hg : ∀ (i : ι), i ∈ s → 0 < g i
rw : AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s
rw₁ rw₂ : MonovaryOn f g s ↔ MonovaryOn f g s
⊢ MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s

Tactic:
rw [monovaryOn_inv_left₀ hf, antivaryOn_inv_right₀ hg]

Premises used: monovaryOn_inv_left₀, antivaryOn_inv_right₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
hg : ∀ (i : ι), i ∈ s → 0 < g i
rw : MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s
rw₁ rw₂ : AntivaryOn f g s ↔ AntivaryOn f g s
⊢ AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s

Tactic:
rw [antivaryOn_inv_left₀ hf, monovaryOn_inv_right₀ hg]

Premises used: antivaryOn_inv_left₀, monovaryOn_inv_right₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
f : ι → α
g : ι → β
hf : StrongLT (π := fun (i : ι) ↦ α) 0 f
hg : StrongLT (π := fun (i : ι) ↦ β) 0 g
rw : Antivary f g⁻¹ ↔ Monovary f g
rw₁ rw₂ : Monovary f g ↔ Monovary f g
⊢ Monovary f⁻¹ g⁻¹ ↔ Monovary f g

Tactic:
rw [monovary_inv_left₀ hf, antivary_inv_right₀ hg]

Premises used: antivary_inv_right₀, monovary_inv_left₀
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
f : ι → α
g : ι → β
hf : StrongLT (π := fun (i : ι) ↦ α) 0 f
hg : StrongLT (π := fun (i : ι) ↦ β) 0 g
rw : Monovary f g⁻¹ ↔ Antivary f g
rw₁ rw₂ : Antivary f g ↔ Antivary f g
⊢ Antivary f⁻¹ g⁻¹ ↔ Antivary f g

Tactic:
rw [antivary_inv_left₀ hf, monovary_inv_right₀ hg]

Premises used: monovary_inv_right₀, antivary_inv_left₀
-- 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 ι
simp_rw :
  MonovaryOn f g s ↔
    (∀ (x : ι) (x_1 : x ∈ s) (x_2 : ι) (x_3 : x_2 ∈ s), f x < f x_2 → g x ≤ g x_2) ∧
      ∀ (x : ι) (x_1 : x ∈ s) (x_2 : ι) (x_3 : x_2 ∈ s), g x < g x_2 → f x ≤ f x_2
⊢ MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)

Tactic:
simp_rw [smul_nonneg_iff_pos_imp_nonneg, sub_pos, sub_nonneg, forall_and]

Premises used: sub_pos, smul_nonneg_iff_pos_imp_nonneg, sub_nonneg, forall_and
-- 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 ι
⊢ MonovaryOn f g s ↔
    (∀ (x : ι) (x_1 : x ∈ s) (x_2 : ι) (x_3 : x_2 ∈ s), f x < f x_2 → g x ≤ g x_2) ∧
      ∀ (x : ι) (x_1 : x ∈ s) (x_2 : ι) (x_3 : x_2 ∈ s), g x < g x_2 → f x ≤ f x_2

Tactic:
(and_iff_right_of_imp MonovaryOn.symm).symm

Premises used: MonovaryOn.symm, MonovaryOn, and_iff_right_of_imp, Iff.symm
-- 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 ι
⊢ MonovaryOn f g s ↔
    (∀ (x : ι) (x_1 : x ∈ s) (x_2 : ι) (x_3 : x_2 ∈ s), f x < f x_2 → g x ≤ g x_2) ∧
      ∀ (x : ι) (x_1 : x ∈ s) (x_2 : ι) (x_3 : x_2 ∈ s), g x < g x_2 → f x ≤ f x_2

Tactic:
exact (and_iff_right_of_imp MonovaryOn.symm).symm

Premises used: MonovaryOn.symm, and_iff_right_of_imp, Iff.symm
-- 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 →
            0 ≤
              (f j - f i) •
                HSub.hSub (α := βᵒᵈ) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)
                  (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i)) ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0
⊢ MonovaryOn (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) s ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0

Tactic:
rw [monovaryOn_iff_forall_smul_nonneg]

Premises used: monovaryOn_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 : ι → β
s : Set ι
⊢ (∀ ⦃i : ι⦄,
      i ∈ s →
        ∀ ⦃j : ι⦄,
          j ∈ s →
            0 ≤
              (f j - f i) •
                HSub.hSub (α := βᵒᵈ) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)
                  (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i)) ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (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 : ι → β
⊢ (∀ ⦃i : ι⦄,
      Membership.mem (γ := Set ι) Set.univ i →
        ∀ ⦃j : ι⦄, Membership.mem (γ := Set ι) Set.univ j → 0 ≤ (f j - f i) • (g j - g i)) ↔
    ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)

Tactic:
simp only [Set.mem_univ, forall_true_left]

Premises used: forall_true_left, Set.mem_univ