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

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)
ι : 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
refine' ⟨not_imp_not.1 fun h ↦ _, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm _⟩
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
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
rw [MonovaryOn] at h
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
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
push_neg at h
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
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
obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
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
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
set τ : Perm ι := (Equiv.swap x y).trans σ
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
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
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
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)
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
refine' ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' _).ne
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)

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)
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)
obtain rfl | hxy := eq_or_ne x y
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))
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)
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]
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))
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))
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)
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))
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))
simp_rw [mem_erase] at hz
no goals
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))
rw [swap_apply_of_ne_of_ne hz.2.1 hz.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
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
ι : 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
refine' (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ _)
no goals
ι : 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
obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
no goals
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)
cases lt_irrefl _ hfxy
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)
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)
convert h.sum_smul_comp_perm_le_sum_smul ((set_support_inv_eq _).subset.trans hσ) using 1
no goals
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)
simp_rw [Function.comp_apply, apply_inv_self]