mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_le_integral : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f : X → E}
  {s : Set X} [OrderClosedTopology E],
  MeasureTheory.Integrable f μ → 0 ≤ᵐ[μ] f → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X), f x ∂μ
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.kerTotal.eq_1 : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  KaehlerDifferential.kerTotal R S =
    Submodule.span S
      (((Set.range fun x => ((fun₀ | x.1 => 1) + fun₀ | x.2 => 1) - fun₀ | x.1 + x.2 => 1) ∪
          Set.range fun x => ((fun₀ | x.2 => x.1) + fun₀ | x.1 => x.2) - fun₀ | x.1 * x.2 => 1) ∪
        Set.range fun x => fun₀ | (algebraMap R S) x => 1)
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- Replace the coefficient of a `p : SkewPolynomial R` at a given degree `n : ℕ`
by a given value `a : R`. If `a = 0`, this is equal to `p.erase n`
If `p.natDegree < n` and `a ≠ 0`, this increases the degree to `n`.  -/
SkewPolynomial.update : {R : Type u_1} → [inst : Semiring R] → SkewPolynomial R → ℕ → R → SkewPolynomial R
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unop_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ), S.unop.X₃ = Opposite.unop S.X₁
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc.trans_right_one : ∀ {n : ℕ} {i j k : Fin n} [NeZero n], j ≤ k → ⇑(i.cycleIcc k) ∘ ⇑(k.cycleIcc j) = ⇑(i.cycleIcc k)
-- Init.Data.UInt.Lemmas
BitVec.ofNatLT_uInt8ToNat : ∀ (n : UInt8), n.toNat#'⋯ = n.toBitVec
-- Mathlib.Order.Category.HeytAlg
/-- Typecheck a `HeytingHom` as a morphism in `HeytAlg`.  -/
HeytAlg.ofHom : {X Y : Type u} →
  [inst : HeytingAlgebra X] → [inst_1 : HeytingAlgebra Y] → HeytingHom X Y → (HeytAlg.of X ⟶ HeytAlg.of Y)
-- Mathlib.NumberTheory.Height.NumberField
NumberField.multisetInfinitePlace.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.multisetInfinitePlace K = Finset.univ.val.bind fun v => Multiset.replicate v.mult ↑v
-- Mathlib.Geometry.Manifold.Complex
/-- A holomorphic function on a compact connected complex manifold is the constant function `f ≡ v`,
for some value `v`.  -/
MDifferentiable.exists_eq_const_of_compactSpace : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {H : Type u_3} [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
  {M : Type u_4} [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I 1 M] [CompactSpace M]
  [PreconnectedSpace M] {f : M → F}, MDiff f → ∃ v, f = Function.const M v
-- Mathlib.Analysis.Meromorphic.NormalForm
MeromorphicAt.meromorphicOrderAt_eq_zero_iff_toMeromorphicNFAt_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → (meromorphicOrderAt f x = 0 ↔ toMeromorphicNFAt f x x ≠ 0)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1π_comp_map_assoc : ∀ {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) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k} (h : groupHomology B 1 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.H1π A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.map f φ 1) h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ f φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H1π B) h)
-- Lean.Declaration
Lean.ConstantInfo.axiomInfo.inj : ∀ {val val_1 : Lean.AxiomVal}, Lean.ConstantInfo.axiomInfo val = Lean.ConstantInfo.axiomInfo val_1 → val = val_1
-- Mathlib.CategoryTheory.Abelian.FunctorCategory
CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{z, w} D]
  [inst_2 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C),
  (CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.kernelComparison (CategoryTheory.Limits.cokernel.π α)
        ((CategoryTheory.evaluation C D).obj X))
      (CategoryTheory.Limits.kernel.map ((CategoryTheory.Limits.cokernel.π α).app X)
        (CategoryTheory.Limits.cokernel.π (α.app X)) (CategoryTheory.CategoryStruct.id (G.obj X))
        (CategoryTheory.Limits.PreservesCokernel.iso ((CategoryTheory.evaluation C D).obj X) α).hom ⋯)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
