mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- If a compact operator preserves a closed submodule, its restriction to that submodule is
compact.

Note that, following mathlib's convention in linear algebra, `restrict` designates the restriction
of an endomorphism `f : E →ₗ E` to an endomorphism `f' : ↥V →ₗ ↥V`. To prove that the restriction
`f' : ↥U →ₛₗ ↥V` of a compact operator `f : E →ₛₗ F` is compact, apply
`IsCompactOperator.codRestrict` to `f ∘ U.subtypeL`, which is compact by
`IsCompactOperator.comp_clm`.  -/
IsCompactOperator.restrict : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_3} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] {f : M₁ →ₗ[R₁] M₁},
  IsCompactOperator ⇑f →
    ∀ {V : Submodule R₁ M₁} (hV : ∀ v ∈ V, f v ∈ V), IsClosed ↑V → IsCompactOperator ⇑(f.restrict hV)
-- Init.ByCases
/-- A function applied to a `dite` is a `dite` of that function applied to each of the branches.  -/
apply_dite : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (P : Prop) [inst : Decidable P] (x : P → α) (y : ¬P → α),
  f (dite P x y) = if h : P then f (x h) else f (y h)
-- Init.Data.Rat.Lemmas
Rat.num_divInt_den : ∀ (a : ℚ), Rat.divInt a.num ↑a.den = a
-- Mathlib.Data.Num.Lemmas
PosNum.cast_one : ∀ {α : Type u_1} [inst : One α] [inst_1 : Add α], ↑1 = 1
-- Mathlib.Order.Heyting.Basic
hnot_top : ∀ {α : Type u_2} [inst : CoheytingAlgebra α], ￢⊤ = ⊥
-- Mathlib.Data.Matrix.Mul
Matrix.mul_one : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix m n α), M * 1 = M
-- Mathlib.Algebra.Category.Ring.Limits
CommSemiRingCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommSemiRingCat)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_eq_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Set α} (hf : (s ∩ Function.mulSupport f).Finite),
  ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ hf.toFinset, f i
-- Init.Data.Nat.Lcm
Nat.eq_zero_of_lcm_eq_zero : ∀ {m n : ℕ}, m.lcm n = 0 → m = 0 ∨ n = 0
-- Mathlib.Analysis.InnerProductSpace.PiL2
Module.Basis.coe_toOrthonormalBasis : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (v : Module.Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v),
  ⇑(v.toOrthonormalBasis hv) = ⇑v
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.ext : ∀ (M : Type u_4) [inst : MulOne M] {f g : Monoid.End M}, (∀ (x : M), f x = g x) → f = g
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.zero_on_compl : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  Set.EqOn (⇑f) 0 (↑K)ᶜ
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_unitIso_hom_app_right_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L))
  (X_1 : D),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).unitIso.hom.app X).right.app X_1 =
    CategoryTheory.CategoryStruct.id (X.right.obj X_1)
-- Mathlib.NumberTheory.Height.Basic
/-- Eta-expanded form of `Height.logHeight_one` -/
Height.fun_logHeight_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2},
  (Height.logHeight fun x => 1) = 0
