mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- A structure containing information on the way a space `H` embeds in a
model vector space `E` over the field `𝕜`. This is all that is needed to
define a `C^n` manifold with model space `H`, and model vector space `E`.

We require that, when the field is `ℝ` or `ℂ`, the range is `ℝ`-convex, as this is what is needed
to do calculus and covers the standard examples of manifolds with boundary. Over other fields,
we require that the range is `univ`, as there is no relevant notion of manifold with boundary there.
 -/
ModelWithCorners : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_2) →
      [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (H : Type u_3) → [TopologicalSpace H] → Type (max u_2 u_3)
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesSummable.smul : ∀ {f : ℕ → ℂ} (c : ℂ) {s : ℂ}, LSeriesSummable f s → LSeriesSummable (c • f) s
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.frequently_le_exp : ∀ {u : ℕ → ENNReal} {a : EReal}, ExpGrowth.expGrowthInf u < a → ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ (a * ↑n).exp
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesFiniteLimits.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  autoParam
      (∀ (J : Type) [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
        CategoryTheory.Limits.PreservesLimitsOfShape J F)
      CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits._autoParam →
    CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
/-- [Stacks Tag 01TB](https://stacks.math.columbia.edu/tag/01TB) ((1) => (3)) -/
AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [JacobsonSpace ↥Y] [AlgebraicGeometry.LocallyOfFiniteType f],
  closedPoints ↥X ⊆ ⇑f ⁻¹' closedPoints ↥Y
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanIsKan_desc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] (s : CategoryTheory.Bicategory.LeftExtension f g),
  (CategoryTheory.Bicategory.lanIsKan f g).desc s = CategoryTheory.Bicategory.lanDesc s
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A function to 𝕜 is meromorphic in normal form on `U` iff its inverse is.
 -/
meromorphicNFOn_fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜},
  MeromorphicNFOn (fun x => (f x)⁻¹) U ↔ MeromorphicNFOn f U
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instSubsemiringClass : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  SubsemiringClass (Subalgebra R A) A
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_comp_neg_id : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜),
  (FormalMultilinearSeries.ofScalars E c).compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 E) =
    FormalMultilinearSeries.ofScalars E fun k => (-1) ^ k * c k
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₁.eq_2 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0) (one : P.X 2 ⟶ Q.X 1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f''),
  Homotopy.mkCoinductiveAux₁ e zero one comm_one succ 1 = ⟨one, ⟨(succ 0 ⟨zero, ⟨one, comm_one⟩⟩).fst, ⋯⟩⟩
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.countable_self_fgequiv_of_countable : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] [Countable M], Countable (L.FGEquiv M M)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instInhabitedRefIdent : Inhabited Lean.Lsp.RefIdent
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist_bot : ∀ {V : Type u_1} {u v : V}, ⊥.dist u v = 0
-- Mathlib.Order.BoundedOrder.Lattice
min_bot_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderBot α] (a : α), min a ⊥ = ⊥
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.mk.inj : ∀ {ref declId : Lean.Syntax} {modifiers : Lean.Elab.Modifiers} {isClass allowIndices allowSortPolymorphism : Bool}
  {shortDeclName declName : Lean.Name} {levelNames : List Lean.Name} {binders : Lean.Syntax}
  {type? : Option Lean.Syntax} {ctors : Array Lean.Elab.Command.CtorView}
  {computedFields : Array Lean.Elab.Command.ComputedFieldView} {derivingClasses : Array Lean.Elab.DerivingClassView}
  {docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)} {isCoinductive : Bool}
  {ref_1 declId_1 : Lean.Syntax} {modifiers_1 : Lean.Elab.Modifiers}
  {isClass_1 allowIndices_1 allowSortPolymorphism_1 : Bool} {shortDeclName_1 declName_1 : Lean.Name}
  {levelNames_1 : List Lean.Name} {binders_1 : Lean.Syntax} {type?_1 : Option Lean.Syntax}
  {ctors_1 : Array Lean.Elab.Command.CtorView} {computedFields_1 : Array Lean.Elab.Command.ComputedFieldView}
  {derivingClasses_1 : Array Lean.Elab.DerivingClassView}
  {docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)} {isCoinductive_1 : Bool},
  { ref := ref, declId := declId, modifiers := modifiers, isClass := isClass, allowIndices := allowIndices,
        allowSortPolymorphism := allowSortPolymorphism, shortDeclName := shortDeclName, declName := declName,
        levelNames := levelNames, binders := binders, type? := type?, ctors := ctors, computedFields := computedFields,
        derivingClasses := derivingClasses, docString? := docString?, isCoinductive := isCoinductive } =
      { ref := ref_1, declId := declId_1, modifiers := modifiers_1, isClass := isClass_1,
        allowIndices := allowIndices_1, allowSortPolymorphism := allowSortPolymorphism_1,
        shortDeclName := shortDeclName_1, declName := declName_1, levelNames := levelNames_1, binders := binders_1,
        type? := type?_1, ctors := ctors_1, computedFields := computedFields_1, derivingClasses := derivingClasses_1,
        docString? := docString?_1, isCoinductive := isCoinductive_1 } →
    ref = ref_1 ∧
      declId = declId_1 ∧
        modifiers = modifiers_1 ∧
          isClass = isClass_1 ∧
            allowIndices = allowIndices_1 ∧
              allowSortPolymorphism = allowSortPolymorphism_1 ∧
                shortDeclName = shortDeclName_1 ∧
                  declName = declName_1 ∧
                    levelNames = levelNames_1 ∧
                      binders = binders_1 ∧
                        type? = type?_1 ∧
                          ctors = ctors_1 ∧
                            computedFields = computedFields_1 ∧
                              derivingClasses = derivingClasses_1 ∧
                                docString? = docString?_1 ∧ isCoinductive = isCoinductive_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_union_of_contains_eq_false_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        m₁.contains k = false →
          Std.DHashMap.Internal.Raw₀.Const.getD (m₁.union m₂) k fallback =
            Std.DHashMap.Internal.Raw₀.Const.getD m₂ k fallback
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, List.find? (fun x => cmp x.fst k == Ordering.eq) t.toList = none ↔ k ∉ t
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.limplies_unsat : ∀ {α : Type u} {σ1 : Type v} {σ2 : Type w} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2),
  Std.Tactic.BVDecide.LRAT.Internal.Limplies α f2 f1 →
    Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f1 → Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f2
