mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Defs
/-- A `DivInvMonoid` is a `Monoid` with operations `/` and `⁻¹` satisfying
`div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹`.

This deduplicates the name `div_eq_mul_inv`.
The default for `div` is such that `a / b = a * b⁻¹` holds by definition.

Adding `div` as a field rather than defining `a / b := a * b⁻¹` allows us to
avoid certain classes of unification failures, for example:
Let `Foo X` be a type with a `∀ X, Div (Foo X)` instance but no
`∀ X, Inv (Foo X)`, e.g. when `Foo X` is a `EuclideanDomain`. Suppose we
also have an instance `∀ X [Cromulent X], GroupWithZero (Foo X)`. Then the
`(/)` coming from `GroupWithZero.div` cannot be definitionally equal to
the `(/)` coming from `Foo.Div`.

In the same way, adding a `zpow` field makes it possible to avoid definitional failures
in diamonds. See the definition of `Monoid` and Note [forgetful inheritance] for more
explanations on this.
 -/
DivInvMonoid : Type u → Type u
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.forget_map : ∀ (R : Type u) [inst : Semiring R] {M N : SemimoduleCat R} (f : M ⟶ N),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget (SemimoduleCat R)).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Spanning.contract_eq_loopyOn : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Spanning X → M.contract X = Matroid.loopyOn (M.E \ X)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_empty : ∀ {α : Type u_1} (M : Matroid α), M.delete ∅ = M
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkItem.activeTags : Std.Format.WorkItem✝ → ℕ
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} (i : Fin m),
  (Polynomial.degreeLT.addLinearEquiv R m n).symm
      ((LinearMap.inl R ↥(Polynomial.degreeLT R m) ↥(Polynomial.degreeLT R n)) ((Polynomial.degreeLT.basis R m) i)) =
    (Polynomial.degreeLT.basis R (m + n)) (Fin.castAdd n i)
-- Mathlib.Tactic.CrossRefAttribute
/-- The supported external databases  -/
Mathlib.CrossRef.Database : Type
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.instIsAddTorsionFreeLocallyConstantInt : ∀ (α : Type u_1) [inst : TopologicalSpace α], IsAddTorsionFree (LocallyConstant α ℤ)
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_le_encard_edgeSet : ∀ {V : Type u_1} {G : SimpleGraph V}, G.vertexCoverNum ≤ G.edgeSet.encard
-- Mathlib.Order.Lattice
/-- Pointwise maximum of two monotone functions is a monotone function.  -/
Monotone.max : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β},
  Monotone f → Monotone g → Monotone fun x => max (f x) (g x)
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.brecOn.go : {α : Type u} →
  {motive : Ordnode α → Sort u_1} →
    (t : Ordnode α) → ((t : Ordnode α) → Ordnode.below t → motive t) → motive t ×' Ordnode.below t
-- Mathlib.Data.Ordmap.Ordnode
/-- O(1). Is the set empty?

```
empty ∅ = tt
empty {1, 2, 3} = ff
```
 -/
Ordnode.empty : {α : Type u_1} → Ordnode α → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_mul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x → ∀ (d : 𝔸'), fderivWithin 𝕜 (fun y => c y * d) s x = d • fderivWithin 𝕜 c s x
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {x : R},
  (IsDiscreteValuationRing.addVal R) x = 0 ↔ IsUnit x
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.norm_qParam_lt_one : ∀ {h : ℝ}, 0 < h → ∀ {z : ℂ}, 0 < z.im → ‖Function.Periodic.qParam h z‖ < 1
-- Init.Data.Fin.Lemmas
Fin.castSucc.eq_1 : ∀ {n : ℕ}, Fin.castSucc = Fin.castAdd 1
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regulator.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.Units.regulator K = ZLattice.covolume (NumberField.Units.unitLattice K) MeasureTheory.volume
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.withEqs.go : {α : Type} →
  Array Lean.Elab.Term.Discr →
    (Array Lean.Expr → Lean.Elab.TermElabM α) →
      ℕ → List Lean.Meta.Match.Pattern → Array Lean.Expr → Lean.Elab.TermElabM α
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.foldrM.eq_def : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : (a : α) → β a → δ → m δ)
  (x : δ) (x_1 : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldrM f x x_1 =
    match x, x_1 with
    | d, Std.DHashMap.Internal.AssocList.nil => pure d
    | d, Std.DHashMap.Internal.AssocList.cons a b es => do
      let d ← Std.DHashMap.Internal.AssocList.foldrM f d es
      f a b d
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.toIsFilteredOrEmpty : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsFiltered C],
  CategoryTheory.IsFilteredOrEmpty C