-- Mathlib.Data.Set.NAry
Set.image2_inter_union_subset : ∀ {α : Type u_1} {β : Type u_3} {f : α → α → β} {s t : Set α},
  (∀ (a b : α), f a b = f b a) → Set.image2 f (s ∩ t) (s ∪ t) ⊆ Set.image2 f s t
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.restriction.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K K_1 : HomologicalComplex C c'),
  K = K_1 → ∀ (e e_1 : c.Embedding c') (e_e : e = e_1) [inst_2 : e.IsRelIff], K.restriction e = K_1.restriction e_1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Icc_add_Ico_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α),
  Set.Icc a b + Set.Ico c d ⊆ Set.Ico (a + c) (b + d)
-- Mathlib.Algebra.Regular.SMul
IsSMulRegular.mul : ∀ {R : Type u_1} {M : Type u_3} {a b : R} [inst : SMul R M] [inst_1 : Mul R] [IsScalarTower R R M],
  IsSMulRegular M a → IsSMulRegular M b → IsSMulRegular M (a * b)
-- Mathlib.Topology.Order
TopologicalSpace.le_generateFrom_iff_subset_isOpen : ∀ {α : Type u} {g : Set (Set α)} {t : TopologicalSpace α}, t ≤ TopologicalSpace.generateFrom g ↔ g ⊆ {s | IsOpen s}
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.instDistribMulActionSubtypeAEEqFunMemAddSubgroupLp : {M : Type u_1} →
  {α : Type u_3} →
    {E : Type u_4} →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {μ : MeasureTheory.Measure α} →
            {p : ENNReal} →
              [inst_2 : Monoid M] →
                [inst_3 : MulAction M α] →
                  [MeasureTheory.SMulInvariantMeasure M α μ] →
                    [MeasurableConstSMul M α] → DistribMulAction Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
-- Init.Data.Fin.Lemmas
/-- `castSucc i` is positive when `i` is positive  -/
Fin.castSucc_pos : ∀ {n : ℕ} [inst : NeZero n] {i : Fin n}, 0 < i → 0 < i.castSucc
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.least : {α : Type u_1} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : Std.PRange.Least? α] → [Std.PRange.LawfulUpwardEnumerableLeast? α] → [hn : Nonempty α] → α
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] (L : StrongDual ℝ E),
  ProbabilityTheory.HasGaussianLaw X P →
    MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) L =
      Complex.exp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * Complex.I - ↑(ProbabilityTheory.variance (⇑L ∘ X) P) / 2)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If a continuous multilinear map is constructed from a multilinear map via the constructor
`mkContinuous`, then its norm is bounded by the bound given to the constructor if it is
nonnegative.  -/
MultilinearMap.mkContinuous_norm_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] (f : MultilinearMap 𝕜 E G)
  {C : ℝ}, 0 ≤ C → ∀ (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖), ‖f.mkContinuous C H‖ ≤ C
-- Mathlib.Tactic.Linarith.Frontend
/-- `applyContrLemma` inspects the target to see if it can be moved to a hypothesis by negation.
For example, a goal `⊢ a ≤ b` can become `b < a ⊢ false`.
If this is the case, it applies the appropriate lemma and introduces the new hypothesis.
It returns the type of the terms in the comparison (e.g. the type of `a` and `b` above) and the
newly introduced local constant.
Otherwise returns `none`.
 -/
Mathlib.Tactic.Linarith.applyContrLemma : Lean.MVarId → Lean.MetaM (Option (Lean.Expr × Lean.Expr) × Lean.MVarId)
-- Mathlib.Algebra.Algebra.Spectrum.Pi
Pi.spectrum_eq : ∀ {ι : Type u_1} {R : Type u_4} {κ : ι → Type u_5} [inst : CommSemiring R] [inst_1 : (i : ι) → Ring (κ i)]
  [inst_2 : (i : ι) → Algebra R (κ i)] (a : (i : ι) → κ i), spectrum R a = ⋃ i, spectrum R (a i)
-- Mathlib.Topology.Homotopy.Path
/-- The reverse of a path homotopy class. This is `Path.symm` descended to the quotient.  -/
Path.Homotopic.Quotient.symm : {X : Type u} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → Path.Homotopic.Quotient x₀ x₁ → Path.Homotopic.Quotient x₁ x₀
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.arrowCongr'_refl : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁]
  [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁] [inst_4 : NonUnitalNonAssocSemiring A₂]
  [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂],
  (StarAlgEquiv.refl R A₁).arrowCongr' (StarAlgEquiv.refl R A₂) = Equiv.refl (A₁ →⋆ₙₐ[R] A₂)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerMap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t)
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C],
  CategoryTheory.Limits.FormalCoproduct.powerMap (CategoryTheory.CategoryStruct.id U) α =
    CategoryTheory.CategoryStruct.id (U.power α)
