-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : LinearOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
refine :
  ∀ (h : ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₁ :
  ∀
    (h :
      ¬∀ ⦃i : ι⦄,
          i ∈ (↑s : Set ι) →
            ∀ ⦃j : ι⦄, j ∈ (↑s : Set ι) → (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j → f i ≤ f j),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₂ :
  ∀ (h : ∃ i ∈ (↑s : Set ι), ∃ j ∈ (↑s : Set ι), (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j ∧ f j < f i),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₃ refine₄ :
  ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
    (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₅ :
  ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
    (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
    let τ := Equiv.trans (Equiv.swap x y) σ;
    ∀ (hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
      ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₆ :
  ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
    (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
    let τ := Equiv.trans (Equiv.swap x y) σ;
    ∀ (hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
      LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
inl :
  ∀ (x : ι) (hx hy : x ∈ (↑s : Set ι)) (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) x)
    (hfxy : f x < f x),
    let τ := Equiv.trans (Equiv.swap x x) σ;
    ∀ (hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
      LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
inr inr₁ :
  ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
    (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
    let τ := Equiv.trans (Equiv.swap x y) σ;
    ∀ (hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)) (hxy : x ≠ y),
      LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
inr₂ :
  ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
    (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
    let τ := Equiv.trans (Equiv.swap x y) σ;
    ∀ (hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)) (hxy : x ≠ y),
      ∑ i ∈ (s.erase x).erase y, f i • g ((σ : (a : ι) → ι) i) +
          (f y • g ((σ : (a : ι) → ι) y) + f x • g ((σ : (a : ι) → ι) x)) <
        ∑ x_1 ∈ (s.erase x).erase y, f x_1 • g ((σ : (a : ι) → ι) ((Equiv.swap x y : (a : ι) → ι) x_1 : ι)) +
          (f y • g ((σ : (a : ι) → ι) x) + f x • g ((σ : (a : ι) → ι) y))
inr₃ :
  ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
    (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
    let τ := Equiv.trans (Equiv.swap x y) σ;
    ∀ (hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)) (hxy : x ≠ y) (z : ι) (hz : z ∈ (s.erase x).erase y),
      f z • g ((σ : (a : ι) → ι) z) = f z • g ((σ : (a : ι) → ι) ((Equiv.swap x y : (a : ι) → ι) z : ι))
inr₄ :
  ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
    (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
    let τ := Equiv.trans (Equiv.swap x y) σ;
    ∀ (hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)) (hxy : x ≠ y) (z : ι) (hz : z ≠ y ∧ z ≠ x ∧ z ∈ s),
      f z • g ((σ : (a : ι) → ι) z) = f z • g ((σ : (a : ι) → ι) ((Equiv.swap x y : (a : ι) → ι) z : ι))
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)

Tactic:
classical
  refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm <| by
    simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_symm_eq _).subset.trans hσ)⟩
  rw [MonovaryOn] at h
  push Not 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]

Premises used: add_assoc, MonovaryOn, Finset.mem_erase, Equiv.Perm, Function.comp_apply, Equiv.swap_apply_right, Equiv.coe_trans, Equiv.swap_apply_left, Not, rfl