mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
algebraicIndependent_iff_injective_aeval : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A], AlgebraicIndependent R x ↔ Function.Injective ⇑(MvPolynomial.aeval x)
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the largest key that is
less than the given key.
 -/
Std.ExtDTreeMap.getKeyLT : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → α
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_singleton_mul : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f g : A),
  ProjectiveSpectrum.zeroLocus 𝒜 {f * g} = ProjectiveSpectrum.zeroLocus 𝒜 {f} ∪ ProjectiveSpectrum.zeroLocus 𝒜 {g}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_le_size_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)}, t.size ≤ (t.insertMany l).size
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The limit of `wideCospan s`. (This will be the supremum of the set of subobjects.)
 -/
CategoryTheory.Subobject.widePullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        [CategoryTheory.Limits.HasWidePullbacks C] → {A : C} → Set (CategoryTheory.Subobject A) → C
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_compl : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α},
  MeasurableSet s →
    ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤ → ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ
-- Mathlib.Order.Filter.Germ.Basic
/-- Coercion from functions to germs as an additive monoid homomorphism.  -/
Filter.Germ.coeAddHom : {α : Type u_1} → {M : Type u_5} → [inst : AddMonoid M] → (l : Filter α) → (α → M) →+ l.Germ M
-- Init.Data.List.Lemmas
/-- We can prove that two folds over the same list are related (by some arbitrary relation)
if we know that the initial elements are related and the folding function, for each element of the list,
preserves the relation.
 -/
List.foldr_rel : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ}
  {r : β → γ → Prop},
  r a b →
    (∀ a ∈ l, ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) →
      r (List.foldr (fun a acc => f a acc) a l) (List.foldr (fun a acc => g a acc) b l)
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.coeff_congr : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} {f : Polynomial R} {r : R},
  f.coeff m = r → m = n → ∀ {s : R}, r = s → f.coeff n = s
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.bind_ret : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream'.WSeq α), s.bind (Stream'.WSeq.ret ∘ f) ~ʷ Stream'.WSeq.map f s
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.toIsPrincipalIdealRing : ∀ {R : Type u} {inst : CommRing R} {inst_1 : IsDomain R} [self : IsDiscreteValuationRing R], IsPrincipalIdealRing R
-- Init.Data.Format.Basic
Std.Format.FlattenAllowability.allow.inj : ∀ {fits fits_1 : Bool},
  Std.Format.FlattenAllowability.allow fits = Std.Format.FlattenAllowability.allow fits_1 → fits = fits_1
-- Mathlib.Order.CompleteBooleanAlgebra
/-- A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice
whose `⊔` distributes over `⨅`.  -/
Order.Coframe : Type u_1 → Type u_1
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_le_rpow_of_nonpos : ∀ {x : NNReal} {z : ℝ} {y : NNReal}, 0 < x → x ≤ y → z ≤ 0 → y ^ z ≤ x ^ z
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X} {g : c.pt ⟶ Y} [F.IsWellOrderContinuous] [inst_4 : SuccOrder J]
  [WellFoundedLT J],
  (∀ (j : J),
      ¬IsMax j →
        CategoryTheory.HasLiftingPropertyFixedBot (F.map (CategoryTheory.homOfLE ⋯)) p
          (CategoryTheory.CategoryStruct.comp (c.ι.app (Order.succ j)) g)) →
    ∀ (sq : CategoryTheory.CommSq f (c.ι.app ⊥) p g), sq.HasLift
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂)[k] = t₂[k]
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def : ∀ {ι : Type u_7} {𝕜 : Type u_8} [inst : RCLike 𝕜] {E : Type u_9} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : FiniteDimensional 𝕜 E] {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) [inst_5 : DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V)
  (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ),
  DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV' =
    ((DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV').symm a).fst
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.csInf_le_of_le : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {a b : α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → BddBelow s → b ∈ s → b ≤ a → sInf s ≤ a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_le_minKey!_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        (compare t.minKey! (Std.DTreeMap.Internal.Impl.erase! k t).minKey!).isLE = true
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_destruct : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β},
  Stream'.WSeq.LiftRel R s t →
    Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) s.destruct t.destruct
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_ofNonUnitalRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R →ₙ+* S) (g : S →ₙ+* R) (h₁ : g.comp f = NonUnitalRingHom.id R) (h₂ : f.comp g = NonUnitalRingHom.id S),
  (RingEquiv.ofNonUnitalRingHom f g h₁ h₂).symm = RingEquiv.ofNonUnitalRingHom g f h₂ h₁
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.mem_range_preOmega_iff : ∀ {x : Ordinal.{u_1}}, x ∈ Set.range ⇑Ordinal.preOmega ↔ x.IsInitial
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.commute_of_mem_adjoin_self : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {a b : A},
  b ∈ R[a] → Commute a b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH1_zero : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H), groupHomology.mapShortComplexH1 f 0 = 0
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.toAddSubmonoid_injective : ∀ {M : Type u_1} [inst : AddZeroClass M], Function.Injective SaturatedAddSubmonoid.toAddSubmonoid
-- Mathlib.MeasureTheory.MeasurableSpace.Card
MeasurableSpace.generateMeasurableRec_mono : ∀ {α : Type u} (s : Set (Set α)), Monotone (MeasurableSpace.generateMeasurableRec s)
-- Mathlib.Order.Filter.Extr
inf_eq_of_isMinOn : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] [inst_1 : OrderTop β] {D : α → β} {s : Finset α} {a : α},
  a ∈ s → IsMinOn D (↑s) a → s.inf D = D a
