mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Jensen
/-- A form of the **equality case of Jensen's equality** for the case of strict convex and positive
weights.  -/
StrictConvexOn.map_sum_eq_iff_of_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          (f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k)
-- Lean.Elab.SyntheticMVars
/-- Try to synthesize the given pending synthetic metavariable.  -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeSyntheticMVar : Lean.MVarId → Bool → Bool → Lean.Elab.TermElabM Bool
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The identity morphism of an object in `P.Comma L R Q W`.  -/
CategoryTheory.MorphismProperty.Comma.id : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      [Q.ContainsIdentities] →
                        [W.ContainsIdentities] → (X : CategoryTheory.MorphismProperty.Comma L R P Q W) → X.Hom X
-- Mathlib.LinearAlgebra.Finsupp.Defs
Module.End.ringEquivEndFinsupp_apply_apply_support : ∀ {ι : Type u_4} {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (i : ι) (a : Module.End (Module.End R M) M) (a_1 : ι →₀ M),
  (((Module.End.ringEquivEndFinsupp i) a) a_1).support = Finsupp.onFinsetSupport a_1.support (⇑a ∘ ⇑a_1)
-- Mathlib.Order.Ideal
Order.Ideal.isIdeal : ∀ {P : Type u_1} [inst : LE P] (s : Order.Ideal P), Order.IsIdeal ↑s
-- Lean.CoreM
Lean.Core.instMonadDeclNameGeneratorCoreM : Lean.MonadDeclNameGenerator Lean.CoreM
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.nndist_toLp_snd : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (y₁ y₂ : β), nndist (WithLp.toLp p (0, y₁)) (WithLp.toLp p (0, y₂)) = nndist y₁ y₂
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.restrict_split : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι},
  I ≤ J → ∀ (i : ι) (x : ℝ), (BoxIntegral.Prepartition.split J i x).restrict I = BoxIntegral.Prepartition.split I i x
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_add_cbm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B C : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f → ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]
-- Mathlib.Tactic.TermCongr
/-- Make sure that the expected type of `pf` is an iff by unification.  -/
Mathlib.Tactic.TermCongr.ensureIff : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.List.Lemmas
List.head_tail : ∀ {α : Type u_1} {l : List α} (h : l.tail ≠ []), l.tail.head h = l[1]
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
CuspForm.divDiscriminant_apply : ∀ {k : ℤ} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (z : UpperHalfPlane),
  f.divDiscriminant z = f z / ModularForm.discriminant z
-- Mathlib.Analysis.InnerProductSpace.LinearMap
ContinuousLinearMap.reApplyInnerSelf_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) (x : E) {c : 𝕜}, T.reApplyInnerSelf (c • x) = ‖c‖ ^ 2 * T.reApplyInnerSelf x
-- Init.Data.UInt.Lemmas
UInt32.toUInt32_toUInt16 : ∀ (n : UInt32), n.toUInt16.toUInt32 = n % 65536
-- Init.Data.UInt.Lemmas
USize.toBitVec_toUInt64 : ∀ (n : USize), n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.neutralInst? : Lean.Meta.Grind.AC.Struct → Option Lean.Expr
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.core.inj : ∀ {a b : Lean.Expr} {lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr} {a_1 b_1 : Lean.Expr}
  {lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.EqCnstrProof.core a b lhs rhs =
      Lean.Meta.Grind.Arith.Linear.EqCnstrProof.core a_1 b_1 lhs_1 rhs_1 →
    a = a_1 ∧ b = b_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries_two : Real.sqrtTwoAddSeries 0 2 = √(2 + √2)
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.mk : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          (F : CategoryTheory.Functor A C) →
            (π : F.comp ι ⟶ CategoryTheory.Functor.id A) →
              autoParam (∀ (X : A), CategoryTheory.Epi (π.app X))
                  CategoryTheory.Abelian.LeftResolution.epi_π_app._autoParam →
                CategoryTheory.Abelian.LeftResolution ι
-- Mathlib.Data.Finset.Image
Finset.map_nonempty : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α}, (Finset.map f s).Nonempty ↔ s.Nonempty
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sub_iUnion₂ : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Sub α] (s : Set α) (t : (i : ι) → κ i → Set α),
  s - ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s - t i j
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minEntry?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  (Std.Internal.List.minEntry? l).isSome = !l.isEmpty
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
/-- Hölder's inequality, as an inequality on the `ℒp` seminorm of an elementwise operation
`fun x => b (f x) (g x)`.  -/
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.Measure α} {f : α → E} {g : α → F}
  {p q r : ENNReal},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      ∀ (b : E → F → G) (c : NNReal),
        (∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ↑c * ‖f x‖ * ‖g x‖) →
          ∀ [hpqr : p.HolderTriple q r],
            MeasureTheory.eLpNorm (fun x => b (f x) (g x)) r μ ≤
              ↑c * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g q μ
