mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.not_equiv_of_X_ne : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 0 * Q 2 ≠ Q 0 * P 2 → ¬P ≈ Q
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.forget_map : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} (a : X ⟶ Y),
  CategoryTheory.Bicategory.InducedBicategory.forget.map a = a.hom
-- Mathlib.Topology.Order.LeftRightLim
Antitone.leftLim_le_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f → ∀ {x y : α}, x < y → Function.leftLim f y ≤ Function.rightLim f x
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.mkCleanName : Lean.Name → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Name
-- Lean.Elab.Syntax
Lean.Elab.Term.ToParserDescrContext : Type
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} →
            {f : X₁ ⟶ X₂} →
              (ι : Type w) →
                (π : ι → α) →
                  (cofan₁ : CategoryTheory.Limits.Cofan fun i => A (π i)) →
                    (cofan₂ : CategoryTheory.Limits.Cofan fun i => B (π i)) →
                      CategoryTheory.Limits.IsColimit cofan₁ →
                        CategoryTheory.Limits.IsColimit cofan₂ →
                          (m : cofan₁.pt ⟶ cofan₂.pt) →
                            autoParam
                                (∀ (i : ι),
                                  CategoryTheory.CategoryStruct.comp (cofan₁.inj i) m =
                                    CategoryTheory.CategoryStruct.comp (g (π i)) (cofan₂.inj i))
                                HomotopicalAlgebra.AttachCells.hm._autoParam →
                              (g₁ : cofan₁.pt ⟶ X₁) →
                                (g₂ : cofan₂.pt ⟶ X₂) →
                                  CategoryTheory.IsPushout g₁ m f g₂ → HomotopicalAlgebra.AttachCells g f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF → ∀ {k a : α} {v : β k}, (m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.isUnit.match_1.congr_eq_2 : ∀ {n : ℕ} (motive : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (x : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (h_1 : (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → motive [l])
  (h_2 : (x : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → motive x)
  (x_1 : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  x = x_1 →
    (∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), x_1 = [l] → False) →
      (match x with
        | [l] => h_1 l
        | x => h_2 x) ≍
        h_2 x_1
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.quot_mul : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat)
  (x y : MonCat.Colimits.Prequotient F),
  Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) (x.mul y) =
    Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) x * Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) y
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_lt : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α],
  |a|ₘ < b ↔ b⁻¹ < a ∧ a < b
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.existsRatHint_of_ratHintsExhaustive : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRatAdd →
    ∀ (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (ℕ × Array ℕ)),
      f.ratHintsExhaustive pivot ratHints = true →
        ∀ c' ∈ f.toList,
          pivot.negate ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c' → ∃ i, f.clauses[ratHints[i].1]! = some c'
-- Mathlib.Analysis.LocallyConvex.AbsConvex
closedAbsConvexHull_eq_closure_absConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E},
  (closedAbsConvexHull 𝕜) s = closure ((absConvexHull 𝕜) s)
-- Mathlib.Algebra.Module.Torsion.Basic
_private.Mathlib.Algebra.Module.Torsion.Basic.0.Submodule.disjoint_torsionBySet_ideal.match_1_1.eq_2 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_2 ()
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsFlat.subset_of_isBasis_of_isBasis : ∀ {α : Type u_2} {M : Matroid α} {F : Set α}, M.IsFlat F → ∀ ⦃I X : Set α⦄, M.IsBasis I F → M.IsBasis I X → X ⊆ F
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_top : ∀ {K : Type u} [inst : Field K] (x : K), x ∈ ⊤
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The **Borel Isomorphism Theorem**: Any two uncountable standard Borel spaces are
Borel isomorphic.  -/
PolishSpace.measurableEquivOfNotCountable : {α : Type u_4} →
  {β : Type u_6} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] →
        [StandardBorelSpace α] → [StandardBorelSpace β] → ¬Countable α → ¬Countable β → α ≃ᵐ β
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.mono : ∀ {𝕜 : 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] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s t : Set E},
  HasFDerivWithinAt f f' t x → s ⊆ t → HasFDerivWithinAt f f' s x
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.le_orthogonal_orthogonal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} {N : Submodule R M}, B.IsRefl → N ≤ B.orthogonal (B.orthogonal N)
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopCat.Presheaf.isSheaf_of_isOpenEmbedding : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} {f : X ⟶ Y} {F : TopCat.Presheaf C Y}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  F.IsSheaf → TopCat.Presheaf.IsSheaf (h.functor.op.comp F)
-- Mathlib.Topology.Category.Profinite.CofilteredLimit
Profinite.exists_locallyConstant_finite_nonempty : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J]
  {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1} [Finite α] [Nonempty α]
  (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toTop) α),
  ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
