-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem limplies_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n)
    (f_AssignmentsInvariant : AssignmentsInvariant f) :
    Limplies (PosFin n) f f.assignments

Proof state:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
⊢ i.val < f.assignments.size

Tactic:
rw [hsize]

Result:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
⊢ i.val < n

Proof state:
n : Nat
f : DefaultFormula n
f_AssignmentsInvariant : f.AssignmentsInvariant
⊢ Limplies (PosFin n) f f.assignments

Tactic:
intro p pf

Result:
n : Nat
f : DefaultFormula n
f_AssignmentsInvariant : f.AssignmentsInvariant
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.assignments

Proof state:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
h : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Tactic:
simp_all [getElem!, i.2.2, decidableGetElem?]

Result:
no goals

Proof state:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_AssignmentsInvariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → Limplies (PosFin n) f (i, b)
⊢ ∀ (i : PosFin n), hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Tactic:
intro i

Result:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_AssignmentsInvariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → Limplies (PosFin n) f (i, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Proof state:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Tactic:
by_cases hasAssignment (decide (p i = false)) (f.assignments[i.1]'(by rw [hsize]; exact i.2.2))

Result:
case pos
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
h✝ : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Proof state:
n : Nat
f : DefaultFormula n
f_AssignmentsInvariant : f.AssignmentsInvariant
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.assignments

Tactic:
rcases f_AssignmentsInvariant with ⟨hsize, f_AssignmentsInvariant⟩

Result:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_AssignmentsInvariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → Limplies (PosFin n) f (i, b)
⊢ p ⊨ f.assignments

Proof state:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
h : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
f_AssignmentsInvariant : p ⊨ (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Tactic:
by_cases hpi : p i <;> simp [hpi, Entails.eval] at f_AssignmentsInvariant

Result:
no goals

Proof state:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_AssignmentsInvariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → Limplies (PosFin n) f (i, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Tactic:
specialize f_AssignmentsInvariant i (decide (p i = false))

Result:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Proof state:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
⊢ i.val < n

Tactic:
exact i.2.2

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
h : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Tactic:
specialize f_AssignmentsInvariant h p pf

Result:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
h : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
f_AssignmentsInvariant : p ⊨ (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Proof state:
case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Tactic:
next h => simp_all [getElem!, i.2.2, decidableGetElem?]

Result:
no goals

Proof state:
case pos
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_AssignmentsInvariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → Limplies (PosFin n) f (i, decide (p i = false))
h✝ : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

Tactic:
next h =>
specialize f_AssignmentsInvariant h p pf
by_cases hpi : p i <;> simp [hpi, Entails.eval] at f_AssignmentsInvariant

Result:
no goals