mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_eq_prod_of_nonempty : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  {eX eX' : OpenPartialHomeomorph X X'} {eY eY' : OpenPartialHomeomorph Y Y'},
  (eX.prod eY).source.Nonempty → (eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY')
-- Init.Data.Array.Lemmas
Array.replace_append_left : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {xs ys : Array α},
  a ∈ xs → (xs ++ ys).replace a b = xs.replace a b ++ ys
-- Mathlib.Algebra.Ring.Parity
Even.odd_add : ∀ {α : Type u_2} [inst : Semiring α] {a b : α}, Even a → Odd b → Odd (b + a)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_mul : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, PowerSeries.X * φ = φ * PowerSeries.X
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_inter_add_sdiff₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet t μ →
    MeasureTheory.IntegrableOn f s μ → ∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.Order.WithBot
WithBot.toDual_symm : ∀ {α : Type u_1}, WithBot.toDual.symm = WithTop.ofDual
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.toEnd_apply_apply : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x : L)
  (m : M), ((LieModule.toEnd R L M) x) m = ⁅x, m⁆
-- Mathlib.Data.Matrix.Basic
Matrix.piAlgEquiv_apply : ∀ {n : Type u_3} {ι : Type u_14} {β : ι → Type u_15} (R : Type u_16) [inst : CommSemiring R]
  [inst_1 : (i : ι) → Semiring (β i)] [inst_2 : (i : ι) → Algebra R (β i)] [inst_3 : Fintype n] [inst_4 : DecidableEq n]
  (f : Matrix n n ((i : ι) → β i)) (i : ι), (Matrix.piAlgEquiv R) f i = f.map fun x => x i
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instLeftCancelSemigroup : {α : Type u_1} → [LeftCancelSemigroup α] → LeftCancelSemigroup αᵒᵈ
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.isBasis_iff_cover : ∀ {α : Type u_2} [inst : TopologicalSpace α] {B : Set (TopologicalSpace.Opens α)},
  TopologicalSpace.Opens.IsBasis B ↔ ∀ (U : TopologicalSpace.Opens α), ∃ Us ⊆ B, U = sSup Us
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- A family is linearly independent if and only if all of its finite subfamily is
linearly independent.  -/
linearIndependent_iff_finset_linearIndependent : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v ↔ ∀ (s : Finset ι), LinearIndependent R (v ∘ Subtype.val)
-- Init.PropLemmas
exists₄_congr : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4}
  {p q : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop},
  (∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d ↔ q a b c d) →
    ((∃ a b c d, p a b c d) ↔ ∃ a b c d, q a b c d)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.mul_comp : ∀ {R : Type u_1} [inst : CommSemiring R] (p q r : Polynomial R), (p * q).comp r = p.comp r * q.comp r
-- Mathlib.Analysis.Calculus.Deriv.Star
HasStrictDerivAt.star : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {f' : F} {x : 𝕜}
  [TrivialStar 𝕜], HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => star (f x)) (star f') x
-- Mathlib.Order.Max
instNoMinOrderForallOfNonempty : ∀ {ι : Type u} {π : ι → Type u_3} [Nonempty ι] [inst : (i : ι) → Preorder (π i)] [∀ (i : ι), NoMinOrder (π i)],
  NoMinOrder ((i : ι) → π i)
-- Init.Data.BitVec.Lemmas
BitVec.toInt_xor : ∀ {w : ℕ} (x y : BitVec w), (x ^^^ y).toInt = (↑(x.toNat ^^^ y.toNat)).bmod (2 ^ w)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instLTOfPreorder : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [Preorder Y] → [inst_2 : Zero Y] → LT (Function.locallyFinsuppWithin U Y)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instBooleanAlgebra : {α : Type u_1} → [inst : MeasurableSpace α] → BooleanAlgebra (Subtype MeasurableSet)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {X Y : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : X ⟶ Y),
  CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor.map f =
    CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map f
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toStructuredArrow_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X Y : J} (f : X ⟶ Y),
  c.toStructuredArrow.map f = CategoryTheory.StructuredArrow.homMk f ⋯
