mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Card
Finset.card_eq_succ_iff_cons : ∀ {α : Type u_1} {s : Finset α} {n : ℕ}, s.card = n + 1 ↔ ∃ a t, ∃ (h : a ∉ t), Finset.cons a t h = s ∧ t.card = n
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.StrictOrLazy.strict.sizeOf_spec : ∀ {α β : Type} [inst : SizeOf α] [inst_1 : SizeOf β] (a : α), sizeOf (Lean.Widget.StrictOrLazy.strict a) = 1 + sizeOf a
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.inv_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R) (n : ℤ), A⁻¹ ^ n = (A ^ n)⁻¹
-- Mathlib.Order.Basic
forall_ge_iff_le : ∀ {α : Type u_2} [inst : Preorder α] {a b : α}, (∀ ⦃c : α⦄, a ≤ c → b ≤ c) ↔ b ≤ a
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Multiset.esymm_pair_two : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R), (x ::ₘ {y}).esymm 2 = x * y
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The identity refinement of a pre-`0`-hypercover.  -/
CategoryTheory.PreZeroHypercover.Hom.id : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {S : C} → (E : CategoryTheory.PreZeroHypercover S) → E.Hom E
-- Mathlib.LinearAlgebra.Dimension.Finite
rank_zero_iff_forall_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M], Module.rank R M = 0 ↔ ∀ (x : M), x = 0
-- Mathlib.Order.Hom.Basic
OrderEmbedding.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (f : α ↪o β), f.comp (OrderEmbedding.id β) = f
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentations.mk.inj : ∀ {presentations presentations_1 : Array ProofWidgets.ExprPresentationData},
  { presentations := presentations } = { presentations := presentations_1 } → presentations = presentations_1
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.toEquivalence_unitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [inst_2 : ∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)]
  [inst_3 : ∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : C),
  adj.toEquivalence.unitIso.inv.app X = CategoryTheory.inv (adj.unit.app X)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Topology.IsClosedEmbedding.map_tprod : ∀ {ι : Type u_4} {α : Type u_5} {α' : Type u_6} {G : Type u_7} [inst : CommMonoid α] [inst_1 : CommMonoid α']
  [inst_2 : TopologicalSpace α] [inst_3 : TopologicalSpace α'] [T2Space α'] (f : ι → α) {L : SummationFilter ι} {g : G}
  [inst_5 : FunLike G α α'] [MonoidHomClass G α α'],
  Topology.IsClosedEmbedding ⇑g → g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)
-- Mathlib.Topology.Order.Lattice
ContinuousOn.finset_inf' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {t : Set X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (s.inf' hne f) t
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core.sizeOf_spec : ∀ (e : Lean.Expr) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core e lhs rhs) = 1 + sizeOf e + sizeOf lhs + sizeOf rhs
-- Mathlib.Topology.MetricSpace.HausdorffDimension
IsometryEquiv.dimH_univ : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] (e : X ≃ᵢ Y),
  dimH Set.univ = dimH Set.univ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Construct a structured arrow from a morphism.  -/
CategoryTheory.StructuredArrow.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} → {Y : C} → {T : CategoryTheory.Functor C D} → (S ⟶ T.obj Y) → CategoryTheory.StructuredArrow S T
-- Mathlib.Analysis.Calculus.FDeriv.Prod
/-- A variant of `hasFDerivAtFilter_finCons` where the derivative variables are free on the RHS
instead.  -/
hasFDerivAtFilter_finCons' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ}
  {l : Filter (E × E)},
  HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') l ↔
    HasFDerivAtFilter φ φ' l ∧ HasFDerivAtFilter φs φs' l
