mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.AlgebraicClosure
/-- **Alias** of `algebraicClosure.algEquivOfAlgEquiv`.

---

If `E` and `K` are isomorphic as `F`-algebras, then `algebraicClosure F E` and
`algebraicClosure F K` are also isomorphic as `F`-algebras.  -/
AlgEquiv.algebraicClosure : {F : Type u_1} →
  {E : Type u_2} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {K : Type u_3} →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] → (E ≃ₐ[F] K) → ↥(algebraicClosure F E) ≃ₐ[F] ↥(algebraicClosure F K)
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.div : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f g : α → G}
  [MeasurableDiv₂ G], Measurable f → Measurable g → Measurable (f / g)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.ι_forgetStalk_hom_assoc : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ) {Z : Type u}
  (h : (smoothSheaf IM I M R).presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (TypeCat.ofHom
        ⇑(CommRingCat.Hom.hom
            (CategoryTheory.Limits.colimit.ι
              ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)))
      (CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf)
        U)
      h
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_tprod_le_of_forall_le_of_nonneg : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] {f : ι → M} {C : ℝ},
  0 ≤ C → (∀ (i : ι), ‖f i‖ ≤ C) → ‖∏' (i : ι), f i‖ ≤ C
-- Mathlib.Data.Pi.Interval
Pi.card_Ioi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [inst_4 : (i : ι) → LocallyFiniteOrderTop (α i)] (a : (i : ι) → α i),
  (Finset.Ioi a).card = ∏ i, (Finset.Ici (a i)).card - 1
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.le_log_one_add_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → 2 * x / (x + 2) ≤ Real.log (1 + x)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.add_le_sum : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι}
  [AddLeftMono N] {i j : ι}, (∀ i ∈ s, 0 ≤ f i) → i ∈ s → j ∈ s → i ≠ j → f i + f j ≤ ∑ k ∈ s, f k
-- Mathlib.Data.Finite.Defs
Prop.instFinite : Finite Prop
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.normal.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {a a_1 : Λ},
  Turing.TM2to1.Λ'.normal a = Turing.TM2to1.Λ'.normal a_1 → a = a_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffineLift_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.NonsingularLift ⟦P⟧),
  { point := ⟦P⟧, nonsingular := hP }.toAffineLift = WeierstrassCurve.Jacobian.Point.toAffine W P
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_cons' : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : AddCommMonoid M] (h : a ∉ s),
  (Finset.cons a s h).sum = fun f => f a + ∑ x ∈ s, f x
-- Mathlib.Topology.Algebra.UniformConvergence
instAddUniformFun : {α : Type u_1} → {β : Type u_2} → [Add β] → Add (UniformFun α β)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeMapCocone_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₅, u₅} E] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D}
  {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Functor.mapCoconeMapCocone c).inv.hom = CategoryTheory.CategoryStruct.id (H'.obj (H.obj c.pt))
-- Mathlib.Analysis.Complex.Circle
Real.fourierChar_ne_one : Real.fourierChar ≠ 1
-- Mathlib.Algebra.Group.Even
IsSquare.sq : ∀ {α : Type u_2} [inst : Monoid α] (r : α), IsSquare (r ^ 2)
-- Mathlib.Topology.Maps.Basic
/-- A map is open if and only if the `Set.kernImage` of every *closed* set is closed.  -/
isOpenMap_iff_closure_kernImage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f ↔ ∀ {s : Set X}, closure (Set.kernImage f s) ⊆ Set.kernImage f (closure s)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceShiftRight : Lean.Meta.Simp.DSimproc
-- Init.Data.UInt.Lemmas
USize.zero_def : 0 = { toBitVec := 0 }
-- Mathlib.Algebra.Category.MonCat.Shrink
instSmallCompMonCatForgetMonoidHomCarrierOfSmallObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C MonCat)
  [∀ (X : C), Small.{w, w'} ↑(F.obj X)],
  CategoryTheory.FunctorToTypes.Small.{w, w', v, u} (F.comp (CategoryTheory.forget MonCat))
-- Mathlib.Algebra.Star.StarAlgHom
/-- A *⋆-algebra homomorphism* is an algebra homomorphism between `R`-algebras `A` and `B`
equipped with a `star` operation, and this homomorphism is also `star`-preserving.  -/
«term_→⋆ₐ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Tactic.Tauto
/-- Debug `grind` by identifying places where it does not yet supersede `tauto`.  -/
linter.tacticAnalysis.regressions.tautoToGrind : Lean.Option Bool
-- Mathlib.Order.Filter.Lift
Filter.lift'_le : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Set β} {h : Filter β} {s : Set α},
  s ∈ f → Filter.principal (g s) ≤ h → f.lift' g ≤ h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.get_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {hk : k ∈ t₁} (h : t₁.Equiv t₂), t₁.get k hk = t₂.get k ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?!.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α fun x => β) (k : α) (v : β),
  Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?! t k v =
    match Std.DTreeMap.Internal.Impl.Const.get? t k with
    | none => (none, Std.DTreeMap.Internal.Impl.insertIfNew! k v t)
    | some b => (some b, t)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.getKey! t.maxKey! = t.maxKey!
-- Mathlib.Data.Matrix.Diagonal
Matrix.row_diagonal : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (d : n → α) (j : n),
  (Matrix.diagonal d).row j = Pi.single j (d j)
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.List.ProveNilOrConsResult.cons.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(List «$α»)} (a : Q(«$α»)) (s' : Q(List «$α»)) (pf : Q(«$s» = «$a» :: «$s'»)),
  sizeOf (Mathlib.Meta.List.ProveNilOrConsResult.cons a s' pf) = 1 + sizeOf a + sizeOf s' + sizeOf pf
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_const_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (α : ℝ),
  ProbabilityTheory.mgf (fun ω => α * X ω) μ t = ProbabilityTheory.mgf X μ (α * t)
-- Mathlib.Algebra.Star.Subalgebra
/-- The pointwise `star` of a subalgebra is a subalgebra.  -/
Subalgebra.involutiveStar : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] → [inst_4 : StarRing A] → [StarModule R A] → InvolutiveStar (Subalgebra R A)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.IsMultiplicative],
  W.op.IsMultiplicative
