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 α β
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 ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i)
have h : Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i))
Tactic: convert!
    hfg.sum_smul_comp_perm_le_sum_smul
      (show {x | σ⁻¹ x ≠ x} ⊆ s by simp [set_support_symm_eq, hσ]) using 1
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)
have refine : ∀ (h : ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)),
  ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
Tactic: refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm <| by
    simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_symm_eq _).subset.trans hσ)⟩
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)
⊢ ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
have h₁ : ¬∀ ⦃i : ι⦄,
    i ∈ (↑s : Set ι) → ∀ ⦃j : ι⦄, j ∈ (↑s : Set ι) → (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j → f i ≤ f j
Tactic: rw [MonovaryOn] 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h :
  ¬∀ ⦃i : ι⦄,
      i ∈ (↑s : Set ι) →
        ∀ ⦃j : ι⦄, j ∈ (↑s : Set ι) → (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j → f i ≤ f j
⊢ ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
have h₁ : ∃ i ∈ (↑s : Set ι), ∃ j ∈ (↑s : Set ι), (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j ∧ f j < f i
Tactic: push Not 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : ∃ i ∈ (↑s : Set ι), ∃ j ∈ (↑s : Set ι), (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j ∧ f j < f i
⊢ ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
have obtain : ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
  (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
  ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
Tactic: obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
⊢ {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
have refine : ∀ (z : ι) (hz : Membership.mem (γ := Set ι) {x_1 : ι | (Equiv.swap x y : (a : ι) → ι) x_1 ≠ x_1} z), z ∈ (↑s : Set ι)
Tactic: refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
z : ι
hz : Membership.mem (γ := Set ι) {x_1 : ι | (Equiv.swap x y : (a : ι) → ι) x_1 ≠ x_1} z
⊢ z ∈ (↑s : Set ι)
have inl : ∀ (hx : z ∈ (↑s : Set ι)) (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) z < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f z)
  (hz : Membership.mem (γ := Set ι) {x : ι | (Equiv.swap z y : (a : ι) → ι) x ≠ x} z), z ≠ y → z ∈ (↑s : Set ι)
Tactic: obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz
Cleared hypotheses: x, hx, hgxy, hfxy, τ, hz
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
z : ι
hz : Membership.mem (γ := Set ι) {x_1 : ι | (Equiv.swap x y : (a : ι) → ι) x_1 ≠ x_1} z
inl :
  ∀ (hx : z ∈ (↑s : Set ι)) (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) z < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f z)
    (hz : Membership.mem (γ := Set ι) {x : ι | (Equiv.swap z y : (a : ι) → ι) x ≠ x} z), z ≠ y → z ∈ (↑s : Set ι)
⊢ z ∈ (↑s : Set ι)
have inr : ∀ (hy : z ∈ (↑s : Set ι)) (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) z) (hfxy : f z < f x)
  (hz : Membership.mem (γ := Set ι) {x_1 : ι | (Equiv.swap x z : (a : ι) → ι) x_1 ≠ x_1} z), x ≠ z → z ∈ (↑s : Set ι)
Tactic: obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz
Cleared hypotheses: y, hy, hgxy, hfxy, τ, hz
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
⊢ ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
have hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
Tactic: have hτs : {x | τ x ≠ x} ⊆ s := by
    refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
    obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
have refine : LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
Tactic: refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
have inl : ∀ (hy : x ∈ (↑s : Set ι)) (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) x) (hfxy : f x < f x),
  let τ := Equiv.trans (Equiv.swap x x) σ;
  ∀ (hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
Tactic: obtain rfl | hxy := eq_or_ne x y
Cleared hypotheses: y, hy, hgxy, hfxy, τ, hτs
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
inl :
  ∀ (hy : x ∈ (↑s : Set ι)) (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) x) (hfxy : f x < f x),
    let τ := Equiv.trans (Equiv.swap x x) σ;
    ∀ (hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
      LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
⊢ LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
have inr : ∀ (hxy : x ≠ y), LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
Tactic: obtain rfl | hxy := eq_or_ne x y
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hxy : x ≠ y
⊢ LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g ((τ : (a : ι) → ι) i))
have inr : ∑ i ∈ (s.erase x).erase y, f i • g ((σ : (a : ι) → ι) i) +
    (f y • g ((σ : (a : ι) → ι) y) + f x • g ((σ : (a : ι) → ι) x)) <
  ∑ x_1 ∈ (s.erase x).erase y, f x_1 • g ((σ : (a : ι) → ι) ((Equiv.swap x y : (a : ι) → ι) x_1 : ι)) +
    (f y • g ((σ : (a : ι) → ι) x) + f x • g ((σ : (a : ι) → ι) y))
Tactic: simp only [τ, ← s.sum_erase_add _ hx,
    ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩),
    add_assoc, Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hxy : x ≠ y
⊢ ∑ i ∈ (s.erase x).erase y, f i • g ((σ : (a : ι) → ι) i) +
      (f y • g ((σ : (a : ι) → ι) y) + f x • g ((σ : (a : ι) → ι) x)) <
    ∑ x_1 ∈ (s.erase x).erase y, f x_1 • g ((σ : (a : ι) → ι) ((Equiv.swap x y : (a : ι) → ι) x_1 : ι)) +
      (f y • g ((σ : (a : ι) → ι) x) + f x • g ((σ : (a : ι) → ι) y))
have inr : ∀ (z : ι) (hz : z ∈ (s.erase x).erase y),
  f z • g ((σ : (a : ι) → ι) z) = f z • g ((σ : (a : ι) → ι) ((Equiv.swap x y : (a : ι) → ι) z : ι))
Tactic: refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
    (smul_add_smul_lt_smul_add_smul hfxy hgxy)
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hxy : x ≠ y
z : ι
hz : z ∈ (s.erase x).erase y
⊢ f z • g ((σ : (a : ι) → ι) z) = f z • g ((σ : (a : ι) → ι) ((Equiv.swap x y : (a : ι) → ι) z : ι))
have hz₁ : z ≠ y ∧ z ≠ x ∧ z ∈ s
Tactic: simp_rw [mem_erase] at hz
Cleared hypotheses: hz
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hxy : x ≠ y
z : ι
hz : z ≠ y ∧ z ≠ x ∧ z ∈ s
⊢ f z • g ((σ : (a : ι) → ι) z) = f z • g ((σ : (a : ι) → ι) ((Equiv.swap x y : (a : ι) → ι) z : ι))
have inr : f z • g ((σ : (a : ι) → ι) z) = f z • g ((σ : (a : ι) → ι) z)
Tactic: rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)
have refine : ∀ (h : ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)),
  ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
