awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hxy : x ≠ y
inr :
  ∑ 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))
⊢ LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))

Tactic:
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]

Premises used: Iff.mpr, add_assoc, Ne.symm, Finset.mem_erase, Finset.sum_erase_add, And.intro, Function.comp_apply, Equiv.swap_apply_right, Finset.erase, Equiv.coe_trans, Equiv.swap_apply_left
-- 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 ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := 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))

Tactic:
add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
    (smul_add_smul_lt_smul_add_smul hfxy hgxy)

Premises used: add_lt_add_of_le_of_lt, smul_add_smul_lt_smul_add_smul, Eq.le, Finset.sum_congr, rfl
-- 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 ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hxy : x ≠ y
inr :
  ∀ (z : ι) (hz : z ∈ (s.erase x).erase y),
    f z • g ((σ : (a : ι) → ι) z) = f z • g ((σ : (a : ι) → ι) ((Equiv.swap x y : (a : ι) → ι) z : ι))
⊢ ∑ 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))

Tactic:
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)

Premises used: add_lt_add_of_le_of_lt, smul_add_smul_lt_smul_add_smul, Eq.le, Finset.sum_congr, rfl
-- 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 ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := 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
⊢ z ≠ y ∧ z ≠ x ∧ z ∈ s

Tactic:
simp_rw [mem_erase] at hz

Premises used: Finset.mem_erase
-- 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 ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := 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
inr inr₁ : f z • g ((σ : (a : ι) → ι) z) = f z • g ((σ : (a : ι) → ι) z)
⊢ f z • g ((σ : (a : ι) → ι) z) = f z • g ((σ : (a : ι) → ι) ((Equiv.swap x y : (a : ι) → ι) z : ι))

Tactic:
rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]

Premises used: Equiv.swap_apply_of_ne_of_ne, And.right, And.left
-- 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 : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    AntivaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)

Tactic:
(hfg.dual_right.sum_smul_comp_perm_eq_sum_smul_iff hσ).trans monovaryOn_toDual_right

Premises used: AntivaryOn.dual_right, monovaryOn_toDual_right, MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff, Iff.trans, OrderDual
-- 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 ι)
⊢ {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)

Tactic:
have hσinv : { x | σ⁻¹ x ≠ x } ⊆ s := (set_support_symm_eq _).subset.trans hσ
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)

Tactic:
(Iff.trans ?_ <| hfg.sum_smul_comp_perm_eq_sum_smul_iff hσinv).trans
    ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff, Iff.intro, Iff.trans
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
refine_1 :
  Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine_2 :
  ∀ (h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)), MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
refine_3 :
  ∀ (h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)), MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)

Tactic:
refine (Iff.trans ?_ <| hfg.sum_smul_comp_perm_eq_sum_smul_iff hσinv).trans
    ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff, Iff.intro, Iff.trans
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
refine_1 : Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i))
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)

Tactic:
apply eq_iff_eq_cancel_right.2

Premises used: Iff.mpr, eq_iff_eq_cancel_right
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
refine_1 :
  Eq.{u_3 + 1} (α := β) (∑ x ∈ s, f x • g ((Equiv.symm σ : (a : ι) → ι) x)) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i))
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i))

Tactic:
rw [σ.sum_comp' s (fun i j ↦ f i • g j) hσ]

Premises used: Equiv.Perm.sum_comp', HSMul.hSMul
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ x ∈ s, f x • g ((Equiv.symm σ : (a : ι) → ι) x)) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i))