-- Init.Data.List.TakeDrop
List.takeWhile.eq_def : ∀ {α : Type u} (p : α → Bool) (x : List α),
  List.takeWhile p x =
    match x with
    | [] => []
    | hd :: tl =>
      match p hd with
      | true => hd :: List.takeWhile p tl
      | false => []
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_equiv_eq_comap_symm : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S) (K : Subsemiring R),
  Subsemiring.map (↑f) K = Subsemiring.comap (↑f.symm) K
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists'.cons.match_1.eq_1 : ∀ {α : Type u_1} (motive : Lists α → Lists' α true → Sort u_2) (fst : Bool) (a : Lists' α fst) (l : Lists' α true)
  (h_1 : (fst : Bool) → (a : Lists' α fst) → (l : Lists' α true) → motive ⟨fst, a⟩ l),
  (match ⟨fst, a⟩, l with
    | ⟨fst, a⟩, l => h_1 fst a l) =
    h_1 fst a l
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toArray_filterMap! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  {f : α → β → Option γ},
  t.WF →
    Std.DTreeMap.Internal.Impl.Const.toArray (Std.DTreeMap.Internal.Impl.filterMap! f t) =
      Array.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Std.Data.DTreeMap.Raw.Basic
/-- Carries out a monadic action on each mapping in the tree map in ascending order.  -/
Std.DTreeMap.Raw.forM : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {m : Type w → Type w₂} →
        [Monad m] → ((a : α) → β a → m PUnit.{w + 1}) → Std.DTreeMap.Raw α β cmp → m PUnit.{w + 1}
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.liftEquiv_symm_apply_coe : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C] (f' : TensorProduct R A B →ₐ[S] C),
  ↑(Algebra.TensorProduct.liftEquiv.symm f') =
    (f'.comp Algebra.TensorProduct.includeLeft, (AlgHom.restrictScalars R f').comp Algebra.TensorProduct.includeRight)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.bilinLeftCLM_apply : ∀ {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedAddCommGroup D]
  [inst_7 : NormedSpace ℝ D] [inst_8 : NormedAddCommGroup G] [inst_9 : NormedSpace ℝ G] [inst_10 : NormedSpace 𝕜 F]
  [inst_11 : NormedSpace 𝕜 E] [inst_12 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {g : D → F}
  (hg : Function.HasTemperateGrowth g) (f : SchwartzMap D E),
  ⇑((SchwartzMap.bilinLeftCLM B hg) f) = fun x => (B (f x)) (g x)
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- The descent of a composition is homotopic to the composition of the descents.  -/
CategoryTheory.InjectiveResolution.descCompHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y Z : C} →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) →
            (I : CategoryTheory.InjectiveResolution X) →
              (J : CategoryTheory.InjectiveResolution Y) →
                (K : CategoryTheory.InjectiveResolution Z) →
                  Homotopy (CategoryTheory.InjectiveResolution.desc (CategoryTheory.CategoryStruct.comp f g) K I)
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.desc f J I)
                      (CategoryTheory.InjectiveResolution.desc g K J))