-- Batteries.Data.Array.Basic
/-- Find the first minimal element of an array. If the array is empty, `d` is
returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered.
 -/
Array.minD : {α : Type u_1} → [ord : Ord α] → (xs : Array α) → α → optParam ℕ 0 → optParam ℕ xs.size → α
-- Mathlib.RingTheory.Extension.Basic
/-- `Cotangent.val` as a linear isomorphism.  -/
Algebra.Extension.cotangentEquivCotangentKer : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → {P : Algebra.Extension R S} → P.Cotangent ≃ₗ[P.Ring] P.ker.Cotangent
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The range of the inclusion map is equal to the kernel of the projection map.  -/
GroupExtension.range_inl_eq_ker_rightHom : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (self : GroupExtension N E G), self.inl.range = self.rightHom.ker
-- Mathlib.Algebra.Lie.Basic
LieHom.instLinearMapClass : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], LinearMapClass (L₁ →ₗ⁅R⁆ L₂) R L₁ L₂
-- Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
/-- **Dominated convergence theorem** for nonnegative `AEMeasurable` functions.  -/
MeasureTheory.tendsto_lintegral_of_dominated_convergence' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal}
  (bound : α → ENNReal),
  (∀ (n : ℕ), AEMeasurable (F n) μ) →
    (∀ (n : ℕ), F n ≤ᵐ[μ] bound) →
      ∫⁻ (a : α), bound a ∂μ ≠ ⊤ →
        (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
          Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
  (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getKey a l h = Std.Internal.List.getKeyD a l fallback
-- Init.Data.SInt.Basic
instShiftLeftInt16 : ShiftLeft Int16
-- Aesop.Tree.Check
Aesop.MVarClusterRef.checkIntroducedMVars : Aesop.MVarClusterRef → Lean.Meta.SavedState → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeId_hom_app_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} (X : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.Cone.postcomposeId.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.Algebra.Star.Unitary
unitarySubgroup_toSubmonoid : ∀ {G : Type u_2} [inst : Group G] [inst_1 : StarMul G], (unitarySubgroup G).toSubmonoid = unitary G
-- Lean.Server.References
Lean.Server.TransientWorkerILean.mk.inj : ∀ {moduleUri : Lean.Lsp.DocumentUri} {version : ℕ} {directImports : Lean.Server.DirectImports}
  {isSetupFailure? : Option Bool} {refs : Lean.Lsp.ModuleRefs} {decls : Lean.Lsp.Decls}
  {moduleUri_1 : Lean.Lsp.DocumentUri} {version_1 : ℕ} {directImports_1 : Lean.Server.DirectImports}
  {isSetupFailure?_1 : Option Bool} {refs_1 : Lean.Lsp.ModuleRefs} {decls_1 : Lean.Lsp.Decls},
  { moduleUri := moduleUri, version := version, directImports := directImports, isSetupFailure? := isSetupFailure?,
        refs := refs, decls := decls } =
      { moduleUri := moduleUri_1, version := version_1, directImports := directImports_1,
        isSetupFailure? := isSetupFailure?_1, refs := refs_1, decls := decls_1 } →
    moduleUri = moduleUri_1 ∧
      version = version_1 ∧
        directImports = directImports_1 ∧ isSetupFailure? = isSetupFailure?_1 ∧ refs = refs_1 ∧ decls = decls_1
-- Lean.Elab.AssertExists
Lean.Elab.Command.AssertExists.mk.inj : ∀ {isDecl : Bool} {givenName modName : Lean.Name} {isDecl_1 : Bool} {givenName_1 modName_1 : Lean.Name},
  { isDecl := isDecl, givenName := givenName, modName := modName } =
      { isDecl := isDecl_1, givenName := givenName_1, modName := modName_1 } →
    isDecl = isDecl_1 ∧ givenName = givenName_1 ∧ modName = modName_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKey?_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).maxKey? = some k ↔
    (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.hom_ext' : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {Z : C} (g h : ⨁ f ⟶ Z),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) g =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) h) →
    g = h
-- Mathlib.Logic.Function.Basic
Function.Bijective.injective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → Function.Injective f
-- Mathlib.Algebra.Group.Finsupp
Finsupp.neg_apply : ∀ {ι : Type u_1} {G : Type u_6} [inst : NegZeroClass G] (g : ι →₀ G) (a : ι), (-g) a = -g a
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.σ_smul : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) (x y : S), P.σ x • y = x * y
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle.π_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] (j : J),
  (CategoryTheory.Pretriangulated.productTriangle.π T j).hom₂ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₂) j
