-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈ clause)
    (h2 : DefaultClause.ofArray clause.toArray = some lratClause) : l ∈ lratClause.clause

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

Tactic:
rw [DefaultClause.insert] at h2

Result:
case cons.h_2
n : Nat
l hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ {lratClause : DefaultClause n}, l ∈ tl → DefaultClause.ofArray tl.toArray = some lratClause → l ∈ lratClause.clause
lratClause : DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (DefaultClause n)
acc✝ : DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some DefaultClause.empty) tl =
    some acc✝
h2 :
  (if heq1 : List.contains acc✝.clause (hd.fst, !hd.snd) = true then none
    else
      if heq2 : List.contains acc✝.clause 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

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

Tactic:
assumption

Result:
no goals

Proof state:
case nil
n : Nat
l : Literal (PosFin n)
lratClause : DefaultClause n
h1 : l ∈ []
h2 : DefaultClause.ofArray #[] = some lratClause
⊢ l ∈ lratClause.clause

Tactic:
cases h1

Result:
no goals

Proof state:
case cons.h_2.isFalse.isFalse.tail
n : Nat
l hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ {lratClause : DefaultClause n}, l ∈ tl → DefaultClause.ofArray tl.toArray = some lratClause → l ∈ lratClause.clause
lratClause : DefaultClause n
acc✝¹ : Option (DefaultClause n)
acc✝ : DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬List.contains acc✝.clause (hd.fst, !hd.snd) = true
h✝ : ¬List.contains acc✝.clause 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

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

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

Tactic:
apply ih

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

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

Tactic:
unfold DefaultClause.ofArray

Result:
n : Nat
l hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ {lratClause : DefaultClause n}, l ∈ tl → DefaultClause.ofArray tl.toArray = some lratClause → l ∈ lratClause.clause
lratClause : DefaultClause n
acc✝¹ : Option (DefaultClause n)
acc✝ : DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some DefaultClause.empty) tl =
    some acc✝
h✝ : ¬List.contains acc✝.clause (hd.fst, !hd.snd) = true
h : List.contains acc✝.clause 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 DefaultClause.empty) tl.toArray) =
    some acc✝