mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.length_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Analysis.CStarAlgebra.Classes
instCommCStarAlgebraForall : {ι : Type u_1} →
  {A : ι → Type u_2} → [Fintype ι] → [(i : ι) → CommCStarAlgebra (A i)] → CommCStarAlgebra ((i : ι) → A i)
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.L1.dist_def : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f g : ↥(MeasureTheory.Lp β 1 μ)), dist f g = (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ).toReal
-- Mathlib.Data.Set.Finite.Basic
Set.card_lt_card : ∀ {α : Type u} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s ⊂ t → Fintype.card ↑s < Fintype.card ↑t
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜),
  HasFDerivAt (fun x => Polynomial.eval x p)
    (ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))) x
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Ring.HasFiniteQuotients.instNorthcottIdealNatCardQuot : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R], Northcott fun p => Submodule.cardQuot p
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Try adding the lemma to the `RefinedDiscrTree`.  -/
Mathlib.Tactic.LibraryRewrite.addRewriteEntry : Lean.Name →
  Lean.ConstantInfo →
    Lean.MetaM
      (List
        (Mathlib.Tactic.LibraryRewrite.RewriteLemma ×
          List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.const_smul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : SMul 𝕜 β] [ContinuousConstSMul 𝕜 β],
  MeasureTheory.StronglyMeasurable f → ∀ (c : 𝕜), MeasureTheory.StronglyMeasurable (c • f)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_eq_nat : ∀ {m : ℕ∞} {n : ℕ}, ↑m = ↑n ↔ m = ↑n
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.prodAssoc_apply : ∀ (R : Type u_3) (M₁ : Type u_4) (M₂ : Type u_5) (M₃ : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (a : (M₁ × M₂) × M₃), (LinearEquiv.prodAssoc R M₁ M₂ M₃) a = AddEquiv.prodAssoc.toFun a
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.of_symm_of : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  (x : TensorProduct R A B), (GradedTensorProduct.of R 𝒜 ℬ).symm ((GradedTensorProduct.of R 𝒜 ℬ) x) = x
-- Mathlib.FieldTheory.SeparableDegree
/-- If a polynomial has separable contraction, then its separable degree is equal to the degree of
the given separable contraction.  -/
Polynomial.HasSeparableContraction.natSepDegree_eq : ∀ {F : Type u} [inst : Field F] {f : Polynomial F} {q : ℕ} [ExpChar F q] (hf : Polynomial.HasSeparableContraction q f),
  f.natSepDegree = hf.degree
-- Mathlib.Order.Atoms
IsAtom.ne_iff_eq_bot : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, IsAtom a → b ≤ a → (b ≠ a ↔ b = ⊥)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.symm_bijective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β],
  Function.Bijective OrderMonoidIso.symm
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.combine_NonnegCoeffs : ∀ {p₁ p₂ : Lean.Grind.CommRing.Poly}, p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.combine p₂).NonnegCoeffs
-- Mathlib.Topology.Maps.Basic
IsOpenMap.interior_preimage_subset_preimage_interior : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ {s : Set Y}, interior (f ⁻¹' s) ⊆ f ⁻¹' interior s
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelComparison_comp_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison f G)
      (CategoryTheory.Limits.kernel.ι (G.map f)) =
    G.map (CategoryTheory.Limits.kernel.ι f)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.inv_fun_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence] (X Y : C) (f : X ⟶ Y),
  F.inv.map (F.map f) =
    CategoryTheory.CategoryStruct.comp (F.asEquivalence.unitInv.app X)
      (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.unit.app Y))
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.bind : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α β : Type u}
  {post : β → Pred} {epost : EPred} (x : m α) (f : α → m β),
  ⦃ Std.Internal.Do.wp x (fun a => Std.Internal.Do.wp (f a) post epost) epost ⦄ x >>= f ⦃ post; epost ⦄
-- Mathlib.ModelTheory.Substructures
Set.Countable.substructure_closure : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] {s : Set M} [Countable ((l : ℕ) × L.Functions l)],
  s.Countable → Countable ↥((FirstOrder.Language.Substructure.closure L).toFun s)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {a b : α} (hab : cmp a b = Ordering.eq) {h' : a ∈ t}, t[a] = t[b]
-- Mathlib.Data.Vector.MapLemmas
List.Vector.map₂_map_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {n : ℕ} (xs : List.Vector α n) (ys : List.Vector β n)
  (f₁ : γ → β → ζ) (f₂ : α → γ),
  List.Vector.map₂ f₁ (List.Vector.map f₂ xs) ys = List.Vector.map₂ (fun x y => f₁ (f₂ x) y) xs ys
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ →
    ∀ {k : α} {v : β} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.instExistsMulOfLE : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] [inst_2 : Mul α] [inst_3 : Mul β] [ExistsMulOfLE α]
  [ExistsMulOfLE β], ExistsMulOfLE (α × β)
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.dvdNotUnit_left_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q r : M}, Associated p q → (DvdNotUnit p r ↔ DvdNotUnit q r)
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.setLIntegral_preCDF_fst : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℚ) {s : Set α},
  MeasurableSet s →
    ∀ [MeasureTheory.IsFiniteMeasure ρ], ∫⁻ (x : α) in s, ProbabilityTheory.preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) s
