mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (List.map Sigma.fst l).contains k = false → (↑(m.insertMany l)).getKey! k = m.getKey! k
-- Mathlib.Algebra.Lie.IdealOperations
/-- Note that the inequality can be strict; e.g., the inclusion of an Abelian subalgebra of a
simple algebra.  -/
LieIdeal.map_bracket_le : ∀ {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'] (f : L →ₗ⁅R⁆ L') {I₁ I₂ : LieIdeal R L},
  LieIdeal.map f ⁅I₁, I₂⁆ ≤ ⁅LieIdeal.map f I₁, LieIdeal.map f I₂⁆
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_X : ∀ {R : Type u_1} [inst : Semiring R] (x y : R), Polynomial.evalEval x y Polynomial.X = y
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.le_centralizer : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [h : IsMulCommutative ↥H], H ≤ Subgroup.centralizer ↑H
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.homeomorph_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (hf : IsHomeomorph f) (a : X), (IsHomeomorph.homeomorph f hf) a = f a
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
/-- An abbreviation for the action of `externalProductBifunctor J₁ J₂ C` on objects.  -/
CategoryTheory.MonoidalCategory.externalProduct : {J₁ : Type u₁} →
  {J₂ : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} J₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            [CategoryTheory.MonoidalCategory C] →
              CategoryTheory.Functor J₁ C → CategoryTheory.Functor J₂ C → CategoryTheory.Functor (J₁ × J₂) C
-- Mathlib.Computability.Primrec.List
Primrec.list_findIdx : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → List β} {p : α → β → Bool},
  Primrec f → Primrec₂ p → Primrec fun a => List.findIdx (p a) (f a)