-- Mathlib.Data.Seq.Basic
Stream'.Seq.nil_append : ∀ {α : Type u} (s : Stream'.Seq α), Stream'.Seq.nil.append s = s
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v))
  (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ F).inv.app X =
    CategoryTheory.CategoryStruct.id X.left
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.typeAscriptions : Lean.Option Bool
-- Mathlib.CategoryTheory.Functor.Hom
/-- `Functor.hom` is the hom-pairing, sending `(X, Y)` to `X ⟶ Y`, contravariant in `X` and
covariant in `Y`.  -/
CategoryTheory.Functor.hom : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (Cᵒᵖ × C) (Type v)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (x : M),
  (f.lift hg) (f x) = g x
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.height_le_spanFinrank : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (I : Ideal R), I ≠ ⊤ → I.height ≤ ↑(Submodule.spanFinrank I)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.seq : ∀ {hd : ℝ → ℝ} {tl : List (ℝ → ℝ)} (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (hd :: tl)),
  (∀ x ∈ ms.seq, x.2.Sorted) → Stream'.Seq.Pairwise (fun x1 x2 => x1 > x2) ms.seq → ms.Sorted
-- Mathlib.Data.Set.Function
Set.SurjOn.inter : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : α → β},
  Set.SurjOn f s₁ t → Set.SurjOn f s₂ t → Set.InjOn f (s₁ ∪ s₂) → Set.SurjOn f (s₁ ∩ s₂) t