Tactic: classical
  refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm <| by
    simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_symm_eq _).subset.trans hσ)⟩
  rw [MonovaryOn] at h
  push Not at h
  obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
  set τ : Perm ι := (Equiv.swap x y).trans σ
  have hτs : {x | τ x ≠ x} ⊆ s := by
    refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
    obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
  refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne
  obtain rfl | hxy := eq_or_ne x y
  · cases lt_irrefl _ hfxy
  simp only [τ, ← s.sum_erase_add _ hx,
    ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩),
    add_assoc, Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
  refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
    (smul_add_smul_lt_smul_add_smul hfxy hgxy)
  simp_rw [mem_erase] at hz
  rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
refine :
  ∀ (h : ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)
have refine₁ : ∀
  (h :
    ¬∀ ⦃i : ι⦄,
        i ∈ (↑s : Set ι) →
          ∀ ⦃j : ι⦄, j ∈ (↑s : Set ι) → (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j → f i ≤ f j),
  ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
Tactic: classical
  refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm <| by
    simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_symm_eq _).subset.trans hσ)⟩
  rw [MonovaryOn] at h
  push Not at h
  obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
  set τ : Perm ι := (Equiv.swap x y).trans σ
  have hτs : {x | τ x ≠ x} ⊆ s := by
    refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
    obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
  refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne
  obtain rfl | hxy := eq_or_ne x y
  · cases lt_irrefl _ hfxy
  simp only [τ, ← s.sum_erase_add _ hx,
    ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩),
    add_assoc, Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
  refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
    (smul_add_smul_lt_smul_add_smul hfxy hgxy)
  simp_rw [mem_erase] at hz
  rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
refine :
  ∀ (h : ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₁ :
  ∀
    (h :
      ¬∀ ⦃i : ι⦄,
          i ∈ (↑s : Set ι) →
            ∀ ⦃j : ι⦄, j ∈ (↑s : Set ι) → (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j → f i ≤ f j),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)
have refine₂ : ∀ (h : ∃ i ∈ (↑s : Set ι), ∃ j ∈ (↑s : Set ι), (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j ∧ f j < f i),
  ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
Tactic: classical
  refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm <| by
    simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_symm_eq _).subset.trans hσ)⟩
  rw [MonovaryOn] at h
  push Not at h
  obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
  set τ : Perm ι := (Equiv.swap x y).trans σ
  have hτs : {x | τ x ≠ x} ⊆ s := by
    refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
    obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
  refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne
  obtain rfl | hxy := eq_or_ne x y
  · cases lt_irrefl _ hfxy
  simp only [τ, ← s.sum_erase_add _ hx,
    ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩),
    add_assoc, Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
  refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
    (smul_add_smul_lt_smul_add_smul hfxy hgxy)
  simp_rw [mem_erase] at hz
  rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]