mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.condition_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C))
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] {i j : J} (f : i ⟶ j) {Z : C}
  (h : CategoryTheory.Limits.chosenCoend F ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι F i) h) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι F j) h)
-- Mathlib.Data.Nat.Basic
Nat.instLinearOrder : LinearOrder ℕ
-- Init.Core
/-- Strict subset relation: `a ⊂ b`  

Conventions for notations in identifiers:

 * The recommended spelling of `⊂` in identifiers is `ssubset`. -/
«term_⊂_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Pull back a `NoZeroDivisors` instance along an injective function.  -/
Function.Injective.noZeroDivisors : ∀ {M₀ : Type u_1} {M₀' : Type u_3} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : Mul M₀'] [inst_3 : Zero M₀']
  (f : M₀ → M₀'),
  Function.Injective f → f 0 = 0 → (∀ (x y : M₀), f (x * y) = f x * f y) → ∀ [NoZeroDivisors M₀'], NoZeroDivisors M₀
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- If `X` is a simplicial set, then the inclusion `(⊥ : SSet) ⟶ X` of the empty
subcomplex of `X` is a relative cell complex with basic cells given by boundary
inclusions `∂Δ[d] ⟶ Δ[d]`, one for each nondegenerate `d`-simplex of `X`.  -/
SSet.relativeCellComplex : (X : SSet) → HomotopicalAlgebra.RelativeCellComplex (fun n x => (SSet.boundary n).ι) ⊥.ι
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_inv_pre : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasColimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)]
  [inst_5 : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.pre F E)] (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (E.obj k))
      (CategoryTheory.inv (CategoryTheory.Limits.colimit.pre F E)) =
    CategoryTheory.Limits.colimit.ι (E.comp F) k
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.swap_map_inl : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} {f : Sum.inl X ⟶ Sum.inl Y}, (CategoryTheory.Sum.swap C D).map f = f
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorInfo.ref : Lean.Elab.Term.MVarErrorInfo → Lean.Syntax
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_dblX : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).dblX (⇑f ∘ P) = f (W'.dblX P)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {x : M × M'},
  mfderiv% Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- The explicit cokernel is isomorphic to the usual cokernel.  -/
SemiNormedGrp.explicitCokernelIso : {X Y : SemiNormedGrp} → (f : X ⟶ Y) → SemiNormedGrp.explicitCokernel f ≅ CategoryTheory.Limits.cokernel f
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.OptionT.orElse.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) →
    (__do_lift : Option α) →
      ((a : α) → motive (some a)) → ((x : Option α) → (∀ (a : α), x = some a → False) → motive x) → motive __do_lift
