mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f` is an immersion at `x`, it maps its domain chart's target `(h.domChart.extend I).target`
to its codomain chart's target `(h.domChart.extend J).target`.

Roig and Domingues' [roigdomingues1992] definition of immersions only asks for this inclusion
between the targets of the local charts: using mathlib's formalisation conventions, that condition
is *slightly* weaker than `source_subset_preimage_source`: the latter implies that
`h.codChart.extend J ∘ f` maps `h.domChart.source` to
`(h.codChart.extend J).target = (h.codChart.extend I) '' h.codChart.source`,
but that does *not* imply `f` maps `h.domChart.source` to `h.codChart.source`;
a priori `f` could map some point `f ∘ h.domChart.extend I x ∉ h.codChart.source` into the target.
Note that this difference only occurs because of our design using junk values;
this is not a mathematically meaningful difference.

At the same time, this condition is fairly weak: it is implied, for instance, by `f` being
continuous at `x` (see `mk_of_continuousAt`), which is easy to ascertain in practice.

See `target_subset_preimage_target` for a version stated using preimages instead of images.
 -/
Manifold.IsImmersionAtOfComplement.map_target_subset_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x),
  (⇑h.equiv ∘ fun x => (x, 0)) '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
AffineMap.restrict.surjective : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : AffineSubspace k P₁}
  {F : AffineSubspace k P₂} [inst_7 : Nonempty ↥E] [inst_8 : Nonempty ↥F] (h : AffineSubspace.map φ E = F),
  Function.Surjective ⇑(φ.restrict ⋯)
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- `ModuleCat.Hom.hom` bundled as an additive equivalence.  -/
ModuleCat.homAddEquiv : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → (M ⟶ N) ≃+ (↑M →ₗ[R] ↑N)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.completeSpace_iff : ∀ {α : Type u_1} [inst : UniformSpace α], CompleteSpace (TopologicalSpace.NonemptyCompacts α) ↔ CompleteSpace α
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `f : X → Y` is Lipschitz continuous on `s`, then `dimH (f '' s) ≤ dimH s`.  -/
LipschitzOnWith.dimH_image_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {K : NNReal} {f : X → Y} {s : Set X},
  LipschitzOnWith K f s → dimH (f '' s) ≤ dimH s
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- If `S` satisfies going-down as an `R`-algebra and `P` lies over `p`, the height of `P` is equal
to the height of `p` plus the height of the image of `P` in `S ⧸ p S`
(Matsumura 13.B Th. 19 (2)).
 -/
Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {S : Type u_2} [inst_2 : CommRing S] [inst_3 : Algebra R S]
  [IsNoetherianRing S] [Algebra.HasGoingDown R S] (p : Ideal R) [p.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p],
  P.height = p.height + (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) P).height
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.le_centralizer_iff : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ Subgroup.centralizer ↑K ↔ K ≤ Subgroup.centralizer ↑H
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addHaarContent_outerMeasure_self_pos : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G), 0 < (MeasureTheory.Measure.haar.addHaarContent K₀).outerMeasure ↑K₀
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_nil_iff_mem_support : ∀ {V : Type u_1} {G : SimpleGraph V} {u v v' : V} (p : G.Walk u v), SimpleGraph.Walk.nil.IsSubwalk p ↔ v' ∈ p.support
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyπ_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology] (φ : S₁ ⟶ S₂)
  {Z : C} (h : S₂.leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.leftHomologyπ
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ)
      (CategoryTheory.CategoryStruct.comp S₂.leftHomologyπ h)
-- Mathlib.Order.Preorder.Finite
Set.Finite.exists_lt_map_eq_of_forall_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] {t : Set β} {f : α → β} [Infinite α],
  (∀ (a : α), f a ∈ t) → t.Finite → ∃ a b, a < b ∧ f a = f b
-- Mathlib.Analysis.Complex.Basic
Complex.equivRealProd_apply_le : ∀ (z : ℂ), ‖Complex.equivRealProd z‖ ≤ ‖z‖
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_lt_toNNRat_iff : ∀ {p q : ℚ}, 0 < p → (q.toNNRat < p.toNNRat ↔ q < p)
-- Mathlib.Topology.Connected.Basic
isPreconnected_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, IsPreconnected (connectedComponent x)
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Position.mk.injEq : ∀ (line character line_1 character_1 : ℕ),
  ({ line := line, character := character } = { line := line_1, character := character_1 }) =
    (line = line_1 ∧ character = character_1)
-- Init.Data.SInt.IntToBitVec
ISize.lt_iff_toBitVec64_slt : ∀ {a b : ISize} (h : System.Platform.numBits = 64), a < b ↔ (a.toBitVec64 h).slt (b.toBitVec64 h) = true
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLikeOrderEmbedding_apply : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] (f : C(X, ℝ)),
  (ContinuousMap.realToRCLikeOrderEmbedding X 𝕜) f = ContinuousMap.realToRCLike 𝕜 f
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.IsMinimalPrime.isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] {I p : Ideal R}, I.IsMinimalPrime p → p.IsPrime
-- Mathlib.Algebra.Group.Defs
/-- If all multiplications cancel on the left then every element is left-regular.  -/
IsLeftRegular.all : ∀ {R : Type u_2} [inst : Mul R] [IsLeftCancelMul R] (g : R), IsLeftRegular g
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.LazyEntry.mk.injEq : ∀ (previous : Option Lean.Meta.RefinedDiscrTree.ExprInfo) (stack : List Lean.Meta.RefinedDiscrTree.StackEntry)
  (mctx : Lean.MetavarContext) (labelledStars? : Option (Array Lean.MVarId))
  (computedKeys : List Lean.Meta.RefinedDiscrTree.Key) (previous_1 : Option Lean.Meta.RefinedDiscrTree.ExprInfo)
  (stack_1 : List Lean.Meta.RefinedDiscrTree.StackEntry) (mctx_1 : Lean.MetavarContext)
  (labelledStars?_1 : Option (Array Lean.MVarId)) (computedKeys_1 : List Lean.Meta.RefinedDiscrTree.Key),
  ({ previous := previous, stack := stack, mctx := mctx, labelledStars? := labelledStars?,
        computedKeys := computedKeys } =
      { previous := previous_1, stack := stack_1, mctx := mctx_1, labelledStars? := labelledStars?_1,
        computedKeys := computedKeys_1 }) =
    (previous = previous_1 ∧
      stack = stack_1 ∧ mctx = mctx_1 ∧ labelledStars? = labelledStars?_1 ∧ computedKeys = computedKeys_1)
-- Mathlib.Algebra.Star.Module
/-- The skew-adjoint part of an element of a star module, as a linear map.  -/
skewAdjointPart : (R : Type u_1) →
  {A : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : StarMul R] →
        [inst_2 : TrivialStar R] →
          [inst_3 : AddCommGroup A] →
            [inst_4 : Module R A] →
              [inst_5 : StarAddMonoid A] → [inst_6 : StarModule R A] → [Invertible 2] → A →ₗ[R] ↥(skewAdjoint A)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_contract_eq_contract_sdiff : ∀ {α : Type u_1} (M : Matroid α) (C₁ C₂ : Set α), (M.contract C₁).contract C₂ = (M.contract C₁).contract (C₂ \ C₁)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.Algebra.Order.Ring.Interval
/-- Let `k : ℤ`. If its multiple of `r > 0` in a strict ordered ring lies strictly between
the preceding and succeeding multiples `r * (m - 1)` and `r * (m + 1)`, then `k = m`.  -/
IsStrictOrderedRing.int_eq_of_mul_mem_Ioo : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {r : R},
  0 < r → ∀ {k m : ℤ}, r * ↑k ∈ Set.Ioo (r * ↑(m - 1)) (r * ↑(m + 1)) → k = m
-- Mathlib.Tactic.Translate.GuessName
/-- Helper for `fixAbbreviation`.
Note: this function has a quadratic number of recursive calls, but is not a performance
bottleneck.  -/
Mathlib.Tactic.GuessName.fixAbbreviationAux : Mathlib.Tactic.GuessName.GuessNameData → List String → List String → String
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between a nonzero vector and its negation.  -/
InnerProductGeometry.angle_self_neg_of_nonzero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x : V},
  x ≠ 0 → InnerProductGeometry.angle x (-x) = Real.pi
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.algHom_comp_convMul_distrib : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid C] [inst_6 : Module R C]
  [inst_7 : CoalgebraStruct R C] (h : A →ₐ[R] B) (f g : WithConv (C →ₗ[R] A)),
  h.toLinearMap ∘ₗ (f * g).ofConv =
    (WithConv.toConv (h.toLinearMap ∘ₗ f.ofConv) * WithConv.toConv (h.toLinearMap ∘ₗ g.ofConv)).ofConv
-- Mathlib.Order.LiminfLimsup
Filter.frequently_lt_of_liminf_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.frequently_lt_of_liminf_lt._auto_1 →
    Filter.liminf u f < b → ∃ᶠ (x : α) in f, u x < b
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Faithful.of_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [(F.comp G).Faithful], F.Faithful
-- Mathlib.Data.EReal.Basic
EReal.toReal_coe : ∀ (x : ℝ), (↑x).toReal = x
-- Mathlib.Analysis.Complex.Circle
/-- The elements of the circle embed into the units.  -/
Circle.toUnits : Circle →* ℂˣ
-- Mathlib.Data.Nat.Choose.Sum
/-- The sum along the antidiagonal of `(n+1).choose i * f i j` can be split into two sums along the
antidiagonal at rank `n`, respectively of `n.choose i * f i (j+1)` and `n.choose j * f (i+1) j`.  -/
Finset.sum_antidiagonal_choose_succ_mul : ∀ {R : Type u_1} [inst : NonAssocSemiring R] (f : ℕ → ℕ → R) (n : ℕ),
  ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), ↑((n + 1).choose ij.1) * f ij.1 ij.2 =
    ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, ↑(n.choose ij.1) * f ij.1 (ij.2 + 1) +
      ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, ↑(n.choose ij.2) * f (ij.1 + 1) ij.2
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_succ : ∀ (n : ℕ), (n + 1).factorial = (n + 1) * n.factorial
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.num.inj : ∀ {k k_1 : ℤ}, Int.Internal.Linear.Poly.num k = Int.Internal.Linear.Poly.num k_1 → k = k_1
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.mutuallySingular_singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  MeasureTheory.VectorMeasure.MutuallySingular (s.singularPart μ) μ.toENNRealVectorMeasure
-- Mathlib.Analysis.Convolution
/-- The convolution of `f` and `g` exists at `x` when the function `t ↦ L (f t) (g (x - t))` is
integrable. There are various conditions on `f` and `g` to prove this.  -/
MeasureTheory.ConvolutionExistsAt : {𝕜 : Type u𝕜} →
  {G : Type uG} →
    {E : Type uE} →
      {E' : Type uE'} →
        {F : Type uF} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedAddCommGroup E'] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NontriviallyNormedField 𝕜] →
                  [inst_4 : NormedSpace 𝕜 E] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      [inst_6 : NormedSpace 𝕜 F] →
                        [inst_7 : MeasurableSpace G] →
                          [Sub G] →
                            (G → E) →
                              (G → E') →
                                G →
                                  (E →L[𝕜] E' →L[𝕜] F) →
                                    autoParam (MeasureTheory.Measure G) MeasureTheory.ConvolutionExistsAt._auto_1 → Prop
-- Mathlib.Topology.Category.CompHaus.Frm
CompHausOpToFrame.faithful : (compHausToTop.op.comp topCatOpToFrm).Faithful
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_neg : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E},
  Balanced 𝕜 (-s) ↔ Balanced 𝕜 s
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.tryCatch_Except : ∀ {ε α : Type} {post : α → Prop} {epost : EPost⟨ε → Prop⟩} (x : Except ε α) (h : ε → Except ε α),
  ⦃ Std.Internal.Do.wp x post epost⟨fun e => Std.Internal.Do.wp (h e) post epost⟩ ⦄ MonadExceptOf.tryCatch x h ⦃ post;
    epost ⦄
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.array.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.array = 1
-- Mathlib.Algebra.Lie.Classical
/-- There is a constructive inverse of `Pso p q R i`.  -/
LieAlgebra.Orthogonal.invertiblePso : (p : Type u_2) →
  (q : Type u_3) →
    (R : Type u₂) →
      [inst : DecidableEq p] →
        [inst_1 : DecidableEq q] →
          [inst_2 : CommRing R] →
            [inst_3 : Fintype p] →
              [inst_4 : Fintype q] → {i : R} → i * i = -1 → Invertible (LieAlgebra.Orthogonal.Pso p q R i)
-- Mathlib.Order.Filter.Map
Filter.mem_bind : ∀ {α : Type u_1} {β : Type u_2} {s : Set β} {f : Filter α} {m : α → Filter β}, s ∈ f.bind m ↔ ∃ t ∈ f, ∀ x ∈ t, s ∈ m x
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.forgetful_obj : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] (𝒳 : CategoryTheory.BasedCategory 𝒮)
  (𝒴 : CategoryTheory.BasedCategory 𝒮) (F : CategoryTheory.BasedFunctor 𝒳 𝒴),
  (CategoryTheory.BasedNatTrans.forgetful 𝒳 𝒴).obj F = F.toFunctor
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Integrability in the change of variable formula for differentiable functions (one-variable
version): if a function `f` is injective and differentiable on a measurable set `s ⊆ ℝ`, then a
function `g : ℝ → F` is integrable on `f '' s` if and only if `|(f' x)| • g ∘ f` is integrable on
`s`.  -/
MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      Set.InjOn f s →
        ∀ (g : ℝ → F),
          MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume ↔
            MeasureTheory.IntegrableOn (fun x => |f' x| • g (f x)) s MeasureTheory.volume
-- Mathlib.Algebra.Star.Basic
eq_star_of_eq_star : ∀ {R : Type u} [inst : InvolutiveStar R] {r s : R}, r = star s → s = star r
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- A function `f` has the continuous linear map `f'` as derivative at `x` within a set `s` if
`f x' = f x + f' (x' - x) + o (x' - x)` when `x'` tends to `x` inside `s`.  -/
HasFDerivWithinAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : TopologicalSpace E] →
            {F : Type u_3} →
              [inst_4 : AddCommGroup F] →
                [inst_5 : Module 𝕜 F] → [inst_6 : TopologicalSpace F] → (E → F) → (E →L[𝕜] F) → Set E → E → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.idCompId_simplex : ∀ {X : SSet.Truncated 2} (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })),
  (SSet.Truncated.Edge.CompStruct.idCompId x).simplex =
    (CategoryTheory.ConcreteCategory.hom
        (X.map
          (SimplexCategory.Truncated.σ₂ 0 SSet.Truncated.Edge.CompStruct._proof_2 SSet.Truncated.Edge._proof_2).op))
      ((CategoryTheory.ConcreteCategory.hom
          (X.map (SimplexCategory.Truncated.σ₂ 0 SSet.Truncated.Edge._proof_3 SSet.Truncated.Edge._proof_1).op))
        x)