-- Mathlib.GroupTheory.Index
AddSubgroup.index_strictAnti : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H < K → ∀ [H.FiniteIndex], K.index < H.index
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.instModule : {R : Type u_1} →
  [inst : Semiring R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddCommMonoid X] → [inst_3 : Module R X] → Module (OreLocalization S R) (OreLocalization S X)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm_le_comap : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] (I : Ideal S), Ideal.spanNorm R I ≤ Ideal.comap (algebraMap R S) I
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- A compositum of purely inseparable extensions is purely inseparable.  -/
IntermediateField.isPurelyInseparable_iSup : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Sort u_1}
  {t : ι → IntermediateField F E} [h : ∀ (i : ι), IsPurelyInseparable F ↥(t i)], IsPurelyInseparable F ↥(⨆ i, t i)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionItemCapabilities.mk : Option Bool → Lean.Lsp.CompletionItemCapabilities
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_norm_expr : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs lhs' rhs' : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.norm_eq_cert lhs rhs lhs' rhs' = true →
    (Lean.Grind.CommRing.Expr.denote ctx lhs = Lean.Grind.CommRing.Expr.denote ctx rhs) =
      (Lean.Grind.CommRing.Expr.denote ctx lhs' = Lean.Grind.CommRing.Expr.denote ctx rhs')
-- Mathlib.RingTheory.Jacobson.Polynomial
Ideal.jacobson_bot_polynomial_of_jacobson_bot : ∀ {R : Type u_1} [inst : CommRing R], ⊥.jacobson = ⊥ → ⊥.jacobson = ⊥
-- Mathlib.Data.Finset.Insert
Multiset.toFinset_zero : ∀ {α : Type u_1} [inst : DecidableEq α], Multiset.toFinset 0 = ∅
-- Mathlib.Data.NNReal.Defs
NNReal.coe_zpow : ∀ (r : NNReal) (n : ℤ), ↑(r ^ n) = ↑r ^ n
-- Mathlib.SetTheory.Ordinal.FixedPoint
/-- `Ordinal.deriv` enumerates the fixed points of a normal function.  -/
Ordinal.deriv_eq_enumOrd : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → Ordinal.deriv f = Ordinal.enumOrd (Function.fixedPoints f)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basis
/-- The `TensorAlgebra` of a free module over an integral domain is a domain.  -/
TensorAlgebra.instIsDomain : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.Free R M], IsDomain (TensorAlgebra R M)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow_sorted : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {n : ℕ} {r : ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow basis_hd basis_tl n r).Sorted
-- Mathlib.Topology.Algebra.Monoid
Pi.separatelyContinuousMul : ∀ {ι : Type u_1} {C : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (C i)] [inst_1 : (i : ι) → Mul (C i)]
  [∀ (i : ι), SeparatelyContinuousMul (C i)], SeparatelyContinuousMul ((i : ι) → C i)
