mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure : ∀ {G : Type u_3} {inst : AddGroup G} {inst_1 : TopologicalSpace G} {inst_2 : MeasurableSpace G}
  {μ : MeasureTheory.Measure G} [self : μ.IsAddHaarMeasure], μ.IsOpenPosMeasure
-- Init.Data.Vector.Lemmas
Vector.all_flatMap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m} {p : β → Bool},
  (xs.flatMap f).all p = xs.all fun a => (f a).all p
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.coe_normUnit_of_ne_zero : ∀ {R : Type u} [inst : Field R] {p : Polynomial R} [inst_1 : DecidableEq R],
  p ≠ 0 → ↑(normUnit p) = Polynomial.C p.leadingCoeff⁻¹
-- Init.Data.SInt.Bitwise
ISize.toBitVec_xor : ∀ (a b : ISize), (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The empty locally ringed space.  -/
AlgebraicGeometry.LocallyRingedSpace.empty : AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.Topology.Order
continuous_iInf_dom : ∀ {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} {i : ι},
  Continuous f → Continuous f
-- Mathlib.Data.List.MinMax
List.minimum_singleton : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] (a : α), [a].minimum = ↑a
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Bundle `αᵣ _ _ _` as an isomorphism of trifunctors.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso : (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.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
            CategoryTheory.bifunctorComp₁₂ (CategoryTheory.MonoidalCategory.curriedTensor C)
                (CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D) ≅
              (CategoryTheory.bifunctorComp₂₃ (CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D)
                  (CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D)).flip
-- Mathlib.Data.Finset.NAry
Finset.card_image₂_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
  (Finset.image₂ f s t).card = s.card * t.card ↔ Set.InjOn (fun x => f x.1 x.2) (↑s ×ˢ ↑t)
-- Init.Data.Option.Attach
Option.get_unattach : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }} {h : o.unattach.isSome = true}, o.unattach.get h = ↑(o.get ⋯)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_ciSup : ∀ {ι : Type u} (f : ι → Cardinal.{v}) (c : Cardinal.{v}), c * ⨆ i, f i = ⨆ i, c * f i
-- Mathlib.Data.Finsupp.Defs
/-- Given finitely supported functions `g₁ : α →₀ M` and `g₂ : α →₀ N` and function `f : M → N → O`,
`Finsupp.zipWith f hf g₁ g₂` is the finitely supported function `α →₀ O` satisfying
`zipWith f hf g₁ g₂ a = f (g₁ a) (g₂ a)`, which is well-defined when `f 0 0 = 0`.  -/
Finsupp.zipWith : {α : Type u_1} →
  {M : Type u_4} →
    {N : Type u_5} →
      {O : Type u_6} →
        [inst : Zero M] →
          [inst_1 : Zero N] → [inst_2 : Zero O] → (f : M → N → O) → f 0 0 = 0 → (α →₀ M) → (α →₀ N) → α →₀ O
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.isEmpty_of_commSq : ∀ {W X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {i : W ⟶ X} {j : W ⟶ Y},
  CategoryTheory.CommSq i j f g → Disjoint (Set.range ⇑f) (Set.range ⇑g) → IsEmpty ↥W
-- Lean.Data.Lsp.Extra
Lean.Lsp.HighlightMatchesOptions : Type
-- Mathlib.Topology.IsLocalHomeomorph
/-- Proves that `f` satisfies `IsLocalHomeomorph f`. The condition `h` is weaker than the
definition of `IsLocalHomeomorph f`, since it only requires `e : OpenPartialHomeomorph X Y` to
agree with `f` on its source `e.source`, as opposed to on the whole space `X`.  -/
IsLocalHomeomorph.mk : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  (∀ (x : X), ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source) → IsLocalHomeomorph f
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- An `AbstractSimplicialComplex` is a `PreAbstractSimplicialComplex` which contains all singletons.
 -/
AbstractSimplicialComplex : Type u_1 → Type u_1
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.mk.inj : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {toLinearMap : M →ₗ[R] N →ₗ[R] R}
  {isPerfPair_toLinearMap : toLinearMap.IsPerfPair} {root : ι ↪ M} {coroot : ι ↪ N}
  {root_coroot_two : ∀ (i : ι), (toLinearMap (root i)) (coroot i) = 2} {reflectionPerm : ι → ι ≃ ι}
  {reflectionPerm_root : ∀ (i j : ι), root j - (toLinearMap (root j)) (coroot i) • root i = root ((reflectionPerm i) j)}
  {reflectionPerm_coroot :
    ∀ (i j : ι), coroot j - (toLinearMap (root i)) (coroot j) • coroot i = coroot ((reflectionPerm i) j)}
  {toLinearMap_1 : M →ₗ[R] N →ₗ[R] R} {isPerfPair_toLinearMap_1 : toLinearMap_1.IsPerfPair} {root_1 : ι ↪ M}
  {coroot_1 : ι ↪ N} {root_coroot_two_1 : ∀ (i : ι), (toLinearMap_1 (root_1 i)) (coroot_1 i) = 2}
  {reflectionPerm_1 : ι → ι ≃ ι}
  {reflectionPerm_root_1 :
    ∀ (i j : ι), root_1 j - (toLinearMap_1 (root_1 j)) (coroot_1 i) • root_1 i = root_1 ((reflectionPerm_1 i) j)}
  {reflectionPerm_coroot_1 :
    ∀ (i j : ι), coroot_1 j - (toLinearMap_1 (root_1 i)) (coroot_1 j) • coroot_1 i = coroot_1 ((reflectionPerm_1 i) j)},
  { toLinearMap := toLinearMap, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
        root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm,
        reflectionPerm_root := reflectionPerm_root, reflectionPerm_coroot := reflectionPerm_coroot } =
      { toLinearMap := toLinearMap_1, isPerfPair_toLinearMap := isPerfPair_toLinearMap_1, root := root_1,
        coroot := coroot_1, root_coroot_two := root_coroot_two_1, reflectionPerm := reflectionPerm_1,
        reflectionPerm_root := reflectionPerm_root_1, reflectionPerm_coroot := reflectionPerm_coroot_1 } →
    toLinearMap = toLinearMap_1 ∧ root = root_1 ∧ coroot = coroot_1 ∧ reflectionPerm = reflectionPerm_1
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.optionEquivLeft_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : Option σ →₀ ℕ) (r : R),
  (MvPowerSeries.optionEquivLeft σ R) ((MvPowerSeries.monomial x) r) =
    (PowerSeries.monomial (x none)) ((MvPowerSeries.monomial x.some) r)
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestMatchAtChain_iff : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain c pos pos' ↔
    pos ≤ pos' ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h : pos'' < pos'), pos''.get ⋯ = c