-- Lean.CoreM
Lean.Core.State.mk.sizeOf_spec : ∀ (env : Lean.Environment) (nextMacroScope : Lean.MacroScope) (ngen : Lean.NameGenerator)
  (auxDeclNGen : Lean.DeclNameGenerator) (traceState : Lean.TraceState) (cache : Lean.Core.Cache)
  (messages : Lean.MessageLog) (infoState : Lean.Elab.InfoState)
  (snapshotTasks : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  sizeOf
      { env := env, nextMacroScope := nextMacroScope, ngen := ngen, auxDeclNGen := auxDeclNGen,
        traceState := traceState, cache := cache, messages := messages, infoState := infoState,
        snapshotTasks := snapshotTasks } =
    1 + sizeOf env + sizeOf nextMacroScope + sizeOf ngen + sizeOf auxDeclNGen + sizeOf traceState + sizeOf cache +
          sizeOf messages +
        sizeOf infoState +
      sizeOf snapshotTasks
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.contDiff : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  ContDiff ℝ ↑n ⇑f
-- Std.Internal.UV.System
Std.Internal.UV.System.PasswdInfo.mk.injEq : ∀ (username : String) (uid gid : Option UInt64) (shell homedir : Option String) (username_1 : String)
  (uid_1 gid_1 : Option UInt64) (shell_1 homedir_1 : Option String),
  ({ username := username, uid := uid, gid := gid, shell := shell, homedir := homedir } =
      { username := username_1, uid := uid_1, gid := gid_1, shell := shell_1, homedir := homedir_1 }) =
    (username = username_1 ∧ uid = uid_1 ∧ gid = gid_1 ∧ shell = shell_1 ∧ homedir = homedir_1)
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.deriv_aeval_eq : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] {R : Type u_2} [inst_2 : CommRing R]
  [inst_3 : Differential R] [inst_4 : Algebra A R] [DifferentialAlgebra A R] (x : R) (p : Polynomial A),
  ((Polynomial.aeval x) p)′ =
    (Polynomial.aeval x) (Differential.mapCoeffs p) + (Polynomial.aeval x) (Polynomial.derivative p) * x′
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_le_size_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {l : List (α × β)}, (↑m).size ≤ (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).size
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- Restrict the source of a partial isomorphism to a smaller dense open.  -/
AlgebraicGeometry.Scheme.PartialIso.restrictSource : {X Y : AlgebraicGeometry.Scheme} → (f : X.PartialIso Y) → (U : X.Opens) → Dense ↑U → U ≤ f.source → X.PartialIso Y
-- Lean.Language.Lean.Types
/-- Additional, untyped snapshots used for reporting, not reuse.  -/
Lean.Language.Lean.CommandElaboratingSnapshot.reportSnap : Lean.Language.Lean.CommandElaboratingSnapshot → Lean.Language.SnapshotTask Lean.Language.SnapshotTree
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.const_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (c : γ) (f : C(α, β)), (ContinuousMap.const β c).comp f = ContinuousMap.const α c
-- Mathlib.GroupTheory.Index
Subgroup.exists_pow_mem_of_relIndex_ne_zero : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  H.relIndex K ≠ 0 → ∀ {a : G}, a ∈ K → ∃ n, 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.equivIsoColimit_symm_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cocone F} (i : r ≅ t)
  (P : CategoryTheory.Limits.IsColimit t),
  (CategoryTheory.Limits.IsColimit.equivIsoColimit i).symm P = P.ofIsoColimit i.symm
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.add_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G},
  IsBoundedBilinearMap 𝕜 f → ∀ (x : E) (y₁ y₂ : F), f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂)
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
/-- Variant of `targetAffineLocally_affineAnd_iff` where `IsAffineHom` is bundled.  -/
AlgebraicGeometry.targetAffineLocally_affineAnd_iff' : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
      AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f ↔
        AlgebraicGeometry.IsAffineHom f ∧
          ∀ (U : Y.Opens),
            AlgebraicGeometry.IsAffineOpen U → Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U))
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.instCategoryEtale : (X : AlgebraicGeometry.Scheme) → CategoryTheory.Category.{u_1, u_1 + 1} X.Etale
-- Mathlib.Topology.Order
generateFrom_iUnion : ∀ {α : Type u} {ι : Sort v} {f : ι → Set (Set α)},
  TopologicalSpace.generateFrom (⋃ i, f i) = ⨅ i, TopologicalSpace.generateFrom (f i)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.coeff_add_eq_right_of_lt : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p q : Polynomial R}, p.natDegree < n → (p + q).coeff n = q.coeff n
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousAt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {x : α},
  LowerSemicontinuousAt f x ↔ ∀ y < f x, ∀ᶠ (x' : α) in nhds x, y < f x'
-- Mathlib.Order.Filter.Map
Filter.comap_sumElim_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : Filter γ) (m₁ : α → γ) (m₂ : β → γ),
  Filter.comap (Sum.elim m₁ m₂) l = Filter.map Sum.inl (Filter.comap m₁ l) ⊔ Filter.map Sum.inr (Filter.comap m₂ l)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_containsThenInsert : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {b : β a}, Std.DHashMap.Internal.Raw.WFImp ↑(m.containsThenInsert a b).2
-- Mathlib.RingTheory.LaurentSeries
/-- The coefficients of a power series vanish in degree strictly less than its valuation.  -/
LaurentSeries.coeff_zero_of_lt_intValuation : ∀ (K : Type u_2) [inst : Field K] {n d : ℕ} {f : PowerSeries K},
  Valued.v ((HahnSeries.ofPowerSeries ℤ K) f) ≤ WithZero.exp (-↑d) → n < d → (PowerSeries.coeff n) f = 0
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_congr : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {v : α →₀ M} {f g : α → β},
  (∀ x ∈ v.support, f x = g x) → Finsupp.mapDomain f v = Finsupp.mapDomain g v
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.lt_of_eq : ∀ {α : Type u_1} {a a' b b' : α} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α],
  a = b → a' + b < b' + a → a' < b'
-- Mathlib.Topology.Algebra.Affine
/-- If `f` is an affine map, then its linear part is an open map iff `f` is an open map.  -/
AffineMap.isOpenMap_linear_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [inst : AddCommGroup V]
  [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P]
  [inst_5 : AddCommGroup W] [inst_6 : TopologicalSpace W] [inst_7 : AddTorsor W Q] [inst_8 : TopologicalSpace Q]
  [IsTopologicalAddTorsor Q] [inst_10 : Ring R] [inst_11 : Module R V] [inst_12 : Module R W] {f : P →ᵃ[R] Q},
  IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f