-- Init.BinderPredicates
/-- Declare `∀ x ⊃ y, ...` as syntax for `∀ x, x ⊃ y → ...` and `∃ x ⊃ y, ...` as syntax for
`∃ x, x ⊃ y ∧ ...`  -/
Lean.«binderPred⊃_» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.instMonoidalCategory : {R : Type u} → [inst : CommRing R] → [Invertible 2] → CategoryTheory.MonoidalCategory (QuadraticModuleCat R)
-- Mathlib.GroupTheory.Goursat
Subgroup.mem_goursatSnd : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {I : Subgroup (G × H)} {h : H},
  h ∈ I.goursatSnd ↔ (1, h) ∈ I
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X)
  (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0) →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) {Z : D}
      (h :
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) ⟶
          Z),
      CategoryTheory.CategoryStruct.comp ((F.rightDerived n).map f)
          (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedObj F n).hom h) =
        CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).hom
          (CategoryTheory.CategoryStruct.comp
            ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
              ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ))
            h)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1IsoOfIsTrivial.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  groupCohomology.H1IsoOfIsTrivial A = groupCohomology.H1IsoOfIsTrivial A
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of the forward direction of `MonoidAlgebra.coeff_inj`. -/
MonoidAlgebra.ext : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x y : MonoidAlgebra R M}, x.coeff = y.coeff → x = y
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.opNorm_prod : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G)
  (g : ContinuousMultilinearMap 𝕜 E G'), ‖f.prod g‖ = max ‖f‖ ‖g‖
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a fallback : α} {v : β k},
      (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ k ∉ m then k else m.getKeyD a fallback
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.singleZeroAlgHom.eq_1 : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M],
  AddMonoidAlgebra.singleZeroAlgHom = { toRingHom := AddMonoidAlgebra.singleZeroRingHom, commutes' := ⋯ }
-- Init.Data.Range.Polymorphic.PRange
Std.Rci.mk.inj : ∀ {α : Type u} {lower lower_1 : α}, lower...* = lower_1...* → lower = lower_1
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.isUniformEmbedding : ∀ {R : Type u_1} [inst : CommSemiring R] {E₁ : Type u_5} {E₂ : Type u_6} [inst_1 : UniformSpace E₁]
  [inst_2 : UniformSpace E₂] [inst_3 : Ring E₁] [IsUniformAddGroup E₁] [inst_5 : Algebra R E₁] [inst_6 : Ring E₂]
  [IsUniformAddGroup E₂] [inst_8 : Algebra R E₂] (e : E₁ ≃A[R] E₂), IsUniformEmbedding ⇑e
-- Mathlib.Order.SuccPred.Tree
RootedTree.mk.injEq : ∀ (α : Type u_2) [semilatticeInf : SemilatticeInf α] [orderBot : OrderBot α] [predOrder : PredOrder α]
  [isPredArchimedean : IsPredArchimedean α] (α_1 : Type u_2) (semilatticeInf_1 : SemilatticeInf α_1)
  (orderBot_1 : OrderBot α_1) (predOrder_1 : PredOrder α_1) (isPredArchimedean_1 : IsPredArchimedean α_1),
  ({ α := α, semilatticeInf := semilatticeInf, orderBot := orderBot, predOrder := predOrder,
        isPredArchimedean := isPredArchimedean } =
      { α := α_1, semilatticeInf := semilatticeInf_1, orderBot := orderBot_1, predOrder := predOrder_1,
        isPredArchimedean := isPredArchimedean_1 }) =
    (α = α_1 ∧ semilatticeInf ≍ semilatticeInf_1 ∧ orderBot ≍ orderBot_1 ∧ predOrder ≍ predOrder_1)
-- Lean.Environment
Lean.Kernel.Exception.unknownConstant.inj : ∀ {env : Lean.Kernel.Environment} {name : Lean.Name} {env_1 : Lean.Kernel.Environment} {name_1 : Lean.Name},
  Lean.Kernel.Exception.unknownConstant env name = Lean.Kernel.Exception.unknownConstant env_1 name_1 →
    env = env_1 ∧ name = name_1
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
/-- For the `I`-adic topology, the neighborhoods of zero has basis given by the powers of `I`.  -/
Ideal.hasBasis_nhds_zero_adic : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), (nhds 0).HasBasis (fun _n => True) fun n => ↑(I ^ n)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.unitOfList_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α},
  (Std.DTreeMap.Raw.Const.unitOfList l cmp).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inrNonUnitalAlgHom_toFun : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A] (a : A),
  (Unitization.inrNonUnitalAlgHom R A) a = ↑a
