mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.hasEval : ∀ {τ : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : TopologicalSpace S] {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a → PowerSeries.HasEval a
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- A cone is dually finitely generated if and only if it is the dual of a finitely generated
cone.  -/
PointedCone.DualFG.iff_exists_fg_dual : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {C : PointedCone R N},
  PointedCone.DualFG p C ↔ ∃ D, Submodule.FG D ∧ PointedCone.dual p ↑D = C
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_self : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β), G.restrict G.edgeSet = G
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], k ∉ t₂ → (t₁ ∩ t₂).get! k = default
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] (f : SupBotHom α β),
  f.toFun = ⇑f
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Flattening with the outer combination specialized to `convexCombPair`.  -/
Convexity.convexCombPair_iConvexComb_iConvexComb : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {J₁ : Type u₁} {J₂ : Type u₂}
  (g₁ : Convexity.StdSimplex R J₁) (g₂ : Convexity.StdSimplex R J₂) (m₁ : J₁ → M) (m₂ : J₂ → M),
  Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb g₁ m₁) (Convexity.iConvexComb g₂ m₂) =
    Convexity.sConvexComb
      (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.map m₁ g₁) (Convexity.StdSimplex.map m₂ g₂))
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β),
  Function.Surjective ⇑e
-- Mathlib.Combinatorics.Colex
/-- `s ≤ {a}` in colex iff all elements of `s` are strictly less than `a`, except possibly `a` in
which case `s = {a}`.  -/
Finset.Colex.toColex_le_singleton : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a : α},
  toColex s ≤ toColex {a} ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)
-- Mathlib.Combinatorics.Additive.Corner.Roth
_private.Mathlib.Combinatorics.Additive.Corner.Roth.0.Corners.triangleIndices.instExplicitDisjoint : ∀ {G : Type u_1} [inst : AddCommGroup G] {A : Finset (G × G)},
  SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint (Corners.triangleIndices✝ A)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.ofEquivalence_Ω₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (𝒞₁ : CategoryTheory.Subobject.Classifier C) (e : C ≌ D), (𝒞₁.ofEquivalence e).Ω₀ = e.functor.obj 𝒞₁.Ω₀
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Subtracting the first vector passed to `oangle` from a multiple of the second vector negates
the sign of the angle.  -/
Orientation.oangle_sign_smul_sub_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ), (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign
-- Init.Data.List.Lemmas
List.isEqv.eq_3 : ∀ {α : Type u} (x x_1 : List α) (x_2 : α → α → Bool),
  (x = [] → x_1 = [] → False) →
    (∀ (a : α) (as : List α) (b : α) (bs : List α), x = a :: as → x_1 = b :: bs → False) → x.isEqv x_1 x_2 = false
-- Init.Data.Float.Model.Unpacked.Round
Float.Model.UnpackedFloat.Accuracy.inexact.sizeOf_spec : ∀ (relativeToPlusOneHalfUlp : Ordering),
  sizeOf (Float.Model.UnpackedFloat.Accuracy.inexact relativeToPlusOneHalfUlp) = 1 + sizeOf relativeToPlusOneHalfUlp
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.Hom.ext : ∀ {A B : MonCat} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.Tactic.ITauto
/-- `(p₁: Decidable A) (p₂: (x: A) ⊢ C) (p₃: (x: ¬ A) ⊢ C) ⊢ C`  -/
Mathlib.Tactic.ITauto.Proof.decidableElim : Bool → Lean.Name → Lean.Name → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.keysArray_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.keysArray = t₂.keysArray
-- Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
CategoryTheory.regularTopology.isLocallySurjective_iff : ∀ {C : Type u_1} (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {FD : D → D → Type u_3} {CD : D → Type w}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  [inst_4 : CategoryTheory.Preregular C] {F G : CategoryTheory.Functor Cᵒᵖ D} (f : F ⟶ G),
  CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f ↔
    ∀ (X : C) (y : CategoryTheory.ToType (G.obj (Opposite.op X))),
      ∃ X' φ,
        ∃ (_ : CategoryTheory.EffectiveEpi φ),
          ∃ x,
            (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X'))) x =
              (CategoryTheory.ConcreteCategory.hom (G.map (Opposite.op φ))) y
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.left_of_add_measure : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε}, MeasureTheory.Integrable f (μ + ν) → MeasureTheory.Integrable f μ
-- Lean.Data.PersistentArray
Lean.PersistentArray.mapM : {α : Type u} →
  {m : Type u → Type v} → [Monad m] → {β : Type u} → (α → m β) → Lean.PersistentArray α → m (Lean.PersistentArray β)
-- Mathlib.Topology.ContinuousOn
ContinuousAt.comp_continuousWithinAt_of_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {y : β},
  ContinuousAt g y → ContinuousWithinAt f s x → f x = y → ContinuousWithinAt (g ∘ f) s x
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousAt.continuousLinearMapCoprod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5}
  [inst_7 : TopologicalSpace X] {f : X → E →L[𝕜] G} {g : X → F →L[𝕜] G} {x : X},
  ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun x => (f x).coprod (g x)) x
