harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
      (input : BinaryRefVec aig w)
      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
      ∀ (idx : Nat) (hidx : idx < w),
        ⟦(blastUdiv aig input).aig, (blastUdiv aig input).vec.get idx hidx, assign⟧
          =
        (lhs / rhs).getLsbD idx

Proof state:
case hfalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
hdiscr✝ :
  ¬⟦assign,
        {
          aig :=
            (blastUdiv.go
                (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig
                w { gate := ((blastConst aig 0#w).aig.mkConstCached false).ref.gate, hgate := ⋯ }
                { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate, hgate := ⋯ }
                ((((input.cast ⋯).cast ⋯).cast ⋯).lhs.cast ⋯) ((((input.cast ⋯).cast ⋯).cast ⋯).rhs.cast ⋯) w 0
                ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)
                ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)).aig,
          ref :=
            {
              gate :=
                (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                      { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                        rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
              hgate := ⋯ } }⟧ =
      true
hdiscr : ¬(rhs == 0#w) = true
hzero : 0#w < rhs
⊢ ((blastConst aig 0#w).aig.mkConstCached false).ref.gate <
    ((blastConst aig 0#w).aig.mkConstCached false).aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
      (input : BinaryRefVec aig w)
      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
      ∀ (idx : Nat) (hidx : idx < w),
        ⟦(blastUdiv aig input).aig, (blastUdiv aig input).vec.get idx hidx, assign⟧
          =
        (lhs / rhs).getLsbD idx

Proof state:
case hq
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx✝ : Nat
hidx✝ : idx✝ < w
hdiscr✝ :
  ¬⟦assign,
        {
          aig :=
            (blastUdiv.go
                (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig
                w { gate := ((blastConst aig 0#w).aig.mkConstCached false).ref.gate, hgate := ⋯ }
                { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate, hgate := ⋯ }
                ((((input.cast ⋯).cast ⋯).cast ⋯).lhs.cast ⋯) ((((input.cast ⋯).cast ⋯).cast ⋯).rhs.cast ⋯) w 0
                ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)
                ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)).aig,
          ref :=
            {
              gate :=
                (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                      { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                        rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
              hgate := ⋯ } }⟧ =
      true
hdiscr : ¬(rhs == 0#w) = true
hzero : 0#w < rhs
idx : Nat
hidx : idx < w
⊢ (0#w).getLsbD idx = false

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SuccPred/WithBot.lean
lemma succ_mono : Monotone (succ : WithBot α → α)
  | ⊥, _, _ => by simp
  | (a : α), ⊥, hab => by simp at hab
  | (a : α), (b : α), hab => Order.succ_le_succ (by simpa using hab)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a b : α
hab : ↑a ≤ ↑b
⊢ a ≤ b

Tactic:
simpa using hab

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : α
hab : ↑a ≤ ⊥
⊢ (↑a).succ ≤ ⊥.succ

Tactic:
simp at hab

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
x✝¹ : WithBot α
x✝ : ⊥ ≤ x✝¹
⊢ ⊥.succ ≤ x✝¹.succ

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_image_homothety (x : E) (r : ℝ) (s : Set E) :
    μ (AffineMap.homothety x r '' s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)) * μ s :=
  calc
    μ (AffineMap.homothety x r '' s) = μ ((fun y => y + x) '' (r • (fun y => y + -x) '' s))

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
s : Set E
⊢ μ ((fun y => y + x) '' (r • (fun y => y + -x) '' s)) = ENNReal.ofReal |r ^ finrank ℝ E| * μ s

Tactic:
simp only [image_add_right, measure_preimage_add_right, addHaar_smul]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
s : Set E
⊢ μ (⇑(AffineMap.homothety x r) '' s) = μ ((fun y => y + x) '' (r • (fun y => y + -x) '' s))

Tactic:
simp only [← image_smul, image_image, ← sub_eq_add_neg]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
s : Set E
⊢ μ (⇑(AffineMap.homothety x r) '' s) = μ ((fun x_1 => r • (x_1 - x) + x) '' s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
s : Set E
⊢ μ (⇑(AffineMap.homothety x r) '' s) = μ ((fun x_1 => r • (x_1 - x) + x) '' s)

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem Preconnected.boxProd (hG : G.Preconnected) (hH : H.Preconnected) :
    (G □ H).Preconnected

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
⊢ (G □ H).Preconnected

Tactic:
rintro x y

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
⊢ (G □ H).Reachable x y

Proof state:
case intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
w₁ : G.Walk x.1 y.1
⊢ (G □ H).Reachable x y

Tactic:
obtain ⟨w₂⟩ := hH x.2 y.2

Result:
case intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
w₁ : G.Walk x.1 y.1
w₂ : H.Walk x.2 y.2
⊢ (G □ H).Reachable x y

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
⊢ (G □ H).Reachable x y

Tactic:
obtain ⟨w₁⟩ := hG x.1 y.1

Result:
case intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
w₁ : G.Walk x.1 y.1
⊢ (G □ H).Reachable x y

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
w₁ : G.Walk x.1 y.1
w₂ : H.Walk x.2 y.2
⊢ (G □ H).Reachable x y

Tactic:
exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_msmooth_support_eq_eq_one_iff
    {s t : Set M} (hs : IsOpen s) (ht : IsClosed t) (h : t ⊆ s) :
    ∃ f : M → ℝ, ContMDiff I 𝓘(ℝ) ∞ f ∧ range f ⊆ Icc 0 1 ∧ support f = s
      ∧ (∀ x, x ∈ t ↔ f x = 1)

Proof state:
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ 0 < g x

Tactic:
apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)

Result:
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ g x ≠ 0
-- Mathlib/Computability/Primrec.lean
theorem of_equiv_symm {β} {e : β ≃ α} :
    haveI := Primcodable.ofEquiv α e
    Primrec e.symm :=
  letI := Primcodable.ofEquiv α e
  encode_iff.1 (show Primrec fun a => encode (e (e.symm a)) by simp [Primrec.encode])

Proof state:
α : Type u_1
inst✝ : Primcodable α
β : Type u_4
e : β ≃ α
this : Primcodable β := Primcodable.ofEquiv α e
⊢ Primrec fun a => encode (e (e.symm a))

Tactic:
simp [Primrec.encode]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem modEq_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) : n ≡ (digits b' n).sum [MOD b]

Proof state:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ (b'.digits n).sum [MOD b]

Tactic:
rw [← ofDigits_one]

Result:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ ofDigits 1 (b'.digits n) [MOD b]

Proof state:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits b' (b'.digits n) ≡ ofDigits 1 (b'.digits n) [MOD b]

Tactic:
convert ofDigits_modEq b' b (digits b' n)

Result:
case h.e'_3.h.e'_3
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ 1 = b' % b

Proof state:
case h.e'_3.h.e'_3
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ 1 = b' % b

Tactic:
exact h.symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1 ≤ w)
    (acc : AIG.RefVec aig w) (lhs rhs : AIG.RefVec aig w) (lexpr rexpr : BitVec w) (assign : Assignment)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsbD idx)
    (hacc : ∀ (idx : Nat) (hidx : idx < w),
                ⟦aig, acc.get idx hidx, assign.toAIGAssignment⟧
                  =
                (BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦
          (go aig lhs rhs (curr + 1) acc).aig,
          (go aig lhs rhs (curr + 1) acc).vec.get idx hidx,
          assign.toAIGAssignment
        ⟧
          =
        (BitVec.mulRec lexpr rexpr w).getLsbD idx

Proof state:
case isFalse
aig : AIG BVBit
curr : Nat
assign : Assignment
idx : Nat
hcurr : curr + 1 ≤ curr + 1
acc lhs rhs : aig.RefVec (curr + 1)
lexpr rexpr : BitVec (curr + 1)
hleft :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
hidx : idx < curr + 1
res : RefVecEntry BVBit (curr + 1)
h✝ : ¬curr + 1 < curr + 1
hgo : { aig := aig, vec := acc } = res
⊢ ⟦assign.toAIGAssignment,
      { aig := { aig := aig, vec := acc }.aig, ref := { aig := aig, vec := acc }.vec.get idx hidx }⟧ =
    (lexpr.mulRec rexpr (curr + 1)).getLsbD idx

Tactic:
rw [hacc]

Result:
case isFalse
aig : AIG BVBit
curr : Nat
assign : Assignment
idx : Nat
hcurr : curr + 1 ≤ curr + 1
acc lhs rhs : aig.RefVec (curr + 1)
lexpr rexpr : BitVec (curr + 1)
hleft :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
hidx : idx < curr + 1
res : RefVecEntry BVBit (curr + 1)
h✝ : ¬curr + 1 < curr + 1
hgo : { aig := aig, vec := acc } = res
⊢ (lexpr.mulRec rexpr curr).getLsbD idx = (lexpr.mulRec rexpr (curr + 1)).getLsbD idx
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1 ≤ w)
    (acc : AIG.RefVec aig w) (lhs rhs : AIG.RefVec aig w) (lexpr rexpr : BitVec w) (assign : Assignment)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsbD idx)
    (hacc : ∀ (idx : Nat) (hidx : idx < w),
                ⟦aig, acc.get idx hidx, assign.toAIGAssignment⟧
                  =
                (BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦
          (go aig lhs rhs (curr + 1) acc).aig,
          (go aig lhs rhs (curr + 1) acc).vec.get idx hidx,
          assign.toAIGAssignment
        ⟧
          =
        (BitVec.mulRec lexpr rexpr w).getLsbD idx

Proof state:
case hacc
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx✝ : Nat
hidx✝ : idx✝ < w
res : RefVecEntry BVBit w
h✝ : curr + 1 < w
hconstant : aig.isConstant (rhs.get (curr + 1) h✝) false = true
hgo : go aig lhs rhs (curr + 1 + 1) acc = res
idx : Nat
hidx : idx < w
⊢ ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ =
    (lexpr.mulRec rexpr curr + if rexpr.getLsbD (curr + 1) = true then lexpr <<< (curr + 1) else 0).getLsbD idx

Tactic:
have : rexpr.getLsbD (curr + 1) = false := by
  rw [← hright]
  exact of_isConstant hconstant

Result:
case hacc
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx✝ : Nat
hidx✝ : idx✝ < w
res : RefVecEntry BVBit w
h✝ : curr + 1 < w
hconstant : aig.isConstant (rhs.get (curr + 1) h✝) false = true
hgo : go aig lhs rhs (curr + 1 + 1) acc = res
idx : Nat
hidx : idx < w
this : rexpr.getLsbD (curr + 1) = false
⊢ ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ =
    (lexpr.mulRec rexpr curr + if rexpr.getLsbD (curr + 1) = true then lexpr <<< (curr + 1) else 0).getLsbD idx
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1 ≤ w)
    (acc : AIG.RefVec aig w) (lhs rhs : AIG.RefVec aig w) (lexpr rexpr : BitVec w) (assign : Assignment)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsbD idx)
    (hacc : ∀ (idx : Nat) (hidx : idx < w),
                ⟦aig, acc.get idx hidx, assign.toAIGAssignment⟧
                  =
                (BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦
          (go aig lhs rhs (curr + 1) acc).aig,
          (go aig lhs rhs (curr + 1) acc).vec.get idx hidx,
          assign.toAIGAssignment
        ⟧
          =
        (BitVec.mulRec lexpr rexpr w).getLsbD idx

Proof state:
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig lhs rhs (curr + 1) acc).aig, ref := (go aig lhs rhs (curr + 1) acc).vec.get idx hidx }⟧ =
    (lexpr.mulRec rexpr w).getLsbD idx

Tactic:
generalize hgo: go aig lhs rhs (curr + 1) acc = res

Result:
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
hgo : go aig lhs rhs (curr + 1) acc = res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lexpr.mulRec rexpr w).getLsbD idx
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1 ≤ w)
    (acc : AIG.RefVec aig w) (lhs rhs : AIG.RefVec aig w) (lexpr rexpr : BitVec w) (assign : Assignment)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsbD idx)
    (hacc : ∀ (idx : Nat) (hidx : idx < w),
                ⟦aig, acc.get idx hidx, assign.toAIGAssignment⟧
                  =
                (BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦
          (go aig lhs rhs (curr + 1) acc).aig,
          (go aig lhs rhs (curr + 1) acc).vec.get idx hidx,
          assign.toAIGAssignment
        ⟧
          =
        (BitVec.mulRec lexpr rexpr w).getLsbD idx

Proof state:
case isFalse
aig : AIG BVBit
curr : Nat
assign : Assignment
idx : Nat
hcurr : curr + 1 ≤ curr + 1
acc lhs rhs : aig.RefVec (curr + 1)
lexpr rexpr : BitVec (curr + 1)
hleft :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
hidx : idx < curr + 1
res : RefVecEntry BVBit (curr + 1)
h✝ : ¬curr + 1 < curr + 1
hgo : { aig := aig, vec := acc } = res
⊢ (lexpr.mulRec rexpr curr).getLsbD idx = (lexpr.mulRec rexpr (curr + 1)).getLsbD idx

Tactic:
rw [BitVec.mulRec_succ_eq]

Result:
case isFalse
aig : AIG BVBit
curr : Nat
assign : Assignment
idx : Nat
hcurr : curr + 1 ≤ curr + 1
acc lhs rhs : aig.RefVec (curr + 1)
lexpr rexpr : BitVec (curr + 1)
hleft :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
hidx : idx < curr + 1
res : RefVecEntry BVBit (curr + 1)
h✝ : ¬curr + 1 < curr + 1
hgo : { aig := aig, vec := acc } = res
⊢ (lexpr.mulRec rexpr curr).getLsbD idx =
    (lexpr.mulRec rexpr curr + if rexpr.getLsbD (curr + 1) = true then lexpr <<< (curr + 1) else 0).getLsbD idx
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1 ≤ w)
    (acc : AIG.RefVec aig w) (lhs rhs : AIG.RefVec aig w) (lexpr rexpr : BitVec w) (assign : Assignment)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsbD idx)
    (hacc : ∀ (idx : Nat) (hidx : idx < w),
                ⟦aig, acc.get idx hidx, assign.toAIGAssignment⟧
                  =
                (BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦
          (go aig lhs rhs (curr + 1) acc).aig,
          (go aig lhs rhs (curr + 1) acc).vec.get idx hidx,
          assign.toAIGAssignment
        ⟧
          =
        (BitVec.mulRec lexpr rexpr w).getLsbD idx

Proof state:
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝ : ¬curr + 1 < w
hgo : { aig := aig, vec := acc } = res
⊢ curr + 1 = w

Tactic:
omega

Result:
no goals