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 : PosSMulMono α β
f : ι → α
g : ι → β
s : Finset ι
σ : Perm ι
x : ι
has : x ∉ s
hamax :
  ∀ x_1 ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x_1, f x_1) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
hfg : MonovaryOn f g (↑(insert x s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert x s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap x ((σ : (a : ι) → ι) x))
hτ : τ = Equiv.trans σ (Equiv.swap x ((σ : (a : ι) → ι) x))
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hind : LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
hσa : x ≠ (σ : (a : ι) → ι) x
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) x : ι)
hx : ¬(σ : (a : ι) → ι) x = x ∧ x ∈ s
⊢ False

Tactic:
has hx.2

Premises used: And.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 : PosSMulMono α β
f : ι → α
g : ι → β
s : Finset ι
σ : Perm ι
x : ι
has : x ∉ s
hamax :
  ∀ x_1 ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x_1, f x_1) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
hfg : MonovaryOn f g (↑(insert x s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert x s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap x ((σ : (a : ι) → ι) x))
hτ : τ = Equiv.trans σ (Equiv.swap x ((σ : (a : ι) → ι) x))
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hind : LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
hσa : x ≠ (σ : (a : ι) → ι) x
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) x : ι)
hx : ¬(σ : (a : ι) → ι) x = x ∧ x ∈ s
⊢ False

Tactic:
exact has hx.2

Premises used: And.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 : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g i) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i))

Tactic:
hfg.dual_right.sum_smul_comp_perm_le_sum_smul hσ

Premises used: MonovaryOn.sum_smul_comp_perm_le_sum_smul, AntivaryOn.dual_right, 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 : PosSMulMono α β
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:
simp [set_support_symm_eq, hσ]

Premises used: Equiv.Perm.set_support_symm_eq
-- 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 : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i))
⊢ LE.le.{u_3} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i)

Tactic:
convert!
    hfg.sum_smul_comp_perm_le_sum_smul
      (show {x | σ⁻¹ x ≠ x} ⊆ s by simp [set_support_symm_eq, hσ]) using 1

Premises used: MonovaryOn.sum_smul_comp_perm_le_sum_smul
-- 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 : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn 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 ((σ⁻¹ : (a : ι) → ι) i))

Tactic:
σ.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 : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn 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 ((σ⁻¹ : (a : ι) → ι) i))

Tactic:
exact σ.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 : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g i) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i)

Tactic:
hfg.dual_right.sum_comp_perm_smul_le_sum_smul hσ

Premises used: MonovaryOn.sum_comp_perm_smul_le_sum_smul, AntivaryOn.dual_right, 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 : PosSMulMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Monovary f g
⊢ LE.le.{u_3} (α := β) (∑ i : ι, f i • g ((σ : (a : ι) → ι) i)) (∑ i : ι, f i • g i)

Tactic:
(hfg.monovaryOn _).sum_smul_comp_perm_le_sum_smul fun _ _ ↦ mem_univ _

Premises used: Finset.mem_univ, Monovary.monovaryOn, MonovaryOn.sum_smul_comp_perm_le_sum_smul
-- 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 : PosSMulMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Antivary f g
⊢ LE.le.{u_3} (α := β) (∑ i : ι, f i • g i) (∑ i : ι, f i • g ((σ : (a : ι) → ι) i))

Tactic:
(hfg.antivaryOn _).sum_smul_le_sum_smul_comp_perm fun _ _ ↦ mem_univ _

Premises used: Finset.mem_univ, AntivaryOn.sum_smul_le_sum_smul_comp_perm, 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 : PosSMulMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Monovary f g
⊢ LE.le.{u_3} (α := β) (∑ i : ι, f ((σ : (a : ι) → ι) i) • g i) (∑ i : ι, f i • g i)

Tactic:
(hfg.monovaryOn _).sum_comp_perm_smul_le_sum_smul fun _ _ ↦ mem_univ _

Premises used: Finset.mem_univ, Monovary.monovaryOn, MonovaryOn.sum_comp_perm_smul_le_sum_smul
-- 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 : PosSMulMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Antivary f g
⊢ LE.le.{u_3} (α := β) (∑ i : ι, f i • g i) (∑ i : ι, f ((σ : (a : ι) → ι) i) • g i)

Tactic:
(hfg.antivaryOn _).sum_smul_le_sum_comp_perm_smul fun _ _ ↦ mem_univ _

Premises used: Finset.mem_univ, AntivaryOn.sum_smul_le_sum_comp_perm_smul, 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 α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)
⊢ LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g i) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i))

Tactic:
simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_symm_eq _).subset.trans hσ)