-- Mathlib.CategoryTheory.Products.Basic
/-- The equivalence between the opposite of a product and the product of the opposites.  -/
CategoryTheory.prodOpEquiv : (C : Type u₃) →
  [inst : CategoryTheory.Category.{v₃, u₃} C] →
    {D : Type u₄} → [inst_1 : CategoryTheory.Category.{v₄, u₄} D] → (C × D)ᵒᵖ ≌ Cᵒᵖ × Dᵒᵖ
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eq_of_eqOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f f' : α → E} {s : Set α},
  Set.EqOn f f' s → eVariationOn f s = eVariationOn f' s
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
/-- If `A` is a finite free `R`-algebra, then `f : A` is nilpotent on `κ(𝔭) ⊗ A` for some
prime `𝔭 ◃ R` if and only if every non-leading coefficient of `charpoly(f)` is in `𝔭`.  -/
isNilpotent_tensor_residueField_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : Module.Free R A] [inst_4 : Module.Finite R A] (f : A) (I : Ideal R) [inst_5 : I.IsPrime],
  IsNilpotent ((algebraMap A (TensorProduct R A I.ResidueField)) f) ↔
    ∀ i < Module.finrank R A, (LinearMap.charpoly ((Algebra.lmul R A) f)).coeff i ∈ I
-- Mathlib.Algebra.Lie.UniversalEnveloping
/-- `Rel` as a ring congruence, used to build the quotient.  -/
UniversalEnvelopingAlgebra.ringCon : (R : Type u₁) →
  (L : Type u₂) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → RingCon (TensorAlgebra R L)
-- Init.Data.Nat.Compare
Nat.compare_eq_lt : ∀ {a b : ℕ}, compare a b = Ordering.lt ↔ a < b
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.canUseLinear : Lean.Name → Lean.MetaM Bool
-- Mathlib.Algebra.Lie.SkewAdjoint
skewAdjointMatricesLieSubalgebraEquivTranspose_apply : ∀ {R : Type u} {n : Type w} [inst : CommRing R] [inst_1 : Fintype n] (J : Matrix n n R) [inst_2 : DecidableEq n]
  {m : Type w} [inst_3 : DecidableEq m] [inst_4 : Fintype m] (e : Matrix n n R ≃ₐ[R] Matrix m m R)
  (h : ∀ (A : Matrix n n R), (e A).transpose = e A.transpose) (A : ↥(skewAdjointMatricesLieSubalgebra J)),
  ↑((skewAdjointMatricesLieSubalgebraEquivTranspose J e h) A) = e ↑A
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.hom_inv_h₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  {i j : E.I₀} (k : E.I₁ i j) {Z : C} (h : E.Y (e.inv.s₁ (e.hom.s₁ k)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.hom.h₁ k) (CategoryTheory.CategoryStruct.comp (e.inv.h₁ (e.hom.s₁ k)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ k).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
-- Lean.Server.References
Lean.Server.instInhabitedModuleImport.default : Lean.Server.ModuleImport
-- Mathlib.Algebra.Group.Hom.Defs
/-- Additive group homomorphisms preserve subtraction.  -/
map_sub : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
  [inst_2 : SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (a b : G), f (a - b) = f a - f b
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ_zero : ∀ {α : Type u} [inst : Lean.Grind.Semiring α], ↑0 = 0
-- Lean.Meta.Tactic.Induction
_private.Lean.Meta.Tactic.Induction.0.Lean.Meta.addRecParams : Lean.MVarId → Array Lean.Expr → List (Option ℕ) → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.Derangements.Basic
Equiv.Perm.subtypeEquivSubtypePerm.eq_1 : ∀ {α : Type u_4} (p : α → Prop) [inst : DecidablePred p],
  Equiv.Perm.subtypeEquivSubtypePerm p =
    { toFun := fun f => ⟨Equiv.Perm.ofSubtype f, ⋯⟩, invFun := fun f => (↑f).subtypePerm ⋯, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.Functor.mapConnectedComponents_mk : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J K) (j : J), F.mapConnectedComponents ⟦j⟧ = ⟦F.obj j⟧
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getDoReassignVars : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
MonoidWithZero.inverse_apply : ∀ {M : Type u_8} [inst : CommMonoidWithZero M] (a : M), MonoidWithZero.inverse a = Ring.inverse a
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- The image under `Circle.exp` of the interval of angles `(-r, r)`.  -/
Circle.centeredArc : ℝ → Set Circle
-- Mathlib.Algebra.Group.Defs
pow_mul' : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ n) ^ m
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_Ico_addNat : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) ⁻¹' Set.Ico (i.addNat m) (j.addNat m) = Set.Ico i j
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso_inv_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).counitIso.inv.app X_1).fst.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.fst.obj X_2)
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.compProd_id_eq_copy_comp : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ],
  μ.compProd ProbabilityTheory.Kernel.id = μ.bind ⇑(ProbabilityTheory.Kernel.copy α)
