awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
change :
  (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹) -
      (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹))).LimZero
⊢ (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹) -
      (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹))).LimZero

Tactic:
change LimZero
                (inv f hf - const abv (lim f) * (inv f hf * const abv (lim f)⁻¹) -
                  (const abv (lim f)⁻¹ - f * (inv f hf * const abv (lim f)⁻¹)))

Premises used: HMul.hMul, CauSeq.inv, HSub.hSub, Inv.inv, CauSeq.lim, CauSeq.const, CauSeq.LimZero
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
rw : (f.inv hf - HMul.hMul (α := CauSeq β abv) (const abv f.lim) (inv (const abv f.lim) ⋯) * f.inv hf).LimZero
⊢ (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹)).LimZero

Tactic:
rw [← mul_assoc, mul_right_comm, const_inv hl]

Premises used: mul_assoc, mul_right_comm, CauSeq.const_inv
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - HMul.hMul (α := CauSeq β abv) (const abv f.lim) (inv (const abv f.lim) ⋯) * f.inv hf).LimZero

Tactic:
h₁ _ _ _
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - HMul.hMul (α := CauSeq β abv) (const abv f.lim) (inv (const abv f.lim) ⋯) * f.inv hf).LimZero

Tactic:
exact h₁ _ _ _
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
rw : (const abv f.lim⁻¹ - f * f.inv hf * const abv f.lim⁻¹).LimZero
⊢ (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹)).LimZero

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (const abv f.lim⁻¹ - f * f.inv hf * const abv f.lim⁻¹).LimZero

Tactic:
h₁ _ _ _
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (const abv f.lim⁻¹ - f * f.inv hf * const abv f.lim⁻¹).LimZero

Tactic:
exact h₁ _ _ _
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹) -
      (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹))).LimZero

Tactic:
exact sub_limZero
                (by rw [← mul_assoc, mul_right_comm, const_inv hl]; exact h₁ _ _ _)
                (by rw [← mul_assoc]; exact h₁ _ _ _)

Premises used: CauSeq.sub_limZero
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : IsComplete α abs
f : CauSeq α abs
x : α
h : f ≤ const abs x
⊢ f.lim ≤ x

Tactic:
CauSeq.const_le.1 <| CauSeq.le_of_eq_of_le (Setoid.symm (equiv_lim f)) h

Premises used: CauSeq.equiv_lim, CauSeq.const_le, Setoid.symm, Iff.mp, CauSeq.le_of_eq_of_le
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : IsComplete α abs
f : CauSeq α abs
x : α
h : const abs x ≤ f
⊢ x ≤ f.lim

Tactic:
CauSeq.const_le.1 <| CauSeq.le_of_le_of_eq h (equiv_lim f)

Premises used: CauSeq.equiv_lim, CauSeq.const_le, Iff.mp, CauSeq.le_of_le_of_eq
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : IsComplete α abs
f : CauSeq α abs
x : α
h : const abs x < f
⊢ x < f.lim

Tactic:
CauSeq.const_lt.1 <| CauSeq.lt_of_lt_of_eq h (equiv_lim f)

Premises used: CauSeq.const_lt, CauSeq.equiv_lim, Iff.mp, CauSeq.lt_of_lt_of_eq
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : IsComplete α abs
f : CauSeq α abs
x : α
h : f < const abs x
⊢ f.lim < x

Tactic:
CauSeq.const_lt.1 <| CauSeq.lt_of_eq_of_lt (Setoid.symm (equiv_lim f)) h

