mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Fernique
/-- **Alias** of `ProbabilityTheory.Fernique.lintegral_closedBall_sdiff_exp_logRatio_mul_sq_le`.

---

Auxiliary lemma for `lintegral_exp_mul_sq_norm_le_mul`, in which we find an upper bound on an
integral by dealing separately with the contribution of each set in a sequence of annuli.
This is the bound of the integral over one of those annuli.  -/
ProbabilityTheory.Fernique.lintegral_closedBall_diff_exp_logRatio_mul_sq_le : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    2⁻¹ < μ {x | ‖x‖ ≤ a} →
      μ {x | ‖x‖ ≤ a} < 1 →
        ∀ (n : ℕ),
          ∫⁻ (x : E) in
              Metric.closedBall 0 (ProbabilityTheory.Fernique.normThreshold a (n + 1)) \
                Metric.closedBall 0 (ProbabilityTheory.Fernique.normThreshold a n),
              ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio (μ {x | ‖x‖ ≤ a}) * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
            μ {x | ‖x‖ ≤ a} *
              ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal * 2 ^ n))
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.eq_or_mem_iff_mem : ∀ {α : Type u} {s : Stream'.WSeq α} {a a' : α} {s' : Stream'.WSeq α},
  some (a', s') ∈ s.destruct → (a ∈ s ↔ a = a' ∨ a ∈ s')
-- Init.Data.List.Find
List.head?_filter : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.filter p l).head? = List.find? p l
-- Mathlib.Order.Ideal
Order.Ideal.isProper_iff_ne_top : ∀ {P : Type u_1} [inst : LE P] [inst_1 : IsDirectedOrder P] [inst_2 : Nonempty P] {I : Order.Ideal P},
  I.IsProper ↔ I ≠ ⊤
-- Init.Data.Bool
Bool.cond_true : ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A binary fan is just a cone on a diagram indexing a product.  -/
CategoryTheory.Limits.BinaryFan : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Type (max (max 0 u) v)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.toAdditive_symm_apply : ∀ {M : Type u_1} {G : Type u_2} [inst : Monoid M] [inst_1 : CommGroup G] [inst_2 : MulDistribMulAction M G]
  (a : ↑(Rep.ofMulDistribMulAction M G)), Rep.toAdditive.symm a = a
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.instToStringGuessLexRel : ToString Lean.Elab.WF.GuessLex.GuessLexRel
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : TopologicalSpace γ] {f : α → β} {g : α → γ},
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun x => (f x, g x)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
DifferentiableOn.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → DifferentiableOn ℝ (fun x => Real.exp (f x)) s
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
lt_or_le_of_add_le_add : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α] [AddLeftStrictMono α] [AddRightMono α] {a₁ a₂ b₁ b₂ : α},
  a₁ + b₁ ≤ a₂ + b₂ → a₁ < a₂ ∨ b₁ ≤ b₂
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.Value.mk : (n : ℕ) → Fin n → Fin.Value✝
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.instInhabitedNode : {α : Type u_1} → {β : Type u_2} → Inhabited (Lean.PersistentHashMap.Node α β)
-- Mathlib.Topology.Semicontinuity.Basic
LowerSemicontinuousOn.sup : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α},
  LowerSemicontinuousOn f s → LowerSemicontinuousOn g s → LowerSemicontinuousOn (fun x => max (f x) (g x)) s
-- Mathlib.RepresentationTheory.Rep.Basic
/-- `unitIso` of the equivalence between `Action` and `Rep`.  -/
Rep.RepToAction_ActionToRep : (k : Type u) →
  (G : Type v) →
    [inst : Ring k] →
      [inst_1 : Monoid G] → (A : Action (ModuleCat k) G) → (Rep.RepToAction k G).obj ((Rep.ActionToRep k G).obj A) ≅ A
-- Mathlib.RingTheory.Jacobson.Semiprimary
instIsReducedOfIsSemisimpleRing : ∀ (R : Type u_5) [inst : CommRing R] [IsSemisimpleRing R], IsReduced R
-- Lean.Parser.Term
Lean.Parser.Term.cdot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.simpLocalDecl : Lean.MVarId →
  Lean.FVarId →
    Lean.Meta.Simp.Context →
      optParam Lean.Meta.Simp.SimprocsArray #[] →
        optParam (Option Lean.Meta.Simp.Discharge) none →
          optParam Bool true →
            optParam Lean.Meta.Simp.Stats { } → Lean.MetaM (Option (Lean.FVarId × Lean.MVarId) × Lean.Meta.Simp.Stats)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- An `AlgEquiv` between two rings restrict to an `AlgEquiv` between the integral closures inside
