awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
o : (Fin 2 → D) → D
in_omega : o ∈ ω
equ :
  f ![a, b] =
    f
      ![(fun (i : Fin (Nat.succ 0).succ) ↦
            o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
          0,
        (fun (i : Fin (Nat.succ 0).succ) ↦
            o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
          1]
asymm :
  Ne.{u_1 + 1} (α := D)
    ((fun (i : Fin (Nat.succ 0).succ) ↦
        o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
      0)
    ((fun (i : Fin (Nat.succ 0).succ) ↦
        o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
      1)
h : (fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 0) = ![a, b]
h₁ : (fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 1) = ![b, a]
⊢ (o fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 0) = o fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 1

Tactic:
convert! symmega ![a, b] ![b, a] (by simp [List.Perm.swap]) o in_omega using 2

Premises used: Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
o : (Fin 2 → D) → D
in_omega : o ∈ ω
equ :
  f ![a, b] =
    f
      ![(fun (i : Fin (Nat.succ 0).succ) ↦
            o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
          0,
        (fun (i : Fin (Nat.succ 0).succ) ↦
            o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
          1]
asymm :
  Ne.{u_1 + 1} (α := D)
    ((fun (i : Fin (Nat.succ 0).succ) ↦
        o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
      0)
    ((fun (i : Fin (Nat.succ 0).succ) ↦
        o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
      1)
⊢ (fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 0) = ![a, b]

Tactic:
simp [Matrix.const_fin1_eq]

Premises used: Matrix.const_fin1_eq
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
o : (Fin 2 → D) → D
in_omega : o ∈ ω
equ :
  f ![a, b] =
    f
      ![(fun (i : Fin (Nat.succ 0).succ) ↦
            o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
          0,
        (fun (i : Fin (Nat.succ 0).succ) ↦
            o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
          1]
asymm :
  Ne.{u_1 + 1} (α := D)
    ((fun (i : Fin (Nat.succ 0).succ) ↦
        o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
      0)
    ((fun (i : Fin (Nat.succ 0).succ) ↦
        o (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
      1)
⊢ (fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 1) = ![b, a]

Tactic:
simp [Matrix.const_fin1_eq]

Premises used: Matrix.const_fin1_eq
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
mcf : HasMaxCutProperty f
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
contr : AdmitsFractional f ω
obtain : ∀ (a b : D) (hab : a ≠ b) (mcfab : HasMaxCutPropertyAt f a b), False
⊢ False

Tactic:
obtain ⟨a, b, hab, mcfab⟩ := mcf
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
contr : AdmitsFractional f ω
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤
    HSMul.hSMul (β := C) ω.size (∑ i : Fin 2, f (![![a, b], ![b, a]] i))

Tactic:
specialize contr ![![a, b], ![b, a]]

Premises used: Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤
    HSMul.hSMul (β := C) ω.size (∑ i : Fin 2, f (![![a, b], ![b, a]] i))
⊢ HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])

Tactic:
rw [Fin.sum_univ_two', ← mcfab.left, ← two_nsmul] at contr

Premises used: Fin.sum_univ_two', And.left, two_nsmul
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
hle : ∀ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] ≤ f i
hlt : ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i
⊢ Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])) <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
apply Multiset.sum_lt_sum

Premises used: Multiset.sum_lt_sum
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
r : Fin (Nat.succ 0).succ → D
rin : r ∈ ω.tt ![![a, b], ![b, a]]
⊢ f ![a, b] ≤ f r

Tactic:
le_of_lt (mcfab.rows_lt_aux hab symmega rin)

Premises used: le_of_lt, Function.HasMaxCutPropertyAt.rows_lt_aux
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
r : Fin (Nat.succ 0).succ → D
rin : r ∈ ω.tt ![![a, b], ![b, a]]
⊢ f ![a, b] ≤ f r

Tactic:
exact le_of_lt (mcfab.rows_lt_aux hab symmega rin)

Premises used: le_of_lt, Function.HasMaxCutPropertyAt.rows_lt_aux
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
hlt : ∀ g ∈ ω, ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i

Tactic:
obtain ⟨g, _⟩ := valid.contains

Premises used: FractionalOperation.IsValid.contains
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
g : (Fin 2 → D) → D
h : g ∈ ω
simp :
  ∃ a_1 ∈ ω,
    Eq.{u_1 + 1} (α := (i : Fin (Nat.succ 0).succ) → D)
      (fun (i : Fin (Nat.succ 0).succ) ↦
        a_1 (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
      fun (i : Fin (Nat.succ 0).succ) ↦ g (swap (φ := fun (x y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i)
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ g (swap (φ := fun (x y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i)) ∈
    ω.tt ![![a, b], ![b, a]]

Tactic:
simp only [FractionalOperation.tt, Multiset.mem_map]

Premises used: FractionalOperation.tt, Multiset.mem_map
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
g : (Fin 2 → D) → D
h_1 : g ∈ ω
w : (Fin 2 → D) → D
h :
  g ∈ ω ∧
    Eq.{u_1 + 1} (α := (i : Fin (Nat.succ 0).succ) → D)
      (fun (i : Fin (Nat.succ 0).succ) ↦
        g (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
      fun (i : Fin (Nat.succ 0).succ) ↦ g (swap (φ := fun (x y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i)
⊢ ∃ a_1 ∈ ω,
    Eq.{u_1 + 1} (α := (i : Fin (Nat.succ 0).succ) → D)
      (fun (i : Fin (Nat.succ 0).succ) ↦
        a_1 (swap (φ := fun (x : Fin 2) (y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i))
      fun (i : Fin (Nat.succ 0).succ) ↦ g (swap (φ := fun (x y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i)

Tactic:
use g
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
g : (Fin 2 → D) → D
h : g ∈ ω
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ g (swap (φ := fun (x y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i)) ∈
    ω.tt ![![a, b], ![b, a]]

Tactic:
have : (fun i => g ((Function.swap ![![a, b], ![b, a]]) i)) ∈ ω.tt ![![a, b], ![b, a]] := by
          simp only [FractionalOperation.tt, Multiset.mem_map]
          use g
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
g : (Fin 2 → D) → D
h : g ∈ ω
this :
  (fun (i : Fin (Nat.succ 0).succ) ↦ g (swap (φ := fun (x y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i)) ∈
    ω.tt ![![a, b], ![b, a]]
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i

Tactic:
⟨_, this, mcfab.rows_lt_aux hab symmega this⟩

Premises used: And.intro, Exists.intro, Function.HasMaxCutPropertyAt.rows_lt_aux
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
g : (Fin 2 → D) → D
h : g ∈ ω
this :
  (fun (i : Fin (Nat.succ 0).succ) ↦ g (swap (φ := fun (x y : Fin (Nat.succ 0).succ) ↦ D) ![![a, b], ![b, a]] i)) ∈
    ω.tt ![![a, b], ![b, a]]
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i

Tactic:
exact ⟨_, this, mcfab.rows_lt_aux hab symmega this⟩
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
⊢ Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])) <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
have half_sharp :
      ((ω.tt ![![a, b], ![b, a]]).map (fun _ => f ![a, b])).sum <
      ((ω.tt ![![a, b], ![b, a]]).map f).sum := by
      apply Multiset.sum_lt_sum
      · intro r rin
        exact le_of_lt (mcfab.rows_lt_aux hab symmega rin)
      · obtain ⟨g, _⟩ := valid.contains
        have : (fun i => g ((Function.swap ![![a, b], ![b, a]]) i)) ∈ ω.tt ![![a, b], ![b, a]] := by
          simp only [FractionalOperation.tt, Multiset.mem_map]
          use g
        exact ⟨_, this, mcfab.rows_lt_aux hab symmega this⟩
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
half_sharp :
  Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])) <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
rw :
  HAdd.hAdd (α := C)
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])))
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum + (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
rw [two_nsmul, two_nsmul]

Premises used: two_nsmul
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
half_sharp :
  Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])) <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ HAdd.hAdd (α := C)
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])))
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum + (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
add_lt_add half_sharp half_sharp

Premises used: add_lt_add
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
half_sharp :
  Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])) <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ HAdd.hAdd (α := C)
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])))
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum + (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
exact add_lt_add half_sharp half_sharp

Premises used: add_lt_add
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
⊢ HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
have sharp :
    2 • ((ω.tt ![![a, b], ![b, a]]).map (fun _ => f ![a, b])).sum <
    2 • ((ω.tt ![![a, b], ![b, a]]).map f).sum := by
    have half_sharp :
      ((ω.tt ![![a, b], ![b, a]]).map (fun _ => f ![a, b])).sum <
      ((ω.tt ![![a, b], ![b, a]]).map f).sum := by
      apply Multiset.sum_lt_sum
      · intro r rin
        exact le_of_lt (mcfab.rows_lt_aux hab symmega rin)
      · obtain ⟨g, _⟩ := valid.contains
        have : (fun i => g ((Function.swap ![![a, b], ![b, a]]) i)) ∈ ω.tt ![![a, b], ![b, a]] := by
          simp only [FractionalOperation.tt, Multiset.mem_map]
          use g
        exact ⟨_, this, mcfab.rows_lt_aux hab symmega this⟩
    rw [two_nsmul, two_nsmul]
    exact add_lt_add half_sharp half_sharp
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])

Tactic:
lt_of_lt_of_le sharp contr

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
h :
  Eq.{u_3 + 1} (α := Multiset C) (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)
    (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))
⊢ HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])

Tactic:
convert! lt_of_lt_of_le sharp contr

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ Eq.{u_3 + 1} (α := Multiset C) (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)
    (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))

Tactic:
simp [FractionalOperation.tt, Multiset.map_map]

Premises used: FractionalOperation.tt, Multiset.map_map
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])

Tactic:
have impos : 2 • (ω.map (fun _ => f ![a, b])).sum < ω.size • 2 • f ![a, b] := by
    convert! lt_of_lt_of_le sharp contr
    simp [FractionalOperation.tt, Multiset.map_map]
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos :
  HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
⊢ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])

Tactic:
have rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b] := nsmul_left_comm ..
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos :
  HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
rhs_swap : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
⊢ Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω) = ω.size • f ![a, b]

Tactic:
simp