mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Format.Modifier
Std.Time.Year.any.sizeOf_spec : sizeOf Std.Time.Year.any = 1
-- Mathlib.Algebra.Algebra.Subalgebra.Operations
instSMulCommClassSubtypeMemSubringSubring : ∀ (B : Type u_2) [inst : Ring B] (G : Type u_4) [inst_1 : Monoid G] [inst_2 : MulSemiringAction G B],
  SMulCommClass G (↥(FixedPoints.subring B G)) B
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrRightEquiv_trans : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [inst : AddZeroClass M] [inst_1 : AddMonoid N₁]
  [inst_2 : AddMonoid N₂] [inst_3 : AddMonoid N₃] (e₁₂ : N₁ ≃+ N₂) (e₂₃ : N₂ ≃+ N₃),
  (e₁₂.trans e₂₃).addMonoidHomCongrRightEquiv = e₁₂.addMonoidHomCongrRightEquiv.trans e₂₃.addMonoidHomCongrRightEquiv
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.revAll.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  s.revAll pat = (s.skipSuffixWhile pat == s.startPos)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Reinterpret a `ContinuousMonoidHom` as a `ContinuousMap`.  -/
ContinuousMonoidHom.toContinuousMap : {A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → (A →ₜ* B) → C(A, B)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link2.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l l'' : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.Tree α β (l.size + l''.size) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.Tree α β (l.size + l''.size)) →
          ((ℓ : Std.DTreeMap.Internal.Impl α β) →
              (hℓ₁ : ℓ.Balanced) →
                (hℓ₂ : ℓ.size = l.size + l''.size) → motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }) →
            motive x
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.append.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b c : RBTree.RBNode α) (y : α) (d : RBTree.RBNode α) (h_1 : (x : RBTree.RBNode α) → motive RBTree.RBNode.nil x)
  (h_2 : (x : RBTree.RBNode α) → motive x RBTree.RBNode.nil)
  (h_3 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.red c y d))
  (h_4 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.black a x b) (RBTree.RBNode.node RBTree.RBColor.black c y d))
  (h_5 :
    (a l : RBTree.RBNode α) →
      (v : α) →
        (r : RBTree.RBNode α) →
          a = RBTree.RBNode.node RBTree.RBColor.black l v r →
            (b : RBTree.RBNode α) →
              (x : α) →
                (c : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.black l v r) (RBTree.RBNode.node RBTree.RBColor.red b x c))
  (h_6 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c l : RBTree.RBNode α) →
          (v : α) →
            (r : RBTree.RBNode α) →
              c = RBTree.RBNode.node RBTree.RBColor.black l v r →
                motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.black l v r)),
  (match RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d with
    | RBTree.RBNode.nil, x => h_1 x
    | x, RBTree.RBNode.nil => h_2 x
    | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d => h_3 a x b c y d
    | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d => h_4 a x b c y d
    | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
      h_5 a l v r h b x c
    | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
      h_6 a x b c l v r h) =
    h_3 a x b c y d
-- Init.Data.List.TakeDrop
List.takeWhile_replicate_eq_filter : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool},
  List.takeWhile p (List.replicate n a) = List.filter p (List.replicate n a)