Finset.nullMeasurableSet_biUnion : ∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} (s : Finset ι),
  (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) → MeasureTheory.NullMeasurableSet (⋃ b ∈ s, f b) μ
-- Init.Data.SInt.Bitwise
Int16.toInt64_or : ∀ (a b : Int16), (a ||| b).toInt64 = a.toInt64 ||| b.toInt64
-- Mathlib.NumberTheory.LucasLehmer
/-- The final evaluation needed to establish the Lucas-Lehmer necessity.  -/
LucasLehmer.X.ω_pow_trace : ∀ {q : ℕ} [inst : Fact (Nat.Prime q)],
  Odd q →
    legendreSym q 3 = -1 →
      legendreSym q 2 = 1 → 4 ∣ q + 1 → LucasLehmer.X.ω ^ ((q + 1) / 4) + LucasLehmer.X.ωb ^ ((q + 1) / 4) = 0
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv
        (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S)
  (m : ↥M) (n : ↥N), (M.mulMap N) (m ⊗ₜ[R] n) = ↑m * ↑n
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- The bottom subalgebra is isomorphic to the field.  -/
Algebra.botEquiv : (F : Type u_1) →
  (R : Type u_2) → [inst : Field F] → [inst_1 : Semiring R] → [Nontrivial R] → [inst_3 : Algebra F R] → ↥⊥ ≃ₐ[F] F
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter_eq_add_one : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  k ∉ t → (f (t.get? k)).isSome = true → (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.size = t.size + 1
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabRci : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Data.Finset.Basic
Equiv.Finset.union_inr : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (h : Disjoint s t) (y : ↥t),
  (Equiv.Finset.union s t h) (Sum.inr y) = ⟨↑y, ⋯⟩
-- Init.Sym.Simp.SimprocDSL
/-- Parenthesized discharger expression.  -/
Lean.Parser.Sym.Simp.dischParen : Lean.ParserDescr
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_self : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, Q ⊢ₛ P → P
-- Mathlib.RingTheory.IsAdjoinRoot
/-- `repr` preserves addition, up to multiples of `f`  -/
IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) (x y : S), h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span {f}
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.ι_apply : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] (x : DirectSum I fun i => A i),
  ↑((TensorAlgebra.ι R) x) = (LinearAlgebra.FreeProduct.ι' R A) x
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_smul : ∀ {σ : Type u_1} {A : Type u_2} [inst : CommSemiring A] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Algebra A R]
  {τ : Type u_4} {S : Type u_5} [inst_3 : CommRing S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [IsScalarTower A R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ (r : A) (f : MvPowerSeries σ R), MvPowerSeries.subst a (r • f) = r • MvPowerSeries.subst a f
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- Let `D` be the decomposition field of `P` in `L/K`. Let `𝓟D` be a prime ideal of `D` below `P`,
then `𝓟D` is unramified over `K`.
 -/
IsDecompositionField.ramificationIdx_eq : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [inst_7 : Algebra A K] [IsFractionRing A K] [inst_9 : Algebra A L] [IsScalarTower A K L] [inst_11 : Algebra B L]
  [IsScalarTower A B L] [IsFractionRing B L] [inst_14 : MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L]
  (D : Type u_5) (𝓞D : Type u_6) [inst_16 : Field D] [inst_17 : Algebra D L] [IsDecompositionField K L P D]
  [inst_19 : CommRing 𝓞D] [inst_20 : Algebra 𝓞D D] [IsFractionRing 𝓞D D] [inst_22 : Algebra 𝓞D B]
  [inst_23 : Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D]
  [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B]
  [inst_31 : Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B] [IsDedekindDomain 𝓞D] [𝓟D.LiesOver p]
  [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal], p ≠ ⊥ → 𝓟D.ramificationIdx A = 1
-- Init.Data.Float.Model.Unpacked.Round
/-- Given a finite float represented as a signed mantissa and an exponent, round it to conform to the
given `Format`.

If necessary, this will both decrease and increase the exponent.
 -/
Float.Model.UnpackedFloat.normalize : Float.Model.Format → ℤ → ℤ → Float.Model.UnpackedFloat.Sign → Float.Model.UnpackedFloat
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens),
  I.ideal V ≤
    RingHom.ker
      (CommRingCat.Hom.hom
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app (↑U).ι ↑V)
          (AlgebraicGeometry.Scheme.Hom.app (I.glueDataObjι U) ((TopologicalSpace.Opens.map (↑U).ι.base).obj ↑V))))
