awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
S : σ → Finset R
htS : ∀ (i : σ), (t : (a : σ) → ℕ) i < #(S i)
x : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval :
  ∀ (s : σ → R) (_ : ∀ (i : σ), s i ∈ S i), Eq.{u_1 + 1} (α := R) ((eval s : (a : MvPolynomial σ R) → R) f : R) (0 : R)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
p q : σ →₀ ℕ
hpq : p + q = t
hq_1 :
  Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u_1, u_2} (R := R)
      (∏ r ∈ S i,
        HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
    q
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
rw : e < #(S i)
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t < HAdd.hAdd (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) p : ℕ) #(S i)

Tactic:
rw [← hpq, map_add, add_lt_add_iff_left, hq, degree_single]

Premises used: map_add, Finsupp.degree_single, add_lt_add_iff_left
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
S : σ → Finset R
htS : ∀ (i : σ), (t : (a : σ) → ℕ) i < #(S i)
x : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval :
  ∀ (s : σ → R) (_ : ∀ (i : σ), s i ∈ S i), Eq.{u_1 + 1} (α := R) ((eval s : (a : MvPolynomial σ R) → R) f : R) (0 : R)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
p q : σ →₀ ℕ
hpq : p + q = t
hq_1 :
  Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u_1, u_2} (R := R)
      (∏ r ∈ S i,
        HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
    q
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
apply : e ≤ (t : (a : σ) → ℕ) i
⊢ e < #(S i)

Tactic:
apply lt_of_le_of_lt _ (htS i)

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
S : σ → Finset R
htS : ∀ (i : σ), (t : (a : σ) → ℕ) i < #(S i)
x : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval :
  ∀ (s : σ → R) (_ : ∀ (i : σ), s i ∈ S i), Eq.{u_1 + 1} (α := R) ((eval s : (a : MvPolynomial σ R) → R) f : R) (0 : R)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
p q : σ →₀ ℕ
hpq : p + q = t
hq_1 :
  Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u_1, u_2} (R := R)
      (∏ r ∈ S i,
        HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
    q
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
⊢ e ≤ (t : (a : σ) → ℕ) i

Tactic:
simp [← hpq, hq]
-- Module: Mathlib.Combinatorics.Optimization.ValuedCSP
Goal:
D : Type u_1
m : ℕ
ω : FractionalOperation D m
valid : ω.IsValid
⊢ ∃ (g : (Fin m → D) → D), g ∈ ω

Tactic:
Multiset.exists_mem_of_ne_zero valid

Premises used: Multiset.exists_mem_of_ne_zero
-- 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
r : Fin 2 → D
rin : r ∈ ω.tt ![![a, b], ![b, a]]
⊢ ∃ a_1 ∈ ω,
    (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)) =
      r

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

Premises used: FractionalOperation.tt, Multiset.mem_map
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
⊢ r = ![r 0, r 1]

Tactic:
simp [← List.ofFn_inj]

Premises used: List.ofFn_inj
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
rw : f ![a, b] < f ![r 0, r 1]
⊢ f ![a, b] < f r

Tactic:
rw [show r = ![r 0, r 1] by simp [← List.ofFn_inj]]
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
apply : f ![a, b] ≠ f ![r 0, r 1]
⊢ f ![a, b] < f ![r 0, r 1]

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

Premises used: And.right, And.left, OfNat.ofNat, lt_of_le_of_ne
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
inl : ∀ (ha0 : a = r 0) (hb1 : b = r 1), r 0 ≠ r 1
inr : ∀ (ha1 : a = r 1) (hb0 : b = r 0), r 0 ≠ r 1
⊢ r 0 ≠ r 1

Tactic:
rcases (mcf.right (r 0) (r 1)).right equ with ⟨ha0, hb1⟩ | ⟨ha1, hb0⟩

Premises used: And.right, OfNat.ofNat
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      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
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
hab₁ : r 0 ≠ r 1
⊢ ∃ a_1 ∈ ω,
    (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)) =
      r

Tactic:
rw [ha0, hb1] at hab
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
hab₁ : r 0 ≠ r 1
rin₁ :
  ∃ a_1 ∈ ω,
    (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)) =
      r
⊢ f ![a, b] = f ![r 0, r 1]

Tactic:
rw [ha0, hb1] at hab
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
hab₁ : r 0 ≠ r 1
rin₁ :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ₁ : f ![a, b] = f ![r 0, r 1]
⊢ a = r 0

Tactic:
rw [ha0, hb1] at hab
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
hab₁ : r 0 ≠ r 1
rin₁ :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ₁ : f ![a, b] = f ![r 0, r 1]
ha0₁ : a = r 0
⊢ b = r 1

Tactic:
rw [ha0, hb1] at hab
-- 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
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
hab : r 0 ≠ r 1
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
⊢ r 0 ≠ r 1

Tactic:
hab
-- 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
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
hab : r 0 ≠ r 1
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
⊢ r 0 ≠ r 1

Tactic:
exact hab
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
⊢ r 1 ≠ r 0

Tactic:
rw [ha1, hb0] at hab
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
hab₁ : r 1 ≠ r 0
⊢ ∃ a_1 ∈ ω,
    (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)) =
      r

Tactic:
rw [ha1, hb0] at hab
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
hab₁ : r 1 ≠ r 0
rin₁ :
  ∃ a_1 ∈ ω,
    (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)) =
      r
⊢ f ![a, b] = f ![r 0, r 1]

Tactic:
rw [ha1, hb0] at hab
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
hab₁ : r 1 ≠ r 0
rin₁ :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ₁ : f ![a, b] = f ![r 0, r 1]
⊢ a = r 1

Tactic:
rw [ha1, hb0] at hab
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
hab₁ : r 1 ≠ r 0
rin₁ :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ₁ : f ![a, b] = f ![r 0, r 1]
ha1₁ : a = r 1
⊢ b = r 0

Tactic:
rw [ha1, hb0] at hab
-- 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
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
hab : r 1 ≠ r 0
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
⊢ r 0 ≠ r 1

Tactic:
hab.symm

Premises used: Ne.symm
-- 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
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
hab : r 1 ≠ r 0
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      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

Premises used: Ne.symm
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
⊢ r 0 ≠ r 1

Tactic:
have asymm : r 0 ≠ r 1 := by
    rcases (mcf.right (r 0) (r 1)).right equ with ⟨ha0, hb1⟩ | ⟨ha1, hb0⟩
    · rw [ha0, hb1] at hab
      exact hab
    · rw [ha1, hb0] at hab
      exact hab.symm
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
asymm : r 0 ≠ r 1
apply : r 0 = r 1
⊢ False

Tactic:
apply asymm
-- 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
r : Fin 2 → D
rin :
  ∃ a_1 ∈ ω,
    (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)) =
      r
equ : f ![a, b] = f ![r 0, r 1]
asymm : r 0 ≠ r 1
obtain :
  ∀ (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)),
    Eq.{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)
⊢ r 0 = r 1

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

Premises used: rfl
-- 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)
change : (o fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 0) = o fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 1
⊢ Eq.{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)

Tactic:
change o (fun j => ![![a, b], ![b, a]] j 0) = o (fun j => ![![a, b], ![b, a]] j 1)

Premises used: Matrix.vecEmpty, OfNat.ofNat, 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)
⊢ (List.ofFn ![a, b]).Perm (List.ofFn ![b, a])

Tactic:
simp [List.Perm.swap]

Premises used: List.Perm.swap