-- Mathlib.Combinatorics.Matroid.Circuit
/-- The fundamental cocircuit of `X` and `e` has the junk value `{e}` if `e ∉ M.E`  -/
Matroid.fundCocircuit_eq_of_notMem_ground : ∀ {α : Type u_1} {M : Matroid α} {e : α} (X : Set α), e ∉ M.E → M.fundCocircuit e X = {e}
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomRight : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] (c : D) {d d' : C} (f : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight c f =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight (Opposite.op c) f.op).unop
-- Lean.CompactedRegion
_private.Lean.CompactedRegion.0.Lean.CompactedRegion.mk.sizeOf_spec : ∀ (filePath : System.FilePath) (size : USize) (isMemoryMapped : Bool) (baseAddr bufferOffset : USize)
  (root : NonScalar),
  sizeOf
      { filePath := filePath, size := size, isMemoryMapped := isMemoryMapped, baseAddr := baseAddr,
        bufferOffset := bufferOffset, root := root } =
    1 + sizeOf filePath + sizeOf size + sizeOf isMemoryMapped + sizeOf baseAddr + sizeOf bufferOffset + sizeOf root
-- Init.Control.Lawful.Instances
ReaderT.run_monadLift : ∀ {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_3} {α ρ : Type u_1} [inst : MonadLiftT n m] (x : n α) (ctx : ρ),
  (monadLift x).run ctx = monadLift x
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.congr : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.isGaussian_conv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [SecondCountableTopology E] {μ ν : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ]
  [ProbabilityTheory.IsGaussian ν], ProbabilityTheory.IsGaussian (μ.conv ν)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_iff_exists_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₂ : P}, p₂ ∈ s → (s.WSameSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂))
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The function from a given ring in the diagram to the colimit ring.  -/
RingCat.Colimits.coconeFun : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → (j : J) → ↑(F.obj j) → RingCat.Colimits.ColimitType F
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.lift_apply_apply : ∀ {R : Type u_1} [inst : CommRing R] {d : ℤ} (r : { r // r * r = ↑d }) (a : ℤ√d), (Zsqrtd.lift r) a = ↑a.re + ↑a.im * ↑r
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- Commutativity of multiplication in commutative subobjects.  -/
setLike_mul_comm : ∀ {S : Type u_3} {M : Type u_4} [inst : SetLike S M] [inst_1 : Mul M] [inst_2 : MulMemClass S M] {s : S}
  [IsMulCommutative ↥s] ⦃a b : M⦄, a ∈ s → b ∈ s → a * b = b * a
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.colimMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [W.IsStableUnderColimitsOfShape J] {X Y : CategoryTheory.Functor J C}
  (f : X ⟶ Y) [inst_3 : CategoryTheory.Limits.HasColimit X] [inst_4 : CategoryTheory.Limits.HasColimit Y],
  W.functorCategory J f → W (CategoryTheory.Limits.colimMap f)
-- Mathlib.Order.CompleteLattice.Lemmas
iInf_bool_eq : ∀ {α : Type u_1} [inst : CompleteLattice α] {f : Bool → α}, ⨅ b, f b = f true ⊓ f false
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.replicate.match_1.splitter : {w : ℕ} →
  (motive : ℕ → BitVec w → Sort u_1) →
    (x : ℕ) →
      (x_1 : BitVec w) → ((x : BitVec w) → motive 0 x) → ((n : ℕ) → (x : BitVec w) → motive n.succ x) → motive x x_1
-- Mathlib.Algebra.Order.Group.Bounds
IsGLB.exists_between_self_add' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {s : Set α} {a ε : α},
  IsGLB s a → a ∉ s → 0 < ε → ∃ b ∈ s, a < b ∧ b < a + ε
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_one_sub_smoothingFn_gt_const : ∀ c < 1, ∀ᶠ (n : ℕ) in Filter.atTop, c < 1 - AkraBazziRecurrence.smoothingFn ↑n
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.sumComm_symm_apply : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (a : W ⊕ V),
  (RelIso.symm SimpleGraph.Iso.sumComm) a = a.swap
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
/-- Premature version of the lemma. Prefer using `left_invariant` instead.  -/
LeftInvariantDerivation.left_invariant' : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G] (g : G)
  (X : LeftInvariantDerivation I G), (hfdifferential ⋯) ((Derivation.evalAt 1) ↑X) = (Derivation.evalAt g) ↑X
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- Given `W : MorphismProperty C` and a well-ordered type `J`, this is
the class of morphisms that are transfinite composition of shape `J`
of morphisms in `W`.  -/
CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C →
      (J : Type w) →
        [inst_1 : LinearOrder J] → [SuccOrder J] → [OrderBot J] → [WellFoundedLT J] → CategoryTheory.MorphismProperty C
-- Qq.Macro
Qq.Impl.unquoteExprMVar : Lean.Expr → Qq.Impl.UnquoteM Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Complex.sin_eq_tsum : ∀ (z : ℂ), Complex.sin z = ∑' (n : ℕ), (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1).factorial
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.bddAbove_preimage : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α},
  s.PartiallyWellOrderedOn r → ∀ {f : ℕ → α}, (∀ (m n : ℕ), m < n → ¬r (f m) (f n)) → BddAbove (f ⁻¹' s)
-- Lean.Level
Lean.mkLevelMVar : Lean.LMVarId → Lean.Level
-- Init.Data.AC
Lean.Data.AC.ContextInformation.isComm : {α : Sort u} → [self : Lean.Data.AC.ContextInformation α] → α → Bool
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_last : ∀ {w : ℕ} (x : BitVec w), x.getMsbD 0 = decide (2 ^ (w - 1) ≤ x.toNat)
-- Std.Data.TreeMap.Raw.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.TreeMap.Raw.getKey? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Option α
-- Init.Data.Array.Lemmas
Array.size_pos_iff_exists_push : ∀ {α : Type u_1} {xs : Array α}, 0 < xs.size ↔ ∃ ys a, xs = ys.push a
-- Mathlib.Tactic.GRewrite.Core
/-- Recursively call `grewriteCore` to process a subgoal of a `gcongr` lemma.

Returns whether we have done a rewrite in this subgoal, in which case it has been closed.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.processGCongrHypothesisAux : Lean.MVarId → Bool → Mathlib.Tactic.GRewrite.Config → Mathlib.Tactic.GRewrite.GRewriteM✝ Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β} {f : Option β → Option β},
  Std.DHashMap.Const.getD (Std.DHashMap.Const.alter m k f) k fallback = (f (Std.DHashMap.Const.get? m k)).getD fallback
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates limits of shape `J`, and `D` has limits of shape `J`, then
`C` has limits of shape `J`.
 -/
CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.CreatesLimitsOfShape J F],
  CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.equivNatTrans_apply : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : CategoryTheory.Functor C₁ C₃)
  (R : CategoryTheory.Functor C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) (w : CategoryTheory.TwoSquare T L R B),
  (CategoryTheory.TwoSquare.equivNatTrans T L R B) w = w.natTrans