-- Mathlib.Order.Filter.ListTraverse
Filter.sequence_mono : ∀ {α : Type u} (as bs : List (Filter α)), List.Forall₂ (fun x1 x2 => x1 ≤ x2) as bs → sequence as ≤ sequence bs
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
/-- Predicate stating that all exponents are zero.  -/
Tactic.ComputeAsymptotics.UnitMonomial.AllZero : Tactic.ComputeAsymptotics.UnitMonomial → Prop
-- Mathlib.Algebra.Group.Equiv.Basic
/-- The equivalence `(M →* N₁) ≃ (M →* N₂)` obtained by postcomposition with
a multiplicative equivalence `e : N₁ ≃* N₂`.  -/
MulEquiv.monoidHomCongrRightEquiv : {M : Type u_4} →
  {N₁ : Type u_9} →
    {N₂ : Type u_10} →
      [inst : MulOneClass M] → [inst_1 : Monoid N₁] → [inst_2 : Monoid N₂] → N₁ ≃* N₂ → (M →* N₁) ≃ (M →* N₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.inv_map_Δ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] {A : Type v} [inst_2 : CommRing A]
  (f : R →+* A), (W.map f).Δ'⁻¹ = (Units.map ↑f) W.Δ'⁻¹
-- Mathlib.Data.SetLike.Basic
/-- The coercion from a term of a `SetLike` to its corresponding `Set` is injective.  -/
SetLike.coe_injective : ∀ {A : Type u_1} {B : outParam (Type u_2)} [self : SetLike A B], Function.Injective SetLike.coe
-- Mathlib.Order.Filter.Prod
Filter.mem_prod_iff_left : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {s : Set (α × β)},
  s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.mkEOIError : Lean.ParseImports.State → Lean.ParseImports.State
