mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.safeForwardRule.inj : ∀ {r₁ : Aesop.ForwardRule} {r₂ : Aesop.SafeRule} {r₁_1 : Aesop.ForwardRule} {r₂_1 : Aesop.SafeRule},
  Aesop.BaseRuleSetMember.safeForwardRule r₁ r₂ = Aesop.BaseRuleSetMember.safeForwardRule r₁_1 r₂_1 →
    r₁ = r₁_1 ∧ r₂ = r₂_1
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.IterM.step_flatMapAfterM.match_3.splitter : {α₂ γ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Option (Std.IterM m γ) → Sort u_3) →
      (it₂ : Option (Std.IterM m γ)) → (Unit → motive none) → ((it₂ : Std.IterM m γ) → motive (some it₂)) → motive it₂
-- Mathlib.RingTheory.Coalgebra.Basic
/-- The counit satisfies the right counitality law  -/
Coalgebra.lTensor_counit_comp_comul : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  [self : Coalgebra R A],
  LinearMap.lTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul = (TensorProduct.mk R A R).flip 1
-- Mathlib.Topology.EMetricSpace.Defs
Metric.eball_prod_same : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal),
  Metric.eball x r ×ˢ Metric.eball y r = Metric.eball (x, y) r
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
  CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ = γ.φQ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.keyAtIdxD_eq_getD_map_getElem? : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β},
  t.Balanced →
    ∀ {i : ℕ} {fallback : α}, t.keyAtIdxD i fallback = (Option.map (fun x => x.fst) t.toListModel[i]?).getD fallback
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_to_distribMulActionHom : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.whiskerHorizontal_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] {T : CategoryTheory.Functor C₁ D₁} {L : CategoryTheory.Functor C₁ C₂}
  {R : CategoryTheory.Functor D₁ D₂} {B : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T L R B)
  {T' : CategoryTheory.Functor C₁ D₁} {B' : CategoryTheory.Functor C₂ D₂} (α : T' ⟶ T) (β : B ⟶ B') (X : C₁),
  (w.whiskerHorizontal α β).app X =
    CategoryTheory.CategoryStruct.comp (R.map (α.app X))
      (CategoryTheory.CategoryStruct.comp (w.natTrans.app X) (β.app (L.obj X)))