-- Lean.Util.Recognizers
Lean.Expr.app3? : Lean.Expr → Lean.Name → Option (Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Isometry.snd_apply : ∀ {R : Type u_2} (M₁ : Type u_3) {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₂ : QuadraticMap R M₂ P) (self : M₁ × M₂), (QuadraticMap.Isometry.snd M₁ Q₂) self = self.2
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.mk.sizeOf_spec : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_3}
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommMonoid M] {M₂ : Type u_4} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂] [inst_8 : SizeOf R] [inst_9 : SizeOf S]
  [inst_10 : SizeOf M] [inst_11 : SizeOf M₂] (toLinearMap : M →ₛₗ[σ] M₂)
  (cont : autoParam (Continuous toLinearMap.toFun) ContinuousLinearMap.cont._autoParam),
  sizeOf { toLinearMap := toLinearMap, cont := cont } = 1 + sizeOf toLinearMap + sizeOf cont
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.isEmbedding_hom : ∀ (R A : CommRingCat) [inst : TopologicalSpace ↑R], Topology.IsEmbedding fun f => ⇑(CommRingCat.Hom.hom f)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- The inverse of `0` in a group with zero is `0`.  -/
LinearOrderedCommGroupWithZero.inv_zero : ∀ {α : Type u_3} [self : LinearOrderedCommGroupWithZero α], 0⁻¹ = 0
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_symm_addEquivTuple : ∀ {R : Type u_3} [inst : Add R] (c₁ c₂ c₃ : R),
  ⇑(QuaternionAlgebra.addEquivTuple c₁ c₂ c₃).symm = ⇑(QuaternionAlgebra.equivTuple c₁ c₂ c₃).symm
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.edist_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
  {f : X → Y}, HolderWith C r f → ∀ {x y : X} {d : ENNReal}, edist x y ≤ d → edist (f x) (f y) ≤ ↑C * d ^ ↑r
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
RingCat.moduleCatRestrictScalarsPseudofunctor_map : ∀ {X Y : CategoryTheory.LocallyDiscrete RingCatᵒᵖ} (f : X ⟶ Y),
  RingCat.moduleCatRestrictScalarsPseudofunctor.map f = (ModuleCat.restrictScalars (RingCat.Hom.hom f.as.unop)).toCatHom
-- Mathlib.RingTheory.AdjoinRoot
/-- If `p : R[X]` is monic, then there exists a finite free extension of `R` that splits `p`.  -/
Polynomial.Monic.exists_splits_map : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : Polynomial R},
  p.Monic →
    ∃ S x x_1,
      ∃ (_ : Module.Finite R S) (_ : Module.Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobeniusPolyAux.eq_1 : ∀ (p x : ℕ),
  WittVector.frobeniusPolyAux p x =
    MvPolynomial.X (x + 1) -
      ∑ i,
        have x_1 := ⋯;
        ∑ j ∈ Finset.range (p ^ (x - ↑i)),
          (MvPolynomial.X ↑i ^ p) ^ (p ^ (x - ↑i) - (j + 1)) * WittVector.frobeniusPolyAux p ↑i ^ (j + 1) *
            MvPolynomial.C
              ↑((p ^ (x - ↑i)).choose (j + 1) / p ^ (x - ↑i - multiplicity p (j + 1)) *
                  p ^ (j - multiplicity p (j + 1)))
-- Mathlib.Geometry.Manifold.DerivationBundle
PointedContMDiffMap.instAlgebraSomeENatTopContMDiffMapModelWithCornersSelf : {𝕜 : 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] →
                      {x : M} →
                        Algebra (PointedContMDiffMap 𝕜 I M (↑⊤) x) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, a ∈ t.erase k → a ∈ t
-- Init.MetaTypes
/-- When `true` (default: `false`), local definitions are unfolded.
That is, given a local context containing `x : t := e`, then the free variable `x` reduces to `e`.
Otherwise, `x` must be provided as a `simp` argument.
 -/
Lean.Meta.DSimp.Config.zetaDelta : Lean.Meta.DSimp.Config → Bool
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.isProbabilityMeasure_ite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : Prop} [inst : Decidable p] {μ ν : MeasureTheory.Measure α}
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν],
  MeasureTheory.IsProbabilityMeasure (if p then μ else ν)
-- Mathlib.Analysis.InnerProductSpace.NormDet
_private.Mathlib.Analysis.InnerProductSpace.NormDet.0.LinearMap.normDet.eq_1 : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V),
  f.normDet =
    if h : Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 ↥f.range) then
      ‖((LinearMap.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis h.some.toBasis) f.rangeRestrict).det‖
    else 0
-- Mathlib.Topology.Compactness.CountablyCompact
/-- The continuous image of a countably compact set is countably compact.  -/
IsCountablyCompact.image : ∀ {E : Type u_2} {F : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace F] {A : Set E},
  IsCountablyCompact A → ∀ {f : E → F}, Continuous f → IsCountablyCompact (f '' A)
