-- Mathlib/Combinatorics/Optimization/ValuedCSP.lean
lemma Function.HasMaxCutProperty.forbids_commutativeFractionalPolymorphism
    {f : (Fin 2 → D) → C} (mcf : f.HasMaxCutProperty)
    {ω : FractionalOperation D 2} (valid : ω.IsValid) (symmega : ω.IsSymmetric) :
    ¬ f.AdmitsFractional ω

Proof state:
case intro.intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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
⊢ False

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

Result:
case intro.intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • ∑ i : Fin 2, f (![![a, b], ![b, a]] i)
⊢ False

Proof state:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
sharp :
  2 • (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • (Multiset.map (fun x => f ![a, b]) ω).sum < ω.size • 2 • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
⊢ (Multiset.map (fun x => f ![a, b]) ω).sum = ω.size • f ![a, b]

Tactic:
simp

Result:
no goals

Proof state:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
⊢ (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
apply Multiset.sum_lt_sum

Result:
case hle
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
⊢ ∀ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] ≤ f i

case hlt
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i

Proof state:
case intro.intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • ∑ i : Fin 2, f (![![a, b], ![b, a]] i)
⊢ False

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

Result:
case intro.intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
⊢ False

Proof state:
case intro.intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
sharp :
  2 • (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • (Multiset.map (fun x => f ![a, b]) ω).sum < ω.size • 2 • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
⊢ False

Tactic:
have distrib : (ω.map (fun _ => f ![a, b])).sum = ω.size • f ![a, b] := by simp

Result:
case intro.intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
sharp :
  2 • (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • (Multiset.map (fun x => f ![a, b]) ω).sum < ω.size • 2 • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x => f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False

Proof state:
case intro.intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
sharp :
  2 • (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • ω.size • f ![a, b] < 2 • ω.size • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x => f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False

Tactic:
exact ne_of_lt impos rfl

Result:
no goals

Proof state:
case intro.intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
sharp :
  2 • (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • (Multiset.map (fun x => f ![a, b]) ω).sum < ω.size • 2 • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x => f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False

Tactic:
rw [rhs_swap, distrib] at impos

Result:
case intro.intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
sharp :
  2 • (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • ω.size • f ![a, b] < 2 • ω.size • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x => f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False