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 (β × α))
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
⊢ 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 : ι))

Tactic:
add_le_add (smul_add_smul_le_smul_add_smul' ?_ ?_) (sum_congr rfl fun x hx ↦ ?_).le

Premises used: add_le_add, Eq.le, smul_add_smul_le_smul_add_smul', 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 : 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 ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a
insert₁ : g ((σ : (a : ι) → ι) a) ≤ g a
insert₂ :
  ∀ (x : ι) (hx : x ∈ s.erase ((Equiv.symm σ : (a : ι) → ι) a)),
    f x • g ((σ : (a : ι) → ι) x) =
      f x • g ((Equiv.swap a ((σ : (a : ι) → ι) a) : (a : ι) → ι) ((σ : (a : ι) → ι) x : ι))
⊢ 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 : ι))

Tactic:
refine add_le_add (smul_add_smul_le_smul_add_smul' ?_ ?_) (sum_congr rfl fun x hx ↦ ?_).le

Premises used: add_le_add, Eq.le, smul_add_smul_le_smul_add_smul', 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 : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
⊢ LE.le (α := Lex (β × α))
    ((toLex : (a : β × α) → Lex (β × α)) (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)) :
      Lex (β × α))
    ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))

Tactic:
specialize hamax (σ.symm a) h1s

Premises used: 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 : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
hamax :
  LE.le (α := Lex (β × α))
    ((toLex : (a : β × α) → Lex (β × α)) (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)) :
      Lex (β × α))
    ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
⊢ (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).1 < (g a, f a).1 ∨
    (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).1 = (g a, f a).1 ∧
      (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2

Tactic:
rw [Prod.Lex.toLex_le_toLex] at hamax

Premises used: Prod.Lex.toLex_le_toLex
-- 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
σ : 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 : ι)
hamax :
  (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).1 < (g a, f a).1 ∨
    (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).1 = (g a, f a).1 ∧
      (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2
insert :
  ∀ (hamax : (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).1 < (g a, f a).1),
    f ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a
insert₁ :
  ∀
    (hamax :
      (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).1 = (g a, f a).1 ∧
        (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2),
    f ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a
⊢ f ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a

Tactic:
rcases hamax with hamax | hamax
-- 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
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
hamax : (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).1 < (g a, f a).1
⊢ f ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a

Tactic:
hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem
-- 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
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
hamax : (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).1 < (g a, f a).1
⊢ f ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a

Tactic:
exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem
-- 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
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
hamax :
  (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).1 = (g a, f a).1 ∧
    (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2
⊢ f ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a

Tactic:
hamax.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 : ι → β
a : ι
s : Finset ι
has : a ∉ s
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
hamax :
  (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).1 = (g a, f a).1 ∧
    (g ((Equiv.symm σ : (a : ι) → ι) a), f ((Equiv.symm σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2
⊢ f ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a

Tactic:
exact hamax.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 : ι → β
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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
⊢ LE.le (α := Lex (β × α))
    ((toLex : (a : β × α) → Lex (β × α)) (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)) : Lex (β × α))
    ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))

Tactic:
specialize hamax (σ a) (mem_of_mem_insert_of_ne (hσ <| σ.injective.ne hσa.symm) hσa.symm)

Premises used: Function.Injective.ne, Ne.symm, Finset.mem_of_mem_insert_of_ne, Equiv.injective, 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
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
hamax :
  LE.le (α := Lex (β × α))
    ((toLex : (a : β × α) → Lex (β × α)) (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)) : Lex (β × α))
    ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
⊢ (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 < (g a, f a).1 ∨
    (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 = (g a, f a).1 ∧
      (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2

Tactic:
rw [Prod.Lex.toLex_le_toLex] at hamax

Premises used: Prod.Lex.toLex_le_toLex
-- 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
σ : 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 : ι)
hamax :
  (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 < (g a, f a).1 ∨
    (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 = (g a, f a).1 ∧
      (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2
insert : ∀ (hamax : (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 < (g a, f a).1), g ((σ : (a : ι) → ι) a) ≤ g a
insert₁ :
  ∀
    (hamax :
      (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 = (g a, f a).1 ∧
        (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2),
    g ((σ : (a : ι) → ι) a) ≤ g a
⊢ g ((σ : (a : ι) → ι) a) ≤ g a

Tactic:
rcases hamax with hamax | hamax
-- 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
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
hamax : (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 < (g a, f a).1
⊢ g ((σ : (a : ι) → ι) a) ≤ g a

Tactic:
hamax.le

Premises used: LT.lt.le
-- 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
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
hamax : (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 < (g a, f a).1
⊢ g ((σ : (a : ι) → ι) a) ≤ g a

Tactic:
exact hamax.le

Premises used: LT.lt.le
-- 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
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
hamax :
  (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 = (g a, f a).1 ∧
    (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2
⊢ g ((σ : (a : ι) → ι) a) ≤ g a

Tactic:
hamax.1.le

Premises used: Eq.le, 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 : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
σ : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
hamax :
  (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 = (g a, f a).1 ∧
    (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2
⊢ g ((σ : (a : ι) → ι) a) ≤ g a

Tactic:
exact hamax.1.le

Premises used: Eq.le, 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 : 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
x : ι
hx : x ∈ s.erase ((Equiv.symm σ : (a : ι) → ι) a)
⊢ ¬(σ : (a : ι) → ι) x = a ∧ x ∈ s

Tactic:
rw [mem_erase, Ne, eq_symm_apply] at hx

Premises used: Ne, Finset.mem_erase, Equiv.eq_symm_apply
-- 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
h1s : Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
x : ι
hx : ¬(σ : (a : ι) → ι) x = a ∧ x ∈ s
rw : x ≠ a
⊢ f x • g ((σ : (a : ι) → ι) x) = f x • g ((Equiv.swap a ((σ : (a : ι) → ι) a) : (a : ι) → ι) ((σ : (a : ι) → ι) x : ι))

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

Premises used: Function.Injective.ne, Equiv.swap_apply_of_ne_of_ne, And.left, Equiv.injective