mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Valuation.Quotient
AddValuation.comap_onQuot_eq : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (J : Ideal R)
  (v : AddValuation (R ⧸ J) Γ₀), (AddValuation.comap (Ideal.Quotient.mk J) v).onQuot ⋯ = v
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.equivUnitsAffineMap_symm_apply_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁), (AffineEquiv.equivUnitsAffineMap.symm u) a = ↑u a
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZif.mk : Std.Time.TimeZone.TZif.TZifV1 → Option Std.Time.TimeZone.TZif.TZifV2 → Std.Time.TimeZone.TZif.TZif
-- Mathlib.RepresentationTheory.Basic
Representation.finsupp_single : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {α : Type u_3} {A : Type u_4}
  [inst_2 : AddCommMonoid A] [inst_3 : Module k A] (ρ : Representation k G A) (g : G) (x : α) (a : A),
  (((ρ.finsupp α) g) fun₀ | x => a) = fun₀ | x => (ρ g) a
-- Mathlib.Analysis.Analytic.Basic
/-- If a function `f` is analytic on a set `s` and `g` is linear, then `g ∘ f` is analytic
on `s`.  -/
ContinuousLinearMap.comp_analyticOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {s : Set E} (g : F →L[𝕜] G),
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (⇑g ∘ f) s
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smulCommClass_set : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α γ] [inst_1 : SMul β γ] [SMulCommClass α β γ],
  SMulCommClass α β (Set γ)
-- Mathlib.Topology.Algebra.Monoid.Defs
Filter.Tendsto.const_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] {α : Type u_2} {f : α → M}
  {x : Filter α} {a : M} (b : M), Filter.Tendsto f x (nhds a) → Filter.Tendsto (fun x => b + f x) x (nhds (b + a))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Chord
/-- A chord of a walk `p` is an edge of `G` between two vertices of `p` which is not one
of the edges of `p`.  -/
SimpleGraph.Walk.IsChord : {V : Type u_1} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → Sym2 V → Prop
-- Std.Do.PostCond
Std.Do.ExceptConds.and.eq_3 : ∀ (ε : Type u) (ps_2 : Std.Do.PostShape) (x_2 y_2 : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps_2)),
  (x_2 ∧ₑ y_2) = (fun e => spred(x_2.1 e ∧ y_2.1 e), x_2.2 ∧ₑ y_2.2)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