-- Mathlib.LinearAlgebra.Basis.Cardinality
finite_of_span_finite_eq_top_finsupp : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial M]
  {ι : Type u_1} {s : Set (ι →₀ M)}, s.Finite → Submodule.span R s = ⊤ → Finite ι
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.revAll_takeEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String}, (s.takeEndWhile pat).revAll pat = true
-- Mathlib.Topology.VectorBundle.Hom
/-- Given trivializations `e₁`, `e₂` for vector bundles `E₁`, `E₂` over a base `B`,
`Pretrivialization.continuousLinearMap σ e₁ e₂` is the induced pretrivialization for the
continuous `σ`-semilinear maps from `E₁` to `E₂`. That is, the map which will later become a
trivialization, after the bundle of continuous semilinear maps is equipped with the right
topological vector bundle structure.  -/
Bundle.Pretrivialization.continuousLinearMap : {𝕜₁ : Type u_1} →
  [inst : NontriviallyNormedField 𝕜₁] →
    {𝕜₂ : Type u_2} →
      [inst_1 : NontriviallyNormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {B : Type u_3} →
            {F₁ : Type u_4} →
              [inst_2 : NormedAddCommGroup F₁] →
                [inst_3 : NormedSpace 𝕜₁ F₁] →
                  {E₁ : B → Type u_5} →
                    [inst_4 : (x : B) → AddCommGroup (E₁ x)] →
                      [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)] →
                        [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                          {F₂ : Type u_6} →
                            [inst_7 : NormedAddCommGroup F₂] →
                              [inst_8 : NormedSpace 𝕜₂ F₂] →
                                {E₂ : B → Type u_7} →
                                  [inst_9 : (x : B) → AddCommGroup (E₂ x)] →
                                    [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] →
                                      [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                        [inst_12 : TopologicalSpace B] →
                                          (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) →
                                            (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) →
                                              [inst_13 : (x : B) → TopologicalSpace (E₁ x)] →
                                                [FiberBundle F₁ E₁] →
                                                  [inst_15 : (x : B) → TopologicalSpace (E₂ x)] →
                                                    [FiberBundle F₂ E₂] →
                                                      [Bundle.Trivialization.IsLinear 𝕜₁ e₁] →
                                                        [Bundle.Trivialization.IsLinear 𝕜₂ e₂] →
                                                          Bundle.Pretrivialization (F₁ →SL[σ] F₂) Bundle.TotalSpace.proj
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns an `Array` of the values in order.  -/
Std.DTreeMap.Internal.Impl.valuesArray : {α : Type u} → {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → Array β
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
/-- If `a ≠ 0, b` are elements of a unique factorization domain, then dividing
out their common factor `c'` gives `a'` and `b'` with no factors in common.  -/
UniqueFactorizationMonoid.exists_reduced_factors : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [UniqueFactorizationMonoid R] (a : R),
  a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.toUnitHom_eq_char' : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {a : ZMod n} (ha : IsUnit a),
  χ a = ↑((MulChar.toUnitHom χ) ha.unit)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.neg.eq_1 : ∀ (t : Tactic.ComputeAsymptotics.Monomial), t.neg = { coef := -t.coef, unit := t.unit }
-- Mathlib.Order.WithBot
WithBot.unbot_coe : ∀ {α : Type u_1} (x : α) (h : optParam (↑x ≠ ⊥) ⋯), (↑x).unbot h = x
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mkAddMonoidHom_apply : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddZeroClass M] [inst_2 : ContinuousAdd M] (a : M),
  SeparationQuotient.mkAddMonoidHom a = SeparationQuotient.mk a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.unreach.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (type : Lean.Expr), sizeOf (Lean.Compiler.LCNF.Code.unreach type) = 1 + sizeOf type
-- Mathlib.CategoryTheory.Generator.Basic
/-- We say that `P : ObjectProperty C` is coseparating if the functors `C(-, G)`
for `G : C` such that `P G` are collectively faithful,
i.e., if `f ≫ h = g ≫ h` for all `h` with codomain in `𝒢` implies `f = g`.  -/
CategoryTheory.ObjectProperty.IsCoseparating : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Tactic.NormNum.OfScientific
Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true : ∀ {α : Type u_1} [inst : DivisionSemiring α] {m e n d : ℕ},
  Mathlib.Meta.NormNum.IsNNRat (↑(NNRat.divNat m (10 ^ e))) n d →
    Mathlib.Meta.NormNum.IsNNRat (OfScientific.ofScientific m true e) n d
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) (n : ℕ), logDeriv (fun x => x ^ n) x = ↑n / x
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.vsub_contLinear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace W]
  [inst_10 : IsTopologicalAddGroup W] [inst_11 : IsTopologicalAddTorsor Q] [inst_12 : TopologicalSpace V]
  [inst_13 : IsTopologicalAddTorsor P] (f g : P →ᴬ[R] Q), (f -ᵥ g).contLinear = f.contLinear - g.contLinear
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometric_sum_eq : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂) (x : 𝔸),
  (ordinaryHypergeometricSeries 𝔸 a b c).sum x =
    ∑' (n : ℕ),
      ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
          (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
        x ^ n
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.failed.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {error error_1 : Std.Http.Protocol.H1.Error},
  Std.Http.Protocol.H1.Reader.State.failed error = Std.Http.Protocol.H1.Reader.State.failed error_1 → error = error_1
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.add_iff_right : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] {a b c d p : M},
  c ≡ d [PMOD p] → (a + c ≡ b + d [PMOD p] ↔ a ≡ b [PMOD p])
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.diagonal_hadamard_adjMatrix : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α] (d : V → α), (Matrix.diagonal d).hadamard (SimpleGraph.adjMatrix α G) = 0
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α}, nhdsSetWithin {x} s = nhdsWithin x s
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
/-- The curve integral of a closed 1-form along the boundary of the image of a unit square
under a smooth map is zero. We may ignore the behavior on a countable set.

