mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.comp_id : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N),
  f.comp (FirstOrder.Language.Hom.id L M) = f
-- Mathlib.Algebra.Quaternion
Quaternion.re_add : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R), (a + b).re = a.re + b.re
-- Mathlib.Tactic.Positivity.Core
/-- Extract a proof that `e` is nonnegative, if possible, from `Strictness` information about `e`.
 -/
Mathlib.Meta.Positivity.Strictness.toNonneg : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      {e : Q(«$α»)} →
        {pα : Q(PartialOrder «$α»)} → Mathlib.Meta.Positivity.Strictness zα e (some pα) → Option Q(0 ≤ «$e»)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.firstReturn_pos : ∀ {p : DyckWord}, p ≠ 0 → 0 < p.firstReturn
-- Mathlib.Topology.Algebra.Order.UpperLower
IsOrderedMonoid.to_hasUpperLowerClosure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : Preorder α] [IsOrderedMonoid α]
  [ContinuousConstSMul α α], HasUpperLowerClosure α
-- Mathlib.Topology.Algebra.Ring.Basic
DiscreteTopology.topologicalRing : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocRing R] [DiscreteTopology R],
  IsTopologicalRing R
-- Mathlib.Algebra.Tropical.BigOperators
Multiset.trop_inf : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : OrderTop R] (s : Multiset R),
  Tropical.trop s.inf = (Multiset.map Tropical.trop s).sum
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_prod_right : ∀ {α : Type u_1} {f : Equiv.Perm α} (l : List (Equiv.Perm α)), (∀ g ∈ l, f.Disjoint g) → f.Disjoint l.prod
-- Mathlib.FieldTheory.Galois.Basic
isGalois_iff_isGalois_top : ∀ {F : Type u_1} {E : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], IsGalois F ↥⊤ ↔ IsGalois F E
-- Lean.Parser.Term
Lean.Parser.Term.letId : Lean.Parser.Parser
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.coe_toLinearMap : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), ⇑f.toLinearMap = ⇑f
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.stripTags.go : {α : Type u_1} → String → Array (Lean.Widget.TaggedText α) → String
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.IterM.step_intermediateDropWhile.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : false = true → motive true) (h_2 : false = false → motive false),
  (match hP : false with
    | true => h_1 hP
    | false => h_2 hP) =
    h_2 ⋯
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instLinearOrderedCommGroupWithZeroValueGroup : {K : Type u_1} → [inst : Field K] → (A : ValuationSubring K) → LinearOrderedCommGroupWithZero A.ValueGroup
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
/-- **Markov's inequality**, also known as **Chebyshev's first inequality**.  -/
MeasureTheory.meas_ge_le_lintegral_div : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → ∀ {ε : ENNReal}, ε ≠ 0 → ε ≠ ⊤ → μ {x | ε ≤ f x} ≤ (∫⁻ (a : α), f a ∂μ) / ε
-- Init.Data.List.TakeDrop
Option.toList.eq_1 : ∀ {α : Type u_1}, none.toList = []
-- Mathlib.RingTheory.SimpleModule.Rank
isSimpleModule_iff_finrank_eq_one : ∀ {R : Type u_1} {M : Type u_2} [inst : DivisionRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsSimpleModule R M ↔ Module.finrank R M = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_of_not_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  ¬P ≈ Q → W'.add P Q = W'.addXYZ P Q
-- Mathlib.Data.Sym.Card
/-- For any fintype `α` of cardinality `n`, `card (Sym α k) = multichoose (card α) k`.  -/
Sym.card_sym_eq_multichoose : ∀ (α : Type u_2) (k : ℕ) [inst : Fintype α] [inst_1 : Fintype (Sym α k)],
  Fintype.card (Sym α k) = (Fintype.card α).multichoose k
-- Lean.Syntax
Lean.Syntax.instHashableRange.hash : Lean.Syntax.Range → UInt64
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
not_linearIndepOn_finset_iffₒₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : LinearOrder R] [CanonicallyOrderedAdd R] [AddRightReflectLE R] [IsCancelAdd M]
  [inst_7 : DecidableEq ι] {s : Finset ι},
  ¬LinearIndepOn R v ↑s ↔ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, 0 < f i
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_embDomain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ↪ β) (l : α →₀ M),
  Finsupp.comapDomain (⇑f) (Finsupp.embDomain f l) ⋯ = l