-- Mathlib.Order.Closure
LowerAdjoint.closure_is_closed : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α),
  u (l.toFun x) ∈ l.closed
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.instNeBotSymmetricIoo : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G] [Filter.atTop.NeBot],
  (SummationFilter.symmetricIoo G).NeBot
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Any type satisfying `MulActionSemiHomClass` can be cast into `MulActionHom` via
`MulActionHomSemiClass.toMulActionHom`.  -/
MulActionHom.instCoeTCOfMulActionSemiHomClass : {M : Type u_2} →
  {N : Type u_3} →
    {φ : M → N} →
      {X : Type u_5} →
        [inst : SMul M X] →
          {Y : Type u_6} →
            [inst_1 : SMul N Y] →
              {F : Type u_8} → [inst_2 : FunLike F X Y] → [MulActionSemiHomClass F φ X Y] → CoeTC F (X →ₑ[φ] Y)
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtr.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {a : α}, IsLocalExtr f a → ∀ {g : β → γ}, Monotone g → IsLocalExtr (g ∘ f) a
-- Mathlib.Order.WithBot
WithBot.unbotD_le_iff : ∀ {α : Type u_1} {a b : α} [inst : LE α] {x : WithBot α}, (x = ⊥ → a ≤ b) → (WithBot.unbotD a x ≤ b ↔ x ≤ ↑b)
-- Mathlib.Data.Multiset.Fold
_private.Mathlib.Data.Multiset.Fold.0.Multiset.«term_*_» : Lean.TrailingParserDescr
-- Mathlib.Control.Monad.Cont
WriterT.mkLabel : {m : Type u → Type v} →
  [Monad m] →
    {α : Type u_1} →
      {β ω : Type u} → [EmptyCollection ω] → MonadCont.Label (α × ω) m β → MonadCont.Label α (WriterT ω m) β
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- If `t` is a point in `X ×[S] Y` above `(x, y, s)`, then this is the image of the unique
point of `Spec κ(s)` in `Spec κ(x) ⊗[κ(s)] κ(y)`.  -/
AlgebraicGeometry.Scheme.Pullback.SpecOfPoint : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} →
    {g : Y ⟶ S} →
      (t : ↥(CategoryTheory.Limits.pullback f g)) →
        ↥(AlgebraicGeometry.Spec (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).tensor)
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.support.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (M : AddSubmonoid G), M.support = { toAddSubmonoid := M ⊓ -M, neg_mem' := ⋯ }
-- Mathlib.RingTheory.Noetherian.Orzech
/-- **Orzech's theorem** for Noetherian modules: if `R` is a ring (not necessarily commutative),
`M` is a Noetherian `R`-module, `N` is a submodule, `f : N →ₗ[R] M` is surjective, then `f` is also
injective.  -/
IsNoetherian.injective_of_surjective_of_submodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  {N : Submodule R M} (f : ↥N →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f
-- Mathlib.Order.Filter.Lift
Filter.principal_le_lift' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {t : Set β},
  Filter.principal t ≤ f.lift' h ↔ ∀ s ∈ f, t ⊆ h s
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.map_apply_map_symm_eq : ∀ {α : Type u_1} {β : Type u_2} {x : FreeAddMonoid β} (e : α ≃ β),
  (FreeAddMonoid.map ⇑e) ((FreeAddMonoid.map ⇑e.symm) x) = x
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- For strong FE-pairs, `P.Λ` is everywhere equal to the Mellin transform of `P.f`.  -/
IsStrongFEPair.Λ_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → P.Λ = mellin P.f
-- Mathlib.Data.Nat.Log
Nat.log_div_base : ∀ (b n : ℕ), Nat.log b (n / b) = Nat.log b n - 1
-- Mathlib.Data.Fintype.Pi
Set.iUnion_fin_add_one_eq_iUnion_succ : ∀ {α : Type u_1} {n : ℕ} (f : Fin (n + 1) → Set α), ⋃ i, f i = f 0 ∪ Set.iUnion (f ∘ Fin.succ)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α}, ∅.contains k = false
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' i, f i x`. Assume that each individual function `f i` is of
class `C^N`, and moreover there is a uniform summable upper bound on the `k`-th derivative
for each `k ≤ N` (except maybe for finitely many `i`s). Then the series is also `C^N`.  -/
contDiff_tsum_of_eventually : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞},
  (∀ (i : α), ContDiff 𝕜 (↑N) (f i)) →
    (∀ (k : ℕ), ↑k ≤ N → Summable (v k)) →
      (∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in Filter.cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) →
        ContDiff 𝕜 ↑N fun x => ∑' (i : α), f i x
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.exists_monotone_subseq : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsPreorder α r],
  s.PartiallyWellOrderedOn r → ∀ {f : ℕ → α}, (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.add_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (f g : ContIntertwiningMap π₁ π₂) (v : V),
  (f + g) v = f v + g v
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_le_of_isSuccPrelimit : ∀ {o : Ordinal.{u_1}},
  Order.IsSuccPrelimit o → ∀ {c : Cardinal.{u_1}}, Cardinal.preAleph o ≤ c ↔ ∀ o' < o, Cardinal.preAleph o' ≤ c
-- Mathlib.NumberTheory.Dioph
Dioph.diophFn_comp1 : ∀ {α : Type u} {S : Set (Option α → ℕ)},
  Dioph S → ∀ {f : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph {v | Option.elim' (f v) v ∈ S}
-- Init.Tactics
/-- This is a "finishing" tactic modification of `simp`. It has two forms.

* `simpa [rules, ⋯] using e` will simplify the goal and the type of
  `e` using `rules`, then try to close the goal using `e`.

  Simplifying the type of `e` makes it more likely to match the goal
  (which has also been simplified). This construction also tends to be
  more robust under changes to the simp lemma set.

  The final match between the simplified `e` and the simplified goal uses
  **reducible** transparency, so it does not unfold semireducible definitions.
  Write `simpa [rules, ⋯] using! e` to perform the match at the ambient
  (default/semireducible) transparency instead.

* `simpa [rules, ⋯]` will simplify the goal and the type of a
  hypothesis `this` if present in the context, then try to close the goal using
  the `assumption` tactic.

As with `simp`, the `!` modifier after `simpa` enables auto-unfolding of
definitions in the simp set.
 -/
Lean.Parser.Tactic.tacticSimpa!__1 : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.trans_target : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z),
  (f.trans g).target =
    (AlgebraicGeometry.Scheme.Hom.opensFunctor g.target.ι).obj
      ((AlgebraicGeometry.Scheme.Hom.opensFunctor g.iso.hom).obj
        ((TopologicalSpace.Opens.map g.source.ι.base).obj (f.target ⊓ g.source)))
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.instOfHasExponent : ∀ (K : Type u_2) (L : Type u_3) [inst : Field K] [inst_1 : Ring L] [IsDomain L] [inst_3 : Algebra K L]
  [IsPurelyInseparable.HasExponent K L], IsPurelyInseparable K L
-- Lean.Expr
/-- Given `a b : Int`, returns `a + b`  -/
Lean.mkIntAdd : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Order.SuccPred.Basic
Order.pred_injective : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α], Function.Injective Order.pred
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_pullback_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : Y ⟶ X) (S : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.pullback f S) ≤
    CategoryTheory.Sieve.pullback (F.map f) (CategoryTheory.Sieve.functorPushforward F S)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.associated_isSymm : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : CommSemiring S] [inst_4 : Algebra S R] (Q : QuadraticForm R M) [inst_5 : Invertible 2],
  LinearMap.IsSymm ((QuadraticMap.associatedHom S) Q)