This theorem is stated in terms of a `C^2` homotopy between two paths.  -/
ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {a b c d : E} {γ₁ : Path a b} {γ₂ : Path c d} {s : Set (↑unitInterval × ↑unitInterval)}
  {t : Set E} {ω : E → E →L[𝕜] F} {dω : E → E →L[ℝ] E →L[𝕜] F} (φ : (↑γ₁).Homotopy ↑γ₂),
  s.Countable →
    (∀ a_1 ∈ Set.Ioo 0 1, ∀ b_1 ∈ Set.Ioo 0 1, φ (a_1, b_1) ∈ t) →
      (∀ a_1 ∈ Set.Ioo 0 1,
          ∀ b_1 ∈ Set.Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))) →
        ContinuousOn ω (closure t) →
          (∀ a_1 ∈ Set.Ioo 0 1,
              ∀ b_1 ∈ Set.Ioo 0 1,
                (a_1, b_1) ∉ s →
                  ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
                    ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u) →
            ContDiffOn ℝ 2 (fun xy => Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Set.Icc 0 1) →
              ∫ᶜ (x : E) in γ₁, ω x + ∫ᶜ (x : E) in φ.evalAt 1, ω x =
                ∫ᶜ (x : E) in γ₂, ω x + ∫ᶜ (x : E) in φ.evalAt 0, ω x
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.nonDegenerate : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (self : SSet.relativeCellComplexOfMono.Cell i d), self.simplex ∈ Y.nonDegenerate d
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- `BinaryBiproduct.bicone P Q` is a limit cone.  -/
CategoryTheory.Limits.BinaryBiproduct.isLimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (P Q : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryBiproduct.bicone P Q).toCone
-- Init.Data.List.Find
List.lt_findIdx_iff : ∀ {α : Type u_1} (xs : List α) (p : α → Bool) (i : ℕ),
  i < List.findIdx p xs ↔ ∃ (h : i < xs.length), ∀ (j : ℕ) (hj : j ≤ i), p xs[j] = false
-- Mathlib.Algebra.Opposites
MulOpposite.unop_injective : ∀ {α : Type u_1}, Function.Injective MulOpposite.unop
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- **Alias** of `MonoidHom.domRestrictHomKerEquiv`.

---

The `MulEquiv` between the kernel of the restriction map to a normal subgroup `H` of homomorphisms
of type `G →* A` and the group of homomorphisms `G ⧸ H →* A`.
 -/
MonoidHom.restrictHomKerEquiv : {G : Type u} →
  [inst : Group G] →
    (A : Type u_1) →
      [inst_1 : CommGroup A] →
        (H : Subgroup G) → [inst_2 : H.Normal] → ↥(MonoidHom.domRestrictHom H A).ker ≃* (G ⧸ H →* A)
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
/-- The lift ring map `gh_n : 𝕎(R/𝔭) →+* R/𝔭^(n+1)` of the `n`-th ghost component
`𝕎(R) →+* R` along the surjective ring map `𝕎(R) →+* 𝕎(R/𝔭)`.
 -/
WittVector.ghostComponentModPPow : {R : Type u} →
  [inst : CommRing R] →
    {p : ℕ} →
      [inst_1 : Fact (Nat.Prime p)] → (n : ℕ) → WittVector p (R ⧸ Ideal.span {↑p}) →+* R ⧸ Ideal.span {↑p} ^ (n + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
CategoryTheory.Limits.hasLimitsOfShape_discrete : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (ι : Type w)
  [Finite ι], CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ι) C
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.mkAtom.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (n : α),
  aig.mkAtom n =
    {
      aig :=
        { decls := aig.decls.push (Std.Sat.AIG.Decl.atom n), cache := aig.cache.noUpdate, hdag := ⋯, hzero := ⋯,
          hconst := ⋯ },
      ref := { gate := aig.decls.size, invert := false, hgate := ⋯ } }
-- Mathlib.Data.Multiset.Bind
Multiset.cons_bind : ∀ {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (f : α → Multiset β), (a ::ₘ s).bind f = f a + s.bind f
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.diagonal_kronecker : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : MulZeroClass α] [inst_1 : DecidableEq l]
  (a : l → α) (B : Matrix m n α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (Matrix.diagonal a) B =
    (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun i => a i • B)
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.ext_iff : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} {x y : Std.Iterators.Types.FilterMap α m n lift f},
  x = y ↔ x.inner = y.inner
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- The ring homomorphism that extends a fractional ideal of `A` to a fractional ideal of `B` for
an extension of domains `A ⊆ B`.
 -/
FractionalIdeal.extendedHom : {A : Type u_1} →
  {K : Type u_2} →
    (L : Type u_3) →
      (B : Type u_4) →
        [inst : CommRing A] →
          [IsDomain A] →
            [inst_2 : CommRing B] →
              [IsDomain B] →
                [inst_4 : Algebra A B] →
                  [Module.IsTorsionFree A B] →
                    [inst_6 : Field K] →
                      [inst_7 : Field L] →
                        [inst_8 : Algebra A K] →
                          [inst_9 : Algebra B L] →
                            [IsFractionRing A K] →
                              [IsFractionRing B L] →
                                FractionalIdeal (nonZeroDivisors A) K →+* FractionalIdeal (nonZeroDivisors B) L
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeGPFree.le_mulRothNumber : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s t : Finset α},
  ThreeGPFree ↑s → s ⊆ t → s.card ≤ mulRothNumber t
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.of_right_eq_zero : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V]
  (f : Module.Dual R V), LinearMap.transvection f 0 = LinearMap.id