-- Init.Prelude
MonadLiftT.mk : {m : Type u → Type v} → {n : Type u → Type w} → ({α : Type u} → m α → n α) → MonadLiftT m n
-- Mathlib.Data.List.MinMax
List.maximum_ne_bot_of_length_pos : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α}, 0 < l.length → l.maximum ≠ ⊥
-- Std.Http.Data.Status
/-- 308 Permanent Redirect
 -/
Std.Http.Status.permanentRedirect : Std.Http.Status
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.biSup_mem : ∀ {α : Type u_2} [inst : CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {ι : Type u_5} {t : Set ι} {f : ι → α},
  t.Finite → (∀ i ∈ t, f i ∈ L) → ⨆ i ∈ t, f i ∈ L
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.offset : ∀ {pat s : String.Slice} {pos : s.Pos},
  pat.isEmpty = false → String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s 0 pos.offset
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_map_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → γ} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.map f t) k = Option.map (f k') (Std.DTreeMap.Raw.Const.get? t k)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_Ico : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m '' Set.Ico i j = Set.Ico (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.Algebra.Group.WithOne.Map
WithZero.map₂_coe_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithZero α) (b : β),
  WithZero.map₂ f a ↑b = WithZero.map (fun x => f x b) a
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
/-- The even subalgebras of the algebras with quadratic form `Q` and `-Q` are isomorphic.

Stated another way, `𝒞ℓ⁺(p,q,r)` and `𝒞ℓ⁺(q,p,r)` are isomorphic.  -/
CliffordAlgebra.evenEquivEvenNeg : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (Q : QuadraticForm R M) → ↥(CliffordAlgebra.even Q) ≃ₐ[R] ↥(CliffordAlgebra.even (-Q))
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.nondegenerate_toMatrix₂_iff : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n]
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂) {B : M₁ →ₗ[R] M₂ →ₗ[R] R},
  ((LinearMap.toMatrix₂ b₁ b₂) B).Nondegenerate ↔ B.Nondegenerate
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_of_gt : ∀ {n : ℕ} {i j k : Fin n}, j < k → (i.cycleIcc j) k = k
-- Mathlib.Topology.Order.Compact
ContinuousOn.image_uIcc_eq_Icc : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : TopologicalSpace β] [DenselyOrdered α] [inst_5 : ConditionallyCompleteLinearOrder β]
  [OrderTopology β] {f : α → β} {a b : α},
  ContinuousOn f (Set.uIcc a b) → f '' Set.uIcc a b = Set.Icc (sInf (f '' Set.uIcc a b)) (sSup (f '' Set.uIcc a b))
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNorm_toMatrix : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NontriviallyNormedField α] [NormedAlgebra ℝ α] [inst_4 : DecidableEq n] (f : (n → α) →L[α] m → α),
  ‖LinearMap.toMatrix' ↑f‖ = ‖f‖
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.centerToMulOpposite_apply_coe : ∀ {M : Type u_2} [inst : MulOneClass M] (r : ↥(Subsemigroup.center M)),
  ↑(Submonoid.centerToMulOpposite r) = MulOpposite.op ↑r
-- Mathlib.Topology.Defs.Basic
/-- The union of a family of open sets is an open set.
Use `isOpen_sUnion` in the root namespace instead.  -/
TopologicalSpace.isOpen_sUnion : ∀ {X : Type u} [self : TopologicalSpace X] (s : Set (Set X)),
  (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instDivisionAddCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α],
  Lex.instDivisionAddCommMonoid = { toSubtractionMonoid := Lex.instSubtractionMonoid, add_comm := ⋯ }
-- Mathlib.Order.SetDissipate
/-- For a directed set of sets `s : ℕ → Set α` and `n : ℕ`, there exists `m : ℕ` (maybe
larger than `n`) such that `s m ⊆ dissipate s n`.  -/
Set.exists_subset_dissipate_of_directed : ∀ {α : Type u_1} {s : ℕ → Set α}, Directed (fun x1 x2 => x1 ⊇ x2) s → ∀ (n : ℕ), ∃ m, s m ⊆ Set.dissipate s n
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldr_eq_foldr_keys' : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {l : List ((a : α) × β a)} {f : δ → α → δ} {init : δ},
  List.foldr (fun a b => f b a.fst) init l = List.foldr (fun a b => f b a) init (Std.Internal.List.keys l)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryGT?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGT? k = t₂.getEntryGT? k
