[GOAL]
ι : 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
[PROOFSTEP]
classical
revert hσ σ hfg
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
· simp only [le_rfl, Finset.sum_empty, imp_true_iff]
intro a s has hamax hind σ hfg hσ
set τ : Perm ι := σ.trans (swap a (σ a)) with hτ
have hτs : {x | τ x ≠ x} ⊆ s := by
  intro x hx
  simp only [Ne.def, Set.mem_setOf_eq, Equiv.coe_trans, Equiv.swap_comp_apply] at hx 
  split_ifs at hx  with h₁ h₂
  · obtain rfl | hax := eq_or_ne x a
    · contradiction
    · exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
  · exact (hx <| σ.injective h₂.symm).elim
  · exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)
specialize hind (hfg.subset <| subset_insert _ _) hτs
simp_rw [sum_insert has]
refine' le_trans _ (add_le_add_left hind _)
obtain hσa | hσa := eq_or_ne a (σ a)
· rw [hτ, ← hσa, swap_self, trans_refl]
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 
simp only [← s.sum_erase_add _ h1s, add_comm]
rw [← add_assoc, ← add_assoc]
simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_inv_self]
refine' add_le_add (smul_add_smul_le_smul_add_smul' _ _) (sum_congr rfl fun x hx ↦ _).le
· specialize hamax (σ⁻¹ a) h1s
  rw [Prod.Lex.le_iff] at hamax 
  cases' hamax with hamax hamax
  · exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax
  · exact hamax.2
· specialize hamax (σ a) (mem_of_mem_insert_of_ne (hσ <| σ.injective.ne hσa.symm) hσa.symm)
  rw [Prod.Lex.le_iff] at hamax 
  cases' hamax with hamax hamax
  · exact hamax.le
  · exact hamax.1.le
· rw [mem_erase, Ne.def, eq_inv_iff_eq] at hx 
  rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]
  rintro rfl
  exact has hx.2
[GOAL]
ι : 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
[PROOFSTEP]
revert hσ σ hfg
[GOAL]
ι : 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
[PROOFSTEP]
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
[GOAL]
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
[PROOFSTEP]
simp only [le_rfl, Finset.sum_empty, imp_true_iff]
[GOAL]
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
[PROOFSTEP]
intro a s has hamax hind σ hfg hσ
[GOAL]
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
[PROOFSTEP]
set τ : Perm ι := σ.trans (swap a (σ a)) with hτ
[GOAL]
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
[PROOFSTEP]
have hτs : {x | τ x ≠ x} ⊆ s := by
  intro x hx
  simp only [Ne.def, Set.mem_setOf_eq, Equiv.coe_trans, Equiv.swap_comp_apply] at hx 
  split_ifs at hx  with h₁ h₂
  · obtain rfl | hax := eq_or_ne x a
    · contradiction
    · exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
  · exact (hx <| σ.injective h₂.symm).elim
  · exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)
