Theorem: CNF.Clause.mem_lrat_of_mem (LeanSAT/Reflect/Glue.lean)

State before:
case nil
n : Nat
l : PosFin n × Bool
lratClause : LRAT.DefaultClause n
h1 : l ∈ []
h2 : LRAT.DefaultClause.ofArray #[] = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
cases h1
State after:
no goals

State before:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 : LRAT.DefaultClause.ofArray (List.toArray (hd :: tl)) = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
unfold LRAT.DefaultClause.ofArray at h2
State after:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray (hd :: tl)) (List.toArray (hd :: tl)).size) =
    some lratClause
⊢ l ∈ lratClause.clause

State before:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray (hd :: tl)) (List.toArray (hd :: tl)).size) =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
rw [Array.foldr_eq_foldr_data,Array.toArray_data] at h2
State after:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := hd :: tl }.data =
    some lratClause
⊢ l ∈ lratClause.clause

State before:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := hd :: tl }.data =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
dsimp only [List.foldr] at h2
State after:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  (match
      List.foldr
        (fun l acc =>
          match acc with
          | none => none
          | some acc => acc.insert l)
        (some LRAT.DefaultClause.empty) tl with
    | none => none
    | some acc => acc.insert hd) =
    some lratClause
⊢ l ∈ lratClause.clause

State before:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  (match
      List.foldr
        (fun l acc =>
          match acc with
          | none => none
          | some acc => acc.insert l)
        (some LRAT.DefaultClause.empty) tl with
    | none => none
    | some acc => acc.insert hd) =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
split at h2
State after:
case cons.h_1
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝ : Option (LRAT.DefaultClause n)
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    none
h2 : none = some lratClause
⊢ l ∈ lratClause.clause

case cons.h_2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 : acc✝.insert hd = some lratClause
⊢ l ∈ lratClause.clause

State before:
case cons.h_1
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝ : Option (LRAT.DefaultClause n)
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    none
h2 : none = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
cases h2
State after:
no goals

State before:
case cons.h_2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 : acc✝.insert hd = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
rw [LRAT.DefaultClause.insert] at h2
State after:
case cons.h_2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 :
  (if heq1 : acc✝.clause.contains (hd.fst, !hd.snd) = true then none
    else
      if heq2 : acc✝.clause.contains hd = true then some acc✝
      else
        let clause := hd :: acc✝.clause;
        let_fun nodupkey := ⋯;
        let_fun nodup := ⋯;
        some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause

State before:
case cons.h_2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 :
  (if heq1 : acc✝.clause.contains (hd.fst, !hd.snd) = true then none
    else
      if heq2 : acc✝.clause.contains hd = true then some acc✝
      else
        let clause := hd :: acc✝.clause;
        let_fun nodupkey := ⋯;
        let_fun nodup := ⋯;
        some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
split at h2
State after:
case cons.h_2.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : acc✝.clause.contains (hd.fst, !hd.snd) = true
h2 : False
⊢ l ∈ lratClause.clause

case cons.h_2.isFalse
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h2 :
  (if heq2 : acc✝.clause.contains hd = true then some acc✝
    else
      let clause := hd :: acc✝.clause;
      let_fun nodupkey := ⋯;
      let_fun nodup := ⋯;
      some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause

State before:
case cons.h_2.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : acc✝.clause.contains (hd.fst, !hd.snd) = true
h2 : False
⊢ l ∈ lratClause.clause
Tactic:
cases h2
State after:
no goals

State before:
case cons.h_2.isFalse
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h2 :
  (if heq2 : acc✝.clause.contains hd = true then some acc✝
    else
      let clause := hd :: acc✝.clause;
      let_fun nodupkey := ⋯;
      let_fun nodup := ⋯;
      some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
split at h2
State after:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : acc✝.clause.contains hd = true
h2 : some acc✝ = some lratClause
⊢ l ∈ lratClause.clause

case cons.h_2.isFalse.isFalse
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 :
  (let clause := hd :: acc✝.clause;
    let_fun nodupkey := ⋯;
    let_fun nodup := ⋯;
    some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause

State before:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : acc✝.clause.contains hd = true
h2 : some acc✝ = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
rename_i h
State after:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some lratClause
⊢ l ∈ lratClause.clause

State before:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
rw [<-Option.some.inj h2] at *
State after:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
⊢ l ∈ acc✝.clause

State before:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
⊢ l ∈ acc✝.clause
Tactic:
cases h1
State after:
case cons.h_2.isFalse.isTrue.head
n : Nat
l : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 : some acc✝ = some acc✝
h✝ : ¬acc✝.clause.contains (l.fst, !l.snd) = true
h : acc✝.clause.contains l = true
⊢ l ∈ acc✝.clause

case cons.h_2.isFalse.isTrue.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ l ∈ acc✝.clause

State before:
case cons.h_2.isFalse.isTrue.head
n : Nat
l : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 : some acc✝ = some acc✝
h✝ : ¬acc✝.clause.contains (l.fst, !l.snd) = true
h : acc✝.clause.contains l = true
⊢ l ∈ acc✝.clause
Tactic:
exact List.mem_of_elem_eq_true h
State after:
no goals

State before:
case cons.h_2.isFalse.isTrue.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ l ∈ acc✝.clause
Tactic:
apply ih
State after:
case cons.h_2.isFalse.isTrue.tail.h1
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ l ∈ tl

case cons.h_2.isFalse.isTrue.tail.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ LRAT.DefaultClause.ofArray (List.toArray tl) = some acc✝

State before:
case cons.h_2.isFalse.isTrue.tail.h1
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ l ∈ tl
Tactic:
assumption
State after:
no goals

State before:
case cons.h_2.isFalse.isTrue.tail.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ LRAT.DefaultClause.ofArray (List.toArray tl) = some acc✝
Tactic:
next heq _ _ =>
unfold LRAT.DefaultClause.ofArray
rw [Array.foldr_eq_foldr_data,Array.toArray_data]
exact heq
State after:
no goals

State before:
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ LRAT.DefaultClause.ofArray (List.toArray tl) = some acc✝
Tactic:
unfold LRAT.DefaultClause.ofArray
State after:
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray tl) (List.toArray tl).size) =
    some acc✝

State before:
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray tl) (List.toArray tl).size) =
    some acc✝
Tactic:
rw [Array.foldr_eq_foldr_data,Array.toArray_data]
State after:
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := tl }.data =
    some acc✝

