harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_trans {x y z : BitVec n} : x < y → y < z → x < z

Proof state:
n : Nat
x y z : BitVec n
⊢ x < y → y < z → x < z

Tactic:
simp only [lt_def]

Result:
n : Nat
x y z : BitVec n
⊢ x.toNat < y.toNat → y.toNat < z.toNat → x.toNat < z.toNat

Proof state:
n : Nat
x y z : BitVec n
⊢ x.toNat < y.toNat → y.toNat < z.toNat → x.toNat < z.toNat

Tactic:
apply Nat.lt_trans

Result:
no goals
-- Mathlib/Analysis/Normed/Field/InfiniteSum.lean
theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ k ∈ range (n + 1), f k * g (n - k)

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
h'f : Summable f
hg : Summable fun x => ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]

Result:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
h'f : Summable f
hg : Summable fun x => ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
h'f : Summable f
hg : Summable fun x => ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2

Tactic:
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' hf h'f hg h'g

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_id' (s : Set α) : (fun x => x) '' s = s

Proof state:
case h
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ (fun x => x) '' s ↔ x✝ ∈ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ (fun x => x) '' s = s

Tactic:
ext

Result:
case h
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ (fun x => x) '' s ↔ x✝ ∈ s
-- Mathlib/RepresentationTheory/Basic.lean
theorem asModuleEquiv_symm_map_rho (g : G) (x : V) :
    ρ.asModuleEquiv.symm (ρ g x) = MonoidAlgebra.of k G g • ρ.asModuleEquiv.symm x

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ ρ.asModuleEquiv (ρ.asModuleEquiv.symm ((ρ g) x)) = ρ.asModuleEquiv ((of k G) g • ρ.asModuleEquiv.symm x)

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ ρ.asModuleEquiv.symm ((ρ g) x) = (of k G) g • ρ.asModuleEquiv.symm x

Tactic:
apply_fun ρ.asModuleEquiv

Result:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ ρ.asModuleEquiv (ρ.asModuleEquiv.symm ((ρ g) x)) = ρ.asModuleEquiv ((of k G) g • ρ.asModuleEquiv.symm x)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
    {l toInsert : List ((a : α) × β a)} {k : α}
    (not_contains : (toInsert.map Sigma.fst).contains k = false)
    {h} :
    getValueCast k (insertList l toInsert) h =
    getValueCast k l (containsKey_of_containsKey_insertList h not_contains)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : (List.map Sigma.fst toInsert).contains k = false
h : containsKey k (insertList l toInsert) = true
⊢ getValueCast k (insertList l toInsert) h = getValueCast k l ⋯

Tactic:
rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, ← getValueCast?_eq_some_getValueCast,
  getValueCast?_insertList_of_contains_eq_false]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : (List.map Sigma.fst toInsert).contains k = false
h : containsKey k (insertList l toInsert) = true
⊢ (List.map Sigma.fst toInsert).contains k = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : (List.map Sigma.fst toInsert).contains k = false
h : containsKey k (insertList l toInsert) = true
⊢ (List.map Sigma.fst toInsert).contains k = false

Tactic:
exact not_contains

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem mem_idealOfSet_compl_singleton (x : X) (f : C(X, R)) :
    f ∈ idealOfSet R ({x}ᶜ : Set X) ↔ f x = 0

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
x : X
f : C(X, R)
⊢ f ∈ idealOfSet R {x}ᶜ ↔ f x = 0

Tactic:
simp only [mem_idealOfSet, compl_compl, Set.mem_singleton_iff, forall_eq]

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem smul {c : K} (hc : c ≠ 0) :
    c • span ℤ (Set.range b) = span ℤ (Set.range (b.isUnitSMul (fun _ ↦ hc.isUnit)))

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
⊢ span ℤ (Set.range fun i => c • b i) = span ℤ (Set.range ⇑(b.isUnitSMul ⋯))

Tactic:
congr!

Result:
case h.e'_6.h.e'_3.h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
x✝ : ι
⊢ c • b x✝ = (b.isUnitSMul ⋯) x✝

Proof state:
case h.e'_6.h.e'_3.h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
x✝ : ι
⊢ c • b x✝ = (b.isUnitSMul ⋯) x✝

