mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.upperBound?_mem : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.OrientedCmp cmp] {t : RBTree.RBSet α cmp},
  t.upperBound? x = some y → y ∈ t
-- Init.Data.Order.PackageFactories
Std.PartialOrderPackage.le_antisymm : ∀ {α : Type u} [self : Std.PartialOrderPackage α] (a b : α), a ≤ b → b ≤ a → a = b
-- Mathlib.Data.Fintype.BigOperators
/-- The sum over a product type equals the sum of fiberwise
sums. For rewriting in the reverse direction, use `Fintype.sum_prod_type`.  -/
Fintype.sum_prod_type' : ∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : AddCommMonoid γ]
  (f : α₁ → α₂ → γ), ∑ x, f x.1 x.2 = ∑ x, ∑ y, f x y
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvironmentHeader.mk : UInt32 →
  Lean.Name →
    Bool →
      Array Lean.Import →
        Array Lean.CompactedRegion →
          Array Lean.EffectiveImport →
            Std.HashMap Lean.Name Lean.ModuleIdx →
              Array Lean.EffectiveImport → Array Lean.ModuleData → Lean.EnvironmentHeader
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_add : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, (p + q).support ⊆ p.support ∪ q.support
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.lie_end_of_apply_eq_smul : ∀ {ι : Type u_5} [inst : Fintype ι] [inst_1 : DecidableEq ι] {R : Type u_8} {M : Type u_9} [inst_2 : CommRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (b : Module.Basis ι R M) (a : ι → R) (s : Module.End R M),
  (∀ (k : ι), s (b k) = a k • b k) → ∀ (i j : ι), ⁅s, b.end (i, j)⁆ = (a i - a j) • b.end (i, j)
-- Init.Data.Order.Lemmas
Std.lt_irrefl : ∀ {α : Type u} [inst : LT α] [i : Std.Irrefl fun x1 x2 => x1 < x2] {a : α}, ¬a < a
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.toAlgHom_apply : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommRing 𝕜] [inst_1 : NoZeroDivisors 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : ContinuousAdd 𝕜] [inst_4 : ContinuousConstSMul 𝕜 𝕜] [inst_5 : TopologicalSpace A] [inst_6 : Semiring A]
  [inst_7 : Algebra 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)) (a : A),
  (WeakDual.CharacterSpace.toAlgHom φ) a = (WeakDual.CharacterSpace.toNonUnitalAlgHom φ).toFun a
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
ContMDiffCovariantDerivativeOn.contMDiff : ∀ {𝕜 : 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} {F : Type u_5} {inst_6 : NormedAddCommGroup F}
  {inst_7 : NormedSpace 𝕜 F} {V : M → Type u_6} {inst_8 : TopologicalSpace (Bundle.TotalSpace F V)}
  {inst_9 : (x : M) → AddCommGroup (V x)} {inst_10 : (x : M) → Module 𝕜 (V x)}
  {inst_11 : (x : M) → TopologicalSpace (V x)} {inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)}
  {inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)} {inst_14 : FiberBundle F V} {inst_15 : IsManifold I 1 M}
  {inst_16 : VectorBundle 𝕜 F V} {k : WithTop ℕ∞} {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x}
  {u : Set M} [self : ContMDiffCovariantDerivativeOn F k cov u] {σ : (x : M) → V x},
  ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) (k + 1) (fun x => ⟨x, σ x⟩) u →
    ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] F))) k (fun x => ⟨x, cov σ x⟩) u
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, (m.getKey? a).isSome = m.contains a
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The condition that an element `Splitting.IndexSet Δ` is the distinguished
element `Splitting.IndexSet.Id Δ`.  -/
CategoryTheory.SimplicialObject.Splitting.IndexSet.EqId : {Δ : SimplexCategoryᵒᵖ} → CategoryTheory.SimplicialObject.Splitting.IndexSet Δ → Prop
-- Mathlib.Data.Complex.Basic
Complex.conj_eq_iff_im : ∀ {z : ℂ}, (starRingEnd ℂ) z = z ↔ z.im = 0
-- Mathlib.Data.Matrix.Block
/-- Extract a block from the diagonal of a block diagonal matrix.