RingHom.quotientKerEquivOfSurjective_symm_comp : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} (hf : Function.Surjective ⇑f),
  (RingHom.quotientKerEquivOfSurjective hf).symm.toRingHom.comp f = Ideal.Quotient.mk (RingHom.ker f)
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- `shiftIso (m + n)` is determined by `shiftIso m` and `shiftIso n`.  -/
CategoryTheory.SingleFunctors.shiftIso_add : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (self : CategoryTheory.SingleFunctors C D A) (n m a a' a'' : A)
  (ha' : n + a = a') (ha'' : m + a' = a''),
  self.shiftIso (m + n) a a'' ⋯ =
    (self.functor a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd D m n) ≪≫
      ((self.functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫
        CategoryTheory.Functor.isoWhiskerRight (self.shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫
          self.shiftIso n a a' ha'
-- Mathlib.Data.List.Map2
List.zipRight'_nil_left : ∀ {α : Type u} {β : Type v} (bs : List β), [].zipRight' bs = (List.map (fun b => (none, b)) bs, [])
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.derivation_ext_iff : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] {D₁ D₂ : Derivation R (MvPolynomial σ R) A},
  D₁ = D₂ ↔ ∀ (i : σ), D₁ (MvPolynomial.X i) = D₂ (MvPolynomial.X i)
-- Lean.Language.Basic
Lean.Language.instInhabitedSnapshotTreeTransform : Inhabited Lean.Language.SnapshotTreeTransform
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.ContextualizedCompletionInfo.info : Lean.Server.Completion.ContextualizedCompletionInfo → Lean.Elab.CompletionInfo
-- Lean.Meta.Basic
/-- key produced using `Config.toKey`.  -/
Lean.Meta.InfoCacheKey.configKey : Lean.Meta.InfoCacheKey → UInt64
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsQuasiInverse.eq_1 : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] (u : V₃ →ₗ[K] V₂) (v : V₂ →ₗ[K] V₃),
  u.IsQuasiInverse v = (u.IsLeftQuasiInverse v ∧ u.IsRightQuasiInverse v)
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.symm : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {f : ℝ → X} {a b : ℝ},
  AbsolutelyContinuousOnInterval f a b → AbsolutelyContinuousOnInterval f b a
-- Lean.Declaration
Lean.DefinitionVal.mk.injEq : ∀ (toConstantVal : Lean.ConstantVal) (value : Lean.Expr) (hints : Lean.ReducibilityHints)
  (safety : Lean.DefinitionSafety) (all : List Lean.Name) (toConstantVal_1 : Lean.ConstantVal) (value_1 : Lean.Expr)
  (hints_1 : Lean.ReducibilityHints) (safety_1 : Lean.DefinitionSafety) (all_1 : List Lean.Name),
  ({ toConstantVal := toConstantVal, value := value, hints := hints, safety := safety, all := all } =
      { toConstantVal := toConstantVal_1, value := value_1, hints := hints_1, safety := safety_1, all := all_1 }) =
    (toConstantVal = toConstantVal_1 ∧ value = value_1 ∧ hints = hints_1 ∧ safety = safety_1 ∧ all = all_1)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.rotateR.fun_cases_unfolding : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll r : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Prop),
  (∀ (lr : Std.DTreeMap.Internal.Impl α β),
      lr.size < Std.DTreeMap.Internal.ratio * ll.size →
        motive lr (Std.DTreeMap.Internal.Impl.singleR k v lk lv ll lr r)) →
    (¬Std.DTreeMap.Internal.Impl.leaf.size < Std.DTreeMap.Internal.ratio * ll.size →
        motive Std.DTreeMap.Internal.Impl.leaf
          (Std.DTreeMap.Internal.Impl.singleR k v lk lv ll Std.DTreeMap.Internal.Impl.leaf r)) →
      (∀ (ls : ℕ) (lk_1 : α) (lv_1 : β lk_1) (ll_1 lr : Std.DTreeMap.Internal.Impl α β),
          ¬(Std.DTreeMap.Internal.Impl.inner ls lk_1 lv_1 ll_1 lr).size < Std.DTreeMap.Internal.ratio * ll.size →
            motive (Std.DTreeMap.Internal.Impl.inner ls lk_1 lv_1 ll_1 lr)
              (Std.DTreeMap.Internal.Impl.doubleR k v lk lv ll lk_1 lv_1 ll_1 lr r)) →
        ∀ (lr : Std.DTreeMap.Internal.Impl α β), motive lr (Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll lr r)
-- Mathlib.GroupTheory.Torsion
/-- The image of a surjective torsion group homomorphism is torsion.  -/
IsMulTorsion.of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {f : G →* H},
  Function.Surjective ⇑f → IsMulTorsion G → IsMulTorsion H
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- **Alias** of `spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius`.

---

**Gelfand's formula**: Given an element `a : A` of a complex Banach algebra, the
`spectralRadius` of `a` is the limit of the sequence `‖a ^ n‖₊ ^ (1 / n)`.  -/
spectrum.gelfand_formula : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] (a : A),
  Filter.Tendsto (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop (nhds (spectralRadius ℂ a))
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.traceAddMonoidHom_apply : ∀ (n : Type u_3) (R : Type u_6) [inst : Fintype n] [inst_1 : AddCommMonoid R] (A : Matrix n n R),
  (Matrix.traceAddMonoidHom n R) A = A.trace
-- Init.Data.Nat.Lemmas
Nat.max_min_distrib_left : ∀ (a b c : ℕ), max a (min b c) = min (max a b) (max a c)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.map : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : α → β),
  l.HasBasis p s → (Filter.map f l).HasBasis p fun i => f '' s i
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_isZero_homology : ∀ {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.HasHomology], S.Exact ↔ CategoryTheory.Limits.IsZero S.homology
-- Mathlib.GroupTheory.Index
AddSubgroup.instFiniteIndex_addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G) [H.FiniteIndex], (H.addSubgroupOf K).FiniteIndex
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.leftUnitor η).hom.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
-- Lean.Elab.Do.InferControlInfo
/-- The number of times the block wires the enclosing continuation into its elaborated expression.
Consumed by `withDuplicableCont` to decide whether to introduce a join point (`> 1`).
 -/
