mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.Pi
/-- If one of the measures `μ i` has value zero on singeltons, them `Measure.pi µ`
has value zero on singletons. The instance below assumes that all `μ i` have value zero on
singletons.  -/
MeasureTheory.Measure.pi_nullSingletonClass : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (i : ι)
  [MeasureTheory.NullSingletonClass (μ i)], MeasureTheory.NullSingletonClass (MeasureTheory.Measure.pi μ)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- In a `BorelSpace` all open sets are measurable.  -/
BorelSpace.opensMeasurable : ∀ {α : Type u_6} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α], OpensMeasurableSpace α
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sub_sUnion : ∀ {α : Type u_2} [inst : Sub α] (s : Set α) (T : Set (Set α)), s - ⋃₀ T = ⋃ t ∈ T, s - t
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The quotient `q` in Weierstrass division, denoted by `f /ʷ g`. Note that when the image of
`g` in the residue field is zero, this is defined to be zero.  -/
PowerSeries.«term_/ʷ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Pi.Basic
/-- The projections of `Functor.pi' F` are isomorphic to the functors of the family `F`  -/
CategoryTheory.Functor.pi'CompEval : {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {A : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
          (F : (i : I) → CategoryTheory.Functor A (C i)) →
            (i : I) → (CategoryTheory.Functor.pi' F).comp (CategoryTheory.Pi.eval C i) ≅ F i
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtype_symm_apply_apply_none : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β) (e : α ≃ { y // y ≠ x }),
  ↑((Equiv.optionSubtype x).symm e) none = x
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_sup : ∀ {α : Type u_1} [inst : DecidableEq α] (u : Finset α), ∀ n < u.card, (Finset.powersetCard n.succ u).sup id = u
-- Mathlib.Topology.MetricSpace.Bounded
totallyBounded_Icc : ∀ {α : Type u} [inst : UniformSpace α] [inst_1 : Preorder α] [CompactIccSpace α] (a b : α), TotallyBounded (Set.Icc a b)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F)
  (γ : Path a b), CurveIntegrable ω γ = IntervalIntegrable (curveIntegralFun ω γ) MeasureTheory.volume 0 1
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.liftAlgHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x : R) [inst_4 : IsLocalization.Away x S] {A : Type u_4} [inst_5 : CommSemiring A]
  [inst_6 : Algebra A R] [inst_7 : Algebra A S] [inst_8 : Algebra A P] [inst_9 : IsScalarTower A R S] {f : R →ₐ[A] P}
  (hf : IsUnit (f x)) (s : S), (IsLocalization.Away.liftAlgHom x hf) s = (IsLocalization.Away.lift x hf) s
-- Mathlib.RingTheory.RingHomProperties
RingHom.StableUnderComposition.respectsIso : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.StableUnderComposition P →
    (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom) → RingHom.RespectsIso P
-- Init.Data.BitVec.Basic
/-- Remainder for signed division rounded to negative infinity.

SMT-LIB name: `bvsmod`.
 -/
BitVec.smod : {m : ℕ} → BitVec m → BitVec m → BitVec m
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.toAddMonoidHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f.toAddMonoidHom = ↑f
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.dirichletInverse_mul_self : ∀ {R : Type u_1} [inst : CommRing R] (f : ArithmeticFunction R) (hf : Invertible (f 1)),
  ArithmeticFunction.dirichletInverse (⇑f) hf * f = 1
-- Init.Data.BitVec.Lemmas
BitVec.instCommutativeHAdd : ∀ {n : ℕ}, Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.toFinset_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] (s t : Set α) [inst_2 : Fintype ↑s] [inst_3 : Fintype ↑t]
  [inst_4 : Fintype ↑(s * t)], (s * t).toFinset = s.toFinset * t.toFinset
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.operation_bind : ∀ {m : Type w → Type w'} [inst : Monad m] {α β : Type w} {x : Std.Iterators.PostconditionT m α}
  {f : α → Std.Iterators.PostconditionT m β},
  (x.bind f).operation = do
    let a ← x.operation
    (fun fa => ⟨↑fa, ⋯⟩) <$> (f ↑a).operation
-- Lean.Data.PersistentArray
Lean.PersistentArray.anyM : {α : Type u} → {m : Type → Type w} → [Monad m] → Lean.PersistentArray α → (α → m Bool) → m Bool
-- Lean.Data.JsonRpc
Lean.JsonRpc.instFromJsonNotification : {α : Type} → [Lean.FromJson α] → Lean.FromJson (Lean.JsonRpc.Notification α)
-- Lean.Parser.Syntax
Lean.Parser.Command.optNamedName.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_right_ι : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data]
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
          i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).right.ι =
    X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯
