mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Eta-expanded form of `CircleIntegrable.mul_continuousOn`

---

If `f` is circle integrable and `g` is continuous on the circle `sphere c |R|`, then `f * g` is
circle integrable.
 -/
CircleIntegrable.fun_mul_continuousOn : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [inst : NormedRing 𝕜] {f g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (fun i => f i * g i) c R
-- Lean.Meta.Tactic.Util
Lean.Meta.appendTagSuffix : Lean.MVarId → Lean.Name → Lean.MetaM Unit
-- Mathlib.Data.Num.Basic
ZNum.neg.inj : ∀ {a a_1 : PosNum}, ZNum.neg a = ZNum.neg a_1 → a = a_1
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toRealPositiveLinear_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] {Λ : CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal}
  (f : CompactlySupportedContinuousMap α ℝ),
  (CompactlySupportedContinuousMap.toRealPositiveLinear Λ) f = ↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart)
-- Mathlib.Analysis.Calculus.Taylor
taylor_isLittleO_univ : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {x₀ : ℝ} {n : ℕ},
  ContDiff ℝ (↑n) f → (fun x => f x - taylorWithinEval f n Set.univ x₀ x) =o[nhds x₀] fun x => (x - x₀) ^ n
-- Mathlib.Order.Atoms
isCoatomistic_iff : ∀ (α : Type u_2) [inst : PartialOrder α] [inst_1 : OrderTop α],
  IsCoatomistic α ↔ ∀ (b : α), ∃ s, IsGLB s b ∧ ∀ a ∈ s, IsCoatom a
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma_cong_eq_self : ∀ (N : ℕ) (g : ConjAct (Matrix.SpecialLinearGroup (Fin 2) ℤ)),
  g • CongruenceSubgroup.Gamma N = CongruenceSubgroup.Gamma N
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Cofan.cofanTypes_pt : ∀ {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.Cofan F), c.cofanTypes.pt = c.pt
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {km : α}, t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare km k).isLE = true
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.Red.reduce_left : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ (FreeGroup.reduce L₁)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Transport being a right adjoint along a natural isomorphism.  -/
CategoryTheory.Functor.isRightAdjoint_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) [F.IsRightAdjoint], G.IsRightAdjoint
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α},
  k ∉ m₁ → Std.ExtDHashMap.Const.get? (m₁.union m₂) k = Std.ExtDHashMap.Const.get? m₂ k
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the sign of the oriented angle at `p` between two points is zero, either one of the points
equals `p` or the unoriented angle is 0 or π.  -/
EuclideanGeometry.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ : P},
  (EuclideanGeometry.oangle p₁ p p₂).sign = 0 →
    p₁ = p ∨ p₂ = p ∨ EuclideanGeometry.angle p₁ p p₂ = 0 ∨ EuclideanGeometry.angle p₁ p p₂ = Real.pi
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- If a function has compact multiplicative support, then either the function is trivial
or the space is finite-dimensional.  -/
HasCompactMulSupport.eq_one_or_finiteDimensional : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_5} [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  {X : Type u_7} [inst_8 : TopologicalSpace X] [inst_9 : One X] [T1Space X] {f : E → X},
  HasCompactMulSupport f → Continuous f → f = 1 ∨ FiniteDimensional 𝕜 E
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_addSubgroup_left_iff_bijective : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G},
  AddSubgroup.IsComplement (↑H) T ↔ Function.Bijective (T.domRestrict Quotient.mk'')
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instCharZero : ∀ {R : Type u_1} {a b : R} [inst : CommRing R] [CharZero R], CharZero (QuadraticAlgebra R a b)
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_bijective_fromSigma : ∀ {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.Cofan F),
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔
    Function.Bijective (CategoryTheory.Limits.CofanTypes.fromSigma F c.cofanTypes)
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.div_tendsto_atBot_leadingCoeff_div_of_degree_eq : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  P.degree = Q.degree →
    Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atBot
      (nhds (P.leadingCoeff / Q.leadingCoeff))
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ext_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {m₁ m₂ : Std.ExtHashSet α}, (∀ (k : α), m₁.get? k = m₂.get? k) → m₁ = m₂
-- Mathlib.Tactic.TFAE
/-- See `haveEqnsDecl`. E.g. `h : 1 → 3 | p => f p`.  -/
Mathlib.Tactic.TFAE.Parser.tfaeHaveEqnsDecl : Lean.Parser.Parser
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.aroots_minpoly_eq_carrier_val : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsSeparable K L]
  (c : ConjRootClass K L) [inst_4 : Fintype ↑c.carrier], c.minpoly.aroots L = c.carrier.toFinset.val
