mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- The space of continuous multilinear maps over an algebra over `R` is a module over `R`, for the
pointwise addition and scalar multiplication.  -/
ContinuousMultilinearMap.instModule : {ι : Type v} →
  {M₁ : ι → Type w₁} →
    {M₂ : Type w₂} →
      {R' : Type u_1} →
        {A : Type u_2} →
          [inst : Semiring R'] →
            [inst_1 : Semiring A] →
              [inst_2 : (i : ι) → AddCommMonoid (M₁ i)] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_5 : TopologicalSpace M₂] →
                      [inst_6 : ContinuousAdd M₂] →
                        [inst_7 : (i : ι) → Module A (M₁ i)] →
                          [inst_8 : Module A M₂] →
                            [inst_9 : Module R' M₂] →
                              [ContinuousConstSMul R' M₂] →
                                [SMulCommClass A R' M₂] → Module R' (ContinuousMultilinearMap A M₁ M₂)
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.takeWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  s.takeWhile pat = s.sliceTo (s.skipPrefixWhile pat)
-- Mathlib.Algebra.BigOperators.Finprod
mul_finprod_cond_ne : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} (a : α),
  Function.HasFiniteMulSupport f → f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.singleton_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} (f : S ⟶ T)
  (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings T),
  (CategoryTheory.Precoverage.ZeroHypercover.singleton f hf).toPreZeroHypercover =
    CategoryTheory.PreZeroHypercover.singleton f
-- Mathlib.RingTheory.TensorProduct.Basic
LinearMap.liftBaseChange_one_tmul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module A N] [inst_8 : IsScalarTower R A N] (l : M →ₗ[R] N) (y : M),
  (LinearMap.liftBaseChange A l) (1 ⊗ₜ[R] y) = l y
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.equivOfIso_apply : ∀ {X Y : SSet} (e : X ≅ Y) (s : X.S),
  (SSet.S.equivOfIso e) s =
    { dim := s.dim,
      simplex := (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := s.dim }))) s.simplex }
-- Mathlib.Order.LiminfLimsup
Filter.mono_blimsup' : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α},
  (∀ᶠ (x : β) in f, p x → u x ≤ v x) → Filter.blimsup u f p ≤ Filter.blimsup v f p
-- Std.Internal.Do.Order.PreservesSup
/-- The frame rule, internalized: for a family of `Sup`-preserving operators `op r` whose resources
compose by `comp` with the action law `op (comp r r') = op r ∘ op r'`, and any post-transformer `k`,
`op F (frameClosure op k Q) ⊑ frameClosure op k (fun a => op F (Q a))`.  -/
Lean.Order.PreservesSup.frameClosure_frames : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {R : Type v} {β : Type w} (op : R → α → α)
  [∀ (r : R), Lean.Order.PreservesSup (op r)] (comp : R → R → R),
  (∀ (r r' : R) (a : α), op (comp r r') a = op r (op r' a)) →
    ∀ (k : (β → α) → α) (Q : β → α) (F : R),
      Lean.Order.PartialOrder.rel (op F (Lean.Order.PreservesSup.frameClosure op k Q))
        (Lean.Order.PreservesSup.frameClosure op k fun a => op F (Q a))
-- Init.Data.UInt.Bitwise
UInt16.ofFin_shiftRight : ∀ (a b : Fin UInt16.size), ↑b < 16 → UInt16.ofFin (a >>> b) = UInt16.ofFin a >>> UInt16.ofFin b
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.instFullPlusQuotient : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  (HomotopyCategory.Plus.quotient C).Full
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.forget_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) {Y X : CategoryTheory.Limits.Cocone F} (f : Y ⟶ X),
  (CategoryTheory.Limits.Cocone.forget F).map f = f.hom
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `M` is finite free over a PID `R`, then for any submodule `N` of the same rank,
we can find basis for `M` and `N` with the same indexing such that the inclusion map
is a square diagonal matrix; this is the basis for `N`. See:
* `Submodule.smithNormalFormTopBasis` for the basis on `M`,
* `Submodule.smithNormalFormCoeffs` for the entries of the diagonal matrix
* `Submodule.smithNormalFormBotBasis_def` for the proof that the inclusion map
  forms a square diagonal matrix.
 -/
Submodule.smithNormalFormBotBasis : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsDomain R] →
              [IsPrincipalIdealRing R] →
                {N : Submodule R M} →
                  [Finite ι] → Module.Basis ι R M → Module.finrank R ↥N = Module.finrank R M → Module.Basis ι R ↥N
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_closure : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (s : Set R),
  (Subsemiring.closure s).op = Subsemiring.closure (MulOpposite.unop ⁻¹' s)
-- Mathlib.GroupTheory.OrderOfElement
/-- See `AddSubgroup.closure_toAddSubmonoid_of_finite` for a version for finite additive groups.  -/
AddSubgroup.closure_toAddSubmonoid_of_isOfFinAddOrder : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G},
  (∀ x ∈ s, IsOfFinAddOrder x) → (AddSubgroup.closure s).toAddSubmonoid = AddSubmonoid.closure s
