awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (goal)
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 : ι) → ι) ((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)
have 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 : ι))
Tactic: simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (goal)
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 : ι))
have insert : f ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a
Tactic: refine add_le_add (smul_add_smul_le_smul_add_smul' ?_ ?_) (sum_congr rfl fun x hx ↦ ?_).le
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (goal)
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
⊢ 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 : ι))
have insert₁ : g ((σ : (a : ι) → ι) a) ≤ g a
Tactic: refine add_le_add (smul_add_smul_le_smul_add_smul' ?_ ?_) (sum_congr rfl fun x hx ↦ ?_).le
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (goal)
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
⊢ 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 : ι))
have 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 : ι))
Tactic: refine add_le_add (smul_add_smul_le_smul_add_smul' ?_ ?_) (sum_congr rfl fun x hx ↦ ?_).le
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (hypothesis)
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 ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a
have 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 (β × α))
Tactic: specialize hamax (σ.symm a) h1s
Cleared hypotheses: hamax
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (hypothesis)
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 (β × α))
⊢ f ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a
have 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
Tactic: rw [Prod.Lex.toLex_le_toLex] at hamax
Cleared hypotheses: hamax
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (goal)
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)).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
have 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
Tactic: rcases hamax with hamax | hamax
Cleared hypotheses: hamax
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (goal)
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
⊢ f ((Equiv.symm σ : (a : ι) → ι) a) ≤ f a
have 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
Tactic: rcases hamax with hamax | hamax
Cleared hypotheses: hamax
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (hypothesis)
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 : ι)
⊢ g ((σ : (a : ι) → ι) a) ≤ g a
have hamax₁ : 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)
Cleared hypotheses: hamax
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (hypothesis)
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) ≤ g a
have 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
Tactic: rw [Prod.Lex.toLex_le_toLex] at hamax
Cleared hypotheses: hamax
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (goal)
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)).1 = (g a, f a).1 ∧
      (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).2 ≤ (g a, f a).2
⊢ g ((σ : (a : ι) → ι) a) ≤ g a
have insert : ∀ (hamax : (g ((σ : (a : ι) → ι) a), f ((σ : (a : ι) → ι) a)).1 < (g a, f a).1), g ((σ : (a : ι) → ι) a) ≤ g a
Tactic: rcases hamax with hamax | hamax
Cleared hypotheses: hamax
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (goal)
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
⊢ g ((σ : (a : ι) → ι) a) ≤ g a
have 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
Tactic: rcases hamax with hamax | hamax
Cleared hypotheses: hamax
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (hypothesis)
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)
⊢ f x • g ((σ : (a : ι) → ι) x) = f x • g ((Equiv.swap a ((σ : (a : ι) → ι) a) : (a : ι) → ι) ((σ : (a : ι) → ι) x : ι))
have hx₁ : ¬(σ : (a : ι) → ι) x = a ∧ x ∈ s
Tactic: rw [mem_erase, Ne, eq_symm_apply] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (goal)
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
⊢ f x • g ((σ : (a : ι) → ι) x) = f x • g ((Equiv.swap a ((σ : (a : ι) → ι) a) : (a : ι) → ι) ((σ : (a : ι) → ι) x : ι))
have rw : x ≠ a
Tactic: rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (goal)
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 ι)
⊢ LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
have empty : ∀ {σ : Perm ι} (hfg : MonovaryOn f g (↑∅ : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑∅ : Set ι)),
  LE.le.{u_3} (α := β) (∑ i ∈ ∅, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ ∅, f i • g i)
Tactic: classical
  induction s using induction_on_max_value fun i ↦ toLex (g i, f i) generalizing σ with
  | empty => simp only [le_rfl, Finset.sum_empty]
  | insert a s has hamax hind => ?_
  set τ : Perm ι := σ.trans (swap a (σ a)) with hτ
  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₂)
  specialize hind (hfg.subset <| subset_insert _ _) hτs
  simp_rw [sum_insert has]
  grw [← hind]
  obtain hσa | hσa := eq_or_ne a (σ a)
  · rw [hτ, ← hσa, swap_self, trans_refl]
  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
  simp only [← s.sum_erase_add _ h1s, add_comm]
  rw [← add_assoc, ← add_assoc]
  simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_symm_apply]
  refine add_le_add (smul_add_smul_le_smul_add_smul' ?_ ?_) (sum_congr rfl fun x hx ↦ ?_).le
  · specialize hamax (σ.symm a) h1s
    rw [Prod.Lex.toLex_le_toLex] at hamax
    rcases hamax with hamax | hamax
    · exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax
    · exact hamax.2
  · specialize hamax (σ a) (mem_of_mem_insert_of_ne (hσ <| σ.injective.ne hσa.symm) hσa.symm)
    rw [Prod.Lex.toLex_le_toLex] at hamax
    rcases hamax with hamax | hamax
    · exact hamax.le
    · exact hamax.1.le
  · rw [mem_erase, Ne, eq_symm_apply] at hx
    rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]
    rintro rfl
    exact has hx.2
Cleared hypotheses: s, σ, hfg, hσ