Lean.Elab.Do.ControlInfo.numRegularExits : Lean.Elab.Do.ControlInfo → ℕ
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The forgetful functor from the over category creates any connected limit.  -/
CategoryTheory.Over.createsLimitsOfShapeForgetOfIsConnected : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [CategoryTheory.IsConnected J] → {B : C} → CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.Over.forget B)
-- Mathlib.Topology.UnitInterval
unitInterval.mem_unitIntervalSubmonoid : ∀ {x : ℝ}, x ∈ unitInterval.submonoid ↔ x ∈ unitInterval
-- Mathlib.Data.Sum.Interval
Finset.mem_sumLexLift : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f₁ : α₁ → β₁ → Finset γ₁} {f₂ : α₂ → β₂ → Finset γ₂} {g₁ : α₁ → β₂ → Finset γ₁} {g₂ : α₁ → β₂ → Finset γ₂}
  {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂} {c : γ₁ ⊕ γ₂},
  c ∈ Finset.sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ a₁ b₁ c₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ c = Sum.inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, a = Sum.inl a₁ ∧ b = Sum.inr b₂ ∧ c = Sum.inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, a = Sum.inl a₁ ∧ b = Sum.inr b₂ ∧ c = Sum.inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ c = Sum.inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConstC : Lean.Grind.CommRing.Poly → ℤ → ℕ → Lean.Grind.CommRing.Poly
-- Init.Core
Ne.symm : ∀ {α : Sort u} {a b : α}, a ≠ b → b ≠ a
-- Mathlib.Order.Interval.Set.ProjIcc
Set.coe_projIcc : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α) (h : a ≤ b) (x : α), ↑(Set.projIcc a b h x) = max a (min b x)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Consumer.normal.injEq : ∀ (promise promise_1 : IO.Promise (Option Std.Http.Chunk)),
  (Std.Http.Body.Channel.Consumer.normal✝ promise = Std.Http.Body.Channel.Consumer.normal✝ promise_1) =
    (promise = promise_1)
-- Mathlib.Order.Bounds.Basic
IsLUB.upperBounds_eq : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsLUB s a → upperBounds s = Set.Ici a
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_lt_ofNat : ∀ {p : ℝ} {n : ℕ} [inst : n.AtLeastTwo], ENNReal.ofReal p < OfNat.ofNat n ↔ p < OfNat.ofNat n
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
contMDiff_iff_contDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'}, ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f ↔ ContDiff 𝕜 n f
-- Init.Data.String.Subslice
String.Slice.startInclusive_toSubslice : ∀ {s : String.Slice}, s.toSubslice.startInclusive = s.startPos
-- Mathlib.Algebra.Group.Basic
smul_ite : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul β α] (p : Prop) [inst_1 : Decidable p] (a b : α) (c : β),
  (c • if p then a else b) = if p then c • a else c • b
-- Mathlib.GroupTheory.Coset.Basic
/-- The natural embedding
`H ⧸ (⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H`.  -/
AddSubgroup.quotientiInfAddSubgroupOfEmbedding : {α : Type u_1} →
  [inst : AddGroup α] →
    {ι : Type u_2} →
      (f : ι → AddSubgroup α) →
        (H : AddSubgroup α) → ↥H ⧸ (⨅ i, f i).addSubgroupOf H ↪ (i : ι) → ↥H ⧸ (f i).addSubgroupOf H
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_max : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] [AddLeftMono α] (a b c : α), a + max b c = max (a + b) (a + c)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {fallback v : β}, (t.insertIfNew k v).getD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then v else t.getD a fallback
-- Init.Data.String.Lemmas.Splits
/-- We say that `p` splits `s` into `t₁` and `t₂` if `s = t₁ ++ t₂` and `p` is the position between `t₁`
and `t₂`.
 -/