-- Init.Data.SInt.Basic
/-- Converts 64-bit signed integers to word-sized signed integers, truncating the bitvector
representation on 32-bit platforms. This conversion is lossless on 64-bit platforms.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.toISize : Int64 → ISize
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.natDegree_map_lt : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial R},
  f p.leadingCoeff = 0 → Polynomial.map f p ≠ 0 → (Polynomial.map f p).natDegree < p.natDegree
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vlt_imp_vlt_of_vle_of_vle : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x x' y y' : R}, x ≤ᵥ x' → y' ≤ᵥ y → x' <ᵥ y' → x <ᵥ y
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.natAbs_pow_inertiaDeg`. -/
Ideal.natAbs_pow_inertiaDeg' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R] [Module.Finite ℤ R]
  (p : ℤ) (P : Ideal R) [P.IsPrime] [P.LiesOver (Ideal.span {p})], p.natAbs ^ P.inertiaDeg ℤ = Ideal.absNorm P
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_unitIso_hom_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (X_1 : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.equivComma.unitIso.hom.app X).app X_1 =
    (match X_1 with
      | CategoryTheory.WithTerminal.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp X)).app x
      | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithTerminal.star)).hom
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_map_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f g : Polynomial R) (m n : ℕ) (φ : R →+* S),
  (Polynomial.map φ f).resultant (Polynomial.map φ g) m n = φ (f.resultant g m n)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.GrpObj G],
  CategoryTheory.GrpObj.ofRepresentableBy G (CategoryTheory.yonedaGrpObj G)
      (CategoryTheory.yonedaGrpObjRepresentableBy G) =
    inst_2
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.forget_map₂ : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {a b : CategoryTheory.Bicategory.InducedBicategory C F} {f g : a ⟶ b} (a_1 : f ⟶ g),
  CategoryTheory.Bicategory.InducedBicategory.forget.map₂ a_1 = a_1.hom
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The underlying morphism of objects in `Comma L R`.  -/
CategoryTheory.MorphismProperty.Comma.Hom.hom : {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} →
                      {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} → X.Hom Y → (X.toComma ⟶ Y.toComma)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase0 : Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.Algebra.Homology.HomologySequence
/-- The morphism `K.opcycles i ⟶ K.cycles j` that is induced by `K.d i j`.  -/
HomologicalComplex.opcyclesToCycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j : ι) → [inst_2 : K.HasHomology i] → [inst_3 : K.HasHomology j] → K.opcycles i ⟶ K.cycles j
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.coprodPresheafObjIso.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (U : (X ⨿ Y).Opens),
  AlgebraicGeometry.Scheme.coprodPresheafObjIso U =
    CategoryTheory.Functor.mapIso (X ⨿ Y).presheaf (CategoryTheory.eqToIso ⋯).op ≪≫
      ((X ⨿ Y).sheaf.isProductOfDisjoint
              ((AlgebraicGeometry.Scheme.Hom.opensFunctor CategoryTheory.Limits.coprod.inl).obj
                ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inl.base).obj U))
              ((AlgebraicGeometry.Scheme.Hom.opensFunctor CategoryTheory.Limits.coprod.inr).obj
                ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inr.base).obj U))
              ⋯).conePointUniqueUpToIso
          (CategoryTheory.Limits.limit.isLimit
            (CategoryTheory.Limits.pair
              ((X ⨿ Y).sheaf.obj.obj
                (Opposite.op
                  ((AlgebraicGeometry.Scheme.Hom.opensFunctor CategoryTheory.Limits.coprod.inl).obj
                    ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inl.base).obj U))))
              ((X ⨿ Y).sheaf.obj.obj
                (Opposite.op
                  ((AlgebraicGeometry.Scheme.Hom.opensFunctor CategoryTheory.Limits.coprod.inr).obj
                    ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inr.base).obj U)))))) ≪≫
        CategoryTheory.Limits.prod.mapIso
          (AlgebraicGeometry.Scheme.Hom.appIso CategoryTheory.Limits.coprod.inl
            ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inl.base).obj U))
          (AlgebraicGeometry.Scheme.Hom.appIso CategoryTheory.Limits.coprod.inr
            ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inr.base).obj U))
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.add_neg_cancel_left : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) (b : α), ↑a + (↑(-a) + b) = b
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.Key.lt : Lean.Meta.DiscrTree.Key → Lean.Meta.DiscrTree.Key → Bool
-- Mathlib.Algebra.BigOperators.Finprod
finprod_ne_zero : ∀ {α : Type u_1} {M₀ : Type u_7} [inst : CommMonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] {f : α → M₀},
  (∀ (i : α), f i ≠ 0) → ∏ᶠ (i : α), f i ≠ 0
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.IsOrtho.zero_right : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {Q : QuadraticMap R M N} (x : M), Q.IsOrtho x 0
-- Mathlib.GroupTheory.Congruence.Defs
/-- The multiplication induced on the quotient by a congruence relation on a type with a
multiplication.  -/
Con.hasMul : {M : Type u_1} → [inst : Mul M] → (c : Con M) → Mul c.Quotient
-- Std.Data.HashSet.Raw
/-- Checks if given key is contained and returns the key if it is, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.HashSet.Raw.get! : {α : Type u} → [BEq α] → [Hashable α] → [Inhabited α] → Std.HashSet.Raw α → α → α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (t.alter k f).size =
        if k ∈ t ∧ (f t[k]?).isNone = true then t.size - 1
        else if k ∉ t ∧ (f t[k]?).isSome = true then t.size + 1 else t.size
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.postcomp_uniq_symm : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation),
  solution'.postcomp ↑(h.uniq h').symm = solution
-- Mathlib.Analysis.Normed.Operator.Completeness
ContinuousLinearMap.ofMemClosureImageCoeBounded_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6}
  [inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂] (f : E' → F)
  {s : Set (E' →SL[σ₁₂] F)} (hs : Bornology.IsBounded s) (hf : f ∈ closure (DFunLike.coe '' s)),
  ⇑(ContinuousLinearMap.ofMemClosureImageCoeBounded f hs hf) = f
-- Mathlib.Order.Interval.Finset.Defs
Set.toFinset_Ico : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α) [inst_2 : Fintype ↑(Set.Ico a b)],
  (Set.Ico a b).toFinset = Finset.Ico a b
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Given a signed measure `s` and a negative measurable set `i`, `toMeasureOfLEZero`
provides the measure, mapping measurable sets `j` to `-s (i ∩ j)`.  -/
MeasureTheory.SignedMeasure.toMeasureOfLEZero : {α : Type u_1} →
  {m : MeasurableSpace α} →
    (s : MeasureTheory.SignedMeasure α) →
      (i : Set α) →
        MeasurableSet i →
          MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i → MeasureTheory.Measure α
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.Const.unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α}, (Std.DHashMap.Raw.Const.unitOfList l).WF
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_mul : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [inst : ProbabilityTheory.IsSFiniteKernel κ] {f : α → β → NNReal} {g : α → β → ENNReal},
  Measurable (Function.uncurry f) →
    Measurable (Function.uncurry g) →
      (κ.withDensity fun a x => ↑(f a x) * g a x) = (κ.withDensity fun a x => ↑(f a x)).withDensity g
-- Mathlib.Analysis.Normed.Group.Basic
enorm_pos' : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ENormedMonoid E] {a : E}, 0 < ‖a‖ₑ ↔ a ≠ 1
-- Mathlib.RingTheory.Localization.AtPrime.Basic
_private.Mathlib.RingTheory.Localization.AtPrime.Basic.0.IsLocalization.AtPrime.termPS : Lean.ParserDescr
-- Init.Data.Iterators.Consumers.Monadic.Collect
/-- Traverses the given iterator and stores the emitted values in an array.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.toArray`.
 -/
