mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- A field is finitely generated if and only if it is essentially of finite type over its prime
subfield.  -/
Field.fg_iff_essFiniteType : ∀ {F : Type u_1} [inst : Field F], Field.FG F ↔ Algebra.EssFiniteType (↥⊥) F
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.del.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → RBTree.RBColor → Sort u_2) (c : RBTree.RBColor)
  (parent : RBTree.RBNode.Path α) (y : α) (b a : RBTree.RBNode α)
  (h_1 : (t : RBTree.RBNode α) → (x : RBTree.RBColor) → motive RBTree.RBNode.Path.root t x)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.red)
  (h_3 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) →
            (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.red)
  (h_4 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.black)
  (h_5 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) →
            (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.black),
  (match RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.red with
    | RBTree.RBNode.Path.root, t, x => h_1 t x
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.red => h_2 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.red => h_3 c a y parent b
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.black => h_4 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.black => h_5 c a y parent b) =
    h_2 c parent y b a
-- Mathlib.Logic.Equiv.Prod
Equiv.sigmaProdDistrib_symm_apply : ∀ {ι : Type u_9} (α : ι → Type u_10) (β : Type u_11) (p : (i : ι) × α i × β),
  (Equiv.sigmaProdDistrib α β).symm p = (⟨p.fst, p.snd.1⟩, p.snd.2)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instFaithfulAlgebraToMonadComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} [R.Faithful] (h : L ⊣ R),
  (CategoryTheory.Monad.comparison h).Faithful
-- Mathlib.RingTheory.Etale.Descent
Algebra.FormallyUnramified.of_formallyUnramified_tensorProduct_of_faithfullyFlat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.FaithfullyFlat R T]
  [Algebra.FormallyUnramified T (TensorProduct R T S)], Algebra.FormallyUnramified R S
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.addFundamentalInterior_subset : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α},
  MeasureTheory.addFundamentalInterior G s ⊆ s
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_functor_obj_left_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.WithTerminal.equivComma.functor.obj F).left.map f = F.map (CategoryTheory.WithTerminal.incl.map f)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.nsmul_eq_nsmul_iff_modEq : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n m : ℕ}, IsOfFinAddOrder x → (n • x = m • x ↔ n ≡ m [MOD addOrderOf x])
-- Init.Data.List.Zip
List.map_zipWithAll : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : Option γ → Option δ → α} {l : List γ}
  {l' : List δ}, List.map f (List.zipWithAll g l l') = List.zipWithAll (fun x y => f (g x y)) l l'
-- Aesop.Script.Step
Aesop.Script.TacticState.applyStep : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Aesop.Script.TacticState → Aesop.Script.Step → m Aesop.Script.TacticState
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAt_pi' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i},
  HasFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasFDerivAt (fun x => Φ x i) (ContinuousLinearMap.proj i ∘SL Φ') x
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- Equation (11.3.8) from Cohn's proof, where we view `Q` as a constant.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₃_mul_Φ : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  Polynomial.map Polynomial.C (Polynomial.C (RatFunc.Luroth.Q₃✝ h)) * RatFunc.Luroth.Φ✝ E = RatFunc.Luroth.θ✝ E
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.totallyBounded_sup : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α},
  (f ⊔ g).TotallyBounded ↔ f.TotallyBounded ∧ g.TotallyBounded
