mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- If every element belongs to at most `n` Finsets, then the sum of their sizes is at most `n`
times how many they are.  -/
Finset.sum_card_inter_le : ∀ {α : Type u_2} [inst : DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ},
  (∀ a ∈ s, {b ∈ B | a ∈ b}.card ≤ n) → ∑ t ∈ B, (s ∩ t).card ≤ s.card * n
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_id : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X}
  {inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀} [self : 𝒰.LocallyDirected] (i : 𝒰.I₀),
  AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans (CategoryTheory.CategoryStruct.id i) =
    CategoryTheory.CategoryStruct.id (𝒰.X i)
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.essSurj_of_iso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.EssSurj] (α : F ≅ G), G.EssSurj
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- The real logarithm is continuous as a function from nonzero reals.  -/
Real.continuous_log : Continuous fun x => Real.log ↑x
-- Mathlib.Analysis.Normed.Affine.MazurUlam
/-- If an isometric self-homeomorphism of a normed vector space over `ℝ` fixes `x` and `y`,
then it fixes the midpoint of `[x, y]`. This is a lemma for a more general Mazur-Ulam theorem,
see below.  -/
IsometryEquiv.midpoint_fixed : ∀ {E : Type u_1} {PE : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MetricSpace PE]
  [inst_3 : NormedAddTorsor E PE] {x y : PE} (e : PE ≃ᵢ PE), e x = x → e y = y → e (midpoint ℝ x y) = midpoint ℝ x y
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.neg : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CommRingCat} → CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.addUnit.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a),
  h.addUnit = (Classical.choose h).copy a ⋯ ↑(-Classical.choose h) ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
/-- The homology of a simplicial set in degree `0` with coefficients
in `R` identifies to a coproduct of copies of `R` indexed by `π₀ X`.  -/
SSet.homology₀Iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (X : SSet) → (R : C) → [inst_3 : CategoryTheory.CategoryWithHomology C] → X.homology R 0 ≅ ∐ fun x => R
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a finite set `s`, the sum of `f i + g i` over `i ∈ s` equals the sum of `f i`
over `i ∈ s` plus the sum of `g i` over `i ∈ s`.  -/
finsum_mem_add_distrib : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f g : α → M} {s : Set α},
  s.Finite → ∑ᶠ (i : α) (_ : i ∈ s), (f i + g i) = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ s), g i
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_hom : ∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] (s : Multiset M) {F : Type u_8}
  [inst_2 : FunLike F M N] [MonoidHomClass F M N] (f : F), (Multiset.map (⇑f) s).prod = f s.prod
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- If `Fₙ` tends locally uniformly to `f` on a set `s`, and `gₙ` tends to `x` within `s`, then
`Fₙ gₙ` tends to `f x` if `f` is continuous at `x` within `s` and `x ∈ s`.  -/
TendstoLocallyUniformlyOn.tendsto_comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {x : α} {p : Filter ι} {g : ι → α},
  TendstoLocallyUniformlyOn F f p s →
    ContinuousWithinAt f s x →
      x ∈ s → Filter.Tendsto g p (nhdsWithin x s) → Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instMax : {α : Type u_2} → [inst : TopologicalSpace α] → Max (TopologicalSpace.Clopens α)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.mapPower_powerMap_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V)
  {α β : Type t} [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C]
  [inst_2 : CategoryTheory.Limits.HasProductsOfShape β C] (g : α → β) {Z : CategoryTheory.Limits.FormalCoproduct C}
  (h : V.power α ⟶ Z),
  CategoryTheory.CategoryStruct.comp (U.mapPower g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f α) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f β)
      (CategoryTheory.CategoryStruct.comp (V.mapPower g) h)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Overlap.nonzero.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)}
  (x x_1 : Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExProd bt sα) e),
  (Mathlib.Tactic.Ring.Common.Overlap.nonzero x = Mathlib.Tactic.Ring.Common.Overlap.nonzero x_1) = (x = x_1)