-- Mathlib.Topology.Subpath
/-- Auxiliary homotopy for `Path.Homotopy.subpathTransSubpath` which includes an unnecessary
copy of `Path.refl`.  -/
Path.Homotopy.subpathTransSubpathRefl : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {a b : X} →
      (γ : Path a b) →
        (t₀ t₁ t₂ : ↑unitInterval) →
          ((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).Homotopy ((γ.subpath t₀ t₂).trans (Path.refl (γ t₂)))
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- The conjugate of a multiplicative character with values in `ℂ` is its inverse.  -/
MulChar.star_eq_inv : ∀ {R : Type u_1} [inst : CommRing R] [Finite Rˣ] (χ : MulChar R ℂ), star χ = χ⁻¹
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a k : α}
  {v : β k}, (t.insert k v).getKey? a = if cmp k a = Ordering.eq then some k else t.getKey? a
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- Auxiliary lemma for the special case of
`dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq` where the orthogonal projection of `p`
to the line `p₁ p₂` is `p₁`.  -/
_private.Mathlib.Geometry.Euclidean.Angle.Bisector.0.EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁ : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Fact (Module.finrank ℝ V = 2)] [inst_5 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ : P},
  p₁ ≠ p₂ →
    2 • EuclideanGeometry.oangle p₂ p₁ p = 2 • EuclideanGeometry.oangle p p₁ p₃ →
      ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₂]) p) = p₁ →
        dist p ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₂]) p) =
          dist p ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₃]) p)
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Uniqueness (up to a unique linear equivalence) of the module defined
by generators and relations.  -/
Module.Relations.Solution.IsPresentation.uniq : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            {solution : relations.Solution M} →
              solution.IsPresentation →
                {N : Type v'} →
                  [inst_3 : AddCommGroup N] →
                    [inst_4 : Module A N] → {solution' : relations.Solution N} → solution'.IsPresentation → M ≃ₗ[A] N
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.lattice.eq_1 : ∀ (L : PeriodPair), L.lattice = Submodule.span ℤ {L.ω₁, L.ω₂}
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.lt_dist_iff_lt_dist_coe_center : ∀ {z w : UpperHalfPlane} {r : ℝ}, r < dist z w ↔ w.im * Real.sinh r < dist ↑z ↑(w.center r)
-- Mathlib.Order.Interval.Set.ProjIcc
/-- Projection of `α` to the closed interval `[a, ∞)`.  -/
Set.projIci : {α : Type u_1} → [inst : LinearOrder α] → (a : α) → α → ↑(Set.Ici a)
-- Mathlib.Order.Monotone.Union
/-- If `f` is monotone both on `s` and `t`, with `s` to the left of `t` and the center
point belonging to both `s` and `t`, then `f` is monotone on `s ∪ t`  -/
MonotoneOn.union_right : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {c : α},
  MonotoneOn f s → MonotoneOn f t → IsGreatest s c → IsLeast t c → MonotoneOn f (s ∪ t)
-- Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
_private.Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts.0.CategoryTheory.Limits.Fan.combPairHoms.match_1.eq_1 : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} (motive : ι₁ ⊕ ι₂ → Sort u_3) (a : ι₁) (h_1 : (a : ι₁) → motive (Sum.inl a))
  (h_2 : (a : ι₂) → motive (Sum.inr a)),
  (match Sum.inl a with
    | Sum.inl a => h_1 a
    | Sum.inr a => h_2 a) =
    h_1 a
-- Mathlib.GroupTheory.Coset.Defs
/-- The equivalence relation corresponding to the partition of a group by left cosets
of a subgroup.  -/
QuotientGroup.leftRel : {α : Type u_1} → [inst : Group α] → Subgroup α → Setoid α
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.constantCoeff_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R], MvPowerSeries.constantCoeff 0 = 0
-- Batteries.Util.ProofWanted
/-- A non-class dependency of the referenced wanted that must be surfaced as a binder on the
*enclosing* declaration (rather than quantified inside the reference's own binder, where it would
be an unsolvable implicit), then threaded into the reference's application.  -/
_private.Batteries.Util.ProofWanted.0.WantedDep : Type
-- Init.Data.List.Sublist
List.IsSuffix.getLast : ∀ {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <:+ l₂) (hx : l₁ ≠ []), l₁.getLast hx = l₂.getLast ⋯
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.surjective_domRestrict_of_isSeparable : ∀ {K : Type u} (L : Type v) {M : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : Field M]
  [inst_4 : Algebra K M] [IsSepClosed M] {E : Type u_1} [inst_6 : Field E] [inst_7 : Algebra K E] [inst_8 : Algebra L E]
  [inst_9 : IsScalarTower K L E] [Algebra.IsSeparable L E], Function.Surjective fun φ => AlgHom.domRestrict L φ
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length_eq_three : ∀ {α : Type u_1} {v : FreeAddMonoid α},
  v.length = 3 ↔ ∃ a b c, v = FreeAddMonoid.of a + FreeAddMonoid.of b + FreeAddMonoid.of c
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- **No wrap-around principle**.

The first `k` elements of `Fin (n + 1)` are `m`-Freiman isomorphic to the first `k` elements of `ℕ`
assuming there is no wrap-around.  -/
Fin.isAddFreimanIso_Iio : ∀ {k m n : ℕ}, m ≠ 0 → m * k ≤ n → IsAddFreimanIso m (Set.Iio ↑k) (Set.Iio k) Fin.val
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
derivWithin_ccos : ∀ {f : ℂ → ℂ} {x : ℂ} {s : Set ℂ},
  DifferentiableWithinAt ℂ f s x →
    UniqueDiffWithinAt ℂ s x → derivWithin (fun x => Complex.cos (f x)) s x = -Complex.sin (f x) * derivWithin f s x
-- Mathlib.Analysis.LocallyConvex.WeakDual
/-- When `B` is right-separating, `F` is linearly equivalent to the strong dual of `E` with the
weak topology.  -/
LinearMap.rightDualEquiv : {𝕜 : Type u_5} →
  {E : Type u_6} →
    {F : Type u_7} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : AddCommGroup F] →
              [inst_4 : Module 𝕜 F] → (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → B.SeparatingRight → F ≃ₗ[𝕜] StrongDual 𝕜 (WeakBilin B)
-- Mathlib.Algebra.Algebra.Bilinear
/-- The multiplication map on an `R`-algebra, as an `A`-linear map from `A ⊗[R] A` to `A`.  -/
LinearMap.mul'' : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → TensorProduct R A A →ₗ[A] A
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Icc_mul_Icc_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : DecidableEq α] [MulLeftMono α] [MulRightMono α]
  [inst_5 : LocallyFiniteOrder α] (a b c d : α), Finset.Icc a b * Finset.Icc c d ⊆ Finset.Icc (a * c) (b * d)