-- Init.Notation
/-- Substring matching for `#guard_msgs`:
- `substring := true` checks that the docstring appears as a substring of the output.
- `substring := false` (the default) requires exact matching (modulo whitespace normalization).
 -/
Lean.guardMsgsSubstring : Lean.ParserDescr
-- Batteries.Data.MLList.Basic
/-- Run a lazy list in a `ReaderT` monad on some fixed state.  -/
MLList.runReader : {m : Type u → Type u} → {ρ α : Type u} → [Monad m] → MLList (ReaderT ρ m) α → ρ → MLList m α
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.neighborFinset_completeEquipartiteGraph : ∀ {r t : ℕ} (v : Fin r × Fin t), (SimpleGraph.completeEquipartiteGraph r t).neighborFinset v = {v.1}ᶜ ×ˢ Finset.univ
-- Mathlib.Data.Multiset.Basic
Multiset.choose_mem : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : Multiset α) (hp : ∃! a, a ∈ l ∧ p a),
  Multiset.choose p l hp ∈ l
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- Returns the smallest element of `α`, or none if `α` is empty.

Only empty types are allowed to define `least? := none`. If `α` is ordered and nonempty, then
the value of `least?` should be the smallest element according to the order on `α`.
 -/
Std.PRange.Least?.least? : {α : Type u} → [self : Std.PRange.Least? α] → Option α
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.instMonoidalOpFunctor : SSet.opFunctor.Monoidal
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- `SimplexCategoryGenRel.δ i` is the `i`-th face map `.mk n ⟶ .mk (n + 1)`.  -/
SimplexCategoryGenRel.δ : {n : ℕ} → Fin (n + 2) → (SimplexCategoryGenRel.mk n ⟶ SimplexCategoryGenRel.mk (n + 1))
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.coreS.sizeOf_spec : ∀ (a b : Lean.Expr) (sa sb : Lean.Meta.Grind.Arith.CommRing.SemiringExpr)
  (ra rb : Lean.Meta.Grind.Arith.CommRing.RingExpr),
  sizeOf (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.coreS a b sa sb ra rb) =
    1 + sizeOf a + sizeOf b + sizeOf sa + sizeOf sb + sizeOf ra + sizeOf rb
