mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- The data required for gluing the colimits of the `Dᵢ : J ⥤ P.Over ⊤ (𝒰.X i)`.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [P.IsStableUnderBaseChange] →
    {S : AlgebraicGeometry.Scheme} →
      {J : Type u_1} →
        [inst : CategoryTheory.Category.{v_1, u_1} J] →
          CategoryTheory.Functor J (P.Over ⊤ S) →
            (𝒰 : S.OpenCover) →
              [inst : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀] →
                [AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] → Type (max (max (u + 1) u_1) u_2)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpMaxAux.eq_1 : AddCommGrpMaxAux = AddCommGrpCat
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₁' : CategoryTheory.MorphismProperty D₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [W₁'.RespectsIso] [W₂'.RespectsIso] [L.IsInduced]
  [L.functor.IsEquivalence] [R.IsInduced] [R.functor.IsEquivalence]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor),
  T.IsLeftDerivabilityStructure ↔ B.IsLeftDerivabilityStructure
-- Init.Internal.Order.Basic
Lean.Order.instPartialOrderStateT : {m : Type u_1 → Type u_2} →
  {σ α : Type u_1} → [inst : (α : Type u_1) → Lean.Order.PartialOrder (m α)] → Lean.Order.PartialOrder (StateT σ m α)
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.createsLimitsOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {K : Type z} →
            [inst_2 : CategoryTheory.Category.{z', z} K] →
              [CategoryTheory.Limits.HasLimitsOfShape K D] →
                CategoryTheory.CreatesLimitsOfShape K (CategoryTheory.sheafToPresheaf J D)
-- Mathlib.AlgebraicGeometry.QuasiAffine
AlgebraicGeometry.Scheme.IsQuasiAffine.mk : ∀ {X : AlgebraicGeometry.Scheme} [toCompactSpace : CompactSpace ↥X]
  [toIsImmersion : AlgebraicGeometry.IsImmersion X.toSpecΓ], X.IsQuasiAffine
-- Mathlib.Control.Monad.Cont
ContT.run_seqRight : ∀ {r : Type u} {m : Type u → Type v} {α β : Type w} (x : ContT r m α) (y : ContT r m β) (k : β → m r),
  (x *> y).run k = x.run fun x => y.run k
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.All_and : ∀ {α : Type u_1} {p q : α → Prop} {t : RBTree.RBNode α},
  RBTree.RBNode.All (fun a => p a ∧ q a) t ↔ RBTree.RBNode.All p t ∧ RBTree.RBNode.All q t
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopologicalSpace.Opens.sheafRestrict_obj_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (U : TopologicalSpace.Opens ↑X)
  (X_1 : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) C) {X_2 Y : (TopologicalSpace.Opens ↑(TopCat.of ↥U))ᵒᵖ}
  (f : X_2 ⟶ Y), (U.sheafRestrict.obj X_1).obj.map f = X_1.obj.map (⋯.functor.map f.unop).op
-- Mathlib.NumberTheory.HeckeRing.Defs
HeckeCoset.one_def : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} (H : Subgroup G), 1 = HeckeCoset.mk H H ⟨1, ⋯⟩
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- Generate the suggestion for rewriting with `lem`.  -/
Mathlib.Tactic.ClickSuggestions.GrwLemma.try : Mathlib.Tactic.ClickSuggestions.GrwInfo →
  Mathlib.Tactic.ClickSuggestions.GrwLemma →
    Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM
      (Mathlib.Tactic.ClickSuggestions.Result Mathlib.Tactic.ClickSuggestions.GrwKey)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_false : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, P ∧ ⌜False⌝ ⊣⊢ₛ ⌜False⌝
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_leftUnitor_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C C) (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor F).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Logic.Equiv.Defs
/-- The right summand of `α ⊕ β` is equivalent to `β`.  -/
Equiv.sumIsRight : {α : Type u_1} → {β : Type u_2} → { x // x.isRight = true } ≃ β
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_of_isOpen : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  IsOpen s → x ∈ s → mfderiv[s] f x = mfderiv% f x
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassDistinguished_mul : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {g g' : PowerSeries A} (hg : (PowerSeries.map (IsLocalRing.residue A)) (g * g') ≠ 0),
  (g * g').weierstrassDistinguished hg = g.weierstrassDistinguished ⋯ * g'.weierstrassDistinguished ⋯
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_notMem : ∀ {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent},
  SimpleGraph.ConnectedComponent.Represents s C → c ∉ C → (c.supp \ s).ncard = c.supp.ncard
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw.WFImp.size_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β},
  Std.DHashMap.Internal.Raw.WFImp m → m.size = (Std.DHashMap.Internal.toListModel m.buckets).length
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.mk.inj : ∀ {α : Type u_1} {E : Set α} {IsBase Indep : Set α → Prop} {indep_iff' : ∀ ⦃I : Set α⦄, Indep I ↔ ∃ B, IsBase B ∧ I ⊆ B}
  {exists_isBase : ∃ B, IsBase B} {isBase_exchange : Matroid.ExchangeProperty IsBase}
  {maximality : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X} {subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E}
  {E_1 : Set α} {IsBase_1 Indep_1 : Set α → Prop} {indep_iff'_1 : ∀ ⦃I : Set α⦄, Indep_1 I ↔ ∃ B, IsBase_1 B ∧ I ⊆ B}
  {exists_isBase_1 : ∃ B, IsBase_1 B} {isBase_exchange_1 : Matroid.ExchangeProperty IsBase_1}
  {maximality_1 : ∀ X ⊆ E_1, Matroid.ExistsMaximalSubsetProperty Indep_1 X}
  {subset_ground_1 : ∀ (B : Set α), IsBase_1 B → B ⊆ E_1},
  { E := E, IsBase := IsBase, Indep := Indep, indep_iff' := indep_iff', exists_isBase := exists_isBase,
        isBase_exchange := isBase_exchange, maximality := maximality, subset_ground := subset_ground } =
      { E := E_1, IsBase := IsBase_1, Indep := Indep_1, indep_iff' := indep_iff'_1, exists_isBase := exists_isBase_1,
        isBase_exchange := isBase_exchange_1, maximality := maximality_1, subset_ground := subset_ground_1 } →
    E = E_1 ∧ IsBase = IsBase_1 ∧ Indep = Indep_1
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Given a map `r : I₁ × I₂ × I₃ → J`, a `BifunctorComp₁₂IndexData r` consists of the data
of a type `I₁₂`, maps `p : I₁ × I₂ → I₁₂` and `q : I₁₂ × I₃ → J`, such that `r` is obtained
by composition of `p` and `q`.  -/
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData : {I₁ : Type u_7} →
  {I₂ : Type u_8} →
    {I₃ : Type u_9} → {J : Type u_10} → (I₁ × I₂ × I₃ → J) → Type (max (max (max (max u_10 (u_11 + 1)) u_7) u_8) u_9)
-- Mathlib.Topology.Order.Hom.Esakia
/-- Composition of `PseudoEpimorphism`s as a `PseudoEpimorphism`.  -/
PseudoEpimorphism.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : Preorder γ] → PseudoEpimorphism β γ → PseudoEpimorphism α β → PseudoEpimorphism α γ
-- Mathlib.Util.AtomM.Recurse
/-- The read-only state of the `AtomM.Recurse` monad.  -/
Mathlib.Tactic.AtomM.Recurse.Context : Type
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.opEquivalence_unitIso : CategoryTheory.RelCat.opEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id CategoryTheory.RelCat)
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.accumulate_mem : ∀ {α : Type u_1} {C : Set (Set α)},
  MeasureTheory.IsSetRing C → ∀ {s : ℕ → Set α}, (∀ (i : ℕ), s i ∈ C) → ∀ (n : ℕ), Set.accumulate s n ∈ C