-- Mathlib.Order.Interval.Set.Infinite
Set.Ioc_infinite : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] {a b : α}, a < b → (Set.Ioc a b).Infinite
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_zero_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {h : (i : ι) → β i → γ},
  DFinsupp.sum 0 h = 0
-- Mathlib.Computability.TuringMachine.Tape
Turing.proj_map_nth : ∀ {ι : Type u_1} {Γ : ι → Type u_2} [inst : (i : ι) → Inhabited (Γ i)] (i : ι) (L : Turing.ListBlank ((i : ι) → Γ i))
  (n : ℕ), (Turing.ListBlank.map (Turing.proj i) L).nth n = L.nth n i
-- Mathlib.Data.EReal.Operations
EReal.add_lt_top : ∀ {x y : EReal}, x ≠ ⊤ → y ≠ ⊤ → x + y < ⊤
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.id_eq : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] (X : CategoryTheory.CatEnriched C),
  CategoryTheory.CategoryStruct.id X = (CategoryTheory.eId CategoryTheory.Cat X).toFunctor.obj { down := { as := () } }
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceTo_sliceTo : ∀ {s : String.Slice} {p₀ p : s.Pos} {h : p ≤ p₀}, String.Slice.Pos.ofSliceTo (p₀.sliceTo p h) = p
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor_smul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant]
  {c : NNReal}, (c • μ').addHaarScalarFactor μ = c • μ'.addHaarScalarFactor μ
-- Mathlib.Order.DirSupClosed
dirSupInaccOn_compl : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α], DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s
-- Init.Data.SInt.Lemmas
Int8.toISize_ofNat' : ∀ {n : ℕ}, ↑n ≤ Int8.maxValue.toInt → (Int8.ofNat n).toISize = ISize.ofNat n
-- Std.Time.Format.Modifier
Std.Time.Modifier.x.sizeOf_spec : ∀ (presentation : Std.Time.OffsetX), sizeOf (Std.Time.Modifier.x presentation) = 1 + sizeOf presentation
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_sub_one : ∀ (r : ENNReal), ⌈r - 1⌉ₑ = ⌈r⌉ₑ - 1
-- Std.Internal.UV.UDP
/-- Receives data from an UDP socket. `size` is for the maximum bytes to receive. The promise
resolves when some data is available or an error occurs.
Furthermore calling this function in parallel with `waitReadable` is not supported.
 -/
Std.Internal.UV.UDP.Socket.recv : Std.Internal.UV.UDP.Socket → UInt64 → IO (IO.Promise (Except IO.Error (ByteArray × Option Std.Net.SocketAddress)))
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeWhisker_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C}
  {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cone F},
  H.mapConeWhisker.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Batteries.Data.AssocList
Batteries.AssocList.find?.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α), Batteries.AssocList.find? a Batteries.AssocList.nil = none
-- Mathlib.Data.Finset.SDiff
Finset.notMem_sdiff_of_mem_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ t → a ∉ s \ t
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.ofNatLT_reduce : ∀ {w : ℕ} (n : ℕ) (h : n < 2 ^ w), n#'h = BitVec.ofNat w n
-- Mathlib.GroupTheory.CoprodI
Con.ker.congr_simp : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] (f f_1 : F), f = f_1 → Con.ker f = Con.ker f_1
-- Init.Data.List.Lemmas
List.isEmpty_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α}, (List.replicate n a).isEmpty = decide (n = 0)
-- Init.Data.Float.Model.Float
Float.Model.mk.inj : ∀ {toBits : UInt64} {valid : Float.Model.Format.binary64.Valid toBits.toBitVec} {toBits_1 : UInt64}
  {valid_1 : Float.Model.Format.binary64.Valid toBits_1.toBitVec},
  { toBits := toBits, valid := valid } = { toBits := toBits_1, valid := valid_1 } → toBits = toBits_1