-- Mathlib.Order.Atoms
isAtomistic_iff : ∀ (α : Type u_2) [inst : PartialOrder α] [inst_1 : OrderBot α],
  IsAtomistic α ↔ ∀ (b : α), ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Cache.ngen : Lean.Meta.LazyDiscrTree.Cache → Lean.NameGenerator
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_singleton : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {i : ι} {v : ι → F} (r : ι → F),
  (Lagrange.interpolate {i} v) r = Polynomial.C (r i)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.tendsto_atBot : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [OrderTopology β],
  Asymptotics.IsEquivalent l u v → Filter.Tendsto u l Filter.atBot → Filter.Tendsto v l Filter.atBot
-- Init.Prelude
/-- Create array `#[]`  -/
Array.mkArray0 : {α : Type u} → Array α
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
/-- For an adjunction `f ⊣ u`, `u` is an absolute left Kan extension of the identity along `f`.
The unit of this Kan extension is given by the unit of the adjunction.  -/
CategoryTheory.Bicategory.Adjunction.isAbsoluteLeftKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {u : b ⟶ a} →
          (adj : CategoryTheory.Bicategory.Adjunction f u) →
            (CategoryTheory.Bicategory.LeftExtension.mk u adj.unit).IsAbsKan
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_units_coe_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α) (u : αˣ), lcm a ↑u = normalize a
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonAssocRing : {R : Type u_1} → {M : Type u_4} → [inst : Ring R] → [AddZeroClass M] → NonAssocRing (AddMonoidAlgebra R M)
-- Mathlib.Data.Bundle
/-- A trivial bundle is equivalent to the product `B × F`.  -/
Bundle.TotalSpace.toProd : (B : Type u_4) → (F : Type u_5) → (Bundle.TotalSpace F fun x => F) ≃ B × F
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, then
for any subset `S` of `K` such that `F(S) / F` is algebraic, the `E(S) / E` and `F(S) / F` have
the same separable degree.  -/
IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] (S : Set K)
  [Algebra.IsAlgebraic F ↥(IntermediateField.adjoin F S)] [IsPurelyInseparable F E],
  Field.sepDegree E ↥(IntermediateField.adjoin E S) = Field.sepDegree F ↥(IntermediateField.adjoin F S)