-- Init.Data.Int.Lemmas
Int.neg_eq_comm : ∀ {a b : ℤ}, -a = b ↔ -b = a
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The forwards direction of the universal property; an algebra morphism out of the graded tensor
product can be assembled from maps on each component that (anti)commute on pure elements of the
corresponding graded algebras.  -/
GradedTensorProduct.lift : {R : Type u_1} →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              [inst_9 : Module ι (Additive ℤˣ)] →
                                {C : Type u_5} →
                                  [inst_10 : Ring C] →
                                    [inst_11 : Algebra R C] →
                                      (f : A →ₐ[R] C) →
                                        (g : B →ₐ[R] C) →
                                          (∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                                              f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)) →
                                            GradedTensorProduct R 𝒜 ℬ →ₐ[R] C
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {km : α}, t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Init.Data.Array.Lex.Lemmas
List.le_toArray : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂
-- Mathlib.Data.ENat.Lattice
ENat.sSup_eq_top_of_infinite : ∀ {s : Set ℕ∞}, s.Infinite → sSup s = ⊤
-- Init.Data.String.Substring
Substring.atEnd : Substring.Raw → String.Pos.Raw → Bool
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.mk.injEq : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (toFun : L → R) (genWeightSpace_ne_bot' : LieModule.genWeightSpace M toFun ≠ ⊥)
  (toFun_1 : L → R) (genWeightSpace_ne_bot'_1 : LieModule.genWeightSpace M toFun_1 ≠ ⊥),
  ({ toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' } =
      { toFun := toFun_1, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'_1 }) =
    (toFun = toFun_1)
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- A map from a space to its completion.  -/
AbstractCompletion.coe : {α : Type u} → [inst : UniformSpace α] → (self : AbstractCompletion.{v, u} α) → α → self.space
-- Mathlib.Analysis.Normed.Module.MStructure
IsMprojection.Mnorm : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] {P : M},
  IsMprojection X P → ∀ (x : X), ‖x‖ = max ‖P • x‖ ‖(1 - P) • x‖
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_cons : ∀ {M : Type u_3} [inst : AddCommMonoid M] (a : M) (s : Multiset M), (a ::ₘ s).sum = a + s.sum
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.forgetAdjToOver_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (Z : CategoryTheory.Over X),
  (CategoryTheory.forgetAdjToOver X).unit.app Z =
    CategoryTheory.Over.homMk
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id Z.left) Z.hom) ⋯
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.composableArrows₅.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS₁ : S₁.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  HomologicalComplex.HomologySequence.composableArrows₅ hS₁ i j hij =
    CategoryTheory.ComposableArrows.mk₅ (HomologicalComplex.homologyMap S₁.f i) (HomologicalComplex.homologyMap S₁.g i)
      (hS₁.δ i j hij) (HomologicalComplex.homologyMap S₁.f j) (HomologicalComplex.homologyMap S₁.g j)
-- Init.PropLemmas
and_iff_right : ∀ {a b : Prop}, a → (a ∧ b ↔ b)
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.piAntidiag_insert : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCancelCommMonoid μ]
  [inst_2 : Finset.HasAntidiagonal μ] [inst_3 : DecidableEq μ] {i : ι} {s : Finset ι} [inst_4 : DecidableEq (ι → μ)],
  i ∉ s →
    ∀ (n : μ),
      (insert i s).piAntidiag n =
        (Finset.HasAntidiagonal.antidiagonal n).biUnion fun p =>
          Finset.image (fun f j => f j + if j = i then p.1 else 0) (s.piAntidiag p.2)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.numParams : Lean.Elab.Command.AddAndFinalizeContext✝ → ℕ
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.ext : ∀ {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.MonoidalLeftAction C D}
  {A : C} {inst_4 : CategoryTheory.AddMonObj A} {M N : CategoryTheory.AddMod D A} {x y : M.Hom N}, x.hom = y.hom → x = y
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.inclusion.eq_1 : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} (h : s ⊆ t),
  ContinuousMap.inclusion h = { toFun := Set.inclusion h, continuous_toFun := ⋯ }