-- Mathlib.Order.BooleanAlgebra.Defs
GeneralizedBooleanAlgebra.toSDiff : {α : Type u} → [self : GeneralizedBooleanAlgebra α] → SDiff α
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedMul.toMulLeftMono : ∀ {α : Type u} [inst : Semigroup α] [inst_1 : LE α] [CanonicallyOrderedMul α], MulLeftMono α
-- LeanSearchClient.LoogleSyntax
/-- Search [Loogle](https://loogle.lean-lang.org/json) from within Lean. This can be used as a command, term or tactic as in the following examples. In the case of a tactic, only valid tactics are displayed.


```lean
#loogle List ?a → ?a

example := #loogle List ?a → ?a

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ
  sorry

```

## Loogle Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.

By lemma name substring:
🔍 \"differ\"
finds all lemmas that have \"differ\" somewhere in their lemma name.

By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b

By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, \"two\", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have \"two\" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

You can modify the Loogle server URL by setting the `LEANSEARCHCLIENT_LOOGLE_API_URL` environment variable.
 -/
LeanSearchClient.loogle_tactic : Lean.ParserDescr
-- Lean.SubExpr
Lean.SubExpr.instToJsonMVarId : Lean.ToJson Lean.MVarId
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_right_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  (F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv
        (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).inv))
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_sub : ∀ (m n : ℕ∞), ↑(m - n) = ↑m - ↑n
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The sum of almost everywhere measurable functions is measurable.  -/
AEMeasurable.tsum : ∀ {X : Type u_6} {E : Type u_7} {ι : Type u_8} [inst : MeasurableSpace X] [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [SecondCountableTopology E]
  [inst_5 : MeasurableSpace E] [BorelSpace E] [MeasurableAdd₂ E] [Countable ι] {L : SummationFilter ι} [L.NeBot]
  [L.filter.IsCountablyGenerated] {μ : MeasureTheory.Measure X} {f : ι → X → E},
  (∀ (i : ι), AEMeasurable (f i) μ) → AEMeasurable (fun x => ∑'[L] (i : ι), f i x) μ
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_map : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] (f : M →ₗ[R'] N)
  (x : TrivSqZeroExt R' M), ((TrivSqZeroExt.map f) x).fst = x.fst
-- Mathlib.Analysis.Analytic.Composition
/-- `compChangeOfVariables m M N` is a bijection between `compPartialSumSource m M N`
and `compPartialSumTarget m M N`, yielding equal sums for functions that correspond to each
other under the bijection. As `compChangeOfVariables m M N` is a dependent function, stating
that it is a bijection is not directly possible, but the consequence on sums can be stated
more easily.  -/
FormalMultilinearSeries.compChangeOfVariables_sum : ∀ {α : Type u_6} [inst : AddCommMonoid α] (m M N : ℕ) (f : (n : ℕ) × (Fin n → ℕ) → α) (g : (n : ℕ) × Composition n → α),
  (∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ FormalMultilinearSeries.compPartialSumSource m M N),
      f e = g (FormalMultilinearSeries.compChangeOfVariables m M N e he)) →
    ∑ e ∈ FormalMultilinearSeries.compPartialSumSource m M N, f e =
      ∑ e ∈ FormalMultilinearSeries.compPartialSumTarget m M N, g e
-- Init.Data.String.Lemmas.Iterate
String.Slice.Model.map_get_revPositionsFrom_of_splits : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String},
  p.Splits t₁ t₂ → List.map (fun p => (↑p).get ⋯) (String.Slice.Model.revPositionsFrom p) = t₁.toList.reverse
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.lift_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (I : Ideal R) [inst_2 : I.IsPrime]
  (f : R →+* S) (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)) (r : R),
  (Ideal.ResidueField.lift I f hf₁ hf₂) ((algebraMap R I.ResidueField) r) = f r
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.zero_fst : ∀ {q : ℕ}, 0.1 = 0
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Given a cofiltered diagram `D` of quasi-compact `S`-schemes with affine transition maps,
and another scheme `X` of finite type over `S`.
Then the canonical map `colim Homₛ(Dᵢ, X) ⟶ Homₛ(lim Dᵢ, X)` is injective.

In other words, for each pair of `a : Homₛ(Dᵢ, X)` and `b : Homₛ(Dⱼ, X)` that give rise to the
same map `Homₛ(lim Dᵢ, X)`, there exists a `k` with `fᵢ : k ⟶ i` and `fⱼ : k ⟶ j` such that
`D(fᵢ) ≫ a = D(fⱼ) ≫ b`.
 -/
AlgebraicGeometry.Scheme.exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (t : D ⟶ (CategoryTheory.Functor.const I).obj S) (f : X ⟶ S)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)]
  [AlgebraicGeometry.LocallyOfFiniteType f] [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {i : I} (a : D.obj i ⟶ X),
  t.app i = CategoryTheory.CategoryStruct.comp a f →
    ∀ {j : I} (b : D.obj j ⟶ X),
      t.app j = CategoryTheory.CategoryStruct.comp b f →
        CategoryTheory.CategoryStruct.comp (c.π.app i) a = CategoryTheory.CategoryStruct.comp (c.π.app j) b →
          ∃ k hik hjk,
            CategoryTheory.CategoryStruct.comp (D.map hik) a = CategoryTheory.CategoryStruct.comp (D.map hjk) b
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.Shatters.mono_right : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s t : Finset α}, t ⊆ s → 𝒜.Shatters s → 𝒜.Shatters t
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] (a : α) (b : β) (s : Set β), a • insert b s = insert (a • b) (a • s)
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.tendsto_norm : ∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → Filter.Tendsto norm l Filter.atTop
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.AttributeEntry.mk.injEq : ∀ {γ : Type} (toOLeanEntry : Lean.KeyedDeclsAttribute.OLeanEntry) (isBuiltin : Bool) (value : γ)
  (toOLeanEntry_1 : Lean.KeyedDeclsAttribute.OLeanEntry) (isBuiltin_1 : Bool) (value_1 : γ),
  ({ toOLeanEntry := toOLeanEntry, isBuiltin := isBuiltin, value := value } =
      { toOLeanEntry := toOLeanEntry_1, isBuiltin := isBuiltin_1, value := value_1 }) =
    (toOLeanEntry = toOLeanEntry_1 ∧ isBuiltin = isBuiltin_1 ∧ value = value_1)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.instLocallyDirectedIsOpenImmersionDirectedAffineCover : {X : AlgebraicGeometry.Scheme} → AlgebraicGeometry.Scheme.Cover.LocallyDirected X.directedAffineCover
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- The linear map from the quotient by a smaller submodule to the quotient by a larger submodule.

This is the `Submodule.Quotient` version of `Quot.Factor`

When the two submodules are of the form `I ^ m • ⊤` and `I ^ n • ⊤` and `n ≤ m`,
please refer to the dedicated version `Submodule.factorPow`.  -/
Submodule.factor : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {p p' : Submodule R M} → p ≤ p' → M ⧸ p →ₗ[R] M ⧸ p'
-- Mathlib.Algebra.Group.End
Equiv.Perm.instInv : {α : Type u_4} → Inv (Equiv.Perm α)
-- Mathlib.Algebra.Ring.Equiv
NonUnitalRingHom.inverse_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R →ₙ+* S) (g : S → R) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a : S),
  (f.inverse g h₁ h₂) a = g a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k k' : α},
  (↑m).WF →
    m.getKey? k = some k' →
      Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.filterMap f m) k =
        (Std.DHashMap.Internal.Raw₀.Const.get? m k).bind fun x => f k' x
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- A universe-heterogeneous version of `Functor.map`.
 -/
