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

Proof state:
case h_1.h_2.intro
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝¹ : Option (Constraint × Coeffs)
hp : positivize? (s, x) = none
x✝ : Option (Constraint × Coeffs)
hn : normalize? (s, x) = some (normalizeConstraint s x, normalizeCoeffs s x)
⊢ ((some (normalizeConstraint s x, normalizeCoeffs s x)).getD (s, x)).fst.sat'
      ((some (normalizeConstraint s x, normalizeCoeffs s x)).getD (s, x)).snd v =
    true

Tactic:
exact normalize_sat w

Result:
no goals

Proof state:
s : Constraint
x v : Coeffs
w : s.sat' x v = true
⊢ ((match positivize? (s, x) with
              | none =>
                match normalize? (s, x) with
                | none => none
                | some (s', x') => some (s', x')
              | some (s', x') => some (normalize (s', x'))).getD
            (s, x)).fst.sat'
      ((match positivize? (s, x) with
            | none =>
              match normalize? (s, x) with
              | none => none
              | some (s', x') => some (s', x')
            | some (s', x') => some (normalize (s', x'))).getD
          (s, x)).snd
      v =
    true

Tactic:
split <;> rename_i hp

Result:
case h_1
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝ : Option (Constraint × Coeffs)
hp : positivize? (s, x) = none
⊢ ((match normalize? (s, x) with
              | none => none
              | some (s', x') => some (s', x')).getD
            (s, x)).fst.sat'
      ((match normalize? (s, x) with
            | none => none
            | some (s', x') => some (s', x')).getD
          (s, x)).snd
      v =
    true

case h_2
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝ : Option (Constraint × Coeffs)
s'✝ : Constraint
x'✝ : Coeffs
hp : positivize? (s, x) = some (s'✝, x'✝)
⊢ ((some (normalize (s'✝, x'✝))).getD (s, x)).fst.sat' ((some (normalize (s'✝, x'✝))).getD (s, x)).snd v = true

Proof state:
case h_1.h_2
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝¹ : Option (Constraint × Coeffs)
hp : positivize? (s, x) = none
x✝ : Option (Constraint × Coeffs)
s'✝ : Constraint
x'✝ : Coeffs
hn : normalize? (s, x) = some (s'✝, x'✝)
⊢ ((some (s'✝, x'✝)).getD (s, x)).fst.sat' ((some (s'✝, x'✝)).getD (s, x)).snd v = true

Tactic:
rcases normalize?_eq_some hn with ⟨rfl, rfl⟩

Result:
case h_1.h_2.intro
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝¹ : Option (Constraint × Coeffs)
hp : positivize? (s, x) = none
x✝ : Option (Constraint × Coeffs)
hn : normalize? (s, x) = some (normalizeConstraint s x, normalizeCoeffs s x)
⊢ ((some (normalizeConstraint s x, normalizeCoeffs s x)).getD (s, x)).fst.sat'
      ((some (normalizeConstraint s x, normalizeCoeffs s x)).getD (s, x)).snd v =
    true

Proof state:
case h_2.intro
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝ : Option (Constraint × Coeffs)
hp : positivize? (s, x) = some (positivizeConstraint s x, positivizeCoeffs s x)
⊢ ((some (normalize (positivizeConstraint s x, positivizeCoeffs s x))).getD (s, x)).fst.sat'
      ((some (normalize (positivizeConstraint s x, positivizeCoeffs s x))).getD (s, x)).snd v =
    true

Tactic:
exact normalize_sat (positivize_sat w)

Result:
no goals

Proof state:
case h_2
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝ : Option (Constraint × Coeffs)
s'✝ : Constraint
x'✝ : Coeffs
hp : positivize? (s, x) = some (s'✝, x'✝)
⊢ ((some (normalize (s'✝, x'✝))).getD (s, x)).fst.sat' ((some (normalize (s'✝, x'✝))).getD (s, x)).snd v = true

Tactic:
rcases positivize?_eq_some hp with ⟨rfl, rfl⟩

Result:
case h_2.intro
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝ : Option (Constraint × Coeffs)
hp : positivize? (s, x) = some (positivizeConstraint s x, positivizeCoeffs s x)
⊢ ((some (normalize (positivizeConstraint s x, positivizeCoeffs s x))).getD (s, x)).fst.sat'
      ((some (normalize (positivizeConstraint s x, positivizeCoeffs s x))).getD (s, x)).snd v =
    true

Proof state:
case h_1.h_1
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝¹ : Option (Constraint × Coeffs)
hp : positivize? (s, x) = none
x✝ : Option (Constraint × Coeffs)
hn : normalize? (s, x) = none
⊢ (none.getD (s, x)).fst.sat' (none.getD (s, x)).snd v = true

Tactic:
simp_all

Result:
no goals

Proof state:
case h_1
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝ : Option (Constraint × Coeffs)
hp : positivize? (s, x) = none
⊢ ((match normalize? (s, x) with
              | none => none
              | some (s', x') => some (s', x')).getD
            (s, x)).fst.sat'
      ((match normalize? (s, x) with
            | none => none
            | some (s', x') => some (s', x')).getD
          (s, x)).snd
      v =
    true

Tactic:
split <;> rename_i hn

Result:
case h_1.h_1
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝¹ : Option (Constraint × Coeffs)
hp : positivize? (s, x) = none
x✝ : Option (Constraint × Coeffs)
hn : normalize? (s, x) = none
⊢ (none.getD (s, x)).fst.sat' (none.getD (s, x)).snd v = true

case h_1.h_2
s : Constraint
x v : Coeffs
w : s.sat' x v = true
x✝¹ : Option (Constraint × Coeffs)
hp : positivize? (s, x) = none
x✝ : Option (Constraint × Coeffs)
s'✝ : Constraint
x'✝ : Coeffs
hn : normalize? (s, x) = some (s'✝, x'✝)
⊢ ((some (s'✝, x'✝)).getD (s, x)).fst.sat' ((some (s'✝, x'✝)).getD (s, x)).snd v = true

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

Tactic:
dsimp [tidyConstraint, tidyCoeffs, tidy, tidy?]

Result:
s : Constraint
x v : Coeffs
w : s.sat' x v = true
⊢ ((match positivize? (s, x) with
              | none =>
                match normalize? (s, x) with
                | none => none
                | some (s', x') => some (s', x')
              | some (s', x') => some (normalize (s', x'))).getD
            (s, x)).fst.sat'
      ((match positivize? (s, x) with
            | none =>
              match normalize? (s, x) with
              | none => none
              | some (s', x') => some (s', x')
            | some (s', x') => some (normalize (s', x'))).getD
          (s, x)).snd
      v =
    true