awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (β × α))
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))
⊢ LE.le.{u_3} (α := β) (∑ i ∈ insert a s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ insert a s, f i • g i)
have hτs : {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₂)
-- 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 (β × α))
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 ∈ insert a s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ insert a s, f i • g i)
have hind₁ : 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
Cleared hypotheses: hind
-- 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)
⊢ LE.le.{u_3} (α := β) (∑ i ∈ insert a s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ insert a s, f i • g i)
have insert : f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤ f a • g a + ∑ i ∈ s, f i • g i
Tactic: simp_rw [sum_insert has]
-- 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)
⊢ f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤ f a • g a + ∑ i ∈ s, f i • g i
have insert : f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
  f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)
Tactic: grw [← hind]
-- 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)
⊢ f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)
have 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)
Tactic: obtain hσa | hσa := eq_or_ne a (σ a)
-- 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)
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)
have 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)
Tactic: obtain hσa | hσa := eq_or_ne a (σ a)
-- 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
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)
⊢ f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)
have 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)
Tactic: rw [hτ, ← hσa, swap_self, trans_refl]
-- 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
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)
⊢ f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)
have 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)
Tactic: rw [hτ, ← hσa, swap_self, trans_refl]
-- 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
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)
⊢ f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)
have insert₃ : f a • g 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]
-- 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
⊢ Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
have hσa₁ : ¬(σ⁻¹ : (a : ι) → ι) a = a
Tactic: rw [Ne, ← inv_eq_iff_eq] at hσa
Cleared hypotheses: hσa
-- 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
⊢ Membership.mem (α := ι) s ((Equiv.symm σ : (a : ι) → ι) a : ι)
have refine : ∀ (h : Eq (α := ι) ((σ : (a : ι) → ι) ((Equiv.symm σ : (a : ι) → ι) a : ι) : ι) ((Equiv.symm σ : (a : ι) → ι) a : ι)),
  (σ⁻¹ : (a : ι) → ι) a = a
Tactic: refine mem_of_mem_insert_of_ne (hσ fun h ↦ hσa ?_) hσa
-- 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
h : Eq (α := ι) ((σ : (a : ι) → ι) ((Equiv.symm σ : (a : ι) → ι) a : ι) : ι) ((Equiv.symm σ : (a : ι) → ι) a : ι)
⊢ (σ⁻¹ : (a : ι) → ι) a = a
have rwa : ∀ (h : a = (Equiv.symm σ : (a : ι) → ι) a), (σ⁻¹ : (a : ι) → ι) a = a
Tactic: rwa [apply_symm_apply, eq_comm] at h
Cleared hypotheses: h
-- 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
h : Eq (α := ι) ((σ : (a : ι) → ι) ((Equiv.symm σ : (a : ι) → ι) a : ι) : ι) ((Equiv.symm σ : (a : ι) → ι) a : ι)
rwa : ∀ (h : a = (Equiv.symm σ : (a : ι) → ι) a), (σ⁻¹ : (a : ι) → ι) a = a
⊢ (σ⁻¹ : (a : ι) → ι) a = a
have rwa₁ : ∀ (h : (Equiv.symm σ : (a : ι) → ι) a = a), (σ⁻¹ : (a : ι) → ι) a = a
Tactic: rwa [apply_symm_apply, eq_comm] at h
Cleared hypotheses: h
-- 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
⊢ f a • g ((σ : (a : ι) → ι) a) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)
have h1s : 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
-- 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) + ∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i) ≤
    f a • g a + ∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i)
have 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))
Tactic: simp only [← s.sum_erase_add _ h1s, add_comm]
-- 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 : ι) → ι) ((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]