mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.isClosed_C0 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  IsClosed C → ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2), IsClosed (Profinite.NobelingProof.C0 C ho)
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway : ∀ (n : ℕ),
  RingHom.StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] =>
    RingHom.IsStandardSmoothOfRelativeDimension n
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.map : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} → ((a : α) → β a → γ a) → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α γ
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.map_extend_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {y : M},
  y ∈ f.source →
    Filter.map (↑(f.extend I)) (nhdsWithin y s) = nhdsWithin (↑(f.extend I) y) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.separatesPoints_def : ∀ {α : Type u_1} [inst : MeasurableSpace α] [hs : MeasurableSpace.SeparatesPoints α] {x y : α},
  (∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) → x = y
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_of_lt_succ : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p < i.succ → p.succAbove i = i.succ
-- Mathlib.Order.CompleteLattice.Basic
iSup_or : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p ∨ q → α},
  ⨆ (x : p ∨ q), s x = (⨆ (i : p), s ⋯) ⊔ ⨆ (j : q), s ⋯
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instInhabitedEmbedFmt.default : Lean.Widget.EmbedFmt✝
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_ne_bot : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, LowerSet.Iic a ≠ ⊥
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_norm_eq_mul : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedRing E]
  [inst_2 : NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) (n : ℕ),
  ‖FormalMultilinearSeries.ofScalars E c n‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖
-- Lean.Message
/-- Creates a string describing an error message `msg` produced at `pos`, optionally ending at `endPos`,
in `fileName`.

Additional optional arguments can be used to prepend a label `kind` describing the severity of
the error (e.g., `"warning"` or `"error"`) and a bracketed `name` label displaying the name of the
error if it has one.
 -/
Lean.mkErrorStringWithPos : String →
  Lean.Position →
    String →
      optParam (Option Lean.Position) none → optParam (Option String) none → optParam (Option Lean.Name) none → String
-- Lean.Declaration
Lean.InductiveVal.mk.inj : ∀ {toConstantVal : Lean.ConstantVal} {numParams numIndices : ℕ} {all ctors : List Lean.Name} {numNested : ℕ}
  {isRec isUnsafe isReflexive : Bool} {toConstantVal_1 : Lean.ConstantVal} {numParams_1 numIndices_1 : ℕ}
  {all_1 ctors_1 : List Lean.Name} {numNested_1 : ℕ} {isRec_1 isUnsafe_1 isReflexive_1 : Bool},
  { toConstantVal := toConstantVal, numParams := numParams, numIndices := numIndices, all := all, ctors := ctors,
        numNested := numNested, isRec := isRec, isUnsafe := isUnsafe, isReflexive := isReflexive } =
      { toConstantVal := toConstantVal_1, numParams := numParams_1, numIndices := numIndices_1, all := all_1,
        ctors := ctors_1, numNested := numNested_1, isRec := isRec_1, isUnsafe := isUnsafe_1,
        isReflexive := isReflexive_1 } →
    toConstantVal = toConstantVal_1 ∧
      numParams = numParams_1 ∧
        numIndices = numIndices_1 ∧
          all = all_1 ∧
            ctors = ctors_1 ∧
              numNested = numNested_1 ∧ isRec = isRec_1 ∧ isUnsafe = isUnsafe_1 ∧ isReflexive = isReflexive_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.braiding_map_braiding : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X W).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g)
        (CategoryTheory.Limits.biprod.braiding Y Z).hom) =
    CategoryTheory.Limits.biprod.map g f
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.small_unop_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ),
  CategoryTheory.ObjectProperty.Small.{w, v, u} P.unop ↔ CategoryTheory.ObjectProperty.Small.{w, v, u} P
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).p =
    CategoryTheory.CategoryStruct.id S.X₂
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Addneg-add-add version.  -/
Finset.ruzsa_triangle_inequality_addNeg_add_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] (A B C : Finset G),
  (A + -C).card * B.card ≤ (A + B).card * (C + B).card
-- Mathlib.Tactic.Algebra.Basic
/-- `algebra` solves equalities in the language of algebras: ring operations and scalar
multiplications.

Given a goal which is an equality in a commutative `R`-algebra `A`, `algebra` parses the LHS and
RHS of the goal as polynomial expressions of `A`-atoms with coefficients in some semiring `R`, and
closes the goal if the two expressions are the same. The `R`-coefficients are put into ring normal
form.

By default, the scalar ring `R` is inferred automatically by looking for scalar multiplications and
`algebraMap`s present in the expressions. The inference procedure assumes that any two rings `R`
and `S` that appear are comparable, in the sense that either `R` is an `S`-algebra or `S` is an
`R`-algebra.