-- Mathlib.FieldTheory.Normal.Basic
/-- [Stacks Tag 09HP](https://stacks.math.columbia.edu/tag/09HP) -/
IntermediateField.normal_inf : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  (E E' : IntermediateField F K) [Normal F ↥E] [Normal F ↥E'], Normal F ↥(E ⊓ E')
-- Init.Data.String.Pattern.Basic
/-- Build an iterator of `SearchStep` corresponding to matches of `pat` along the slice
  `s`. The `SearchStep`s returned by this iterator must contain ranges that are
  adjacent, non-overlapping and cover all of `s`.
   -/
String.Slice.Pattern.ToBackwardSearcher.toSearcher : {ρ : Type} →
  (pat : ρ) →
    {σ : outParam (String.Slice → Type)} →
      [self : String.Slice.Pattern.ToBackwardSearcher pat σ] →
        (s : String.Slice) → Std.Iter (String.Slice.Pattern.SearchStep s)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₁_lt_iff : ∀ {o : Ordinal.{u}}, o.invVeblen₁ < o ↔ o ≠ 0 ∧ o ∉ Set.range Ordinal.gamma
-- Mathlib.MeasureTheory.MeasurableSpace.Pi
/-- Boxes form a π-system.  -/
isPiSystem_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)],
  IsPiSystem (Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s})
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.flip_apply : ∀ {β : Type u_3} {γ : Type u_4} [inst : OmegaCompletePartialOrder β] [inst_1 : OmegaCompletePartialOrder γ]
  {α : Type u_6} (f : α → β →𝒄 γ) (x : β) (y : α), (OmegaCompletePartialOrder.ContinuousHom.flip f) x y = (f y) x
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_isometry_ofLp_infty : ∀ (α : Type u_2) (β : Type u_3) [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β], Isometry WithLp.ofLp
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.Ordering.swap.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Mathlib.Topology.Category.TopCat.Yoneda
ContinuousMap.yonedaPresheaf'_obj : ∀ (Y : Type w') [inst : TopologicalSpace Y] (X : TopCatᵒᵖ),
  (ContinuousMap.yonedaPresheaf' Y).obj X = C(↑(Opposite.unop X), Y)
-- Lean.Language.Basic
/-- Snapshot tree accessor retrieved from `val` before erasure.  -/
Lean.Language.DynamicSnapshot.toSnapshotTreeM : Lean.Language.DynamicSnapshot → Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree
-- Std.Time.Format
Std.Time.DateTime.instRepr : Repr Std.Time.DateTime
-- Mathlib.RingTheory.Valuation.Extension
/-- The class `Valuation.HasExtension vR vA` states that the valuation `vA` on `A` is an extension of
the valuation `vR` on `R`. More precisely, `vR` is equivalent to the comap of the valuation `vA`.
 -/
Valuation.HasExtension : {R : Type u_1} →
  {A : Type u_2} →
    {ΓR : Type u_3} →
      {ΓA : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : Ring A] →
            [inst_2 : LinearOrderedCommMonoidWithZero ΓR] →
              [inst_3 : LinearOrderedCommMonoidWithZero ΓA] → [Algebra R A] → Valuation R ΓR → Valuation A ΓA → Prop
-- Mathlib.Topology.Algebra.Monoid
Filter.TendstoNhdsWithinIio.const_mul : ∀ {α : Type u_2} {𝕜 : Type u_6} [inst : Preorder 𝕜] [inst_1 : Zero 𝕜] [inst_2 : Mul 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [SeparatelyContinuousMul 𝕜] {l : Filter α} {f : α → 𝕜} {b c : 𝕜},
  0 < b →
    ∀ [PosMulStrictMono 𝕜],
      Filter.Tendsto f l (nhdsWithin c (Set.Iio c)) →
        Filter.Tendsto (fun a => b * f a) l (nhdsWithin (b * c) (Set.Iio (b * c)))
-- Mathlib.Data.Int.Log
Int.clog_inv : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ) (r : R), Int.clog b r⁻¹ = -Int.log b r
-- Mathlib.Dynamics.BirkhoffSum.Average
Function.IsFixedPt.birkhoffAverage_eq : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {f : α → α} {x : α},
  Function.IsFixedPt f x → ∀ (g : α → M) {n : ℕ}, ↑n ≠ 0 → birkhoffAverage R f g n x = g x
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.append.inj : ∀ {α : Type u} {a a_1 : Array (Lean.Widget.TaggedText α)},
  Lean.Widget.TaggedText.append a = Lean.Widget.TaggedText.append a_1 → a = a_1
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Given a basis of a module `M₁` over a commutative ring `R`, we get an algebra
equivalence between linear maps `M₁ →ₗ M₁` and square matrices over `R` indexed by the basis.  -/
LinearMap.toMatrixAlgEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {n : Type u_4} →
      [inst_1 : Fintype n] →
        [inst_2 : DecidableEq n] →
          {M₁ : Type u_5} →
            [inst_3 : AddCommMonoid M₁] →
              [inst_4 : Module R M₁] → Module.Basis n R M₁ → (M₁ →ₗ[R] M₁) ≃ₐ[R] Matrix n n R
-- Init.Data.Int.Gcd
Int.gcd_dvd_gcd_mul_right_left : ∀ (a b c : ℤ), a.gcd b ∣ (a * c).gcd b
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_biInter : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set (Submodule R M)), Submodule.span R (⋂ S ∈ s, ↑S) = sInf s
-- Mathlib.Logic.ExistsUnique
/-- Pretty-printing for `ExistsUnique`, following the same pattern as pretty printing for `Exists`.
However, it does *not* merge binders.
 -/