[GOAL]
ι : 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
[PROOFSTEP]
intro x hx
[GOAL]
ι : 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
[PROOFSTEP]
simp only [Ne.def, Set.mem_setOf_eq, Equiv.coe_trans, Equiv.swap_comp_apply] at hx 
[GOAL]
ι : 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
[PROOFSTEP]
split_ifs at hx  with h₁ h₂
[GOAL]
case pos
ι : 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
[PROOFSTEP]
obtain rfl | hax := eq_or_ne x a
[GOAL]
case pos.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
[PROOFSTEP]
contradiction
[GOAL]
case pos.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
[PROOFSTEP]
exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
[GOAL]
case pos
ι : 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
[PROOFSTEP]
exact (hx <| σ.injective h₂.symm).elim
[GOAL]
case neg
ι : 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
[PROOFSTEP]
exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)
[GOAL]
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
[PROOFSTEP]
specialize hind (hfg.subset <| subset_insert _ _) hτs
[GOAL]
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
[PROOFSTEP]
simp_rw [sum_insert has]
[GOAL]
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
[PROOFSTEP]
refine' le_trans _ (add_le_add_left hind _)
[GOAL]
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)
[PROOFSTEP]
obtain hσa | hσa := eq_or_ne a (σ a)
[GOAL]
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)
[PROOFSTEP]
rw [hτ, ← hσa, swap_self, trans_refl]
[GOAL]
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)
[PROOFSTEP]
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 
[GOAL]
ι : 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
[PROOFSTEP]
rw [Ne.def, ← inv_eq_iff_eq] at hσa 
[GOAL]
ι : 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
[PROOFSTEP]
refine' mem_of_mem_insert_of_ne (hσ fun h ↦ hσa _) hσa
[GOAL]
ι : 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
[PROOFSTEP]
rwa [apply_inv_self, eq_comm] at h 
[GOAL]
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)
[PROOFSTEP]
simp only [← s.sum_erase_add _ h1s, add_comm]
[GOAL]
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))
[PROOFSTEP]
rw [← add_assoc, ← add_assoc]
[GOAL]
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)
[PROOFSTEP]
simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_inv_self]
[GOAL]
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))
[PROOFSTEP]
refine' add_le_add (smul_add_smul_le_smul_add_smul' _ _) (sum_congr rfl fun x hx ↦ _).le
[GOAL]
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
[PROOFSTEP]
specialize hamax (σ⁻¹ a) h1s
[GOAL]
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
[PROOFSTEP]
rw [Prod.Lex.le_iff] at hamax 
[GOAL]
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
[PROOFSTEP]
cases' hamax with hamax hamax
[GOAL]
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
[PROOFSTEP]
exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax
[GOAL]
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
[PROOFSTEP]
exact hamax.2
[GOAL]
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
[PROOFSTEP]
specialize hamax (σ a) (mem_of_mem_insert_of_ne (hσ <| σ.injective.ne hσa.symm) hσa.symm)
[GOAL]
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
[PROOFSTEP]
rw [Prod.Lex.le_iff] at hamax 
[GOAL]
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
[PROOFSTEP]
cases' hamax with hamax hamax
[GOAL]
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
[PROOFSTEP]
exact hamax.le
[GOAL]
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
[PROOFSTEP]
exact hamax.1.le
[GOAL]
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))
[PROOFSTEP]
rw [mem_erase, Ne.def, eq_inv_iff_eq] at hx 
[GOAL]
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))
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]
[GOAL]
ι : 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
[PROOFSTEP]
rintro rfl
[GOAL]
ι : 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
[PROOFSTEP]
exact has hx.2
[GOAL]
ι : 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 ↔ MonovaryOn f (g ∘ ↑σ) ↑s
[PROOFSTEP]
classical
refine' ⟨not_imp_not.1 fun h ↦ _, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm _⟩
· rw [MonovaryOn] at h 
  push_neg at h 
  obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
  set τ : Perm ι := (Equiv.swap x y).trans σ
  have hτs : {x | τ x ≠ x} ⊆ s :=
    by
    refine' (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ _)
    obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
  refine' ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' _).ne
  obtain rfl | hxy := eq_or_ne x y
  · cases lt_irrefl _ hfxy
  simp only [← s.sum_erase_add _ hx, ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩), add_assoc,
    Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
  refine' add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ _).le (smul_add_smul_lt_smul_add_smul hfxy hgxy)
  simp_rw [mem_erase] at hz 
  rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
· convert h.sum_smul_comp_perm_le_sum_smul ((set_support_inv_eq _).subset.trans hσ) using 1
  simp_rw [Function.comp_apply, apply_inv_self]
[GOAL]
ι : 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 ↔ MonovaryOn f (g ∘ ↑σ) ↑s
[PROOFSTEP]
refine' ⟨not_imp_not.1 fun h ↦ _, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm _⟩
[GOAL]
case refine'_1
ι : 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
h : ¬MonovaryOn f (g ∘ ↑σ) ↑s
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
rw [MonovaryOn] at h 
[GOAL]
case refine'_1
ι : 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
h : ¬∀ ⦃i : ι⦄, i ∈ ↑s → ∀ ⦃j : ι⦄, j ∈ ↑s → (g ∘ ↑σ) i < (g ∘ ↑σ) j → f i ≤ f j
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
push_neg at h 
[GOAL]
case refine'_1
ι : 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
h : Exists fun ⦃i⦄ => i ∈ ↑s ∧ Exists fun ⦃j⦄ => j ∈ ↑s ∧ (g ∘ ↑σ) i < (g ∘ ↑σ) j ∧ f j < f i
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
set τ : Perm ι := (Equiv.swap x y).trans σ
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
have hτs : {x | τ x ≠ x} ⊆ s :=
  by
  refine' (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ _)
  obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