String.Pos.Splits : {s : String} → s.Pos → String → String → Prop
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eVariationOn_leftLim_le : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α}, IsOpen s → eVariationOn (Function.leftLim f) s ≤ eVariationOn f s
-- Mathlib.Tactic.CrossRefAttribute
/-- The main parser for LMFDB identifiers: it accepts lower case words with `.` in between.
The words can also contain underscores and digits.  -/
Mathlib.CrossRef.lmfdbIdNoAntiquot : Lean.Parser.Parser
-- Lean.Elab.Tactic.Grind.Config
Lean.Elab.Tactic.elabOrderConfig : Lean.Syntax → optParam Lean.Grind.OrderConfig { } → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Grind.Config
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- Semilinear sets are closed under projection (from `ι ⊕ κ → M` to `ι → M` by taking `Sum.inl` on
the index). It is a special case of `IsSemilinearSet.image`.  -/
IsSemilinearSet.proj : ∀ {M : Type u_1} {ι : Type u_3} {κ : Type u_4} [inst : AddCommMonoid M] {s : Set (ι ⊕ κ → M)},
  IsSemilinearSet s → IsSemilinearSet {x | ∃ y, Sum.elim x y ∈ s}
-- Mathlib.CategoryTheory.Action.Basic
Action.hasForgetToV : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        {FV : V → V → Type u_3} →
          {CV : V → Type u_4} →
            [inst_2 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
              [inst_3 : CategoryTheory.ConcreteCategory V FV] → CategoryTheory.HasForget₂ (Action V G) V
-- Mathlib.Analysis.Normed.Module.Convex
Metric.closedBall.eq_1 : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α) (ε : ℝ), Metric.closedBall x ε = {y | dist y x ≤ ε}
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_smulRight : ∀ {M₁ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁] {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {R : Type u_9} {S : Type u_10} [inst_4 : Semiring R]
  [inst_5 : Semiring S] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R S] [inst_9 : Module S M₂]
  [inst_10 : IsScalarTower R S M₂] [inst_11 : TopologicalSpace S] [inst_12 : ContinuousSMul S M₂] (c : M₁ →L[R] S)
  (f : M₂), ↑(c.smulRight f) = (↑c).smulRight f
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_roc_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi + 1
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_sInf : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] {x : M} {S : Set (ClosedSubmodule R M)}, x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s
-- Init.Data.Int.Order
Int.le.dest : ∀ {a b : ℤ}, a ≤ b → ∃ n, a + ↑n = b
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating twice is equivalent to rotating by the sum of the angles.  -/
Orientation.rotation_rotation : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ₁ θ₂ : Real.Angle) (x : V),
  (o.rotation θ₁) ((o.rotation θ₂) x) = (o.rotation (θ₁ + θ₂)) x
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filterMapTR.go.match_3.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → Array β → Sort u_3) (acc : Array β)
  (h_1 : (acc : Array β) → motive [] acc) (h_2 : (a : α) → (as : List α) → (acc : Array β) → motive (a :: as) acc),
  (match [], acc with
    | [], acc => h_1 acc
    | a :: as, acc => h_2 a as acc) =
    h_1 acc
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.injective_comp : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (h : L.Equiv N P), Function.Injective h.comp
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.Hom.instModule : {R : Type u} →
  [inst : Ring R] →
    {M N : ModuleCat R} →
      {S : Type u_1} → [inst_1 : Semiring S] → [inst_2 : Module S ↑N] → [SMulCommClass R S ↑N] → Module S (M ⟶ N)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The internal hom functor given by the monoidal closed structure.  -/
CategoryTheory.MonoidalClosed.internalHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.MonoidalClosed C] → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C C)
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.instAddCommMonoidElemForallObjCompForgetLinearMapIdCarrierSections : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          AddCommMonoid ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Std.IterStep.successor.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3) (it : α) (out : β)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it out with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_1 it out
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A B : CategoryTheory.Endofunctor.Algebra F} {f g : A ⟶ B},
  f = g ↔ autoParam (f.f = g.f) CategoryTheory.Endofunctor.Algebra.ext._auto_1
-- Mathlib.Computability.Language
Language.reverse_reverse : ∀ {α : Type u_1} (l : Language α), l.reverse.reverse = l
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_zero_right_eq_nil : ∀ {m : ℕ}, (m...0).toList = []
-- Mathlib.GroupTheory.PGroup
/-- finite p-groups with different p have coprime orders  -/
IsPGroup.coprime_card_of_ne : ∀ {G : Type u_1} [inst : Group G] {G₂ : Type u_2} [inst_1 : Group G₂] (p₁ p₂ : ℕ) [hp₁ : Fact (Nat.Prime p₁)]
  [hp₂ : Fact (Nat.Prime p₂)],
  p₁ ≠ p₂ →
    ∀ (H₁ : Subgroup G) (H₂ : Subgroup G₂) [Finite ↥H₁] [Finite ↥H₂],
      IsPGroup p₁ ↥H₁ → IsPGroup p₂ ↥H₂ → (Nat.card ↥H₁).Coprime (Nat.card ↥H₂)