-- Mathlib.Tactic.NormNum.Ordinal
/-- The `norm_num` extension for natural power on ordinals.  -/
Mathlib.Meta.NormNum.evalOrdinalNPow : Mathlib.Meta.NormNum.NormNumExt
-- Init.Data.UInt.Lemmas
UInt64.neg_zero : -0 = 0
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorLeftIso_inv_app_unmop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X X_1 : Cᴹᵒᵖ),
  (X.tensorLeftIso.inv.app X_1).unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1.unmop X.unmop)
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (xy, x⁻¹)` is measure-preserving.  -/
MeasureTheory.measurePreserving_mul_prod_inv_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant] [ν.IsMulRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.isoOfLE.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hUV : U ≤ V),
  AlgebraicGeometry.Scheme.Opens.isoOfLE hUV = AlgebraicGeometry.Scheme.Opens.isoOfLE hUV
-- Mathlib.LinearAlgebra.AffineSpace.Independent
AffineIndependent.eq_of_sum_eq_sum_subtype : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {s : Finset V},
  AffineIndependent k Subtype.val →
    ∀ {w₁ w₂ : V → k}, ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i → ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i → ∀ i ∈ s, w₁ i = w₂ i
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.compLeft_apply : ∀ {α : Type u_5} {β : Type u_6} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] (f : α →+ β) (I : Type u_7)
  (h : I → α) (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_neg'' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), deriv (fun x => -x) x = -1
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (r : ℚ), Lean.Grind.Field.NormNum.ofRat r = ↑r.num / ↑r.den
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.instAddPoint : {R : Type u_1} → [inst : CommRing R] → {σ : Type u_5} → (F : FormalGroup R) → Add (F.Point σ)
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.le_of_eq : ∀ {α : Type u_1} {a a' b b' : α} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α],
  a = b → a' + b ≤ b' + a → a' ≤ b'
-- Mathlib.Tactic.NormNum.Basic
/-- If `b` divides `a` and `a` is invertible, then `b` is invertible.  -/
Mathlib.Meta.NormNum.invertibleOfMul : {α : Type u_1} → [inst : Semiring α] → (k : ℕ) → (b a : α) → [Invertible a] → a = ↑k * b → Invertible b
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.ae_toFiniteAux : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ],
  MeasureTheory.ae μ.toFiniteAux = MeasureTheory.ae μ
-- Mathlib.RingTheory.Bialgebra.Hom
/-- The unit of a bialgebra as a `BialgHom`.  -/
Bialgebra.unitBialgHom : (R : Type u_1) →
  (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → R →ₐc[R] A
-- Init.Data.Rat.Lemmas
Rat.normalize_eq_iff : ∀ {d₁ d₂ : ℕ} {n₁ n₂ : ℤ} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0),
  Rat.normalize n₁ d₁ z₁ = Rat.normalize n₂ d₂ z₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
-- Mathlib.Topology.Compactness.SigmaCompact
/-- Prepend the empty set to a compact exhaustion `K n`.  -/
CompactExhaustion.shiftr : {X : Type u_1} → [inst : TopologicalSpace X] → CompactExhaustion X → CompactExhaustion X
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.ext_iff : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : TopologicalSpace A]
  [inst_6 : Module 𝕜 A] {φ ψ : ↑(WeakDual.characterSpace 𝕜 A)}, φ = ψ ↔ ∀ (x : A), φ x = ψ x
-- Mathlib.Tactic.TypeStar
/-- Creates a fresh `Level` parameter which does not appear in the current state's `levelNames`, and
updates the state to include the new level parameter.

By default, the new level parameter is of the form `u_i` and is included in the state as the most
recent level parameter (at the front of the list).

Supplying a `namePrefix` will cause the new level parameter to be of the form `namePrefix_i`, with
`i` starting at `1`.

The new level name can be inserted at a custom position in the list of level names by providing a
function `insert : List Name → Name → List Name` which will be called as
`insert currentLevelNames newLevelName`. It is expected that the result will contain the new level
name and still contain all current level names.
 -/
Lean.Elab.Term.mkFreshLevelParam : optParam Lean.Name `u →
  (optParam (List Lean.Name → Lean.Name → List Lean.Name) fun x head => head :: x) → Lean.Elab.TermElabM Lean.Level
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- The left unitor in the bicategory `Adj B`.  -/
CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : CategoryTheory.Bicategory.Adj B} →
      (α : a ⟶ b) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) α ≅ α