-- Mathlib.FieldTheory.Differential.Liouville
IsLiouville.trans : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Differential F] [inst_3 : Differential K]
  [inst_4 : Algebra F K] [DifferentialAlgebra F K] {A : Type u_3} [inst_6 : Field A] [inst_7 : Algebra K A]
  [inst_8 : Algebra F A] [inst_9 : Differential A] [IsScalarTower F K A] [Differential.ContainConstants F K],
  IsLiouville F K → IsLiouville K A → IsLiouville F A
-- Init.Data.Dyadic.Basic
Dyadic.ofIntWithPrec_shiftLeft_add : ∀ {x i : ℤ} {n : ℕ}, Dyadic.ofIntWithPrec (x <<< n) (i + ↑n) = Dyadic.ofIntWithPrec x i
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_nsmul_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F) (n : ℕ)
  (α : A₁ ⟶ A₂), (n • α).f = n • α.f
-- Mathlib.Data.Matrix.Composition
Matrix.compLinearEquiv_symm_apply : ∀ (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) (R₀ : Type u_7) [inst : Semiring R₀]
  [inst_1 : AddCommMonoid R] [inst_2 : Module R₀ R] (a : Matrix (I × K) (J × L) R),
  (Matrix.compLinearEquiv I J K L R R₀).symm a = (Matrix.comp I J K L R).symm a
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instAddCommMonoid : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : AddCommMonoid γ] → [ContinuousAdd γ] → AddCommMonoid (α →ₘ[μ] γ)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.restrictionToTruncGE'.comm_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i j : ι) {Z : C} (h : (K.truncGE' e).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionToTruncGE'.f K e i)
      (CategoryTheory.CategoryStruct.comp ((K.truncGE' e).d i j) h) =
    CategoryTheory.CategoryStruct.comp ((K.restriction e).d i j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionToTruncGE'.f K e j) h)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The embedding `v.Completion →+* ℝ` associated to a real infinite place has closed image
inside `ℝ`.  -/
NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbeddingOfIsReal : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal),
  IsClosed (Set.range ⇑(NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv))
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Comon_EquivMon_OpOp_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Comon.Comon_EquivMon_OpOp C).inverse = CategoryTheory.Comon.MonOpOpToComon C
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.exists_iterate_derivative_eq_factorial_smul : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (k : ℕ),
  ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ (⇑Polynomial.derivative)^[k] p = k.factorial • gp
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- Rotate a loop walk such that it is centered at the given vertex.  -/
SimpleGraph.Walk.rotate : {V : Type u} → {G : SimpleGraph V} → {v : V} → [DecidableEq V] → (c : G.Walk v v) → (u : V) → u ∈ c.support → G.Walk u u
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableSet.of_union_range_cover : ∀ {α : Type u_1} {α₁ : Type u_6} {α₂ : Type u_7} {mα : MeasurableSpace α} {mα₁ : MeasurableSpace α₁}
  {mα₂ : MeasurableSpace α₂} {i₁ : α₁ → α} {i₂ : α₂ → α} {s : Set α},
  MeasurableEmbedding i₁ →
    MeasurableEmbedding i₂ →
      Set.univ ⊆ Set.range i₁ ∪ Set.range i₂ → MeasurableSet (i₁ ⁻¹' s) → MeasurableSet (i₂ ⁻¹' s) → MeasurableSet s
-- Mathlib.Order.WithBot
WithBot.LE.bot_le : ∀ {α : Type u_1} [inst : LE α] (x : WithBot α), ⊥.LE x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.find?_insert_of_ne : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k' k : α} {v : β} [Std.TransCmp cmp]
  (t : RBTree.RBMap α β cmp), cmp k' k ≠ Ordering.eq → (t.insert k v).find? k' = t.find? k'
-- Lean.LocalContext
/-- The type of the variable.  -/
Lean.LocalDecl.type : Lean.LocalDecl → Lean.Expr
-- Mathlib.NumberTheory.ModularForms.DedekindEta
/-- For `‖q‖ < 1`, the infinite product `∏ (1 - q^(n+1))` is multipliable.  -/
ModularForm.multipliable_one_sub_pow : ∀ {q : ℂ}, ‖q‖ < 1 → Multipliable fun n => 1 - q ^ (n + 1)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.symm_mapAddEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Mul M] (e : R ≃+ S),
  (MonoidAlgebra.mapAddEquiv M e).symm = MonoidAlgebra.mapAddEquiv M e.symm
-- Mathlib.Analysis.Complex.Conformal
/-- Construct a complex-linear map from a real-linear map `ℓ` that maps `I` to `I • ℓ 1`.
 -/
LinearMap.complexOfReal : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℂ E] → (ℓ : ℂ →ₗ[ℝ] E) → ℓ Complex.I = Complex.I • ℓ 1 → ℂ →ₗ[ℂ] E
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.const : Lean.Name → ℕ → Lean.Meta.DiscrTree.Key
-- Std.Tactic.Do.Syntax
/-- If `true` (the default), report a hard error when no `@[spec]` theorem matches the
current program head. If `false`, leave such goals as unsolved VCs for the user to
discharge manually. This is the behaviour that `mvcgen` exhibits implicitly;
the new prototypical `vcgen` opts into it via `(errorOnMissingSpec := false)`.
 -/
