internlm/Lean-Github huggingface dataset:
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f1 f2

case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f2 f1
Tactic:
. intro p
  rw [h p]
  exact id
Proof state after:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f2 f1
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f2 f1
Tactic:
. intro p
  rw [h p]
  exact id
Proof state after:
no goals
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f1 f2
Tactic:
intro p
Proof state after:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f1 → p ⊨ f2
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f1 → p ⊨ f2
Tactic:
rw [h p]
Proof state after:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f2
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f2
Tactic:
exact id
Proof state after:
no goals
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f2 f1
Tactic:
intro p
Proof state after:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Tactic:
rw [h p]
Proof state after:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f2
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f2
Tactic:
exact id
Proof state after:
no goals
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ limplies α f1 f2 ∧ limplies α f2 f1 → liff α f1 f2
Tactic:
intros h p
Proof state after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f1 ↔ p ⊨ f2
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f1 ↔ p ⊨ f2
Tactic:
constructor
Proof state after:
case mpr.mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f1 → p ⊨ f2

case mpr.mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mpr.mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f1 → p ⊨ f2

case mpr.mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Tactic:
. exact h.1 p
Proof state after:
case mpr.mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mpr.mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Tactic:
. exact h.2 p
Proof state after:
no goals
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mpr.mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f1 → p ⊨ f2
Tactic:
exact h.1 p
Proof state after:
no goals
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mpr.mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Tactic:
exact h.2 p
Proof state after:
no goals
Theorem: Sat.liff_unsat
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f1 ↔ unsatisfiable α f2
Tactic:
constructor
Proof state after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f1 → unsatisfiable α f2

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f2 → unsatisfiable α f1
Theorem: Sat.liff_unsat
Proof state before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f1 → unsatisfiable α f2

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f2 → unsatisfiable α f1
Tactic:
. intros f1_unsat p p_entails_f2
  rw [← h p] at p_entails_f2
  exact f1_unsat p p_entails_f2
Proof state after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f2 → unsatisfiable α f1
Theorem: Sat.liff_unsat
Proof state before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f2 → unsatisfiable α f1
Tactic:
. intros f2_unsat p p_entails_f1
  rw [h p] at p_entails_f1
  exact f2_unsat p p_entails_f1
Proof state after:
no goals
Theorem: Sat.liff_unsat
Proof state before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f1 → unsatisfiable α f2
Tactic:
intros f1_unsat p p_entails_f2
Proof state after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f2
⊢ False
Theorem: Sat.liff_unsat
Proof state before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f2
⊢ False
Tactic:
rw [← h p] at p_entails_f2
Proof state after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f1
⊢ False
Theorem: Sat.liff_unsat
Proof state before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f1
⊢ False
Tactic:
exact f1_unsat p p_entails_f2
Proof state after:
no goals
Theorem: Sat.liff_unsat
Proof state before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f2 → unsatisfiable α f1
Tactic:
intros f2_unsat p p_entails_f1
Proof state after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f2_unsat : unsatisfiable α f2
p : α → Bool
p_entails_f1 : p ⊨ f1
⊢ False
Theorem: Sat.liff_unsat
Proof state before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f2_unsat : unsatisfiable α f2
p : α → Bool
p_entails_f1 : p ⊨ f1
⊢ False
Tactic:
rw [h p] at p_entails_f1
Proof state after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f2_unsat : unsatisfiable α f2
p : α → Bool
p_entails_f1 : p ⊨ f2
⊢ False
Theorem: Sat.liff_unsat
Proof state before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f2_unsat : unsatisfiable α f2
p : α → Bool
p_entails_f1 : p ⊨ f2
⊢ False
Tactic:
exact f2_unsat p p_entails_f1
Proof state after:
no goals
Theorem: Sat.limplies_unsat
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f2 f1
⊢ unsatisfiable α f1 → unsatisfiable α f2
Tactic:
intros f1_unsat p p_entails_f2
Proof state after:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f2 f1
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f2
⊢ False
Theorem: Sat.limplies_unsat
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f2 f1
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f2
⊢ False
Tactic:
exact f1_unsat p $ h p p_entails_f2
Proof state after:
no goals
Theorem: Sat.incompatible_of_unsat
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ unsatisfiable α f1 → incompatible α f1 f2
Tactic:
intro h p
Proof state after:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : unsatisfiable α f1
p : α → Bool
⊢ ¬(p ⊨ f1) ∨ ¬(p ⊨ f2)
Theorem: Sat.incompatible_of_unsat
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : unsatisfiable α f1
p : α → Bool
⊢ ¬(p ⊨ f1) ∨ ¬(p ⊨ f2)
Tactic:
exact Or.inl $ h p
Proof state after:
no goals
Theorem: Sat.unsat_of_limplies_and_incompatible
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ limplies α f1 f2 → incompatible α f1 f2 → unsatisfiable α f1
Tactic:
intro h1 h2 p pf1
Proof state after:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
⊢ False
Theorem: Sat.unsat_of_limplies_and_incompatible
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
⊢ False
Tactic:
cases h2 p
Proof state after:
case inl
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f1)
⊢ False