-- Lean.Meta.Tactic.Try.Collect
/-- Returns `true` if `declName` is in the module being compiled.  -/
Lean.Meta.Try.Collector.inCurrentModule : Lean.Name → Lean.CoreM Bool
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.mkIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.CommGrp C} (e e_1 : G.X ≅ H.X) (e_e : e = e_1)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
        CategoryTheory.MonObj.mul),
  CategoryTheory.CommGrp.mkIso e one_f mul_f = CategoryTheory.CommGrp.mkIso e_1 ⋯ ⋯
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_mulSupport : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M),
  ∏ᶠ (a : α) (_ : a ∈ Function.mulSupport f), f a = ∏ᶠ (a : α), f a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.free.generatingSections_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (I : Type u), (SheafOfModules.free.generatingSections I).I = I
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.isoMk.congr_simp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X}
  (hl hl_1 : f.left ≅ g.left) (e_hl : hl = hl_1) (hw : CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom),
  CategoryTheory.Over.isoMk hl hw = CategoryTheory.Over.isoMk hl_1 ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
HasSum.unique : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} [T2Space α] [L.NeBot] {a₁ a₂ : α}, HasSum f a₁ L → HasSum f a₂ L → a₁ = a₂
-- Init.Data.List.Scan.Lemmas
List.getLast_scanl : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} (h : List.scanl f b l ≠ []),
  (List.scanl f b l).getLast h = List.foldl f b l
-- Mathlib.Data.Finset.Basic
Finset.filter_notMem_eq_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} [inst_1 : (i : α) → Decidable (i ∉ t)], {i ∈ s | i ∉ t} = s \ t
-- Init.Prelude
Lean.MonadQuotation.mk : {m : Type → Type} →
  [toMonadRef : Lean.MonadRef m] → m Lean.MacroScope → m Lean.Name → ({α : Type} → m α → m α) → Lean.MonadQuotation m
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.ofCocone_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  [inst_2 : CategoryTheory.IsFiltered I] {F : CategoryTheory.Functor I C}
  (c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)) (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc).F = F
-- Mathlib.Algebra.Group.Hom.Defs
instSubsingletonOneHom : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] [Subsingleton M], Subsingleton (OneHom M N)
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.instConcreteCategoryAddMonoidHomCarrier.eq_1 : AddMonCat.instConcreteCategoryAddMonoidHomCarrier =
  { hom := fun {X Y} => AddMonCat.Hom.hom', ofHom := fun {X Y} => AddMonCat.Hom.mk✝,
    hom_ofHom := @AddMonCat.instConcreteCategoryAddMonoidHomCarrier._proof_1,
    ofHom_hom := @AddMonCat.instConcreteCategoryAddMonoidHomCarrier._proof_2,
    id_apply := @AddMonCat.instConcreteCategoryAddMonoidHomCarrier._proof_3,
    comp_apply := @AddMonCat.instConcreteCategoryAddMonoidHomCarrier._proof_4 }
-- Init.Data.SInt.Lemmas
Int64.toISize_ofBitVec : ∀ (b : BitVec 64), (Int64.ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)
-- Init.Data.List.Lemmas
List.getLastD_mem_cons : ∀ {α : Type u_1} {l : List α} {a : α}, l.getLastD a ∈ a :: l
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.meromorphic_relation : ∀ (L : PeriodPair), Meromorphic (PeriodPair.relation✝ L)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapRingHom_comp_mapDomainRingHom : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddMonoid M] [inst_3 : AddMonoid N] (f : R →+* S) (g : M →+ N),
  (AddMonoidAlgebra.mapRingHom N f).comp (AddMonoidAlgebra.mapDomainRingHom R g) =
    (AddMonoidAlgebra.mapDomainRingHom S g).comp (AddMonoidAlgebra.mapRingHom M f)