Std.Iterators.HetT.map : {m : Type w → Type w'} →
  [Functor m] → {α : Type u} → {β : Type v} → (α → β) → Std.Iterators.HetT m α → Std.Iterators.HetT m β
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
AlgEquiv.isIntegral_iff : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_5} {B : Type u_6} [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B), Algebra.IsIntegral R A ↔ Algebra.IsIntegral R B
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformEmbedding_inr : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β], IsUniformEmbedding Sum.inr
-- Mathlib.Order.Directed
/-- For every pair of elements `a` and `b` there is a `c` such that `r a c` and `r b c`  -/
IsDirected.directed : ∀ {α : Sort u_5} {r : α → α → Prop} [self : IsDirected α r] (a b : α), ∃ c, r a c ∧ r b c
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.getMutualInductName : Lean.Name → optParam Bool false → Lean.Name
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → (aig : Std.Sat.AIG α) → aig.ArbitraryShiftTarget w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Analysis.Normed.Module.Extr
/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum on a set `s` at a point `c` and
`y` is a vector on the same ray as `f c`, then the function `fun x => ‖f x + y‖` has a maximum
on `s` at `c`.  -/
IsMaxOn.norm_add_sameRay : ∀ {α : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : α → E} {s : Set α}
  {c : α} {y : E}, IsMaxOn (norm ∘ f) s c → SameRay ℝ (f c) y → IsMaxOn (fun x => ‖f x + y‖) s c
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a < ArchimedeanClass.mk b → 0 ≤ a → b < a
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.isIntegral_norm : ∀ {R : Type u_1} [inst : CommRing R] {L : Type u_6} (K : Type u_7) [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : Algebra R L] [inst_5 : Algebra R K] [IsScalarTower R K L] {x : L},
  IsIntegral R x → IsIntegral R ((Algebra.norm K) x)
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- The maximum degree of a nonempty graph is less than the number of vertices. Note that the assumption
that `V` is nonempty is necessary, as otherwise this would assert the existence of a
natural number less than zero.  -/
SimpleGraph.maxDegree_lt_card_verts : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Nonempty V],
  G.maxDegree < Fintype.card V
-- Std.Async.Signal
/-- Stop typed at terminal.
 -/
Std.Async.Signal.sigtstp : Std.Async.Signal
-- Lean.Compiler.LCNF.PublicDeclsExt
/-- Creates a replayable local environment extension holding a name set and the list of names in the
order they were added to the set.
 -/
Lean.Compiler.LCNF.mkOrderedDeclSetExt : IO (Lean.EnvExtension (List Lean.Name × Lean.NameSet))
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.commSemiring : (self : CommSemiRingCat) → CommSemiring ↑self
-- Init.Data.Vector.Extract
Vector.extract_append_extract : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j k : ℕ},
  xs.extract i j ++ xs.extract j k = Vector.cast ⋯ (xs.extract (min i j) (max j k))
-- Mathlib.Topology.EMetricSpace.Defs
/-- `WeakEMetricSpace` instance on subsets of emetric spaces  -/
instWeakEMetricSpaceSubtype : {α : Type u_2} → {p : α → Prop} → [inst : TopologicalSpace α] → [WeakEMetricSpace α] → WeakEMetricSpace (Subtype p)
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Summable.multipliableUniformlyOn_nat_one_add : ∀ {α : Type u_1} {K : Set α} {R : Type u_3} [inst : NormedCommRing R] [NormOneClass R] [CompleteSpace R]
  [inst_3 : TopologicalSpace α] {f : ℕ → α → R},
  IsCompact K →
    ∀ {u : ℕ → ℝ},
      Summable u →
        (∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) →
          (∀ (n : ℕ), ContinuousOn (f n) K) → MultipliableUniformlyOn (fun n x => 1 + f n x) K
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `L` are linearly disjoint over `F`, one of them is algebraic,
then `[L(A) : A] = [L : F]`. Note that in Lean `L(A)` is not naturally an `A`-algebra,
so this result is stated in a cumbersome way.  -/
IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L →
      Cardinal.lift.{w, v} (Module.rank ↥A ↥(IntermediateField.extendScalars ⋯)) =
        Cardinal.lift.{v, w} (Module.rank F L)