Tactic:
rw [Basis.isUnitSMul_apply]

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
⊢ c • span ℤ (Set.range ⇑b) = span ℤ (Set.range ⇑(b.isUnitSMul ⋯))

Tactic:
rw [smul_span, Set.smul_set_range]

Result:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
⊢ span ℤ (Set.range fun i => c • b i) = span ℤ (Set.range ⇑(b.isUnitSMul ⋯))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zip_map_left (f : α → γ) (l₁ : Vector α n) (l₂ : Vector β n) :
    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id)

Proof state:
α : Type u_1
γ : Type u_2
n : Nat
β : Type u_3
f : α → γ
l₁ : Vector α n
l₂ : Vector β n
⊢ (map f l₁).zip l₂ = map (Prod.map f id) (l₁.zip l₂)

Tactic:
rw [← zip_map, map_id]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem sInf_toSubsemiring (S : Set (Subalgebra R A)) :
    (sInf S).toSubsemiring = sInf (Subalgebra.toSubsemiring '' S) :=
  SetLike.coe_injective <| by simp

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
⊢ ↑(sInf S).toSubsemiring = ↑(sInf (Subalgebra.toSubsemiring '' S))

Tactic:
simp

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_iSup_eq_left {b : β} {f : ∀ x : β, x = b → α} : ⨆ x, ⨆ h : x = b, f x h = f b rfl :=
  (@le_iSup₂ _ _ _ _ f b rfl).antisymm'
    (iSup_le fun c =>
      iSup_le <| by
        rintro rfl
        rfl)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
c : β
f : (x : β) → x = c → α
⊢ f c ⋯ ≤ f c ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
b : β
f : (x : β) → x = b → α
c : β
⊢ ∀ (i : c = b), f c i ≤ f b ⋯

Tactic:
rintro rfl

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
c : β
f : (x : β) → x = c → α
⊢ f c ⋯ ≤ f c ⋯
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma supIrred_iff_of_finite : SupIrred s ↔ ∃ a, Iic a = s

Proof state:
case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
hs : SupIrred s
⊢ ∃ a, Iic a = s

Tactic:
obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_maximal_wrt id _ (coe_nonempty.2 hs.ne_bot)

Result:
case refine_1.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
hs : SupIrred s
a : α
ha : a ∈ ↑s
has : ∀ a' ∈ ↑s, id a ≤ id a' → id a = id a'
⊢ ∃ a, Iic a = s

Proof state:
case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
⊢ (∃ a, Iic a = s) → SupIrred s

Tactic:
rintro ⟨a, rfl⟩

Result:
case refine_2.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
a : α
⊢ SupIrred (Iic a)

Proof state:
case refine_2.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
a : α
⊢ SupIrred (Iic a)

Tactic:
exact supIrred_Iic _

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
hs : SupIrred s
a : α
ha : a ∈ ↑s
has : ∀ a' ∈ ↑s, id a ≤ id a' → id a = id a'
⊢ ∃ a, Iic a = s

Tactic:
exact ⟨a, (hs.2 <| erase_sup_Iic ha <| by simpa [eq_comm] using has).resolve_left
  (erase_lt.2 ha).ne⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
hs : SupIrred s
a : α
ha : a ∈ ↑s
has : ∀ a' ∈ ↑s, id a ≤ id a' → id a = id a'
⊢ ∀ b ∈ s, a ≤ b → b = a

Tactic:
simpa [eq_comm] using has

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
⊢ SupIrred s ↔ ∃ a, Iic a = s

Tactic:
refine ⟨fun hs ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
hs : SupIrred s
⊢ ∃ a, Iic a = s

case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
⊢ (∃ a, Iic a = s) → SupIrred s
-- Mathlib/RingTheory/Derivation/Basic.lean
theorem leibniz_div_const (a b : K) (h : D b = 0) : D (a / b) = b⁻¹ • D a

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
h : D b = 0
⊢ D (a / b) = b⁻¹ • D a

Tactic:
simp only [leibniz_div, inv_pow, h, smul_zero, sub_zero, smul_smul]

Result:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
h : D b = 0
⊢ ((b ^ 2)⁻¹ * b) • D a = b⁻¹ • D a

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
h : D b = 0
⊢ ((b ^ 2)⁻¹ * b) • D a = b⁻¹ • D a