Premises used: CauSeq.const_lt, CauSeq.lt_of_eq_of_lt, CauSeq.equiv_lim, Setoid.symm, Iff.mp
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : LinearOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
obtain :
  ∀ (σ : Perm ι) (hσ : σ.IsCycleOn (↑s : Set ι)) (hs : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤
      HSMul.hSMul (β := β) (#s) (∑ i ∈ s, f i • g i)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤
    HSMul.hSMul (β := β) (#s) (∑ i ∈ s, f i • g i)

Tactic:
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn

Premises used: Set.Countable.exists_cycleOn, Finset.countable_toSet
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : LinearOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
σ : Perm ι
hσ : σ.IsCycleOn (↑s : Set ι)
hs : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
rw :
  ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i) ≤ HSMul.hSMul (β := β) (#(range #s)) (∑ i ∈ s, f i • g i)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤
    HSMul.hSMul (β := β) (#s) (∑ i ∈ s, f i • g i)

Tactic:
rw [← card_range #s, sum_smul_sum_eq_sum_perm hσ]

Premises used: Finset.card_range, Finset.sum_smul_sum_eq_sum_perm, Finset.card
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : LinearOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
σ : Perm ι
hσ : σ.IsCycleOn (↑s : Set ι)
hs : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i) ≤ HSMul.hSMul (β := β) (#(range #s)) (∑ i ∈ s, f i • g i)

Tactic:
sum_le_card_nsmul _ _ _ fun n _ ↦
    hfg.sum_smul_comp_perm_le_sum_smul fun x hx ↦ hs fun h ↦ hx <| IsFixedPt.perm_pow h _

Premises used: MonovaryOn.sum_smul_comp_perm_le_sum_smul, Function.IsFixedPt.perm_pow, Finset.sum_le_card_nsmul
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : LinearOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
σ : Perm ι
hσ : σ.IsCycleOn (↑s : Set ι)
hs : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i) ≤ HSMul.hSMul (β := β) (#(range #s)) (∑ i ∈ s, f i • g i)

Tactic:
exact sum_le_card_nsmul _ _ _ fun n _ ↦
    hfg.sum_smul_comp_perm_le_sum_smul fun x hx ↦ hs fun h ↦ hx <| IsFixedPt.perm_pow h _

Premises used: MonovaryOn.sum_smul_comp_perm_le_sum_smul, Function.IsFixedPt.perm_pow, Finset.sum_le_card_nsmul
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : LinearOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
obtain :
  ∀ (σ : Perm ι) (hσ : σ.IsCycleOn (↑s : Set ι)) (hs : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤
      HSMul.hSMul (β := β) (#s) (∑ i ∈ s, f i • g i)
obtain₁ :
  ∀ (σ : Perm ι) (hσ : σ.IsCycleOn (↑s : Set ι)) (hs : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i) ≤ HSMul.hSMul (β := β) (#(range #s)) (∑ i ∈ s, f i • g i)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤
    HSMul.hSMul (β := β) (#s) (∑ i ∈ s, f i • g i)

Tactic:
classical
  obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
  rw [← card_range #s, sum_smul_sum_eq_sum_perm hσ]
  exact sum_le_card_nsmul _ _ _ fun n _ ↦
    hfg.sum_smul_comp_perm_le_sum_smul fun x hx ↦ hs fun h ↦ hx <| IsFixedPt.perm_pow h _

Premises used: Set.Countable.exists_cycleOn, Finset.card_range, Finset.card, Finset.countable_toSet
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : LinearOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g (↑s : Set ι)
⊢ HSMul.hSMul (β := β) (#s) (∑ i ∈ s, f i • g i) ≤
    HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i ∈ s, f i) (∑ i ∈ s, g i)

Tactic:
hfg.dual_right.sum_smul_sum_le_card_smul_sum

Premises used: AntivaryOn.dual_right, MonovaryOn.sum_smul_sum_le_card_smul_sum, OrderDual
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : LinearOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Monovary f g
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i : ι, f i) (∑ i : ι, g i) ≤
    HSMul.hSMul (β := β) (Fintype.card ι) (∑ i : ι, f i • g i)

Tactic:
(hfg.monovaryOn _).sum_smul_sum_le_card_smul_sum

Premises used: Monovary.monovaryOn, Fintype.card, MonovaryOn.sum_smul_sum_le_card_smul_sum
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : LinearOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Antivary f g
⊢ HSMul.hSMul (β := β) (Fintype.card ι) (∑ i : ι, f i • g i) ≤
    HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i : ι, f i) (∑ i : ι, g i)

Tactic:
(hfg.dual_right.monovaryOn _).sum_smul_sum_le_card_smul_sum

Premises used: Monovary.monovaryOn, Fintype.card, MonovaryOn.sum_smul_sum_le_card_smul_sum, Antivary.dual_right, OrderDual
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : MonovaryOn f g (↑s : Set ι)
rw : HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤ HSMul.hSMul (β := α) (#s) (∑ i ∈ s, f i * g i)
⊢ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i * g i)

Tactic:
rw [← nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : MonovaryOn f g (↑s : Set ι)
⊢ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤ HSMul.hSMul (β := α) (#s) (∑ i ∈ s, f i * g i)

Tactic:
hfg.sum_smul_sum_le_card_smul_sum

Premises used: MonovaryOn.sum_smul_sum_le_card_smul_sum
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : MonovaryOn f g (↑s : Set ι)
⊢ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤ HSMul.hSMul (β := α) (#s) (∑ i ∈ s, f i * g i)

Tactic:
exact hfg.sum_smul_sum_le_card_smul_sum

Premises used: MonovaryOn.sum_smul_sum_le_card_smul_sum
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g (↑s : Set ι)
rw : HSMul.hSMul (β := α) (#s) (∑ i ∈ s, f i * g i) ≤ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
⊢ HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i * g i) ≤ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i)

Tactic:
rw [← nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g (↑s : Set ι)
⊢ HSMul.hSMul (β := α) (#s) (∑ i ∈ s, f i * g i) ≤ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i)

Tactic:
hfg.card_smul_sum_le_sum_smul_sum

Premises used: AntivaryOn.card_smul_sum_le_sum_smul_sum
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g (↑s : Set ι)
⊢ HSMul.hSMul (β := α) (#s) (∑ i ∈ s, f i * g i) ≤ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i)

Tactic:
exact hfg.card_smul_sum_le_sum_smul_sum

Premises used: AntivaryOn.card_smul_sum_le_sum_smul_sum
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (HAdd.hAdd (α := ℕ) 0 1) ≤
    HPow.hPow (α := α) (β := ℕ) (↑(#s) : α) 0 * ∑ i ∈ s, f i ^ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
rw rw₁ :
  HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) * ∑ i ∈ s, f i = HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) * ∑ i ∈ s, f i
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1 + 1) = HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) * ∑ i ∈ s, f i

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
ha : LE.le.{u_2} (α := α) 0 (∑ i ∈ s, f i)
hbc : HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) ≤ HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) * ∑ i ∈ s, f i ≤
    (HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ LE.le.{u_2} (α := α) 0 (∑ i ∈ s, f i)

Tactic:
sum_nonneg hf

Premises used: Finset.sum_nonneg
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) ≤ HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)

Tactic:
pow_sum_le_card_mul_sum_pow hf _
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ LE.le.{u_2} (α := α) 0 (∑ i ∈ s, f i)

Tactic:
exacts [sum_nonneg hf, pow_sum_le_card_mul_sum_pow hf _]

Premises used: Finset.sum_nonneg
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
rw rw₁ :
  HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i) =
    HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i)
⊢ (HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i =
    HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hbc :
  HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i) ≤
    HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i ^ (n + 1) * f i)
⊢ HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i) ≤
    HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i ^ (n + 1) * f i)

Tactic:
gcongr _ * ?_
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i) ≤
    HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i ^ (n + 1) * f i)

Tactic:
((monovaryOn_self ..).pow_left₀ hf _).sum_mul_sum_le_card_mul_sum

Premises used: monovaryOn_self, MonovaryOn.sum_mul_sum_le_card_mul_sum, MonovaryOn.pow_left₀
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i) ≤
    HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i ^ (n + 1) * f i)

