mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Server.Rpc.Basic
Lean.Server.RpcEncodable.rpcEncode : {α : Type} → [self : Lean.Server.RpcEncodable α] → α → StateM Lean.Server.RpcObjectStore Lean.Json
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
/-- The elements of the basis of neighborhoods of zero for the `I`-adic topology
on an `R`-module `M`, seen as open additive subgroups of `M`.  -/
Ideal.openAddSubgroup : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → ℕ → OpenAddSubgroup R
-- Mathlib.Analysis.Calculus.Deriv.Prod
/-- A variant of `hasDerivWithinAt_finCons` where the derivative variables are free on the RHS
instead.  -/
hasDerivWithinAt_finCons' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : F' 0} {φs' : (i : Fin n) → F' i.succ},
  HasDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') s x ↔
    HasDerivWithinAt φ φ' s x ∧ HasDerivWithinAt φs φs' s x
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.instFaithfulSMul : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_5) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  FaithfulSMul R K
-- Init.Data.Nat.Gcd
Nat.gcd_add_left_left_of_dvd : ∀ {m k : ℕ} (n : ℕ), m ∣ k → (k + n).gcd m = n.gcd m
-- Mathlib.Topology.CantorBendixson
CantorBendixson.perfectKernel.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X),
  CantorBendixson.perfectKernel s = ⋂ a, CantorBendixson.iteratedDerivedSet s a
-- Mathlib.Analysis.Convex.Join
/-- The join of two sets is the union of the segments joining them. This can be interpreted as the
topological join, but within the original space.  -/
convexJoin : (𝕜 : Type u_2) →
  {E : Type u_3} →
    [inst : Semiring 𝕜] → [PartialOrder 𝕜] → [inst_2 : AddCommMonoid E] → [Module 𝕜 E] → Set E → Set E → Set E
-- Mathlib.MeasureTheory.Constructions.Projective
/-- The projective limit of a family of finite measures is unique.  -/
MeasureTheory.IsProjectiveLimit.unique : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {μ ν : MeasureTheory.Measure ((i : ι) → α i)}
  [∀ (i : Finset ι), MeasureTheory.IsFiniteMeasure (P i)],
  MeasureTheory.IsProjectiveLimit μ P → MeasureTheory.IsProjectiveLimit ν P → μ = ν
-- Lean.Parser.Term
Lean.Parser.Term.nofun.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_nonpos_of_lt : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b c : α}, a ≤ 0 → b < c → a + b < c
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiff.restrict_scalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {𝕜' : Type u_3} [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜']
  [inst_7 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F],
  ContDiff 𝕜' n f → ContDiff 𝕜 n f
-- Mathlib.Computability.DFA
DFA.accepts_inter : ∀ {α : Type u} {σ1 σ2 : Type v} (M1 : DFA α σ1) (M2 : DFA α σ2), (M1.inter M2).accepts = M1.accepts ⊓ M2.accepts
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_one : ONote.repr 1 = ↑1
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.notMem_of_notMem_closure : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M} {P : M},
  P ∉ (FirstOrder.Language.Substructure.closure L).toFun s → P ∉ s
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.algebraMap_def : ∀ {α : Type u_1} {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring α]
  [inst_3 : Algebra R A] [inst_4 : Algebra A α] {S : Subalgebra R A} (s : ↥S),
  (algebraMap (↥S) α) s = (algebraMap A α) ↑s
-- Mathlib.Topology.Defs.Induced
Topology.IsOpenEmbedding.toIsEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsOpenEmbedding f → Topology.IsEmbedding f
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₃Unchecked : UInt8 → UInt8 → UInt8 → UInt32
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.biInter_gt_ball : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α) (r : ℝ),
  ⋂ r', ⋂ (_ : r' > r), Metric.ball x r' = Metric.closedBall x r
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Raised.eq_1 : ∀ (n m : ℕ), Ordnode.Raised n m = (m = n ∨ m = n + 1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
/-- For a unit parameter, shifting is the same as mapping by homothety.  -/
AffineSubspace.shift_eq_map_homothety : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : CommRing k] [inst_1 : AddCommGroup V] [inst_2 : AddTorsor V P]
  [inst_3 : Module k V] (s : AffineSubspace k P) (c : P) {r : k},
  IsUnit r → s.shift c r = AffineSubspace.map (AffineMap.homothety c r) s