Mathlib.Notation.unexpandExistsUnique : Lean.PrettyPrinter.Unexpander
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.one.inj : ∀ {name name_1 : Lean.TSyntax `Lean.binderIdent},
  Lean.Parser.Tactic.MRefinePat.one name = Lean.Parser.Tactic.MRefinePat.one name_1 → name = name_1
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum.instZero : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalRing A] → [inst_2 : Module R A] → [Nontrivial R] → (a : A) → Zero ↑(quasispectrum R a)
-- Mathlib.Algebra.Ring.Subring.Basic
RingEquiv.subringCongr_symm : ∀ {R : Type u} [inst : NonAssocRing R] {s t : Subring R} (h : s = t),
  (RingEquiv.subringCongr h).symm = RingEquiv.subringCongr ⋯
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Filter.IsIncreasingApproximateUnit.eventually_nonneg : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {l : Filter A},
  l.IsIncreasingApproximateUnit → ∀ᶠ (x : A) in l, 0 ≤ x
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- a concrete equivalence of any two subobject classifiers  -/
CategoryTheory.Subobject.Classifier.uniqueUpToIso : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C) → 𝒞₁.Ω ≅ 𝒞₂.Ω
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendRestrictScalarsAdj.counit_app : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (x : ModuleCat S),
  (ModuleCat.ExtendRestrictScalarsAdj.counit f).app x = ModuleCat.ExtendRestrictScalarsAdj.Counit.map f
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.toSubmodule_mk : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (p : Submodule R M)
  (h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier), ↑{ toSubmodule := p, lie_mem := h } = p
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.instFunLikeNat : {α : Type u_2} → [inst : Preorder α] → FunLike (OmegaCompletePartialOrder.Chain α) ℕ α
-- Mathlib.Data.Fintype.Sets
Set.toFinset_subset : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s] {t : Finset α}, s.toFinset ⊆ t ↔ s ⊆ ↑t
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- If `s` is a closed subspace with finite codimension, any subspace containing `s` is closed.  -/
Submodule.isClosed_mono_of_finiteDimensional_quotient : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E]
  {s t : Submodule 𝕜 E} [FiniteDimensional 𝕜 (E ⧸ s)], IsClosed ↑s → s ≤ t → IsClosed ↑t
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.map_apply_of : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [inst_2 : (i : ι) → CommRing (G' i)]
  {f' : (i j : ι) → i ≤ j → G' i →+* G' j} (g : (i : ι) → G i →+* G' i)
  (hg : ∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)) {i : ι} (x : G i),
  (Ring.DirectLimit.map g hg) ((Ring.DirectLimit.of G (fun x x_1 h => ⇑(f x x_1 h)) i) x) =
    (Ring.DirectLimit.of G' (fun x x_1 h => ⇑(f' x x_1 h)) i) ((g i) x)
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.setValue_eq : ∀ {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) (a : α) (b : β) [inst : (a' : α) → Decidable (a' = a)]
  [inst_1 : (a' : α) → Decidable (f a' = b)], (f.setValue a b) a = b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keysArray_filter!_key : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : α → Bool},
  t.WF → (Std.DTreeMap.Internal.Impl.filter! (fun k x => f k) t).keysArray = Array.filter f t.keysArray
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwKey.mk.sizeOf_spec : ∀ (numGoals : ℕ) (symm : Bool) (nameLength replacementSize : ℕ) (name : String)
  (replacement : Lean.Meta.AbstractMVarsResult),
  sizeOf
      { numGoals := numGoals, symm := symm, nameLength := nameLength, replacementSize := replacementSize, name := name,
        replacement := replacement } =
    1 + sizeOf numGoals + sizeOf symm + sizeOf nameLength + sizeOf replacementSize + sizeOf name + sizeOf replacement
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eq_U_sub_X_mul_U : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.T R n = Polynomial.Chebyshev.U R n - Polynomial.X * Polynomial.Chebyshev.U R (n - 1)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.neighborSet_snd_subgraphOfAdj : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (hvw : G.Adj v w), (G.subgraphOfAdj hvw).neighborSet w = {v}
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory_braiding_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  (X₁ X₂ : CategoryTheory.Arrow C),
  (β_ X₁ X₂).hom.left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushoutSymmetry (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom)).hom
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Limits.spanExt (β_ X₁.left X₂.left) (β_ X₁.left X₂.right) (β_ X₁.right X₂.left) ⋯ ⋯)).hom
-- Mathlib.Tactic.FinCases
/-- If `e` is of the form `x ∈ (A : List α)`, `x ∈ (A : Finset α)`, or `x ∈ (A : Multiset α)`,
return `some α`, otherwise `none`.  -/
Lean.Elab.Tactic.getMemType : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Expr → m (Option Lean.Expr)
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_eq_zero_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [IsDomain R] [IsDomain S]
  [Module.Free R S] [Module.Finite R S] {x : S}, (Algebra.norm R) x = 0 ↔ x = 0
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_add_Iio : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a + x) ⁻¹' Set.Iio b = Set.Iio (b - a)
-- Mathlib.Data.NNReal.Defs
NNReal.instLinearOrder : LinearOrder NNReal
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.toField : {K : Type u_1} → [inst : Field K] → (s : Subfield K) → Field ↥s
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.substFVars' : Array Lean.Name → Aesop.Script.TacticBuilder
-- Mathlib.Computability.TuringMachine.Computable
/-- input resp. output stack  -/
Turing.FinTM2.k₁ : (self : Turing.FinTM2) → self.K
-- Init.Data.List.Lemmas
List.flatten_eq_nil_iff : ∀ {α : Type u_1} {L : List (List α)}, L.flatten = [] ↔ ∀ l ∈ L, l = []
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.const_mul_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S] {f : α → E}
  {l : Filter α} {g : α → S} {c : S},
  c ≠ 0 →
    ∀ {c' : ℝ}, 0 ≤ c' → Asymptotics.IsBigOWith c' l f g → Asymptotics.IsBigOWith (c' * ‖c‖⁻¹) l f fun x => c * g x
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.Λ'.write : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → Γ → Turing.TM1.Stmt Γ Λ σ → Turing.TM1to1.Λ' Γ Λ σ
-- Mathlib.Algebra.Module.NatInt
/-- All `ℤ`-module structures are equal. See also `AddCommGroup.uniqueIntModule`.  -/
AddCommMonoid.subsingletonIntModule : ∀ {M : Type u_3} [inst : AddCommMonoid M], Subsingleton (Module ℤ M)
-- Init.Data.List.MinMaxIdx
List.minIdxOn_nil_eq_iff_false : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : ℕ} (h : [] ≠ []),
  List.minIdxOn f [] h = x ↔ False
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Construct an affine scheme from a scheme. Also see `AffineScheme.mk` for a non-typeclass
version.  -/
AlgebraicGeometry.AffineScheme.of : (X : AlgebraicGeometry.Scheme) → [h : AlgebraicGeometry.IsAffine X] → AlgebraicGeometry.AffineScheme
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubring.topologicalClosure_mono : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalRing R] [inst_2 : IsSemitopologicalRing R]
  {s t : NonUnitalSubring R}, s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Qq.Macro
Qq.Impl.unquoteMVarCore : Lean.Expr → Qq.Impl.UnquoteM Unit
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.exists_frobenius_solution_fractionRing : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a : FractionRing (WittVector p k)},
  a ≠ 0 → ∃ b, b ≠ 0 ∧ ∃ m, (IsFractionRing.ringEquivOfRingEquiv (WittVector.frobeniusEquiv p k)) b * a = ↑p ^ m * b
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.induced : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F] {t : TopologicalSpace F}
  [LocallyConvexSpace 𝕜 F] (f : E →ₗ[𝕜] F), LocallyConvexSpace 𝕜 E
-- Mathlib.Order.Antisymmetrization
AntisymmRel.symm : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, AntisymmRel r a b → AntisymmRel r b a
-- Mathlib.Algebra.Order.Ring.Abs
odd_abs : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Ring α] {a : α}, Odd |a| ↔ Odd a
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.ext_of_ring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] {f g : R →ₗc[R] A}, f 1 = g 1 → f = g
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run'.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (property : [].length = 0),
  List.MergeSort.Internal.mergeSortTR₂.run'✝ le ⟨[], property⟩ = []
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.map_map : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] [inst_4 : CommRing T] [inst_5 : IsLocalRing T] (f : R →+* S) (g : S →+* T)
  (x : IsLocalRing.ResidueField R) [inst_6 : IsLocalHom f] [inst_7 : IsLocalHom g],
  (IsLocalRing.ResidueField.map g) ((IsLocalRing.ResidueField.map f) x) = (IsLocalRing.ResidueField.map (g.comp f)) x
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.mem_of_mem_of_foldl_folder_eq_some : ∀ {n : ℕ} {acc : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool}
  {ls : List (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))}
  {acc' : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool},
  List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder (some acc) ls = some acc' →
    ∀ l ∈ acc.toList, l ∈ acc'.toList
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
/-- The set of solutions to a linear equation `a + f x = b + g y` in a finitely generated monoid is
semilinear.  -/
isSemilinearSet_setOfPred_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [AddMonoid.FG M] {F : Type u_5}
  {G : Type u_6} [inst_3 : FunLike F M N] [AddMonoidHomClass F M N] [inst_5 : FunLike G M N] [AddMonoidHomClass G M N]
  (a b : N) (f : F) (g : G), IsSemilinearSet {x | a + f x = b + g x}
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.familyOfBFamily_enum : ∀ {α : Type u_1} (o : Ordinal.{u_3}) (f : (a : Ordinal.{u_3}) → a < o → α) (i : Ordinal.{u_3}) (hi : i < o),
  o.familyOfBFamily f ((Ordinal.enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) = f i hi
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Matroidᵣ.ofMatroid.inj : ∀ {α : Type u_2} {toMatroid toMatroid_1 : Matroid α},
  { toMatroid := toMatroid } = { toMatroid := toMatroid_1 } → toMatroid = toMatroid_1
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsTwoSided.pow_succ : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} [I.IsTwoSided] (n : ℕ), I ^ (n + 1) = I * I ^ n
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.instRingHomInvPairToRingHomRingEquivSymm : ∀ {R : Type u_5} {S : Type u_6} [inst : CommRing R] [inst_1 : CommRing S] (f : R ≃+* S), RingHomInvPair ↑f ↑f.symm
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the Möbius function converges absolutely at `s` if and only if `re s > 1`.  -/
ArithmeticFunction.LSeriesSummable_moebius_iff : ∀ {s : ℂ}, LSeriesSummable (fun n => ↑(ArithmeticFunction.moebius n)) s ↔ 1 < s.re
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, ∅.size = 0
-- Mathlib.Data.Multiset.UnionInter
Multiset.nodup_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, (s ∪ t).Nodup ↔ s.Nodup ∧ t.Nodup
-- Init.MetaTypes
Lean.Module.mk : Lean.Syntax → Array Lean.Syntax → Lean.Module