-- Init.Data.SInt.Lemmas
instAssociativeInt64HAdd : Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.map_mem_edgeSet_iff : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {e : Sym2 V},
  Sym2.map (⇑f) e ∈ G'.edgeSet ↔ e ∈ G.edgeSet
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_neg' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.neg.eq_1 : ∀ (G : Type v) [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G]
  [inst_3 : IsIsometricVAdd Gᵃᵒᵖ G], IsometryEquiv.neg G = { toEquiv := Equiv.neg G, isometry_toFun := ⋯ }
-- Init.Data.NeZero
neZero_zero_iff_false : ∀ {α : Type u_1} [inst : Zero α], NeZero 0 ↔ False
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_units_ne_zero : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]ˣ), (↑x).zmodRepr ≠ 0
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_min : ∀ {R : Type u} [inst : LinearOrder R] (x y : R), Tropical.trop (min x y) = Tropical.trop x + Tropical.trop y
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_functor_map_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : X ⟶ Y) (X_1 : C × D),
  (CategoryTheory.Functor.currying.functor.map T).app X_1 = (T.app X_1.1).app X_1.2
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.equivOfComm_apply : ∀ {H : Type u_1} [inst : CommGroup H] (a : H), Abelianization.equivOfComm a = Abelianization.of a
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_self_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i j : ι) [inst_3 : Decidable (i = j)], (b.repr (b i)) j = if i = j then 1 else 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k k' : α},
  m.getKey? k = some k' → (Std.HashMap.filterMap f m)[k]? = m[k]?.bind (f k')
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.insert! k v t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf =>
      Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l r =>
      match compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.balanceL! k' v' (Std.DTreeMap.Internal.Impl.insert! k v l) r
      | Ordering.gt => Std.DTreeMap.Internal.Impl.balanceR! k' v' l (Std.DTreeMap.Internal.Impl.insert! k v r)
      | Ordering.eq => Std.DTreeMap.Internal.Impl.inner sz k v l r
-- Mathlib.RingTheory.NoetherNormalization
/-- `T1 f 1` leads to an algebra equiv `T f`.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.T : {k : Type u_1} →
  [inst : Field k] →
    {n : ℕ} → MvPolynomial (Fin (n + 1)) k → MvPolynomial (Fin (n + 1)) k ≃ₐ[k] MvPolynomial (Fin (n + 1)) k
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.eq_liftOfRightInverse : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group G₃]
  (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker)
  (h : G₂ →* G₃), h.comp f = g → h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.MonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X M M).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.MonObj.mul)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id M))
          CategoryTheory.MonObj.mul)
        (CategoryTheory.CategoryStruct.id M))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.sumInvPow.eq_1 : ∀ (L : PeriodPair) (x : ℂ) (r : ℕ), L.sumInvPow x r = ∑' (l : ↥L.lattice), ((↑l - x) ^ r)⁻¹
-- Mathlib.Data.Multiset.FinsetOps
Multiset.length_ndinsert_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s → (Multiset.ndinsert a s).card = s.card
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivWithinAt_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (x : E) (s : Set E), HasFDerivWithinAt 0 0 s x
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Fact.mk.inj : ∀ {coeffs : Lean.Omega.Coeffs} {constraint : Lean.Omega.Constraint}
  {justification : Lean.Elab.Tactic.Omega.Justification constraint coeffs} {coeffs_1 : Lean.Omega.Coeffs}
  {constraint_1 : Lean.Omega.Constraint} {justification_1 : Lean.Elab.Tactic.Omega.Justification constraint_1 coeffs_1},
  { coeffs := coeffs, constraint := constraint, justification := justification } =
      { coeffs := coeffs_1, constraint := constraint_1, justification := justification_1 } →
    coeffs = coeffs_1 ∧ constraint = constraint_1 ∧ justification ≍ justification_1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toArray_toList : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α], r.toList.toArray = r.toArray
-- Mathlib.Data.Multiset.Defs
Multiset.mem_of_le : ∀ {α : Type u_1} {s t : Multiset α} {a : α}, s ≤ t → a ∈ s → a ∈ t