ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
⊢ ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
revert hσ σ hfg
case h0
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
⊢ ∀ {σ : Perm ι}, MonovaryOn f g ↑∅ → {x | ↑σ x ≠ x} ⊆ ↑∅ → ∑ i in ∅, f i • g (↑σ i) ≤ ∑ i in ∅, f i • g i

case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
⊢ ∀ (a : ι) (s : Finset ι),
    ¬a ∈ s →
      (∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)) →
        (∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i) →
          ∀ {σ : Perm ι},
            MonovaryOn f g ↑(insert a s) →
              {x | ↑σ x ≠ x} ⊆ ↑(insert a s) → ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
⊢ ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
apply Finset.induction_on_max_value (fun i ↦ toLex (g i, f i))
  (p := fun t ↦ ∀ {σ : Perm ι}, MonovaryOn f g t → { x | σ x ≠ x } ⊆ t →
    (∑ i in t, f i • g (σ i)) ≤ ∑ i in t, f i • g i) s
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
⊢ ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
⊢ ∀ (a : ι) (s : Finset ι),
    ¬a ∈ s →
      (∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)) →
        (∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i) →
          ∀ {σ : Perm ι},
            MonovaryOn f g ↑(insert a s) →
              {x | ↑σ x ≠ x} ⊆ ↑(insert a s) → ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
intro a s has hamax hind σ hfg hσ
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
⊢ ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
⊢ ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
set τ : Perm ι := σ.trans (swap a (σ a)) with hτ
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
⊢ ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
⊢ ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
specialize hind (hfg.subset <| subset_insert _ _) hτs
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g i
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
⊢ ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
simp_rw [sum_insert has]
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g i
refine' le_trans _ (add_le_add_left hind _)
case step.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a = ↑σ a
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)

case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
obtain hσa | hσa := eq_or_ne a (σ a)
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
have h1s : σ⁻¹ a ∈ s := by
  rw [Ne.def, ← inv_eq_iff_eq] at hσa
  refine' mem_of_mem_insert_of_ne (hσ fun h ↦ hσa _) hσa
  rwa [apply_inv_self, eq_comm] at h
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + (f (↑σ⁻¹ a) • g (↑σ (↑σ⁻¹ a)) + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑σ x)) ≤
    f a • g a +
      (f (↑σ⁻¹ a) • g (↑(σ.trans (Equiv.swap a (↑σ a))) (↑σ⁻¹ a)) +
        ∑ x in erase s (↑σ⁻¹ a), f x • g (↑(σ.trans (Equiv.swap a (↑σ a))) x))
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
simp only [← s.sum_erase_add _ h1s, add_comm]
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + f (↑σ⁻¹ a) • g (↑σ (↑σ⁻¹ a)) + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑σ x) ≤
    f a • g a + f (↑σ⁻¹ a) • g (↑(σ.trans (Equiv.swap a (↑σ a))) (↑σ⁻¹ a)) +
      ∑ x in erase s (↑σ⁻¹ a), f x • g (↑(σ.trans (Equiv.swap a (↑σ a))) x)
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + (f (↑σ⁻¹ a) • g (↑σ (↑σ⁻¹ a)) + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑σ x)) ≤
    f a • g a +
      (f (↑σ⁻¹ a) • g (↑(σ.trans (Equiv.swap a (↑σ a))) (↑σ⁻¹ a)) +
        ∑ x in erase s (↑σ⁻¹ a), f x • g (↑(σ.trans (Equiv.swap a (↑σ a))) x))
rw [← add_assoc, ← add_assoc]
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + f (↑σ⁻¹ a) • g a + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑σ x) ≤
    f a • g a + f (↑σ⁻¹ a) • g (↑σ a) + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑(Equiv.swap a (↑σ a)) (↑σ x))
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + f (↑σ⁻¹ a) • g (↑σ (↑σ⁻¹ a)) + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑σ x) ≤
    f a • g a + f (↑σ⁻¹ a) • g (↑(σ.trans (Equiv.swap a (↑σ a))) (↑σ⁻¹ a)) +
      ∑ x in erase s (↑σ⁻¹ a), f x • g (↑(σ.trans (Equiv.swap a (↑σ a))) x)
simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_inv_self]
case step.inr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f (↑σ⁻¹ a) ≤ f a

case step.inr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ g (↑σ a) ≤ g a

case step.inr.refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
x : ι
hx : x ∈ erase s (↑σ⁻¹ a)
⊢ f x • g (↑σ x) = f x • g (↑(Equiv.swap a (↑σ a)) (↑σ x))
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + f (↑σ⁻¹ a) • g a + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑σ x) ≤
    f a • g a + f (↑σ⁻¹ a) • g (↑σ a) + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑(Equiv.swap a (↑σ a)) (↑σ x))
refine' add_le_add (smul_add_smul_le_smul_add_smul' _ _) (sum_congr rfl fun x hx ↦ _).le
no goals
case h0
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
⊢ ∀ {σ : Perm ι}, MonovaryOn f g ↑∅ → {x | ↑σ x ≠ x} ⊆ ↑∅ → ∑ i in ∅, f i • g (↑σ i) ≤ ∑ i in ∅, f i • g i
simp only [le_rfl, Finset.sum_empty, imp_true_iff]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
hx : x ∈ {x | ↑τ x ≠ x}
⊢ x ∈ ↑s
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
⊢ {x | ↑τ x ≠ x} ⊆ ↑s
intro x hx
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
hx : ¬(if ↑σ x = a then ↑σ a else if ↑σ x = ↑σ a then a else ↑σ x) = x
⊢ x ∈ ↑s
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
hx : x ∈ {x | ↑τ x ≠ x}
⊢ x ∈ ↑s
simp only [Ne.def, Set.mem_setOf_eq, Equiv.coe_trans, Equiv.swap_comp_apply] at hx
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ↑σ x = a
hx : ¬↑σ a = x
⊢ x ∈ ↑s

case inr.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ¬↑σ x = a
h₂ : ↑σ x = ↑σ a
hx : ¬a = x
⊢ x ∈ ↑s

case inr.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ¬↑σ x = a
h₂ : ¬↑σ x = ↑σ a
hx : ¬↑σ x = x
⊢ x ∈ ↑s
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
hx : ¬(if ↑σ x = a then ↑σ a else if ↑σ x = ↑σ a then a else ↑σ x) = x
⊢ x ∈ ↑s
split_ifs at hx with h₁ h₂
case inl.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
s : Finset ι
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
x : ι
has : ¬x ∈ s
hamax : ∀ (x_1 : ι), x_1 ∈ s → ↑toLex (g x_1, f x_1) ≤ ↑toLex (g x, f x)
hfg : MonovaryOn f g ↑(insert x s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert x s)
τ : Perm ι := σ.trans (Equiv.swap x (↑σ x))
hτ : τ = σ.trans (Equiv.swap x (↑σ x))
h₁ : ↑σ x = x
hx : ¬↑σ x = x
⊢ x ∈ ↑s

