-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem normalize_sat {s x v} (w : s.sat' x v) :
    (normalizeConstraint s x).sat' (normalizeCoeffs s x) v

Proof state:
case isTrue.isTrue
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : x.gcd = 0
h✝ : s.sat 0 = true
⊢ ((some (Constraint.trivial, x)).getD (s, x)).fst.sat' ((some (Constraint.trivial, x)).getD (s, x)).snd v = true

Tactic:
simp

Result:
no goals

Proof state:
case isTrue.isFalse
s : Constraint
x v : Coeffs
h✝ : ¬s.sat 0 = true
h : ∀ (x_1 : Int), x_1 ∈ x → x_1 = 0
w : s.sat 0 = true
⊢ ((some (Constraint.impossible, x)).getD (s, x)).fst.sat' ((some (Constraint.impossible, x)).getD (s, x)).snd v = true

Tactic:
simp_all

Result:
no goals

Proof state:
case isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : ¬x.gcd = 0
⊢ ((if x.gcd = 1 then none else some (s.div x.gcd, x.sdiv ↑x.gcd)).getD (s, x)).fst.sat'
      ((if x.gcd = 1 then none else some (s.div x.gcd, x.sdiv ↑x.gcd)).getD (s, x)).snd v =
    true

Tactic:
split

Result:
case isFalse.isTrue
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : ¬x.gcd = 0
h✝ : x.gcd = 1
⊢ (none.getD (s, x)).fst.sat' (none.getD (s, x)).snd v = true

case isFalse.isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : ¬x.gcd = 0
h✝ : ¬x.gcd = 1
⊢ ((some (s.div x.gcd, x.sdiv ↑x.gcd)).getD (s, x)).fst.sat' ((some (s.div x.gcd, x.sdiv ↑x.gcd)).getD (s, x)).snd v =
    true

Proof state:
case isTrue.isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : x.gcd = 0
h✝ : ¬s.sat 0 = true
⊢ ((some (Constraint.impossible, x)).getD (s, x)).fst.sat' ((some (Constraint.impossible, x)).getD (s, x)).snd v = true

Tactic:
dsimp [Constraint.sat'] at w

Result:
case isTrue.isFalse
s : Constraint
x v : Coeffs
w : s.sat (x.dot v) = true
h : x.gcd = 0
h✝ : ¬s.sat 0 = true
⊢ ((some (Constraint.impossible, x)).getD (s, x)).fst.sat' ((some (Constraint.impossible, x)).getD (s, x)).snd v = true

Proof state:
s : Constraint
x v : Coeffs
w : s.sat' x v = true
⊢ ((if x.gcd = 0 then if s.sat 0 = true then some (Constraint.trivial, x) else some (Constraint.impossible, x)
              else if x.gcd = 1 then none else some (s.div x.gcd, x.sdiv ↑x.gcd)).getD
            (s, x)).fst.sat'
      ((if x.gcd = 0 then if s.sat 0 = true then some (Constraint.trivial, x) else some (Constraint.impossible, x)
            else if x.gcd = 1 then none else some (s.div x.gcd, x.sdiv ↑x.gcd)).getD
          (s, x)).snd
      v =
    true

Tactic:
split <;> rename_i h

Result:
case isTrue
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : x.gcd = 0
⊢ ((if s.sat 0 = true then some (Constraint.trivial, x) else some (Constraint.impossible, x)).getD (s, x)).fst.sat'
      ((if s.sat 0 = true then some (Constraint.trivial, x) else some (Constraint.impossible, x)).getD (s, x)).snd v =
    true

case isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : ¬x.gcd = 0
⊢ ((if x.gcd = 1 then none else some (s.div x.gcd, x.sdiv ↑x.gcd)).getD (s, x)).fst.sat'
      ((if x.gcd = 1 then none else some (s.div x.gcd, x.sdiv ↑x.gcd)).getD (s, x)).snd v =
    true

Proof state:
case isTrue
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : x.gcd = 0
⊢ ((if s.sat 0 = true then some (Constraint.trivial, x) else some (Constraint.impossible, x)).getD (s, x)).fst.sat'
      ((if s.sat 0 = true then some (Constraint.trivial, x) else some (Constraint.impossible, x)).getD (s, x)).snd v =
    true

Tactic:
split

Result:
case isTrue.isTrue
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : x.gcd = 0
h✝ : s.sat 0 = true
⊢ ((some (Constraint.trivial, x)).getD (s, x)).fst.sat' ((some (Constraint.trivial, x)).getD (s, x)).snd v = true

case isTrue.isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : x.gcd = 0
h✝ : ¬s.sat 0 = true
⊢ ((some (Constraint.impossible, x)).getD (s, x)).fst.sat' ((some (Constraint.impossible, x)).getD (s, x)).snd v = true

Proof state:
case isTrue.isFalse
s : Constraint
x v : Coeffs
w : s.sat (x.dot v) = true
h : x.gcd = 0
h✝ : ¬s.sat 0 = true
⊢ ((some (Constraint.impossible, x)).getD (s, x)).fst.sat' ((some (Constraint.impossible, x)).getD (s, x)).snd v = true

Tactic:
simp only [IntList.gcd_eq_zero] at h

Result:
case isTrue.isFalse
s : Constraint
x v : Coeffs
w : s.sat (x.dot v) = true
h✝ : ¬s.sat 0 = true
h : ∀ (x_1 : Int), x_1 ∈ x → x_1 = 0
⊢ ((some (Constraint.impossible, x)).getD (s, x)).fst.sat' ((some (Constraint.impossible, x)).getD (s, x)).snd v = true

Proof state:
case isFalse.isFalse
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : ¬x.gcd = 0
h✝ : ¬x.gcd = 1
⊢ ((some (s.div x.gcd, x.sdiv ↑x.gcd)).getD (s, x)).fst.sat' ((some (s.div x.gcd, x.sdiv ↑x.gcd)).getD (s, x)).snd v =
    true

Tactic:
exact Constraint.div_sat' h w

Result:
no goals

Proof state:
case isTrue.isFalse
s : Constraint
x v : Coeffs
w : s.sat (x.dot v) = true
h✝ : ¬s.sat 0 = true
h : ∀ (x_1 : Int), x_1 ∈ x → x_1 = 0
⊢ ((some (Constraint.impossible, x)).getD (s, x)).fst.sat' ((some (Constraint.impossible, x)).getD (s, x)).snd v = true

Tactic:
simp only [IntList.dot_eq_zero_of_left_eq_zero h] at w

Result:
case isTrue.isFalse
s : Constraint
x v : Coeffs
h✝ : ¬s.sat 0 = true
h : ∀ (x_1 : Int), x_1 ∈ x → x_1 = 0
w : s.sat 0 = true
⊢ ((some (Constraint.impossible, x)).getD (s, x)).fst.sat' ((some (Constraint.impossible, x)).getD (s, x)).snd v = true

Proof state:
case isFalse.isTrue
s : Constraint
x v : Coeffs
w : s.sat' x v = true
h : ¬x.gcd = 0
h✝ : x.gcd = 1
⊢ (none.getD (s, x)).fst.sat' (none.getD (s, x)).snd v = true

Tactic:
exact w

Result:
no goals

Proof state:
s : Constraint
x v : Coeffs
w : s.sat' x v = true
⊢ (normalizeConstraint s x).sat' (normalizeCoeffs s x) v = true

Tactic:
dsimp [normalizeConstraint, normalizeCoeffs, normalize, normalize?]

Result:
s : Constraint
x v : Coeffs
w : s.sat' x v = true
⊢ ((if x.gcd = 0 then if s.sat 0 = true then some (Constraint.trivial, x) else some (Constraint.impossible, x)
              else if x.gcd = 1 then none else some (s.div x.gcd, x.sdiv ↑x.gcd)).getD
            (s, x)).fst.sat'
      ((if x.gcd = 0 then if s.sat 0 = true then some (Constraint.trivial, x) else some (Constraint.impossible, x)
            else if x.gcd = 1 then none else some (s.div x.gcd, x.sdiv ↑x.gcd)).getD
          (s, x)).snd
      v =
    true