-- Mathlib.RingTheory.WittVector.Verschiebung
/-- `WittVector.verschiebung` has polynomial structure given by `WittVector.verschiebungPoly`.
 -/
WittVector.verschiebungFun_isPoly : ∀ (p : ℕ), WittVector.IsPoly p fun R _Rcr => WittVector.verschiebungFun
-- Init.Data.SInt.Lemmas
Int8.eq_iff_toBitVec_eq : ∀ {a b : Int8}, a = b ↔ a.toBitVec = b.toBitVec
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.map_vertex : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} {Y : Type u_3} [inst_2 : Fintype X]
  [inst_3 : Fintype Y] [inst_4 : IsOrderedRing S] [inst_5 : DecidableEq X] [inst_6 : DecidableEq Y] (f : X → Y) (x : X),
  stdSimplex.map f (stdSimplex.vertex x) = stdSimplex.vertex (f x)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- Given a left homology map data `ψ : LeftHomologyMapData φ h₁ h₂` such that
both left homology data `h₁` and `h₂` are preserved by a functor `F`, this is
the induced left homology map data for the morphism `F.mapShortComplex.map φ`.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.map : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {S₁ S₂ : CategoryTheory.ShortComplex C} →
              {φ : S₁ ⟶ S₂} →
                {h₁ : S₁.LeftHomologyData} →
                  {h₂ : S₂.LeftHomologyData} →
                    CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂ →
                      (F : CategoryTheory.Functor C D) →
                        [inst_4 : F.PreservesZeroMorphisms] →
                          [inst_5 : h₁.IsPreservedBy F] →
                            [inst_6 : h₂.IsPreservedBy F] →
                              CategoryTheory.ShortComplex.LeftHomologyMapData (F.mapShortComplex.map φ) (h₁.map F)
                                (h₂.map F)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.subtype.eq_1 : ∀ {M : Type u_4} [inst : MulOneClass M] (S : Submonoid M),
  S.subtype = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `(F ⋙ forget MonCat).sections` is `u`-small, `F` has a limit.  -/
MonCat.HasLimits.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.Analysis.Matrix.Normed
Matrix.nnnorm_lt_iff : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] {r : NNReal},
  0 < r → ∀ {A : Matrix m n α}, ‖A‖₊ < r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ < r
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- No points are in `⊥`.  -/
AffineSubspace.notMem_bot : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (p : P), p ∉ ⊥
-- Lean.Expr
/-- Literal values for `Expr`.  -/
Lean.Literal : Type
-- Mathlib.Topology.Order.ExtrClosure
IsLocalExtrOn.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Preorder Y]
  [OrderClosedTopology Y] {f : X → Y} {s : Set X} {a : X},
  IsLocalExtrOn f s a → ContinuousOn f (closure s) → IsLocalExtrOn f (closure s) a
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.map.eq_1 : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_4)
  [inst_3 : CommSemiring S] {N : Type u_5} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : Module S N]
  (f : M →ₗ[R] N) [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S N],
  DividedPowerAlgebra.map S f = DividedPowerAlgebra.lift' ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
MulEquivClass.map_nonZeroDivisors : ∀ {M₀ : Type u_4} {S : Type u_5} {F : Type u_6} [inst : MonoidWithZero M₀] [inst_1 : MonoidWithZero S]
  [inst_2 : EquivLike F M₀ S] [inst_3 : MulEquivClass F M₀ S] (h : F),
  Submonoid.map h (nonZeroDivisors M₀) = nonZeroDivisors S
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.inclLeftFaithful : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Join.inclLeft C D).Faithful
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∈ m₂ → (m₁ ∩ m₂).get! k = m₁.get! k
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_def'_cert : Int.Internal.Linear.Var → Int.Internal.Linear.Expr → Int.Internal.Linear.Poly → Bool
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.pullbackObjIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D),
  CategoryTheory.Limits.pullbackObjIso f g d =
    CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (CategoryTheory.Limits.cospan f g) d ≪≫
      CategoryTheory.Limits.HasLimit.isoOfNatIso
        (CategoryTheory.Limits.diagramIsoCospan
          ((CategoryTheory.Limits.cospan f g).comp ((CategoryTheory.evaluation D C).obj d)))
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
/-- The bounded above derived category of an abelian category.  -/
DerivedCategory.Minus : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [HasDerivedCategory C] → Type (max u v)
-- Mathlib.Algebra.Star.CHSH
/-- A CHSH tuple in a \*-monoid consists of 4 self-adjoint involutions `A₀ A₁ B₀ B₁` such that
the `Aᵢ` commute with the `Bⱼ`.

The physical interpretation is that `A₀` and `A₁` are a pair of Boolean observables which
are spacelike separated from another pair `B₀` and `B₁` of Boolean observables.
 -/