Tactic:
rw [← mul_self_mul_inv b⁻¹, inv_inv]

Result:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
h : D b = 0
⊢ ((b ^ 2)⁻¹ * b) • D a = (b⁻¹ * b⁻¹ * b) • D a

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
h : D b = 0
⊢ ((b ^ 2)⁻¹ * b) • D a = (b⁻¹ * b⁻¹ * b) • D a

Tactic:
ring_nf

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem is_left_invariant_index {K : Set G} (hK : IsCompact K) (g : G) {V : Set G}
    (hV : (interior V).Nonempty) : index ((fun h => g * h) '' K) V = index K V

Proof state:
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ (fun x => g⁻¹ * (g * x)) '' K = K

Tactic:
convert image_id' _ with h

Result:
case h.e'_2.h.e'_3.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
h : G
⊢ g⁻¹ * (g * h) = h

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ index ((fun h => g * h) '' K) V = index K V

Tactic:
refine le_antisymm (mul_left_index_le hK hV g) ?_

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ index K V ≤ index ((fun h => g * h) '' K) V

Proof state:
case h.e'_2.h.e'_3.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
h : G
⊢ g⁻¹ * (g * h) = h

Tactic:
apply inv_mul_cancel_left

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ index K V ≤ index ((fun h => g * h) '' K) V

Tactic:
convert mul_left_index_le (hK.image <| continuous_mul_left g) hV g⁻¹

Result:
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ K = (fun h => g⁻¹ * h) '' ((fun b => g * b) '' K)

Proof state:
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ K = (fun h => g⁻¹ * h) '' ((fun b => g * b) '' K)

Tactic:
rw [image_image]

Result:
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ K = (fun x => g⁻¹ * (g * x)) '' K

Proof state:
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ K = (fun x => g⁻¹ * (g * x)) '' K

Tactic:
symm

