mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Submersion
/-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.
Additionally, we demand that `f` map `φ.source` into `ψ.source`.

NB. We don't know the particular atlasses used for `M` and `N`, so asking for `φ` and `ψ` to be
in the `atlas` would be too optimistic: lying in the `maximalAtlas` is sufficient.

Implicit in this definition is an abstract choice `F` of a complement of `E''` in `E`: being
a submersion at `x` includes a choice of linear isomorphism between `E` and `E'' × F`, which is
where the choice of `F` enters.
If you need stronger control over the complement `F`, use `IsSubmersionAtOfComplement` instead.
 -/
Manifold.IsSubmersionAt : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {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 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 E'' G →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst : TopologicalSpace M] →
                                  [ChartedSpace H M] →
                                    [inst : TopologicalSpace N] → [ChartedSpace G N] → WithTop ℕ∞ → (M → N) → M → Prop
-- Mathlib.Order.Interval.Finset.Basic
Finset.card_Ico_eq_card_Icc_sub_one : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  (Finset.Ico a b).card = (Finset.Icc a b).card - 1
-- Mathlib.Analysis.Normed.Group.Constructions
nnnorm_ofAdd : ∀ {E : Type u_2} [inst : NNNorm E] (x : E), ‖Multiplicative.ofAdd x‖₊ = ‖x‖₊
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.mk.sizeOf_spec : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [inst_2 : SizeOf ι] [inst_3 : SizeOf V]
  (X : ι → V) (d : (i j : ι) → X i ⟶ X j)
  (shape : autoParam (∀ (i j : ι), ¬c.Rel i j → d i j = 0) HomologicalComplex.shape._autoParam)
  (d_comp_d' :
    autoParam (∀ (i j k : ι), c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (d i j) (d j k) = 0)
      HomologicalComplex.d_comp_d'._autoParam),
  sizeOf { X := X, d := d, shape := shape, d_comp_d' := d_comp_d' } = 1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {a k : α} {v : β k}, (m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a
-- Mathlib.Control.Functor
/-- If we consider `x : F α` to, in some sense, contain values of type `α`,
predicate `Liftp p x` holds iff every value contained by `x` satisfies `p`.  -/
Functor.Liftp : {F : Type u → Type v} → [Functor F] → {α : Type u} → (α → Prop) → F α → Prop
-- Mathlib.Topology.Order.LeftRightLim
mapClusterPt_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] (f : α → β) (a : α), MapClusterPt (Function.rightLim f a) (nhdsWithin a (Set.Ici a)) f
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticRelatedInformation.message : Lean.Lsp.DiagnosticRelatedInformation → String
-- Mathlib.MeasureTheory.Function.LpSeminorm.Count
MeasureTheory.eLpNorm_count_lt_top_of_lt : ∀ {α : Type u_1} {ε : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε]
  {f : α → ε} {p : ENNReal} [Finite α],
  (∀ (i : α), ‖f i‖ₑ < ⊤) → MeasureTheory.eLpNorm f p MeasureTheory.Measure.count < ⊤
-- Mathlib.Order.SuccPred.Relation
/-- For `n < m`, `(n, m)` is in the transitive closure of a relation `~` for `n ≠ m` if `pred i ~ i`
for all `i` between `n` and `m`.  -/
transGen_of_pred_of_lt : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → n < m → Relation.TransGen r n m
-- Mathlib.RingTheory.Morita.Matrix
ModuleCat.matrixEquivalence_functor : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι),
  (ModuleCat.matrixEquivalence R i).functor = ModuleCat.toMatrixModCat R ι
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_smul_real_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E) (r : ℝ), inner 𝕜 (↑r • x) y = r • inner 𝕜 x y
-- Mathlib.Data.Finset.SymmDiff
Finset.symmDiff_def : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), symmDiff s t = s \ t ∪ t \ s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_le_min!_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, t.erase k ≠ ∅ → (cmp t.min! (t.erase k).min!).isLE = true
-- Mathlib.Order.ConditionallyCompleteLattice.Group
ciSup_mul_ciSup_le : ∀ {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [inst : ConditionallyCompleteLattice α]
  [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] {a : α} {g : ι → α} {h : ι' → α},
  (∀ (i : ι) (j : ι'), g i * h j ≤ a) → iSup g * iSup h ≤ a
-- Mathlib.Topology.Separation.Basic
Filter.coclosedCompact_le_cofinite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R0Space X], Filter.coclosedCompact X ≤ Filter.cofinite
-- Mathlib.Algebra.Star.Module
StarModule.decomposeProdAdjoint_symm_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] (a : ↥(selfAdjoint A) × ↥(skewAdjoint A)),
  (StarModule.decomposeProdAdjoint R A).symm a =
    (selfAdjoint.submodule R A).subtype a.1 + (skewAdjoint.submodule R A).subtype a.2
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3}
  {E : Type u_4} [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8}
  [inst_9 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_10 : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)]
  [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE]
  [inst_11 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_12 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)]
  [inst_13 :
    CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)]
  [inst_14 :
    CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)]
  [inst_15 : (CategoryTheory.forget D).ReflectsIsomorphisms] [inst_16 : (CategoryTheory.forget E).ReflectsIsomorphisms]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.IsIso
    ((CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D)
          (CategoryTheory.plusPlusAdjunction J E)).app
      P)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedAtomIso.default : Mathlib.Tactic.BicategoryLike.AtomIso
