ι : 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
ι : 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
have hσinv : { x | σ⁻¹ x ≠ x } ⊆ s := (set_support_inv_eq _).subset.trans 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σ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

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

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
ι : 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
refine' (Iff.trans _ <| hfg.sum_smul_comp_perm_eq_sum_smul_iff hσinv).trans ⟨fun h ↦ _, fun h ↦ _⟩
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)
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
apply eq_iff_eq_cancel_right.2
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)
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)
rw [σ.sum_comp' s (fun i j ↦ f i • g j) hσ]
no goals
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)
congr
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 ∘ ↑σ⁻¹) ∘ ↑σ

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
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
convert h.comp_right σ
no goals
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 ∘ ↑σ⁻¹) ∘ ↑σ
rw [comp.assoc, inv_def, symm_comp_self, comp.right_id]
no goals
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
rw [σ.eq_preimage_iff_image_eq, Set.image_perm hσ]
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

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
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
convert h.comp_right σ.symm
no goals
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
rw [comp.assoc, self_comp_symm, comp.right_id]
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
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
rw [σ.symm.eq_preimage_iff_image_eq]
no goals
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
exact Set.image_perm hσinv