mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
/-- The total derivative of a function in two variables is the sum of the partial derivatives.
Note that to state this (without casts) we need to be able to see through the definition of
`TangentSpace`. Version in terms of the one-variable derivatives.  -/
mfderiv_prod_eq_add_comp : ∀ {𝕜 : 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'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M × M' → M''} {p : M × M'},
  MDiffAt f p →
    mfderiv% f p =
      (mfderiv% fun z => f (z, p.2)) p.1 ∘SL id (ContinuousLinearMap.fst 𝕜 E E') +
        (mfderiv% fun z => f (p.1, z)) p.2 ∘SL id (ContinuousLinearMap.snd 𝕜 E E')
-- Init.Data.Nat.Lemmas
Nat.sub_one_sub_lt : ∀ {i n : ℕ}, i < n → n - 1 - i < n
-- Mathlib.Topology.Path
Path.extend_range : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b), Set.range ⇑γ.extend = Set.range ⇑γ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₂_ext_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G}
  {f₁ f₂ : ↥(groupCohomology.cocycles₂ A)}, f₁ = f₂ ↔ ∀ (g h : G), f₁ (g, h) = f₂ (g, h)
-- Init.Data.Order.Ord
Std.OrientedCmp.lt_of_gt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, cmp a b = Ordering.gt → cmp b a = Ordering.lt
-- Mathlib.SetTheory.Ordinal.Notation
ONote.FundamentalSequenceProp.eq_3 : ∀ (o : ONote) (f : ℕ → ONote),
  o.FundamentalSequenceProp (Sum.inr f) =
    (Order.IsSuccLimit o.repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < o ∧ (o.NF → (f i).NF)) ∧ ∀ a < o.repr, ∃ i, a < (f i).repr)
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Nontrivial S]
  [Algebra.IsStandardSmooth R S] (n : ℕ), Algebra.IsStandardSmoothOfRelativeDimension n R S ↔ Module.rank S Ω[S⁄R] = ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)] {Z_1 : C} (h : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f' f) g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f' (CategoryTheory.Limits.pullback.fst f g))
      h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_1.splitter : (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
  (motive : Std.Tactic.BVDecide.Return aig → Sort u_1) →
    (x : Std.Tactic.BVDecide.Return aig) →
      ((aig_1 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
          (exprRef : aig_1.Ref) →
            (hexpr : aig.decls.size ≤ { aig := aig_1, ref := exprRef }.aig.decls.size) →
              (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑⟨{ aig := aig_1, ref := exprRef }, hexpr⟩).aig) →
                motive { result := ⟨{ aig := aig_1, ref := exprRef }, hexpr⟩, cache := cache }) →
        motive x
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.ofMeasure.inj : ∀ {α : Type u_2} {toMeasure toMeasure_1 : α},
  MeasureTheory.LevyProkhorov.ofMeasure toMeasure = MeasureTheory.LevyProkhorov.ofMeasure toMeasure_1 →
    toMeasure = toMeasure_1
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_inf : ∀ {u v : ℕ → EReal},
  LinearGrowth.linearGrowthInf (u ⊓ v) = min (LinearGrowth.linearGrowthInf u) (LinearGrowth.linearGrowthInf v)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_toIocDiv_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), toIocMod hp a b + ↑(toIocDiv hp a b) * p = b
-- Mathlib.Data.NNRat.Defs
NNRat.ext : ∀ {p q : ℚ≥0}, ↑p = ↑q → p = q
-- Mathlib.Algebra.Module.PUnit
PUnit.vadd_eq' : ∀ {R : Type u_1} (r : PUnit.{u_3 + 1}) (a : R), r +ᵥ a = a
-- Lean.Parser.Extension
Lean.Parser.declareLeadingBuiltinParser : Lean.Name → Lean.Name → ℕ → Lean.CoreM Unit
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.elabInductiveViews : Array Lean.Expr → Array Lean.Elab.Command.InductiveElabStep1 → Lean.Elab.TermElabM Lean.Elab.Command.FinalizeContext✝
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.compl.congr_simp : ∀ {α : Type u_1} {V : Type u_2} [inst : Zero α] [inst_1 : One α] [inst_2 : DecidableEq α] {inst_3 : DecidableEq V}
  [inst_4 : DecidableEq V] (A A_1 : Matrix V V α),
  A = A_1 → ∀ (a a_1 : V), a = a_1 → ∀ (a_2 a_3 : V), a_2 = a_3 → A.compl a a_2 = A_1.compl a_1 a_3
-- Mathlib.Combinatorics.Enumerative.Composition
/-- The composition made of a single block of size `n`.  -/
Composition.single : (n : ℕ) → 0 < n → Composition n
-- Init.Data.UInt.Lemmas
USize.ofBitVec_neg : ∀ (b : BitVec System.Platform.numBits), { toBitVec := -b } = -{ toBitVec := b }
-- Mathlib.Data.NNReal.Basic
NNReal.mul_iSup : ∀ {ι : Sort u_3} (f : ι → NNReal) (a : NNReal), a * ⨆ i, f i = ⨆ i, a * f i
-- Lean.Elab.Binders
Lean.Elab.Term.precheckArrow : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Order.Filter.Pointwise
Filter.bot_mul : ∀ {α : Type u_2} [inst : Mul α] {g : Filter α}, ⊥ * g = ⊥
-- Mathlib.Analysis.Normed.Group.Defs
GroupSeminorm.toSeminormedCommGroup.eq_1 : ∀ {E : Type u_5} [inst : CommGroup E] (f : GroupSeminorm E),
  f.toSeminormedCommGroup =
    { toNorm := f.toSeminormedGroup.toNorm, toGroup := f.toSeminormedGroup.toGroup, mul_comm := ⋯,
      toPseudoMetricSpace := f.toSeminormedGroup.toPseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.compContinuous_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] (f : BoundedContinuousFunction α β) (g : C(δ, α)) (x : δ),
  (f.compContinuous g) x = f (g x)
-- Mathlib.Data.Sym.Sym2
Sym2.pmap_subtype_map_subtypeVal : ∀ {α : Type u_1} {P : α → Prop} (s : Sym2 α) (h : ∀ a ∈ s, P a), Sym2.map Subtype.val (Sym2.pmap Subtype.mk s h) = s
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.IsSplittingField.instFiniteDimensionalSplittingField : ∀ {K : Type v} [inst : Field K] (f : Polynomial K), FiniteDimensional K f.SplittingField
-- Mathlib.Topology.VectorBundle.Hom
hom_trivializationAt_target : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {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 : TopologicalSpace B] [inst_13 : (x : B) → TopologicalSpace (E₁ x)] [inst_14 : FiberBundle F₁ E₁]
  [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂]
  [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ] (x₀ : B),
  (trivializationAt (F₁ →SL[σ] F₂) (fun x => E₁ x →SL[σ] E₂ x) x₀).target =
    ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet) ×ˢ Set.univ
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instDefinable₂Pair : ZFSet.Definable₂ ZFSet.pair
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_add : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv]
  (f g : CauSeq β abv), f.lim + g.lim = (f + g).lim
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {𝔸 : Type u_5} [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸] (c : 𝔸) {f : 𝕜 → 𝔸},
        ContDiffWithinAt 𝕜 (↑n) f s x → iteratedDerivWithin n (fun z => c * f z) s x = c * iteratedDerivWithin n f s x
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage.congr_simp : ∀ {S : AlgebraicGeometry.Scheme} {Ω : Type u} [inst : Field Ω] [inst_1 : IsSepClosed Ω]
  (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) {s₀ : ↥S} (hs₀ : s default = s₀) {X : S.Etale}
  (t t_1 : (AlgebraicGeometry.Scheme.pointSmallEtale s).fiber.obj X),
  t = t_1 →
    AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage s hs₀ t =
      AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage s hs₀ t_1
-- Mathlib.Data.Fintype.Pi
/-- A dependent product of fintypes, indexed by a fintype, is a fintype.  -/
Pi.instFintype : {α : Type u_3} →
  {β : α → Type u_4} → [DecidableEq α] → [Fintype α] → [(a : α) → Fintype (β a)] → Fintype ((a : α) → β a)
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.add_of_omega0_le : ∀ {a b : Ordinal.{u}}, a < Ordinal.omega0 → Ordinal.omega0 ≤ b → a + b = b
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.Functor.toOrderHom_coe : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (F : CategoryTheory.Functor X Y) (a : X),
  F.toOrderHom a = F.obj a
-- Mathlib.CategoryTheory.Discrete.SumsProducts
/-- The discrete category on a product is equivalent to the product of the
discrete categories.  -/
CategoryTheory.Discrete.productEquiv : {J : Type u_1} →
  {K : Type u_2} → CategoryTheory.Discrete (J × K) ≌ CategoryTheory.Discrete J × CategoryTheory.Discrete K
-- Mathlib.Analysis.RCLike.Basic
RCLike.mul_re : ∀ {K : Type u_1} [inst : RCLike K] (z w : K), RCLike.re (z * w) = RCLike.re z * RCLike.re w - RCLike.im z * RCLike.im w
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.hasForgetToAddGroup.eq_1 : AddCommGrpCat.hasForgetToAddGroup =
  {
    forget₂ :=
      { obj := fun X => AddGrpCat.of ↑X, map := fun {X Y} f => AddGrpCat.ofHom (AddCommGrpCat.Hom.hom f),
        map_id := AddCommGrpCat.hasForgetToAddGroup._proof_1, map_comp := @AddCommGrpCat.hasForgetToAddGroup._proof_2 },
    forget_comp := AddCommGrpCat.hasForgetToAddGroup._proof_4 }
-- Mathlib.Analysis.RCLike.Basic
RCLike.continuous_conj : ∀ {K : Type u_1} [inst : RCLike K], Continuous ⇑(starRingEnd K)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_toPlus : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))), CategoryTheory.Presheaf.IsLocallySurjective J (J.toPlus P)
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.instAddCommGroup.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommGroup N],
  AddMonoidHom.instAddCommGroup =
    { toAddMonoid := AddMonoidHom.instAddCommMonoid.toAddMonoid, toNeg := AddMonoidHom.instNeg,
      toSub := AddMonoidHom.instSub, toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯,
      zsmul_neg' := ⋯, neg_add_cancel := ⋯, add_comm := ⋯ }
-- Lean.Expr
/-- Make an n-ary `And` application. `mkAndN []` returns `True`.  -/
Lean.mkAndN : List Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.instHasColimitsOfShapeOfHasColimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  [CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C], CategoryTheory.Limits.HasColimitsOfShape J C
-- Lean.Elab.SyntheticMVars
/-- We use this method to report typeclass (and coercion) resolution problems that are "stuck".
That is, there is nothing else to do, and we don't have enough information to synthesize them using TC resolution.
 -/
Lean.Elab.Term.reportStuckSyntheticMVar : Lean.MVarId → Lean.Elab.Term.SyntheticMVarDecl → optParam Bool false → Lean.Elab.TermElabM Unit
-- Mathlib.Data.Finsupp.BigOperators
Finset.support_sum_eq : ∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] (s : Finset (ι →₀ M)),
  (↑s).PairwiseDisjoint Finsupp.support → (s.sum id).support = s.sup Finsupp.support
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getKey!_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Inhabited α] [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∪ t₂).get! k = t₂.get! k
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
_private.Mathlib.AlgebraicGeometry.Morphisms.FlatRank.0.AlgebraicGeometry.Scheme.Hom.finrank_eq_of_isAffine : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [inst : AlgebraicGeometry.IsAffine S] [AlgebraicGeometry.Flat f]
  [AlgebraicGeometry.IsFinite f] (s : ↥S),
  AlgebraicGeometry.Scheme.Hom.finrank f s = AlgebraicGeometry.IsAffine.finrank✝ f s
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The completion of a module with respect to an ideal.

This is Hausdorff but not necessarily complete: a classical sufficient condition for
completeness is that `I` be finitely generated [Stacks, 05GG].  -/
AdicCompletion : {R : Type u_1} → [inst : CommRing R] → Ideal R → (M : Type u_4) → [inst_1 : AddCommGroup M] → [Module R M] → Type u_4
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `F ⊣ G` and a `CommShift` structure on `F`, these are the candidate
`CommShift.iso a` isomorphisms for a compatible `CommShift` structure on `G`.
 -/
CategoryTheory.Adjunction.RightAdjointCommShift.iso : {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] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {A : Type u_3} →
                [inst_2 : AddGroup A] →
                  [inst_3 : CategoryTheory.HasShift C A] →
                    [inst_4 : CategoryTheory.HasShift D A] →
                      (a : A) →
                        [F.CommShift A] →
                          (CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a)