Tactic:
exact ((monovaryOn_self ..).pow_left₀ hf _).sum_mul_sum_le_card_mul_sum

Premises used: monovaryOn_self, MonovaryOn.sum_mul_sum_le_card_mul_sum, MonovaryOn.pow_left₀
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
simp_rw :
  HPow.hPow (α := α) (↑(#s) : α) n * (↑(#s) : α) * ∑ i ∈ s, f i ^ (n + 1) * f i =
    HPow.hPow (α := α) (↑(#s) : α) (n + 1) * ∑ i ∈ s, f i ^ (n + 1 + 1)
⊢ HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i ^ (n + 1) * f i) =
    HPow.hPow (α := α) (↑(#s) : α) (n + 1) * ∑ i ∈ s, f i ^ (n + 1 + 1)

Tactic:
simp_rw [← mul_assoc, ← pow_succ]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
simp_rw : HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, f i) ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ x ∈ s, f x * f x)
⊢ HPow.hPow (α := α) (β := ℕ) (∑ i ∈ s, f i) 2 ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2)

Tactic:
simp_rw [sq]

Premises used: sq
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
⊢ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, f i) ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ x ∈ s, f x * f x)

Tactic:
(monovaryOn_self _ _).sum_mul_sum_le_card_mul_sum

Premises used: monovaryOn_self, MonovaryOn.sum_mul_sum_le_card_mul_sum
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
⊢ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, f i) ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ x ∈ s, f x * f x)

Tactic:
exact (monovaryOn_self _ _).sum_mul_sum_le_card_mul_sum

Premises used: monovaryOn_self, MonovaryOn.sum_mul_sum_le_card_mul_sum
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
f g : ι → α
inst_4 : Fintype ι
hfg : Monovary f g
⊢ HMul.hMul (α := α) (∑ i : ι, f i) (∑ i : ι, g i) ≤ HMul.hMul (α := α) (↑(Fintype.card ι) : α) (∑ i : ι, f i * g i)

Tactic:
(hfg.monovaryOn _).sum_mul_sum_le_card_mul_sum

Premises used: Monovary.monovaryOn, MonovaryOn.sum_mul_sum_le_card_mul_sum, Fintype.card
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
f g : ι → α
inst_4 : Fintype ι
hfg : Antivary f g
⊢ HMul.hMul (α := α) (↑(Fintype.card ι) : α) (∑ i : ι, f i * g i) ≤ HMul.hMul (α := α) (∑ i : ι, f i) (∑ i : ι, g i)

Tactic:
(hfg.antivaryOn _).card_mul_sum_le_sum_mul_sum

Premises used: Fintype.card, AntivaryOn.card_mul_sum_le_sum_mul_sum, Antivary.antivaryOn
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
inl :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ f i),
    HPow.hPow (α := α) (∑ i ∈ ∅, f i) (n + 1) / HPow.hPow (α := α) (↑(card.{u_1} (α := ι) ∅) : α) n ≤
      ∑ i ∈ ∅, f i ^ (n + 1)
inr :
  ∀ (hs : s.Nonempty),
    HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) / HPow.hPow (α := α) (↑(#s) : α) n ≤ ∑ i ∈ s, f i ^ (n + 1)
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) / HPow.hPow (α := α) (↑(#s) : α) n ≤ ∑ i ∈ s, f i ^ (n + 1)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty