mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.AlgebraicCard
Algebraic.cardinalMk_of_countable_of_charZero : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing A] [IsDomain A] [inst_4 : Algebra R A]
  [Module.IsTorsionFree R A] [Countable R] [CharZero A], Cardinal.mk { x // IsAlgebraic R x } = Cardinal.aleph0
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_lt_iff_lt : ∀ {a b : ℤ} (ha₁ : Int8.minValue.toInt ≤ a) (ha₂ : a ≤ Int8.maxValue.toInt) (hb₁ : Int8.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int8.maxValue.toInt), Int8.ofIntLE a ha₁ ha₂ < Int8.ofIntLE b hb₁ hb₂ ↔ a < b
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (V : S.Opens) [AlgebraicGeometry.GeometricallyIntegral f],
  AlgebraicGeometry.GeometricallyIntegral (f ∣_ V)
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_eq_norm_sq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), RCLike.re (inner 𝕜 x x) = ‖x‖ ^ 2
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.normalizer_le_normalizer_sup_of_normalizer_le_right : ∀ {G : Type u_2} [inst : Group G] {H K : Subgroup G},
  Subgroup.normalizer ↑H ≤ Subgroup.normalizer ↑K → Subgroup.normalizer ↑H ≤ Subgroup.normalizer ↑(K ⊔ H)
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.hasFiniteLimits : CategoryTheory.Limits.HasFiniteLimits FintypeCat
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.nonempty' : ∀ {L : FirstOrder.Language} {T : L.Theory} (self : T.ModelType), Nonempty ↑self
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsCofilteredULiftHom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C],
  CategoryTheory.IsCofiltered (CategoryTheory.ULiftHom C)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_strictMono_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Surjective ⇑f → StrictMono (AddSubsemigroup.comap f)
-- Mathlib.Geometry.Euclidean.Volume.Measure
instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast : ∀ (d : ℕ), (MeasureTheory.Measure.hausdorffMeasure ↑d).IsAddHaarMeasure
-- Mathlib.Topology.Continuous
DenseRange.nonempty_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X}, DenseRange f → (Nonempty α ↔ Nonempty X)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.T_sub : ∀ {R : Type u_1} [inst : Semiring R] (m n : ℤ),
  LaurentPolynomial.T (m - n) = LaurentPolynomial.T m * LaurentPolynomial.T (-n)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalysisLetVarType : Lean.Options → Bool
-- Mathlib.Algebra.Module.Injective
Module.injective_of_ulift_injective : ∀ (R : Type u) [inst : Ring R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Injective R (ULift.{v', v} M) → Module.Injective R M
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.ContextualizedCompletionInfo : Type
-- Mathlib.Order.Interval.Lex
NonemptyInterval.toLex_mono : ∀ {α : Type u_1} [inst : PartialOrder α], Monotone ⇑toLex
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- `irrelevant 𝒜 = ⨁_{i>0} 𝒜ᵢ`  -/
HomogeneousIdeal.irrelevant_eq_iSup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜],
  (HomogeneousIdeal.irrelevant 𝒜).toAddSubmonoid = ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_le_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {km kmi : α}, t.maxKey? = some km → (t.insert k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_inter_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₂.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.ne_zero_of_mem_roots : ∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, a ∈ p.roots → p ≠ 0
-- Mathlib.Lean.Expr.Basic
/-- Given `f a₀ a₁ ... aₙ₋₁`, runs `modifier` on the `i`th argument or
returns the original expression if out of bounds.  -/
Lean.Expr.modifyArg : (Lean.Expr → Lean.Expr) → (e : Lean.Expr) → ℕ → optParam ℕ e.getAppNumArgs → Lean.Expr
-- Init.Data.Array.MinMax
Array.isSome_max?_iff : ∀ {α : Type u_1} {xs : Array α} [inst : Max α], xs.max?.isSome = true ↔ xs ≠ #[]
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.indicatorConstLp_coeFn_notMem : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E},
  ∀ᵐ (x : α) ∂μ, x ∉ s → ↑↑(MeasureTheory.indicatorConstLp p hs hμs c) x = 0
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- In the characteristic zero case, the weights in the centroid sum
to 1 if the number of points is `n + 1`.  -/
Finset.sum_centroidWeights_eq_one_of_card_eq_add_one : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] {n : ℕ},
  s.card = n + 1 → ∑ i ∈ s, Finset.centroidWeights k s i = 1
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- If the inner product of two unit vectors is strictly less than `1`, then the two vectors are
distinct. One form of the equality case for Cauchy-Schwarz.  -/
inner_lt_one_iff_real_of_norm_eq_one : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  ‖x‖ = 1 → ‖y‖ = 1 → (inner ℝ x y < 1 ↔ x ≠ y)
-- Init.Data.Rat.Lemmas
Rat.neg_zero : -0 = 0
-- Mathlib.Order.Category.HeytAlg
HeytAlg.inv_hom_apply : ∀ {X Y : HeytAlg} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.colimitCocone.eq_1 : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)),
  AlgebraicGeometry.PresheafedSpace.colimitCocone F =
    { pt := AlgebraicGeometry.PresheafedSpace.colimit F,
      ι :=
        {
          app := fun j =>
            { base := CategoryTheory.Limits.colimit.ι (F.comp (AlgebraicGeometry.PresheafedSpace.forget C)) j,
              c :=
                CategoryTheory.Limits.limit.π (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp
                  (Opposite.op j) },
          naturality := ⋯ } }
-- Mathlib.Data.Finset.Preimage
Finset.preimage.congr_simp : ∀ {α : Type u} {β : Type v} (s s_1 : Finset β) (e_s : s = s_1) (f f_1 : α → β) (e_f : f = f_1)
  (hf : Set.InjOn f (f ⁻¹' ↑s)), s.preimage f hf = s_1.preimage f_1 ⋯
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- If `P : ProjectiveResolution X`, then the chosen `(projectiveResolutions C).obj X`
is isomorphic (in the homotopy category) to `P.complex`.  -/
CategoryTheory.ProjectiveResolution.iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasProjectiveResolutions C] →
        {X : C} →
          (P : CategoryTheory.ProjectiveResolution X) →
            (CategoryTheory.projectiveResolutions C).obj X ≅
              (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj P.complex
-- Lean.Elab.Command
Lean.Elab.Command.Linter : Type
-- Mathlib.Algebra.Group.Translate
translate_eq_domAddActMk_vadd : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] (a : G) (f : G → α), translate a f = DomAddAct.mk (-a) +ᵥ f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.comp_right_triangle_aux : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b}
  (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂),
  CategoryTheory.Bicategory.rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp g₂ g₁)).hom
      (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp g₂ g₁)).inv
-- Mathlib.Geometry.Manifold.Algebra.SMul
instContMDiffSMulOfNatWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : SMul G M]
  [ContMDiffSMul I I' 2 G M], ContMDiffSMul I I' 1 G M
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.smul_def : ∀ {G : Type u_1} {K : Type u_2} {V : Type u_3} [inst : AddCommGroup V] [inst_1 : DivisionRing K] [inst_2 : Module K V]
  [inst_3 : Group G] [inst_4 : DistribMulAction G V] [inst_5 : SMulCommClass G K V] (g : G) (x : Projectivization K V),
  SMul.smul g x = Projectivization.map ((DistribMulAction.toModuleEnd K V) g) ⋯ x
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- The change-of-basis matrix between two orthonormal bases with the opposite orientations has
determinant -1.  -/
OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e f : OrthonormalBasis ι ℝ E),
  e.toBasis.orientation ≠ f.toBasis.orientation → e.toBasis.det ⇑f = -1
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.neg_mul : ∀ {w : ℕ} (x y : BitVec w), (~~~x + 1#w) * y = ~~~(x * y) + 1#w
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km : α},
  t.min? = some km → km ∈ t
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.CongrInfo.none.sizeOf_spec : sizeOf Lean.Meta.Sym.CongrInfo.none = 1
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.rightUnitorNatIsoCat_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitorNatIsoCat a b).inv.toNatTrans.app X =
    (CategoryTheory.Bicategory.rightUnitor X).inv
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (b : β a), m.insertₘ a b = if m.containsₘ a = true then m.replaceₘ a b else (m.consₘ a b).expandIfNecessary
-- Mathlib.Analysis.Calculus.Deriv.Prod
HasStrictDerivAt.prodMk : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f₁ : 𝕜 → F} {f₁' : F} {x : 𝕜} {G : Type w} [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 G] {f₂ : 𝕜 → G} {f₂' : G},
  HasStrictDerivAt f₁ f₁' x → HasStrictDerivAt f₂ f₂' x → HasStrictDerivAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') x
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresenter.mk : String → ProofWidgets.LayoutKind → (Lean.Expr → Lean.MetaM ProofWidgets.Html) → ProofWidgets.ExprPresenter
-- Mathlib.Order.Filter.AtTopBot.Finset
Filter.tendsto_finset_Ici_atBot_atTop : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α],
  Filter.Tendsto Finset.Ici Filter.atBot Filter.atTop
-- Lean.Elab.InfoTree.Types
Lean.Elab.MacroExpansionInfo.output : Lean.Elab.MacroExpansionInfo → Lean.Syntax
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.comp_continuousOn : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β}
  [inst_2 : TopologicalSpace δ] {s : Set δ} {g : δ → α} {b : δ},
  IsLocalMax f (g b) → ContinuousOn g s → b ∈ s → IsLocalMaxOn (f ∘ g) s b
-- Mathlib.Data.Set.Countable
Finset.countable_toSet : ∀ {α : Type u} (s : Finset α), (↑s).Countable
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instIsAddTorsionFree : IsAddTorsionFree ℕ
-- Mathlib.Data.Fintype.Defs
Fintype.mk : {α : Type u_4} → (elems : Finset α) → (∀ (x : α), x ∈ elems) → Fintype α
-- Mathlib.Algebra.Free
FreeAddSemigroup.instLawfulMonad : LawfulMonad FreeAddSemigroup
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.toReal_rpow : ∀ (x : ENNReal) (z : ℝ), x.toReal ^ z = (x ^ z).toReal
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.clift_self : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {T : Bundle.Trivialization F proj} {ι : Type u_5} [inst_3 : TopologicalSpace ι]
  [inst_4 : LocallyCompactPair ι ↑T.baseSet] {γ : C(ι, ↑T.baseSet)} {i : ι} {e : ↑T.source},
  proj ↑e = ↑(γ i) → (T.clift (e, γ)) i = e
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.setIntegral_density : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s → ∀ {A : Set γ}, MeasurableSet A → ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  (CochainComplex.mappingCone.inl φ).comp (CochainComplex.mappingCone.snd φ) ⋯ = 0
-- Mathlib.Topology.ContinuousMap.Polynomial
/-- Every polynomial with coefficients in a topological semiring gives a (bundled) continuous function.
 -/
Polynomial.toContinuousMap : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : TopologicalSpace R] → [IsTopologicalSemiring R] → Polynomial R → C(R, R)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.refl.sizeOf_spec : ∀ {R : Type u} [inst : Rack R] [inst_1 : SizeOf R] {a : Rack.PreEnvelGroup R},
  sizeOf Rack.PreEnvelGroupRel'.refl = 1 + sizeOf a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a fallback : α} {v : β},
      (m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree.  -/
Std.DTreeMap.Internal.Impl.BalancedTree.impl : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl.BalancedTree α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- **Alias** of `AlgebraicGeometry.StructureSheaf.algebraMap_germ`. -/
AlgebraicGeometry.StructureSheaf.toOpen_germ : ∀ {R : Type u} [inst : CommRing R] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hxU : x ∈ U),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op U))))
      ((AlgebraicGeometry.structurePresheafInCommRingCat R).germ U x hxU) =
    AlgebraicGeometry.StructureSheaf.toStalk R x
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.IsSubDPIdeal.self : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I), hI.IsSubDPIdeal I
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.brecOn_2.eq : ∀ {motive_1 : Lean.IR.IRType → Sort u} {motive_2 : Array Lean.IR.IRType → Sort u}
  {motive_3 : List Lean.IR.IRType → Sort u} (t : List Lean.IR.IRType)
  (F_1 : (t : Lean.IR.IRType) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.IR.IRType) → Lean.IR.IRType.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.IR.IRType) → Lean.IR.IRType.below_2 t → motive_3 t),
  Lean.IR.IRType.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.IR.IRType.brecOn_2.go t F_1 F_2 F_3).2
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_eq_toFinset_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (s : Set α) [inst_1 : Fintype ↑s],
  ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ s.toFinset, f i
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.le_degreeOf_of_mem_support : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} (i : σ) {s : σ →₀ ℕ},
  s ∈ p.support → s i ≤ MvPolynomial.degreeOf i p
-- Mathlib.Algebra.Field.Periodic
/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
`y ∈ Ioc a (a + c)` such that `f x = f y`.  -/
Function.Periodic.exists_mem_Ioc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α] [inst_1 : LinearOrder α]
  [IsOrderedAddMonoid α] [Archimedean α],
  Function.Periodic f c → 0 < c → ∀ (x a : α), ∃ y ∈ Set.Ioc a (a + c), f x = f y
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_eq_aleph0 : ∀ {c : Cardinal.{u}}, Cardinal.lift.{v, u} c = Cardinal.aleph0 ↔ c = Cardinal.aleph0
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
/-- **Alias** of the forward direction of `ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith`. -/
ApproximatesLinearOn.lipschitzOnWith : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {s : Set E} {c : NNReal}, ApproximatesLinearOn f f' s c → LipschitzOnWith c (f - ⇑f') s
-- Init.Data.List.TakeDrop
List.takeWhile_filter : ∀ {α : Type u_1} {p q : α → Bool} {l : List α},
  List.takeWhile q (List.filter p l) = List.filter p (List.takeWhile (fun a => !p a || q a) l)
-- Mathlib.Data.List.Sym
List.Perm.sym2 : ∀ {α : Type u_1} {xs ys : List α}, xs.Perm ys → xs.sym2.Perm ys.sym2
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_swapEquiv_symm_apply : ∀ {R : Type u_3} (c₁ c₃ : R) [inst : CommRing R] (t : QuaternionAlgebra R c₃ 0 c₁),
  ((QuaternionAlgebra.swapEquiv c₁ c₃).symm t).imK = -t.imK
-- Lean.Compiler.NameMangling
String.Internal.mangle : String → String
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.isBigO_congr_left : ∀ {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [inst : Norm G] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedAddCommGroup F'] {k : α → G} {f' : α → E'} {g' : α → F'} {l : Filter α},
  f' =Θ[l] g' → (f' =O[l] k ↔ g' =O[l] k)
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `ContinuousWithinAt.inv` -/
ContinuousWithinAt.fun_inv : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Inv G]
  [ContinuousInv G] {f : X → G} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun i => (f i)⁻¹) s x
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- In a Dedekind domain, the (nonzero) prime elements of the monoid with zero `Ideal A`
are exactly the prime ideals.  -/
Ideal.prime_iff_isPrime : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {P : Ideal A}, P ≠ ⊥ → (Prime P ↔ P.IsPrime)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_mkPiAlgebra_le : ∀ {𝕜 : Type u} {ι : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {A : Type u_1}
  [inst_2 : NormedCommRing A] [inst_3 : NormedAlgebra 𝕜 A] [Nonempty ι],
  ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ 1
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- The definition of `AffineIndependent`.  -/
affineIndependent_def : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P),
  AffineIndependent k p ↔ ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → (s.weightedVSub p) w = 0 → ∀ i ∈ s, w i = 0
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_enorm_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {f : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ → (MeasureTheory.MemLp (fun x => ‖f x‖ₑ) p μ ↔ MeasureTheory.MemLp f p μ)
-- Init.Data.UInt.Lemmas
UInt64.lt_iff_le_and_ne : ∀ {a b : UInt64}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_add_div_mul : ∀ {a c : Ordinal.{u_4}}, c < a → ∀ (b d : Ordinal.{u_4}), (a * b + c) / (a * d) = b / d
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Complex.hasDerivAt_tan : ∀ {x : ℂ}, Complex.cos x ≠ 0 → HasDerivAt Complex.tan (1 / Complex.cos x ^ 2) x
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n)
      ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) =
    0
-- Init.Data.Order.Ord
Std.OrientedCmp.mk : ∀ {α : Type u} {cmp : α → α → Ordering}, (∀ {a b : α}, cmp a b = (cmp b a).swap) → Std.OrientedCmp cmp
-- Mathlib.Data.PNat.Interval
PNat.map_subtype_embedding_Ico : ∀ (a b : ℕ+), Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Ico a b) = Finset.Ico ↑a ↑b
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.orthogonalProjectionFn.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K K_1 : Submodule 𝕜 E} (e_K : K = K_1) [inst_3 : K.HasOrthogonalProjection] (x x_1 : E),
  x = x_1 → Submodule.orthogonalProjectionFn x = Submodule.orthogonalProjectionFn x_1
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.isFiniteKernel_seq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [h : ProbabilityTheory.IsSFiniteKernel κ] (n : ℕ), ProbabilityTheory.IsFiniteKernel (κ.seq n)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk_lt_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (x y : K)
  (hx : 0 ≤ ArchimedeanClass.mk x) (hy : 0 ≤ ArchimedeanClass.mk y),
  ArchimedeanClass.FiniteElement.mk x hx < ArchimedeanClass.FiniteElement.mk y hy ↔ x < y
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a `k`-linear `G`-representation `V, ρ`, this is the map `(V ⊗ k[G])_G →ₗ[k] V` sending
`⟦v ⊗ single g r⟧ ↦ r • ρ(g⁻¹)(v)`.  -/
Representation.ofCoinvariantsTprodLeftRegular : {k : Type u_6} →
  {G : Type u_7} →
    {V : Type u_8} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) → (ρ.tprod (Representation.leftRegular k G)).Coinvariants →ₗ[k] V
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.closure_univ : ∀ {M : Type u_1} [inst : MulOneClass M], Submonoid.closure Set.univ = ⊤
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.left_eq_zero_of_add_eq_zero : ∀ {a b : Ordinal.{u_4}}, a + b = 0 → a = 0