This is the block form of `Matrix.diag`, and the left-inverse of `Matrix.blockDiagonal`.  -/
Matrix.blockDiag : {m : Type u_2} → {n : Type u_3} → {o : Type u_4} → {α : Type u_12} → Matrix (m × o) (n × o) α → o → Matrix m n α
-- Mathlib.Analysis.SpecificLimits.Normed
SeminormedAddCommGroup.cauchySeq_of_le_geometric : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] {C r : ℝ},
  r < 1 → ∀ {u : ℕ → α}, (∀ (n : ℕ), ‖u n - u (n + 1)‖ ≤ C * r ^ n) → CauchySeq u
-- Lean.Data.Json.Basic
Lean.Json.bool.sizeOf_spec : ∀ (b : Bool), sizeOf (Lean.Json.bool b) = 1 + sizeOf b
-- Mathlib.Data.Sum.Basic
Sum.LiftRel.exists_of_isRight_left : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ},
  Sum.LiftRel r s x y → x.isRight = true → ∃ b d, s b d ∧ x = Sum.inr b ∧ y = Sum.inr d
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
/-- Alternative formulation of `contravariant_sequence_exact₁`  -/
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (n₀ n₁ : ℕ)
  (h : 1 + n₀ = n₁),
  { X₁ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext S.X₂ Y n₀),
      X₂ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext S.X₁ Y n₀),
      X₃ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext S.X₃ Y n₁),
      f := AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.f).precomp Y ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.Exact
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {x y : CategoryTheory.Coverage C},
  x.coverings = y.coverings → x = y
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.sub_left : ∀ {R₁ : Type u_4} {M₁ : Type u_5} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B₁ : LinearMap.BilinForm R₁ M₁} (x y z : M₁), (B₁ (x - y)) z = (B₁ x) z - (B₁ y) z
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (n : ℤ) [t.IsLE X n]
  (i : EInt), t.IsLE ((t.eTruncGE.obj i).obj X) n
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
/-- In a topological vector space with separating dual, the group of continuous linear equivalences
acts transitively on the set of nonzero vectors: given two nonzero vectors `x` and `y`, there
exists `A : V ≃L[R] V` mapping `x` to `y`.  -/
SeparatingDual.exists_continuousLinearEquiv_apply_eq : ∀ {R : Type u_1} {V : Type u_2} [inst : Field R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace V] [IsTopologicalRing R] [inst_5 : Module R V] [SeparatingDual R V]
  [IsTopologicalAddGroup V] [ContinuousSMul R V] {x y : V}, x ≠ 0 → y ≠ 0 → ∃ A, A x = y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsert!_fst : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.containsThenInsert! k v t).1 = Std.DTreeMap.Internal.Impl.contains k t
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.HasLimit.productLimitCone_cone_π : ∀ {R : Type u} [inst : Ring R] {J : Type w} (f : J → ModuleCat R),
  (ModuleCat.HasLimit.productLimitCone f).cone.π =
    CategoryTheory.Discrete.natTrans fun j => ModuleCat.ofHom (LinearMap.proj j.as)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.fst_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C × D} (f : X ⟶ Y), (CategoryTheory.Prod.fst C D).map f = f.1
-- Mathlib.Algebra.Group.Action.Defs
instVAddOfAdd.eq_1 : ∀ {α : Type u} [inst : Add α], instVAddOfAdd = { vadd := fun x y => Add.add x y }
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.dominant_eq_topologically : @AlgebraicGeometry.IsDominant =
  AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => DenseRange