-- Mathlib.Topology.Algebra.InfiniteSum.Group
tsum_const : ∀ {β : Type u_2} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [IsTopologicalAddGroup G]
  [T2Space G] (a : G), ∑' (x : β), a = Nat.card β • a
-- Init.GetElem
/-- Internal implementation of `as[i]!`. Do not use directly.  -/
List.get!Internal : {α : Type u_1} → [Inhabited α] → List α → ℕ → α
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_mono : ∀ {σs : List (Type u)} {P P' Q Q' : Std.Do.SPred σs}, (Q ⊢ₛ P) → (P' ⊢ₛ Q') → (P → P') ⊢ₛ Q → Q'
-- Mathlib.Algebra.Ring.NonZeroDivisors
IsRightRegular.pow_injective : ∀ {M : Type u_2} [inst : Monoid M] [IsMulTorsionFree M] {x : M},
  IsRightRegular x → x ≠ 1 → Function.Injective fun n => x ^ n
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {ζ : K} {k : ℕ},
  2 < k → IsPrimitiveRoot ζ k → NumberField.InfinitePlace.nrRealPlaces K = 0
-- Mathlib.Topology.Homotopy.HSpaces
/-- A topological space `X` is an H-space if it behaves like a (potentially non-associative)
topological group, but where the axioms for a group only hold up to homotopy.
 -/
HSpace : (X : Type u) → [TopologicalSpace X] → Type u
-- Mathlib.Data.Num.Basic
PosNum.instLT : LT PosNum
-- Mathlib.MeasureTheory.Measure.Dirac
/-- Given that `α` is a countable, measurable space with all singleton sets measurable,
write the measure of a set `s` as the sum of the measure of `{x}` for all `x ∈ s`.  -/
MeasureTheory.Measure.tsum_indicator_apply_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α)
  (s : Set α), MeasurableSet s → ∑' (x : α), s.indicator (fun x => μ {x}) x = μ s
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_Ici : ∀ (x : NNReal), NNReal.toReal '' Set.Ici x = Set.Ici ↑x
-- Init.Data.Vector.Lex
Vector.lt_iff_exists : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] {xs ys : Vector α n},
  xs < ys ↔ ∃ i, ∃ (h : i < n), (∀ (j : ℕ) (hj : j < i), xs[j] = ys[j]) ∧ xs[i] < ys[i]
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_add_Ioi : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a + x) ⁻¹' Set.Ioi b = Set.Ioi (b - a)
-- Std.Data.TreeMap.Raw.AdditionalOperations
/-- Updates the values of the map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.TreeMap.Raw.filterMap : {α : Type u} →
  {β : Type v} →
    {γ : Type w} → {cmp : α → α → Ordering} → (α → β → Option γ) → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α γ cmp
