mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Set.OrdConnected
Set.image_subtype_val_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [s.OrdConnected] (x y : ↑s), Subtype.val '' Set.Ioc x y = Set.Ioc ↑x ↑y
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.mono_inl_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.FinitaryExtensive C]
  {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.Mono c.inl
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.ext_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtDHashMap α β},
  (∀ (k : α), m₁.get? k = m₂.get? k) → m₁ = m₂
-- Batteries.Data.UInt
UInt8.toUInt32_toNat : ∀ (x : UInt8), x.toUInt32.toNat = x.toNat
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.lt_irrefl : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a : α},
  ¬Std.PRange.UpwardEnumerable.LT a a
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.Scheme.Hom.isOpen_quasiFiniteAt : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f],
  IsOpen {x | AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x}
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.Monic.dvd_iff_fraction_map_dvd_fraction_map : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsIntegrallyClosed R] {p q : Polynomial R},
  p.Monic → q.Monic → (Polynomial.map (algebraMap R K) q ∣ Polynomial.map (algebraMap R K) p ↔ q ∣ p)
-- Mathlib.CategoryTheory.Sites.Plus
/-- The plus construction, a functor sending `P` to `J.plusObj P`.  -/
CategoryTheory.GrothendieckTopology.plusFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type w) →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Functor Cᵒᵖ D)
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.env : Lean.Server.Snapshots.Snapshot → Lean.Environment
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.isBase_of_ground_subset_closure : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Indep I → M.E ⊆ M.closure I → M.IsBase I
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.mk.injEq : ∀ (toGoalState : Lean.Meta.Grind.GoalState) (mvarId : Lean.MVarId) (toGoalState_1 : Lean.Meta.Grind.GoalState)
  (mvarId_1 : Lean.MVarId),
  ({ toGoalState := toGoalState, mvarId := mvarId } = { toGoalState := toGoalState_1, mvarId := mvarId_1 }) =
    (toGoalState = toGoalState_1 ∧ mvarId = mvarId_1)
