-- Mathlib/Tactic/Sat/FromLRAT.lean
theorem Valuation.mk_implies {p} {as ps} (as₁) : as = List.reverseAux as₁ ps →
    (Valuation.mk as).implies p ps as₁.length → p

Proof state:
case cons
p a : Prop
as as₁ : List Prop
⊢ ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n

Tactic:
induction as₁ with
| nil => simp
| cons b as₁ ih => simpa using fun n bs ↦ ih (n+1) _ (Nat.succ_add ..) _

Result:
no goals

Proof state:
case nil
p : Prop
as as₁ : List Prop
⊢ as = as₁.reverseAux [] → (mk as).implies p [] as₁.length → p

Tactic:
exact fun _ ↦ id

Result:
no goals

Proof state:
case cons.cons
p a : Prop
as : List Prop
b : Prop
as₁ : List Prop
ih : ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n
⊢ ∀ (n n' : ℕ), n' = (b :: as₁).length + n → ∀ (bs : List Prop), mk ((b :: as₁).reverseAux bs) n' ↔ mk bs n

Tactic:
simpa using fun n bs ↦ ih (n+1) _ (Nat.succ_add ..) _

Result:
no goals

Proof state:
case cons.nil
p a : Prop
as : List Prop
⊢ ∀ (n n' : ℕ), n' = [].length + n → ∀ (bs : List Prop), mk ([].reverseAux bs) n' ↔ mk bs n

Tactic:
simp

Result:
no goals

Proof state:
case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = as₁.reverseAux as → (mk as✝).implies p as as₁.length → p
as₁ : List Prop
⊢ as✝ = as₁.reverseAux (a :: as) → (mk as✝).implies p (a :: as) as₁.length → p

Tactic:
refine fun e H ↦ @ih (a::as₁) e (H ?_)

Result:
case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = as₁.reverseAux as → (mk as✝).implies p as as₁.length → p
as₁ : List Prop
e : as✝ = as₁.reverseAux (a :: as)
H : (mk as✝).implies p (a :: as) as₁.length
⊢ mk as✝ as₁.length ↔ a

Proof state:
case cons
p a : Prop
as as₁ : List Prop
⊢ mk (as₁.reverseAux (a :: as)) as₁.length ↔ a

Tactic:
suffices ∀ n n', n' = List.length as₁ + n →
  ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a::as)

Result:
case cons
p a : Prop
as as₁ : List Prop
⊢ ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n

Proof state:
p : Prop
as ps as₁ : List Prop
⊢ as = as₁.reverseAux ps → (mk as).implies p ps as₁.length → p

Tactic:
induction ps generalizing as₁ with
| nil => exact fun _ ↦ id
| cons a as ih =>
  refine fun e H ↦ @ih (a::as₁) e (H ?_)
  subst e; clear ih H
  suffices ∀ n n', n' = List.length as₁ + n →
    ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a::as)
  induction as₁ with
  | nil => simp
  | cons b as₁ ih => simpa using fun n bs ↦ ih (n+1) _ (Nat.succ_add ..) _

Result:
no goals

Proof state:
case cons
p a : Prop
as as₁ : List Prop
ih :
  ∀ (as₁_1 : List Prop),
    as₁.reverseAux (a :: as) = as₁_1.reverseAux as → (mk (as₁.reverseAux (a :: as))).implies p as as₁_1.length → p
H : (mk (as₁.reverseAux (a :: as))).implies p (a :: as) as₁.length
⊢ mk (as₁.reverseAux (a :: as)) as₁.length ↔ a

Tactic:
clear ih H

Result:
case cons
p a : Prop
as as₁ : List Prop
⊢ mk (as₁.reverseAux (a :: as)) as₁.length ↔ a

Proof state:
case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = as₁.reverseAux as → (mk as✝).implies p as as₁.length → p
as₁ : List Prop
e : as✝ = as₁.reverseAux (a :: as)
H : (mk as✝).implies p (a :: as) as₁.length
⊢ mk as✝ as₁.length ↔ a

Tactic:
subst e

Result:
case cons
p a : Prop
as as₁ : List Prop
ih :
  ∀ (as₁_1 : List Prop),
    as₁.reverseAux (a :: as) = as₁_1.reverseAux as → (mk (as₁.reverseAux (a :: as))).implies p as as₁_1.length → p
H : (mk (as₁.reverseAux (a :: as))).implies p (a :: as) as₁.length
⊢ mk (as₁.reverseAux (a :: as)) as₁.length ↔ a