-- 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 hlt.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]
g : (Fin 2 → D) → D
h✝ : g ∈ ω
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i

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

Result:
case hlt.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]
g : (Fin 2 → D) → D
h✝ : g ∈ ω
this : (fun i => g (swap ![![a, b], ![b, a]] i)) ∈ ω.tt ![![a, b], ![b, a]]
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i

Proof state:
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

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

Result:
case hlt.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]
g : (Fin 2 → D) → D
h✝ : g ∈ ω
⊢ ∃ 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 • 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
⊢ False

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]

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]
⊢ False

Proof state:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
mcf : HasMaxCutProperty f
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
contr : AdmitsFractional f ω
⊢ False

Tactic:
obtain ⟨a, b, hab, mcfab⟩ := mcf

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
contr : AdmitsFractional f ω
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ False

Proof state:
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]
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)

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.h.e'_3
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
⊢ Multiset.map (fun x => f ![a, b]) ω = Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])

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

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]
half_sharp :
  (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum +
      (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    (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

Result:
no goals

Proof state:
case hlt.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]
g : (Fin 2 → D) → D
h✝ : g ∈ ω
this : (fun i => g (swap ![![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⟩

Result:
no goals

Proof state:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
mcf : HasMaxCutProperty f
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
⊢ ¬AdmitsFractional f ω

Tactic:
intro contr

Result:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
mcf : HasMaxCutProperty f
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
contr : AdmitsFractional f ω
⊢ False

Proof state:
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

Tactic:
intro r rin

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]
r : Fin (Nat.succ 0).succ → D
rin : r ∈ ω.tt ![![a, b], ![b, a]]
⊢ f ![a, b] ≤ f r