-- Mathlib.Analysis.Normed.Lp.lpSpace
intCast_memℓp_infty : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (z : ℤ),
  Memℓp ↑z ⊤
-- Mathlib.Topology.FiberBundle.Basic
/-- Given a type `E` equipped with a fiber bundle structure, this is a `Prop` typeclass
for trivializations of `E`, expressing that a trivialization is in the designated atlas for the
bundle.  This is needed because lemmas about the linearity of trivializations or the continuity (as
functions to `F →L[R] F`, where `F` is the model fiber) of the transition functions are only
expected to hold for trivializations in the designated atlas.  -/
MemTrivializationAtlas : {B : Type u_2} →
  {F : Type u_3} →
    [inst : TopologicalSpace B] →
      [inst_1 : TopologicalSpace F] →
        {E : B → Type u_5} →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [inst_3 : (b : B) → TopologicalSpace (E b)] →
              [FiberBundle F E] → Bundle.Trivialization F Bundle.TotalSpace.proj → Prop
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mapMahlerMeasure_eq : ∀ {A : Type u_1} [inst : Semiring A] (p : Polynomial A) (v : A →+* ℂ),
  p.mapMahlerMeasure v = (Polynomial.map v p).mahlerMeasure
-- Qq.Match
Qq.Impl.term_comefrom_Do_In_ : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.differentiable_iteratedDeriv_cos : ∀ (n : ℕ), Differentiable ℂ (iteratedDeriv n Complex.cos)
-- Mathlib.Topology.Order.DenselyOrdered
Ioc_subset_closure_interior : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a b : α),
  Set.Ioc a b ⊆ closure (interior (Set.Ioc a b))