-- Mathlib.Data.Int.AbsoluteValue
AbsoluteValue.map_units_intCast : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : CommRing S] [inst_2 : LinearOrder S] [IsStrictOrderedRing S]
  [Nontrivial R] (abv : AbsoluteValue R S) (x : ℤˣ), abv ↑↑x = 1
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget₂Grp_obj_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C),
  ((CategoryTheory.CommGrp.forget₂Grp C).obj A).X = A.X
-- Init.Data.List.Monadic
List.foldrM_map : ∀ {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} [inst : Monad m] [LawfulMonad m]
  {f : β₁ → β₂} {g : β₂ → α → m α} {l : List β₁} {init : α},
  List.foldrM g init (List.map f l) = List.foldrM (fun x y => g (f x) y) init l
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  {U V : CategoryTheory.Functor X Y} (α : U ⟶ V) (x : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y)
  (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map α).app x).fst.app X_1 =
    x.fst.map (α.app X_1)
-- Mathlib.Computability.Primrec.Basic
Primrec.cond : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Bool} {f g : α → σ},
  Primrec c → Primrec f → Primrec g → Primrec fun a => bif c a then f a else g a
-- Mathlib.Algebra.AddConstMap.Basic
/-- A bundled map `f : G → H` such that `f (x + a) = f x + b` for all `x`,
denoted as `f : G →+c[a, b] H`.

One can think about `f` as a lift to `G` of a map between two `AddCircle`s.  -/
AddConstMap.«term_→+c[_,_]_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- **Alias** of `Int.natAbs_sum_le`. -/
nat_abs_sum_le : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → ℤ), (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs
-- Mathlib.Algebra.Ring.Subsemiring.Order
/-- A subsemiring of a strict ordered semiring is a strict ordered semiring.  -/
Subsemiring.toIsStrictOrderedRing : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] (s : Subsemiring R),
  IsStrictOrderedRing ↥s
-- Mathlib.MeasureTheory.Measure.PreVariation
/-- A set function is σ-subadditive on measurable sets if the value assigned to the union of a
countable disjoint family of measurable sets is bounded above by the sum of values on the family.  -/
MeasureTheory.IsSigmaSubadditiveSetFun : {X : Type u_1} → [MeasurableSpace X] → (Set X → ENNReal) → Prop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {fallback : α}, t.getKeyD t.maxKey! fallback = t.maxKey!
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.F.sizeOf_spec : ∀ {B : Type v} [inst : SizeOf B] (a : B), sizeOf (CartanMatrix.Generators.F a) = 1 + sizeOf a
-- Mathlib.Data.List.Fold
/-- **Second Bird–Wadler duality theorem**.  -/
List.foldr_flip_eq_foldl : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {b : β} [RightCommutative v],
  List.foldr (flip v) b l = List.foldl v b l
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
IterateAddAct.instMeasurableSpace.eq_1 : ∀ {α : Type u_1} {f : α → α}, IterateAddAct.instMeasurableSpace = ⊤
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.add_extMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (f g : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
  (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0)
  (hg : CategoryTheory.CategoryStruct.comp g (R.cocomplex.d n m) = 0),
  R.extMk f m hm hf + R.extMk g m hm hg = R.extMk (f + g) m hm ⋯
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- A family of `PowerSeries` in the form `1 + f i` is multipliable if the order of `f i` tends to
infinity.  -/
PowerSeries.WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {ι : Type u_2} [inst_2 : LinearOrder ι]
  [LocallyFiniteOrderBot ι] {f : ι → PowerSeries R},
  Filter.Tendsto (fun i => (f i).order) Filter.atTop (nhds ⊤) → Multipliable fun x => 1 + f x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldr.eq_2 : ∀ {α : Type u_1} {σ : Sort u_2} (f : α → σ → σ) (x : σ) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α),
  RBTree.RBNode.foldr f (RBTree.RBNode.node c l v r) x = RBTree.RBNode.foldr f l (f v (RBTree.RBNode.foldr f r x))