-- Lean.Meta.Tactic.Try.Collect
/-- Relevant declarations by `libSearch`  -/
Lean.Meta.Try.Collector.Result.libSearchResults : Lean.Meta.Try.Collector.Result → Lean.Meta.Try.Collector.OrdSet (Lean.Name × Lean.Meta.Grind.EMatchTheoremKind)
-- Mathlib.Logic.Small.Set
small_setProd : ∀ {α : Type u1} {β : Type u2} (s : Set α) (t : Set β) [Small.{u, u1} ↑s] [Small.{u, u2} ↑t],
  Small.{u, max u1 u2} ↑(s ×ˢ t)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.inter₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} {h₁ : 0 < m₁.buckets.size}
  {h₂ : 0 < m₂.buckets.size} (a : m₁.WF) (a_1 : m₂.WF),
  Std.DHashMap.Raw.WF.below a →
    motive m₁ a → Std.DHashMap.Raw.WF.below a_1 → motive m₂ a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonLogConfig.fromJson : Lean.Json → Except String Lean.Lsp.LogConfig
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mkIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f : C ≌ D} (η : e.functor ≅ f.functor),
  (CategoryTheory.Equivalence.mkIso η).hom = CategoryTheory.Equivalence.mkHom η.hom
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
/-- The projection from the product of localizations at primes to the product of
localizations at maximal ideals.  -/
PrimeSpectrum.piLocalizationToMaximal : (R : Type u_1) → [inst : CommSemiring R] → PrimeSpectrum.PiLocalization R →ₐ[R] MaximalSpectrum.PiLocalization R
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.mk : {α : Type u} →
  {β : α → Type v} →
    {_cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw._auto_1} →
      Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Raw α β _cmp
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.ker_fst : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'], (MonoidHom.fst G G').ker = ⊥.prod ⊤
-- Init.Data.Float.Model.Float32
Float32.Model.instNeg : Neg Float32.Model
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.rnDeriv_mconv : ∀ {G : Type u_3} [inst : Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [MeasureTheory.SFinite μ] {ν₁ ν₂ : MeasureTheory.Measure G}
  [MeasureTheory.IsFiniteMeasure ν₁] [MeasureTheory.IsFiniteMeasure ν₂] [ν₁.HaveLebesgueDecomposition μ]
  [ν₂.HaveLebesgueDecomposition μ],
  ν₁.AbsolutelyContinuous μ →
    ν₂.AbsolutelyContinuous μ →
      (ν₁.mconv ν₂).rnDeriv μ =ᵐ[μ] MeasureTheory.mlconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ
-- Init.Data.Slice.Array.Lemmas
Array.stop_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (Std.Rco.Sliceable.mkSlice xs lo...hi).stop = min hi xs.size
-- Std.Data.HashMap.Lemmas
/-- Variant of `getElem?_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.HashMap.getElem?_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α},
  (Std.HashMap.map f m)[k]? = Option.pmap (fun v h' => f (m.getKey k h') v) m[k]? ⋯
-- Mathlib.Util.AtLocation
Mathlib.Tactic.BehaviorIfUnchanged.error.sizeOf_spec : sizeOf Mathlib.Tactic.BehaviorIfUnchanged.error = 1
-- Mathlib.Analysis.SpecialFunctions.Sqrt
ContDiffWithinAt.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞} {s : Set E}
  {x : E}, ContDiffWithinAt ℝ n f s x → f x ≠ 0 → ContDiffWithinAt ℝ n (fun y => √(f y)) s x
-- Mathlib.Logic.Basic
Ne.dite_ne_left_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a : α} {B : ¬P → α},
  (∀ (h : ¬P), a ≠ B h) → (dite P (fun x => a) B ≠ a ↔ ¬P)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₂_of_isCharTwoJEqZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF], W.b₂ = 0
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc_map_le_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X),
  (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ).map (CategoryTheory.homOfLE ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ j ⋯).hom
      (CategoryTheory.CategoryStruct.comp τ (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjSuccIso hj F τ).inv)
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- A choice of chart on the co-domain `N` of a local property of `f` at `x`:
w.r.t. this chart and `h.domChart`, `f` has the local property `P` at `x`
The particular chart is arbitrary, but this choice matches the witness given by `h.domChart`.  -/
Manifold.LiftSourceTargetPropertyAt.codChart : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_4} →
      {H : Type u_6} →
        {G : Type u_8} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 F G} →
                            {M : Type u_10} →
                              {N : Type u_12} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              {P :
                                                  (M → N) →
                                                    OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} →
                                                Manifold.LiftSourceTargetPropertyAt I J n f x P →
                                                  OpenPartialHomeomorph N G
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.AlmostMono.mk.inj : ∀ {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ι → Option α) → κ} {line : Combinatorics.Line (Option α) ι}
  {color : κ} {has_color : ∀ (x : α), C (↑line (some x)) = color} {line_1 : Combinatorics.Line (Option α) ι}
  {color_1 : κ} {has_color_1 : ∀ (x : α), C (↑line_1 (some x)) = color_1},
  { line := line, color := color, has_color := has_color } =
      { line := line_1, color := color_1, has_color := has_color_1 } →
    line = line_1 ∧ color = color_1
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- A sequential limit of measurable `ℝ≥0`-valued functions is measurable.  -/
NNReal.measurable_of_tendsto : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : ℕ → α → NNReal} {g : α → NNReal},
  (∀ (i : ℕ), Measurable (f i)) → Filter.Tendsto f Filter.atTop (nhds g) → Measurable g
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- The morphisms between the `obj` fields of descent data.  -/
CategoryTheory.Pseudofunctor.DescentData'.Hom.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} →
                  {D₁ D₂ : F.DescentData' sq sq₃} → D₁.Hom D₂ → (i : ι) → D₁.obj i ⟶ D₂.obj i
-- Mathlib.Tactic.Check
/-- Delaborates `type` as ` binders* : returnType`. Note the leading space; this means that we
ought to put `{.ofConstName c}` directly before it. Note: this strategy gives us hover
information on `c`, allowing the user to inspect the full type signature if they wish.  -/
_private.Mathlib.Tactic.Check.0.Mathlib.Tactic.checkCoreAux.delabSignatureWithoutImplicit : Lean.Expr → Lean.MessageData
-- Mathlib.Topology.MetricSpace.Congruence
Congruent.refl : ∀ {ι : Type u_1} {P₁ : Type u_3} [inst : PseudoEMetricSpace P₁] (v₁ : ι → P₁), Congruent v₁ v₁
-- ProofWidgets.Data.Html
ProofWidgets.Html.text.sizeOf_spec : ∀ (a : String), sizeOf (ProofWidgets.Html.text a) = 1 + sizeOf a
-- Mathlib.Analysis.RCLike.Basic
RCLike.pos_iff_exists_ofReal : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, 0 < z ↔ ∃ x > 0, ↑x = z
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  (X₁ X₂ : CategoryTheory.Arrow C),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding X₁ X₂).hom.right = (β_ X₁.right X₂.right).hom
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.measure_closedBall_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ}, μ (Metric.closedBall x r) < ⊤
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toAlgHom_eq_coe : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ↑e = ↑e
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- Note: This does not hold for `n = ∞`. `f` being `C^∞` at `x` means that for every `n`, `f` is
`C^n` on some neighborhood of `x`, but this neighborhood can depend on `n`.  -/
contMDiffAt_iff_contMDiffAt_nhds : ∀ {𝕜 : 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 : M → M'} {x : M} {n : WithTop ℕ∞}
  [IsManifold I n M] [IsManifold I' n M'],
  n ≠ ↑⊤ → (ContMDiffAt I I' n f x ↔ ∀ᶠ (x' : M) in nhds x, ContMDiffAt I I' n f x')
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.colimitCoconeOfUnique_cocone_pt : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C),
  (CategoryTheory.Limits.colimitCoconeOfUnique f).cocone.pt = f default
-- Lean.Server.References
Lean.Server.LoadedILean.mk.injEq : ∀ (moduleUri : Lean.Lsp.DocumentUri) (ileanPath : System.FilePath) (directImports : Lean.Server.DirectImports)
  (refs : Lean.Lsp.ModuleRefs) (decls : Lean.Lsp.Decls) (moduleUri_1 : Lean.Lsp.DocumentUri)
  (ileanPath_1 : System.FilePath) (directImports_1 : Lean.Server.DirectImports) (refs_1 : Lean.Lsp.ModuleRefs)
  (decls_1 : Lean.Lsp.Decls),
  ({ moduleUri := moduleUri, ileanPath := ileanPath, directImports := directImports, refs := refs, decls := decls } =
      { moduleUri := moduleUri_1, ileanPath := ileanPath_1, directImports := directImports_1, refs := refs_1,
        decls := decls_1 }) =
    (moduleUri = moduleUri_1 ∧
      ileanPath = ileanPath_1 ∧ directImports = directImports_1 ∧ refs = refs_1 ∧ decls = decls_1)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Isδ₀.iff : ∀ {j : ℕ} {i : Fin (j + 2)}, AlgebraicTopology.DoldKan.Isδ₀ (SimplexCategory.δ i) ↔ i = 0
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
mem_perfectClosure_iff : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ perfectClosure F E ↔ ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range
-- Mathlib.Order.LatticeIntervals
Set.Ici.coe_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] (a : α), ↑⊤ = ⊤
-- Init.Data.SInt.Bitwise
Int8.shiftRight_zero : ∀ {a : Int8}, a >>> 0 = a
-- Aesop.Search.Expansion.Norm
Aesop.runNormRule : Lean.MVarId →
  Aesop.UnorderedArraySet Lean.MVarId →
    Aesop.IndexMatchResult Aesop.NormRule → Aesop.NormM (Option Aesop.NormRuleResult)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.forIn_eq_forIn_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} {α_1 : Type u_1} {init : α_1}
  {f : α × β → α_1 → m (ForInStep α_1)} [inst : Monad m] [LawfulMonad m] {t : RBTree.RBMap α β cmp},
  forIn t init f = forIn t.toList init f
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.CreatesFiniteLimits.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          autoParam
              ((J : Type) →
                [inst_2 : CategoryTheory.SmallCategory J] →
                  [CategoryTheory.FinCategory J] → CategoryTheory.CreatesLimitsOfShape J F)
              CategoryTheory.Limits.CreatesFiniteLimits.createsFiniteLimits._autoParam →
            CategoryTheory.Limits.CreatesFiniteLimits F
-- Lean.Meta.CtorRecognizer
/-- Returns `true`, if `e` is constructor application of builtin literal defeq to
a constructor application.
 -/
Lean.Meta.isConstructorApp : Lean.Expr → Lean.MetaM Bool
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.hom_ext : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : StandardEtalePair R} {f g : P.Ring →ₐ[R] S}, f P.X = g P.X → f = g
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.category_comp_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X Y Z : CategoryTheory.Limits.Cone F} (f : CategoryTheory.Limits.ConeMorphism X Y)
  (g : CategoryTheory.Limits.ConeMorphism Y Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Algebra.Order.Star.Conjneg
conjneg_nonneg : ∀ {G : Type u_1} {R : Type u_2} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : PartialOrder R]
  [inst_3 : StarRing R] [StarOrderedRing R] {f : G → R}, 0 ≤ conjneg f ↔ 0 ≤ f
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.finsetSum'`. -/
MeasureTheory.IsStronglyProgressive.finset_sum' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : AddCommMonoid β]
  [ContinuousAdd β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) → MeasureTheory.IsStronglyProgressive f (∑ c ∈ s, U c)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.isTrivial : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Bool
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.root_push : ∀ {x : ℕ} {self : Batteries.UnionFind}, self.push.rootD x = self.rootD x
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.zeroAdd.sizeOf_spec : sizeOf FirstOrder.Field.FieldAxiom.zeroAdd = 1
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The underlying element of `v.1.Completion`.  -/
NumberField.InfinitePlace.Completion.toCompletion : {K : Type u_1} → [inst : Field K] → {v : NumberField.InfinitePlace K} → v.Completion → (↑v).Completion
-- Mathlib.Combinatorics.Schnirelmann
/-- **Alias** of `schnirelmannDensity_sdiff_singleton_zero`.

---

The Schnirelmann density is unaffected by removing `0`.  -/
schnirelmannDensity_diff_singleton_zero : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] [inst_1 : DecidablePred fun x => x ∈ A \ {0}],
  schnirelmannDensity (A \ {0}) = schnirelmannDensity A