-- Init.Data.Dyadic.Round
_private.Init.Data.Dyadic.Round.0.Rat.toDyadic.match_1.splitter : (motive : ℤ → Sort u_1) →
  (prec : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive prec
-- Std.Http.Protocol.H1
/-- Finalizes and serializes the outgoing start-line + headers.

This applies connection/identity defaults, enforces framing-header
normalization rules based on status semantics, then appends encoded bytes to
writer output and enters `.writingBody`.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.writeHead : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Message.Head dir.swap → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- Hölder's inequality for the integral of a product of norms. The integral of the product of two
norms of functions is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are
conjugate exponents.  -/
MeasureTheory.integral_mul_norm_le_Lp_mul_Lq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_6} [inst : NormedAddCommGroup E]
  {f g : α → E} {p q : ℝ},
  p.HolderConjugate q →
    MeasureTheory.MemLp f (ENNReal.ofReal p) μ →
      MeasureTheory.MemLp g (ENNReal.ofReal q) μ →
        ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ (a : α), ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ (a : α), ‖g a‖ ^ q ∂μ) ^ (1 / q)
-- Mathlib.RingTheory.WittVector.Complete
WittVector.le_coeff_eq_iff_le_sub_coeff_eq_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] {x y : WittVector p k} {n : ℕ},
  (∀ i < n, x.coeff i = y.coeff i) ↔ ∀ i < n, (x - y).coeff i = 0
-- Mathlib.Analysis.Complex.Poisson
/-- The Herglotz–Riesz kernel integral of a circle-integrable function is differentiable in the pole
parameter, throughout the open ball.
 -/
differentiableOn_circleAverage_herglotzRieszKernel_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {R : ℝ},
  CircleIntegrable f 0 R →
    DifferentiableOn ℂ (fun w => Real.circleAverage (fun ζ => herglotzRieszKernel 0 w ζ • f ζ) 0 R) (Metric.ball 0 R)
-- Mathlib.RingTheory.Localization.Defs
/-- The kernel of `algebraMap` is equal to the annihilator by `map_units'`  -/
IsLocalization.eq_iff_exists : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {x y : R}, (algebraMap R S) x = (algebraMap R S) y ↔ ∃ c, ↑c * x = ↑c * y
-- Mathlib.Algebra.Quandle
/-- The action of the `Shelf` over `α`  -/
Shelf.act : {α : Type u} → [self : Shelf α] → α → α → α
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_mul_le_left : ∀ {R : Type u} [inst : CommSemiring R] (f g : R), PrimeSpectrum.basicOpen (f * g) ≤ PrimeSpectrum.basicOpen f
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toAddMonoidHom_id : ∀ (α : Type u_5) [inst : NonUnitalNonAssocSemiring α], ↑(CentroidHom.id α) = AddMonoidHom.id α
-- Mathlib.Order.KrullDimension
/-- The Krull dimension is the supremum of the elements' heights.

If `α` is `Nonempty`, then `krullDim_eq_iSup_height_of_nonempty`, with the coercion from
`ℕ∞` to `WithBot ℕ∞` outside the supremum, can be more convenient.
 -/
Order.krullDim_eq_iSup_height : ∀ {α : Type u_1} [inst : Preorder α], Order.krullDim α = ⨆ a, ↑(Order.height a)
-- Init.Tactics
/-- Syntax for creating a hypothesis before clearing values.
In `(hx : x = _)`, the value of `x` is unified with `_`.
 -/
Lean.Parser.Tactic.clearValueHyp : Lean.ParserDescr
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.enum_bot : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] [inst_1 : WellFoundedLT α]
  [inst_2 : IsRegularCardinalOrder α] {s : Set α} {hs : IsCofinal s}, ↑((Order.enum s hs) ⊥) = sInf s