-- Std.Async.Select
_private.Std.Async.Select.0.Std.Async.Waiter.mk : {α : Type} → IO.Ref Bool → IO.Promise (Except IO.Error α) → Std.Async.Waiter α
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.Realize.match_1.eq_4 : ∀ {L : FirstOrder.Language} {M : Type u_5} {α : Type u_3}
  (motive : (x : ℕ) → L.BoundedFormula α x → (α → M) → (Fin x → M) → Sort u_4) (x : ℕ) (f₁ f₂ : L.BoundedFormula α x)
  (v : α → M) (xs : Fin x → M)
  (h_1 : (x : ℕ) → (_v : α → M) → (_xs : Fin x → M) → motive x FirstOrder.Language.BoundedFormula.falsum _v _xs)
  (h_2 :
    (x : ℕ) →
      (t₁ t₂ : L.Term (α ⊕ Fin x)) →
        (v : α → M) → (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂) v xs)
  (h_3 :
    (x l : ℕ) →
      (R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin x)) →
          (v : α → M) → (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.rel R ts) v xs)
  (h_4 : (x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → (v : α → M) → (xs : Fin x → M) → motive x (f₁.imp f₂) v xs)
  (h_5 : (x : ℕ) → (f : L.BoundedFormula α (x + 1)) → (v : α → M) → (xs : Fin x → M) → motive x f.all v xs),
  (match x, f₁.imp f₂, v, xs with
    | x, FirstOrder.Language.BoundedFormula.falsum, _v, _xs => h_1 x _v _xs
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂, v, xs => h_2 x t₁ t₂ v xs
    | x, FirstOrder.Language.BoundedFormula.rel R ts, v, xs => h_3 x l R ts v xs
    | x, f₁.imp f₂, v, xs => h_4 x f₁ f₂ v xs
    | x, f.all, v, xs => h_5 x f v xs) =
    h_4 x f₁ f₂ v xs
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_X_of_ne : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {i j : σ}, i ≠ j → MvPolynomial.degreeOf i (MvPolynomial.X j) = 0
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivInvMonoid` if it admits a surjective map
that preserves `1`, `*`, `⁻¹`, and `/` to a `DivInvMonoid`. See note [reducible non-instances].  -/
Function.Surjective.divInvMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₂] →
      [inst_1 : One M₂] →
        [inst_2 : Pow M₂ ℕ] →
          [inst_3 : Inv M₂] →
            [inst_4 : Div M₂] →
              [inst_5 : Pow M₂ ℤ] →
                [inst_6 : DivInvMonoid M₁] →
                  (f : M₁ → M₂) →
                    Function.Surjective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → DivInvMonoid M₂
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- If `m` and `n` are finite, the rank of `m × n` matrices is `(#m).lift * (#n).lift`.  -/
rank_matrix : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] (m : Type v) (n : Type w) [Finite m] [Finite n],
  Module.rank R (Matrix m n R) =
    Cardinal.lift.{max v w u, v} (Cardinal.mk m) * Cardinal.lift.{max v w u, w} (Cardinal.mk n)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.symm_mk_neg : ∀ {M : Type u_1} [inst : Neg M] (a : Mᵈᵃᵃ), DomAddAct.mk.symm (-a) = -DomAddAct.mk.symm a
-- Mathlib.Algebra.Ring.Commute
mul_self_eq_mul_self_iff : ∀ {R : Type u} [inst : NonUnitalNonAssocCommRing R] [NoZeroDivisors R] {a b : R}, a * a = b * b ↔ a = b ∨ a = -b
-- Mathlib.Data.ENNReal.Lemmas
ENNReal.coe_finset_sup : ∀ {α : Type u_1} {s : Finset α} {f : α → NNReal}, ↑(s.sup f) = s.sup fun x => ↑(f x)
-- Mathlib.Order.Filter.Ker
Filter.ker_bot : ∀ {α : Type u_2}, ⊥.ker = ∅
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN_toPolyN : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (e : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Poly.denoteN ctx e.toPolyN = Lean.Grind.Linarith.Expr.denoteN ctx e
-- Mathlib.Order.Hom.CompleteLattice
/-- The proposition that members of `sSupHomClass`s commute with arbitrary suprema/joins.  -/
sSupHomClass.map_sSup : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {inst : SupSet α} {inst_1 : SupSet β} {inst_2 : FunLike F α β}
  [self : sSupHomClass F α β] (f : F) (s : Set α), f (sSup s) = sSup (⇑f '' s)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` reflects colimits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits
of shape `J`.  -/
CategoryTheory.Limits.reflectsLimitsOfShape_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
  [CategoryTheory.Limits.ReflectsColimitsOfShape Jᵒᵖ F.unop], CategoryTheory.Limits.ReflectsLimitsOfShape J F
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_sub_of_le : ∀ {a b : Int64}, 0 ≤ b → b ≤ a → (a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg
-- Lean.Elab.Tactic.Omega.Frontend
/-- Split a disjunction in a `MetaProblem`, and if we find a new usable fact
call `omegaImpl` in both branches.
 -/
Lean.Elab.Tactic.Omega.splitDisjunction : Lean.Elab.Tactic.Omega.MetaProblem → Lean.Elab.Tactic.Omega.OmegaM Lean.Expr
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.exists_eq_mk₃ : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] (w u v : DirectLimit F f),
  ∃ i x y z, w = ⟦⟨i, x⟩⟧ ∧ u = ⟦⟨i, y⟩⟧ ∧ v = ⟦⟨i, z⟩⟧
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcConnectParams.toJson : Lean.Lsp.RpcConnectParams → Lean.Json
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_exp : ∀ {a : EReal}, (ExpGrowth.expGrowthSup fun n => (a * ↑n).exp) = a