-- Mathlib.Data.Finmap
/-- `any f s` returns `true` iff there exists a value `v` in `s` such that `f v = true`.  -/
Finmap.any : {α : Type u} → {β : α → Type v} → ((x : α) → β x → Bool) → Finmap β → Bool
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Result.mk.injEq : ∀ (allConsts unfoldCandidates eqnCandidates : Lean.Meta.Try.Collector.OrdSet Lean.Name)
  (funIndCandidates : Lean.Meta.FunInd.SeenCalls) (indCandidates : Array Lean.Meta.Try.Collector.InductionCandidate)
  (libSearchResults : Lean.Meta.Try.Collector.OrdSet (Lean.Name × Lean.Meta.Grind.EMatchTheoremKind))
  (allConsts_1 unfoldCandidates_1 eqnCandidates_1 : Lean.Meta.Try.Collector.OrdSet Lean.Name)
  (funIndCandidates_1 : Lean.Meta.FunInd.SeenCalls) (indCandidates_1 : Array Lean.Meta.Try.Collector.InductionCandidate)
  (libSearchResults_1 : Lean.Meta.Try.Collector.OrdSet (Lean.Name × Lean.Meta.Grind.EMatchTheoremKind)),
  ({ allConsts := allConsts, unfoldCandidates := unfoldCandidates, eqnCandidates := eqnCandidates,
        funIndCandidates := funIndCandidates, indCandidates := indCandidates, libSearchResults := libSearchResults } =
      { allConsts := allConsts_1, unfoldCandidates := unfoldCandidates_1, eqnCandidates := eqnCandidates_1,
        funIndCandidates := funIndCandidates_1, indCandidates := indCandidates_1,
        libSearchResults := libSearchResults_1 }) =
    (allConsts = allConsts_1 ∧
      unfoldCandidates = unfoldCandidates_1 ∧
        eqnCandidates = eqnCandidates_1 ∧
          funIndCandidates = funIndCandidates_1 ∧
            indCandidates = indCandidates_1 ∧ libSearchResults = libSearchResults_1)
-- Std.Time.DateTime
/-- Creates a new `Timestamp` out of a `DateTime`.
 -/
Std.Time.DateTime.toTimestamp : Std.Time.DateTime → Std.Time.Timestamp
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- A `WeierstrassCurve` is in short normal form, if its `a₁, a₂, a₃ = 0`.
In other words it is `Y² = X³ + a₄X + a₆`.

This is the normal form of characteristic ≠ 2 or 3, and
also the normal form of characteristic = 3 and j = 0.  -/
WeierstrassCurve.IsShortNF : {R : Type u_1} → [CommRing R] → WeierstrassCurve R → Prop
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.mk.injEq : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁))
  (unit_whiskerRight_map :
    autoParam
      (∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁),
        CategoryTheory.CategoryStruct.comp (adj X₁).unit
            (CategoryTheory.Functor.whiskerRight (F.map f) (G.obj (Opposite.op X₁))) =
          CategoryTheory.CategoryStruct.comp (adj Y₁).unit ((F.obj Y₁).whiskerLeft (G.map f.op)))
      CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map._autoParam)
  (adj_1 : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁))
  (unit_whiskerRight_map_1 :
    autoParam
      (∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁),
        CategoryTheory.CategoryStruct.comp (adj_1 X₁).unit
            (CategoryTheory.Functor.whiskerRight (F.map f) (G.obj (Opposite.op X₁))) =
          CategoryTheory.CategoryStruct.comp (adj_1 Y₁).unit ((F.obj Y₁).whiskerLeft (G.map f.op)))
      CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map._autoParam),
  ({ adj := adj, unit_whiskerRight_map := unit_whiskerRight_map } =
      { adj := adj_1, unit_whiskerRight_map := unit_whiskerRight_map_1 }) =
    (adj = adj_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- `HasCokernels` represents the existence of cokernels for every morphism.  -/
CategoryTheory.Limits.HasCokernels : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_inter_add_sdiff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasurableSet t → μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s
-- Mathlib.FieldTheory.Separable
Algebra.isSeparable_def : ∀ (F : Type u_1) (K : Type u_3) [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K],
  Algebra.IsSeparable F K ↔ ∀ (x : K), IsSeparable F x
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (state : Std.Mutex (Std.CloseableChannel.Bounded.State✝ α)),
  sizeOf { state := state } = 1 + sizeOf state
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.Indep.coindep : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → M✶.Coindep I
-- Mathlib.Topology.Inseparable
SeparationQuotient.tendsto_lift₂_nhdsWithin : ∀ {X : Type u_1} {Y : Type u_2} {α : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y → α}
  {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d} {x : X} {y : Y}
  {s : Set (SeparationQuotient X × SeparationQuotient Y)} {l : Filter α},
  Filter.Tendsto (Function.uncurry (SeparationQuotient.lift₂ f hf))
      (nhdsWithin (SeparationQuotient.mk x, SeparationQuotient.mk y) s) l ↔
    Filter.Tendsto (Function.uncurry f) (nhdsWithin (x, y) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s))
      l