* `algebra with R` uses the term `R` as the scalar ring, instead of attempting to infer it
automatically.
 -/
Mathlib.Tactic.Algebra.algebraWith : Lean.ParserDescr
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing : {A : Type u_1} → [self : NonUnitalCommCStarAlgebra A] → NonUnitalNormedCommRing A
-- Lean.Data.PersistentHashMap
_private.Lean.Data.PersistentHashMap.0.Lean.PersistentHashMap.foldlMAux.traverse : {m : Type w → Type w'} →
  [Monad m] →
    {σ : Type w} →
      {α : Type u_1} →
        {β : Type u_2} → (σ → α → β → m σ) → (keys : Array α) → (vals : Array β) → keys.size = vals.size → ℕ → σ → m σ
-- Init.Data.Nat.Lemmas
Nat.add_mod_eq_add_mod_left : ∀ {a d b : ℕ} (c : ℕ), a % d = b % d → (c + a) % d = (c + b) % d
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.smul_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  {X : Cᵒᵖ} (r : ↑(R.obj.obj X)), PresheafOfModules.Sheafify.smul α φ r 0 = 0
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
eval_det : ∀ {n : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_3} [inst_2 : CommRing R]
  (M : Matrix n n (Polynomial R)) (r : R),
  Polynomial.eval r M.det = (Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M)).det
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- Coloring induced from a homomorphism to a colored graph.  -/
SimpleGraph.Coloring.comap : {V : Type u} →
  {G : SimpleGraph V} →
    {V' : Type u_4} → {G' : SimpleGraph V'} → {α : Type u_5} → G'.Coloring α → G →g G' → G.Coloring α
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.liftConeMorphism_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t)
  (s : CategoryTheory.Limits.Cone F), (h.liftConeMorphism s).hom = h.lift s
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_id : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  CategoryTheory.CategoryStruct.id X ∣_ U =
    CategoryTheory.CategoryStruct.id ↑((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X).base).obj U)
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- If `f` is continuous at `b` and differentiable on `Iio b`, then `f` is continuous on
`Iic b`.  -/
_private.Mathlib.Analysis.Calculus.DerivativeTest.0.continuousOn_Iic : ∀ {f : ℝ → ℝ} {b : ℝ}, ContinuousAt f b → DifferentiableOn ℝ f (Set.Iio b) → ContinuousOn f (Set.Iic b)
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.evaluation_aut_bijective_of_isGalois : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C)
  [CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj),
  Function.Bijective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) a
-- Mathlib.CategoryTheory.EpiMono
/-- When `g` is an isomorphism, `f ≫ g` is epic iff `f` is.  -/
CategoryTheory.epi_comp_iff_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [CategoryTheory.IsIso g], CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g) ↔ CategoryTheory.Epi f
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι},
  IsOpen s →
    (TendstoLocallyUniformlyOn F f p s ↔
      ∀ x ∈ s, Filter.Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ nhds x) (uniformity β))