State before:
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := tl }.data =
    some acc✝
Tactic:
exact heq
State after:
no goals

State before:
case cons.h_2.isFalse.isFalse
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 :
  (let clause := hd :: acc✝.clause;
    let_fun nodupkey := ⋯;
    let_fun nodup := ⋯;
    some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
cases h1
State after:
case cons.h_2.isFalse.isFalse.head
n : Nat
l : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (l.fst, !l.snd) = true
h✝ : ¬acc✝.clause.contains l = true
h2 :
  (let clause := l :: acc✝.clause;
    let_fun nodupkey := ⋯;
    let_fun nodup := ⋯;
    some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause

case cons.h_2.isFalse.isFalse.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 :
  (let clause := hd :: acc✝.clause;
    let_fun nodupkey := ⋯;
    let_fun nodup := ⋯;
    some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
a✝ : List.Mem l tl
⊢ l ∈ lratClause.clause

State before:
case cons.h_2.isFalse.isFalse.head
n : Nat
l : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (l.fst, !l.snd) = true
h✝ : ¬acc✝.clause.contains l = true
h2 :
  (let clause := l :: acc✝.clause;
    let_fun nodupkey := ⋯;
    let_fun nodup := ⋯;
    some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
simp only [<-Option.some.inj h2]
State after:
case cons.h_2.isFalse.isFalse.head
n : Nat
l : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (l.fst, !l.snd) = true
h✝ : ¬acc✝.clause.contains l = true
h2 :
  (let clause := l :: acc✝.clause;
    let_fun nodupkey := ⋯;
    let_fun nodup := ⋯;
    some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ l :: acc✝.clause

State before:
case cons.h_2.isFalse.isFalse.head
n : Nat
l : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (l.fst, !l.snd) = true
h✝ : ¬acc✝.clause.contains l = true
h2 :
  (let clause := l :: acc✝.clause;
    let_fun nodupkey := ⋯;
    let_fun nodup := ⋯;
    some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ l :: acc✝.clause
Tactic:
constructor
State after:
no goals

State before:
case cons.h_2.isFalse.isFalse.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 :
  (let clause := hd :: acc✝.clause;
    let_fun nodupkey := ⋯;
    let_fun nodup := ⋯;
    some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
a✝ : List.Mem l tl
⊢ l ∈ lratClause.clause
Tactic:
simp only at h2
State after:
case cons.h_2.isFalse.isFalse.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ l ∈ lratClause.clause

State before:
case cons.h_2.isFalse.isFalse.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ l ∈ lratClause.clause
Tactic:
simp only [<-Option.some.inj h2]
State after:
case cons.h_2.isFalse.isFalse.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ l ∈ hd :: acc✝.clause

State before:
case cons.h_2.isFalse.isFalse.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ l ∈ hd :: acc✝.clause
Tactic:
rename_i heq _ _ _
State after:
case cons.h_2.isFalse.isFalse.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ l ∈ hd :: acc✝.clause

State before:
case cons.h_2.isFalse.isFalse.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ l ∈ hd :: acc✝.clause
Tactic:
apply List.Mem.tail
State after:
case cons.h_2.isFalse.isFalse.tail.a
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ List.Mem l acc✝.clause

State before:
case cons.h_2.isFalse.isFalse.tail.a
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ List.Mem l acc✝.clause
Tactic:
apply ih
State after:
case cons.h_2.isFalse.isFalse.tail.a.h1
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ l ∈ tl

case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ LRAT.DefaultClause.ofArray (List.toArray tl) = some acc✝

State before:
case cons.h_2.isFalse.isFalse.tail.a.h1
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ l ∈ tl

case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ LRAT.DefaultClause.ofArray (List.toArray tl) = some acc✝
Tactic:
assumption
State after:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ LRAT.DefaultClause.ofArray (List.toArray tl) = some acc✝

State before:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ LRAT.DefaultClause.ofArray (List.toArray tl) = some acc✝
Tactic:
unfold LRAT.DefaultClause.ofArray
State after:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray tl) (List.toArray tl).size) =
    some acc✝

State before:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray tl) (List.toArray tl).size) =
    some acc✝
Tactic:
rw [Array.foldr_eq_foldr_data,Array.toArray_data]
State after:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := tl }.data =
    some acc✝

State before:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := tl }.data =
    some acc✝
Tactic:
exact heq
State after:
no goals