IsCHSHTuple : {R : Type u_1} → [inst : Monoid R] → [StarMul R] → R → R → R → R → Prop
-- Mathlib.GroupTheory.IsSubnormal
/-- An additive subgroup `H` of an additive group `G` satisfies `IsSubnormal` if
* either `H = ⊤`;
* or there is an additive subgroup `K` of `G` containing `H` and such that `H` is normal in `K` and
  `K` satisfies `IsSubnormal`.

Equivalently, `H.IsSubnormal` means that there is a chain of additive subgroups
`H₀ ≤ H₁ ≤ ... ≤ Hₙ` such that
* `H = H₀`,
* `G = Hₙ`,
* for each `i ∈ {0, ..., n - 1}`, `Hᵢ` is a normal additive subgroup of `Hᵢ₊₁`.

See `isSubnormal_iff` for this characterisation.
 -/
AddSubgroup.IsSubnormal : {G : Type u_2} → [inst : AddGroup G] → AddSubgroup G → Prop
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_sub_sub : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Sub β]
  [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.CondIndepFun m' hm' (f i - f j) (f k - f l) μ
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonServerCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.ServerCapabilities
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_sub_nat : ∀ (f : CircleDeg1Lift) (x : ℝ) (n : ℕ), f (x - ↑n) = f x - ↑n
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.mk : (value : String) →
  autoParam (Std.Http.Header.IsValidHeaderName value) Std.Http.Header.Name.isValidHeaderValue._autoParam →
    autoParam (Std.Http.Internal.IsLowerCase value) Std.Http.Header.Name.isLowerCase._autoParam → Std.Http.Header.Name
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
/-- Variant of `eisensteinSeries_tendstoLocallyUniformly` formulated with maps `ℂ → ℂ`, which is
nice to have for holomorphicity later.  -/
EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn : ∀ {k : ℤ} {N : ℕ},
  3 ≤ k →
    ∀ (a : Fin 2 → ZMod N),
      TendstoLocallyUniformlyOn
        (fun s => (fun z => ∑ x ∈ s, EisensteinSeries.eisSummand k (↑x) z) ∘ ↑UpperHalfPlane.ofComplex)
        (⇑(EisensteinSeries.eisensteinSeriesSIF a k) ∘ ↑UpperHalfPlane.ofComplex) Filter.atTop {z | 0 < z.im}
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.tendsto_nhds_nhds : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {a : α} {b : β},
  Filter.Tendsto f (nhds a) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) b < ε
-- Init.Data.List.ToArray
List.toArray_replicate : ∀ {α : Type u_1} (n : ℕ) (v : α), (List.replicate n v).toArray = Array.replicate n v
-- Init.Data.List.Scan.Lemmas
List.getElem?_scanl_zero : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β}, (List.scanl f b l)[0]? = some b
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Permuting rows and columns with the same equivalence does not change the determinant.  -/
Matrix.det_submatrix_equiv_self : ∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] {R : Type v} [inst_4 : CommRing R] (e : n ≃ m) (A : Matrix m m R),
  (A.submatrix ⇑e ⇑e).det = A.det
-- Mathlib.Algebra.Ring.Defs
/-- A not-necessarily-unital, not-necessarily-associative ring.  -/
NonUnitalNonAssocRing : Type u → Type u
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_insertList_of_contains_eq_false_left : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.containsKey k l = false →
        Std.Internal.List.getValueD k (Std.Internal.List.insertList l toInsert) fallback =
          Std.Internal.List.getValueD k toInsert fallback
-- Mathlib.RingTheory.SimpleModule.Isotypic
Submodule.le_isotypicComponent : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (m : Submodule R M),
  m ≤ isotypicComponent R M ↥m
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `none` if no such key exists.
 -/
Std.ExtDTreeMap.getKeyLT? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Option α
-- Mathlib.Topology.UniformSpace.Basic
entourageProd_subset : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {s : Set ((α × β) × α × β)},
  s ∈ uniformity (α × β) → ∃ u ∈ uniformity α, ∃ v ∈ uniformity β, entourageProd u v ⊆ s