-- Init.Data.Array.Lemmas
Array.anyM.loop.eq_1 : ∀ {α : Type u} {m : Type → Type w} [inst : Monad m] (p : α → m Bool) (as : Array α) (stop : ℕ) (h : stop ≤ as.size)
  (j : ℕ),
  Array.anyM.loop p as stop h j =
    if hlt : j < stop then
      have this := ⋯;
      do
      let __do_lift ← p as[j]
      if __do_lift = true then pure true else Array.anyM.loop p as stop h (j + 1)
    else pure false
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.exists_lt_add_of_not_isPrincipal_add`. -/
Ordinal.exists_lt_add_of_not_principal_add : ∀ {a : Ordinal.{u}}, ¬Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) a → ∃ b < a, ∃ c < a, b + c = a
-- Init.Classical
/-- The Double Negation Theorem: `¬¬P` is equivalent to `P`.
The left-to-right direction, double negation elimination (DNE),
is classically true but not constructively.  -/
Classical.not_not : ∀ {a : Prop}, ¬¬a ↔ a
-- Mathlib.Data.Nat.ModEq
Nat.modEq_modulus_mul_add_iff : ∀ {n a b c : ℕ}, a ≡ n * b + c [MOD n] ↔ a ≡ c [MOD n]
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.sheafCompose_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  {F G : CategoryTheory.Functor A B} (H : CategoryTheory.Functor A B) (η : F ⟶ G) (γ : G ⟶ H)
  [inst_3 : J.HasSheafCompose F] [inst_4 : J.HasSheafCompose G] [inst_5 : J.HasSheafCompose H],
  CategoryTheory.sheafCompose_map J (CategoryTheory.CategoryStruct.comp η γ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafCompose_map J η) (CategoryTheory.sheafCompose_map J γ)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.mk.injEq : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  (toAddEquiv : G ≃+ H)
  (continuous_toFun : autoParam (Continuous toAddEquiv.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toAddEquiv.invFun) Homeomorph.continuous_invFun._autoParam)
  (toAddEquiv_1 : G ≃+ H)
  (continuous_toFun_1 : autoParam (Continuous toAddEquiv_1.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun_1 : autoParam (Continuous toAddEquiv_1.invFun) Homeomorph.continuous_invFun._autoParam),
  ({ toAddEquiv := toAddEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toAddEquiv := toAddEquiv_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 }) =
    (toAddEquiv = toAddEquiv_1)
-- Lean.PrivateName
_private.Lean.PrivateName.0.Lean.privatePrefixAux : Lean.Name → Lean.Name
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a right homology data `h` is preserved by a functor `F`, this functor
preserves the kernel of `h.g' : h.Q ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg' : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [h.IsPreservedBy F],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair h.g' 0) F
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shiftFunctorOpIso.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n m : ℤ)
  (hnm : n + m = 0),
  CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm =
    CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm
-- Mathlib.Order.Filter.Basic
Filter.eventually_iff_all_subsets : ∀ {α : Type u} {f : Filter α} {p : α → Prop}, (∀ᶠ (x : α) in f, p x) ↔ ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
-- Mathlib.RingTheory.Derivation.Lie
/-- Generate an element of `couple` from `x y` satisfying the compatibility equation.  -/
Derivation.Compatible.mk : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u_2} →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          {A' : Type u_3} →
            [inst_3 : CommRing A'] →
              [inst_4 : Algebra R A'] →
                [inst_5 : Algebra A A'] →
                  [inst_6 : IsScalarTower R A A'] →
                    (x : Derivation R A' A') →
                      (y : Derivation R A A) →
                        ⇑x ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑y → ↥(Derivation.couple R A A')
-- Mathlib.RingTheory.PowerSeries.Order
/-- `PowerSeries.divXPowOrder` as a `MonoidHom`.  -/
PowerSeries.divXPowOrderHom : {R : Type u_1} → [inst : Semiring R] → [NoZeroDivisors R] → [Nontrivial R] → PowerSeries R →* PowerSeries R
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.incl_range : ∀ {V₁ : Type u_3} [inst : SeminormedAddCommGroup V₁] (s : AddSubgroup V₁), (NormedAddGroupHom.incl s).range = s
-- Mathlib.Topology.Instances.RealVectorSpace
/-- A topological group carries at most one structure of a topological `ℝ`-module, so for any
topological `ℝ`-algebra `A` (e.g. `A = ℂ`) and any topological group that is both a topological
`ℝ`-module and a topological `A`-module, these structures agree.  -/
Real.isScalarTower : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousSMul ℝ E]
  [T2Space E] {A : Type u_3} [inst_5 : TopologicalSpace A] [inst_6 : Ring A] [inst_7 : Algebra ℝ A]
  [inst_8 : Module A E] [ContinuousSMul ℝ A] [ContinuousSMul A E], IsScalarTower ℝ A E
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiffOn_proj : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  {s : Set (Bundle.TotalSpace F E)}, ContMDiffOn (IB.prod (modelWithCornersSelf 𝕜 F)) IB n Bundle.TotalSpace.proj s
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
_private.Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal.0.IsCyclotomicExtension.Rat.inertiaDegIn_ramificationIdxIn_aux : ∀ (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [IsCyclotomicExtension {n} ℚ K],
  n = p ^ (k + 1) * m →
    ¬p ∣ m →
      (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = orderOf ↑p ∧
        (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p ^ k * (p - 1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_naturality_apply : ∀ {S T : SSet} (f : S ⟶ T) {n : ℕ} (i : Fin (n + 2)) (x : S.obj (Opposite.op { len := n + 1 })),
  (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n })))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ T i))
      ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n + 1 }))) x)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Construct a `Mor₁` term from a lean expression.  -/