-- Mathlib.Algebra.Module.Congruence.Defs
/-- The kernel of a `MulActionHom` as a congruence relation.  -/
SMulCon.ker : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} → {N : Type u_4} → [inst : SMul R M] → [inst_1 : SMul S N] → {φ : R → S} → (M →ₑ[φ] N) → SMulCon R M
-- Mathlib.Algebra.Ring.InjSurj
/-- A type endowed with `0`, `1` and `+` is an additive group with one, if it admits an injective
map that preserves `0`, `1` and `+` to an additive group with one.  See note
[reducible non-instances].  -/
Function.Injective.addGroupWithOne : {R : Type u_1} →
  {S : Type u_3} →
    [inst : Zero S] →
      [inst_1 : One S] →
        [inst_2 : Add S] →
          [inst_3 : SMul ℕ S] →
            [inst_4 : Neg S] →
              [inst_5 : Sub S] →
                [inst_6 : SMul ℤ S] →
                  [inst_7 : NatCast S] →
                    [inst_8 : IntCast S] →
                      [inst_9 : AddGroupWithOne R] →
                        (f : S → R) →
                          Function.Injective f →
                            f 0 = 0 →
                              f 1 = 1 →
                                (∀ (x y : S), f (x + y) = f x + f y) →
                                  (∀ (x : S), f (-x) = -f x) →
                                    (∀ (x y : S), f (x - y) = f x - f y) →
                                      (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                        (∀ (n : ℤ) (x : S), f (n • x) = n • f x) →
                                          (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → AddGroupWithOne S
-- Mathlib.CategoryTheory.Sites.Point.Conservative
/-- [Stacks Tag 00YK](https://stacks.math.columbia.edu/tag/00YK) ((1)) -/
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point},
  P.IsConservativeFamilyOfPoints →
    ∀ (A : Type u') [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
      [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w}
      [inst_4 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_5 : CategoryTheory.ConcreteCategory A FC]
      [(CategoryTheory.forget A).ReflectsIsomorphisms]
      [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)]
      [hJ : J.HasSheafCompose (CategoryTheory.forget A)],
      CategoryTheory.JointlyReflectIsomorphisms fun Φ => Φ.obj.sheafFiber
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.keysArray.eq_1 : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β),
  t.keysArray = Std.DTreeMap.Internal.Impl.foldl (fun l k x => l.push k) (Array.emptyWithCapacity t.size) t
-- Mathlib.RepresentationTheory.FDRep
/-- The underlying `LinearEquiv` of an isomorphism of representations.  -/
FDRep.isoToLinearEquiv : {R : Type u} → {G : Type v} → [inst : CommRing R] → [inst_1 : Monoid G] → {V W : FDRep R G} → (V ≅ W) → ↑V.V ≃ₗ[R] ↑W.V
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesColimit_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [inst_3 : sSupHomClass F α β] {J : Type w} [inst_4 : CategoryTheory.Category.{w', w} J]
  (K : CategoryTheory.Functor J α), CategoryTheory.Limits.PreservesColimit K (↑f).toFunctor
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.mem_iff : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x : R), x ∈ I ↔ I.ringCon x 0
-- Init.Data.List.ToArray
List.zipWithMAux_toArray_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u} {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] (f : α → β → m γ)
  (as : List α) (bs : List β) (xs : Array γ),
  as.toArray.zipWithMAux bs.toArray f 0 xs = do
    let __do_lift ← List.zipWithM f as bs
    pure (xs ++ __do_lift.toArray)
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.span_singleton_absNorm : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] {I : Ideal S},
  Nat.Prime (Ideal.absNorm I) → Ideal.span {↑(Ideal.absNorm I)} = Ideal.comap (algebraMap ℤ S) I
-- Init.Data.Range.Polymorphic.Instances
Std.Rxo.LawfulHasSize.of_closed : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [DecidableLE α] [inst_3 : LT α] [DecidableLT α]
  [Std.LawfulOrderLT α] [Std.IsPartialOrder α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_9 : Std.Rxc.HasSize α] [Std.Rxc.LawfulHasSize α],
  Std.Rxo.LawfulHasSize α
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `g` is meromorphic at `x`, then `f + g` is meromorphic at `x` if and only if `f` is meromorphic
at `x`.
 -/