-- Init.Data.Int.DivMod.Lemmas
Int.mod_bmod_mul_of_pos : ∀ {a : ℕ} (b : ℤ) (c : ℕ), 0 < a → 2 ∣ c → (↑a * b).bmod (a * c) = ↑a * b.bmod c
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.toPresheafOfModules_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (N : M.Submodule) (X : Cᵒᵖ),
  N.toPresheafOfModules.obj X = ModuleCat.of ↑(R.obj X) ↥(N.obj X)
-- Mathlib.Topology.Compactness.Lindelof
/-- The disjoint union of two Lindelöf spaces is Lindelöf.  -/
instLindelofSpaceSum : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LindelofSpace X]
  [LindelofSpace Y], LindelofSpace (X ⊕ Y)
-- Mathlib.Order.Preorder.Finsupp
/-- The order on `Finsupp`s over a partial order embeds into the order on functions  -/
Finsupp.orderEmbeddingToFun : {ι : Type u_1} → {M : Type u_2} → [inst : Zero M] → [inst_1 : LE M] → (ι →₀ M) ↪o (ι → M)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_add_add_comm_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M]
  {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)
-- Init.System.ST
EST.Out.ok : {ε σ α : Type} → α → Void σ → EST.Out ε σ α
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.instTopologicalSpace : TopologicalSpace UpperHalfPlane
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.rid`.  -/
TensorProduct.AlgebraTensorModule.rid : (R : Type uR) →
  (A : Type uA) →
    (M : Type uM) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module A M] → [inst_6 : IsScalarTower R A M] → TensorProduct R M R ≃ₗ[A] M
-- Init.Data.BitVec.Bitblast
BitVec.shiftLeftRec_zero : ∀ {w₁ w₂ : ℕ} {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec y 0 = x <<< (y &&& BitVec.twoPow w₂ 0)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticSequence.id : IsEllipticSequence id
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.freeYoneda.isDetecting : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  (PresheafOfModules.freeYoneda R).IsDetecting
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesMap_opcyclesIso_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (γ : CategoryTheory.ComposableArrows.mk₂ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₂ f₂' f₃'),
  autoParam (γ = CategoryTheory.ComposableArrows.homMk₂ (α.app 1) (α.app 2) (α.app 3) ⋯ ⋯)
      CategoryTheory.Abelian.SpectralObject.opcyclesMap_opcyclesIso_hom._auto_1 →
    ∀ (n₀ n₁ n₂ : ℤ)
      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesMap_opcyclesIso_hom._auto_3)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesMap_opcyclesIso_hom._auto_5),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.ShortComplex.opcyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂))
          (X.opcyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).hom =
        CategoryTheory.CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom
          (X.opcyclesMap f₂ f₃ f₂' f₃' γ n₁)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_zero : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A], CFC.abs 0 = 0
-- Init.Data.SInt.Lemmas
Int32.ofNat_int16ToNatClampNeg : ∀ (x : Int16), 0 ≤ x → Int32.ofNat x.toNatClampNeg = x.toInt32
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.ofFreeAddGroup.eq_1 : ∀ (X : Type u_5), FreeAddGroupBasis.ofFreeAddGroup X = { repr := AddEquiv.refl (FreeAddGroup X) }
-- Mathlib.Analysis.Asymptotics.TVS
ContinuousLinearMap.isThetaTVS_comp : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} (g : E →L[𝕜] F),
  Topology.IsInducing ⇑g → (⇑g ∘ f) =Θ[𝕜; l] f
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupUnits : {numVarsSucc : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula numVarsSucc →
    Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))
-- Std.Do.Triple.SpecLemmas
/-- Converts a range to the list of all numbers in the range.
 -/
Std.Legacy.Range.toList : Std.Legacy.Range → List ℕ
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- The sum of a locally finite collection of sections is differentiable on a set `u`
if each section is.  -/
MDifferentiableOn.sum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B}
  {ι : Type u_9} {t : ι → (x : B) → E x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) → (∀ (i : ι), MDiff[u] (T% t)) → MDiff[u] fun x => ⟨x, ∑' (i : ι), t i x⟩
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.hexagon_reverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).braiding Z).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) (Y.braiding Z).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.braiding Z).hom (CategoryTheory.CategoryStruct.id Y)))
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.inducedFunctor_comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor C 𝒳} (hF : F.comp p = (CategoryTheory.Functor.const C).obj S),
  (CategoryTheory.Functor.Fiber.inducedFunctor hF).comp CategoryTheory.Functor.Fiber.fiberInclusion = F
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
/-- The `Finset` of walks from `u` to `v` with length less than `n`. See `finsetWalkLength` for
context. In particular, we use this definition for `SimpleGraph.Path.instFintype`.  -/
SimpleGraph.finsetWalkLengthLT : {V : Type u} → (G : SimpleGraph V) → [DecidableEq V] → [G.LocallyFinite] → ℕ → (u v : V) → Finset (G.Walk u v)
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instIsCancelMulZero : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [IsCancelMulZero α], IsCancelMulZero (Lex α)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_Ioi : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R},
  0 ≤ a → Nat.cast ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋₊
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop},
  Filter.blimsup u f p = sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
-- Init.Data.BitVec.Lemmas
/-- zero extending a bitvector to width 1 equals the boolean of the lsb.  -/
BitVec.setWidth_one_eq_ofBool_getLsb_zero : ∀ {w : ℕ} (x : BitVec w), BitVec.setWidth 1 x = BitVec.ofBool (x.getLsbD 0)
-- Init.GrindInstances.ToInt
Lean.Grind.instLTUSizeUintNumBits : Lean.Grind.ToInt.LT USize (Lean.Grind.IntInterval.uint System.Platform.numBits)
-- Mathlib.Tactic.GCongr.Core
/-- Check whether `e` has a `gcongrHole` mdata annotation.  -/
Mathlib.Tactic.GCongr.hasHoleAnnotation : Lean.Expr → Bool
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- In finite-dimensional spaces, a continuous linear map is positive iff it is equal to the sum
of rank-one positive operators.  -/
ContinuousLinearMap.isPositive_iff_eq_sum_rankOne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {T : E →L[𝕜] E}, T.IsPositive ↔ ∃ m u, T = ∑ i, ((InnerProductSpace.rankOne 𝕜) (u i)) (u i)
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.continuous_isUnit_unit : ∀ {X : Type u_1} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : NormedRing R] [CompleteSpace R] {f : C(X, R)}
  (h : ∀ (x : X), IsUnit (f x)), Continuous fun x => ⋯.unit
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_univ_pi : ∀ {M : Type u_5} {ι : Type u_6} {π : ι → Type u_7} [inst : (i : ι) → SMul M (π i)] (c : M) (s : (i : ι) → Set (π i)),
  c • Set.univ.pi s = Set.univ.pi (c • s)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.exists_subset_lt_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : Set α → Prop} {U : Set α} {ε : ENNReal},
  μ.InnerRegularWRT p q → p ∅ → q U → μ U ≠ ⊤ → ε ≠ 0 → ∃ K ⊆ U, p K ∧ μ U < μ K + ε
-- Mathlib.RingTheory.Algebraic.Integral
/-- In an algebra generated by a single algebraic element over a domain `R`, every element is
algebraic. This may fail when `R` is not a domain: see https://mathoverflow.net/a/132192/ for
an example.  -/
Algebra.isAlgebraic_adjoin_singleton_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors R]
  {s : S}, R[s].IsAlgebraic ↔ IsAlgebraic R s
-- Mathlib.LinearAlgebra.Dimension.OrzechProperty
linearIndependent_of_top_le_span_of_card_le_finrank : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [OrzechProperty R] [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  {ι : Type u_3} [inst_4 : Fintype ι] {b : ι → M},
  ⊤ ≤ Submodule.span R (Set.range b) → Fintype.card ι ≤ Module.finrank R M → LinearIndependent R b
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.vecMul_fromCols : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Semiring R] [inst_1 : Fintype m]
  (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R),
  Matrix.vecMul v (B₁.fromCols B₂) = Sum.elim (Matrix.vecMul v B₁) (Matrix.vecMul v B₂)
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Asymptotics.isLittleO_sum_range_of_tendsto_zero : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] {f : ℕ → α},
  Filter.Tendsto f Filter.atTop (nhds 0) → (fun n => ∑ i ∈ Finset.range n, f i) =o[Filter.atTop] fun n => ↑n
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (L : CategoryTheory.Functor (HomotopicalAlgebra.CofibrantObject.HoCat C) D)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject.HoCat C))],
  CategoryTheory.IsIso
    (CategoryTheory.Functor.whiskerRight HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans L)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lt_lift_iff : ∀ {a : Ordinal.{u}} {b : Ordinal.{max u v}}, b < Ordinal.lift.{v, u} a ↔ ∃ a' < a, Ordinal.lift.{v, u} a' = b
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm' : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} [inst : ENorm ε] {μ : MeasureTheory.Measure α}
  {f : α → ε}, 0 < q → ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = MeasureTheory.eLpNorm' f q μ ^ q
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_sub : ∀ (a b c : Ordinal.{u_4}), a * (b - c) = a * b - a * c
-- Mathlib.Topology.Category.Profinite.Limits
Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier : CompHausLike.HasExplicitFiniteCoproducts fun Y => TotallyDisconnectedSpace ↑Y
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.opENorm_le_bound₂ : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {C : ENNReal},
  (∀ (x : E) (y : F), ‖(f x) y‖ₑ ≤ C * ‖x‖ₑ * ‖y‖ₑ) → ‖f‖ₑ ≤ C
-- Mathlib.Data.Nat.Fib.Zeckendorf
List.IsZeckendorfRep_nil : [].IsZeckendorfRep
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} →
      {I : Type w'} →
        {U : I → C} →
          (ev : (i j : I) → ⦃T : C⦄ → (T ⟶ U i) → (T ⟶ U j) → ↑(G.obj (Opposite.op T))) →
            autoParam
                (∀ (i j : I) ⦃T T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i) (b : T' ⟶ U j),
                  (CategoryTheory.ConcreteCategory.hom (G.map φ.op)) (ev i j a b) =
                    ev i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b))
                CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp._autoParam →
              CategoryTheory.PresheafOfGroups.OneCochain G U
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.ofIdComp_left_as : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t :
    CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)),
  t.ofIdComp.left.as = PUnit.unit
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.atom_eq_eval : ∀ {M : Type u_1} [inst : GroupWithZero M] (x : M), x = Mathlib.Tactic.FieldSimp.NF.eval [(1, x)]
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.natCast_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (n : ℕ), (↑n).toProd.2 = ↑n
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- A `grw` suggestion section.  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.grw : Mathlib.Tactic.ClickSuggestions.GrwInfo →
  Array Mathlib.Tactic.ClickSuggestions.GrwLemma → Mathlib.Tactic.ClickSuggestions.Candidates✝
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- If the image of an element `m : M` in `R[M]` belongs the submodule generated by
the closure of some `s : Set M` then `m ∈ closure s`.  -/
AddMonoidAlgebra.mem_closure_of_mem_span_closure : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddMonoid M] [Nontrivial R] {m : M} {s : Set M},
  AddMonoidAlgebra.of' R M m ∈ Submodule.span R ↑(Submonoid.closure (AddMonoidAlgebra.of' R M '' s)) →
    m ∈ AddSubmonoid.closure s