-- Mathlib.Algebra.Module.FinitePresentation
Module.finitePresentation_of_surjective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [h : Module.FinitePresentation R M] (l : M →ₗ[R] N),
  Function.Surjective ⇑l → l.ker.FG → Module.FinitePresentation R N
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.rightHom_map : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (equiv : S.Equiv S') (e : E), S'.rightHom (equiv e) = S.rightHom e
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_pos_iff : ∀ {n : ℕ}, 0 < ArithmeticFunction.vonMangoldt n ↔ IsPrimePow n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.event : Lean.Lsp.SemanticTokenType
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.small : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M}, Manifold.IsSubmersionAtOfComplement F I J n f x → Small.{u, u_5} F
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAt.differentiableAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F}, HasGradientAt f f' x → DifferentiableAt 𝕜 f x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} {l : List α} {k : α} {fallback : Unit},
  (t.insertManyIfNewUnit l).getD k fallback = ()
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instAddAction.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  LowerSet.instAddAction = Function.Injective.addAction SetLike.coe ⋯ ⋯
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.modEq_neg`. -/
AddCommGroup.ModEq.of_neg' : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, a ≡ b [PMOD -p] → a ≡ b [PMOD p]
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.norm_toL1_eq_lintegral_norm : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β) (hf : MeasureTheory.Integrable f μ),
  ‖MeasureTheory.Integrable.toL1 f hf‖ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
-- Init.Notation
/-- `a <<< b` computes `a` shifted to the left by `b` places.
The meaning of this notation is type-dependent.
* On `Nat`, this is equivalent to `a * 2 ^ b`.
* On `UInt8` and other fixed width unsigned types, this is the same but
  truncated to the bit width. 

Conventions for notations in identifiers:

 * The recommended spelling of `<<<` in identifiers is `shiftLeft`. -/
«term_<<<_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Category.CompHausLike.Cartesian
/-- When the predicate `P` is preserved under taking type-theoretic products and `PUnit` satisfies it,
then `CompHausLike P` is a cartesian monoidal category.

This could be an instance but that causes some slowness issues with typeclass search, therefore we
keep it as a def and turn it on as an instance for the explicit examples of `CompHausLike` as
needed.
 -/
CompHausLike.cartesianMonoidalCategory : {P : TopCat → Prop} →
  [∀ (X Y : CompHausLike P), CompHausLike.HasProp P (↑X.toTop × ↑Y.toTop)] →
    [CompHausLike.HasProp P PUnit.{u + 1}] → CategoryTheory.CartesianMonoidalCategory (CompHausLike P)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.IsDiscrete.has_maximal_element : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : ValuativeRel R} [self : ValuativeRel.IsDiscrete R],
  ∃ γ < 1, ∀ δ < 1, δ ≤ γ
-- Init.Data.Option.Lemmas
Option.comp_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} (h : β → γ) (g : α → β) (x : Option α),
  Option.map (h ∘ g) x = Option.map h (Option.map g x)
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.instIsStableUnderRetractsInverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) (P : CategoryTheory.MorphismProperty D) [P.IsStableUnderRetracts],
  (P.inverseImage F).IsStableUnderRetracts
-- Mathlib.Data.Stream.Init
Stream'.mem_of_get_eq : ∀ {α : Type u} {n : ℕ} {s : Stream' α} {a : α}, a = s.get n → a ∈ s
-- Mathlib.Algebra.CharP.Defs
/-- The characteristic is zero if the exponential characteristic is one.  -/
charZero_of_expChar_one' : ∀ (R : Type u_1) [inst : NonAssocSemiring R] [Nontrivial R] [hq : ExpChar R 1], CharZero R
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_eq_maxKeyD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t.maxKey! = t.maxKeyD default
-- Std.Http.Data.Headers.Basic
Std.Http.Header.mk : {α : Type} → (Std.Http.Header.Value → Option α) → (α → Std.Http.Header.Name × Std.Http.Header.Value) → Std.Http.Header α
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- $aba$ is a vector.  -/
CliffordAlgebra.ι_mul_ι_mul_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a b : M),
  (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a =
    (CliffordAlgebra.ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
CategoryTheory.comonEquiv_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.comonEquiv.counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl (((CategoryTheory.cartesianComon C).comp (CategoryTheory.Comon.forget C)).obj x))
      ⋯
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.congr_fun : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} {f g : 𝒜 →+*ᵍ ℬ}, f = g → ∀ (x : A), f x = g x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.sinPartialHomeomorph.eq_1 : Real.sinPartialHomeomorph =
  { toFun := Real.sin, invFun := Real.arcsin, source := Set.Ioo (-(Real.pi / 2)) (Real.pi / 2),
    target := Set.Ioo (-1) 1, map_source' := Real.sinPartialHomeomorph._proof_2,
    map_target' := Real.sinPartialHomeomorph._proof_3, left_inv' := Real.sinPartialHomeomorph._proof_4,
    right_inv' := Real.sinPartialHomeomorph._proof_5, continuousOn_toFun := Real.sinPartialHomeomorph._proof_6,
    continuousOn_invFun := Real.sinPartialHomeomorph._proof_7, open_source := Real.sinPartialHomeomorph._proof_8,
    open_target := Real.sinPartialHomeomorph._proof_9 }
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPFVarsAnonymous : Lean.Options → Bool
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- An absolute left Kan extension is a Kan extension that commutes with any 1-morphism.  -/
CategoryTheory.Bicategory.LeftExtension.IsAbsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : a ⟶ b} → {g : a ⟶ c} → CategoryTheory.Bicategory.LeftExtension f g → Type (max (max u v) w)
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R], Polynomial.content 1 = 1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.id_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.id h).φK = CategoryTheory.CategoryStruct.id h.K
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.disjoint_countablePartition : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] {n : ℕ} {s t : Set α},
  s ∈ MeasurableSpace.countablePartition α n → t ∈ MeasurableSpace.countablePartition α n → s ≠ t → Disjoint s t