-- Mathlib.Order.Filter.SmallSets
/-- The filter `l.smallSets` is the largest filter containing all powersets of members of `l`.  -/
Filter.smallSets : {α : Type u_1} → Filter α → Filter (Set α)
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
/-- If `L : C ⥤ D` is a localization functor with respect to a Serre class `P` in
the abelian category `C`, then `D` is an abelian category.
Note that we assume that `D` has already been equipped with a preadditive structure,
and that `L` is additive. Otherwise, see the results in the file
`Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean`
which applies because `P.isoModSerre` has a calculus of left and right fractions.  -/
CategoryTheory.ObjectProperty.SerreClassLocalization.abelian : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {D : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} D] →
          (L : CategoryTheory.Functor C D) →
            (P : CategoryTheory.ObjectProperty C) →
              [inst_3 : P.IsSerreClass] →
                [L.IsLocalization P.isoModSerre] →
                  [inst_5 : CategoryTheory.Preadditive D] → [L.Additive] → CategoryTheory.Abelian D
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.isInferredPublic : Lean.Environment → Lean.Elab.Modifiers → Bool
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.instCoeFunHomForallCarrierCarrier : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (X Y : AlgebraicGeometry.PresheafedSpace C) → CoeFun (X ⟶ Y) fun x => ↑↑X → ↑↑Y
-- Mathlib.Data.Multiset.Basic
Multiset.choose_eq_iff : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : Multiset α) (hp : ∃! a, a ∈ l ∧ p a) {a : α},
  Multiset.choose p l hp = a ↔ a ∈ l ∧ p a
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.symm_proj_apply : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : ∀ (x : B), Nonempty (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (z : Bundle.TotalSpace F E),
  z.proj ∈ e.baseSet → e.symm z.proj (↑e z).2 = z.snd
-- Mathlib.Algebra.Group.Finsupp
Finsupp.single_neg : ∀ {ι : Type u_1} {G : Type u_6} [inst : AddGroup G] (a : ι) (b : G), (fun₀ | a => -b) = -fun₀ | a => b
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.addSubgroup_antitone : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  Antitone ArchimedeanClass.addSubgroup
-- Mathlib.Topology.Category.TopCat.Basic
/-- Typecheck a `ContinuousMap` as a morphism in `TopCat`.  -/
TopCat.ofHom : {X Y : Type u} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → (TopCat.of X ⟶ TopCat.of Y)
-- Mathlib.NumberTheory.LSeries.Positivity
/-- If all values of a `ℂ`-valued arithmetic function are nonnegative reals and `x` is a
real number in the domain of absolute convergence, then the `n`th iterated derivative
of the associated L-series is nonnegative real when `n` is even and nonpositive real
when `n` is odd.  -/
ArithmeticFunction.iteratedDeriv_LSeries_alternating : ∀ (a : ArithmeticFunction ℂ),
  (∀ (n : ℕ), 0 ≤ a n) →
    ∀ {x : ℝ}, LSeries.abscissaOfAbsConv ⇑a < ↑x → ∀ (n : ℕ), 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries fun x => a x) ↑x