-- Mathlib.Algebra.Module.LinearMap.Defs
SemilinearMapClass.map_smul_inv : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} {F : Type u_14} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M]
  [inst_5 : Module S M₃] {σ : R →+* S} (f : F) [inst_6 : FunLike F M M₃] [SemilinearMapClass F σ M M₃] {σ' : S →+* R}
  [RingHomInvPair σ σ'] (c : S) (x : M), c • f x = f (σ' c • x)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.isLeftInversion_of_mem_leftInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B},
  cs.IsReduced ω → ∀ {t : W}, t ∈ cs.leftInvSeq ω → cs.IsLeftInversion (cs.wordProd ω) t
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
derivWithin_cos : ∀ {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → derivWithin (fun x => Real.cos (f x)) s x = -Real.sin (f x) * derivWithin f s x
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.join.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.WSeq α) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (s : Stream'.WSeq α) → motive (some s)),
  (match none with
    | none => h_1 ()
    | some s => h_2 s) =
    h_1 ()
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_bot_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  A.relrank ⊥ = 1
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
/-- Predicate asserting that `pat[0...needlePos] = s[stackPos - needlePos...stackPos]`.  -/
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch : ByteArray → ByteArray → ℕ → ℕ → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_incl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  (c.ofArrowIso e).incl =
    CategoryTheory.CategoryStruct.comp c.incl
      ((CategoryTheory.Functor.const J).map (CategoryTheory.Arrow.Hom.right e.hom))
-- Mathlib.Order.Defs.Unbundled
/-- The carrier of a `RelLowerSet`.  -/
RelLowerSet.carrier : {α : Type u_1} → [inst : LE α] → {P : α → Prop} → RelLowerSet P → Set α
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.of_isIso_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a : R ⟶ X} [CategoryTheory.IsIso a]
  [CategoryTheory.Mono f], CategoryTheory.IsKernelPair f a a
-- Init.Data.String.Lemmas.IsEmpty
String.startPos_ne_endPos_iff : ∀ {s : String}, s.startPos ≠ s.endPos ↔ s ≠ ""
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.sin_eq_sin_iff : ∀ {x y : ℂ}, Complex.sin x = Complex.sin y ↔ ∃ k, y = 2 * ↑k * ↑Real.pi + x ∨ y = (2 * ↑k + 1) * ↑Real.pi - x
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.div_tendsto_atBot_of_degree_gt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Q.degree < P.degree →
    Q ≠ 0 →
      P.leadingCoeff / Q.leadingCoeff ≤ 0 →
        Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atBot
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.Trivialization.contMDiff_iff : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  {f : M → Bundle.TotalSpace F E},
  (∀ (x : M), f x ∈ e.source) →
    (ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f ↔
      (ContMDiff IM IB n fun x => (f x).proj) ∧ ContMDiff IM (modelWithCornersSelf 𝕜 F) n fun x => (↑e (f x)).2)