-- Mathlib.Algebra.Group.Units.Defs
Units.eq_one : ∀ {M : Type u_1} [inst : Monoid M] [Subsingleton Mˣ] (u : Mˣ), u = 1
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- The Bochner integral  -/
MeasureTheory.integral : {α : Type u_6} →
  {G : Type u_7} →
    [inst : NormedAddCommGroup G] → [NormedSpace ℝ G] → {x : MeasurableSpace α} → MeasureTheory.Measure α → (α → G) → G
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Limits.pairComp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (X Y : C) (F : CategoryTheory.Functor C D),
  CategoryTheory.Limits.pairComp X Y F = CategoryTheory.Limits.diagramIsoPair ((CategoryTheory.Limits.pair X Y).comp F)
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.slope_le_leftDeriv_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConvexOn ℝ S f → x ∈ S → y ∈ interior S → x < y → slope f x y ≤ derivWithin f (Set.Iio y) y
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
isSymmSndFDerivWithinAt_congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E} {f : E → F}
  {x : E}, s =ᶠ[nhds x] t → (IsSymmSndFDerivWithinAt 𝕜 f s x ↔ IsSymmSndFDerivWithinAt 𝕜 f t x)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_sigma_of_isSeparator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w}
  (f : β → C) [inst_2 : CategoryTheory.Limits.HasCoproduct f] (b : β),
  CategoryTheory.IsSeparator (f b) → CategoryTheory.IsSeparator (∐ f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.instSMulVariableChange : {R : Type u} → [inst : CommRing R] → SMul (WeierstrassCurve.VariableChange R) (WeierstrassCurve R)
-- Lean.Elab.Command
Lean.Elab.Command.ModuleLinter.mk.inj : ∀ {run : Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit}
  {name : autoParam Lean.Name Lean.Elab.Command.ModuleLinter.name._autoParam}
  {run_1 : Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit}
  {name_1 : autoParam Lean.Name Lean.Elab.Command.ModuleLinter.name._autoParam},
  { run := run, name := name } = { run := run_1, name := name_1 } → run = run_1 ∧ name = name_1
-- Mathlib.Order.Category.BoolAlg
/-- Construct a bundled `BoolAlg` from the underlying type and typeclass.  -/
BoolAlg.of : (carrier : Type u_1) → [str : BooleanAlgebra carrier] → BoolAlg
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Path.extend.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y),
  γ.extend = { toFun := Set.IccExtend Path.extend._proof_2 ⇑γ, continuous_toFun := ⋯ }
-- Mathlib.Tactic.LinearCombination
Mathlib.Tactic.LinearCombination.Expanded.proof.injEq : ∀ (rel : Mathlib.Ineq) (pf : Lean.Term) (rel_1 : Mathlib.Ineq) (pf_1 : Lean.Term),
  (Mathlib.Tactic.LinearCombination.Expanded.proof rel pf =
      Mathlib.Tactic.LinearCombination.Expanded.proof rel_1 pf_1) =
    (rel = rel_1 ∧ pf = pf_1)