-- Mathlib.RingTheory.HopfAlgebra.Basic
/-- Upgrade a commutative bialgebra to a Hopf algebra by specifying the antipode `A →ₐ[R] A`
with appropriate conditions.  -/
HopfAlgebra.ofAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring A] →
        [inst_2 : Bialgebra R A] →
          (antipode : A →ₐ[R] A) →
            (Algebra.TensorProduct.lift antipode (AlgHom.id R A) ⋯).comp (Bialgebra.comulAlgHom R A) =
                (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A) →
              (Algebra.TensorProduct.lift (AlgHom.id R A) antipode ⋯).comp (Bialgebra.comulAlgHom R A) =
                  (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A) →
                HopfAlgebra R A
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context.mk.injEq : ∀ (knowsType knowsLevel inBottomUp parentIsApp : Bool) (subExpr : Lean.SubExpr)
  (knowsType_1 knowsLevel_1 inBottomUp_1 parentIsApp_1 : Bool) (subExpr_1 : Lean.SubExpr),
  ({ knowsType := knowsType, knowsLevel := knowsLevel, inBottomUp := inBottomUp, parentIsApp := parentIsApp,
        subExpr := subExpr } =
      { knowsType := knowsType_1, knowsLevel := knowsLevel_1, inBottomUp := inBottomUp_1, parentIsApp := parentIsApp_1,
        subExpr := subExpr_1 }) =
    (knowsType = knowsType_1 ∧
      knowsLevel = knowsLevel_1 ∧ inBottomUp = inBottomUp_1 ∧ parentIsApp = parentIsApp_1 ∧ subExpr = subExpr_1)