-- Mathlib.Topology.Instances.Discrete
DiscreteTopology.firstCountableTopology : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α], FirstCountableTopology α
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.cyclesOpIso_inv_op_iCycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {Z : Cᵒᵖ} (h : S.op.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.cyclesOpIso.inv (CategoryTheory.CategoryStruct.comp S.op.iCycles h) =
    CategoryTheory.CategoryStruct.comp S.pOpcycles.op h
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.Rewrites.nonterminal_input_mem : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {u v : List (Symbol T N)},
  r.Rewrites u v → Symbol.nonterminal r.input ∈ u
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Restriction of an `AddSemigroup` hom to its range interpreted as a subsemigroup.  -/
AddHom.srangeRestrict : {M : Type u_1} → [inst : Add M] → {N : Type u_5} → [inst_1 : Add N] → (f : M →ₙ+ N) → M →ₙ+ ↥f.srange
-- Mathlib.Topology.Bornology.Absorbs
absorbs_zero_iff : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [(Bornology.cobounded G₀).NeBot] {E : Type u_3}
  [inst_3 : AddMonoid E] [inst_4 : DistribMulAction G₀ E] {s : Set E}, Absorbs G₀ s 0 ↔ 0 ∈ s
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.orElse_Except : ∀ {α ε : Type u_1} {x : Except ε α} {h : Unit → Except ε α}
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε Std.Do.PostShape.pure)),
  ⦃(Std.Do.wp x).apply (Q.1, fun x => (Std.Do.wp (h ())).apply Q, Q.2.2)⦄ OrElse.orElse x h ⦃Q⦄
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.prod` -/
Meromorphic.fun_prod : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_5} {s : Finset ι} {F : ι → 𝕜 → 𝕜'},
  (∀ σ ∈ s, Meromorphic (F σ)) → Meromorphic fun a => ∏ c ∈ s, F c a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.getD a fallback =
    if h : compare k a = Ordering.eq then cast ⋯ v else t.getD a fallback
-- Mathlib.Algebra.Opposites
PreOpposite.op'.injEq : ∀ {α : Type u_3} (unop' unop'_1 : α), ({ unop' := unop' } = { unop' := unop'_1 }) = (unop' = unop'_1)
-- Std.Net.Addr
Std.Net.instDecidableEqAddressFamily : DecidableEq Std.Net.AddressFamily
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.lift_ι_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A)
  (cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)) (x : M),
  ((CliffordAlgebra.lift Q) ⟨f, cond⟩) ((CliffordAlgebra.ι Q) x) = f x
-- Mathlib.Order.RelSeries
/-- To show a proposition `p` for `xs : RelSeries r` it suffices to show it for all singletons
and to show that when `p` holds for `xs` it also holds for `xs` prepended with one element.

Note: This can also be used to construct data, but it does not have good definitional properties,
since `(p.cons x hx).tail _ = p` is not a definitional equality.
 -/
RelSeries.inductionOn : {α : Type u_1} →
  {r : SetRel α α} →
    (motive : RelSeries r → Sort u_3) →
      ((x : α) → motive (RelSeries.singleton r x)) →
        ((p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)) →
          (p : RelSeries r) → motive p
-- Mathlib.Algebra.DirectSum.Module
/-- Direct sums of isomorphic modules are isomorphic.  -/
DirectSum.congrLinearEquiv : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      {N : ι → Type u_3} →
        [inst_1 : (i : ι) → AddCommMonoid (N i)] →
          [inst_2 : (i : ι) → Module R (N i)] →
            {P : ι → Type u_4} →
              [inst_3 : (i : ι) → AddCommMonoid (P i)] →
                [inst_4 : (i : ι) → Module R (P i)] →
                  ((i : ι) → N i ≃ₗ[R] P i) → (DirectSum ι fun i => N i) ≃ₗ[R] DirectSum ι fun i => P i
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.natDegree_map_of_leadingCoeff_ne_zero : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {p : Polynomial R} (f : R →+* S),
  f p.leadingCoeff ≠ 0 → (Polynomial.map f p).natDegree = p.natDegree
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConst_isPowMul : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 → f c ≠ 0 → IsPowMul ⇑f → IsPowMul (seminormFromConst' c f)
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Matrix.IsHermitian.isClosedEmbedding_cfcAux : ∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜}
  (hA : A.IsHermitian), Topology.IsClosedEmbedding ⇑hA.cfcAux
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_of_mul_le_left : ∀ {α : Type u} [inst : Mul α] [inst_1 : Preorder α] [CanonicallyOrderedMul α] {a b c : α}, a * b ≤ c → a ≤ c
-- Mathlib.Topology.Defs.Filter
/-- A `setoid` version of `Inseparable`, used to define the `SeparationQuotient`.  -/
inseparableSetoid : (X : Type u_1) → [TopologicalSpace X] → Setoid X
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le_cert.match_1.congr_eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (p₁ p₂ : Int.Internal.Linear.Poly)
  (h_1 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k_1 : ℤ) → motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_1))
  (h_2 :
    (k k_1 : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_1 v p))
  (h_3 : (c₁ c₂ : ℤ) → motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂))
  (k k_1 : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
  p₁ = Int.Internal.Linear.Poly.num k →
    p₂ = Int.Internal.Linear.Poly.add k_1 v p →
      (match p₁, p₂ with
        | Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_2 => h_1 k v p k_2
        | Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_2 v p => h_2 k k_2 v p
        | Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ => h_3 c₁ c₂
        | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) ≍
        h_2 k k_1 v p
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.smul_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {B : Type u_6} [inst : SMul B A] (r : B) (M : CStarMatrix m n A) (i : m)
  (j : n), (r • M) i j = r • M i j
-- Mathlib.MeasureTheory.Group.Arithmetic
Multiset.measurable_sum : ∀ {M : Type u_2} {α : Type u_4} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} (l : Multiset (α → M)), (∀ f ∈ l, Measurable f) → Measurable l.sum
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst : Inhabited β], (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) (a : B),
  (CategoryTheory.CategoryStruct.id F).app a = CategoryTheory.CategoryStruct.id (F.obj a)
-- Mathlib.Algebra.Order.Interval.Set.Instances
/-- The coercion from `Set.Ioc 0 1` as a `MonoidHom`.  -/
Set.Ioc.coeMonoidHom : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : PartialOrder R] → [inst_2 : IsStrictOrderedRing R] → ↑(Set.Ioc 0 1) →* R
-- Mathlib.GroupTheory.MonoidLocalization.Lemmas
Submonoid.IsLocalizationMap.pi : ∀ {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [inst : (i : ι) → CommMonoid (M i)]
  [inst_1 : (i : ι) → CommMonoid (N i)] (S : (i : ι) → Submonoid (M i)) {f : (i : ι) → M i → N i},
  (∀ (i : ι), (S i).IsLocalizationMap (f i)) → (Submonoid.pi Set.univ S).IsLocalizationMap (Pi.map f)
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `take`. (Can also be used in lieu of `take` if you know the
index is within the range of the data structure.)

```
takeAux {a, b, c, d} 2 = {a, b}
takeAux {a, b, c, d} 5 = {a, b, c, d}
```  -/
Ordnode.takeAux : {α : Type u_1} → Ordnode α → ℕ → Ordnode α
-- Mathlib.CategoryTheory.Sites.CoverPreserving
CategoryTheory.CompatiblePreserving.compatible : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D},
  CategoryTheory.CompatiblePreserving K G →
    ∀ (ℱ : CategoryTheory.Sheaf K (Type w)) {Z : C} {T : CategoryTheory.Presieve Z}
      {x : CategoryTheory.Presieve.FamilyOfElements (G.op.comp ℱ.obj) T},
      x.Compatible →
        ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
          (hg₂ : T g₂),
          CategoryTheory.CategoryStruct.comp f₁ (G.map g₁) = CategoryTheory.CategoryStruct.comp f₂ (G.map g₂) →
            (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) =
              (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
-- Mathlib.Tactic.Ring.Basic
/-- Evaluate the inverse of a natural number expression.  -/
Mathlib.Tactic.Ring.RingCompute.inv : {u : Lean.Level} →
  {α : Q(Type u)} →
    (_sα : Q(CommSemiring «$α»)) →
      {a : Q(«$α»)} →
        Option Q(CharZero «$α») →
          (_sfα : Q(Semifield «$α»)) →
            Mathlib.Tactic.Ring.RatCoeff a →
              Mathlib.Tactic.AtomM (Option (Mathlib.Tactic.Ring.Common.Result Mathlib.Tactic.Ring.RatCoeff q(«$a»⁻¹)))
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.below.oldAtom : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)}
  {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1 → Prop} {idx : ℕ}
  {map : Std.HashMap α ℕ} {a : α} {n : ℕ} (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map)
  (hlt : idx < decls.size) (hatom : decls[idx] = Std.Sat.AIG.Decl.atom a) (hmap : map[a]? = some n),
  Std.Sat.AIG.RelabelNat.State.Inv2.below hinv → motive idx map hinv → Std.Sat.AIG.RelabelNat.State.Inv2.below ⋯
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} {val val_1 : X.val ⟶ Y.val},
  { val := val } = { val := val_1 } → val = val_1
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.Context.proof : Lean.Meta.Grind.Collector.Context✝ → Lean.Expr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_eq_none : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, a ∉ m → Std.ExtDHashMap.Const.get? m a = none
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.blocks_le : ∀ {n : ℕ} (c : Composition n) {i : ℕ}, i ∈ c.blocks → i ≤ n
-- Lean.Parser.Do
Lean.Parser.Term.doSeq.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- **Alias** of `Localization.AtPrime.eq_maximalIdeal_iff_under_eq`. -/
Localization.AtPrime.eq_maximalIdeal_iff_comap_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [hI : I.IsPrime] {J : Ideal (Localization.AtPrime I)},
  Ideal.under R J = I ↔ J = IsLocalRing.maximalIdeal (Localization.AtPrime I)
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.mem_strictPeriods_iff : ∀ {R : Type u_1} [inst : Ring R] {𝒢 : Subgroup (GL (Fin 2) R)} {x : R},
  x ∈ 𝒢.strictPeriods ↔ Matrix.GeneralLinearGroup.upperRightHom x ∈ 𝒢
-- Std.Sync.SharedMutex
/-- An exclusion primitive that allows a number of readers or at most one writer access to a shared
state of type `α`.
 -/
Std.SharedMutex : Type → Type
-- Init.Data.Range.Polymorphic.Iterators
/-- Internal function that constructs an iterator for a left-unbounded right-closed range `*...=hi`.
This is an internal function.
Use `Ric.iter` instead, which requires
importing `Std.Data.Iterators`.
 -/
Std.Ric.Internal.iter : {α : Type u} → [Std.PRange.Least? α] → Std.Ric α → Std.Iter α
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Combine a family of continuous alternating maps with the same domain and codomains `M' i` into a
continuous alternating map taking values in the space of functions `Π i, M' i`.  -/
ContinuousAlternatingMap.pi : {R : Type u_1} →
  {M : Type u_2} →
    {ι : Type u_6} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : TopologicalSpace M] →
              {ι' : Type u_7} →
                {M' : ι' → Type u_8} →
                  [inst_4 : (i : ι') → AddCommMonoid (M' i)] →
                    [inst_5 : (i : ι') → TopologicalSpace (M' i)] →
                      [inst_6 : (i : ι') → Module R (M' i)] →
                        ((i : ι') → M [⋀^ι]→L[R] M' i) → M [⋀^ι]→L[R] ((i : ι') → M' i)
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.of_comp : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  [h : Algebra.EssFiniteType R T], Algebra.EssFiniteType S T
-- Mathlib.Probability.Distributions.Gamma
ProbabilityTheory.cdf_gammaMeasure_eq_integral : ∀ {a r : ℝ},
  0 < a →
    0 < r →
      ∀ (x : ℝ),
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gammaMeasure a r)) x =
          ∫ (x : ℝ) in Set.Iic x, ProbabilityTheory.gammaPDFReal a r x
-- Mathlib.Algebra.Ring.Opposite
/-- A ring homomorphism `f : R →+* S` such that `f x` commutes with `f y` for all `x, y` defines
a ring homomorphism to `Sᵐᵒᵖ`.  -/
RingHom.toOpposite : {R : Type u_2} →
  {S : Type u_3} →
    [inst : Semiring R] → [inst_1 : Semiring S] → (f : R →+* S) → (∀ (x y : R), Commute (f x) (f y)) → R →+* Sᵐᵒᵖ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.singleton_eq_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {p : α × β}, {p} = ∅.insert p.1 p.2
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.congr_of_eventuallyEq_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → g =ᶠ[nhdsWithin x (insert x s)] f → ContinuousWithinAt g s x
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeff_ofCoeff : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : ℕ →₀ M),
  { coeff := x }.coeff = x