-- Mathlib.Data.Complex.Basic
Complex.div_intCast : ∀ (z : ℂ) (n : ℤ), z / ↑n = { re := z.re / ↑n, im := z.im / ↑n }
-- Mathlib.Order.Defs.LinearOrder
max_assoc : ∀ {α : Type u_1} [inst : LinearOrder α] (a b c : α), max (max a b) c = max a (max b c)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.neg_add_eq_iff_eq_add : ∀ {w : ℕ} (a b c : BitVec w), (~~~a + 1#w + b == c) = (b == c + a)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.congr_mul.injEq : ∀ {R : Type u} [inst : Rack R] {a b a' b' : Rack.PreEnvelGroup R} (ha : Rack.PreEnvelGroupRel' R a a')
  (hb : Rack.PreEnvelGroupRel' R b b') (ha_1 : Rack.PreEnvelGroupRel' R a a') (hb_1 : Rack.PreEnvelGroupRel' R b b'),
  (ha.congr_mul hb = ha_1.congr_mul hb_1) = (ha = ha_1 ∧ hb = hb_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_insert_le_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {k : α} {v : β}, (cmp (t.insert k v).minKey! t.minKey!).isLE = true
-- Mathlib.Data.List.Basic
List.head?_flatten_replicate : ∀ {α : Type u} {n : ℕ}, n ≠ 0 → ∀ (l : List α), (List.replicate n l).flatten.head? = l.head?
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.ctor.inj : ∀ {i : Lean.IR.CtorInfo} {ys : Array Lean.IR.Arg} {i_1 : Lean.IR.CtorInfo} {ys_1 : Array Lean.IR.Arg},
  Lean.IR.Expr.ctor i ys = Lean.IR.Expr.ctor i_1 ys_1 → i = i_1 ∧ ys = ys_1
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.End.mulActionLeft : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → MulAction (CategoryTheory.End X)ᵐᵒᵖ (X ⟶ Y)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.hasNoetherianRange_iff_range : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂}, f.HasNoetherianRange ↔ IsNoetherian K ↥f.range
-- Mathlib.Topology.Order.Basic
/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(-∞, x)` is separated above from `f x` is countable.  -/
countable_image_gt_image_Iio : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : LinearOrder β] (f : β → α) [SecondCountableTopology α], {x | ∃ z, f x < z ∧ ∀ y < x, z ≤ f y}.Countable
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_filter_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  m.WF →
    ((Std.DHashMap.Raw.filter f m).isEmpty = true ↔
      ∀ (k : α) (h : k ∈ m), f (m.getKey k h) (Std.DHashMap.Raw.Const.get m k h) = false)
-- Init.Data.List.Lemmas
List.getElem?_append_right : ∀ {α : Type u_1} {l₁ l₂ : List α} {i : ℕ}, l₁.length ≤ i → (l₁ ++ l₂)[i]? = l₂[i - l₁.length]?
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.toPullback_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀}
  [inst_1 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] (k : E.I₁ i₁ i₂) {Z : C} (h : E.X i₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (E.toPullback k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (E.f i₁) (E.f i₂)) h) =
    CategoryTheory.CategoryStruct.comp (E.p₁ k) h
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.unionFuel.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  (match 0 with
    | 0 => h_1 ()
    | fuel.succ => h_2 fuel) =
    h_1 ()
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.instMonoidalPreadditive : ∀ {R : Type u} [inst : CommRing R], CategoryTheory.MonoidalPreadditive (ModuleCat R)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_of_contains_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α},
  t.WF → (Std.DTreeMap.Raw.map f t).contains k = true → t.contains k = true
-- Mathlib.Analysis.Seminorm
SeminormClass.toAddGroupSeminormClass : ∀ {F : Type u_12} {𝕜 : outParam (Type u_13)} {E : outParam (Type u_14)} {inst : SeminormedRing 𝕜} {inst_1 : AddGroup E}
  {inst_2 : SMul 𝕜 E} {inst_3 : FunLike F E ℝ} [self : SeminormClass F 𝕜 E], AddGroupSeminormClass F E ℝ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom
      (CategoryTheory.Limits.pullback.snd g f) =
    CategoryTheory.Limits.pullback.fst f g
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (i : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMap ((NumberField.mixedEmbedding.fundamentalCone.completeBasis K) ↑i) =
    NumberField.mixedEmbedding.normAtAllPlaces
      ((NumberField.mixedEmbedding K)
        ((algebraMap (NumberField.RingOfIntegers K) K)
          ↑(NumberField.Units.fundSystem K (NumberField.mixedEmbedding.fundamentalCone.equivFinRank.symm i))))
-- Mathlib.Algebra.Polynomial.Div
Polynomial.map_dvd_map : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  Function.Injective ⇑f → ∀ {x y : Polynomial R}, x.Monic → (Polynomial.map f x ∣ Polynomial.map f y ↔ x ∣ y)
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.instIsLocalizedModuleTensorProductMap : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {M' : Type u_4} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  (N : Type u_5) (N' : Type u_6) [inst_5 : AddCommMonoid N] [inst_6 : Module R N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S f] [IsLocalizedModule S g],
  IsLocalizedModule S (TensorProduct.map f g)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}
  {hc : t.maxKey he ∈ t}, t.getKey (t.maxKey he) hc = t.maxKey he
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.OpenCover.restrict_X : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) (x : 𝒰.I₀),
  (𝒰.restrict U).X x = ↑((TopologicalSpace.Opens.map (𝒰.f x).base).obj U)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Orientation.rotation.congr_simp : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o o_1 : Orientation ℝ V (Fin 2)), o = o_1 → ∀ (θ θ_1 : Real.Angle), θ = θ_1 → o.rotation θ = o_1.rotation θ_1
-- Mathlib.Order.Interval.Basic
/-- Consider an interval `[a, b]` as the set `[a, b]`.  -/
Interval.coeHom : {α : Type u_1} → [inst : PartialOrder α] → Interval α ↪o Set α
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.of_associated : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {r r' : R},
  Associated r r' → ∀ [IsLocalization.Away r S], IsLocalization.Away r' S
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Injective.State.thms : Lean.Meta.Grind.Injective.State → Lean.Meta.Grind.InjectiveTheoremsArray
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.merge : ℕ → Std.Format.SpaceResult✝ → (ℕ → Std.Format.SpaceResult✝) → Std.Format.SpaceResult✝
-- Lean.Attributes
Lean.AttributeExtensionOLeanEntry.mk : Lean.Name → Lean.Name → List Lean.DataValue → Lean.AttributeExtensionOLeanEntry
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic.0.termY : Lean.ParserDescr
-- Mathlib.Algebra.Order.Hom.Basic
map_div_le_add : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [GroupSeminormClass F α β] (f : F) (x y : α), f (x / y) ≤ f x + f y
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
/-- A map `f` is said to be conformal if it has a conformal differential `f'`.  -/
ConformalAt : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : NormedAddCommGroup X] →
      [inst_1 : NormedAddCommGroup Y] → [NormedSpace ℝ X] → [NormedSpace ℝ Y] → (X → Y) → X → Prop