case inl.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ↑σ x = a
hx : ¬↑σ a = x
hax : x ≠ a
⊢ x ∈ ↑s
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ↑σ x = a
hx : ¬↑σ a = x
⊢ x ∈ ↑s
obtain rfl | hax := eq_or_ne x a
no goals
case inl.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
s : Finset ι
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
x : ι
has : ¬x ∈ s
hamax : ∀ (x_1 : ι), x_1 ∈ s → ↑toLex (g x_1, f x_1) ≤ ↑toLex (g x, f x)
hfg : MonovaryOn f g ↑(insert x s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert x s)
τ : Perm ι := σ.trans (Equiv.swap x (↑σ x))
hτ : τ = σ.trans (Equiv.swap x (↑σ x))
h₁ : ↑σ x = x
hx : ¬↑σ x = x
⊢ x ∈ ↑s
contradiction
no goals
case inl.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ↑σ x = a
hx : ¬↑σ a = x
hax : x ≠ a
⊢ x ∈ ↑s
exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
no goals
case inr.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ¬↑σ x = a
h₂ : ↑σ x = ↑σ a
hx : ¬a = x
⊢ x ∈ ↑s
exact (hx <| σ.injective h₂.symm).elim
no goals
case inr.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ¬↑σ x = a
h₂ : ¬↑σ x = ↑σ a
hx : ¬↑σ x = x
⊢ x ∈ ↑s
exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)
no goals
case step.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a = ↑σ a
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
rw [hτ, ← hσa, swap_self, trans_refl]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : ¬↑σ⁻¹ a = a
⊢ ↑σ⁻¹ a ∈ s
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
⊢ ↑σ⁻¹ a ∈ s
rw [Ne.def, ← inv_eq_iff_eq] at hσa
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : ¬↑σ⁻¹ a = a
h : ↑σ (↑σ⁻¹ a) = ↑σ⁻¹ a
⊢ ↑σ⁻¹ a = a
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : ¬↑σ⁻¹ a = a
⊢ ↑σ⁻¹ a ∈ s
refine' mem_of_mem_insert_of_ne (hσ fun h ↦ hσa _) hσa
no goals
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : ¬↑σ⁻¹ a = a
h : ↑σ (↑σ⁻¹ a) = ↑σ⁻¹ a
⊢ ↑σ⁻¹ a = a
rwa [apply_inv_self, eq_comm] at h
case step.inr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : ↑toLex (g (↑σ⁻¹ a), f (↑σ⁻¹ a)) ≤ ↑toLex (g a, f a)
⊢ f (↑σ⁻¹ a) ≤ f a
case step.inr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f (↑σ⁻¹ a) ≤ f a
specialize hamax (σ⁻¹ a) h1s
case step.inr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax :
  (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst < (g a, f a).fst ∨
    (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst = (g a, f a).fst ∧ (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).snd ≤ (g a, f a).snd
⊢ f (↑σ⁻¹ a) ≤ f a
case step.inr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : ↑toLex (g (↑σ⁻¹ a), f (↑σ⁻¹ a)) ≤ ↑toLex (g a, f a)
⊢ f (↑σ⁻¹ a) ≤ f a
rw [Prod.Lex.le_iff] at hamax
case step.inr.refine'_1.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst < (g a, f a).fst
⊢ f (↑σ⁻¹ a) ≤ f a

case step.inr.refine'_1.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst = (g a, f a).fst ∧ (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).snd ≤ (g a, f a).snd
⊢ f (↑σ⁻¹ a) ≤ f a
case step.inr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax :
  (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst < (g a, f a).fst ∨
    (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst = (g a, f a).fst ∧ (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).snd ≤ (g a, f a).snd
⊢ f (↑σ⁻¹ a) ≤ f a
cases' hamax with hamax hamax
no goals
case step.inr.refine'_1.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst < (g a, f a).fst
⊢ f (↑σ⁻¹ a) ≤ f a
exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax
no goals
case step.inr.refine'_1.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst = (g a, f a).fst ∧ (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).snd ≤ (g a, f a).snd
⊢ f (↑σ⁻¹ a) ≤ f a
exact hamax.2
case step.inr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : ↑toLex (g (↑σ a), f (↑σ a)) ≤ ↑toLex (g a, f a)
⊢ g (↑σ a) ≤ g a
case step.inr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ g (↑σ a) ≤ g a
specialize hamax (σ a) (mem_of_mem_insert_of_ne (hσ <| σ.injective.ne hσa.symm) hσa.symm)
case step.inr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax :
  (g (↑σ a), f (↑σ a)).fst < (g a, f a).fst ∨
    (g (↑σ a), f (↑σ a)).fst = (g a, f a).fst ∧ (g (↑σ a), f (↑σ a)).snd ≤ (g a, f a).snd
⊢ g (↑σ a) ≤ g a
case step.inr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : ↑toLex (g (↑σ a), f (↑σ a)) ≤ ↑toLex (g a, f a)
⊢ g (↑σ a) ≤ g a
rw [Prod.Lex.le_iff] at hamax
case step.inr.refine'_2.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ a), f (↑σ a)).fst < (g a, f a).fst
⊢ g (↑σ a) ≤ g a

case step.inr.refine'_2.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ a), f (↑σ a)).fst = (g a, f a).fst ∧ (g (↑σ a), f (↑σ a)).snd ≤ (g a, f a).snd
⊢ g (↑σ a) ≤ g a
case step.inr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax :
  (g (↑σ a), f (↑σ a)).fst < (g a, f a).fst ∨
    (g (↑σ a), f (↑σ a)).fst = (g a, f a).fst ∧ (g (↑σ a), f (↑σ a)).snd ≤ (g a, f a).snd
⊢ g (↑σ a) ≤ g a
cases' hamax with hamax hamax
no goals
case step.inr.refine'_2.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ a), f (↑σ a)).fst < (g a, f a).fst
⊢ g (↑σ a) ≤ g a
exact hamax.le
no goals
case step.inr.refine'_2.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ a), f (↑σ a)).fst = (g a, f a).fst ∧ (g (↑σ a), f (↑σ a)).snd ≤ (g a, f a).snd
⊢ g (↑σ a) ≤ g a
exact hamax.1.le
case step.inr.refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
x : ι
hx : ¬↑σ x = a ∧ x ∈ s
⊢ f x • g (↑σ x) = f x • g (↑(Equiv.swap a (↑σ a)) (↑σ x))
case step.inr.refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
x : ι
hx : x ∈ erase s (↑σ⁻¹ a)
⊢ f x • g (↑σ x) = f x • g (↑(Equiv.swap a (↑σ a)) (↑σ x))
rw [mem_erase, Ne.def, eq_inv_iff_eq] at hx
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
x : ι
hx : ¬↑σ x = a ∧ x ∈ s
⊢ x ≠ a
case step.inr.refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
x : ι
hx : ¬↑σ x = a ∧ x ∈ s
⊢ f x • g (↑σ x) = f x • g (↑(Equiv.swap a (↑σ a)) (↑σ x))
rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
s : Finset ι
σ : Perm ι
x : ι
has : ¬x ∈ s
hamax : ∀ (x_1 : ι), x_1 ∈ s → ↑toLex (g x_1, f x_1) ≤ ↑toLex (g x, f x)
hfg : MonovaryOn f g ↑(insert x s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert x s)
τ : Perm ι := σ.trans (Equiv.swap x (↑σ x))
hτ : τ = σ.trans (Equiv.swap x (↑σ x))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : x ≠ ↑σ x
h1s : ↑σ⁻¹ x ∈ s
hx : ¬↑σ x = x ∧ x ∈ s
⊢ False
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
x : ι
hx : ¬↑σ x = a ∧ x ∈ s
⊢ x ≠ a
rintro rfl
no goals
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
s : Finset ι
σ : Perm ι
x : ι
has : ¬x ∈ s
hamax : ∀ (x_1 : ι), x_1 ∈ s → ↑toLex (g x_1, f x_1) ≤ ↑toLex (g x, f x)
hfg : MonovaryOn f g ↑(insert x s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert x s)
τ : Perm ι := σ.trans (Equiv.swap x (↑σ x))
hτ : τ = σ.trans (Equiv.swap x (↑σ x))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : x ≠ ↑σ x
h1s : ↑σ⁻¹ x ∈ s
hx : ¬↑σ x = x ∧ x ∈ s
⊢ False
exact has hx.2