Premises used: MonovaryOn.sum_smul_comp_perm_le_sum_smul, HasSubset.Subset.trans, Eq.subset, Equiv.Perm.set_support_symm_eq
-- 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)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)

Tactic:
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σ)⟩
-- 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 : ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)
⊢ ¬∀ ⦃i : ι⦄,
      i ∈ (↑s : Set ι) →
        ∀ ⦃j : ι⦄, j ∈ (↑s : Set ι) → (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j → f i ≤ f j

Tactic:
rw [MonovaryOn] at h

Premises used: MonovaryOn
-- 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 :
  ¬∀ ⦃i : ι⦄,
      i ∈ (↑s : Set ι) →
        ∀ ⦃j : ι⦄, j ∈ (↑s : Set ι) → (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j → f i ≤ f j
⊢ ∃ i ∈ (↑s : Set ι), ∃ j ∈ (↑s : Set ι), (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j ∧ f j < f i

Tactic:
push Not at h

Premises used: Not
-- 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 : ∃ i ∈ (↑s : Set ι), ∃ j ∈ (↑s : Set ι), (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j ∧ f j < f i
obtain :
  ∀ (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)
⊢ ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)

Tactic:
obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := 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 ι)
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) σ
⊢ {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)

Tactic:
(set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)

Premises used: Equiv.Perm.set_support_mul_subset, Equiv.swap, setOf, HasSubset.Subset.trans, Set.union_subset
-- 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) σ
refine :
  ∀ (z : ι) (hz : Membership.mem (γ := Set ι) {x_1 : ι | (Equiv.swap x y : (a : ι) → ι) x_1 ≠ x_1} z), z ∈ (↑s : Set ι)
⊢ {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)

Tactic:
refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)

Premises used: Equiv.Perm.set_support_mul_subset, Equiv.swap, HasSubset.Subset.trans, Set.union_subset
-- 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) σ
z : ι
hz : Membership.mem (γ := Set ι) {x_1 : ι | (Equiv.swap x y : (a : ι) → ι) x_1 ≠ x_1} z
inl :
  ∀ (hx : z ∈ (↑s : Set ι)) (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) z < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f z)
    (hz : Membership.mem (γ := Set ι) {x : ι | (Equiv.swap z y : (a : ι) → ι) x ≠ x} z), z ≠ y → z ∈ (↑s : Set ι)
inr :
  ∀ (hy : z ∈ (↑s : Set ι)) (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) z) (hfxy : f z < f x)
    (hz : Membership.mem (γ := Set ι) {x_1 : ι | (Equiv.swap x z : (a : ι) → ι) x_1 ≠ x_1} z), x ≠ z → z ∈ (↑s : Set ι)
⊢ z ∈ (↑s : Set ι)

Tactic:
obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz

Premises used: Equiv.swap_apply_ne_self_iff, Iff.mp, 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 ι)
y : ι
hy : y ∈ (↑s : Set ι)
z : ι
hx : z ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) z < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f z
τ : Perm ι := Equiv.trans (Equiv.swap z y) σ
hz : Membership.mem (γ := Set ι) {x : ι | (Equiv.swap z y : (a : ι) → ι) x ≠ x} z
left : z ≠ y
⊢ z ∈ (↑s : Set ι)

Tactic:
assumption
-- 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 ι)
z : ι
hy : z ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) z
hfxy : f z < f x
τ : Perm ι := Equiv.trans (Equiv.swap x z) σ
hz : Membership.mem (γ := Set ι) {x_1 : ι | (Equiv.swap x z : (a : ι) → ι) x_1 ≠ x_1} z
left : x ≠ z
⊢ z ∈ (↑s : Set ι)

Tactic:
assumption
-- 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) σ
⊢ {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)

Tactic:
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
-- 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 ι)
⊢ ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)

Tactic:
((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne

Premises used: MonovaryOn.sum_smul_comp_perm_le_sum_smul, LE.le.trans_lt', LT.lt.ne
-- 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 ι)
refine : LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
⊢ ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)

Tactic:
refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne

Premises used: MonovaryOn.sum_smul_comp_perm_le_sum_smul, LE.le.trans_lt', LT.lt.ne
-- 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 ι)
inl :
  ∀ (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 :
  ∀ (hxy : x ≠ y),
    LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
⊢ LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))

Tactic:
obtain rfl | hxy := eq_or_ne x y

Premises used: eq_or_ne, 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 hy : x ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) x
hfxy : f x < f x
τ : Perm ι := 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))

Tactic:
cases lt_irrefl _ hfxy

Premises used: lt_irrefl