-- Lean.Data.NameTrie
Lean.NamePart.num.sizeOf_spec : ∀ (n : ℕ), sizeOf (Lean.NamePart.num n) = 1 + sizeOf n
-- Mathlib.Analysis.CStarAlgebra.Fuglede
_private.Mathlib.Analysis.CStarAlgebra.Fuglede.0.SemiconjBy.star_right_of_unital : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a b x : A} [IsStarNormal a] [IsStarNormal b],
  SemiconjBy x a b → SemiconjBy x (star a) (star b)
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- A pushout square in `Type` where the top map is injective is a pullback square.
This is also essentially the lemma `isPullback_of_isPushout_of_mono_left`
from the file `CategoryTheory.Adhesive.Basic` in the case of the adhesive category of types.  -/
CategoryTheory.Limits.Types.isPullback_of_isPushout : ∀ {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPushout t l r b →
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom t) → CategoryTheory.IsPullback t l r b
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev.congr_simp : ∀ {s : String.Slice} (pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≠ s.startPos), pos.prev h = pos_1.prev ⋯
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell`. -/
Topology.CWComplex.cellFrontier_union_openCell_eq_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.cellFrontier n i ∪ Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.closedCell n i
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_eq_done_iff : ∀ {b : UInt8}, ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.done ↔ b &&& 128 = 0
-- Mathlib.RingTheory.Smooth.Kaehler
sectionOfRetractionKerToTensorAux.congr_simp : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] (l l_1 : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S)))
  (e_l : l = l_1) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (σ σ_1 : S → P) (e_σ : σ = σ_1)
  (hσ : ∀ (x : S), (algebraMap P S) (σ x) = x) [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S]
  (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥),
  sectionOfRetractionKerToTensorAux l hl σ hσ hf' = sectionOfRetractionKerToTensorAux l_1 ⋯ σ_1 ⋯ hf'
-- Mathlib.Order.Directed
DirectedOn.fst : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r₂ : β → β → Prop} {d : Set (α × β)},
  DirectedOn (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) d → DirectedOn (fun x1 x2 => r x1 x2) (Prod.fst '' d)
-- Mathlib.Topology.Homotopy.HSpaces
/-- The definition `toHSpace` is not an instance because it comes together with a
multiplicative version which would lead to a diamond since a topological field would inherit
two `HSpace` structures, one from the `MulOneClass` and one from the `AddZeroClass`.
In the case of an additive group, we make `IsTopologicalAddGroup.hSpace` an instance.  -/
IsTopologicalAddGroup.toHSpace : (M : Type u) → [inst : AddZeroClass M] → [inst_1 : TopologicalSpace M] → [ContinuousAdd M] → HSpace M
-- Mathlib.Data.Set.Finite.Lattice
Set.Finite.iInf_biSup_of_antitone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι'] [Nonempty ι'] [IsDirectedOrder ι']
  [inst_3 : Order.Coframe α] {s : Set ι},
  s.Finite → ∀ {f : ι → ι' → α}, (∀ i ∈ s, Antitone (f i)) → ⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfcₙHom : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A)
  (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) (ha : autoParam (p a) nnnorm_cfcₙHom._auto_1),
  ‖(cfcₙHom ⋯) f‖₊ = ‖f‖₊
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIcc : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → (a b : α) → Fintype ↑(Set.Icc a b)
-- Init.Control.Option
OptionT.instMonadLift : {m : Type u → Type v} → [Monad m] → MonadLift m (OptionT m)
-- Std.Data.String.ToInt
String.toInt?_comp_toSlice : String.Slice.toInt? ∘ String.toSlice = String.toInt?
-- Lean.Message
Lean.instBEqMessageSeverity : BEq Lean.MessageSeverity
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalOptionExprCore : {α : Type} → (Lean.Expr → Lean.MetaM α) → Lean.Expr → Lean.MetaM (Option α)
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
/-- The obvious functor `ShortComplex (J ⥤ C) ⥤ J ⥤ ShortComplex C`.  -/
CategoryTheory.ShortComplex.FunctorEquivalence.functor : (J : Type u_1) →
  (C : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          CategoryTheory.Functor (CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
            (CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
-- Mathlib.Analysis.Convex.Function
/-- Concavity of functions  -/
ConcaveOn : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {β : Type u_5} →
      [Semiring 𝕜] →
        [PartialOrder 𝕜] →
          [AddCommMonoid E] → [AddCommMonoid β] → [PartialOrder β] → [SMul 𝕜 E] → [SMul 𝕜 β] → Set E → (E → β) → Prop
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- An affine combination of two `C^k` connections is a `C^k` connection.  -/
ContMDiffCovariantDerivativeOn.affine_combination : ∀ {𝕜 : 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] {cov cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {u : Set M}
  {f : M → 𝕜} {n : WithTop ℕ∞},
  ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) n f u →
    ContMDiffCovariantDerivativeOn F n cov u →
      ContMDiffCovariantDerivativeOn F n cov' u →
        ContMDiffCovariantDerivativeOn F n (fun σ => f • cov σ + (1 - f) • cov' σ) u
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.preimageIso_mapIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} [inst_2 : F.Full] [inst_3 : F.Faithful] (f : X ≅ Y),
  F.preimageIso (F.mapIso f) = f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instNonemptyState : Nonempty Lean.Meta.Grind.State
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.ofNat_lt_cast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {m n : ℕ} [inst_5 : m.AtLeastTwo], OfNat.ofNat m < ↑n ↔ OfNat.ofNat m < n
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
/-- The natural homomorphism from `Rˣ` to `K⟮∅, n⟯`.  -/
IsDedekindDomain.selmerGroup.fromUnit : {R : Type u} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      {K : Type v} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → {n : ℕ} → Rˣ →* ↥IsDedekindDomain.selmerGroup
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.sum_subtype_add_sum_subtype : ∀ {M : Type u_4} {ι : Type u_7} [inst : Fintype ι] [inst_1 : AddCommMonoid M] (p : ι → Prop) (f : ι → M)
  [inst_2 : DecidablePred p], ∑ i, f ↑i + ∑ i, f ↑i = ∑ i, f i
-- Mathlib.Data.Finsupp.Basic
Finsupp.embDomain_comapDomain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] {f : α ↪ β} {g : β →₀ M},
  ↑g.support ⊆ Set.range ⇑f → Finsupp.embDomain f (Finsupp.comapDomain (⇑f) g ⋯) = g
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.isLeftDerivedFunctor_iff_of_iso : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF' LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : L.comp LF ⟶ F) (α' : L.comp LF' ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  (e : LF ≅ LF'),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft e.hom) α' = α →
    (LF.IsLeftDerivedFunctor α W ↔ LF'.IsLeftDerivedFunctor α' W)
-- Aesop.Forward.State
Aesop.InstMap.mk.injEq : ∀ (map map_1 : Lean.PHashMap Aesop.SlotIndex (Aesop.EMap (Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp))),
  ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.Data.Set.Function
Set.MapsTo.subset_preimage : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s t → s ⊆ f ⁻¹' t
-- Mathlib.Data.Setoid.Partition
/-- The equivalence relation made from the equivalence classes of an equivalence relation `r`
equals `r`.  -/
Setoid.mkClasses_classes : ∀ {α : Type u_1} (r : Setoid α), Setoid.mkClasses r.classes ⋯ = r
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- A commutative group object is a monoid object.  -/
CategoryTheory.CommGrp.toMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommGrp C → CategoryTheory.Mon C
-- Lean.Elab.Tactic.Omega.Core
/-- Helper function for adding an inequality of the form `const + Coeffs.dot coeffs atoms ≥ 0`
to a `Problem`.

(This is only used while initializing a `Problem`. During elimination we use `addConstraint`.)
 -/
Lean.Elab.Tactic.Omega.Problem.addInequality : Lean.Elab.Tactic.Omega.Problem →
  ℤ → Lean.Omega.Coeffs → Option Lean.Elab.Tactic.Omega.Proof → Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Data.Sym.Basic
Sym.mem_mk : ∀ {α : Type u_1} {n : ℕ} (a : α) (s : Multiset α) (h : s.card = n), a ∈ Sym.mk s h ↔ a ∈ s
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.cast'.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig1 aig2 : Std.Sat.AIG α} (s : aig1.RefVec len)
  (h :
    (∀ {i : ℕ} (h : i < len), s.refs[i].gate < aig1.decls.size) →
      ∀ {i : ℕ} (h : i < len), s.refs[i].gate < aig2.decls.size),
  s.cast' h = { refs := s.refs, hrefs := ⋯ }
-- Init.Data.Array.DecidableEq
Array.isEqvAux.congr_simp : ∀ {α : Type u} (xs xs_1 : Array α) (e_xs : xs = xs_1) (ys ys_1 : Array α) (e_ys : ys = ys_1) (hsz : xs.size = ys.size)
  (p p_1 : α → α → Bool),
  p = p_1 → ∀ (i i_1 : ℕ) (e_i : i = i_1) (x : i ≤ xs.size), xs.isEqvAux ys hsz p i x = xs_1.isEqvAux ys_1 ⋯ p_1 i_1 ⋯
-- Mathlib.RingTheory.Invariant.Basic
/-- The isomorphism between `stabilizer G Q ⧸ inertia G Q` and the Galois group of the residue fields
extension `B ⧸ Q` over `A ⧸ P`.
 -/
Ideal.Quotient.stabilizerQuotientInertiaEquiv : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (G : Type u_3) →
            [inst_3 : Group G] →
              [Finite G] →
                [inst_5 : MulSemiringAction G B] →
                  [SMulCommClass G A B] →
                    (P : Ideal A) →
                      (Q : Ideal B) →
                        [Q.IsPrime] →
                          [inst_8 : Q.LiesOver P] →
                            [Algebra.IsInvariant A B G] →
                              ↥(MulAction.stabilizer G Q) ⧸ Ideal.inertia (↥(MulAction.stabilizer G Q)) Q ≃*
                                (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mem_map : ∀ {X Y : TopCat} {f : X ⟶ Y} {U : TopologicalSpace.Opens ↑Y} {x : ↑X},
  x ∈ (TopologicalSpace.Opens.map f).obj U ↔ (TopCat.Hom.hom f) x ∈ U
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.type₁_index : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d + 1} {i : Fin (d + 1)} (h : SSet.prodStdSimplex.pairingCore.IsIndex x hd i.succ), h.type₁.index = i
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.iInf_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M),
  ↑(⨅ i, p i) = ⨅ i, ↑(p i)
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.normalize.processInaccessible : Lean.Expr → Lean.Elab.Term.ToDepElimPattern.M Lean.Expr
-- Mathlib.Topology.Algebra.Support
tsupport_smul_subset_right : ∀ {X : Type u_1} [inst : TopologicalSpace X] {M : Type u_9} {α : Type u_10} [inst_1 : Zero α]
  [inst_2 : SMulZeroClass M α] (f : X → M) (g : X → α), (tsupport fun x => f x • g x) ⊆ tsupport g