awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t < HAdd.hAdd (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) p : ℕ) #(S i)
have rw : e < #(S i)
Tactic: rw [← hpq, map_add, add_lt_add_iff_left, hq, degree_single]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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 < #(S i)
have apply : e ≤ (t : (a : σ) → ℕ) i
Tactic: apply lt_of_le_of_lt _ (htS i)
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
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]]
⊢ f ![a, b] < f r
have 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
Tactic: rw [FractionalOperation.tt, Multiset.mem_map] at rin
Cleared hypotheses: rin
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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
⊢ f ![a, b] < f r
have rw : f ![a, b] < f ![r 0, r 1]
Tactic: rw [show r = ![r 0, r 1] by simp [← List.ofFn_inj]]
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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
⊢ f ![a, b] < f ![r 0, r 1]
have apply : f ![a, b] ≠ f ![r 0, r 1]
Tactic: apply lt_of_le_of_ne (mcf.right (r 0) (r 1)).left
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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
have inl : ∀ (ha0 : a = r 0) (hb1 : b = r 1), r 0 ≠ r 1
Tactic: rcases (mcf.right (r 0) (r 1)).right equ with ⟨ha0, hb1⟩ | ⟨ha1, hb0⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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
⊢ r 0 ≠ r 1
have inr : ∀ (ha1 : a = r 1) (hb0 : b = r 0), r 0 ≠ r 1
Tactic: rcases (mcf.right (r 0) (r 1)).right equ with ⟨ha0, hb1⟩ | ⟨ha1, hb0⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
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 0 ≠ r 1
have hab₁ : r 1 ≠ r 0
Tactic: rw [ha1, hb0] at hab
Cleared hypotheses: hab, rin, equ, ha1, hb0
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
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]
⊢ False
have asymm : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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
⊢ False
have apply : r 0 = r 1
Tactic: apply asymm
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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
⊢ r 0 = r 1
have 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)
Tactic: obtain ⟨o, in_omega, rfl⟩ := rin
Cleared hypotheses: r, rin, equ, asymm
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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)
⊢ 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)
have change : (o fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 0) = o fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 1
Tactic: change o (fun j => ![![a, b], ![b, a]] j 0) = o (fun j => ![![a, b], ![b, a]] j 1)
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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)
⊢ (o fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 0) = o fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 1
have h : (fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 0) = ![a, b]
Tactic: convert! symmega ![a, b] ![b, a] (by simp [List.Perm.swap]) o in_omega using 2
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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]
⊢ (o fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 0) = o fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 1
have h₁ : (fun (j : Fin 2) ↦ ![![a, b], ![b, a]] j 1) = ![b, a]
Tactic: convert! symmega ![a, b] ![b, a] (by simp [List.Perm.swap]) o in_omega using 2
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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 ω
⊢ False
have obtain : ∀ (a b : D) (hab : a ≠ b) (mcfab : HasMaxCutPropertyAt f a b), False
Tactic: obtain ⟨a, b, hab, mcfab⟩ := mcf
Cleared hypotheses: mcf
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
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
⊢ False
have 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))
Tactic: specialize contr ![![a, b], ![b, a]]
Cleared hypotheses: contr
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
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))
⊢ False
have contr₁ : 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
Cleared hypotheses: contr
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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
have hle : ∀ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] ≤ f i
Tactic: apply Multiset.sum_lt_sum
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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
⊢ 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
have hlt : ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i
Tactic: apply Multiset.sum_lt_sum
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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])
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i
have hlt : ∀ g ∈ ω, ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i
Tactic: obtain ⟨g, _⟩ := valid.contains
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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]]
have 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)
Tactic: simp only [FractionalOperation.tt, Multiset.mem_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
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 ∈ ω
w : (Fin 2 → D) → D
⊢ ∃ 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)
have 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)
Tactic: use g
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
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 ∈ ω
⊢ ∃ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] < f i
have 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]]
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
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
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
have 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
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⟩