-- Mathlib.Data.PFun
/-- The type of partial functions `α →. β` is equivalent to
the type of pairs `(p : α → Prop, f : Subtype p → β)`.  -/
PFun.equivSubtype : {α : Type u_1} → {β : Type u_2} → (α →. β) ≃ (p : α → Prop) × (Subtype p → β)
-- Init.Data.Fin.Lemmas
Fin.exists_fin_one : ∀ {p : Fin 1 → Prop}, (∃ i, p i) ↔ p 0
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautologicalRelations_G : ∀ (A : Type u) [inst : Ring A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M],
  (Module.Presentation.tautologicalRelations A M).G = M
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} [inst_2 : Inhabited β] {f : β → β},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.Const.modify m k f) k' =
    if (k == k') = true then (Option.map f (Std.ExtDHashMap.Const.get? m k)).get! else Std.ExtDHashMap.Const.get! m k'
-- Lean.Data.Lsp.Internal
/-- Name of the module that is imported.  -/
Lean.Lsp.ImportInfo.module : Lean.Lsp.ImportInfo → String
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_div_const_uIcc : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b c : α),
  (fun x => x / a) '' Set.uIcc b c = Set.uIcc (b / a) (c / a)
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroupClass.seminormedAddCommGroup : {E : Type u_1} →
  [inst : SeminormedAddCommGroup E] →
    {S : Type u_2} → [inst_1 : SetLike S E] → [AddSubgroupClass S E] → (s : S) → SeminormedAddCommGroup ↥s
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.mul_inverse_cancel_right : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x y : M₀), IsUnit x → y * x * Ring.inverse x = y
-- Mathlib.Algebra.Module.Equiv.Basic
Units.toLinearMap_mulRightLinearEquiv : ∀ {R : Type u_9} {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (u : Aˣ), ↑(Units.mulRightLinearEquiv R u) = LinearMap.mulRight R ↑u
-- Mathlib.Combinatorics.Additive.Convolution
Finset.op_smul_convolution_eq_convolution_smul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (s : G),
  (MulOpposite.op s • A).convolution B = A.convolution (s • B)
-- Mathlib.Analysis.Fourier.ZMod
/-- The discrete Fourier transform on `ℤ / N ℤ` (with the counting measure), bundled as a linear
equivalence. Denoted as `𝓕` within the `ZMod` namespace.
 -/
ZMod.dft : {N : ℕ} → [NeZero N] → {E : Type u_1} → [inst : AddCommGroup E] → [inst_1 : Module ℂ E] → (ZMod N → E) ≃ₗ[ℂ] ZMod N → E
-- Init.Data.Int.DivMod.Lemmas
Int.zero_bmod : ∀ {m : ℕ}, Int.bmod 0 m = 0
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.algebra : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsLocalRing R] →
      {R₀ : Type u_4} → [inst_2 : CommRing R₀] → [Algebra R₀ R] → Algebra R₀ (IsLocalRing.ResidueField R)
-- Init.Data.Iterators.Basic
Std.IterStep.successor_done : ∀ {α : Type u} {β : Type w}, Std.IterStep.done.successor = none
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A `c : Bicone F` is:
* an object `c.pt` and
* morphisms `π j : pt ⟶ F j` and `ι j : F j ⟶ pt` for each `j`,
* such that `ι j ≫ π j'` is the identity when `j = j'` and zero otherwise.
 -/
CategoryTheory.Limits.Bicone.π : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → (self : CategoryTheory.Limits.Bicone F) → (j : J) → self.pt ⟶ F j
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.forget_reflects_isos : ∀ {R : Type u} [inst : CommRing R], (CategoryTheory.forget (AlgCat R)).ReflectsIsomorphisms
-- Mathlib.Order.Interval.Set.OrderEmbedding
OrderEmbedding.preimage_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) (x : α),
  ⇑e ⁻¹' Set.Ici (e x) = Set.Ici x