Std.IterM.Total.toArray : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [Monad m] → [inst : Std.Iterator α m β] → [Std.Iterators.Finite α m] → Std.IterM.Total m β → m (Array β)
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.mergeSort.eq_1 : ∀ {α : Type u_1} (x : α → α → Bool), [].mergeSort x = []
-- Init.Data.List.MinMaxOn
List.minOn.congr_simp : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] {inst_1 : DecidableLE β} [inst_2 : DecidableLE β] (f f_1 : α → β),
  f = f_1 → ∀ (l l_1 : List α) (e_l : l = l_1) (h : l ≠ []), List.minOn f l h = List.minOn f_1 l_1 ⋯
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.adjoint_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E], ContinuousLinearMap.adjoint 1 = 1
-- Mathlib.Order.Filter.IsBounded
/-- For nontrivial filters in linear orders, coboundedness for `≥` implies frequent boundedness
from above.  -/
Filter.IsCobounded.frequently_le : ∀ {α : Type u_1} {f : Filter α} [inst : LinearOrder α] [f.NeBot],
  Filter.IsCobounded (fun x1 x2 => x2 ≤ x1) f → ∃ l, ∃ᶠ (x : α) in f, x ≤ l
-- Mathlib.Algebra.Group.Defs
zpow_zero : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G), a ^ 0 = 1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k : α} {fallback : β k}, m₂.contains k = false → (m₁.union m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  (∀ x ∈ s, f₁ x = f x) → f₁ x = f x → mfderiv[s] f₁ x = mfderiv[s] f x
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.mapM'_eq_mapM.go : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β} (l : List α)
  (acc : List β),
  List.mapM.loop f l acc = do
    let __do_lift ← List.mapM' f l
    pure (acc.reverse ++ __do_lift)
-- Mathlib.CategoryTheory.LiftingProperties.Limits
CategoryTheory.IsPushout.hasLiftingProperty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z W : C} {f : X ⟶ Y} {s : X ⟶ Z} {g : Z ⟶ W}
  {t : Y ⟶ W},
  CategoryTheory.IsPushout s f g t →
    ∀ {Z' W' : C} (g' : Z' ⟶ W') [CategoryTheory.HasLiftingProperty f g'], CategoryTheory.HasLiftingProperty g g'
