mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Multiset.ZeroCons
Multiset.zero_ne_cons : ∀ {α : Type u_1} {a : α} {m : Multiset α}, 0 ≠ a ::ₘ m
-- Mathlib.MeasureTheory.Function.LpSeminorm.Trim
MeasureTheory.eLpNorm_trim : ∀ {α : Type u_1} {ε : Type u_3} {m m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] (hm : m ≤ m0) {f : α → ε},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.eLpNorm f p (μ.trim hm) = MeasureTheory.eLpNorm f p μ
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.instPowFinNatOfNeZero : {n : ℕ} → [NeZero n] → Pow (Fin n) ℕ
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.mk_neg : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x : L),
  -ConjRootClass.mk K x = ConjRootClass.mk K (-x)
-- Mathlib.Algebra.Order.Group.Units
/-- The units of an ordered commutative additive monoid form an ordered commutative
additive group.  -/
AddUnits.isOrderedAddMonoid : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α], IsOrderedAddMonoid (AddUnits α)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.finCategoryWidePushout : {J : Type v} → [Fintype J] → CategoryTheory.FinCategory (CategoryTheory.Limits.WidePushoutShape J)
-- Mathlib.GroupTheory.Commutator.Basic
/-- **The Hall-Witt identity**  -/
addCommutatorElement_addCommutatorElement_addConj_add : ∀ {G : Type u_1} [inst : AddGroup G] (a b c : G), ⁅⁅a, b⁆, b + c + -b⁆ + ⁅⁅b, c⁆, c + a + -c⁆ + ⁅⁅c, a⁆, a + b + -a⁆ = 0
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  (U.cechIsoAugmentedCechNerve hT).inv.left = (U.cechIsoCechNerve hT).inv
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.ofClass_comp_monoidWithZeroHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulZeroOneClass α] [inst_4 : MulZeroOneClass β] [inst_5 : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β),
  MonoidWithZeroHom.ofClass (f.comp g) = (MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass g)
-- Mathlib.RingTheory.Perfection
Perfection.coeff_ne_zero_of_le : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] {f : Perfection R p}
  {m n : ℕ}, (Perfection.coeff R p m) f ≠ 0 → m ≤ n → (Perfection.coeff R p n) f ≠ 0
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.zigzag_symm : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J], Std.Symm CategoryTheory.Zigzag
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.measure_eq_zero_or_one_of_indep_self : ∀ {Ω : Type u_2} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.Indep m m μ → ∀ {t : Set Ω}, MeasurableSet t → μ t = 0 ∨ μ t = 1
-- Mathlib.Data.Set.Function
Set.EqOn.bijOn_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β},
  Set.EqOn f₁ f₂ s → (Set.BijOn f₁ s t ↔ Set.BijOn f₂ s t)