Result:
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ (fun x => g⁻¹ * (g * x)) '' K = K
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
theorem blastShiftLeft.go_decl_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
    (acc : AIG.RefVec aig w) :
    ∀ (idx : Nat) (h1) (h2),
        (go aig distance curr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
res : AIG.RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
            (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls.size
⊢ (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig.decls[idx✝] = aig.decls[idx✝]

case isTrue.h1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
res : AIG.RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
            (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls.size
⊢ idx✝ < (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig.decls.size

Tactic:
rw [AIG.LawfulVecOperator.decl_eq (f := blastShiftLeft.twoPowShift)]

Result:
case isTrue.h2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
res : AIG.RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
            (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls.size
⊢ idx✝ < (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig.decls.size
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_modifyKey_self [BEq α] [LawfulBEq α] {k : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) {h : containsKey k (modifyKey k f l)} :
    haveI h' : containsKey k l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
h : containsKey k (modifyKey k f l) = true
⊢ getValueCast k (modifyKey k f l) h = f (getValueCast k l ⋯)

Tactic:
simp [getValueCast_modifyKey, hl]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
h : containsKey k (modifyKey k f l) = true
⊢ containsKey k l = true

Tactic:
rwa [containsKey_modifyKey] at h

Result:
no goals
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem map' (H : A.LinearDisjoint L) (K : Type*) [Field K] [Algebra F K] [Algebra L K]
    [IsScalarTower F L K] [Algebra E K] [IsScalarTower F E K] [IsScalarTower L E K] :
    (A.map (IsScalarTower.toAlgHom F E K)).LinearDisjoint L

Proof state:
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint (IsScalarTower.toAlgHom F L E).range
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra L K
inst✝³ : IsScalarTower F L K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsScalarTower L E K
⊢ (IntermediateField.map (IsScalarTower.toAlgHom F E K) A).LinearDisjoint (IsScalarTower.toAlgHom F L K).range

Tactic:
have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)

Result:
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint (IsScalarTower.toAlgHom F L E).range
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra L K
inst✝³ : IsScalarTower F L K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsScalarTower L E K
this :
  (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra).LinearDisjoint
    (Subalgebra.map (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E).range)
⊢ (IntermediateField.map (IsScalarTower.toAlgHom F E K) A).LinearDisjoint (IsScalarTower.toAlgHom F L K).range
-- Mathlib/Data/Multiset/Bind.lean
theorem bind_congr {f g : α → Multiset β} {m : Multiset α} :
    (∀ a ∈ m, f a = g a) → bind m f = bind m g

Proof state:
α : Type u_1
β : Type v
f g : α → Multiset β
m : Multiset α
⊢ (∀ a ∈ m, f a = g a) → m.bind f = m.bind g

Tactic:
simp +contextual [bind]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem Image.lift_fac (F' : MonoFactorisation f) : Image.lift F' ≫ F'.m = Image.ι f

Proof state:
case h
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => f x_1 = ↑x) ⋯) = ι f x

Tactic:
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]

Result:
case h
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ ↑x = ι f x

Proof state:
case h
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (lift F' ≫ F'.m) x = ι f x

Tactic:
change (F'.e ≫ F'.m) _ = _

Result:
case h
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => f x_1 = ↑x) ⋯) = ι f x

Proof state:
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f

Tactic:
funext x

Result:
case h
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (lift F' ≫ F'.m) x = ι f x

Proof state:
case h
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ ↑x = ι f x

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Deriv.lean
/-- The abscissa of absolute convergence of the point-wise product of a power of `log` and `f`
is the same as that of `f`. -/
@[simp]
lemma LSeries.absicssaOfAbsConv_logPowMul {f : ℕ → ℂ} {m : ℕ} :
    abscissaOfAbsConv (logMul^[m] f) = abscissaOfAbsConv f

Proof state:
case succ
f : ℕ → ℂ
n : ℕ
ih : abscissaOfAbsConv (logMul^[n] f) = abscissaOfAbsConv f
⊢ abscissaOfAbsConv (logMul^[n + 1] f) = abscissaOfAbsConv f

Tactic:
simp [ih, Function.iterate_succ', Function.comp_def,
-Function.comp_apply, -Function.iterate_succ]

Result:
no goals

Proof state:
case zero
f : ℕ → ℂ
⊢ abscissaOfAbsConv (logMul^[0] f) = abscissaOfAbsConv f

Tactic:
simp

Result:
no goals

Proof state:
f : ℕ → ℂ
m : ℕ
⊢ abscissaOfAbsConv (logMul^[m] f) = abscissaOfAbsConv f

Tactic:
induction m with
| zero => simp
| succ n ih => simp [ih, Function.iterate_succ', Function.comp_def,
    -Function.comp_apply, -Function.iterate_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem map_lt [LT α] [LT β]
    {l₁ l₂ : List α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) :
    map f l₁ < map f l₂

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h✝ : l₁ < l₂
h : [] < []
⊢ map f [] < map f []

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
l₁✝ l₂✝ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h✝ : l₁✝ < l₂✝
a : α
l₁ l₂ : List α
h : Lex (fun x1 x2 => x1 < x2) l₁ l₂
⊢ ?m.119928 < ?m.119929

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
l₁✝ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h✝ : l₁✝ < l₂
a : α
l₁ : List α
h : a :: l₁ < []
⊢ map f (a :: l₁) < map f []

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
l₁✝ l₂✝ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h✝ : l₁✝ < l₂✝
a : α
l₁ : List α
b : α
l₂ : List α
h : a < b
⊢ map f (a :: l₁) < map f (b :: l₂)

Tactic:
simp [cons_lt_cons_iff, w, h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
l₁✝ l₂✝ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h✝ : l₁✝ < l₂✝
a : α
l₁ l₂ : List α
h : Lex (fun x1 x2 => x1 < x2) l₁ l₂
⊢ map f (a :: l₁) < map f (a :: l₂)

Tactic:
simp [cons_lt_cons_iff, List.map_lt w (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
l₁ l₂✝ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h✝ : l₁ < l₂✝
b : α
l₂ : List α
h : [] < b :: l₂
⊢ map f [] < map f (b :: l₂)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ < l₂
⊢ map f l₁ < map f l₂

Tactic:
match l₁, l₂, h with
| nil, nil, h => simp at h
| nil, cons b l₂, h => simp
| cons a l₁, nil, h => simp at h
| cons a l₁, cons _ l₂, .cons h =>
  simp [cons_lt_cons_iff, List.map_lt w (by simpa using h)]
| cons a l₁, cons b l₂, .rel h =>
  simp [cons_lt_cons_iff, w, h]

Result:
no goals