-- Mathlib.Data.List.Cycle
Cycle.mem_reverse_iff : ∀ {α : Type u_1} {a : α} {s : Cycle α}, a ∈ s.reverse ↔ a ∈ s
-- Mathlib.Algebra.Algebra.Subalgebra.Operations
Subalgebra.mem_of_span_eq_top_of_smul_pow_mem : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (S' : Subalgebra R S) (s : Set S) (l : ↑s →₀ S),
  (Finsupp.linearCombination S Subtype.val) l = 1 →
    s ⊆ ↑S' → (∀ (i : ↑s), l i ∈ S') → ∀ (x : S), (∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ S') → x ∈ S'
-- Mathlib.CategoryTheory.Limits.Cones
/-- There is a morphism from a cocone to its extension.  -/
CategoryTheory.Limits.Cocone.extendHom : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cocone F) → {X : C} → (f : s.pt ⟶ X) → s ⟶ s.extend f
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.map_mk' : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
  (L R : Turing.ListBlank Γ),
  Turing.Tape.map f (Turing.Tape.mk' L R) = Turing.Tape.mk' (Turing.ListBlank.map f L) (Turing.ListBlank.map f R)
-- Mathlib.Analysis.Complex.Harmonic.MeanValue
/-- The Mean Value Property of harmonic functions: If f : ℂ → F is harmonic on a disc of radius
|R| and center c and continuous on its closure, then the circle average circleAverage f c R
equals f c.
 -/
InnerProductSpace.HarmonicContOnCl.circleAverage_eq : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [CompleteSpace F] {f : ℂ → F} {c : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicContOnCl f (Metric.ball c |R|) → Real.circleAverage f c R = f c