-- Aesop.Rule.Name
Aesop.instBEqBuilderName : BEq Aesop.BuilderName
-- Lean.Elab.Tactic.Grind.Basic
/-- Returns the list of goals. Goals may or may not already be assigned.  -/
Lean.Elab.Tactic.Grind.getGoals : Lean.Elab.Tactic.Grind.GrindTacticM (List Lean.Meta.Grind.Goal)
-- Lean.Elab.SyntheticMVars
/-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use `synthesizeUsingDefault`  -/
Lean.Elab.Term.withSynthesizeLight : {m : Type → Type u_1} → {α : Type} → [MonadFunctorT Lean.Elab.TermElabM m] → m α → m α
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c : α}, a ∣ b → c ∣ b → lcm a c ∣ b
-- Mathlib.Algebra.Group.Equiv.Defs
/-- An additive equivalence of additive groups preserves negation.  -/
AddEquiv.map_neg : ∀ {G : Type u_7} {H : Type u_8} [inst : AddGroup G] [inst_1 : SubtractionMonoid H] (h : G ≃+ H) (x : G), h (-x) = -h x
-- Mathlib.GroupTheory.Congruence.Defs
Con.rel_mk : ∀ {M : Type u_1} [inst : Mul M] {s : Setoid M} {h : ∀ {w x y z : M}, s w x → s y z → s (w * y) (x * z)} {a b : M},
  { toSetoid := s, mul' := h } a b ↔ s a b
-- Mathlib.Order.Filter.Map
Filter.map_principal : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Filter.map f (Filter.principal s) = Filter.principal (f '' s)
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.of_equiv : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f : M →ₗ[R] N} (e : TensorProduct R S M ≃ₗ[S] N),
  (∀ (x : M), e (1 ⊗ₜ[R] x) = f x) → IsBaseChange S f
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstFieldDeclParser : optParam ℕ 0 → Lean.Parser.Parser
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.algebraMap_def : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  algebraMap (MvPolynomial σ R) (MvPolynomial σ S) = MvPolynomial.map (algebraMap R S)
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.ext : ∀ {α : Type u_1} {p q : PMF α}, (∀ (x : α), p x = q x) → p = q
-- Lean.Environment
Lean.ImportM : Type → Type
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInst.mk.injEq : ∀ (toIndGroupInfo : Lean.Elab.Structural.IndGroupInfo) (levels : List Lean.Level) (params : Array Lean.Expr)
  (toIndGroupInfo_1 : Lean.Elab.Structural.IndGroupInfo) (levels_1 : List Lean.Level) (params_1 : Array Lean.Expr),
  ({ toIndGroupInfo := toIndGroupInfo, levels := levels, params := params } =
      { toIndGroupInfo := toIndGroupInfo_1, levels := levels_1, params := params_1 }) =
    (toIndGroupInfo = toIndGroupInfo_1 ∧ levels = levels_1 ∧ params = params_1)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart.instIsFiniteMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.IsFiniteMeasure (μ.singularPart ν)
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.stronglyMeasurable_condExpKernel : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : Set Ω},
  MeasurableSet s → MeasureTheory.StronglyMeasurable fun ω => ((ProbabilityTheory.condExpKernel μ m) ω) s
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projectionOnto`.

---

Projection to a submodule along a complement. It is the unique
linear map `f : E → p` such that `f x = x` for `x ∈ p` and `f x = 0` for `x ∈ q`.

For the projection from `E` to `E`, see `Submodule.projection`. See also:
* `Submodule.projectionOntoL` and `Submodule.projectionL` for the continuous versions.
* `Submodule.orthogonalProjection` and `Submodule.orthogonalProjectionOnto` for the projections
  along the orthogonal subspace.

See also `LinearMap.linearProjOfIsCompl`.  -/
Submodule.linearProjOfIsCompl : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → (p q : Submodule R E) → IsCompl p q → E →ₗ[R] ↥p
-- Mathlib.Data.Set.Piecewise
Set.piecewise_eq_of_notMem : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)] {i : α},
  i ∉ s → s.piecewise f g i = g i
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_iff_of_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ D} {φ : F₁ ⟶ F₂} {ψ : F₂ ⟶ F₃} {φψ : F₁ ⟶ F₃},
  CategoryTheory.CategoryStruct.comp φ ψ = φψ →
    ∀ [CategoryTheory.Presheaf.IsLocallyInjective J ψ],
      CategoryTheory.Presheaf.IsLocallyInjective J φψ ↔ CategoryTheory.Presheaf.IsLocallyInjective J φ
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- If `Φ : C ⥤ D` is an additive functor, a cochain `z : Cochain K L n` between
cochain complexes in `C` can be mapped to a cochain between the cochain complexes
in `D` obtained by applying the functor
`Φ.mapHomologicalComplex _ : CochainComplex C ℤ ⥤ CochainComplex D ℤ`.  -/
CochainComplex.HomComplex.Cochain.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          {D : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_1, u_2} D] →
              [inst_3 : CategoryTheory.Preadditive D] →
                CochainComplex.HomComplex.Cochain K L n →
                  (Φ : CategoryTheory.Functor C D) →
                    [inst_4 : Φ.Additive] →
                      CochainComplex.HomComplex.Cochain ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj K)
                        ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) n
-- Mathlib.Data.List.Basic
List.Sublist.antisymm : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₂.Sublist l₁ → l₁ = l₂
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.leftInv.eq_3 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (n : ℕ),
  p.leftInv i x n.succ.succ =
    -∑ c,
        ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑c)
          (p.leftInv i x (↑c).length)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntThms.default : Lean.Meta.Grind.Arith.Cutsat.ToIntThms
-- Mathlib.GroupTheory.OrderOfElement
pow_eq_pow_iff_modEq : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] {x : G} {m n : ℕ}, x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_multiset_prod : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : Multiset (MvPolynomial σ R)),
  s.prod.totalDegree ≤ (Multiset.map MvPolynomial.totalDegree s).sum
-- Init.Data.Nat.Gcd
Nat.gcd_left_eq_iff : ∀ {m m' n : ℕ}, m.gcd n = m'.gcd n ↔ ∀ (k : ℕ), k ∣ n → (k ∣ m ↔ k ∣ m')
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_hom_app_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C)
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B))
  (X : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)),
  ((CategoryTheory.Over.ConstructProducts.conesEquivUnitIso B F).hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.CategoryTheory.Triangulated.Functor
/-- The canonical isomorphism `(𝟭 C).mapTriangle ≅ 𝟭 (Triangle C)`.  -/
CategoryTheory.Functor.mapTriangleIdIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (CategoryTheory.Functor.id C).mapTriangle ≅ CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.toFinite_absolutelyContinuous : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SFinite μ],
  μ.toFinite.AbsolutelyContinuous μ
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
/-- If `ι.obj X₁ ⟶ ι.obj X₂ ⟶ ι.obj X₃ ⟶ ...` is a distinguished triangle,
then `X₃` is a cokernel of `X₁ ⟶ X₂`.  -/
CategoryTheory.Triangulated.AbelianSubcategory.isColimitCokernelCoforkOfDistTriang : {C : Type u_1} →
  {A : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
              [inst_5 : CategoryTheory.Pretriangulated C] →
                [inst_6 : CategoryTheory.Category.{v_2, u_2} A] →
                  {ι : CategoryTheory.Functor A C} →
                    (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)),
                        n < 0 → f = 0) →
                      [inst_7 : CategoryTheory.Preadditive A] →
                        [ι.Full] →
                          [inst_9 : ι.Faithful] →
                            [CategoryTheory.Limits.HasFiniteProducts A] →
                              [inst_11 : ι.Additive] →
                                {X₁ X₂ X₃ : A} →
                                  (f₁ : X₁ ⟶ X₂) →
                                    (f₂ : X₂ ⟶ X₃) →
                                      (f₃ : ι.obj X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)) →
                                        (hT :
                                            CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                          CategoryTheory.Limits.IsColimit
                                            (CategoryTheory.Limits.CokernelCofork.ofπ f₂ ⋯)
-- Mathlib.AlgebraicGeometry.Gluing
/-- The glue data of locally ringed spaces associated to a family of glue data of schemes.  -/
AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData : AlgebraicGeometry.Scheme.GlueData → AlgebraicGeometry.LocallyRingedSpace.GlueData
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureInformation.activeParameter? : Lean.Lsp.SignatureInformation → Option ℕ
-- Mathlib.Topology.Separation.DisjointCover
/-- If `S` is any neighbourhood of the diagonal in a topological space `X`, any point of `X` has an
open neighbourhood `U` such that `U ×ˢ U ⊆ S`.  -/
TopologicalSpace.exists_open_prod_subset_of_mem_nhds_diagonal : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (X × X)},
  S ∈ nhdsSet (Set.diagonal X) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ S
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.iterationObjRightIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C),
  (CategoryTheory.SmallObject.iterationObjRightIso I κ f).hom =
    CategoryTheory.Arrow.Hom.right ((CategoryTheory.SmallObject.ιIteration I κ).app f)
-- Lean.DocString.Types
/-- A link to some URL.
 -/
Lean.Doc.Inline.link : {i : Type u} → Array (Lean.Doc.Inline i) → String → Lean.Doc.Inline i
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toLinearEquiv_trans : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_5 : RingHomInvPair σ₁₃ σ₃₁] [inst_6 : RingHomInvPair σ₃₁ σ₁₃] [inst_7 : RingHomInvPair σ₂₃ σ₃₂]
  [inst_8 : RingHomInvPair σ₃₂ σ₂₃] [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_11 : SeminormedAddCommGroup E] [inst_12 : SeminormedAddCommGroup E₂] [inst_13 : SeminormedAddCommGroup E₃]
  [inst_14 : Module R E] [inst_15 : Module R₂ E₂] [inst_16 : Module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃),
  (e.trans e').toLinearEquiv = e.trans e'.toLinearEquiv
-- Init.Data.UInt.Lemmas
UInt8.ofFin_le_iff_le : ∀ {a b : Fin UInt8.size}, UInt8.ofFin a ≤ UInt8.ofFin b ↔ a ≤ b
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
EReal.measurableEmbedding_coe : MeasurableEmbedding Real.toEReal
-- Mathlib.Combinatorics.SetFamily.FourFunctions
collapse_of_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] {𝒜 : Finset (Finset α)} {a : α}
  {f : Finset α → β} {s t u : Finset α}, a ∉ s → t ∈ 𝒜 → u ∈ 𝒜 → t = s → u = insert a s → collapse✝ 𝒜 a f s = f t + f u
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeTR.eq_1 : ∀ {α : Type u_1} (n : ℕ) (l : List α), List.takeTR n l = List.takeTR.go✝ l l n #[]
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_self : ∀ {A : Type u_1} {E : Type u_2} {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module ℂ A}
  {inst_3 : AddCommGroup E} {inst_4 : Module ℂ E} {inst_5 : PartialOrder A} {inst_6 : SMul A E} {inst_7 : Norm A}
  {inst_8 : Norm E} [self : CStarModule A E] {x : E}, inner A x x = 0 ↔ x = 0
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.of_isLocalization : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R)
  [IsLocalization M S], Algebra.EssFiniteType R S
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toArray_eq_empty_iff : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], r.toArray = #[] ↔ (Std.PRange.succ? r.lower).isNone = true
-- Lean.Environment
/-- Get the current state of the given extension in the given environment.  -/
Lean.PersistentEnvExtension.getState : {α β σ : Type} →
  [Inhabited σ] →
    (ext : Lean.PersistentEnvExtension α β σ) →
      Lean.Environment →
        optParam Lean.EnvExtension.AsyncMode ext.toEnvExtension.asyncMode → optParam Lean.Name Lean.Name.anonymous → σ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.compare_maxKey_modify_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {f : β → β} {he : (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = false},
  compare ((Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey he) (t.maxKey ⋯) = Ordering.eq
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_even_mul_odd : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [T2Space M] [ContinuousMul M] {f : ℕ → M},
  (Multipliable fun k => f (2 * k)) →
    (Multipliable fun k => f (2 * k + 1)) → (∏' (k : ℕ), f (2 * k)) * ∏' (k : ℕ), f (2 * k + 1) = ∏' (k : ℕ), f k
-- Std.Data.HashSet.IteratorLemmas
_private.Std.Data.HashSet.IteratorLemmas.0.Std.HashSet.Raw.iter.eq_1 : ∀ {α : Type u} (m : Std.HashSet.Raw α), m.iter = Std.Iter.map (fun e => e.fst) m.inner.inner.iter
-- Mathlib.NumberTheory.Multiplicity
odd_sq_dvd_geom_sum₂_sub : ∀ {R : Type u_1} [inst : CommRing R] (a b : R) {p : ℕ},
  Odd p → ↑p ^ 2 ∣ ∑ i ∈ Finset.range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
deriv_sqrt_mul_log' : (deriv fun x => √x * Real.log x) = fun x => (2 + Real.log x) / (2 * √x)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instFiniteMapEmbedding : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finite] {f : α ↪ β}, (M.mapEmbedding f).Finite
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- The set of infinite places of `L` that are ramified over a given infinite place of `K`.  -/
NumberField.InfinitePlace.ramifiedPlacesOver : {K : Type u_4} →
  (L : Type u_5) →
    [inst : Field K] →
      [inst_1 : Field L] → [Algebra K L] → NumberField.InfinitePlace K → Set (NumberField.InfinitePlace L)
-- Std.Do.PostCond
Std.Do.ExceptConds.fst_false : ∀ {ε : Type u} {ps : Std.Do.PostShape}, Std.Do.ExceptConds.false.1 = fun _ε => ⌜False⌝
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.faithfulVAdd : ∀ {M' : Type u_4} {α : Type u_5} [inst : AddZeroClass M'] [inst_1 : VAdd M' α] {S : AddSubmonoid M'}
  [FaithfulVAdd M' α], FaithfulVAdd (↥S) α
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
          (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h)))
-- Mathlib.Order.Heyting.Basic
hnot_inf_distrib : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a b : α), ￢(a ⊓ b) = ￢a ⊔ ￢b
-- Mathlib.Data.ENat.Basic
ENat.add_one_le_iff : ∀ {m n : ℕ∞}, m ≠ ⊤ → (m + 1 ≤ n ↔ m < n)
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
MeasurableEquiv.coe_IicProdIoc : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] [inst_4 : (i : ι) → MeasurableSpace (X i)] {a b : ι} (hab : a ≤ b),
  ⇑(MeasurableEquiv.IicProdIoc hab) = IicProdIoc a b
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.toOption : {ρ : Type} →
  {ρ_1 : ρ} →
    {σ : String.Slice → Type} →
      [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ] →
        {s : String.Slice} → String.Slice.RevSplitIterator ρ_1 s → Option (Std.Iter (String.Slice.Pattern.SearchStep s))
-- Init.Core
/-- Transforms a pair by applying functions to both elements.

Examples:
* `(1, 2).map (· + 1) (· * 3) = (2, 6)`
* `(1, 2).map toString (· * 3) = ("1", 6)`
 -/
Prod.map : {α₁ : Type u₁} → {α₂ : Type u₂} → {β₁ : Type v₁} → {β₂ : Type v₂} → (α₁ → α₂) → (β₁ → β₂) → α₁ × β₁ → α₂ × β₂
-- Mathlib.Algebra.Order.Ring.Abs
abs_sq : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α] (x : α), |x ^ 2| = x ^ 2
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instLattice : {G : Type u_1} →
  [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [SeparatelyContinuousAdd G] → Lattice (OpenAddSubgroup G)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instMulZeroClass : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : MulZeroClass β] → [ContinuousMul β] → MulZeroClass (ZeroAtInftyContinuousMap α β)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.keys_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] {β : Type v} {l : List ((_ : α) × β)} {f : α → β → Bool},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.keys (List.filter (fun x => f x.fst x.snd) l) =
      (List.filter (fun x => f (↑x) (Std.Internal.List.getValue (↑x) l ⋯)) (Std.Internal.List.keys l).attach).unattach
-- Init.Data.String.Basic
String.Pos.ofSlice_lt_ofSlice_iff : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {q r : (s.slice p₀ p₁ h).Pos},
  String.Pos.ofSlice q < String.Pos.ofSlice r ↔ q < r
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.rank_le_finrank_engel : ∀ (K : Type u_7) {L : Type u_8} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : Module.Finite K L] (x : L), LieAlgebra.rank K L ≤ Module.finrank K ↥(LieSubalgebra.engel K x)