-- Mathlib.Logic.Equiv.Set
Equiv.preimage_eq_iff_eq_image : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set β) (t : Set α), ⇑e ⁻¹' s = t ↔ s = ⇑e '' t
-- Aesop.Saturate
_private.Aesop.Saturate.0.Aesop.saturateCore.trySafeRules : Aesop.LocalRuleSet →
  Lean.MVarId → Aesop.UnorderedArraySet Lean.MVarId → Lean.Meta.SavedState → Aesop.SaturateM (Option Aesop.GoalDiff)
-- Std.Internal.Do.Order.Basic
/-- Entailment on a function lattice is pointwise. `β` is recoverable from the operands' types, so
unlike a carrier-only parameter this is a usable `@[grind =]` trigger; it lets `grind` push `⊑`
through a state argument down to the base lattice.  -/
Lean.Order.le_pi_eq_forall : ∀ {σ : Type v} {β : σ → Type w} [inst : (s : σ) → Lean.Order.PartialOrder (β s)] (a b : (s : σ) → β s),
  Lean.Order.PartialOrder.rel a b = ∀ (s : σ), Lean.Order.PartialOrder.rel (a s) (b s)
-- Mathlib.Probability.Moments.Basic
ContinuousLinearEquiv.integral_comp_id_comm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] [inst_9 : MeasurableSpace E]
  {μ : MeasureTheory.Measure E} (L : E ≃L[𝕜] F), ∫ (x : E), L x ∂μ = L (∫ (x : E), x ∂μ)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The kernel of a zero morphism is isomorphic to the source.  -/
CategoryTheory.Limits.kernelZeroIsoSource : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → {X Y : C} → CategoryTheory.Limits.kernel 0 ≅ X
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.coeff_domCongr : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N) (f : MonoidAlgebra A M) (n : N),
  ((MonoidAlgebra.domCongr R A e) f).coeff n = f.coeff (e.symm n)
-- Mathlib.Data.Fin.Tuple.Basic
/-- As a binary function, `Fin.snoc` is injective.  -/
Fin.snoc_injective2 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1}, Function.Injective2 Fin.snoc
-- Mathlib.Order.CompactlyGenerated.Basic
Directed.disjoint_iSup_right : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLattice α] {f : ι → α} [IsCompactlyGenerated α] {a : α},
  Directed (fun x1 x2 => x1 ≤ x2) f → (Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i))
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.norm_ne_one : ∀ (z : Complex.UnitDisc), ‖↑z‖ ≠ 1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.let.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {decl decl_1 : Lean.Compiler.LCNF.LetDecl pu},
  Lean.Compiler.LCNF.CodeDecl.let decl = Lean.Compiler.LCNF.CodeDecl.let decl_1 → decl = decl_1
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasLeftResolutions_of_iso_of_essSurj_of_full : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [L.functor.EssSurj] [R.functor.Full] [R.IsInduced] [W₂'.RespectsIso]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor) [B.HasLeftResolutions], T.HasLeftResolutions
-- Mathlib.CategoryTheory.Monoidal.Discrete
/-- An additive morphism between `AddMonoid`s gives a
monoidal functor between the corresponding discrete monoidal categories.  -/
CategoryTheory.Discrete.addMonoidalFunctor : {M : Type u} →
  [inst : AddMonoid M] →
    {N : Type u'} →
      [inst_1 : AddMonoid N] → (M →+ N) → CategoryTheory.Functor (CategoryTheory.Discrete M) (CategoryTheory.Discrete N)
-- Mathlib.Topology.Coherent
Topology.IsCoherentWith.isClosed_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)} {t : Set X},
  Topology.IsCoherentWith S → (IsClosed t ↔ ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t))
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.selfEquivSigmaOrbitsQuotientStabilizer.eq_1 : ∀ (G : Type u) (X : Type v) [inst : AddGroup G] [inst_1 : AddAction G X],
  AddAction.selfEquivSigmaOrbitsQuotientStabilizer G X = AddAction.selfEquivSigmaOrbitsQuotientStabilizer' G X ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