-- Mathlib.Analysis.Meromorphic.Order
eventuallyConst_nhdsNE_iff_meromorphicOrderAt_sub_eq_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  Filter.EventuallyConst f (nhdsWithin x {x}ᶜ) ↔ ∃ c, meromorphicOrderAt (fun x => f x - c) x = ⊤
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cocone G} {t : CategoryTheory.Limits.Cocone F}
  (P : CategoryTheory.Limits.IsColimit t) (Q : CategoryTheory.Limits.IsColimit s) (w : F ≅ G),
  CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).hom (Q.desc r) = P.map r w.hom
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_refl' : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A], ⇑(ContinuousAlgEquiv.refl R A) = id
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.snd_apply' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {s : Set γ},
  MeasurableSet s → (κ.snd a) s = (κ a) (Prod.snd ⁻¹' s)
-- Std.Internal.Do.Order.Basic
Lean.Order.top_le_ofProp : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l] (p : Prop),
  p → Lean.Order.PartialOrder.rel Lean.Order.top (Lean.Order.CompleteLattice.ofProp p)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- `WeakLimitCone F` contains a cone over `F` together with the information that it is
a weak limit.  -/
CategoryTheory.Limits.WeakLimitCone : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] → CategoryTheory.Functor J C → Type (max (max u_1 u_3) v_3)
-- Mathlib.RingTheory.DedekindDomain.Different
/-- If `b` is an `A`-integral basis of `L` with discriminant `b`, then `d • a * x` is integral over
`A` for all `a ∈ I` and `x ∈ Iᵛ`.  -/
isIntegral_discr_mul_of_mem_traceDual : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [IsFractionRing A K]
  [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] (I : Submodule B L)
  {ι : Type u_4} [inst_16 : DecidableEq ι] [inst_17 : Fintype ι] {b : Module.Basis ι K L},
  (∀ (i : ι), IsIntegral A (b i)) →
    ∀ {a x : L}, a ∈ I → x ∈ Submodule.traceDual A K I → IsIntegral A (Algebra.discr K ⇑b • a * x)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.compare_minKey_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {he : t.modify k f ≠ ∅}, cmp ((t.modify k f).minKey he) (t.minKey ⋯) = Ordering.eq