-- Aesop.Builder.NormSimp
_private.Aesop.Builder.NormSimp.0.Aesop.getSimpEntriesForConst : Lean.Name → Lean.MetaM (Array Lean.Meta.SimpEntry)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_span_le_card : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
  (Submodule.span R s).spanRank ≤ Cardinal.mk ↑s
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharTwoJEqZeroNF_spec : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2],
  W.a₁ = 0 → (W.toCharTwoJEqZeroNF • W).IsCharTwoJEqZeroNF
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.norm_orthogonalProjectionOnto_apply`. -/
Submodule.norm_orthogonalProjection_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] {v : E}, v ∈ K → ‖K.orthogonalProjectionOnto v‖ = ‖v‖
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (x : Associates ↥(nonZeroDivisors R)),
  ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) x) =
    ↑((Ideal.associatesEquivIsPrincipal R) ↑(associatesNonZeroDivisorsEquiv.symm x))
-- Mathlib.Data.Finsupp.Basic
/-- Combine finitely supported functions over `{a // P a}` and `{a // ¬P a}`, by case-splitting on
`P a`.  -/
Finsupp.piecewise : {α : Type u_1} →
  {M : Type u_12} →
    [inst : Zero M] → {P : α → Prop} → [DecidablePred P] → (Subtype P →₀ M) → ({ a // ¬P a } →₀ M) → α →₀ M
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_of_not_isPrime`. -/
Ideal.ramificationIdx'_of_not_isPrime : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S],
  ¬q.IsPrime → q.ramificationIdx R = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₆_of_isCharTwoJNeZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2], W.b₆ = 0
-- Mathlib.Combinatorics.Schnirelmann
/-- The Schnirelmann density is increasing with the set.  -/
schnirelmannDensity_le_of_subset : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {B : Set ℕ} [inst_1 : DecidablePred fun x => x ∈ B],
  A ⊆ B → schnirelmannDensity A ≤ schnirelmannDensity B
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
UniqueDiffWithinAt.smul_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E} {G : Type u_4} [inst_3 : GroupWithZero G]
  [inst_4 : DistribMulAction G E] [ContinuousConstSMul G E] [SMulCommClass G 𝕜 E] {c : G},
  c ≠ 0 → (UniqueDiffWithinAt 𝕜 (c • s) (c • x) ↔ UniqueDiffWithinAt 𝕜 s x)
-- Batteries.Lean.Expr
/-- Like `withApp` but ignores metadata.  -/
Lean.Expr.withApp' : {α : Sort u_1} → Lean.Expr → (Lean.Expr → Array Lean.Expr → α) → α
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
/-- Even though `p.restrictScalars S` has type `Submodule S M`, it is still an `R`-module.  -/
Submodule.restrictScalars.origModule : (S : Type u_1) →
  (R : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Semiring S] →
            [inst_3 : Module S M] →
              [inst_4 : Module R M] →
                [inst_5 : SMul S R] →
                  [inst_6 : IsScalarTower S R M] → (p : Submodule R M) → Module R ↥(Submodule.restrictScalars S p)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.instFullUnderToUnder : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor D T) [F.Full], (CategoryTheory.StructuredArrow.toUnder X F).Full
-- Mathlib.Order.CompleteLattice.Defs
toDual_sSup : ∀ {α : Type u_1} [inst : SupSet α] (s : Set α), OrderDual.toDual (sSup s) = sInf (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.MemLp.piecewise : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {s : Set α} {f : α → ε}
  [inst_2 : DecidablePred fun x => x ∈ s] {g : α → ε},
  MeasurableSet s →
    MeasureTheory.MemLp f p (μ.restrict s) →
      MeasureTheory.MemLp g p (μ.restrict sᶜ) → MeasureTheory.MemLp (s.piecewise f g) p μ
-- Mathlib.Topology.DenseEmbedding
/-- This is a shortcut for `hs.isDenseInducing_val.extend f`. It is useful because if `s : Set α`
is dense then the coercion `(↑) : s → α` automatically satisfies `IsUniformInducing` and
`IsDenseInducing` so this gives access to the theorems satisfied by a uniform extension by simply
mentioning the density hypothesis.  -/
Dense.extend : {α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [TopologicalSpace β] → {s : Set α} → Dense s → (↑s → β) → α → β
-- Std.Async.TCP
/-- Gets the remote address of the client socket.
 -/
Std.Async.TCP.Socket.Client.getPeerName : Std.Async.TCP.Socket.Client → IO Std.Net.SocketAddress
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀_zero : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → Zero (G i)] [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)], DirectLimit.map₀ f 0 = 0
-- Mathlib.Tactic.Translate.Core
/-- Apply attributes to the original and translated declarations.  -/
Mathlib.Tactic.Translate.applyAttributes : Mathlib.Tactic.Translate.TranslateData →
  Mathlib.Tactic.Translate.Config → Lean.Name → Lean.Name → Lean.Elab.TermElabM (Array Lean.Name)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [inst_3 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A]
  (G₀ : CategoryTheory.Sheaf J₀ A) (X : C) (i i' : (data X).I₀) (j : (data X).I₁ i i') {Z : A}
  (h : G₀.obj.obj (Opposite.op ((data X).Y j)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i)
      (CategoryTheory.CategoryStruct.comp (G₀.obj.map ((data X).p₁ j).op) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i')
      (CategoryTheory.CategoryStruct.comp (G₀.obj.map ((data X).p₂ j).op) h)
-- Lean.Meta.Diagnostics
/-- We use below that this returns `m` unchanged if `s.isEmpty`
 -/
Lean.Meta.appendSection : Array Lean.MessageData → Lean.Name → String → Lean.Meta.DiagSummary → optParam Bool true → Array Lean.MessageData
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.of_obj : ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Module.Finite R S] [inst_4 : Algebra.Etale R S], (CommAlgCat.FiniteEtale.of R S).obj = CommAlgCat.of R S
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.continuous_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : TopologicalSpace X],
  Continuous ⇑Metric.Snowflaking.toSnowflaking
-- Lean.Meta.Tactic.Grind.Extension
/-- A constraint of the form `size lhs < n`. The `lhs` is one of the bound variables.
The size is computed ignoring implicit terms, but sharing is not taken into account.
 -/
Lean.Meta.Grind.EMatchTheoremConstraint.sizeLt : ℕ → ℕ → Lean.Meta.Grind.EMatchTheoremConstraint
-- Init.Grind.Interactive
/-- * `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`,
  or else fails.
* `case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses
  with inaccessible names to the given names.
* `case tag₁ | tag₂ => tac` is equivalent to `(case tag₁ => tac); (case tag₂ => tac)`.
 -/
Lean.Parser.Tactic.Grind.case : Lean.ParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.hom_inv_rightUnitor : ∀ {R : Type u} [inst : CommSemiring R] {M : SemimoduleCat R},
  SemimoduleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv = ↑(TensorProduct.rid R ↑M).symm
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.symm_apply_eq : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (f : Equidecomp X G) {x y : X},
  x ∈ f.target → y ∈ f.source → (↑f.symm.toPartialEquiv x = y ↔ x = ↑f.toPartialEquiv y)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_succ_eq_bot`. -/
lowerCentralSeries_succ_eq_bot : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) {n : ℕ},
  S.lowerCentralSeries n ≤ Subgroup.center G → S.lowerCentralSeries (n + 1) = ⊥
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- Let `S` be the localization of `R` at `p` and `N` be a localization of `M` at `p`.
This is the localization of an `R`-submodule of `M` viewed as an `S`-submodule of `N`.  -/
Submodule.localized' : {R : Type u_1} →
  (S : Type u_2) →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Algebra R S] →
                      [inst_7 : Module S N] →
                        [IsScalarTower R S N] →
                          (p : Submonoid R) →
                            [IsLocalization p S] →
                              (f : M →ₗ[R] N) → [IsLocalizedModule p f] → Submodule R M → Submodule S N
-- Mathlib.Algebra.Module.LinearMap.End
/-- Each element of the monoid defines a linear map.

This is a stronger version of `DistribSMul.toAddMonoidHom`.  -/
DistribSMul.toLinearMap : (R : Type u_1) →
  {S : Type u_3} →
    (M : Type u_4) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [inst_3 : DistribSMul S M] → [SMulCommClass S R M] → S → M →ₗ[R] M
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_eq_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β} {h : a ∈ m},
  Std.ExtDHashMap.Const.get m a h = Std.ExtDHashMap.Const.getD m a fallback
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.theory_model_iff : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.ElementaryEmbedding M N) (T : L.Theory), M ⊨ T ↔ N ⊨ T
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- A partial map is an `S`-map if the underlying morphism is.  -/
AlgebraicGeometry.Scheme.PartialMap.IsOver : {X Y : AlgebraicGeometry.Scheme} → (S : AlgebraicGeometry.Scheme) → [X.Over S] → [Y.Over S] → X.PartialMap Y → Prop
-- Mathlib.Computability.Reduce
ComputablePred.computable_of_manyOneReducible : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
  p ≤₀ q → ComputablePred q → ComputablePred p
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.LocalGeneratorsData.isLocallyFree : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.LocalGeneratorsData) [q.IsLocallyFreeData], M.IsLocallyFree
-- Init.Data.Subtype.Order
Subtype.instMaxEqOr : ∀ {α : Type u} [inst : Max α] [inst_1 : Std.MaxEqOr α] {P : α → Prop}, Std.MaxEqOr (Subtype P)
-- Mathlib.Topology.Connected.Basic
isConnected_range : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [ConnectedSpace α] {f : α → β},
  Continuous f → IsConnected (Set.range f)
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instIsInducedOppositeOpOp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.IsInduced], Φ.op.IsInduced
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.mk.inj : ∀ {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {toFun : UpperHalfPlane → ℂ}
  {slash_action_eq' : ∀ γ ∈ Γ, SlashAction.map k γ toFun = toFun} {toFun_1 : UpperHalfPlane → ℂ}
  {slash_action_eq'_1 : ∀ γ ∈ Γ, SlashAction.map k γ toFun_1 = toFun_1},
  { toFun := toFun, slash_action_eq' := slash_action_eq' } =
      { toFun := toFun_1, slash_action_eq' := slash_action_eq'_1 } →
    toFun = toFun_1
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprMVarId_mathlib : Lean.ToExpr Lean.MVarId
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (f : x ⟶ y) (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).map f).snd.app X_1 =
    ψ.right.map (f.snd.app X_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.size_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.size = t₂.size
-- Mathlib.Data.ZMod.QuotientRing
/-- `ℤ` modulo the ideal generated by `n : ℕ` is `ZMod n`.  -/
Int.quotientSpanNatEquivZMod : (n : ℕ) → ℤ ⧸ Ideal.span {↑n} ≃+* ZMod n
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonneg_antisymm : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d] {a : ℤ√↑d}, a.Nonneg → (-a).Nonneg → a = 0
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.iInf_mul'` for the general case, and `ENNReal.iInf_mul_of_ne` for another special
case that assumes `a ≠ 0` but does not require `Nonempty ι`.  -/
ENNReal.iInf_mul : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι],
  (a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0) → (⨅ i, f i) * a = ⨅ i, f i * a
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getValueCastD : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [LawfulBEq α] → (a : α) → List ((a : α) × β a) → β a → β a
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly_succ : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (d : ℕ),
  p.hilbertPoly (d + 1) = ∑ i ∈ p.support, p.coeff i • Polynomial.preHilbertPoly F d i
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.trustSubst : Lean.Option Bool
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.eq_iff : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M) {x y : G},
  f x = f y ↔ -y + x ∈ f.ker
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfLocalizations_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P} {x : N},
  (f.mulEquivOfLocalizations k) x = (f.lift ⋯) x
