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

Tactic:
mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)

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

Tactic:
exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)

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

Tactic:
have hτs : {x | τ x ≠ x} ⊆ s := by
    intro x hx
    simp only [τ, Ne, Set.mem_setOf_eq, Equiv.swap_comp_apply] at hx
    split_ifs at hx with h₁ h₂
    · obtain rfl | hax := eq_or_ne x a
      · contradiction
      · exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
    · exact (hx <| σ.injective h₂.symm).elim
    · exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ 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 : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
hind :
  ∀ {σ : Perm ι} (hfg : MonovaryOn f g (↑s : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)

Tactic:
specialize hind (hfg.subset <| subset_insert _ _) hτs

Premises used: MonovaryOn.subset, Finset.subset_insert
-- 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 : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
σ : Perm ι
hfg : MonovaryOn f g (↑(Insert.insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(Insert.insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
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)
insert : f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤ f a • g a + ∑ i ∈ s, f i • g i
⊢ LE.le.{u_3} (α := β) (∑ i ∈ Insert.insert a s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ Insert.insert a s, f i • g i)

Tactic:
simp_rw [sum_insert has]

Premises used: Finset.sum_insert
-- 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 : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
σ : Perm ι
hfg : MonovaryOn f g (↑(Insert.insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(Insert.insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
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)
insert :
  f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)
⊢ f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤ f a • g a + ∑ i ∈ s, f i • g i

Tactic:
grw [← hind]
-- 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 : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
σ : Perm ι
hfg : MonovaryOn f g (↑(Insert.insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(Insert.insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
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)
insert :
  ∀ (hσa : a = (σ : (a : ι) → ι) a),
    f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
      f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)
insert₁ :
  ∀ (hσa : a ≠ (σ : (a : ι) → ι) a),
    f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
      f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)
⊢ f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)

Tactic:
obtain hσa | hσa := eq_or_ne a (σ a)

Premises used: eq_or_ne, 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 : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
σ : Perm ι
hfg : MonovaryOn f g (↑(Insert.insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(Insert.insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
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 : a = (σ : (a : ι) → ι) a
insert :
  f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a)) : (a : ι) → ι) i)
insert₁ :
  f a • g a + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((Equiv.trans σ (Equiv.swap a a) : (a : ι) → ι) i)
insert₂ :
  f a • g a + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((Equiv.trans σ (Equiv.refl ι) : (a : ι) → ι) i)
insert₃ insert₄ :
  f a • g a + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤ f a • g a + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)
⊢ f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)

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

Premises used: Equiv.trans_refl, Equiv.swap_self
-- 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 : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
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 : a ≠ (σ : (a : ι) → ι) a
⊢ ¬(σ⁻¹ : (a : ι) → ι) a = a

Tactic:
rw [Ne, ← inv_eq_iff_eq] at hσa

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

Tactic:
mem_of_mem_insert_of_ne (hσ fun h ↦ hσa ?_) hσa

Premises used: Finset.mem_of_mem_insert_of_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 : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
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 : ¬(σ⁻¹ : (a : ι) → ι) a = a
refine :
  ∀ (h : Eq (α := ι) ((σ : (a : ι) → ι) ((Equiv.symm σ : (a : ι) → ι) a : ι) : ι) ((Equiv.symm σ : (a : ι) → ι) a : ι)),
    (σ⁻¹ : (a : ι) → ι) a = a
⊢ Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)

Tactic:
refine mem_of_mem_insert_of_ne (hσ fun h ↦ hσa ?_) hσa

Premises used: Finset.mem_of_mem_insert_of_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 : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
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 : ¬(σ⁻¹ : (a : ι) → ι) a = a
h : Eq (α := ι) ((σ : (a : ι) → ι) ((Equiv.symm σ : (a : ι) → ι) a : ι) : ι) ((Equiv.symm σ : (a : ι) → ι) a : ι)
rwa : ∀ (h : a = (Equiv.symm σ : (a : ι) → ι) a), (σ⁻¹ : (a : ι) → ι) a = a
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : (Equiv.symm σ : (a : ι) → ι) a = a), (σ⁻¹ : (a : ι) → ι) a = a
⊢ (σ⁻¹ : (a : ι) → ι) a = a

Tactic:
rwa [apply_symm_apply, eq_comm] at h

Premises used: Equiv.apply_symm_apply, eq_comm
-- 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 : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
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 : a ≠ (σ : (a : ι) → ι) a
⊢ Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)

Tactic:
have h1s : σ.symm 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_symm_apply, eq_comm] at 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 : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
σ : Perm ι
hfg : MonovaryOn f g (↑(Insert.insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(Insert.insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
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 : a ≠ (σ : (a : ι) → ι) a
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
insert :
  f a • g ((σ : (a : ι) → ι) a) +
      (f ((Equiv.symm σ : (a : ι) → ι) a) • g ((σ : (a : ι) → ι) ((Equiv.symm σ : (a : ι) → ι) a : ι)) +
        ∑ i ∈ s.erase ((Equiv.symm σ : (a : ι) → ι) a), f i • g ((σ : (a : ι) → ι) i)) ≤
    f a • g a +
      (f ((Equiv.symm σ : (a : ι) → ι) a) • g ((τ : (a : ι) → ι) ((Equiv.symm σ : (a : ι) → ι) a : ι)) +
        ∑ i ∈ s.erase ((Equiv.symm σ : (a : ι) → ι) a), f i • g ((τ : (a : ι) → ι) i))
⊢ f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)

Tactic:
simp only [← s.sum_erase_add _ h1s, add_comm]

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

Tactic:
rw [← add_assoc, ← add_assoc]

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

Tactic:
simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Function.comp_apply, Equiv.coe_trans, Equiv.swap_apply_left