-- Mathlib/Combinatorics/Optimization/ValuedCSP.lean
lemma Function.HasMaxCutPropertyAt.rows_lt_aux
    {f : (Fin 2 → D) → C} {a b : D} (mcf : f.HasMaxCutPropertyAt a b) (hab : a ≠ b)
    {ω : FractionalOperation D 2} (symmega : ω.IsSymmetric)
    {r : Fin 2 → D} (rin : r ∈ (ω.tt ![![a, b], ![b, a]])) :
    f ![a, b] < f r

Proof state:
case inr.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
⊢ r 0 ≠ r 1

Tactic:
rw [ha1, hb0] at hab

Result:
case inr.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
hab : r 1 ≠ r 0
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
⊢ r 0 ≠ r 1

Proof state:
case inr.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
hab : r 1 ≠ r 0
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
⊢ r 0 ≠ r 1

Tactic:
exact hab.symm

Result:
no goals

Proof state:
case intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 => o (swap ![![a, b], ![b, a]] i)) 0, (fun i => o (swap ![![a, b], ![b, a]] i)) 1]
asymm : (fun i => o (swap ![![a, b], ![b, a]] i)) 0 ≠ (fun i => o (swap ![![a, b], ![b, a]] i)) 1
⊢ (o fun j => ![![a, b], ![b, a]] j 0) = o fun j => ![![a, b], ![b, a]] j 1

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

Result:
no goals

Proof state:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : r ∈ ω.tt ![![a, b], ![b, a]]
⊢ f ![a, b] < f r

Tactic:
rw [FractionalOperation.tt, Multiset.mem_map] at rin

Result:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
⊢ f ![a, b] < f r

Proof state:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
⊢ f ![a, b] ≠ f ![r 0, r 1]

Tactic:
intro equ

Result:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
⊢ False

Proof state:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
⊢ f ![a, b] < f ![r 0, r 1]

Tactic:
apply lt_of_le_of_ne (mcf.right (r 0) (r 1)).left

Result:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
⊢ f ![a, b] ≠ f ![r 0, r 1]

Proof state:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
asymm : r 0 ≠ r 1
⊢ r 0 = r 1

Tactic:
obtain ⟨o, in_omega, rfl⟩ := rin

Result:
case intro.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid 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 => o (swap ![![a, b], ![b, a]] i)) 0, (fun i => o (swap ![![a, b], ![b, a]] i)) 1]
asymm : (fun i => o (swap ![![a, b], ![b, a]] i)) 0 ≠ (fun i => o (swap ![![a, b], ![b, a]] i)) 1
⊢ (fun i => o (swap ![![a, b], ![b, a]] i)) 0 = (fun i => o (swap ![![a, b], ![b, a]] i)) 1

Proof state:
case inl.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
⊢ r 0 ≠ r 1

Tactic:
rw [ha0, hb1] at hab

Result:
case inl.intro
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
hab : r 0 ≠ r 1
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
⊢ r 0 ≠ r 1

Proof state:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
⊢ f ![a, b] < f r

Tactic:
rw [show r = ![r 0, r 1] by simp [← List.ofFn_inj]]

Result:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
⊢ f ![a, b] < f ![r 0, r 1]

Proof state:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
asymm : r 0 ≠ r 1
⊢ False

Tactic:
apply asymm

Result:
D : Type u_1
C : Type u_3
inst✝ : OrderedCancelAddCommMonoid C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
asymm : r 0 ≠ r 1
⊢ r 0 = r 1