-- Std.Data.Internal.List.Associative
Std.Internal.List.contains_of_contains_insertList_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true →
    Std.Internal.List.containsKey k l = false → Std.Internal.List.containsKey k toInsert = true
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_inr : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : StarAddMonoid A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : StarAddMonoid B], ⇑(NonUnitalStarAlgHom.inr R A B) = Prod.mk 0
-- Mathlib.Geometry.Polygon.Basic
Polygon.HasNondegenerateVertices.three_le : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} {n : ℕ} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] [inst_4 : NeZero n] [Nontrivial R] {poly : Polygon P n},
  Polygon.HasNondegenerateVertices R poly → 3 ≤ n
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.identFnAux.parse : String.Pos.Raw →
  Option Lean.Parser.Token →
    Bool → Lean.Name → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Init.Data.ToString.Macro
termS!_ : Lean.ParserDescr
-- Mathlib.Order.Lex
instBEqColex : (α : Type u_2) → [BEq α] → BEq (Colex α)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_sub_const_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x - a) ⁻¹' Set.Ioc b c = Set.Ioc (b + a) (c + a)
-- Lean.Declaration
Lean.OpaqueVal.toConstantVal : Lean.OpaqueVal → Lean.ConstantVal
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- If `n % 4 = 1`, then `(-1)^(n/2) = 1`.  -/
ZMod.neg_one_pow_div_two_of_one_mod_four : ∀ {n : ℕ}, n % 4 = 1 → (-1) ^ (n / 2) = 1
-- Mathlib.CategoryTheory.Limits.Indization.LocallySmall
CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (w : F ≅ G) (j : J) {F_1 : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_4 : CategoryTheory.ConcreteCategory C F_1]
  (x : carrier (CategoryTheory.Limits.limit F)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π G j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.HasLimit.isoOfNatIso w).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (w.hom.app j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.one_le_rpow : ∀ {x z : ℝ}, 1 ≤ x → 0 ≤ z → 1 ≤ x ^ z
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u v : β → α} {p : β → Prop},
  (∀ᶠ (a : β) in f, p a → u a = v a) → Filter.bliminf u f p = Filter.bliminf v f p
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.iter_toArray : ∀ {β : Type w} {n : ℕ} {xs : Vector β n}, xs.toArray.iter = xs.iter
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_inv : ∀ (x : ℝ), Real.log x⁻¹ = -Real.log x
-- Mathlib.Analysis.Complex.Basic
Complex.summable_conj : ∀ {α : Type u_1} {f : α → ℂ}, (Summable fun x => (starRingEnd ℂ) (f x)) ↔ Summable f
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If all elements of a `Finset` satisfy the predicate `p`, a product
over `s.subtype p` equals that product over `s`.  -/
Finset.prod_subtype_of_mem : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] (f : ι → M) {p : ι → Prop}
  [inst_1 : DecidablePred p], (∀ x ∈ s, p x) → ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s, f x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_rpow_of_nonpos : ∀ {x y z : ℝ}, 0 < x → x ≤ y → z ≤ 0 → y ^ z ≤ x ^ z
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.op_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A),
  P.op.π = P.ι.op
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.subset_right_C : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P), c.C ⊆ c.right.C
-- Mathlib.RingTheory.Finiteness.Small
Submodule.small_span_singleton : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Small.{u, u_1} R]
  (m : M), Small.{u, u_2} ↥(R ∙ m)
-- Init.Data.UInt.Bitwise
UInt32.xor_not : ∀ {a b : UInt32}, a ^^^ ~~~b = ~~~(a ^^^ b)
-- Init.Data.Array.Find
Array.findIdx_subtype : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Array.findIdx f xs = Array.findIdx g xs.unattach
-- Mathlib.Topology.Algebra.ConstMulAction
tendsto_const_smul_iff₀ : ∀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀]
  [inst_2 : MulAction G₀ α] [ContinuousConstSMul G₀ α] {f : β → α} {l : Filter β} {a : α} {c : G₀},
  c ≠ 0 → (Filter.Tendsto (fun x => c • f x) l (nhds (c • a)) ↔ Filter.Tendsto f l (nhds a))
-- Init.Data.SInt.Bitwise
Int64.or_assoc : ∀ (a b c : Int64), a ||| b ||| c = a ||| (b ||| c)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_inter!_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true →
          Std.DTreeMap.Internal.Impl.Const.get! (m₁.inter! m₂) k = Std.DTreeMap.Internal.Impl.Const.get! m₁ k