Tactic:
congr
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
⊢ MonovaryOn (ι := ι) (f ∘ (⇑σ : (a : ι) → ι)) (comp (β := ι) (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (⇑σ : (a : ι) → ι))
    ((⇑σ : (a : ι) → ι) ⁻¹' (↑s : Set ι))

Tactic:
h.comp_right σ

Premises used: MonovaryOn.comp_right, DFunLike.coe
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
h₁ : g = comp (β := ι) (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (⇑σ : (a : ι) → ι)
h₂ : (↑s : Set ι) = (⇑σ : (a : ι) → ι) ⁻¹' (↑s : Set ι)
⊢ MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)

Tactic:
convert! h.comp_right σ

Premises used: MonovaryOn.comp_right, DFunLike.coe
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
h₁ : g = g ∘ comp (β := ι) (⇑σ⁻¹ : (a : ι) → ι) (⇑σ : (a : ι) → ι)
h₂ : g = g ∘ comp (β := ι) (⇑(Equiv.symm σ) : (a : ι) → ι) (⇑σ : (a : ι) → ι)
h₃ : g = g ∘ id
h₄ h₅ : g = g
⊢ g = comp (β := ι) (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (⇑σ : (a : ι) → ι)

Tactic:
rw [comp_assoc, inv_def, symm_comp_self, comp_id]

Premises used: Function.comp_id, Equiv.symm_comp_self, Equiv.Perm.inv_def, Function.comp_assoc
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
h₁ : (⇑σ : (a : ι) → ι) '' (↑s : Set ι) = (↑s : Set ι)
h₂ h₃ : (↑s : Set ι) = (↑s : Set ι)
⊢ (↑s : Set ι) = (⇑σ : (a : ι) → ι) ⁻¹' (↑s : Set ι)

Tactic:
rw [σ.eq_preimage_iff_image_eq, Set.image_perm hσ]

Premises used: Equiv.eq_preimage_iff_image_eq, Set.image_perm
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
⊢ MonovaryOn (ι := ι) (comp (β := ι) (f ∘ (⇑σ : (a : ι) → ι)) (⇑(Equiv.symm σ) : (a : ι) → ι))
    (g ∘ (⇑(Equiv.symm σ) : (a : ι) → ι)) ((⇑(Equiv.symm σ) : (a : ι) → ι) ⁻¹' (↑s : Set ι))

Tactic:
h.comp_right σ.symm

Premises used: MonovaryOn.comp_right, Equiv.symm, DFunLike.coe
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
h₁ : f = comp (β := ι) (f ∘ (⇑σ : (a : ι) → ι)) (⇑(Equiv.symm σ) : (a : ι) → ι)
h₂ : (↑s : Set ι) = (⇑(Equiv.symm σ) : (a : ι) → ι) ⁻¹' (↑s : Set ι)
⊢ MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)

Tactic:
convert! h.comp_right σ.symm

Premises used: MonovaryOn.comp_right, Equiv.symm, DFunLike.coe
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
h₁ : f = f ∘ comp (β := ι) (⇑σ : (a : ι) → ι) (⇑(Equiv.symm σ) : (a : ι) → ι)
h₂ : f = f ∘ id
h₃ h₄ : f = f
⊢ f = comp (β := ι) (f ∘ (⇑σ : (a : ι) → ι)) (⇑(Equiv.symm σ) : (a : ι) → ι)

Tactic:
rw [comp_assoc, self_comp_symm, comp_id]

Premises used: Function.comp_id, Equiv.self_comp_symm, Function.comp_assoc
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
h₁ : (⇑(Equiv.symm σ) : (a : ι) → ι) '' (↑s : Set ι) = (↑s : Set ι)
⊢ (↑s : Set ι) = (⇑(Equiv.symm σ) : (a : ι) → ι) ⁻¹' (↑s : Set ι)

Tactic:
rw [σ.symm.eq_preimage_iff_image_eq]

Premises used: Equiv.eq_preimage_iff_image_eq, Equiv.symm
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
⊢ (⇑(Equiv.symm σ) : (a : ι) → ι) '' (↑s : Set ι) = (↑s : Set ι)

Tactic:
Set.image_perm hσinv

Premises used: Set.image_perm
-- 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 ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
⊢ (⇑(Equiv.symm σ) : (a : ι) → ι) '' (↑s : Set ι) = (↑s : Set ι)

Tactic:
exact Set.image_perm hσinv

Premises used: Set.image_perm
-- 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 : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    AntivaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)

Tactic:
(hfg.dual_right.sum_comp_perm_smul_eq_sum_smul_iff hσ).trans monovaryOn_toDual_right

Premises used: AntivaryOn.dual_right, monovaryOn_toDual_right, Iff.trans, MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff, OrderDual
-- 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 α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Monovary f g
⊢ Eq.{u_3 + 1} (α := β) (∑ i : ι, f i • g ((σ : (a : ι) → ι) i)) (∑ i : ι, f i • g i) ↔
    Monovary f (g ∘ (⇑σ : (a : ι) → ι))

Tactic:
simp [(hfg.monovaryOn _).sum_smul_comp_perm_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

Premises used: Finset.mem_univ, Monovary.monovaryOn, MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff
-- 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 α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Monovary f g
⊢ Eq.{u_3 + 1} (α := β) (∑ i : ι, f ((σ : (a : ι) → ι) i) • g i) (∑ i : ι, f i • g i) ↔
    Monovary (f ∘ (⇑σ : (a : ι) → ι)) g

Tactic:
simp [(hfg.monovaryOn _).sum_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

Premises used: Finset.mem_univ, Monovary.monovaryOn, MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff
-- 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 α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Antivary f g
⊢ Eq.{u_3 + 1} (α := β) (∑ i : ι, f i • g ((σ : (a : ι) → ι) i)) (∑ i : ι, f i • g i) ↔
    Antivary f (g ∘ (⇑σ : (a : ι) → ι))

Tactic:
simp [(hfg.antivaryOn _).sum_smul_comp_perm_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

Premises used: Finset.mem_univ, AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff, Antivary.antivaryOn
-- 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 α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Antivary f g
⊢ Eq.{u_3 + 1} (α := β) (∑ i : ι, f ((σ : (a : ι) → ι) i) • g i) (∑ i : ι, f i • g i) ↔
    Antivary (f ∘ (⇑σ : (a : ι) → ι)) g

Tactic:
simp [(hfg.antivaryOn _).sum_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

Premises used: Finset.mem_univ, AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff, Antivary.antivaryOn