-- Lean.Meta.Basic
Lean.Meta.instBEqAbstractMVarsResult : BEq Lean.Meta.AbstractMVarsResult
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_insertIfNew_le_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {he : t.isEmpty = false},
  (compare ((Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey ⋯) (t.minKey he)).isLE = true
-- Mathlib.Analysis.Analytic.Binomial
Complex.one_div_one_sub_pow_hasFPowerSeriesOnBall_zero : ∀ (a : ℕ),
  HasFPowerSeriesOnBall (fun x => 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n => ↑((a + n).choose a)) 0 1
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- There are finitely many simple graphs on a given finite type.  -/
SimpleGraph.instFinite : ∀ {V : Type u} [Finite V], Finite (SimpleGraph V)
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.go : Lean.Expr → Lean.Meta.Sym.M✝ Lean.Expr
-- Batteries.Data.UnionFind.Basic
/-- Link a union-find node to a root node. Panics if either index is out of bounds.  -/
Batteries.UnionFind.link! : (self : Batteries.UnionFind) → ℕ → (y : ℕ) → self.parent y = y → Batteries.UnionFind
-- Mathlib.SetTheory.Cardinal.ToNat
/-- A version of `toNat_eq_iff` for literals  -/
Cardinal.toNat_eq_ofNat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], Cardinal.toNat c = OfNat.ofNat n ↔ c = OfNat.ofNat n
-- Mathlib.Data.Seq.Computation
/-- `Results s a n` completely characterizes a terminating computation:
it asserts that `s` terminates after exactly `n` steps, with result `a`.  -/
Computation.Results : {α : Type u} → Computation α → α → ℕ → Prop
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.coind_comp_friend_left.match_1_1.eq_2 : ∀ {α : Type u_1} (motive : (Stream'.Seq α → Stream'.Seq α) → Prop)
  (motive_1 : Option (α × Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation × Subtype motive) → Sort u_2) (hd : α)
  (opf' : Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) (op' : Subtype motive) (h_1 : Unit → motive_1 none)
  (h_2 :
    (hd : α) →
      (opf' : Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) →
        (op' : Subtype motive) → motive_1 (some (hd, opf', op'))),
  (match some (hd, opf', op') with
    | none => h_1 ()
    | some (hd, opf', op') => h_2 hd opf' op') =
    h_2 hd opf' op'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, (t.insertIfNew k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Mathlib.Data.Fintype.EquivFin
Fintype.card_le_one_iff : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α ≤ 1 ↔ ∀ (a b : α), a = b
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.mem_iSup : ∀ {M : Type u_1} [inst : Add M] {ι : Sort u_3} (p : ι → AddSubsemigroup M) {m : M},
  m ∈ ⨆ i, p i ↔ ∀ (N : AddSubsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_fin_one_of : ∀ {R : Type u_6} [inst : AddCommMonoid R] (a : R), !![a].trace = a
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHSubOffset_4 : HSub Std.Time.WallTime Std.Time.Second.Offset Std.Time.WallTime
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Spanning.cRank_le_cardinalMk : ∀ {α : Type u} {M : Matroid α} {X : Set α} [M.InvariantCardinalRank], M.Spanning X → M.cRank ≤ Cardinal.mk ↑X
-- Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal
/-- Given a bilinear form `B` and some `x` such that `B x x ≠ 0`, the span of the singleton of `x`
is complement to its orthogonal complement.  -/
LinearMap.isCompl_span_singleton_orthogonal : ∀ {K : Type u_7} {V : Type u_9} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {B : V →ₗ[K] V →ₗ[K] K}
  {x : V}, (B x) x ≠ 0 → IsCompl (K ∙ x) (Submodule.orthogonalBilin B (K ∙ x))
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.hasStrictDerivAt_smul : ∀ {g : GL (Fin 2) ℝ},
  0 < (↑g).det →
    ∀ (τ : UpperHalfPlane),
      HasStrictDerivAt (fun z => ↑(g • ↑UpperHalfPlane.ofComplex z)) (↑(↑g).det / UpperHalfPlane.denom g ↑τ ^ 2) ↑τ
-- Init.Data.Range.Polymorphic.PRange
Std.Rco.mk.inj : ∀ {α : Type u} {lower upper lower_1 upper_1 : α},
  ((lower...upper) = lower_1...upper_1) → lower = lower_1 ∧ upper = upper_1
-- Mathlib.Algebra.Group.Nat.Even
Nat.not_even_one : ¬Even 1
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.dist_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y] {C r : NNReal} {f : X → Y},
  HolderWith C r f → ∀ (x y : X), dist (f x) (f y) ≤ ↑C * dist x y ^ ↑r
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_pow_le_of_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a : WithBot ℕ} (b : ℕ), p.degree ≤ a → (p ^ b).degree ≤ ↑b * a
-- Init.Data.UInt.Log2
/-- Base-two logarithm of 16-bit unsigned integers. Returns `⌊max 0 (log₂ a)⌋`.

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `UInt16.log2 0 = 0`
 * `UInt16.log2 1 = 0`
 * `UInt16.log2 2 = 1`
 * `UInt16.log2 4 = 2`
 * `UInt16.log2 7 = 2`
 * `UInt16.log2 8 = 3`
 -/
UInt16.log2 : UInt16 → UInt16
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : TopologicalSpace α] →
          [inst_3 : TopologicalSpace β] → (toOrderHom : α →o β) → Continuous toOrderHom.toFun → α →Co β
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Integration by parts**. Special case of
`intervalIntegrable.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right`
where the functions have a derivative also at the endpoints.
For improper integrals, see
`MeasureTheory.integral_mul_deriv_eq_deriv_mul`,
`MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul`,
and `MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul`.  -/
intervalIntegral.integral_mul_deriv_eq_deriv_mul : ∀ {a b : ℝ} {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A},
  (∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x) →
    (∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x) →
      IntervalIntegrable u' MeasureTheory.volume a b →
        IntervalIntegrable v' MeasureTheory.volume a b →
          ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.instFiniteTypeLocalizationOfFGSubtypeMemSubmonoid : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S] (M : Submonoid S) [Monoid.FG ↥M], Algebra.FiniteType R (Localization M)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.cokernelSequence_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.cokernelSequence f).X₁ = X
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The map that picks up the middle vertex of a 2-simplex, as a morphism in the 2-truncated
simplex category.  -/
SSet.Truncated.ι1₂ : { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 } ⟶
  { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 }
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- The linear equivalence between the fractional ideal `I` in a faithful localization
and the integral ideal `I.num`.  -/
FractionalIdeal.equivNumOfIsLocalization : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] →
            [FaithfulSMul R P] → [IsLocalization S P] → (I : FractionalIdeal S P) → ↥↑I ≃ₗ[R] ↥I.num
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Derivative of `f` at the point `x` within the set `s`, if it exists.  Zero otherwise.