/-- Joyal's trick: that cofibrations have the left lifting property
with respect to trivial fibrations follows from the left lifting property
of trivial cofibrations with respect to fibrations and a few other
consequences of the model categories axioms.  -/
HomotopicalAlgebra.ModelCategory.hasLiftingProperty_of_joyalTrick : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty]
  [(HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C)]
  [CategoryTheory.Limits.HasPushouts C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition]
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange],
  (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.WeakEquivalence i]
      [HomotopicalAlgebra.Fibration p], CategoryTheory.HasLiftingProperty i p) →
    ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.Fibration p]
      [HomotopicalAlgebra.WeakEquivalence p], CategoryTheory.HasLiftingProperty i p
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- An injective family `v : ι → E` is orthonormal if and only if `Subtype.val : (range v) → E` is
orthonormal.  -/
orthonormal_subtype_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E}, Function.Injective v → (Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.box.sizeOf_spec : ∀ (ty : Lean.IR.IRType) (x : Lean.IR.VarId), sizeOf (Lean.IR.Expr.box ty x) = 1 + sizeOf ty + sizeOf x
-- Mathlib.Algebra.Order.Group.Synonym
isRightRegular_toDual : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, IsRightRegular (OrderDual.toDual a) ↔ IsRightRegular a
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The anti-equivalence between simplicial objects and cosimplicial objects.  -/
CategoryTheory.simplicialCosimplicialEquiv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (CategoryTheory.SimplicialObject C)ᵒᵖ ≌ CategoryTheory.CosimplicialObject Cᵒᵖ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.instIsStableUnderCoproductsInnerAnodyneExtensions : CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{u_1, u_2, u_2 + 1} SSet.innerAnodyneExtensions
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_mul_of_dvd_left : ∀ {a b c : ℤ}, a ∣ b → a ∣ b * c
-- Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
/-- A version of Chebyshev-Markov's inequality using Lp-norms.  -/
MeasureTheory.mul_meas_ge_le_pow_eLpNorm' : ∀ {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [inst : TopologicalSpace ε'] [inst_1 : ContinuousENorm ε']
  {p : ENNReal} (μ : MeasureTheory.Measure α),
  p ≠ 0 →
    p ≠ ⊤ →
      ∀ {f : α → ε'},
        MeasureTheory.AEStronglyMeasurable f μ →
          ∀ (ε : ENNReal), ε ^ p.toReal * μ {x | ε ≤ ‖f x‖ₑ} ≤ MeasureTheory.eLpNorm f p μ ^ p.toReal
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.succ_mono : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  CategoryTheory.Mono (ModuleCat.ofHom (Profinite.NobelingProof.πs C o))
-- Mathlib.MeasureTheory.Integral.Bochner.Set
Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → ℝ} {x : X},
  Continuous f → HasCompactSupport f → 0 ≤ f → f x ≠ 0 → 0 < ∫ (x : X), f x ∂μ
-- Mathlib.Topology.LocallyConstant.Basic
/-- Given a clopen set `U` and a locally constant function `f`,
`LocallyConstant.indicator` returns the locally constant function that is `f` on `U` and `0`
otherwise.  -/
LocallyConstant.indicator : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {R : Type u_5} → [Zero R] → {U : Set X} → LocallyConstant X R → IsClopen U → LocallyConstant X R
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_dvd_fdiv : ∀ {a b c : ℤ}, a ∣ b → b ∣ c → b.fdiv a ∣ c.fdiv a
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of the reverse direction of `ValuativeRel.mul_vlt_mul_iff_left`. -/
ValuativeRel.mul_vlt_mul_left : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ z → x <ᵥ y → x * z <ᵥ y * z
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_smul' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {A : Type u_2} [inst : CommSemiring A] [inst_1 : Algebra A ℝ] (c : A)
  (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.variance (c • X) μ = c ^ 2 • ProbabilityTheory.variance X μ
-- Init.Data.List.MinMax
List.min?_singleton : ∀ {α : Type u_1} [inst : Min α] {x : α}, [x].min? = some x
-- Aesop.RuleTac.GoalDiff
Aesop.isGoalDiffDefeqLDecl : Lean.LocalDecl → Lean.LocalDecl → Lean.MetaM Bool
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiset.disjoint_finsetSum_right : ∀ {ι : Type u_1} {α : Type u_6} {i : Finset ι} {f : ι → Multiset α} {a : Multiset α},
  Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- Equality behind `AddSemiconjBy a x y`; useful for rewriting.  -/
AddSemiconjBy.eq : ∀ {S : Type u_1} [inst : Add S] {a x y : S}, AddSemiconjBy a x y → a + x = y + a
-- Mathlib.Dynamics.Ergodic.Conservative
/-- Poincaré recurrence theorem: if `f` is a conservative dynamical system and `s` is a measurable
set, then for `μ`-a.e. `x`, if the orbit of `x` visits `s` at least once, then it visits `s`
infinitely many times.  -/
MeasureTheory.Conservative.ae_forall_image_mem_imp_frequently_image_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ →
      ∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair.parallelPairHom_left : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y},
  CategoryTheory.Limits.parallelPair.parallelPairHom f g CategoryTheory.Limits.WalkingParallelPairHom.left = f
-- Mathlib.NumberTheory.Dioph
Dioph.DiophList.forall : ∀ {α : Type u} (l : List (Set (α → ℕ))), List.Forall Dioph l → Dioph {v | List.Forall (fun S => v ∈ S) l}
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.linearEquivConj_mulRight : ∀ {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₂] (f : A₁ ≃ₐ[R] A₂) (x : A₁),
  (↑f).conj (LinearMap.mulRight R x) = LinearMap.mulRight R (f x)
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- Component of the integer not multiplied by `√d`  -/
Zsqrtd.re : {d : ℤ} → ℤ√d → ℤ
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- The sup of two orthogonal subspaces equals the subspace orthogonal
to the inf.  -/
ClosedSubmodule.sup_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [CompleteSpace E] (K₁ K₂ : ClosedSubmodule 𝕜 E), K₁ᗮ ⊔ K₂ᗮ = (K₁ ⊓ K₂)ᗮ
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.S.congr_simp : ∀ (l : Type u_4) (R : Type u₂) {inst : DecidableEq l} [inst_1 : DecidableEq l] [inst_2 : CommRing R] (a a_1 : l ⊕ l),
  a = a_1 → ∀ (a_2 a_3 : l ⊕ l), a_2 = a_3 → LieAlgebra.Orthogonal.S l R a a_2 = LieAlgebra.Orthogonal.S l R a_1 a_3
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.of.injEq : ∀ (carrier : Type u) [commRing : CommRing carrier] (carrier_1 : Type u) (commRing_1 : CommRing carrier_1),
  (CommRingCat.of carrier = CommRingCat.of carrier_1) = (carrier = carrier_1 ∧ commRing ≍ commRing_1)
-- Lean.Meta.AbstractNestedProofs
Lean.Meta.AbstractNestedProofs.Context.mk.inj : ∀ {cache cache_1 : Bool}, { cache := cache } = { cache := cache_1 } → cache = cache_1
-- Mathlib.Geometry.Diffeology.Basic
/-- Smooth reparametrisations of plots need to be plots.  -/
DiffeologicalSpace.plot_reparam : ∀ {X : Type u_1} [self : DiffeologicalSpace X] {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X}
  {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
  p ∈ DiffeologicalSpace.plots m → ContDiff ℝ (↑⊤) f → p ∘ f ∈ DiffeologicalSpace.plots n
-- Lean.Linter.UnusedVariables
/-- Interpret an `IgnoreFunction` from the environment.  -/
Lean.Linter.mkIgnoreFn : Lean.Name → Lean.ImportM Lean.Linter.IgnoreFunction
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- The Cartesian product of two continuous multilinear maps, as a continuous multilinear map.  -/
ContinuousMultilinearMap.prod : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        {M₃ : Type w₃} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : (i : ι) → Module R (M₁ i)] →
                    [inst_5 : Module R M₂] →
                      [inst_6 : Module R M₃] →
                        [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] →
                          [inst_8 : TopologicalSpace M₂] →
                            [inst_9 : TopologicalSpace M₃] →
                              ContinuousMultilinearMap R M₁ M₂ →
                                ContinuousMultilinearMap R M₁ M₃ → ContinuousMultilinearMap R M₁ (M₂ × M₃)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.IsCover.externalCoveringNumber_le_encard : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A C : Set X} {ε : NNReal},
  Metric.IsCover ε A C → Metric.externalCoveringNumber ε A ≤ C.encard
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_lt_one_right' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulLeftStrictMono α] (a : α) {b : α}, b < 1 → a * b < a
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticTag.deprecated.sizeOf_spec : sizeOf Lean.Lsp.DiagnosticTag.deprecated = 1
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.pair_eq_singleton : ∀ (x : ZFSet.{u_1}), {x, x} = {x}
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.forIn'_eq_forIn'_toList : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_5 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toList init fun a ha acc => f a ⋯ acc
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.starProjection_inner_eq_zero`.

---

The characterization of the orthogonal projection.  -/
Submodule.orthogonalProjectionFn_inner_eq_zero : ∀ {𝕜 : 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 w : E), w ∈ K → inner 𝕜 (v - K.starProjection v) w = 0
-- Lean.MetavarContext
Lean.MetavarContext.UnivMVarParamResult.mk.sizeOf_spec : ∀ (mctx : Lean.MetavarContext) (newParamNames : Array Lean.Name) (nextParamIdx : ℕ) (expr : Lean.Expr),
  sizeOf { mctx := mctx, newParamNames := newParamNames, nextParamIdx := nextParamIdx, expr := expr } =
    1 + sizeOf mctx + sizeOf newParamNames + sizeOf nextParamIdx + sizeOf expr
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.simp_certC : ℤ →
  Lean.Grind.CommRing.Poly →
    ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → ℕ → Bool
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {f : α → β × γ}, Measurable f → Measurable fun a => (f a).2
-- Mathlib.Order.Heyting.Hom
BiheytingHomClass.toCoheytingHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : BiheytingAlgebra α]
  {x : BiheytingAlgebra β} [BiheytingHomClass F α β], CoheytingHomClass F α β
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, panicking if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyGE! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap.Raw α β cmp → α → α
-- Mathlib.MeasureTheory.Measure.EverywherePos
IsCompact.everywherePosSubset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  IsCompact s → IsCompact (μ.everywherePosSubset s)
-- Mathlib.Algebra.MvPolynomial.Derivation
/-- `MvPolynomial.mkDerivation` as a linear equivalence.  -/
MvPolynomial.mkDerivationEquiv : {σ : Type u_1} →
  (R : Type u_2) →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : Module R A] →
            [inst_3 : Module (MvPolynomial σ R) A] →
              [inst_4 : IsScalarTower R (MvPolynomial σ R) A] → (σ → A) ≃ₗ[R] Derivation R (MvPolynomial σ R) A
-- Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Polynomial.Bivariate.Transcendental.algEquivAdjoin_swap_eq_aeval : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : A}
  (hx : Transcendental R x) (p : Polynomial (Polynomial R)),
  (Polynomial.Bivariate.Transcendental.algEquivAdjoin hx) (Polynomial.Bivariate.swap p) =
    (Polynomial.aeval (Polynomial.C ⟨x, ⋯⟩)) p
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.mk.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (toFun toFun_1 : X → Y)
  (e_toFun : toFun = toFun_1) (continuous_toFun : Continuous toFun),
  { toFun := toFun, continuous_toFun := continuous_toFun } = { toFun := toFun_1, continuous_toFun := ⋯ }