-- Mathlib.RingTheory.TensorProduct.Free
/-- Given an `R`-algebra `A` and an `R`-basis of `M`, this is an `R`-linear isomorphism
`A ⊗[R] M ≃ (ι →₀ A)` (which is in fact `A`-linear).  -/
Algebra.TensorProduct.basisAux : {R : Type u_1} →
  (A : Type u_2) →
    {M : Type uM} →
      {ι : Type uι} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → Module.Basis ι R M → TensorProduct R A M ≃ₗ[R] ι →₀ A
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.sub : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : AddGroup β] [IsTopologicalAddGroup β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f - g) μ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
SSet.Subcomplex.Pairing.isRegular_iff_nonempty_weakRankFunction : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper], P.IsRegular ↔ Nonempty (P.WeakRankFunction ℕ)
-- Mathlib.Topology.MetricSpace.Isometry
/-- `α` and `β` are isometric if there is an isometric bijection between them.  -/
IsometryEquiv : (α : Type u) → (β : Type v) → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → Type (max u v)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contDiffWithinAtProp_self_target : ∀ {𝕜 : 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} {E' : Type u_5}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : H → E'} {s : Set H} {x : H},
  ContDiffWithinAtProp I (modelWithCornersSelf 𝕜 E') n f s x ↔
    ContDiffWithinAt 𝕜 n (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x)
-- Init.Data.UInt.Lemmas
UInt8.eq_of_toBitVec_eq : ∀ {a b : UInt8}, a.toBitVec = b.toBitVec → a = b
-- Mathlib.Topology.Order.MonotoneContinuity
OrderIso.continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β), Continuous ⇑e
-- Mathlib.Analysis.Complex.Polynomial.Basic
/-- An irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group.  -/
Polynomial.Gal.galActionHom_bijective_of_prime_degree' : ∀ {p : Polynomial ℚ},
  Irreducible p →
    Nat.Prime p.natDegree →
      Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ) →
        Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3 →
          Function.Bijective ⇑(Polynomial.Gal.galActionHom p ℂ)
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_eq_sInf : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.exponent G = sInf {d | 0 < d ∧ ∀ (x : G), d • x = 0}
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.div_left : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {s t : Set α},
  IsLowerSet t → IsUpperSet (s / t)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsSingular.not_isRegular : ∀ {c : Cardinal.{u_1}}, c.IsSingular → ¬c.IsRegular
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.declName? : Lean.Elab.Term.SavedContext → Option Lean.Name
-- Mathlib.ModelTheory.LanguageMap
/-- The inverse of an equivalence of first-order languages.  -/
FirstOrder.Language.LEquiv.symm : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → (L ≃ᴸ L') → (L' ≃ᴸ L)
-- Mathlib.Order.Disjoint
Codisjoint.ne_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b → (a ≠ b ↔ a ≠ ⊤ ∨ b ≠ ⊤)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftCoyonedaEquiv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {F G : CategoryTheory.Functor C (Type (max w v₁))}
  (α : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) (β : F ⟶ G),
  CategoryTheory.uliftCoyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.ConcreteCategory.hom (β.app (Opposite.unop X))) (CategoryTheory.uliftCoyonedaEquiv α)
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.nonempty_Iio`. -/
Finset.Aesop.nonempty_Iio_of_not_isMin : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α], ¬IsMin a → (Finset.Iio a).Nonempty
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_updateFinset : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] [inst_1 : DecidableEq δ] {s : Finset δ}
  {x : (i : δ) → X i}, Measurable (Function.updateFinset x s)
-- Mathlib.Algebra.Group.Pi.Basic
Function.comp_eq_const_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) (f : α → β) {g : β → γ},
  Function.Injective g → (g ∘ f = Function.const α (g b) ↔ f = Function.const α b)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- Ideals in a Dedekind domain have gcd and lcm operators that (trivially) are compatible with
the normalization operator.  -/
Ideal.instStrongNormalizedGCDMonoid : {A : Type u_2} → [inst : CommRing A] → [IsDedekindDomain A] → StrongNormalizedGCDMonoid (Ideal A)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'.d_comp_d : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i j k : ι),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'.d K e i j) (HomologicalComplex.truncGE'.d K e j k) = 0
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
SimpleGraph.IsExtremal.eq_1 : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] (p : SimpleGraph V → Prop),
  G.IsExtremal p =
    (p G ∧ ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj], p G' → G'.edgeFinset.card ≤ G.edgeFinset.card)
-- Init.Data.Iterators.Basic
/-- Every iterator is a plausible indirect successor of itself.  -/
Std.Iter.IsPlausibleIndirectSuccessorOf.refl : ∀ {α β : Type w} [inst : Std.Iterator α Id β] (it : Std.Iter β), it.IsPlausibleIndirectSuccessorOf it
-- Lean.Elab.Term.TermElabM
/-- Execute `x` with the context saved using `saveContext`.
 -/
Lean.Elab.Term.withSavedContext : {α : Type} → Lean.Elab.Term.SavedContext → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α