-- Mathlib.Tactic.NormNum.Irrational
Mathlib.Meta.NormNum.NotPowerCertificate.mk.inj : ∀ {m n k : Q(ℕ)} {pf_left : Q(«$k» ^ «$n» < «$m»)} {pf_right : Q(«$m» < («$k» + 1) ^ «$n»)} {k_1 : Q(ℕ)}
  {pf_left_1 : Q(«$k_1» ^ «$n» < «$m»)} {pf_right_1 : Q(«$m» < («$k_1» + 1) ^ «$n»)},
  { k := k, pf_left := pf_left, pf_right := pf_right } = { k := k_1, pf_left := pf_left_1, pf_right := pf_right_1 } →
    k = k_1 ∧ pf_left = pf_left_1 ∧ pf_right = pf_right_1
-- Init.Data.Nat.Lemmas
Nat.exists_add_one_eq : ∀ {a : ℕ}, (∃ n, n + 1 = a) ↔ 0 < a
-- Mathlib.Tactic.TacticAnalysis
_private.Mathlib.Tactic.TacticAnalysis.0.Mathlib.TacticAnalysis.Entry.import.unsafe_impl_5 : Mathlib.TacticAnalysis.Entry → Lean.Environment → Lean.Options → Except String (Lean.Option Bool)
-- Init.Data.List.Basic
List.Perm.below.swap : ∀ {α : Type u} {motive : (a a_1 : List α) → a.Perm a_1 → Prop} (x y : α) (l : List α), List.Perm.below ⋯
-- Mathlib.CategoryTheory.Limits.Types.End
/-- The wedge corresponding to the explicit end in `Type`.  -/
CategoryTheory.Limits.Types.wedge : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))) → CategoryTheory.Limits.Wedge F
-- Mathlib.Algebra.Lie.Abelian
LieModule.coe_maxTrivHom_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (f : M →ₗ⁅R,L⁆ N) (m : ↥(LieModule.maxTrivSubmodule R L M)),
  ↑((LieModule.maxTrivHom f) m) = f ↑m
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Measurable.nndist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] [SecondCountableTopology α] {f g : β → α},
  Measurable f → Measurable g → Measurable fun b => nndist (f b) (g b)
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_singleton : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {x : α} {f : α → β}, List.maxIdxOn f [x] ⋯ = 0
-- Mathlib.Order.Height
Set.chainHeight_eq_of_relIso : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} (s : Set α) (e : r ≃r r'),
  (⇑e '' s).chainHeight r' = s.chainHeight r
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.toNNReal : ∀ {p q : ℝ}, p.HolderConjugate q → p.toNNReal.HolderConjugate q.toNNReal
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.prod_withDensity₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {mβ : MeasurableSpace β}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : α → ENNReal} {g : β → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g ν → (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun z => f z.1 * g z.2
-- Mathlib.RepresentationTheory.Action
/-- The tensor (multiplication) of the linearize functor.  -/
Representation.LinearizeMonoidal.μ : {G : Type v} →
  [inst : Monoid G] →
    (X Y : Action (Type w) G) →
      {k : Type u} →
        [inst_1 : CommSemiring k] →
          ((Representation.linearize k G X).tprod (Representation.linearize k G Y)).IntertwiningMap
            (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
CategoryTheory.Limits.instIsIsoCoprodComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison G X Y)
-- Init.Data.Array.Int
Array.prod_reverse_int : ∀ (xs : Array ℤ), xs.reverse.prod = xs.prod
-- Std.Data.TreeMap.Raw.Iterator
/-- Returns a finite iterator over the keys of a tree map.
The iterator yields the keys in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.TreeMap.Raw.keysIter : {α β : Type u} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Std.Iter α
-- Init.Data.String.Lemmas.FindPos
String.Pos.prevn_add_one : ∀ {n : ℕ} {s : String} {p : s.Pos}, p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n
-- Mathlib.Topology.Category.Profinite.Product
Profinite.isIso_indexCone_lift : ∀ {ι : Type u} {X : ι → Type} [inst : (i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)}
  [inst_1 : ∀ (i : ι), T2Space (X i)] [inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)] (hC : IsCompact C),
  CategoryTheory.IsIso ((Profinite.limitConeIsLimit (Profinite.indexFunctor hC)).lift (Profinite.indexCone hC))