-- Mathlib/Algebra/Order/Rearrangement.lean
theorem MonovaryOn.sum_smul_comp_perm_le_sum_smul (hfg : MonovaryOn f g s)
    (hσ : {x | σ x ≠ x} ⊆ s) : ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i

Proof state:
case step.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ 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 ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hσa : a = σ a
⊢ f a • g (σ a) + ∑ i ∈ s, f i • g (σ i) ≤ f a • g a + ∑ i ∈ s, f i • g (τ i)

Tactic:
rw [hτ, ← hσa, swap_self, trans_refl]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i

Tactic:
revert hσ σ hfg

Result:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
⊢ ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i

Proof state:
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ 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 ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hσa : a ≠ σ a
⊢ f a • g (σ a) + ∑ i ∈ s, f i • g (σ i) ≤ f a • g a + ∑ i ∈ s, f i • g (τ i)

Tactic:
have h1s : σ⁻¹ a ∈ s := by
  rw [Ne, ← 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

Result:
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ 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 ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hσa : a ≠ σ a
h1s : σ⁻¹ a ∈ s
⊢ f a • g (σ a) + ∑ i ∈ s, f i • g (σ i) ≤ f a • g a + ∑ i ∈ s, f i • g (τ i)

Proof state:
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
x : ι
h₁ : ¬σ x = a
h₂ : σ x = σ a
hx : ¬a = x
⊢ x ∈ ↑s

Tactic:
exact (hx <| σ.injective h₂.symm).elim

Result:
no goals

Proof state:
case step.inr.refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ 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 ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ 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))

Tactic:
rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]

Result:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ 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 ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hσa : a ≠ σ a
h1s : σ⁻¹ a ∈ s
x : ι
hx : ¬σ x = a ∧ x ∈ s
⊢ x ≠ a