-- Init.Data.String.Lemmas.Pattern.Split.Pred
String.toList_split_prop : ∀ {s : String} {p : Char → Prop} [inst : DecidablePred p],
  List.map String.Slice.copy (s.split p).toList =
    List.map String.ofList (List.splitOnP (fun b => decide (p b)) s.toList)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The `v`-adic norm of an integer is 1 if and only if it is not in the ideal.  -/
NumberField.FinitePlace.norm_eq_one_iff_notMem : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x : R),
  ‖(NumberField.FinitePlace.embedding v) ((algebraMap R K) x)‖ = 1 ↔ x ∉ v.asIdeal
-- Mathlib.Data.Num.Basic
instOneZNum : One ZNum
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The univariate polynomials `Φₙ` congruent to `φₙ`.  -/
WeierstrassCurve.Φ : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → ℤ → Polynomial R
-- Mathlib.MeasureTheory.Measure.Stieltjes
Monotone.stieltjesFunction_eq : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] [inst_2 : OrderTopology R] {f : R → ℝ}
  (hf : Monotone f) (x : R), ↑hf.stieltjesFunction x = Function.rightLim f x
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : InfSet γ]
  (f : sInfHom β γ) (g : sInfHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsLimitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)],
  (P.limitsClosure J).IsClosedUnderIsomorphisms
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial_pos : ∀ (n k : ℕ), 0 < (n + 1).ascFactorial k
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonAssocSemiring : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [MulOneClass M] → NonAssocSemiring (MonoidAlgebra R M)
-- Mathlib.Dynamics.Flow
/-- The map `ϕ t` as a homeomorphism.  -/
Flow.toHomeomorph : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] → [inst_1 : TopologicalSpace α] → [inst_2 : AddGroup τ] → Flow τ α → τ → α ≃ₜ α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.equiv_iff_toList_perm_toList : ∀ {α : Type u} {β : Type v} (m₁ m₂ : Std.DHashMap.Raw α fun x => β),
  m₁.Equiv m₂ ↔ (Std.DHashMap.Raw.Const.toList m₁).Perm (Std.DHashMap.Raw.Const.toList m₂)
-- Mathlib.Algebra.MvPolynomial.Cardinal
MvPolynomial.cardinalMk_eq_max_lift : ∀ {σ : Type u} {R : Type v} [inst : CommSemiring R] [Nonempty σ] [Nontrivial R],
  Cardinal.mk (MvPolynomial σ R) =
    max (max (Cardinal.lift.{u, v} (Cardinal.mk R)) (Cardinal.lift.{v, u} (Cardinal.mk σ))) Cardinal.aleph0
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_le_iff_sle : ∀ (a b : BitVec 16), Int16.ofBitVec a ≤ Int16.ofBitVec b ↔ a.sle b = true
-- Mathlib.Algebra.Category.Ring.Under.Basic
AlgEquiv.toUnder_inv_right_apply : ∀ {R : CommRingCat} {A B : Type u} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra (↑R) A]
  [inst_3 : Algebra (↑R) B] (f : A ≃ₐ[↑R] B) (b : B),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f.toUnder.inv)) b = f.symm b
-- Mathlib.Data.QPF.Multivariate.Constructions.Quot
/-- `mvFunctor` instance for `Quot1` with well-behaved `R`  -/
MvQPF.Quot1.mvFunctor : {n : ℕ} →
  {F : TypeVec.{u} n → Type u} →
    (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) →
      [inst : MvFunctor F] →
        (∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : α.Arrow β), R a b → R (MvFunctor.map f a) (MvFunctor.map f b)) →
          MvFunctor (MvQPF.Quot1 R)
-- Batteries.Data.List.Basic
List.zipWithLeft.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (x : List β), List.zipWithLeft f [] x = []