-- Mathlib.LinearAlgebra.Matrix.Invertible
Matrix.isUnit_conjTranspose : ∀ {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α] [inst_3 : StarRing α]
  (A : Matrix n n α), IsUnit A.conjTranspose ↔ IsUnit A
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle from `x` to `y`, modulo `2 * π`. If either vector is 0, this is 0.
See `InnerProductGeometry.angle` for the corresponding unoriented angle definition.  -/
Orientation.oangle : {V : Type u_1} →
  [inst : NormedAddCommGroup V] →
    [inst_1 : InnerProductSpace ℝ V] → [Fact (Module.finrank ℝ V = 2)] → Orientation ℝ V (Fin 2) → V → V → Real.Angle
-- Init.Grind.AC
Lean.Grind.AC.eq_expr_seq_seq : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (e : Lean.Grind.AC.Expr) (s₁ s₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Expr.denote ctx e = Lean.Grind.AC.Seq.denote ctx s₁ →
    Lean.Grind.AC.Seq.denote ctx s₁ = Lean.Grind.AC.Seq.denote ctx s₂ →
      Lean.Grind.AC.Expr.denote ctx e = Lean.Grind.AC.Seq.denote ctx s₂
-- Mathlib.Topology.Algebra.StarSubalgebra
/-- The `elemental` star subalgebra generated by a normal element is commutative.  -/
StarAlgebra.elemental.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : Semiring A] →
            [inst_4 : StarRing A] →
              [inst_5 : IsSemitopologicalSemiring A] →
                [inst_6 : ContinuousStar A] →
                  [inst_7 : Algebra R A] →
                    [inst_8 : StarModule R A] →
                      [T2Space A] → {x : A} → [IsStarNormal x] → CommSemiring ↥(StarAlgebra.elemental R x)