-- Init.Data.SInt.Basic
/-- Converts a 64-bit signed integer to an 8-bit signed integer by truncating its bitvector
representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.toInt8 : Int64 → Int8
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.blast : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.BinaryRefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.essentiallySmall_of_small_of_locallySmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [Small.{w, u} C] [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.EssentiallySmall.{w, v, u} C
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.State.symbols : Lean.Meta.Grind.NormalizePattern.State → Array Lean.HeadIndex
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.zero_smul : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : Zero M] [inst_3 : Zero X] [inst_4 : SMulWithZero M X] [ContinuousSMul M X] {f : α → M} {g : α → X}
  {l : Filter α} {a : X},
  Filter.Tendsto f l (nhds 0) → Filter.Tendsto g l (nhds a) → Filter.Tendsto (fun x => f x • g x) l (nhds 0)
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.toEquiv_injective : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N], Function.Injective LieModuleEquiv.toEquiv
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- `GL(2, ℝ)` acts transitively on the upper half-plane.  -/
UpperHalfPlane.isPretransitiveGL2R : MulAction.IsPretransitive (GL (Fin 2) ℝ) UpperHalfPlane
-- Mathlib.Data.Set.Image
Set.range_nonempty : ∀ {α : Type u_1} {ι : Sort u_4} [h : Nonempty ι] (f : ι → α), (Set.range f).Nonempty
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- Coalgebra equivalences are symmetric.  -/
CoalgEquiv.symm : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₗc[R] B) → B ≃ₗc[R] A
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.toList.isEmpty = t.isEmpty
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- A `σ₁₂`-semilinear isometric embedding of a normed `R`-module into an `R₂`-module,
denoted as `f : E →ₛₗᵢ[σ₁₂] E₂`.  -/
«term_→ₛₗᵢ[_]_» : Lean.TrailingParserDescr
-- Lean.Elab.DeclModifiers
/-- Fully qualified name that will be used to name the declaration in the kernel.  -/
Lean.Elab.ExpandDeclIdResult.declName : Lean.Elab.ExpandDeclIdResult → Lean.Name
-- Mathlib.Algebra.Ring.Periodic
List.periodic_prod : ∀ {α : Type u_1} {β : Type u_2} {c : α} [inst : Add α] [inst_1 : MulOneClass β] (l : List (α → β)),
  (∀ f ∈ l, Function.Periodic f c) → Function.Periodic l.prod c
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.aleph0_le_cof : ∀ {o : Ordinal.{u_1}}, Cardinal.aleph0 ≤ o.cof ↔ Order.IsSuccLimit o
-- Mathlib.Algebra.Torsor.Defs
/-- `p' ↦ p /ₛ p'` as an equivalence.  -/
Equiv.constSDiv : {G : Type u_1} → {P : Type u_2} → [inst : Group G] → [Torsor G P] → P → P ≃ G
-- Mathlib.Algebra.Group.Units.Hom
IsUnit.of_leftInverse : ∀ {F : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : FunLike G N M]
  [inst_2 : Monoid M] [inst_3 : Monoid N] [MonoidHomClass G N M] {f : F} {x : M} (g : G),
  Function.LeftInverse ⇑g ⇑f → IsUnit (f x) → IsUnit x
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_iff_tendsto' : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜},
  (∀ᶠ (x : α) in l, g x = 0 → f x = 0) → (f =o[l] g ↔ Filter.Tendsto (fun x => f x / g x) l (nhds 0))
-- Mathlib.NumberTheory.ModularForms.Discriminant
_private.Mathlib.NumberTheory.ModularForms.Discriminant.0.ModularForm.termΔ : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.rightLeft : Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.Topology.Algebra.MulAction
Continuous.smul : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X},
  Continuous f → Continuous g → Continuous (f • g)
-- Batteries.Data.UInt
UInt32.toUInt8_toNat : ∀ (x : UInt32), x.toUInt8.toNat = x.toNat % 2 ^ 8
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- When `y` and `z` are both near `x` (the difference is in a ball),
initial coefficients of `f.val y` and `f.val z` agree.  -/
HahnEmbedding.Partial.coeff_eq_of_mem : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [IsOrderedAddMonoid R] [Archimedean R] (x : M) {y z : ↥(↑f).domain} {c : FiniteArchimedeanClass M},
  ↑y - x ∈ FiniteArchimedeanClass.ball K c →
    ↑z - x ∈ FiniteArchimedeanClass.ball K c →
      ∀ {d : FiniteArchimedeanClass M}, d ≤ c → (ofLex (↑↑f y)).coeff d = (ofLex (↑↑f z)).coeff d