-- Mathlib.Data.List.Sublists
List.sublists'Aux_eq_array_foldl : ∀ {α : Type u} (a : α) (r₁ r₂ : List (List α)),
  List.sublists'Aux a r₁ r₂ = (Array.foldl (fun r l => r.push (a :: l)) r₂.toArray r₁.toArray).toList
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.equivalenceOfReindexing`.

---

The categories of cocones over `F` and `G` are equivalent if `F` and `G` are naturally
isomorphic (possibly after changing the indexing category by an equivalence).
 -/
CategoryTheory.Limits.Cocones.equivalenceOfReindexing : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {G : CategoryTheory.Functor K C} →
                (e : K ≌ J) → (e.functor.comp F ≅ G) → (CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone G)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableOn_id : ∀ {𝕜 : 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] {s : Set M}, MDiff[s] id
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.isIso_pushoutSection_iff : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT),
  CategoryTheory.IsIso (AlgebraicGeometry.pushoutSection H hUST hUSX hUY) ↔
    CategoryTheory.IsPushout (AlgebraicGeometry.Scheme.Hom.appLE iX US UX hUSX)
      (AlgebraicGeometry.Scheme.Hom.appLE f US UT hUST) (AlgebraicGeometry.Scheme.Hom.appLE g UX UY ⋯)
      (AlgebraicGeometry.Scheme.Hom.appLE iY UT UY ⋯)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.centerEquivRootsOfUnity_invFun.eq_1 : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V] (r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)),
  SpecialLinearGroup.centerEquivRootsOfUnity_invFun r = ⟨⟨LinearMap.equivOfIsUnitDet ⋯, ⋯⟩, ⋯⟩
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_nonpos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulMono G₀], a⁻¹ ≤ 0 ↔ a ≤ 0
-- Aesop.BuiltinRules
Aesop.BuiltinRules.empty_false : ∀ (h : Empty), False
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_nonneg : ∀ {K : Type u_1} [inst : RCLike K] {x : ℝ}, 0 ≤ ↑x ↔ 0 ≤ x
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The right inverse of matrix A equals the left inverse of A when they exist.  -/
Matrix.right_inv_eq_left_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B C : Matrix n n α},
  A * B = 1 → C * A = 1 → B = C
-- Mathlib.Analysis.Seminorm
/-- We define the supremum of an arbitrary subset of `Seminorm 𝕜 E` as follows:
* if `s` is `BddAbove` *as a set of functions `E → ℝ`* (that is, if `s` is pointwise bounded
  above), we take the pointwise supremum of all elements of `s`, and we prove that it is indeed a
  seminorm.
* otherwise, we take the zero seminorm `⊥`.

There are two things worth mentioning here:
* First, it is not trivial at first that `s` being bounded above *by a function* implies
  being bounded above *as a seminorm*. We show this in `Seminorm.bddAbove_iff` by using
  that the `Sup s` as defined here is then a bounding seminorm for `s`. So it is important to make
  the case disjunction on `BddAbove ((↑) '' s : Set (E → ℝ))` and not `BddAbove s`.
* Since the pointwise `Sup` already gives `0` at points where a family of functions is
  not bounded above, one could hope that just using the pointwise `Sup` would work here, without the
  need for an additional case disjunction. As discussed on Zulip, this doesn't work because this can
  give a function which does *not* satisfy the seminorm axioms (typically sub-additivity).
 -/
Seminorm.instSupSet : {𝕜 : Type u_3} →
  {E : Type u_7} → [inst : NormedField 𝕜] → [inst_1 : AddCommGroup E] → [inst_2 : Module 𝕜 E] → SupSet (Seminorm 𝕜 E)
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousOn_iff_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  UpperSemicontinuous (s.domRestrict f) ↔ UpperSemicontinuousOn f s
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.isNat_prime_1 : ∀ {n : ℕ}, Mathlib.Meta.NormNum.IsNat n 1 → ¬Nat.Prime n
-- Mathlib.Topology.Connected.Basic
Topology.IsInducing.isPreconnected_image : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : α → β},
  Topology.IsInducing f → (IsPreconnected (f '' s) ↔ IsPreconnected s)
-- Init.Data.List.MinMaxOn
List.minOn?_eq_some_minOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  List.minOn? f xs = some (List.minOn f xs h)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- The Beta function `Β (u, v)`, defined as `∫ x:ℝ in 0..1, x ^ (u - 1) * (1 - x) ^ (v - 1)`.  -/
Complex.betaIntegral : ℂ → ℂ → ℂ
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.lintegral_swapRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {g : γ × β → ENNReal},
  Measurable g → ∫⁻ (c : γ × β), g c ∂κ.swapRight a = ∫⁻ (bc : β × γ), g bc.swap ∂κ a
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.Nonempty.ciSup_eq_max'_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] (f : ι → α) {s : Finset ι}
  (h : s.Nonempty) (h' : optParam (Finset.image f s).Nonempty ⋯), ⨆ i ∈ s, f i = (Finset.image f s).max' h'
-- Mathlib.Data.Fintype.Card
Fintype.not_injective_of_card_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Fintype.card β < Fintype.card α → ¬Function.Injective f