Mathlib.Tactic.BicategoryLike.MkMor₁.ofExpr : {m : Type → Type} → [self : Mathlib.Tactic.BicategoryLike.MkMor₁ m] → Lean.Expr → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackComparison_comp_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPullback f g] [inst_3 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
  {Z_1 : D} (h : G.obj Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.snd f g)) h
-- Mathlib.Algebra.Order.Interval.Basic
Interval.div_bot : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : CommGroup α] [inst_2 : MulLeftMono α] (s : Interval α), s / ⊥ = ⊥
-- Aesop.Search.SearchM
Aesop.SearchM.Context.mk : Aesop.LocalRuleSet → Aesop.NormSimpContext → Aesop.Options' → Aesop.SearchM.Context
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.reverse.eq_1 : ∀ {α : Type u_1}, RBTree.RBNode.nil.reverse = RBTree.RBNode.nil
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.mapIdIso.eq_1 : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat),
  CategoryTheory.Pseudofunctor.Grothendieck.mapIdIso F =
    CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Mathlib.Data.Fin.Embedding
Fin.coe_succEmb : ∀ {n : ℕ}, ⇑(Fin.succEmb n) = Fin.succ
-- Mathlib.Analysis.Normed.Module.Basic
RealNormedSpace.noncompactSpace : ∀ (E : Type u_3) [inst : NormedAddCommGroup E] [Nontrivial E] [NormedSpace ℝ E], NoncompactSpace E
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.degree_k_eq_degree : ∀ {m : Lean.Grind.CommRing.Mon}, m.degree_k = m.degree
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_unit_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [inst_2 : ∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))]
  (B : C),
  (CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).unit.app B =
    CategoryTheory.Limits.limit.lift
      (CategoryTheory.Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))
      (CategoryTheory.Comonad.ComonadicityInternal.unitFork adj B)
-- Init.Data.Vector.Lex
Vector.not_lt_empty : ∀ {α : Type u_1} [inst : LT α] (xs : Vector α 0), ¬xs < #v[]
-- Mathlib.Analysis.Convex.Strict
/-- An open convex set is strictly convex.  -/
Convex.strictConvex_of_isOpen : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : Module 𝕜 E] {s : Set E}, IsOpen s → Convex 𝕜 s → StrictConvex 𝕜 s
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Pretrivialization.continuousAlternatingMapCoordChange_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] {B : Type u_3} [inst_1 : TopologicalSpace B]
  {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_5}
  [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : FiberBundle F₁ E₁]
  [inst_14 : (x : B) → TopologicalSpace (E₂ x)] [inst_15 : FiberBundle F₂ E₂]
  {e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [inst_16 : Bundle.Trivialization.IsLinear 𝕜 e₁] [inst_17 : Bundle.Trivialization.IsLinear 𝕜 e₁']
  [inst_18 : Bundle.Trivialization.IsLinear 𝕜 e₂] [inst_19 : Bundle.Trivialization.IsLinear 𝕜 e₂'],
  ∀ b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet),
    ∀ (L : F₁ [⋀^ι]→L[𝕜] F₂),
      (Bundle.Pretrivialization.continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂' b) L =
        (↑(Bundle.Pretrivialization.continuousAlternatingMap 𝕜 ι e₁' e₂')
            ⟨b, (Bundle.Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂).symm b L⟩).2
-- Mathlib.RingTheory.Ideal.HasGoingUp
Ideal.exists_ideal_gt_liesOver_of_lt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.HasGoingUp R S] {p q : Ideal R} [q.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p],
  p < q → ∃ Q, P < Q ∧ Q.IsPrime ∧ Q.LiesOver q
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.instInhabited : Inhabited PFunctor.{u_2, u_1}