MeromorphicAt.meromorphicAt_add_iff_meromorphicAt₂ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E}, MeromorphicAt g x → (MeromorphicAt (f + g) x ↔ MeromorphicAt f x)
-- Mathlib.Data.Finset.Disjoint
Finset.mem_disjUnion : ∀ {α : Type u_5} {s t : Finset α} {h : Disjoint s t} {a : α}, a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t
-- Mathlib.Analysis.RCLike.Extend
Module.Dual.extendRCLike_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F),
  fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))
-- Mathlib.Data.Finite.Defs
not_infinite_iff_finite : ∀ {α : Sort u_1}, ¬Infinite α ↔ Finite α
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.inter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β},
  m₁.WF → m₂.WF → (m₁ ∩ m₂).WF
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → HasDerivWithinAt f₁ f' s x
-- Lean.Elab.InfoTree.Main
Lean.Elab.CommandInfo.format : Lean.Elab.ContextInfo → Lean.Elab.CommandInfo → IO Std.Format
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- Auxiliary definition for `forgetToPresheafModuleCatObj`.  -/
PresheafOfModules.forgetToPresheafModuleCatObjObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (X : Cᵒᵖ) → CategoryTheory.Limits.IsInitial X → PresheafOfModules R → Cᵒᵖ → ModuleCat ↑(R.obj X)
-- Init.Grind.Ring.Field
Lean.Grind.Field.of_pow_eq_zero : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α) (n : ℕ), a ^ n = 0 → a = 0
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (u v : V), G.dist u v = (G.edist u v).toNat
-- Mathlib.Data.Seq.Computation
Computation.Terminates.mk : ∀ {α : Type u} {s : Computation α}, (∃ a, a ∈ s) → s.Terminates
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.fst_obj : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R), (CategoryTheory.Comma.fst L R).obj X = X.left
-- Init.Data.List.Monadic
List.filterMapM.loop.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (x : List β),
  List.filterMapM.loop f [] x = pure x.reverse
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.mul_inv_cancel : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (φ : MvPowerSeries σ k),
  MvPowerSeries.constantCoeff φ ≠ 0 → φ * φ⁻¹ = 1
-- Mathlib.Computability.NFA
/-- `M.evalFrom S x` computes all possible paths through `M` with input `x` starting at an element
of `S`.  -/
NFA.evalFrom : {α : Type u} → {σ : Type v} → NFA α σ → Set σ → List α → Set σ
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent.eq_1 : ∀ {R : Type u_1} [inst : Semiring R],
  Polynomial.toLaurent = (AddMonoidAlgebra.mapDomainRingHom R ↑Int.ofNatHom).comp (Polynomial.toFinsuppIso R).toRingHom
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair.parallelPairHom_id : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  {x : CategoryTheory.Limits.WalkingParallelPair},
  CategoryTheory.Limits.parallelPair.parallelPairHom f g (CategoryTheory.CategoryStruct.id x) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.parallelPair.parallelPairObj X Y x)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.isOpen_inter_preimage : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set Y}, IsOpen s → IsOpen (e.source ∩ ↑e ⁻¹' s)
-- ProofWidgets.Component.Basic
ProofWidgets.Component.mk.inj : ∀ {Props : Type} {toModule : Lean.Widget.Module} {«export» : String} {toModule_1 : Lean.Widget.Module}
  {export_1 : String},
  { toModule := toModule, «export» := «export» } = { toModule := toModule_1, «export» := export_1 } →
    toModule = toModule_1 ∧ «export» = export_1
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce_negRev_left_cancel : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeAddGroup.reduce (FreeAddGroup.negRev L ++ L) = []
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.homCategory.ext : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {m n : η ⟶ θ}, (∀ (b : B), m.as.app b = n.as.app b) → m = n
-- Init.Data.ByteArray.Basic
/-- Creates an iterator at the beginning of an array.  -/
ByteArray.mkIterator : ByteArray → ByteArray.Iterator
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.instNonemptyTransvectionStructOfNontrivial : ∀ (n : Type u_1) (R : Type u₂) [CommRing R] [Nontrivial n], Nonempty (Matrix.TransvectionStruct n R)
-- Init.Meta.Defs
/-- Extracts the parsed name from the syntax of an identifier.

Returns `Name.anonymous` if the syntax is malformed.
 -/
Lean.TSyntax.getId : Lean.Ident → Lean.Name
-- Std.Http.Data.Status
Std.Http.Status.variantAlsoNegotiates.sizeOf_spec : sizeOf Std.Http.Status.variantAlsoNegotiates = 1
-- Lean.Expr
/-- `.forallE x t b bi` is now the preferred form.
 -/
Lean.mkForall : Lean.Name → Lean.BinderInfo → Lean.Expr → Lean.Expr → Lean.Expr