-- Init.Data.BitVec.Basic
/-- We prefer `x[i]?` as the simp normal form for `getLsb?`  -/
BitVec.getLsb?_eq_getElem? : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x.getLsb? i = x[i]?
-- Lean.Meta.LazyDiscrTree
/-- Information generation from imported modules.  -/
Lean.Meta.LazyDiscrTree.ImportData : Type
-- Mathlib.RingTheory.Ideal.Height
/-- A prime ideal has height zero if and only if it is minimal  -/
Ideal.height_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [I.IsPrime], I.height = 0 ↔ I ∈ minimalPrimes R
-- Mathlib.FieldTheory.AlgebraicClosure
/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
if it is algebraic over `F`.  -/
le_algebraicClosure : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  [Algebra.IsAlgebraic F ↥L], L ≤ algebraicClosure F E
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Expr.denote.match_1.eq_7 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (a : Lean.Grind.Linarith.Expr)
  (h_1 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_2 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_3 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b))
  (h_5 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (h_6 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_7 : (a : Lean.Grind.Linarith.Expr) → motive a.neg),
  (match a.neg with
    | Lean.Grind.Linarith.Expr.zero => h_1 ()
    | Lean.Grind.Linarith.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_5 k a
    | Lean.Grind.Linarith.Expr.intMul k a => h_6 k a
    | a.neg => h_7 a) =
    h_7 a
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_eq_subst_cert : Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.instFree : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, Module.Free R W'.CoordinateRing
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.move_right_mk' : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (L R : Turing.ListBlank Γ),
  Turing.Tape.move Turing.Dir.right (Turing.Tape.mk' L R) = Turing.Tape.mk' (Turing.ListBlank.cons R.head L) R.tail
-- Mathlib.Topology.VectorBundle.Riemannian
/-- Given two continuous maps into the same fibers of a continuous Riemannian bundle,
their inner product is continuous. Version with `ContinuousWithinAt`.  -/
ContinuousWithinAt.inner_bundle : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F : Type u_2} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_3} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E] {M : Type u_4}
  [inst_8 : TopologicalSpace M] [h : IsContinuousRiemannianBundle F E] {b : M → B} {v w : (x : M) → E (b x)} {s : Set M}
  {x : M},
  ContinuousWithinAt (fun m => ⟨b m, v m⟩) s x →
    ContinuousWithinAt (fun m => ⟨b m, w m⟩) s x → ContinuousWithinAt (fun m => inner ℝ (v m) (w m)) s x
-- Mathlib.Topology.ContinuousOn
ContinuousOn.finCons : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {X : Fin (n + 1) → Type u_5}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)] {f : α → X 0} {s : Set α} {g : α → (j : Fin n) → X j.succ},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun a => Fin.cons (f a) (g a)) s
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.delta_mul : ∀ {f : ℕ → ℂ}, f 1 = 1 → LSeries.delta * f = LSeries.delta
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Mapping from variables to their denotations.
Remark each variable can be in only one ring.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.vars : Lean.Meta.Grind.Arith.Linear.Struct → Lean.PArray Lean.Expr
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
/-- The convolution `f * g` is `C^n` when `f` is locally integrable and `g` is `C^n` and compactly
supported. Version where `g` depends on an additional parameter in an open subset `s` of a
parameter space `P` (and the compact support `k` is independent of the parameter in `s`).  -/
MeasureTheory.contDiffOn_convolution_right_with_param : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [inst_8 : MeasurableSpace G]
  [inst_9 : NormedAddCommGroup G] [BorelSpace G] [inst_11 : NormedSpace 𝕜 G] [inst_12 : NormedAddCommGroup P]
  [inst_13 : NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} {f : G → E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F)
  {g : P → G → E'} {s : Set P} {k : Set G},
  IsOpen s →
    IsCompact k →
      (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
        MeasureTheory.LocallyIntegrable f μ →
          ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ) →
            ContDiffOn 𝕜 (↑n) (fun q => MeasureTheory.convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)
-- Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
IsHomeomorphicTrivialFiberBundle.proj_eq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B}, IsHomeomorphicTrivialFiberBundle F proj → ∃ e, proj = Prod.fst ∘ ⇑e
-- Mathlib.Analysis.Convex.Function
ConcaveOn.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E}
  {f g : E → β}, ConcaveOn 𝕜 s f → Set.EqOn f g s → ConcaveOn 𝕜 s g
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- The fields `levelParams` and `proof` are used to encode the proof of the simp theorem.
If the `proof` is a global declaration `c`, we store `Expr.const c []` at `proof` without the universe levels, and `levelParams` is set to `#[]`
When using the lemma, we create fresh universe metavariables.
Motivation: most simp theorems are global declarations, and this approach is faster and saves memory.

The field `levelParams` is not empty only when we elaborate an expression provided by the user, and it contains universe metavariables.
Then, we use `abstractMVars` to abstract the universe metavariables and create new fresh universe parameters that are stored at the field `levelParams`.
 -/
Lean.Meta.SimpTheorem : Type
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
ClassGroup.extendedIdeal.congr_simp : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Module.IsTorsionFree A B] [inst_4 : IsDomain A] [inst_5 : IsDomain B]
  (I I_1 : ↥(nonZeroDivisors (Ideal A))), I = I_1 → ClassGroup.extendedIdeal A B I = ClassGroup.extendedIdeal A B I_1