-- Mathlib.Algebra.Group.Action.Sum
Sum.vadd_def : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β] (a : M) (x : α ⊕ β),
  a +ᵥ x = Sum.map (fun x => a +ᵥ x) (fun x => a +ᵥ x) x
-- Mathlib.Algebra.Homology.Homotopy
/-- Variant of `nullHomotopicMap` where the input consists only of the
relevant maps `C_i ⟶ D_j` such that `c.Rel j i`.  -/
Homotopy.nullHomotopicMap' : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → ((i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) → (C ⟶ D)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.isEmbedding_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α], Topology.IsEmbedding fun x => {x}
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The supremum of a collection of sieves: the union of them all.  -/
CategoryTheory.Sieve.sup : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → Set (CategoryTheory.Sieve X) → CategoryTheory.Sieve X
-- Mathlib.Control.Traversable.Instances
Option.traverse.eq_1 : ∀ {F : Type u → Type v} [inst : Applicative F] {α : Type u_1} {β : Type u} (f : α → F β),
  Option.traverse f = Option.mapA f
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.instHasProdOfCompleteSpaceOfIsFiniteMeasureVariation : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G]
  [MeasureTheory.IsFiniteMeasure μ.variation], μ.HasProd ν B
-- Mathlib.RingTheory.AdjoinRoot
/-- `AdjoinRoot.map` as a `RingEquiv`.  -/
AdjoinRoot.mapRingEquiv : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R ≃+* S) →
          (p : Polynomial R) → (q : Polynomial S) → Associated (Polynomial.map (↑f) p) q → AdjoinRoot p ≃+* AdjoinRoot q
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₁ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ)
  (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).inv.app X).hom₁ =
    (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₁
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.dropLast.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) →
      (Unit → motive []) →
        ((head : α) → motive [head]) → ((a : α) → (as : List α) → (as = [] → False) → motive (a :: as)) → motive x
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.refl_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Equivalence.refl.functor = CategoryTheory.Functor.id C
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} {f : RatFunc K} [Valuation.IsTrivialOn K v],
  1 < v RatFunc.X → f ≠ 0 → v f = v RatFunc.X ^ f.intDegree
-- Init.Data.SInt.Bitwise
Int8.neg_one_shiftLeft_and_shiftLeft : ∀ {a b : Int8}, (-1) <<< b &&& a <<< b = a <<< b
-- Mathlib.Order.Filter.AtTopBot.Monoid
/-- In an ordered multiplicative monoid, if `f` and `g` tend to `+∞`, then so does `f * g`.

Earlier, this name was used for a similar lemma about semirings,
which is now called `Filter.Tendsto.atTop_mul_atTop₀`.  -/
Filter.Tendsto.atTop_mul_atTop : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instGroupCoeOfSubgroupClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Group (R i)] →
              [∀ (i : ι), SubgroupClass (S i) (R i)] → Group (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.Hom.toImage_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : ↑Y.affineOpens),
  AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Scheme.Hom.toImage f)
      ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.imageι f).base).obj ↑U) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Hom.ker f).subschemeObjIso U).hom
      (CommRingCat.ofHom
        (Ideal.Quotient.lift ((AlgebraicGeometry.Scheme.Hom.ker f).ideal U)
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f ↑U)) ⋯))
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale_map : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (φ : R →+* S) (r : R)
  (f : PowerSeries R),
  (PowerSeries.rescale (φ r)) ((PowerSeries.map φ) f) = (PowerSeries.map φ) ((PowerSeries.rescale r) f)
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `C ≤ f'`, then `f` grows at least as fast
as `C * x`, i.e., `C * (y - x) ≤ f y - f x` whenever `x ≤ y`.  -/
mul_sub_le_image_sub_of_le_deriv : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → ∀ {C : ℝ}, (∀ (x : ℝ), C ≤ deriv f x) → ∀ ⦃x y : ℝ⦄, x ≤ y → C * (y - x) ≤ f y - f x
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.mk : {numVarsSucc : ℕ} →
  (clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc)) →
    autoParam (∀ (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc), (l, true) ∉ clause ∨ (l, false) ∉ clause)
        Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodupkey._autoParam →
      autoParam (List.Nodup clause) Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodup._autoParam →
        Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- A bilinear map gives a quadratic map by applying the argument twice.  -/
LinearMap.BilinMap.toQuadraticMap : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → LinearMap.BilinMap R M N → QuadraticMap R M N
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.onBoundedFormula.eq_2 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (g : L →ᴸ L') (x : ℕ) (t₁ t₂ : L.Term (α ⊕ Fin x)),
  g.onBoundedFormula (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = (g.onTerm t₁).bdEqual (g.onTerm t₂)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.size_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.Equiv t₂ → t₁.size = t₂.size
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instStarModuleSubtypePreLpMemAddSubgroup : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : (i : α) → StarAddMonoid (E i)] [inst_2 : ∀ (i : α), NormedStarGroup (E i)] [inst_3 : Star 𝕜]
  [inst_4 : NormedRing 𝕜] [inst_5 : (i : α) → Module 𝕜 (E i)] [inst_6 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)]
  [∀ (i : α), StarModule 𝕜 (E i)], StarModule 𝕜 ↥(lp E p)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.Const.insertMany : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)]
  {m : Std.DHashMap.Raw α fun x => β} {l : ρ}, m.WF → (Std.DHashMap.Raw.Const.insertMany m l).WF
-- Init.Data.List.Sublist
List.IsInfix.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.Sublist l₂
-- Mathlib.Data.Set.Lattice
Set.sigmaToiUnion_bijective : ∀ {α : Type u_1} {β : Type u_2} (t : α → Set β),
  Pairwise (Function.onFun Disjoint t) → Function.Bijective (Set.sigmaToiUnion t)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.involutive_invert : ∀ {R : Type u_3} [inst : CommSemiring R], Function.Involutive ⇑LaurentPolynomial.invert
-- Init.Control.Lawful.Instances
OptionT.run.eq_1 : ∀ {m : Type u → Type v} {α : Type u} (x : OptionT m α), x.run = x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂)[k] = t₁[k]
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.box.congr_simp : ∀ {ι : Type u_1} (n n_1 : ℕ) (e_n : n = n_1) [inst : NeZero n] (ν ν_1 : ι → ℤ),
  ν = ν_1 → BoxIntegral.unitPartition.box n ν = BoxIntegral.unitPartition.box n_1 ν_1
-- Init.Data.BitVec.Lemmas
BitVec.not_ofBool : ∀ {b : Bool}, ~~~BitVec.ofBool b = BitVec.ofBool !b
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_toSubmodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L),
  ↑L'.toSubmodule = ↑L'
-- Mathlib.Algebra.Lie.AdjointAction.Basic
/-- Commuting elements have commuting adjoint actions.  -/
LieAlgebra.commute_ad_of_commute : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a b : A},
  Commute a b → Commute ((LieAlgebra.ad R A) a) ((LieAlgebra.ad R A) b)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α} {v : β}, (m.insert k v).getKey! k = k