-- Aesop.BuiltinRules.DestructProducts
_private.Aesop.BuiltinRules.DestructProducts.0.Aesop.BuiltinRules.destructProductHyp?.go : Lean.MVarId →
  Lean.FVarId →
    Lean.Expr →
      Lean.Expr →
        Lean.Expr → Lean.Expr → Lean.Name → Lean.Name → Lean.Name → Lean.MetaM (Aesop.Script.LazyStep × Lean.MVarId)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_zero`. -/
ModularForm.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.Tactic.IntervalCases
/-- Given `e`, return `(z, n, p)` where `p : e = n` and `n` is a numeral
appropriate for the type denoting the integer `z`.  -/
Mathlib.Tactic.IntervalCases.Methods.eval : Mathlib.Tactic.IntervalCases.Methods → Lean.Expr → Lean.MetaM (ℤ × Lean.Expr × Lean.Expr)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.isExponentiable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {I J : C}
  (f : I ⟶ J) [CategoryTheory.ExponentiableMorphism f], CategoryTheory.IsExponentiable f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k : α} {h' : k ∈ t.insertManyIfNewUnit l} (contains : k ∈ t),
      (t.insertManyIfNewUnit l).getKey k h' = t.getKey k contains
-- Mathlib.Data.List.Permutation
/-- The pair `[a, b]` is a permutation of a list if and only if that list is equal to `[a, b]` or
to `[b, a]`.  -/
List.pair_perm : ∀ {α : Type u_1} {a b : α} {l : List α}, [a, b].Perm l ↔ l = [a, b] ∨ l = [b, a]
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.d_fstX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j)
      (HomologicalComplex.homotopyCofiber.fstX φ j k hjk) =
    -CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij) (F.d j k)
-- Init.Data.Int.Order
Int.sub_lt_of_sub_lt : ∀ {a b c : ℤ}, a - b < c → a - c < b
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNonUnitalCommRing : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [NonUnitalCommRing R] → NonUnitalCommRing (l.Germ R)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.irreducible_pow_sup_of_le : ∀ {T : Type u_4} [inst : CommRing T] [IsDedekindDomain T] {I J : Ideal T},
  Irreducible J → ∀ (n : ℕ), ↑n ≤ emultiplicity J I → J ^ n ⊔ I = J ^ n
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConst.go.induct_unfolding : ∀ (k : ℤ) (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k_1 : ℤ), motive (Lean.Grind.CommRing.Poly.num k_1) (Lean.Grind.CommRing.Poly.num (k * k_1))) →
    (∀ (k_1 : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (Lean.Grind.CommRing.Poly.mulConst.go k p) →
          motive (Lean.Grind.CommRing.Poly.add k_1 m p)
            (Lean.Grind.CommRing.Poly.add (k * k_1) m (Lean.Grind.CommRing.Poly.mulConst.go k p))) →
      ∀ (a : Lean.Grind.CommRing.Poly), motive a (Lean.Grind.CommRing.Poly.mulConst.go k a)
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
AddSubgroup.properlyDiscontinuousVAdd_iff_of_isFiniteRelIndex : ∀ {Γ : Type u_1} {α : Type u_2} [inst : AddGroup Γ] [inst_1 : TopologicalSpace α] [inst_2 : AddAction Γ α]
  [ContinuousConstVAdd Γ α] {G H : AddSubgroup Γ},
  G ≤ H → ∀ [G.IsFiniteRelIndex H], ProperlyDiscontinuousVAdd (↥G) α ↔ ProperlyDiscontinuousVAdd (↥H) α
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating the first vector by the angle between the two vectors and swapping the vectors
results in an angle of 0.  -/
Orientation.oangle_rotation_oangle_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), o.oangle y ((o.rotation (o.oangle x y)) x) = 0
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.mem_L1_toReal_of_lintegral_ne_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → MeasureTheory.MemLp (fun x => (f x).toReal) 1 μ
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The existence of a right adjoint of `f`.  -/
CategoryTheory.Bicategory.IsLeftAdjoint : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → {a b : B} → (a ⟶ b) → Prop