-- Mathlib.RingTheory.Ideal.Maps
instIsTwoSidedAnnihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (Module.annihilator R M).IsTwoSided
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.spineInjective : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ}, Function.Injective ⇑(sx.spineEquiv n)
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatClamp n).toBitVec = n#'hn
-- Mathlib.Algebra.Group.Basic
eq_div_of_mul_eq' : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a * c = b → a = b / c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constEntryAtIdxD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {i : ℕ} {fallback : α × β},
  t₁.Equiv t₂ → Std.DTreeMap.Const.entryAtIdxD t₁ i fallback = Std.DTreeMap.Const.entryAtIdxD t₂ i fallback
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedIRType : Inhabited Lean.IR.IRType
-- ProofWidgets.Component.FilterDetails
/-- Contents of the `<summary>`.  -/
ProofWidgets.FilterDetailsProps.summary : ProofWidgets.FilterDetailsProps → ProofWidgets.Html
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.liftOn_ofFractionRing_mk : ∀ {K : Type u} [inst : CommRing K] {P : Sort v} (n : Polynomial K) (d : ↥(nonZeroDivisors (Polynomial K)))
  (f : Polynomial K → Polynomial K → P)
  (H :
    ∀ {p q p' q' : Polynomial K},
      q ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q'),
  { toFractionRing := Localization.mk n d }.liftOn f H = f n ↑d
-- Init.Data.Range.Polymorphic.PRange
/-- An upward-unbounded range of elements of `α` with an open lower bound.

`a<...*` is the range of all values greater than `a : α`.
This is notation for `Roi.mk a`.
 -/
Std.Roi : Type u → Type u
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Have.have : ∀ {σs : List (Type u)} {P H PH T : Std.Do.SPred σs}, (P ∧ H ⊣⊢ₛ PH) → (P ⊢ₛ H) → (PH ⊢ₛ T) → P ⊢ₛ T
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.equivQuotMaximalIdeal_symm_apply_mk : ∀ {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] (Rₚ : Type u_8) [inst_2 : CommRing Rₚ]
  [inst_3 : Algebra R Rₚ] [inst_4 : IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ] (x : R) (s : ↥p.primeCompl),
  (IsLocalization.AtPrime.equivQuotMaximalIdeal p Rₚ).symm
      ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal Rₚ)) (IsLocalization.mk' Rₚ x s)) =
    (Ideal.Quotient.mk p) x * ((Ideal.Quotient.mk p) ↑s)⁻¹
-- Init.Data.Nat.Coprime
Nat.Coprime.gcd_mul_right_cancel : ∀ {k n : ℕ} (m : ℕ), k.Coprime n → (m * k).gcd n = m.gcd n
-- Mathlib.FieldTheory.Galois.Basic
/-- A quadratic separable extension is Galois.
 -/
Algebra.IsQuadraticExtension.isGalois : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [Algebra.IsQuadraticExtension F K] [Algebra.IsSeparable F K], IsGalois F K
-- Lean.Compiler.IR.Basic
Lean.IR.VarId.mk.injEq : ∀ (idx idx_1 : Lean.IR.Index), ({ idx := idx } = { idx := idx_1 }) = (idx = idx_1)
-- Batteries.Data.Fin.Fold
Fin.foldl_eq_foldl_finRange : ∀ {α : Type u_1} {n : ℕ} (f : α → Fin n → α) (x : α), Fin.foldl n f x = List.foldl f x (List.finRange n)
-- Lean.Elab.App
/-- `f : fType  -/
Lean.Elab.Term.ElabElim.State.fType : Lean.Elab.Term.ElabElim.State → Lean.Expr
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s₁ s₂ : Set M}, IsLinearSet s₁ → IsLinearSet s₂ → IsLinearSet (s₁ + s₂)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.memLp_norm_rpow_iff : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {q : ENNReal} {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    q ≠ 0 → q ≠ ⊤ → (MeasureTheory.MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ ↔ MeasureTheory.MemLp f p μ)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.pre_map_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C)
  {X Y : CategoryTheory.Grothendieck (G.comp F)} (f : X ⟶ Y),
  ((CategoryTheory.Grothendieck.pre F G).map f).base = G.map f.base
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.sub : ∀ {n a b c d : ℕ}, c ≤ a → d ≤ b → a ≡ b [MOD n] → c ≡ d [MOD n] → a - c ≡ b - d [MOD n]
-- Init.Data.Vector.Lemmas
Vector.idRun_foldrM : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β → Id β} {b : β} {xs : Vector α n},
  (Vector.foldrM f b xs).run = Vector.foldr (fun x1 x2 => (f x1 x2).run) b xs
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.expCoeff_cast : ∀ (n : ℕ), ↑(WeierstrassCurve.expCoeff✝ n) = if Even n then ↑n / 2 else ↑n
-- Mathlib.GroupTheory.GroupAction.OfQuotient
MulDistribMulAction.instQuotientSubgroupSubtypeMemSubmonoidSubmonoid : {G : Type u_1} →
  [inst : Group G] →
    {A : Type u_2} →
      [inst_1 : Monoid A] →
        [inst_2 : MulDistribMulAction G A] →
          {H : Subgroup G} → [inst_3 : H.Normal] → MulDistribMulAction (G ⧸ H) ↥(FixedPoints.submonoid (↥H) A)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.sieve₁'_toPreOneHypercover_eq_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (i j : E.I₀), E.toPreOneHypercover.sieve₁' i j = ⊤
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.mk.inj : ∀ {ι : Type u_1} {X : Type u_2} {inst : TopologicalSpace X} {s : Set X} {toFun : ι → C(X, ℝ)}
  {locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)} {nonneg' : 0 ≤ toFun} {le_one' : toFun ≤ 1}
  {eventuallyEq_one' : ∀ x ∈ s, ∃ i, ⇑(toFun i) =ᶠ[nhds x] 1} {toFun_1 : ι → C(X, ℝ)}
  {locallyFinite'_1 : LocallyFinite fun i => Function.support ⇑(toFun_1 i)} {nonneg'_1 : 0 ≤ toFun_1}
  {le_one'_1 : toFun_1 ≤ 1} {eventuallyEq_one'_1 : ∀ x ∈ s, ∃ i, ⇑(toFun_1 i) =ᶠ[nhds x] 1},
  { toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg', le_one' := le_one',
        eventuallyEq_one' := eventuallyEq_one' } =
      { toFun := toFun_1, locallyFinite' := locallyFinite'_1, nonneg' := nonneg'_1, le_one' := le_one'_1,
        eventuallyEq_one' := eventuallyEq_one'_1 } →
    toFun = toFun_1
-- Init.Data.Int.Lemmas
Int.subNatNat_of_le : ∀ {m n : ℕ}, n ≤ m → Int.subNatNat m n = ↑(m - n)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.Iterators.Types.DropWhile.instIterator.match_3.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} →
          (it : Std.IterM m β) →
            (motive : it.internalState.inner.Step → Sort u_3) →
              (x : it.internalState.inner.Step) →
                ((it' : Std.IterM m β) →
                    (out : β) →
                      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
                        motive ⟨Std.IterStep.yield it' out, h⟩) →
                  ((it' : Std.IterM m β) →
                      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) →
                        motive ⟨Std.IterStep.skip it', h⟩) →
                    ((h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) →
                      motive x
-- Mathlib.Analysis.Complex.Circle
/-- The map `fun t => exp (t * I)` from `ℝ` to the unit circle in `ℂ`.  -/
Circle.exp : C(ℝ, Circle)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_starClosure : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : IsScalarTower R A A]
  [inst_7 : SMulCommClass R A A] (S : NonUnitalSubalgebra R A), ↑S.starClosure = ↑(S ⊔ star S)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.any_eq_false_iff_forall_mem_getKey_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulHashable α]
  [EquivBEq α] {p : α → β → Bool},
  m.WF → (m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p (m.getKey a h) (Std.DHashMap.Raw.Const.get m a h) = false)
-- Mathlib.Data.Finset.Basic
Finset.erase_insert_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), (insert a s).erase a ⊆ s
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.nthRoots_zero : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (r : R), Polynomial.nthRoots 0 r = 0
-- Mathlib.CategoryTheory.Discrete.Basic
/-- A discrete category is equivalent to its opposite category.  -/
CategoryTheory.Discrete.opposite : (α : Type u₁) → (CategoryTheory.Discrete α)ᵒᵖ ≌ CategoryTheory.Discrete α
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- **Alias** of `MeasureTheory.IntegrableOn.of_ae_sdiff_eq_zero`.

---

If a function is integrable on a set `s`, and its enorm vanishes on `t \ s`,
then it is integrable on `t` if `t` is null-measurable.  -/
MeasureTheory.IntegrableOn.of_ae_diff_eq_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s t : Set α} {μ : MeasureTheory.Measure α} {ε' : Type u_7}
  [inst : TopologicalSpace ε'] [inst_1 : ENormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.NullMeasurableSet t μ → (∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0) → MeasureTheory.IntegrableOn f t μ
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.qParam_tendsto : ∀ {h : ℝ},
  0 < h → Filter.Tendsto (Function.Periodic.qParam h) (Filter.comap Complex.im Filter.atTop) (nhdsWithin 0 {0}ᶜ)
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_eq : ∀ {n : ℕ} (x : BitVec n), BitVec.setWidth n x = x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false → (Std.DHashMap.Raw.Const.insertMany m l).getKey! k = m.getKey! k
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α}, ∅.isEmpty = true
-- Mathlib.Order.Fin.Basic
Fin.castAddOrderEmb_toEmbedding : ∀ {n : ℕ} (m : ℕ), (Fin.castAddOrderEmb m).toEmbedding = { toFun := Fin.castAdd m, inj' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.isIso_inl_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Epi f],
  CategoryTheory.IsIso (CategoryTheory.Limits.pushout.inl f f)
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp : ∀ {S : LightProfinite}, (LightProfinite.Extend.functorOp S.asLimitCone).Final
-- Mathlib.Geometry.RingedSpace.Basic
/-- If the germ of a section `f` is a unit in the stalk at `x`, then `f` must be a unit on some small
neighborhood around `x`.
 -/
AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ : ∀ (X : AlgebraicGeometry.RingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
  (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U),
  IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f) →
    ∃ V i, ∃ (_ : x ∈ V), IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) f)
-- Lean.Parser.Basic
Lean.Parser.invalidLongestMatchParser : Lean.Parser.ParserState → Lean.Parser.ParserState