Lean.Elab.Tactic.Do.VCGen.Config.errorOnMissingSpec : Lean.Elab.Tactic.Do.VCGen.Config → Bool
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_g : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (hfg : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker),
  (CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).g = g
-- Mathlib.Lean.ContextInfo
/-- Embeds a `MetaM` action in `CommandElabM`, returning both the result and InfoTrees produced.  -/
Lean.Elab.ContextInfo.runMetaMCapturingInfoTree : {α : Type} →
  Lean.Elab.ContextInfo →
    Lean.LocalContext → Lean.MetaM α → Lean.Elab.Command.CommandElabM (α × Lean.PersistentArray Lean.Elab.InfoTree)
-- Mathlib.Data.Sum.Interval
Finset.sumLift₂_nonempty : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f : α₁ → β₁ → Finset γ₁} {g : α₂ → β₂ → Finset γ₂} {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂},
  (Finset.sumLift₂ f g a b).Nonempty ↔
    (∃ a₁ b₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ (f a₁ b₁).Nonempty) ∨
      ∃ a₂ b₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ (g a₂ b₂).Nonempty
-- Init.Data.UInt.Lemmas
UInt16.ofNat_one : UInt16.ofNat 1 = 1
-- Mathlib.Data.Real.Embedding
mul_smul_one_lt_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M] {num : ℤ}
  {n den : ℕ}, 0 < n → ∀ {x : M}, (num * ↑n) • 1 < (↑n * ↑den) • x ↔ num • 1 < den • x
-- Mathlib.Algebra.Ring.Action.Submonoid
/-- The additive submonoid of elements fixed under the whole action.  -/
FixedPoints.addSubmonoid : (M : Type u_1) → (α : Type u_2) → [inst : Monoid M] → [inst_1 : AddMonoid α] → [DistribMulAction M α] → AddSubmonoid α
-- Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
/-- **Dominated convergence theorem** for filters with a countable basis.  -/
MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_2} {l : Filter ι}
  [l.IsCountablyGenerated] {F : ι → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal),
  (∀ᶠ (n : ι) in l, Measurable (F n)) →
    (∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) →
      ∫⁻ (a : α), bound a ∂μ ≠ ⊤ →
        (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) l (nhds (f a))) →
          Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) l (nhds (∫⁻ (a : α), f a ∂μ))
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.instMulSemiringActionSemiHomClassCoeMonoidHom : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (φ : M →* N) (R : Type u_10) [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] (S : Type u_12) [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S],
  MulSemiringActionSemiHomClass (R →ₑ+*[φ] S) (⇑φ) R S
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.forM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (f : α → m PUnit.{u_1 + 1}),
  RBTree.RBNode.forM f RBTree.RBNode.nil = pure PUnit.unit
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.isUnit_den : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ), ‖↑r‖ ≤ 1 → IsUnit ↑r.den
-- Mathlib.NumberTheory.ModularForms.LFunction
_private.Mathlib.NumberTheory.ModularForms.LFunction.0.instIsArithmeticHSMulConjActGeneralLinearGroupFinOfNatNatRealSubgroupCoeMulEquivToConjActInvMonoidHomSpecialLinearGroupToGLIntMapCastRingHomS : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic],
  (ConjAct.toConjAct
        (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))⁻¹ •
      Γ).IsArithmetic