-- Mathlib.Algebra.Lie.Ideal
LieHom.map_le_idealRange : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L),
  LieIdeal.map f I ≤ f.idealRange
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] {P : Algebra.PreSubmersivePresentation R S ι σ} (x : ↥P.ker),
  P.cotangentComplexAux (Algebra.Extension.Cotangent.mk x) = 0 ↔
    ∀ (i : σ), (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) ↑x) = 0
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instMul : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} → [GradedRing 𝒜] → (x : Submonoid A) → Mul (HomogeneousLocalization 𝒜 x)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.singleton_smul_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (a : α) (b : β), {a} • {b} = {a • b}
-- Mathlib.Topology.MetricSpace.Thickening
/-- The (open) thickening `Metric.thickening δ E` with a fixed thickening radius `δ` is
an increasing function of the subset `E`.  -/
Metric.thickening_subset_of_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) {E₁ E₂ : Set α},
  E₁ ⊆ E₂ → Metric.thickening δ E₁ ⊆ Metric.thickening δ E₂
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
CochainComplex.isIso_pOpcycles₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℕ) [inst_2 : HomologicalComplex.HasHomology K 0],
  CategoryTheory.IsIso (HomologicalComplex.pOpcycles K 0)
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
rieszContentAux_union : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [T2Space X] [LocallyCompactSpace X] {K₁ K₂ : TopologicalSpace.Compacts X},
  Disjoint ↑K₁ ↑K₂ → rieszContentAux Λ (K₁ ⊔ K₂) = rieszContentAux Λ K₁ + rieszContentAux Λ K₂
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (T : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.OplaxMonoidal.η F))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.LaxMonoidal.ε F)) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj T (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.coe_toLaurentAlg : ∀ {R : Type u_1} [inst : CommSemiring R], ⇑Polynomial.toLaurentAlg = ⇑Polynomial.toLaurent
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
IsSelfAdjoint.quasispectrumRestricts : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
  {a : A}, IsSelfAdjoint a → QuasispectrumRestricts a ⇑Complex.reCLM
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isNonloop_of_not_isLoop : ∀ {α : Type u_1} {M : Matroid α} {e : α},
  autoParam (e ∈ M.E) Matroid.isNonloop_of_not_isLoop._auto_1 → ¬M.IsLoop e → M.IsNonloop e