-- Init.Data.List.Attach
List.countP_attachWith : ∀ {α : Type u_1} {p : α → Prop} {q : α → Bool} {l : List α} (H : ∀ a ∈ l, p a),
  List.countP (fun a => q ↑a) (l.attachWith p H) = List.countP q l
-- Mathlib.CategoryTheory.Limits.Final
/-- The hypotheses also imply that `F` is initial, see `initial_of_comp_full_faithful`.  -/
CategoryTheory.Functor.initial_of_comp_full_faithful' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.Full] [G.Faithful] [(F.comp G).Initial], G.Initial
-- Mathlib.Algebra.Lie.OfAssociative
AlgEquiv.toLieEquiv_symm_apply : ∀ {R : Type u} {A₁ : Type v} {A₂ : Type w} [inst : CommRing R] [inst_1 : Ring A₁] [inst_2 : Ring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₂), e.toLieEquiv.symm x = e.symm x
-- Mathlib.Data.Set.Image
Subtype.preimage_coe_compl' : ∀ {α : Type u_1} (s : Set α), (fun x => ↑x) ⁻¹' s = ∅
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.colimit_add_mk_eq' : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) {j : J} (x y : ↑(F.obj j)),
  ModuleCat.FilteredColimits.M.mk F ⟨j, x⟩ + ModuleCat.FilteredColimits.M.mk F ⟨j, y⟩ =
    ModuleCat.FilteredColimits.M.mk F ⟨j, x + y⟩
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.HasRightDerivedFunctor.hasLeftKanExtension' : ∀ {C : Type u_1} {H : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_5, u_2} H} {F : CategoryTheory.Functor C H}
  {W : CategoryTheory.MorphismProperty C} [self : F.HasRightDerivedFunctor W], W.Q.HasLeftKanExtension F
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- See Note [custom simps projection]  -/
ModelWithCorners.Simps.symm_apply : (𝕜 : Type u_4) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_5) →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] → (H : Type u_6) → [inst_3 : TopologicalSpace H] → ModelWithCorners 𝕜 E H → E → H
-- Mathlib.Topology.Algebra.UniformConvergence
instInvUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Inv β], instInvUniformFun = { inv := instInvUniformFun._aux_1 }
-- Mathlib.CategoryTheory.Endomorphism
/-- `f.mapIso` as a group hom between automorphism groups.  -/
CategoryTheory.Functor.mapAut : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      {D : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} D] →
          (f : CategoryTheory.Functor C D) → CategoryTheory.Aut X →* CategoryTheory.Aut (f.obj X)
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_toNat : Cardinal.toNat Cardinal.continuum = 0
-- Mathlib.Analysis.Normed.Module.Basic
/-- Preimages of cobounded sets under the algebra map are cobounded.  -/
tendsto_algebraMap_cobounded : ∀ (𝕜 : Type u_6) (𝕜' : Type u_7) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜']
  [NormOneClass 𝕜'], Filter.Tendsto (⇑(algebraMap 𝕜 𝕜')) (Bornology.cobounded 𝕜) (Bornology.cobounded 𝕜')