-- Init.Grind.Module.Basic
Lean.Grind.NatModule.add_nsmul : ∀ {M : Type u} [inst : Lean.Grind.NatModule M] (n m : ℕ) (a : M), (n + m) • a = n • a + m • a
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `*` is a commutative semigroup, if it admits a surjective map that preserves
`*` from a commutative semigroup. See note [reducible non-instances].  -/
Function.Surjective.commMagma : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₂] →
      [inst_1 : CommMagma M₁] →
        (f : M₁ → M₂) → Function.Surjective f → (∀ (x y : M₁), f (x * y) = f x * f y) → CommMagma M₂
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.one_natPow : ∀ {b : ℕ}, Nat.pow 1 b = 1
-- Init.Data.List.ToArray
List.zipWithAll_toArray : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → Option β → γ) (as : List α) (bs : List β),
  Array.zipWithAll f as.toArray bs.toArray = (List.zipWithAll f as bs).toArray
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `p` be the minimal polynomial of `x`. If `y` is a conjugate root of `x`, then `p y = 0`.
 -/
IsConjRoot.aeval_eq_zero : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x y : A},
  IsConjRoot R x y → (Polynomial.aeval y) (minpoly R x) = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {h' : k ∈ Std.DHashMap.map f m},
  (Std.DHashMap.map f m).get k h' = f k (m.get k ⋯)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapDomain_algebraMap : ∀ {R : Type u_1} (A : Type u_4) {M : Type u_7} {N : Type u_8} {F : Type u_10} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] [inst_5 : FunLike F M N]
  [AddMonoidHomClass F M N] (f : F) (r : R),
  AddMonoidAlgebra.mapDomain (⇑f) ((algebraMap R (AddMonoidAlgebra A M)) r) = (algebraMap R (AddMonoidAlgebra A N)) r
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.coeMulHom.eq_1 : ∀ {α : Type u} [inst : Mul α], WithOne.coeMulHom = { toFun := WithOne.coe, map_mul' := ⋯ }
-- Mathlib.Order.RelIso.Set
/-- A relation `r` is well-founded iff every downward-interval `{ a | r a b }` of it is
well-founded.  -/
wellFounded_iff_wellFounded_subrel : ∀ {α : Type u_1} {r : α → α → Prop} [IsTrans α r], WellFounded r ↔ ∀ (b : α), WellFounded (Subrel r fun x => r x b)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.one.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} [inst_1 : SizeOf J],
  sizeOf CommRingCat.Colimits.Prequotient.one = 1
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The inverse of the restriction to `ball 0 1` is continuous on the image.  -/
Topology.CWComplex.continuousOn_symm : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} [self : Topology.CWComplex C] (n : ℕ)
  (i : Topology.CWComplex.cell C n),
  ContinuousOn (↑(Topology.CWComplex.map n i).symm) (Topology.CWComplex.map n i).target
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_fst_eq_self_iff_mem : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) {g : G},
  1 ∈ T → (↑(hST.equiv g).1 = g ↔ g ∈ S)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_snd : ∀ {𝕜 : 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'] {s : Set (M × M')} {x : M × M'},
  UniqueMDiffAt[s] x → mfderiv[s] Prod.snd x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.mem_stabilizer_set' : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {s : Set α},
  s.Finite → (a ∈ AddAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a +ᵥ b ∈ s)
-- Init.Data.List.Basic
List.erase.eq_2 : ∀ {α : Type u_1} [inst : BEq α] (x a : α) (as : List α),
  (a :: as).erase x =
    match a == x with
    | true => as
    | false => a :: as.erase x
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.costar_apply : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) {u v : U} (e : u ⟶ v),
  φ.costar v (Quiver.Costar.mk e) = Quiver.Costar.mk (φ.map e)
-- Mathlib.Data.Set.Basic
Set.Nonempty.of_sdiff : ∀ {α : Type u} {s t : Set α}, (s \ t).Nonempty → s.Nonempty
-- Mathlib.Data.Multiset.UnionInter
Multiset.le_inter_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u