-- Batteries.Data.Random.MersenneTwister
/-- Apply the twisting transformation to the given state.  -/
Batteries.Random.MersenneTwister.State.twist : {cfg : Batteries.Random.MersenneTwister.Config} →
  Batteries.Random.MersenneTwister.State cfg → Batteries.Random.MersenneTwister.State cfg
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F] [IsPrincipalIdealRing O],
  v.Integers O → ¬DenselyOrdered ↑(Set.range ⇑v)
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBMap.alter.adapt.match_3.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option (α × β) → Sort u_3) (k' : α) (v' : β) (h_1 : Unit → motive none)
  (h_2 : (k' : α) → (v' : β) → motive (some (k', v'))),
  (match some (k', v') with
    | none => h_1 ()
    | some (k', v') => h_2 k' v') =
    h_2 k' v'
-- Mathlib.RingTheory.Localization.Module
LinearMap.extendScalarsOfIsLocalizationEquiv_apply : ∀ {R : Type u_3} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (f : M →ₗ[R] N),
  (LinearMap.extendScalarsOfIsLocalizationEquiv S A) f = LinearMap.extendScalarsOfIsLocalization S A f
-- Std.Do.Triple.SpecLemmas
throwThe.eq_1 : ∀ (ε : Type u) {m : Type v → Type w} [inst : MonadExceptOf ε m] {α : Type v} (e : ε),
  throwThe ε e = MonadExceptOf.throw e
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.fundamentalGroupToMulOpposite_surjective : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x}))
  [PathConnectedSpace E], Function.Surjective ⇑(hp.fundamentalGroupToMulOpposite e)
-- Init.Grind.Ring.CommSolver
Eq.ndrec_symm.congr_simp : ∀ {α : Sort u2} {a : α} {motive : α → Sort u1} (m m_1 : motive a),
  m = m_1 → ∀ {b : α} (h : b = a), Eq.ndrec_symm m h = Eq.ndrec_symm m_1 h
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_iSup : ∀ {ι : Sort u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : ι → Subalgebra R Aᵐᵒᵖ), (iSup S).unop = ⨆ i, (S i).unop
-- Batteries.Data.Fin.Coding
Fin.decodeProd_encodeProd : ∀ {m n : ℕ} (x : Fin m × Fin n), Fin.decodeProd (Fin.encodeProd x) = x
-- Mathlib.Data.List.MinMax
List.max_le_of_forall_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderBot α] (l : List α) (a : α),
  (∀ x ∈ l, x ≤ a) → List.foldr max ⊥ l ≤ a
-- Mathlib.Order.BoundedOrder.Basic
Prod.snd_bot : ∀ (α : Type u) (β : Type v) [inst : Bot α] [inst_1 : Bot β], ⊥.2 = ⊥
-- Init.Data.Array.Lemmas
Array.elem_push_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α}, Array.elem a (xs.push a) = true
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `a ^ (0 : ℕ)`.
This extension is run in addition to the general `a ^ b` extension (they are overlapping).  -/
Mathlib.Meta.Positivity.evalPowZeroNat : Mathlib.Meta.Positivity.PositivityExt