case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f2)
⊢ False
Theorem: Sat.unsat_of_limplies_and_incompatible
Proof state before:
case inl
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f1)
⊢ False

case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f2)
⊢ False
Tactic:
. next h2 =>
  exact h2 pf1
Proof state after:
case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f2)
⊢ False
Theorem: Sat.unsat_of_limplies_and_incompatible
Proof state before:
case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f2)
⊢ False
Tactic:
. next h2 =>
  exact h2 $ h1 p pf1
Proof state after:
no goals
Theorem: Sat.unsat_of_limplies_and_incompatible
Proof state before:
case inl
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f1)
⊢ False
Tactic:
next h2 =>
exact h2 pf1
Proof state after:
no goals
Theorem: Sat.unsat_of_limplies_and_incompatible
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2✝ : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h2 : ¬(p ⊨ f1)
⊢ False
Tactic:
exact h2 pf1
Proof state after:
no goals
Theorem: Sat.unsat_of_limplies_and_incompatible
Proof state before:
case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f2)
⊢ False
Tactic:
next h2 =>
exact h2 $ h1 p pf1
Proof state after:
no goals
Theorem: Sat.unsat_of_limplies_and_incompatible
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2✝ : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h2 : ¬(p ⊨ f2)
⊢ False
Tactic:
exact h2 $ h1 p pf1
Proof state after:
no goals
Theorem: Sat.incompatible.symm
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f1 f2 ↔ incompatible α f2 f1
Tactic:
constructor
Proof state after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f1 f2 → incompatible α f2 f1

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f2 f1 → incompatible α f1 f2
Theorem: Sat.incompatible.symm
Proof state before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f1 f2 → incompatible α f2 f1

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f2 f1 → incompatible α f1 f2
Tactic:
. intro h p
  exact Or.symm $ h p
Proof state after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f2 f1 → incompatible α f1 f2
Theorem: Sat.incompatible.symm
Proof state before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f2 f1 → incompatible α f1 f2
Tactic:
. intro h p
  exact Or.symm $ h p
Proof state after:
no goals
Theorem: Sat.incompatible.symm
Proof state before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f1 f2 → incompatible α f2 f1
Tactic:
intro h p
Proof state after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : incompatible α f1 f2
p : α → Bool
⊢ ¬(p ⊨ f2) ∨ ¬(p ⊨ f1)
Theorem: Sat.incompatible.symm
Proof state before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : incompatible α f1 f2
p : α → Bool
⊢ ¬(p ⊨ f2) ∨ ¬(p ⊨ f1)
Tactic:
exact Or.symm $ h p
Proof state after:
no goals
Theorem: Sat.incompatible.symm
Proof state before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f2 f1 → incompatible α f1 f2
Tactic:
intro h p
Proof state after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : incompatible α f2 f1
p : α → Bool
⊢ ¬(p ⊨ f1) ∨ ¬(p ⊨ f2)
Theorem: Sat.incompatible.symm
Proof state before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : incompatible α f2 f1
p : α → Bool
⊢ ¬(p ⊨ f1) ∨ ¬(p ⊨ f2)
Tactic:
exact Or.symm $ h p
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.IsPrefix_aig
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ IsPrefix aig.decls (f aig input).aig.decls
Tactic:
apply IsPrefix.of
Proof state after:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]

case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Theorem: AIG.LawfulStreamOperator.IsPrefix_aig
Proof state before:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]

case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. intro idx h
  apply decl_eq
Proof state after:
case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Theorem: AIG.LawfulStreamOperator.IsPrefix_aig
Proof state before:
case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. apply le_size
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.IsPrefix_aig
Proof state before:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]
Tactic:
intro idx h
Proof state after:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
idx : Nat
h : idx < aig.decls.size
⊢ (f aig input).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.LawfulStreamOperator.IsPrefix_aig
Proof state before:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
idx : Nat
h : idx < aig.decls.size
⊢ (f aig input).aig.decls[idx] = aig.decls[idx]
Tactic:
apply decl_eq
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.IsPrefix_aig
Proof state before:
case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
apply le_size
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.lt_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Tactic:
have h1 := entry.ref.hgate
Proof state after:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Theorem: AIG.LawfulStreamOperator.lt_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Tactic:
have h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size := by
  apply le_size
Proof state after:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Theorem: AIG.LawfulStreamOperator.lt_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.lt_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
Tactic:
apply le_size
Proof state after:
no goals