-- Mathlib.Analysis.Normed.Group.Continuity
comap_norm_nhds_zero : ∀ {E : Type u_4} [inst : SeminormedAddGroup E], Filter.comap norm (nhds 0) = nhds 0
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.submodule_mk : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v : V)
  (hv : v ≠ 0), (Projectivization.mk K v hv).submodule = K ∙ v
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃}
  (chosenPullback : CategoryTheory.Limits.ChosenPullback h₁₂.p₂ h₂₃.p₁) (p : chosenPullback.pullback ⟶ S)
  (p₁ : chosenPullback.pullback ⟶ X₁) (p₃ : chosenPullback.pullback ⟶ X₃) (l : h₁₃.LiftStruct p₁ p₃ p)
  (hp₁ :
    autoParam (CategoryTheory.CategoryStruct.comp chosenPullback.p₁ h₁₂.p₁ = p₁)
      CategoryTheory.Limits.ChosenPullback₃.hp₁._autoParam)
  (hp₃ :
    autoParam (CategoryTheory.CategoryStruct.comp chosenPullback.p₂ h₂₃.p₂ = p₃)
      CategoryTheory.Limits.ChosenPullback₃.hp₃._autoParam)
  (chosenPullback_1 : CategoryTheory.Limits.ChosenPullback h₁₂.p₂ h₂₃.p₁) (p_1 : chosenPullback_1.pullback ⟶ S)
  (p₁_1 : chosenPullback_1.pullback ⟶ X₁) (p₃_1 : chosenPullback_1.pullback ⟶ X₃) (l_1 : h₁₃.LiftStruct p₁_1 p₃_1 p_1)
  (hp₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp chosenPullback_1.p₁ h₁₂.p₁ = p₁_1)
      CategoryTheory.Limits.ChosenPullback₃.hp₁._autoParam)
  (hp₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp chosenPullback_1.p₂ h₂₃.p₂ = p₃_1)
      CategoryTheory.Limits.ChosenPullback₃.hp₃._autoParam),
  ({ chosenPullback := chosenPullback, p := p, p₁ := p₁, p₃ := p₃, l := l, hp₁ := hp₁, hp₃ := hp₃ } =
      { chosenPullback := chosenPullback_1, p := p_1, p₁ := p₁_1, p₃ := p₃_1, l := l_1, hp₁ := hp₁_1, hp₃ := hp₃_1 }) =
    (chosenPullback = chosenPullback_1 ∧ p ≍ p_1 ∧ p₁ ≍ p₁_1 ∧ p₃ ≍ p₃_1 ∧ l ≍ l_1)
-- Mathlib.Algebra.Ring.Defs
neg_mul_eq_mul_neg : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -(a * b) = a * -b
-- Mathlib.NumberTheory.SmoothNumbers
/-- All `m`, `0 < m < n` are `n`-smooth numbers  -/
Nat.mem_smoothNumbers_of_lt : ∀ {m n : ℕ}, 0 < m → m < n → m ∈ n.smoothNumbers
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_Ioc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m '' Set.Ioc i j = Set.Ioc (Fin.castAdd m i) (Fin.castAdd m j)
-- Init.Data.SInt.Lemmas
Int32.toInt64_ofNat : ∀ {n : ℕ}, n ≤ 2147483647 → (OfNat.ofNat n).toInt64 = OfNat.ofNat n
-- Mathlib.Order.Interval.Set.Basic
Set.isEmpty_Iio_zero : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], IsEmpty ↑(Set.Iio 0)