-- Mathlib.NumberTheory.NumberField.ExistsRamified
/-- Any number field that is unramified over `ℚ` has rank `1`.  -/
NumberField.finrank_eq_one_of_unramified : ∀ {K : Type u_1} {𝒪 : Type u_2} [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsIntegralClosure 𝒪 ℤ K] [Algebra.Unramified ℤ 𝒪], Module.finrank ℚ K = 1
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.Z_u₃_spec : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.Z✝ S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃✝ S) =
    FermatLastTheoremForThreeGen.Solution.z✝ S
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Evaluation of a `ContinuousAlternatingMap` at a vector as an `AddMonoidHom`.  -/
ContinuousAlternatingMap.applyAddHom : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] → [inst_7 : ContinuousAdd N] → (ι → M) → M [⋀^ι]→L[R] N →+ N
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α], (↑m).WF → (Std.DHashMap.Raw.Const.toArray ↑m).size = (↑m).size
-- Mathlib.Data.Set.Insert
Set.instNonemptyElemInsert : ∀ {α : Type u_1} (a : α) (s : Set α), Nonempty ↑(insert a s)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_mul_isBoundedUnder_ge : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l g →
    Filter.Tendsto (fun x => f x * g x) l Filter.atBot → Filter.Tendsto f l Filter.atBot
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.lt_iff : ∀ {α : Type u_1} [inst : LT α] {a b : DegLex (α →₀ ℕ)},
  a < b ↔
    Finsupp.degree (ofDegLex a) < Finsupp.degree (ofDegLex b) ∨
      Finsupp.degree (ofDegLex a) = Finsupp.degree (ofDegLex b) ∧ toLex (ofDegLex a) < toLex (ofDegLex b)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_eq_false_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = true → t.isEmpty = false
-- Mathlib.Data.Multiset.Basic
/-- The equivalence between lists and multisets of a subsingleton type.  -/
Multiset.subsingletonEquiv : (α : Type u_1) → [Subsingleton α] → List α ≃ Multiset α
-- Mathlib.GroupTheory.IsSubnormal
/-- The inverse image of a subnormal subgroup under a group homomorphism is a subnormal subgroup.  -/
Subgroup.IsSubnormal.comap : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] {H' : Subgroup G'} (f : G →* G'),
  H'.IsSubnormal → (Subgroup.comap f H').IsSubnormal
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
CStarAlgebra.instNonnegSpectrumClass : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A], NonnegSpectrumClass ℝ A
-- Mathlib.RingTheory.Coalgebra.TensorProduct
/-- `lTensor M f : M ⊗ N →ₗc M ⊗ P` is the natural coalgebra morphism induced by `f : N →ₗc P`.  -/
CoalgHom.lTensor : {R : Type u_5} →
  (M : Type u_6) →
    {N : Type u_7} →
      {P : Type u_8} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      [inst_7 : Coalgebra R M] →
                        [inst_8 : Coalgebra R N] →
                          [inst_9 : Coalgebra R P] → (N →ₗc[R] P) → TensorProduct R M N →ₗc[R] TensorProduct R M P
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The category of affine schemes  -/
AlgebraicGeometry.AffineScheme : Type (u_1 + 1)
-- Mathlib.Topology.Category.TopCat.Opens
IsOpenMap.coe_functor_obj : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑X),
  ↑(hf.functor.obj U) = ⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_alter_eq_add_one : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)},
  m.WF → k ∉ m → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size + 1
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.instRepresentablyCoflatOppositeOpOfRepresentablyFlat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F], CategoryTheory.RepresentablyCoflat F.op
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.head_mk : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : List Γ), (Turing.ListBlank.mk l).head = l.headI
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_succ : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin n), Fin.cons x p i.succ = p i
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Algebra.TensorProduct.algEquivIncludeRange_tmul : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] (x : S) (y : T),
  (Algebra.TensorProduct.algEquivIncludeRange R S T) (x ⊗ₜ[R] y) =
    Algebra.TensorProduct.includeLeft.rangeRestrict x ⊗ₜ[R] Algebra.TensorProduct.includeRight.rangeRestrict y
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.locallyQuasiFinite_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.LocallyQuasiFinite f ↔
    ∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).QuasiFinite
-- Init.Data.SInt.Lemmas
Int16.toBitVec_ofBitVec : ∀ (b : BitVec 16), (Int16.ofBitVec b).toBitVec = b
-- Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderComonoid.counit_mem : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  (P : CategoryTheory.MorphismProperty C) {c : C} {inst_2 : CategoryTheory.ComonObj c}
  [self : P.IsStableUnderComonoid c], P CategoryTheory.ComonObj.counit
-- Mathlib.Topology.Algebra.Monoid
Subsemigroup.continuousMul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [ContinuousMul M] (S : Subsemigroup M),
  ContinuousMul ↥S
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.toLatticeHom : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] →
        [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → BoundedLatticeHom α β → LatticeHom α β
-- Mathlib.Data.Set.NAry
Set.image2_inter_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β},
  Function.Injective2 f → Set.image2 f (s ∩ s') t = Set.image2 f s t ∩ Set.image2 f s' t