-- Init.Data.Array.Lemmas
Array.all_eq_true_iff_forall_mem : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, xs.all p = true ↔ ∀ x ∈ xs, p x = true
-- Mathlib.Tactic.Positivity.Core
/-- A variation on `assumption` when the hypothesis is `lo < e` where `lo` is a numeral.  -/
Mathlib.Meta.Positivity.compareHypLT : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      (pα : Q(PartialOrder «$α»)) →
        (lo e : Q(«$α»)) → Q(«$lo» < «$e») → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e (some pα))
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instValuationRingSubtypeMem : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), ValuationRing ↥A
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_roc_eq_add : ∀ {m n i fallback : ℕ}, i < n - m → (m<...=n).toList.getD i fallback = m + 1 + i
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioc_uIcc_uIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α},
  Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.uIcc a b)) (Filter.principal (Set.uIcc a b))
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_eq_zero_iff : ∀ {x : NNReal} {y : ℝ}, x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
-- Mathlib.Analysis.Real.Pi.Wallis
Real.Wallis.W_eq_integral_sin_pow_div_integral_sin_pow : ∀ (k : ℕ),
  (Real.pi / 2)⁻¹ * Real.Wallis.W k =
    (∫ (x : ℝ) in 0..Real.pi, Real.sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..Real.pi, Real.sin x ^ (2 * k)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k} {h₁ : a ∈ t.insertIfNew k v},
  (t.insertIfNew k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey a ⋯
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'.loop.match_5.splitter : {α : Type u_1} →
  {β : Type u_3} →
    (as : List α) →
      (motive : (x : List α) → β → (∃ bs, bs ++ x = as) → Sort u_2) →
        (x : List α) →
          (x_1 : β) →
            (x_2 : ∃ bs, bs ++ x = as) →
              ((b : β) → (x : ∃ bs, bs ++ [] = as) → motive [] b x) →
                ((a : α) → (as' : List α) → (b : β) → (h : ∃ bs, bs ++ a :: as' = as) → motive (a :: as') b h) →
                  motive x x_1 x_2
-- Init.Data.Bool
/-- Boolean “exclusive or”. `xor x y` can be written `x ^^ y`.

`x ^^ y` is `true` when precisely one of `x` or `y` is `true`. Unlike `and` and `or`, it does not
have short-circuiting behavior, because one argument's value never determines the final value. Also
unlike `and` and `or`, there is no commonly-used corresponding propositional connective.

Examples:
 * `false ^^ false = false`
 * `true ^^ false = true`
 * `false ^^ true = true`
 * `true ^^ true = false`


Conventions for notations in identifiers:

 * The recommended spelling of `^^` in identifiers is `xor`. -/
Bool.xor : Bool → Bool → Bool
-- Mathlib.Combinatorics.Matroid.Map
/-- Given `M : Matroid α` and `X : Set α`, the restriction of `M` to `X`,
viewed as a matroid on type `X` with ground set `univ`.
Always isomorphic to `M ↾ X`. If `X = M.E`, then isomorphic to `M`.  -/
Matroid.restrictSubtype : {α : Type u_1} → Matroid α → (X : Set α) → Matroid ↑X
-- Mathlib.CategoryTheory.Limits.Creates
/-- Any cone lifts through the identity functor.  -/
CategoryTheory.idLiftsCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {K : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Functor.id C))) →
            CategoryTheory.LiftableCone K (CategoryTheory.Functor.id C) c
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The difference of `v` from its orthogonal projection onto `K` is in `Kᗮ`.  -/
Submodule.sub_starProjection_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (v : E), v - K.starProjection v ∈ Kᗮ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.ExtDHashMap.Const.ofList l).getKey? k' = some k