[GOAL]
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
⊢ {x | ↑τ x ≠ x} ⊆ ↑s
[PROOFSTEP]
refine' (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ _)
[GOAL]
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
z : ι
hz : z ∈ {x_1 | ↑(Equiv.swap x y) x_1 ≠ x_1}
⊢ z ∈ ↑s
[PROOFSTEP]
obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz
[GOAL]
case intro.inl
ι : 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
y : ι
hy : y ∈ ↑s
z : ι
hx : z ∈ ↑s
hgxy : (g ∘ ↑σ) z < (g ∘ ↑σ) y
hfxy : f y < f z
τ : Perm ι := (Equiv.swap z y).trans σ
hz : z ∈ {x | ↑(Equiv.swap z y) x ≠ x}
left✝ : z ≠ y
⊢ z ∈ ↑s
[PROOFSTEP]
assumption
[GOAL]
case intro.inr
ι : 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
x : ι
hx : x ∈ ↑s
z : ι
hy : z ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) z
hfxy : f z < f x
τ : Perm ι := (Equiv.swap x z).trans σ
hz : z ∈ {x_1 | ↑(Equiv.swap x z) x_1 ≠ x_1}
left✝ : x ≠ z
⊢ z ∈ ↑s
[PROOFSTEP]
assumption
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
refine' ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' _).ne
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g (↑σ i) < ∑ i in s, f i • g (↑τ i)
[PROOFSTEP]
obtain rfl | hxy := eq_or_ne x y
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inl
ι : 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
x : ι
hx hy : x ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) x
hfxy : f x < f x
τ : Perm ι := (Equiv.swap x x).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g (↑σ i) < ∑ i in s, f i • g (↑τ i)
[PROOFSTEP]
cases lt_irrefl _ hfxy
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inr
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
⊢ ∑ i in s, f i • g (↑σ i) < ∑ i in s, f i • g (↑τ i)
[PROOFSTEP]
simp only [← s.sum_erase_add _ hx, ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩), add_assoc,
  Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inr
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
⊢ ∑ x in erase (erase s x) y, f x • g (↑σ x) + (f y • g (↑σ y) + f x • g (↑σ x)) <
    ∑ x_1 in erase (erase s x) y, f x_1 • g (↑σ (↑(Equiv.swap x y) x_1)) + (f y • g (↑σ x) + f x • g (↑σ y))