-- Mathlib.Algebra.Ring.Pi
RingHom.pi_injective : ∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [inst : (i : I) → NonAssocSemiring (f i)]
  [inst_1 : NonAssocSemiring γ] (g : (i : I) → γ →+* f i),
  (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(RingHom.pi g)
-- Mathlib.RingTheory.AdicCompletion.Completeness
_private.Mathlib.RingTheory.AdicCompletion.Completeness.0.AdicCompletion.ofValEqZeroAux_exists : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {a b c : ℕ} {x : AdicCompletion I M} (h : c = b + a),
  ↑x a = 0 → ∃ t, (Submodule.powSMulQuotInclusion I M h ⊤) t = ↑x c
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_inf_div_inf_le_mabs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b c : α), |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
-- Mathlib.Topology.PartialHomeomorph.Defs
Homeomorph.toPartialHomeomorphOfImageEq_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (t : Set Y) (h : ⇑e '' s = t), (e.toPartialHomeomorphOfImageEq s t h).target = t
-- Mathlib.Algebra.GroupWithZero.Prod
/-- Multiplication as a multiplicative homomorphism with zero.  -/
mulMonoidWithZeroHom : {M₀ : Type u_1} → [inst : CommMonoidWithZero M₀] → M₀ × M₀ →*₀ M₀
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_comp_neg_atTop_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] {l : Filter α}
  {f : G → α}, Filter.Tendsto (fun x => f (-x)) Filter.atTop l ↔ Filter.Tendsto f Filter.atBot l
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_of_measurable_union_cover : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (s t : Set α),
  MeasurableSet s →
    MeasurableSet t → Set.univ ⊆ s ∪ t → (Measurable fun a => f ↑a) → (Measurable fun a => f ↑a) → Measurable f
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_zero_of_row_eq_zero : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A : Matrix n n R}
  (i : n), (∀ (j : n), A i j = 0) → A.det = 0
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.limit_add_val : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u})
  (x y : ↑(ProfiniteAddGrp.limit F).toProfinite.toTop) (j : J), ↑(x + y) j = ↑x j + ↑y j
-- Aesop.Index.Forward
/-- Get the forward rules whose maximal premises likely unify with `e`.
Each returned pair `(r, i)` contains a rule `r` and the index `i` of the premise
of `r` that likely unifies with `e`.  -/
Aesop.ForwardIndex.get : Aesop.ForwardIndex → Lean.Expr → Lean.MetaM (Array (Aesop.ForwardRule × Aesop.PremiseIndex))
-- Init.Data.Array.Lemmas
Array.and_any_distrib_left : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool} {q : Bool}, (q && xs.any p) = xs.any fun a => q && p a
-- Init.Prelude
instMonadReaderOfOfMonadLift : {ρ : Type u} → {m : Type u → Type v} → {n : Type u → Type w} → [MonadLift m n] → [MonadReaderOf ρ m] → MonadReaderOf ρ n
-- Init.Data.Int.Basic
Int.zero_ne_one : 0 ≠ 1
-- Mathlib.Logic.Equiv.Prod
Equiv.prodShear_symm_apply : ∀ {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂),
  ⇑(e₁.prodShear e₂).symm = fun y => (e₁.symm y.1, (e₂ (e₁.symm y.1)).symm y.2)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.blocksFun_congr : ∀ {n₁ n₂ : ℕ} (c₁ : Composition n₁) (c₂ : Composition n₂) (i₁ : Fin c₁.length) (i₂ : Fin c₂.length),
  n₁ = n₂ → c₁.blocks = c₂.blocks → ↑i₁ = ↑i₂ → c₁.blocksFun i₁ = c₂.blocksFun i₂