them.  -/
AlgEquiv.mapIntegralClosure : {R : Type u_1} →
  {A : Type u_2} →
    {S : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R S] → (A ≃ₐ[R] S) → ↥(integralClosure R A) ≃ₐ[R] ↥(integralClosure R S)
-- Mathlib.CategoryTheory.Category.Preorder
PartialOrder.isIso_iff_eq : ∀ {X : Type u} [inst : PartialOrder X] {a b : X} (f : a ⟶ b), CategoryTheory.IsIso f ↔ a = b
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree.height`.  -/
Tree.height : {α : Type u_1} → Tree α → ℕ
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilteriUnion_mono : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) {l₁ l₂ : BoxIntegral.IntegrationParams},
  l₁ ≤ l₂ →
    ∀ (π₀ : BoxIntegral.Prepartition I),
      BoxIntegral.IntegrationParams.toFilteriUnion I π₀ ≤ BoxIntegral.IntegrationParams.toFilteriUnion I π₀
-- Mathlib.Analysis.Convex.Hull
AffineMap.image_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] (f : E →ᵃ[𝕜] F) (s : Set E),
  ⇑f '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f '' s)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyComplex.isComplex : ∀ {K : Type u_1} {inst : Field K} [self : NumberField.IsTotallyComplex K] (v : NumberField.InfinitePlace K), v.IsComplex
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_eq_top_iff : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α) (x : γ),
  κ.rnDeriv η a x = ⊤ ↔ (a, x) ∈ κ.mutuallySingularSet η
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piSplitAt_apply : ∀ {ι : Type u_7} [inst : DecidableEq ι] (i : ι) (Y : ι → Type u_8) [inst_1 : (j : ι) → TopologicalSpace (Y j)]
  (f : (j : ι) → Y j), (Homeomorph.piSplitAt i Y) f = (f i, fun j => f ↑j)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget.rhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget aig w) → aig.RefVec self.n
-- Init.Data.Array.Extract
Array.popWhile_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool},
  Array.popWhile p (Array.replicate n a) = if p a = true then #[] else Array.replicate n a
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- Typecheck a bifunctor `C ⥤ Dᵒᵖ ⥤ Type w` as a profunctor.  -/
CategoryTheory.Functor.profunctor : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C (CategoryTheory.Functor Dᵒᵖ (Type w)) →
          CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.reduce_v : ∀ (u : PNat.XgcdType), u.reduce.v = u.v
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Coindep.compl_spanning : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Coindep I → M.Spanning (M.E \ I)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.whisker_exchange : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {Q X Y Z : CategoryTheory.LocalizedMonoidal L W ε} (f : Q ⟶ X) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q g)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ioi : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a * x) ⁻¹' Set.Ioi b = Set.Ioi (b / a)
-- Batteries.Tactic.PrintPrefix
/-- Print the type of a declaration.  -/
Batteries.Tactic.PrintPrefixConfig.showTypes : Batteries.Tactic.PrintPrefixConfig → Bool
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.sizeLt.sizeOf_spec : ∀ (lhs n : ℕ), sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.sizeLt lhs n) = 1 + sizeOf lhs + sizeOf n
-- Mathlib.Topology.Algebra.Star.LinearMap
/-- The intrinsic star additive monoid structure on continuous linear maps.  -/
ContinuousLinearMap.intrinsicStarAddMonoid : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : InvolutiveStar R] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module R E] →
              [inst_4 : StarAddMonoid E] →
                [StarModule R E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module R F] →
                      [inst_8 : StarAddMonoid F] →
                        [StarModule R F] →
                          [inst_10 : TopologicalSpace E] →
                            [inst_11 : TopologicalSpace F] →
                              [ContinuousStar E] →
                                [ContinuousStar F] → [inst_14 : ContinuousAdd F] → StarAddMonoid (WithConv (E →L[R] F))
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.InitResults.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (tree : Lean.Meta.RefinedDiscrTree.PreDiscrTree α)
  (errors : Array Lean.Meta.RefinedDiscrTree.ImportFailure✝),
  sizeOf { tree := tree, errors := errors } = 1 + sizeOf tree + sizeOf errors
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Measure.integral_comp_inv_mul_right : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (g : ℝ → F) (a : ℝ),
  ∫ (x : ℝ), g (x * a⁻¹) = |a| • ∫ (y : ℝ), g y
-- Mathlib.Algebra.Star.CentroidHom
CentroidHom.instStarAddMonoid : {α : Type u_1} → [inst : NonUnitalNonAssocSemiring α] → [StarRing α] → StarAddMonoid (CentroidHom α)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vaddCommClass_finset'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : VAdd α γ] [inst_2 : VAdd β γ]
  [VAddCommClass α β γ], VAddCommClass (Finset α) β (Finset γ)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
/-- Pull an additive submonoid back to an opposite submonoid along
`AddOpposite.unop`  -/
AddSubmonoid.op : {M : Type u_2} → [inst : AddZeroClass M] → AddSubmonoid M → AddSubmonoid Mᵃᵒᵖ
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- A linear isometric equivalence that sends an orthonormal basis to a given orthonormal basis.  -/
Orthonormal.equiv : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {ι : Type u_4} →
            {ι' : Type u_5} →
              {E' : Type u_7} →
                [inst_3 : SeminormedAddCommGroup E'] →
                  [inst_4 : InnerProductSpace 𝕜 E'] →
                    {v : Module.Basis ι 𝕜 E} →
                      Orthonormal 𝕜 ⇑v → {v' : Module.Basis ι' 𝕜 E'} → Orthonormal 𝕜 ⇑v' → ι ≃ ι' → E ≃ₗᵢ[𝕜] E'
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- Simplicial `n`-chains `(X.chainComplex R).X n` of a simplicial set `X`
with coefficients in `R` identify to a coproduct of copies of `R`
indexed by `X _⦋n⦌`.  -/
SSet.isColimitChainComplexXCofan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (X : SSet) → (R : C) → (n : ℕ) → CategoryTheory.Limits.IsColimit (X.chainComplexXCofan R n)
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.mk : {α : Type u_1} →
  {s : Set α} →
    (toFun : ℕ → Set α) →
      (∀ (n : ℕ), Finite ↑(toFun n)) → (∀ (n : ℕ), toFun n ⊆ toFun (n + 1)) → ⋃ n, toFun n = s → s.FiniteExhaustion
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.mapₘ : {α : Type u} →
  {β : α → Type v} →
    {δ : α → Type w} → Std.DHashMap.Internal.Raw₀ α β → ((a : α) → β a → δ a) → Std.DHashMap.Internal.Raw₀ α δ
-- Mathlib.Order.CompleteLattice.Lemmas
disjoint_sSup_left : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : Set α} {b : α}, Disjoint (sSup a) b → ∀ {i : α}, i ∈ a → Disjoint i b
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.simprocExtension : Lean.Meta.Simp.SimprocExtension
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {V V₁ : (x : M') → TangentSpace I' x},
  VectorField.mpullbackWithin I I' f (V + V₁) s =
    VectorField.mpullbackWithin I I' f V s + VectorField.mpullbackWithin I I' f V₁ s
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The trivial `AddSubsemigroup` `∅` of an additive magma `M`.  -/
AddSubsemigroup.instBot : {M : Type u_1} → [inst : Add M] → Bot (AddSubsemigroup M)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.simproc.inj : ∀ {declName declName_1 : Lean.Name},
  Lean.Elab.Tactic.ResolveSimpIdResult.simproc declName = Lean.Elab.Tactic.ResolveSimpIdResult.simproc declName_1 →
    declName = declName_1
-- Mathlib.Geometry.Manifold.Immersion
/-- Given an immersion `f` at `x` w.r.t. a complement `F`, this construction provides
a continuous linear equivalence from `F` to the small complement of `F`:
mathematically, this is just the identity map; however, this is technically useful as it enables
us to always work with `hf.smallComplement`.  -/
Manifold.IsImmersionAtOfComplement.smallEquiv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        {F : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup E''] →
                [inst_4 : NormedSpace 𝕜 E''] →
                  [inst_5 : NormedAddCommGroup F] →
                    [inst_6 : NormedSpace 𝕜 F] →
                      {H : Type u_7} →
                        [inst_7 : TopologicalSpace H] →
                          {G : Type u_9} →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    [inst_9 : TopologicalSpace M] →
                                      [inst_10 : ChartedSpace H M] →
                                        {N : Type u_13} →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    (hf : Manifold.IsImmersionAtOfComplement F I J n f x) →
                                                      F ≃L[𝕜] hf.smallComplement
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- If `F` creates limits of any size, it creates finite limits.  -/
CategoryTheory.Limits.CreatesLimitsOfSize.createsFiniteLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] → CategoryTheory.Limits.CreatesFiniteLimits F
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- A special case of `lift_cRank_submatrix` for when the row types are in the same universe.  -/
Matrix.cRank_submatrix : ∀ {m : Type um} {n₀ : Type un₀} {R : Type uR} {m₀ : Type um} {n : Type un} [inst : Semiring R] (A : Matrix m n R)
  (em : m₀ ≃ m) (en : n₀ ≃ n), (A.submatrix ⇑em ⇑en).cRank = A.cRank
-- Std.Sat.CNF.Basic
Std.Sat.CNF.instDecidableExistsVarMemOfDecidableEq : {α : Type u_1} → {f : Std.Sat.CNF α} → [DecidableEq α] → Decidable (∃ v, Std.Sat.CNF.VarMem v f)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.toFormula.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} (x l : ℕ) (_R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin x)),
  (FirstOrder.Language.BoundedFormula.rel _R ts).toFormula = _R.formula ts
-- Mathlib.Data.Nat.Dist
Nat.dist_self : ∀ (n : ℕ), n.dist n = 0
-- Mathlib.Topology.Algebra.Monoid
exists_nhds_one_split4 : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [ContinuousMul M] {u : Set M},
  u ∈ nhds 1 → ∃ V ∈ nhds 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Notation for the product  -/
CategoryTheory.Limits.«term_⨯_» : Lean.TrailingParserDescr
-- Lean.Message
/-- Lifted `Format.group`  -/
Lean.MessageData.group : Lean.MessageData → Lean.MessageData
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.restrict_exists_div_eq : ∀ {K : Type u_7} [inst : DivisionRing K] {Γ₀ : Type u_8} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀) (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ),
  ∃ r s, 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict s = ↑γ
-- Std.Sync.Channel
/-- This function is a no-op and just a convenient way to expose the synchronous API of the channel.
 -/
Std.CloseableChannel.sync : {α : Type} → Std.CloseableChannel α → Std.CloseableChannel.Sync α
-- Mathlib.Algebra.ContinuedFractions.Translations
_private.Mathlib.Algebra.ContinuedFractions.Translations.0.GenContFract.contsAux.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortComplexObj_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C), (Φ.shortComplexObj X).g = Φ.π.app X
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.isAddMonHom_preimage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful) {X Y : C}
  [inst_5 : CategoryTheory.AddMonObj X] [inst_6 : CategoryTheory.AddMonObj Y] (f : F.obj X ⟶ F.obj Y)
  [CategoryTheory.IsAddMonHom f], CategoryTheory.IsAddMonHom (hF.preimage f)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_reindex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {ι : Type w'}
  (e : ι ≃ E.I₀), (E.reindex e).presieve₀ = E.presieve₀
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryingEquiv_symm_apply_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (G : CategoryTheory.Functor (C × D) E) (X : C) (Y : D),
  ((CategoryTheory.Functor.curryingEquiv.symm G).obj X).obj Y = G.obj (X, Y)
-- Mathlib.RingTheory.HahnSeries.Cardinal
/-- The `κ`-bounded subfield of Hahn series with less than `κ` terms.  -/
HahnSeries.cardSuppLTSubfield : (Γ : Type u_1) →
  (R : Type u_2) →
    (κ : Cardinal.{u_1}) →
      [inst : LinearOrder Γ] →
        [inst_1 : AddCommGroup Γ] →
          [inst_2 : IsOrderedAddMonoid Γ] →
            [inst_3 : Field R] → [hκ : Fact (Cardinal.aleph0 < κ)] → Subfield (HahnSeries Γ R)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map'_id_id : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f],
  (CategoryTheory.Limits.Sigma.map' id fun a => CategoryTheory.CategoryStruct.id (f a)) =
    CategoryTheory.CategoryStruct.id (∐ f)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.trace.injEq : ∀ (indent : ℕ) (cls : Lean.Name) (msg : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) (collapsed : Bool)
  (children :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
      (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren))
  (indent_1 : ℕ) (cls_1 : Lean.Name) (msg_1 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) (collapsed_1 : Bool)
  (children_1 :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
      (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)),
  (Lean.Widget.MsgEmbed.trace indent cls msg collapsed children =
      Lean.Widget.MsgEmbed.trace indent_1 cls_1 msg_1 collapsed_1 children_1) =
    (indent = indent_1 ∧ cls = cls_1 ∧ msg = msg_1 ∧ collapsed = collapsed_1 ∧ children = children_1)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.zero_toOuterMeasure : ∀ {α : Type u_1} {_m : MeasurableSpace α}, MeasureTheory.Measure.toOuterMeasure 0 = 0
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- Cast an iso in `TopModuleCat` into a continuous linear equiv.  -/
CategoryTheory.Iso.toContinuousLinearEquiv : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] → {X Y : TopModuleCat R} → (X ≅ Y) → ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.State.mk : Lean.Parser.TokenTable →
  Lean.Parser.SyntaxNodeKindSet → Lean.Parser.ParserCategories → Lean.Parser.ParserExtension.State
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.trivial_X_mon_mul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.MonObj.mul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.Data.FunLike.Equiv
EquivLike.bijective_comp : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [inst : EquivLike E α β] (e : E) (f : β → γ),
  Function.Bijective (f ∘ ⇑e) ↔ Function.Bijective f