If the derivative exists (i.e., `∃ f', HasDerivWithinAt f f' s x`), then
`f x' = f x + (x' - x) • derivWithin f s x + o(x' - x)` where `x'` converges to `x` inside `s`.
 -/
derivWithin : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type v} → [inst_1 : AddCommGroup F] → [Module 𝕜 F] → [TopologicalSpace F] → (𝕜 → F) → Set 𝕜 → 𝕜 → F
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Ring.polarBilin_pi : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (Mᵢ i)] [inst_2 : AddCommGroup P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P),
  (QuadraticMap.pi Q).polarBilin = ∑ i, LinearMap.compl₁₂ (Q i).polarBilin (LinearMap.proj i) (LinearMap.proj i)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] [IsDomain R₂]
  [Module.Free R₂ M₂] [Module.Finite R₂ M₂] {B : LinearMap.BilinForm R₂ M₂}, B.Nondegenerate ↔ LinearMap.ker B = ⊥
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.zero_lt_pow : ∀ (n : ℕ), 0 < 2 ^ n
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
AnalyticAt.hasFPowerSeriesAt : ∀ {𝕜 : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [CharZero 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜},
  AnalyticAt 𝕜 f x →
    HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.mk.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S']
  (toRingHom toRingHom_1 : P.Ring →+* P'.Ring) (e_toRingHom : toRingHom = toRingHom_1)
  (toRingHom_algebraMap :
    ∀ (x : R), toRingHom ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x))
  (algebraMap_toRingHom :
    ∀ (x : P.Ring), (algebraMap P'.Ring S') (toRingHom x) = (algebraMap S S') ((algebraMap P.Ring S) x)),
  { toRingHom := toRingHom, toRingHom_algebraMap := toRingHom_algebraMap,
      algebraMap_toRingHom := algebraMap_toRingHom } =
    { toRingHom := toRingHom_1, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
-- LeanSearchClient.Basic
statesearch.queries : Lean.Option ℕ
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
exists_one_lt_mul_of_lt : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : PartialOrder α] [CanonicallyOrderedMul α] {a b : α},
  a < b → ∃ c, ∃ (_ : 1 < c), a * c = b
-- Mathlib.Algebra.TrivSqZeroExt.Ideal
TrivSqZeroExt.kerIdeal.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] [inst_4 : IsCentralScalar R M],
  TrivSqZeroExt.kerIdeal R M = RingHom.ker (TrivSqZeroExt.fstHom R R M)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂'_apply' : ∀ {n : Type u_11} {m : Type u_12} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq m] {T : Type u_16} [inst_4 : CommSemiring T] (M : Matrix n m T) (v : n → T) (w : m → T),
  (((Matrix.toLinearMap₂' T) M) v) w = v ⬝ᵥ M.mulVec w
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The isomorphism which an adjunction `F ⊣ G` induces on `F.op ⋙ uliftCoyoneda`.
This states that `Adjunction.homEquiv` is natural in both arguments.  -/
CategoryTheory.Adjunction.compUliftCoyonedaIso : {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} →
            (F ⊣ G) →
              (F.op.comp CategoryTheory.uliftCoyoneda.{max w v₁, v₂, u₂} ≅
                CategoryTheory.uliftCoyoneda.{max w v₂, v₁, u₁}.comp
                  ((CategoryTheory.Functor.whiskeringLeft D C (Type (max (max w v₂) v₁))).obj G))
-- Mathlib.FieldTheory.PrimitiveElement
/-- This is the heart of the proof of the primitive element theorem. It shows that if `F` is
infinite and `α` and `β` are separable over `F` then `F⟮α, β⟯` is generated by a single element.  -/
Field.primitive_element_inf_aux : ∀ (F : Type u_1) [inst : Field F] [Infinite F] {E : Type u_2} [inst_2 : Field E] (α β : E) [inst_3 : Algebra F E]
  [Algebra.IsSeparable F E], ∃ γ, F⟮α, β⟯ = F⟮γ⟯
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.map_toSubalgebra : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : StarRing B]
  [inst_8 : Algebra R B] [inst_9 : StarModule R B] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B},
  (StarSubalgebra.map f S).toSubalgebra = Subalgebra.map (↑f) S.toSubalgebra
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousId'_inv_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F'' : CategoryTheory.Functor C C}
  (eF'' : F'' ≅ CategoryTheory.Functor.id C) (A : Type u) [inst_1 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : F''.IsContinuous J J] (X : CategoryTheory.Sheaf J A)
  (X_1 : Cᵒᵖ),
  ((CategoryTheory.Functor.sheafPushforwardContinuousId' eF'' A J).inv.app X).hom.app X_1 =
    X.obj.map (eF''.hom.app (Opposite.unop X_1)).op
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.forall_mono : ∀ {σs : List (Type u)} {α : Sort u_1} {Φ Ψ : α → Std.Do.SPred σs}, (∀ (a : α), Φ a ⊢ₛ Ψ a) → (∀ a, Φ a) ⊢ₛ ∀ a, Ψ a
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.coprime_of_coprime : ∀ {x y z : ℤ}, PythagoreanTriple x y z → x.gcd y = 1 → y.gcd z = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- If `c` is a colimiting binary coproduct cocone, and we have an initial object,
then we have `IsPushout 0 0 c.inl c.inr`
(where each `0` is the unique morphism from the initial object).  -/
CategoryTheory.IsPushout.of_is_coproduct : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y}
  (h : CategoryTheory.Limits.IsColimit c) (t : CategoryTheory.Limits.IsInitial Z),
  CategoryTheory.IsPushout
    (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }))
    (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Composing on the right by a function preserves uniform Cauchy sequences  -/
UniformCauchySeqOnFilter.comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α}
  {γ : Type u_5},
  UniformCauchySeqOnFilter F p p' → ∀ (g : γ → α), UniformCauchySeqOnFilter (fun n => F n ∘ g) p (Filter.comap g p')
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.restr_eq_of_source_subset : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α}, e.source ⊆ s → e.restr s = e