-- Mathlib.Data.Ineq
/-- The three-element type `Ineq` is used to represent the strength of a comparison between
terms.  -/
Mathlib.Ineq : Type
-- Mathlib.Data.Multiset.ZeroCons
Multiset.singleton_subset : ∀ {α : Type u_1} {s : Multiset α} {a : α}, {a} ⊆ s ↔ a ∈ s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_union_le_size_add_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∪ m₂).size ≤ m₁.size + m₂.size
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonResolveSupport : Lean.ToJson Lean.Lsp.ResolveSupport
-- Mathlib.RepresentationTheory.Continuous.TopRep
_private.Mathlib.RepresentationTheory.Continuous.TopRep.0.TopRep.mk : {k : Type u} →
  {G : Type v} →
    [inst : Ring k] →
      [inst_1 : TopologicalSpace k] →
        [inst_2 : Monoid G] →
          (V : Type w) →
            [hV1 : AddCommGroup V] →
              [hV2 : Module k V] →
                [hV3 : TopologicalSpace V] →
                  [hV4 : IsTopologicalAddGroup V] → [hV5 : ContinuousSMul k V] → ContRepresentation k G V → TopRep k G
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_div_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] (c : 𝕜 → 𝕜') (d : 𝕜'), derivWithin (fun x => c x / d) s x = derivWithin c s x / d
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.degree_restriction : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R}, p.restriction.degree = p.degree
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
StrongDual.symm_toWeakDual : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E],
  StrongDual.toWeakDual.symm = WeakDual.toStrongDual
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forIn_eq : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''}
  [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : Std.IteratorLoop α m n]
  [hl : Std.LawfulIteratorLoop α m n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : Std.IterM m β}
  {init : γ} {f : β → γ → n (ForInStep γ)},
  forIn it init f =
    Std.IterM.DefaultConsumers.forIn' (fun x x_1 f x_2 => monadLift x_2 >>= f) γ (fun x x_1 x_2 => True) it init
      it.IsPlausibleIndirectOutput ⋯ fun out x acc => do
      let __do_lift ← f out acc
      pure ⟨__do_lift, trivial⟩
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
Measurable.map_measurableSpace_eq : ∀ {X : Type u_3} {Z : Type u_5} [inst : MeasurableSpace X] [StandardBorelSpace X] [inst_2 : MeasurableSpace Z]
  [MeasurableSpace.CountablySeparated Z] {f : X → Z},
  Measurable f → Function.Surjective f → MeasurableSpace.map f inst = inst_2
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.isUniformInducing_toLp : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β], IsUniformInducing (WithLp.toLp p)
-- Init.Data.Array.Range
Array.range_add : ∀ {n m : ℕ}, Array.range (n + m) = Array.range n ++ Array.map (fun x => n + x) (Array.range m)
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
/-- **Chevalley's Theorem**: The image of a locally constructible set under a
morphism of finite presentation is locally constructible.  -/
AlgebraicGeometry.Scheme.Hom.isLocallyConstructible_image : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [hf : AlgebraicGeometry.LocallyOfFinitePresentation f]
  [AlgebraicGeometry.QuasiCompact f] {s : Set ↥X},
  Topology.IsLocallyConstructible s → Topology.IsLocallyConstructible (⇑f '' s)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_3 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.xor with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_3 ()
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
_private.Mathlib.AlgebraicTopology.SimplicialSet.Degenerate.0.SSet.unique_nonDegenerate.isIso_factorThruImage_g : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := n })} {m₁ m₂ : ℕ} {f₁ : { len := n } ⟶ { len := m₁ }}
  (hf₁ : CategoryTheory.SplitEpi f₁) {y₁ : ↑(X.nonDegenerate m₁)},
  x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁ →
    ∀ {f₂ : { len := n } ⟶ { len := m₂ }} {y₂ : X.obj (Opposite.op { len := m₂ })},
      x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) y₂ →
        CategoryTheory.IsIso (CategoryTheory.Limits.factorThruImage (SSet.unique_nonDegenerate.g✝ hf₁ f₂))
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Function.locallyFinsuppWithin.toClosedBall_support_subset_closedBall : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] {r : ℝ} (f : Function.locallyFinsupp E ℤ),
  ((Function.locallyFinsuppWithin.toClosedBall r) f).support ⊆ Metric.closedBall 0 |r|
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.of_boundedUnder_im : ∀ {l : Filter ℂ},
  Filter.Tendsto Complex.re l Filter.atTop →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l Complex.im →
      Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l Complex.im → Complex.IsExpCmpFilter l
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_inv : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i j : I} (h : i = j),
  (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C h).inv = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.rightUnitor_naturality_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [inst_5 :
    ∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  {X X' : CategoryTheory.GradedObject I C} (φ : X ⟶ X') {Z : CategoryTheory.GradedObject I C} (h : X' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom φ
        (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.rightUnitor X').hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.rightUnitor X).hom
      (CategoryTheory.CategoryStruct.comp φ h)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_spec_mk : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x y : R) (hy : y ∈ M),
  IsLocalization.mk' S x ⟨y, hy⟩ * (algebraMap R S) y = (algebraMap R S) x
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- Every self-adjoint operator on an inner product space is symmetric.  -/
IsSelfAdjoint.isSymmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {A : E →L[𝕜] E}, IsSelfAdjoint A → (↑A).IsSymmetric
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.WithGeneratedByTopology.continuous_equiv`. -/
continuous_to_deltaGenerated : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y],
  Continuous ⇑Topology.WithGeneratedByTopology.equiv
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.restrictAddMonoidHom.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_5} [inst_6 : TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} (G : Type u_10) [inst_9 : AddMonoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffAdd I' n G] {U V : TopologicalSpace.Opens N} (h : U ≤ V),
  ContMDiffMap.restrictAddMonoidHom I I' G h =
    { toFun := fun f => ⟨⇑f ∘ Set.inclusion h, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.sumMap : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {W : Type u_5} [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
  IsHomeomorph f → IsHomeomorph g → IsHomeomorph (Sum.map f g)
-- Aesop.Tree.Data
Aesop.GoalData.successProbability : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.Percent
-- Init.Data.Iterators.Basic
/-- Makes a single step with the given iterator `it`, potentially emitting a value and providing a
succeeding iterator. If this function is used recursively, termination can sometimes be proved with
the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
 -/
Std.Iter.step : {α β : Type w} → [inst : Std.Iterator α Id β] → (it : Std.Iter β) → it.Step
-- Mathlib.Algebra.Group.Equiv.Opposite
AddOpposite.opMulEquiv_toEquiv : ∀ {α : Type u_2} [inst : Mul α], ↑AddOpposite.opMulEquiv = AddOpposite.opEquiv
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (vec : aig.RefVec len)
  (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func],
  aig.decls.size ≤ (Std.Sat.AIG.RefVec.fold aig vec func).aig.decls.size
-- Mathlib.Logic.Equiv.Set
/-- If sets `s` and `t` are separated by a decidable predicate, then `s ∪ t` is equivalent to
`s ⊕ t`.  -/
Equiv.Set.union' : {α : Type u_3} →
  {s t : Set α} → (p : α → Prop) → [DecidablePred p] → (∀ x ∈ s, p x) → (∀ x ∈ t, ¬p x) → ↑(s ∪ t) ≃ ↑s ⊕ ↑t
-- Mathlib.GroupTheory.Perm.Fin
Fin.sign_cycleRange : ∀ {n : ℕ} (i : Fin n), Equiv.Perm.sign i.cycleRange = (-1) ^ ↑i
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.neg_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a : X ⟶ Y), -a = 0 - a
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.instSMulCommClass : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommGroup M] [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : Module R M]
  [inst_7 : Module S M] [inst_8 : Module A M] (Q : QuadraticForm A M) [inst_9 : IsScalarTower R A M]
  [inst_10 : IsScalarTower S A M], SMulCommClass R S (CliffordAlgebra Q)
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.comp.match_1.eq_3 : ∀ {C : Type u_1}
  (motive : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Sort u_2)
  (x : CategoryTheory.WithInitial C) (_X : C)
  (h_1 :
    (_X _Y _Z : C) →
      motive (CategoryTheory.WithInitial.of _X) (CategoryTheory.WithInitial.of _Y) (CategoryTheory.WithInitial.of _Z))
  (h_2 :
    (x : CategoryTheory.WithInitial C) →
      (_X : C) → motive CategoryTheory.WithInitial.star x (CategoryTheory.WithInitial.of _X))
  (h_3 :
    (x : CategoryTheory.WithInitial C) →
      (_X : C) → motive x (CategoryTheory.WithInitial.of _X) CategoryTheory.WithInitial.star)
  (h_4 :
    (_Y : C) →
      (x : CategoryTheory.WithInitial C) → motive (CategoryTheory.WithInitial.of _Y) CategoryTheory.WithInitial.star x)
  (h_5 : Unit → motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star),
  (match x, CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.of _Z =>
      h_1 _X _Y _Z
    | CategoryTheory.WithInitial.star, x, CategoryTheory.WithInitial.of _X => h_2 x _X
    | x, CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.star => h_3 x _X
    | CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.star, x => h_4 _Y x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star => h_5 ()) =
    h_3 x _X
-- Mathlib.Data.Nat.Nth
/-- An alternative recursive definition of `Nat.nth`: `Nat.nth s n` is the infimum of `x ∈ s` such
that `Nat.nth s k < x` for all `k < n`, if this set is nonempty. We do not assume that the set is
nonempty because we use the same "garbage value" `0` both for `sInf` on `ℕ` and for `Nat.nth s n`
for `n ≥ #s`.  -/
Nat.nth_eq_sInf : ∀ (p : ℕ → Prop) (n : ℕ), Nat.nth p n = sInf {x | p x ∧ ∀ k < n, Nat.nth p k < x}
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided : ∀ {R : Type u_1} [inst : Ring R], CanLift (Ideal R) (TwoSidedIdeal R) ⇑TwoSidedIdeal.asIdeal fun x => x.IsTwoSided
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- `HasExactColimitsOfShape (Finset (Discrete J)) C` implies `HasExactColimitsOfShape (Discrete J) C`
 -/
CategoryTheory.hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] (J : Type u_1)
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) C]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete J)) C]
  [CategoryTheory.HasExactColimitsOfShape (Finset (CategoryTheory.Discrete J)) C],
  CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.H : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (self : FermatLastTheoremForThreeGen.Solution'✝ hζ),
  FermatLastTheoremForThreeGen.Solution'.a✝ self ^ 3 + FermatLastTheoremForThreeGen.Solution'.b✝ self ^ 3 =
    ↑(FermatLastTheoremForThreeGen.Solution'.u✝ self) * FermatLastTheoremForThreeGen.Solution'.c✝ self ^ 3
-- Mathlib.Analysis.Complex.Poisson
/-- **Poisson integral formula** for ℂ-differentiable functions on arbitrary disks in the complex plane,
formulated with the Poisson kernel of integration expanded.
 -/
DiffContOnCl.circleAverage_poissonKernel_smul' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ} [CompleteSpace E]
  {c : ℂ},
  DiffContOnCl ℂ f (Metric.ball c R) →
    w ∈ Metric.ball c R →
      Real.circleAverage (fun z => ((‖z - c‖ ^ 2 - ‖w - c‖ ^ 2) / ‖z - c - (w - c)‖ ^ 2) • f z) c R = f w
-- Mathlib.NumberTheory.Real.Irrational
irrational_mul_natCast_iff : ∀ {n : ℕ} {x : ℝ}, Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x
-- Lean.PrettyPrinter.Delaborator.Metavariable
/-- Constructs a `?m` term using the name of `m` or its index. Does not add terminfo.
The metavariable does not need to be type correct in the current local context.
 -/
Lean.PrettyPrinter.Delaborator.delabMVarAux : Lean.MVarId → Lean.PrettyPrinter.Delaborator.DelabM Lean.Term
-- Init.Data.Nat.Lemmas
Nat.pow_two_sub_pow_two : ∀ (a b : ℕ), a ^ 2 - b ^ 2 = (a + b) * (a - b)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.mul_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (f g : A →A[R] A) (x : A), (f * g) x = f (g x)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- Construct an isomorphism of group objects by giving an isomorphism between the underlying
objects and checking compatibility with unit and multiplication only in the forward direction.  -/
CategoryTheory.CommGrp.mkIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {G H : CategoryTheory.CommGrp C} →
          (e : G.X ≅ H.X) →
            autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
                _auto_93✝ →
              autoParam
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
                      CategoryTheory.MonObj.mul)
                  _auto_95✝ →
                (G ≅ H)
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Multiset.prod_map_neg : ∀ {M : Type u_2} [inst : CommMonoid M] [inst_1 : HasDistribNeg M] (s : Multiset M),
  (Multiset.map Neg.neg s).prod = (-1) ^ s.card * s.prod
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.CheckResult.progress.sizeOf_spec : sizeOf Lean.Meta.Grind.CheckResult.progress = 1
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.State.set : Lean.Meta.Sym.AlphaShareCommon.State → Lean.PHashSet Lean.Meta.Sym.AlphaKey
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_eq_zero : ∀ {x : ℝ}, ↑x = 0 ↔ x = 0
-- Lean.Parser.Term
Lean.Parser.Termination.suffix.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.AssertExists
/-- `importPathMessage env idx` produces a message laying out an import chain from `idx` to the
current module. The output is of the form
```
Lean.Init,
  which is imported by Lean.Elab.Command,
  which is imported by Lean.Elab.AssertExists,
  which is imported by this file.
```
if `env` is an `Environment` and `idx` is the module index of `Lean.Init`.  -/
Lean.Elab.Command.importPathMessage : Lean.Environment → Lean.ModuleIdx → Lean.MessageData
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ofSurjective_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (val : ι → S)
  (h : Function.Surjective ⇑(MvPolynomial.aeval val)) (a : ι), (Algebra.Generators.ofSurjective val h).val a = val a
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top : ∀ {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α] ⦃x : α⦄, x ≠ ⊤ → x + -x = 0
-- Std.Http.Data.Headers.Name
/-- Standard Expect header name
 -/
Std.Http.Header.Name.expect : Std.Http.Header.Name
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- If `F.mapCone (cone U)` is a limit cone,
then `SheafConditionEqualizerProducts.fork` is an equalizer.
 -/
TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitSheafConditionForkOfIsLimitMapCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op) →
                CategoryTheory.Limits.IsLimit (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_le_coeIdeal : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_3) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {I J : Ideal R}, ↑I ≤ ↑J ↔ I ≤ J
-- Mathlib.Analysis.Convex.Basic
Monotone.convex_ge : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Monotone f → ∀ (r : β), Convex 𝕜 {x | r ≤ f x}
-- Batteries.Data.List.Basic
/-- Left-biased version of `List.zipWith`. `zipWithLeft' f as bs` applies `f` to each
pair of elements `aᵢ ∈ as` and `bᵢ ∈ bs`. If `bs` is shorter than `as`, `f` is
applied to `none` for the remaining `aᵢ`. Returns the results of the `f`
applications and the remaining `bs`.
```
zipWithLeft' prod.mk [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
zipWithLeft' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
```
 -/
List.zipWithLeft' : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → Option β → γ) → List α → List β → List γ × List β