-- Mathlib.Analysis.Fourier.AddCircle
/-- **Alias** of the forward direction of `MeasureTheory.memLp_haarAddCircle_iff`. -/
MeasureTheory.MemLp.of_haarAddCircle : ∀ {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal},
  MeasureTheory.MemLp f p AddCircle.haarAddCircle → MeasureTheory.MemLp f p MeasureTheory.volume
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).op =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Opposite.op X)).symm
-- Mathlib.Topology.Constructions
Pi.continuous_domRestrict_apply : ∀ {X : Type u} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] (s : Set X) {f : X → Z},
  Continuous f → Continuous (s.domRestrict f)
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instInfClosedSubgroup : (G : Type u) → [inst : Group G] → [inst_1 : TopologicalSpace G] → Min (ClosedSubgroup G)
-- Mathlib.FieldTheory.IntermediateField.Algebraic
mem_subalgebraEquivIntermediateField : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Algebra.IsAlgebraic K L] {S : Subalgebra K L} {x : L}, x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S
-- Mathlib.SetTheory.Cardinal.Finite
Cardinal.natCast_le_toENat_iff : ∀ {n : ℕ} {c : Cardinal.{u_3}}, ↑n ≤ Cardinal.toENat c ↔ ↑n ≤ c
-- Init.Control.Lawful.Instances
OptionT.run_bind_lift : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : m α) (f : α → OptionT m β),
  (OptionT.lift x >>= f).run = do
    let a ← x
    (f a).run
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.neg : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α],
  Function.Periodic f c → Function.Periodic f (-c)
-- Mathlib.InformationTheory.Hamming
Hamming.instNormedAddGroupOfAddGroup : {ι : Type u_2} →
  {β : ι → Type u_3} →
    [Fintype ι] → [(i : ι) → DecidableEq (β i)] → [(i : ι) → AddGroup (β i)] → NormedAddGroup (Hamming β)
-- Mathlib.CategoryTheory.Limits.IsConnected
CategoryTheory.isConnected_of_hasInitial : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasInitial C],
  CategoryTheory.IsConnected C
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.mk.sizeOf_spec : ∀ {α σ : Type} [inst : SizeOf α] [inst_1 : SizeOf σ]
  (name : autoParam Lean.Name Lean.SimplePersistentEnvExtensionDescr.name._autoParam) (addEntryFn : σ → α → σ)
  (addImportedFn : Array (Array α) → σ) (toArrayFn : List α → Array α)
  (exportEntriesFnEx? : Option (Lean.Environment → σ → List α → Lean.OLeanEntries (Array α)))
  (asyncMode : Lean.EnvExtension.AsyncMode) (replay? : Option (List α → σ → σ → List α × σ)),
  sizeOf
      { name := name, addEntryFn := addEntryFn, addImportedFn := addImportedFn, toArrayFn := toArrayFn,
        exportEntriesFnEx? := exportEntriesFnEx?, asyncMode := asyncMode, replay? := replay? } =
    1 + sizeOf name + sizeOf exportEntriesFnEx? + sizeOf asyncMode + sizeOf replay?
-- Mathlib.GroupTheory.CoprodI
FreeGroup.freeGroupUnitEquivInt.eq_1 : FreeGroup.freeGroupUnitEquivInt =
  { toFun := fun x => ((FreeGroup.map fun x => 1) x).sum, invFun := fun x => FreeGroup.of () ^ x,
    left_inv := FreeGroup.freeGroupUnitEquivInt._proof_3, right_inv := FreeGroup.freeGroupUnitEquivInt._proof_1 }
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
/-- The (universal) derivation in `(KaehlerDifferential f).Derivation f`
when `f : A ⟶ B` is a morphism in the category `CommRingCat`.  -/
CommRingCat.KaehlerDifferential.D : {A B : CommRingCat} → (f : A ⟶ B) → (CommRingCat.KaehlerDifferential f).Derivation f
-- Init.Prelude
/-- Auxiliary unsafe constant used by the Compiler to mark unreachable code.

Like `lcProof`, this is an `unsafe axiom`, which means that even though it is
not sound, the kernel will not let us use it for regular proofs.

Executing this expression to actually synthesize a value of type `α` causes
**immediate undefined behavior**, and the compiler does take advantage of this
to optimize the code assuming that it is not called. If it is not optimized out,
it is likely to appear as a print message saying "unreachable code", but this
behavior is not guaranteed or stable in any way.
 -/
lcUnreachable : {α : Sort u} → α