[PROOFSTEP]
refine' add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ _).le (smul_add_smul_lt_smul_add_smul hfxy hgxy)
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inr
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
z : ι
hz : z ∈ erase (erase s x) y
⊢ f z • g (↑σ z) = f z • g (↑σ (↑(Equiv.swap x y) z))
[PROOFSTEP]
simp_rw [mem_erase] at hz 
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inr
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
z : ι
hz : z ≠ y ∧ z ≠ x ∧ z ∈ s
⊢ f z • g (↑σ z) = f z • g (↑σ (↑(Equiv.swap x y) z))
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
[GOAL]
case refine'_2
ι : 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
h : MonovaryOn f (g ∘ ↑σ) ↑s
⊢ ∑ i in s, f i • g i ≤ ∑ i in s, f i • g (↑σ i)
[PROOFSTEP]
convert h.sum_smul_comp_perm_le_sum_smul ((set_support_inv_eq _).subset.trans hσ) using 1
[GOAL]
case h.e'_3
ι : 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
h : MonovaryOn f (g ∘ ↑σ) ↑s
⊢ ∑ i in s, f i • g i = ∑ i in s, f i • (g ∘ ↑σ) (↑σ⁻¹ i)
[PROOFSTEP]
simp_rw [Function.comp_apply, apply_inv_self]
[GOAL]
ι : 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 ↔ ¬MonovaryOn f (g ∘ ↑σ) ↑s
[PROOFSTEP]
simp [← hfg.sum_smul_comp_perm_eq_sum_smul_iff hσ, lt_iff_le_and_ne, hfg.sum_smul_comp_perm_le_sum_smul hσ]
[GOAL]
ι : 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
[PROOFSTEP]
convert hfg.sum_smul_comp_perm_le_sum_smul (show {x | σ⁻¹ x ≠ x} ⊆ s by simp only [set_support_inv_eq, hσ]) using 1
[GOAL]
ι : 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
⊢ {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
[PROOFSTEP]
simp only [set_support_inv_eq, hσ]
[GOAL]
case h.e'_3
ι : 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)
[PROOFSTEP]
exact σ.sum_comp' s (fun i j ↦ f i • g j) hσ
[GOAL]
ι : 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 ↔ MonovaryOn (f ∘ ↑σ) g ↑s
[PROOFSTEP]
have hσinv : {x | σ⁻¹ x ≠ x} ⊆ s := (set_support_inv_eq _).subset.trans hσ
[GOAL]
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f (↑σ i) • g i = ∑ i in s, f i • g i ↔ MonovaryOn (f ∘ ↑σ) g ↑s
[PROOFSTEP]
refine' (Iff.trans _ <| hfg.sum_smul_comp_perm_eq_sum_smul_iff hσinv).trans ⟨fun h ↦ _, fun h ↦ _⟩
[GOAL]
case refine'_1
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f (↑σ i) • g i = ∑ i in s, f i • g i ↔ ∑ i in s, f i • g (↑σ⁻¹ i) = ∑ i in s, f i • g i
[PROOFSTEP]
apply eq_iff_eq_cancel_right.2
[GOAL]
case refine'_1.a
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f (↑σ i) • g i = ∑ i in s, f i • g (↑σ⁻¹ i)
[PROOFSTEP]
rw [σ.sum_comp' s (fun i j ↦ f i • g j) hσ]
[GOAL]
case refine'_1.a
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ x in s, f x • g (↑σ.symm x) = ∑ i in s, f i • g (↑σ⁻¹ i)
[PROOFSTEP]
congr
[GOAL]
case refine'_2
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ↑σ⁻¹) ↑s
⊢ MonovaryOn (f ∘ ↑σ) g ↑s
[PROOFSTEP]
convert h.comp_right σ
[GOAL]
case h.e'_7
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ↑σ⁻¹) ↑s
⊢ g = (g ∘ ↑σ⁻¹) ∘ ↑σ
[PROOFSTEP]
rw [comp.assoc, inv_def, symm_comp_self, comp.right_id]
[GOAL]
case h.e'_8
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ↑σ⁻¹) ↑s
⊢ ↑s = ↑σ ⁻¹' ↑s
[PROOFSTEP]
rw [σ.eq_preimage_iff_image_eq, Set.image_perm hσ]
[GOAL]
case refine'_3
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ↑σ) g ↑s
⊢ MonovaryOn f (g ∘ ↑σ⁻¹) ↑s
[PROOFSTEP]
convert h.comp_right σ.symm
[GOAL]
case h.e'_6
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ↑σ) g ↑s
⊢ f = (f ∘ ↑σ) ∘ ↑σ.symm
[PROOFSTEP]
rw [comp.assoc, self_comp_symm, comp.right_id]
[GOAL]
case h.e'_8
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ↑σ) g ↑s
⊢ ↑s = ↑σ.symm ⁻¹' ↑s
[PROOFSTEP]
rw [σ.symm.eq_preimage_iff_image_eq]
[GOAL]
case h.e'_8
ι : 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
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ↑σ) g ↑s
⊢ ↑σ.symm '' ↑s = ↑s
[PROOFSTEP]
exact Set.image_perm hσinv
[GOAL]
ι : 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 ↔ ¬MonovaryOn (f ∘ ↑σ) g ↑s
[PROOFSTEP]
simp [← hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ, lt_iff_le_and_ne, hfg.sum_comp_perm_smul_le_sum_smul hσ]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g i < ∑ i in s, f i • g (↑σ i) ↔ ¬AntivaryOn f (g ∘ ↑σ) ↑s
[PROOFSTEP]
simp [← hfg.sum_smul_eq_sum_smul_comp_perm_iff hσ, lt_iff_le_and_ne, eq_comm, hfg.sum_smul_le_sum_smul_comp_perm hσ]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g i < ∑ i in s, f (↑σ i) • g i ↔ ¬AntivaryOn (f ∘ ↑σ) g ↑s
[PROOFSTEP]
simp [← hfg.sum_smul_eq_sum_comp_perm_smul_iff hσ, eq_comm, lt_iff_le_and_ne, hfg.sum_smul_le_sum_comp_perm_smul hσ]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f i • g (↑σ i) = ∑ i : ι, f i • g i ↔ Monovary f (g ∘ ↑σ)
[PROOFSTEP]
simp [(hfg.monovaryOn _).sum_smul_comp_perm_eq_sum_smul_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f i • g (↑σ i) < ∑ i : ι, f i • g i ↔ ¬Monovary f (g ∘ ↑σ)
[PROOFSTEP]
simp [(hfg.monovaryOn _).sum_smul_comp_perm_lt_sum_smul_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f (↑σ i) • g i = ∑ i : ι, f i • g i ↔ Monovary (f ∘ ↑σ) g
[PROOFSTEP]
simp [(hfg.monovaryOn _).sum_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f (↑σ i) • g i < ∑ i : ι, f i • g i ↔ ¬Monovary (f ∘ ↑σ) g
[PROOFSTEP]
simp [(hfg.monovaryOn _).sum_comp_perm_smul_lt_sum_smul_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f i • g (↑σ i) = ∑ i : ι, f i • g i ↔ Antivary f (g ∘ ↑σ)
[PROOFSTEP]
simp [(hfg.antivaryOn _).sum_smul_eq_sum_smul_comp_perm_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f i • g i < ∑ i : ι, f i • g (↑σ i) ↔ ¬Antivary f (g ∘ ↑σ)
[PROOFSTEP]
simp [(hfg.antivaryOn _).sum_smul_lt_sum_smul_comp_perm_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f (↑σ i) • g i = ∑ i : ι, f i • g i ↔ Antivary (f ∘ ↑σ) g
[PROOFSTEP]
simp [(hfg.antivaryOn _).sum_smul_eq_sum_comp_perm_smul_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f i • g i < ∑ i : ι, f (↑σ i) • g i ↔ ¬Antivary (f ∘ ↑σ) g
[PROOFSTEP]
simp [(hfg.antivaryOn _).sum_smul_lt_sum_comp_perm_smul_iff fun _ _ ↦ mem_univ _]