-- Init.Data.Array.Extract
Array.takeWhile_append_of_pos : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α},
  (∀ a ∈ xs, p a = true) → Array.takeWhile p (xs ++ ys) = xs ++ Array.takeWhile p ys
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_nonneg : ∀ {n : ℕ}, 0 ≤ ArithmeticFunction.vonMangoldt n
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_strict_mono : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α},
  HasSum f a₁ → HasSum g a₂ → f < g → a₁ < a₂
-- Lean.Data.PPContext
Lean.PPContext.openDecls : Lean.PPContext → List Lean.OpenDecl
-- Mathlib.Data.Finite.Prod
MulEquiv.finite_right : ∀ {α : Type u_3} {β : Type u_4} [inst : Mul α] [inst_1 : Mul β] [Finite β], Finite (α ≃* β)
-- Aesop.Forward.Substitution
/-- The empty substitution for a rule with the given number of premise
indexes.  -/
Aesop.Substitution.empty : ℕ → ℕ → Aesop.Substitution
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_eq_single : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : AddCommMonoid M] {f : α → M} (a : α),
  (∀ (x : α), x ≠ a → f x = 0) → ∑ x, f x = f a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.SemiCartesianMonoidalCategory C
-- Mathlib.Order.Interval.Finset.Defs
/-- An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances.  -/
IsEmpty.toLocallyFiniteOrderBot : {α : Type u_1} → [inst : Preorder α] → [IsEmpty α] → LocallyFiniteOrderBot α
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {n : Type u_4} [inst_2 : DecidableEq n]
  [inst_3 : Fintype n] (M : Matrix n n R) (f : R →+* S), (M.map ⇑f).charmatrix = M.charmatrix.map (Polynomial.map f)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseIdx.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (a : α) (as : List α) (n : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (head : α) → (as : List α) → motive (head :: as) 0)
  (h_3 : (a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ),
  (match a :: as, n.succ with
    | [], x => h_1 x
    | head :: as, 0 => h_2 head as
    | a :: as, n.succ => h_3 a as n) =
    h_3 a as n
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_15.eq_2 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : CategoryTheory.WithTerminal Cᵒᵖ) → (x ⟶ y) → Sort u_3) (unop : C)
  (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (x y : C) →
      (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y)) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op x)) (CategoryTheory.WithTerminal.of (Opposite.op y)) f)
  (h_2 :
    (unop : C) →
      (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op unop)) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => h_1 x y f
    | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => h_2 unop x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_2 unop x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.ShiftTarget w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Data.Finmap
Finmap.insert_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b b' : β a} (s : Finmap β),
  Finmap.insert a b' (Finmap.insert a b s) = Finmap.insert a b' s
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.alt.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (ctorName : Lean.Name) (params : Array (Lean.Compiler.LCNF.Param pu))
  (code : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_1) (ctorName_1 : Lean.Name)
  (params_1 : Array (Lean.Compiler.LCNF.Param pu)) (code_1 : Lean.Compiler.LCNF.Code pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_1),
  (Lean.Compiler.LCNF.Alt.alt ctorName params code h = Lean.Compiler.LCNF.Alt.alt ctorName_1 params_1 code_1 h_1) =
    (ctorName = ctorName_1 ∧ params = params_1 ∧ code = code_1)
-- Mathlib.NumberTheory.JacobiSum.Basic
_private.Mathlib.NumberTheory.JacobiSum.Basic.0.jacobiSum_eq_aux : ∀ {F : Type u_1} {R : Type u_2} [inst : CommRing F] [Nontrivial F] [inst_2 : Fintype F] [inst_3 : DecidableEq F]
  [inst_4 : CommRing R] (χ ψ : MulChar F R),
  jacobiSum χ ψ = ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ Finset.univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_apply_of_not_predicate : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f : R → R} (a : A),
  ¬p a → cfc f a = 0
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.equivCompletion_apply : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (self : v.Completion),
  (NumberField.InfinitePlace.Completion.equivCompletion v) self = self.toCompletion
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- Given `x, y : E ⊗ F`, `x = y` iff `⟪x, a ⊗ₜ b⟫ = ⟪y, a ⊗ₜ b⟫` for all `a, b`.  -/
TensorProduct.ext_iff_inner_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  {x y : TensorProduct 𝕜 E F}, x = y ↔ ∀ (a : E) (b : F), inner 𝕜 x (a ⊗ₜ[𝕜] b) = inner 𝕜 y (a ⊗ₜ[𝕜] b)