mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `limit F` is functorial in `F`, when `C` has all limits of shape `J`.  -/
CategoryTheory.Limits.lim : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [CategoryTheory.Limits.HasLimitsOfShape J C] → CategoryTheory.Functor (CategoryTheory.Functor J C) C
-- Lean.Meta.Tactic.Intro
_private.Lean.Meta.Tactic.Intro.0.Lean.Meta.mkAuxNameImp.mkAuxNameWithoutGivenName : Bool → Bool → Lean.LocalContext → Lean.Name → List Lean.Name → Lean.MetaM (Lean.Name × List Lean.Name)
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The underlying object of the tensor product of two bimodules.  -/
Bimod.TensorBimod.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.Limits.HasCoequalizers C] → {R S T : CategoryTheory.Mon C} → Bimod R S → Bimod S T → C
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialSimplicialEquiv_unitIso_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor SimplexCategory C)ᵒᵖ),
  (CategoryTheory.cosimplicialSimplicialEquiv C).unitIso.inv.app X = (Opposite.unop X).opUnopIso.inv.op
-- Mathlib.Algebra.Ring.Subsemiring.Order
Subsemiring.coe_nonneg : ∀ (R : Type u_1) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R],
  ↑(Subsemiring.nonneg R) = (AddSubmonoid.nonneg R).carrier
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- The identity isomorphism as a continuous `R`-algebra equivalence.  -/
ContinuousAlgEquiv.refl : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : TopologicalSpace A] → [inst_3 : Algebra R A] → A ≃A[R] A
-- Mathlib.Algebra.Free
/-- Recursor for `FreeMagma` using `x * y` instead of `FreeMagma.mul x y`.  -/
FreeMagma.recOnMul : {α : Type u} →
  {C : FreeMagma α → Sort l} →
    (x : FreeMagma α) → ((x : α) → C (FreeMagma.of x)) → ((x y : FreeMagma α) → C x → C y → C (x * y)) → C x
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_mul_const_field : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {v : 𝕜 → 𝕜'} (u : 𝕜'), derivWithin (fun y => v y * u) s x = derivWithin v s x * u
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineMap.lineMap_vsub : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (p₁ p₂ p₃ : P₁) (c : k),
  (AffineMap.lineMap p₁ p₂) c -ᵥ p₃ = (AffineMap.lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)) c
-- Mathlib.Algebra.Notation
/-- A notation class for the *positive part* function: `a⁺`.  -/
PosPart : Type u_1 → Type u_1
-- Mathlib.NumberTheory.NumberField.EquivReindex
/-- An equivalence between the set of embeddings of `K` into `ℂ` and the
index set of the chosen basis of the ring of integers of `K`.  -/
NumberField.equivReindex : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] → (K →+* ℂ) ≃ Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)
-- Mathlib.Tactic.FBinop
FBinopElab.instToExprSRec.toExpr : FBinopElab.SRec → Lean.Expr
-- Mathlib.RingTheory.Regular.IsSMulRegular
IsSMulRegular.submodule : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Submodule R M)
  (r : R), IsSMulRegular M r → IsSMulRegular (↥N) r
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.d₁₂.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G),
  groupCohomology.d₁₂ A =
    ModuleCat.ofHom { toFun := fun f g => (A.ρ g.1) (f g.2) - f (g.1 * g.2) + f g.1, map_add' := ⋯, map_smul' := ⋯ }
-- Init.Data.SInt.Basic
Int16.instNeg : Neg Int16
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
MeasureTheory.analyticSet_empty : ∀ {α : Type u_1} [inst : TopologicalSpace α], MeasureTheory.AnalyticSet ∅
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_zero : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂], ↑0 = 0
-- Mathlib.Tactic.Linter.AuxLemma
/-- The `auxLemma` linter emits a warning on any explicit reference to an auto-generated
auxiliary declaration (such as `_proof_1`, `match_1`, or `_sizeOf_1`).

These names are internal to the Lean elaborator and are not stable across refactors.  -/
Mathlib.Linter.AuxLemma.linter.auxLemma : Lean.Option Bool
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.prodUnique_symm_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] [inst_5 : Unique M₂] (a : M),
  LinearEquiv.prodUnique.symm a = (a, default)
-- Mathlib.GroupTheory.Congruence.Hom
Con.mkMulHom_apply : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) (a : M), c.mkMulHom a = ↑a
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.coe_of : ∀ (R : Type u) [inst : CommRing R] (X : Type v) [inst_1 : CommRing X] [inst_2 : Bialgebra R X],
  ↑(CommBialgCat.of R X) = X
-- Std.Internal.Do.Order.Basic
Lean.Order.iInf_prop_eq_forall : ∀ {ι : Type u} (f : ι → Prop), Lean.Order.iInf f = ∀ (i : ι), f i
-- Mathlib.Algebra.Lie.Basis.Base
/-- The elements `LieAlgebra.Basis.baseSupp` as roots in the sense of `LieSubalgebra.root`.  -/
LieAlgebra.Basis.baseSupp' : {ι : Type u_1} →
  {K : Type u_2} →
    {L : Type u_3} →
      [inst : Fintype ι] →
        [inst_1 : Field K] →
          [inst_2 : CharZero K] →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra K L] →
                [inst_5 : FiniteDimensional K L] →
                  {H : LieSubalgebra K L} → (b : LieAlgebra.Basis ι H) → ι → ↥LieSubalgebra.root
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPullback.of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C},
  sq₁.IsPullback → ∀ (e : sq₁ ≅ sq₂), sq₂.IsPullback
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_sub_right_right_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime x (z * x - y) ↔ IsRelPrime x y
-- Mathlib.FieldTheory.NormalizedTrace
_private.Mathlib.FieldTheory.NormalizedTrace.0.Algebra.normalizedTraceAux_map : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] {E : Type u_3}
  [inst_3 : Field E] [inst_4 : Algebra F E] (f : E →ₐ[F] K) (a : E),
  Algebra.normalizedTraceAux✝ F K (f a) = Algebra.normalizedTraceAux✝ F E a
-- Mathlib.RingTheory.Trace.Basic
Algebra.trace_surjective : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  [Algebra.IsSeparable K L], Function.Surjective ⇑(Algebra.trace K L)
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements.  -/
unop_map_list_prod : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] {F : Type u_8} [inst_2 : FunLike F M Nᵐᵒᵖ]
  [MonoidHomClass F M Nᵐᵒᵖ] (f : F) (l : List M),
  MulOpposite.unop (f l.prod) = (List.map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
-- Mathlib.Algebra.Order.Sub.Basic
AddLECancellable.lt_tsub_iff_left : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable c → (a < b - c ↔ c + a < b)
-- Mathlib.GroupTheory.Commutator.Basic
mem_addCommutatorSet_iff : ∀ {G : Type u_1} [inst : AddGroup G] {g : G}, g ∈ addCommutatorSet G ↔ ∃ g₁ g₂, ⁅g₁, g₂⁆ = g
-- Aesop.Stats.Basic
Aesop.ForwardInstantiationStats.mk.injEq : ∀ («matches» hyps matches_1 hyps_1 : ℕ),
  ({ «matches» := «matches», hyps := hyps } = { «matches» := matches_1, hyps := hyps_1 }) =
    («matches» = matches_1 ∧ hyps = hyps_1)
-- Mathlib.GroupTheory.Commutator.Basic
instCharacteristicAddCommutator : ∀ (G : Type u_1) [inst : AddGroup G], (addCommutator G).Characteristic
-- Mathlib.Data.Sym.Sym2
/-- A dependent recursion principle for `Sym2` that uses heterogeneous equality.  -/
Sym2.hrec : {α : Type u_1} →
  {motive : Sym2 α → Sort u_4} →
    (f : (a b : α) → motive s(a, b)) → (∀ (a b : α), f a b ≍ f b a) → (z : Sym2 α) → motive z
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.mul_right_eq_one : ∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Semiring R] [inst_2 : Module Rᵐᵒᵖ M] [inst_3 : Module R M]
  (x : TrivSqZeroExt R M) (r : R),
  x.fst * r = 1 → x * (TrivSqZeroExt.inl r + TrivSqZeroExt.inr (-(r • MulOpposite.op r • x.snd))) = 1
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.tendsto_log_nat_add_one_sub_log : Filter.Tendsto (fun k => Real.log (↑k + 1) - Real.log ↑k) Filter.atTop (nhds 0)
-- Lean.Data.Json.FromToJson.Basic
Lean.List.toJson : {α : Type u_1} → [Lean.ToJson α] → List α → Lean.Json
-- Mathlib.Order.Cover
CovBy.Ioo_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ⋖ b → ∀ (c : α), Set.Ioo a c = Set.Ico b c
-- Mathlib.NumberTheory.ModularForms.DedekindEta
_private.Mathlib.NumberTheory.ModularForms.DedekindEta.0.termℍₒ : Lean.ParserDescr
-- Lean.Compiler.LCNF.Basic
/-- The code we are acting on is still pure, things like reordering up to value dependencies are
acceptable.
 -/
Lean.Compiler.LCNF.Purity.pure : Lean.Compiler.LCNF.Purity
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- If the vector passed to `secondInter` is given by a subtraction involving the point in
`secondInter`, the result lies in the span of the two points.  -/
EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p₁ p₂ : P),
  s.secondInter p₁ (p₂ -ᵥ p₁) ∈ line[ℝ, p₁, p₂]
-- Init.Data.Array.Range
Array.range_eq_empty_iff : ∀ {n : ℕ}, Array.range n = #[] ↔ n = 0
-- Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.TerminationMeasure.ref : Lean.Elab.TerminationMeasure → Lean.Syntax
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.options : Aesop.Frontend.TacticConfig → Aesop.Options
-- Mathlib.Algebra.Lie.Extension
/-- The extension of Lie algebras defined by a 2-cocycle.  -/
LieAlgebra.Extension.ofTwoCocycle : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : LieRing M] →
              [inst_4 : LieAlgebra R M] →
                [IsLieAbelian M] →
                  [inst_6 : LieRingModule L M] →
                    [inst_7 : LieModule R L M] → ↥(LieModule.Cohomology.twoCocycle R L M) → LieAlgebra.Extension R M L
-- Mathlib.Logic.Hydra
/-- The relation that specifies valid moves in our hydra game. `CutExpand r s' s`
means that `s'` is obtained by removing one head `a ∈ s` and adding back an arbitrary
multiset `t` of heads such that all `a' ∈ t` satisfy `r a' a`.

This is most directly translated into `s' = s.erase a + t`, but `Multiset.erase` requires
`DecidableEq α`, so we use the equivalent condition `s' + {a} = s + t` instead, which
is also easier to verify for explicit multisets `s'`, `s` and `t`.

We also don't include the condition `a ∈ s` because `s' + {a} = s + t` already
guarantees `a ∈ s + t`, and if `r` is irreflexive then `a ∉ t`, which is the
case when `r` is well-founded, the case we are primarily interested in.

The lemma `Relation.cutExpand_iff` below converts between this convenient definition
and the direct translation when `r` is irreflexive.  -/
Relation.CutExpand : {α : Type u_1} → (α → α → Prop) → Multiset α → Multiset α → Prop
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- Morphisms in `SimplicialObject.Split C` are morphisms of simplicial objects that
are compatible with the splittings.  -/
CategoryTheory.SimplicialObject.Split.Hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.SimplicialObject.Split C → CategoryTheory.SimplicialObject.Split C → Type v_1
-- Mathlib.Tactic.Polynomial.Core
Mathlib.Tactic.Polynomial.PolynomialExt.mk.inj : ∀ {infer infer_1 : Lean.Expr → Lean.MetaM Lean.Expr}, { infer := infer } = { infer := infer_1 } → infer = infer_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insert k v).contains k = true
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_subset_Ioo_union_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a ⊆ Set.Ioo a b ∪ Set.Ici b
-- Mathlib.Topology.DiscreteSubset
/-- The filter of sets with no accumulation points inside a set `S : Set X`, implemented
as the supremum over all punctured neighborhoods within `S`.  -/
Filter.codiscreteWithin : {X : Type u_1} → [TopologicalSpace X] → Set X → Filter X
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instZero : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Zero (ModularForm Γ k)
-- Mathlib.Topology.Order.OrderClosed
Ioo_subset_closure_interior : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {a b : α},
  Set.Ioo a b ⊆ closure (interior (Set.Ioo a b))
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.add_eq_map₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Add β] (f g : MeasureTheory.SimpleFunc α β),
  f + g = MeasureTheory.SimpleFunc.map (fun p => p.1 + p.2) (f.pair g)
-- Mathlib.AlgebraicGeometry.Stalk
/-- For a local ring `(R, 𝔪)`,
this is the isomorphism between the stalk of `Spec R` at `𝔪` and `R`.  -/
AlgebraicGeometry.stalkClosedPointIso : (R : CommRingCat) → [inst : IsLocalRing ↑R] → (AlgebraicGeometry.Spec R).presheaf.stalk (IsLocalRing.closedPoint ↑R) ≅ R
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.primeSpectrumOrderIsoSpec_apply : ∀ (R : Type u) [inst : CommRing R] (x : PrimeSpectrum R),
  (AlgebraicGeometry.primeSpectrumOrderIsoSpec R) x = OrderDual.toDual x
-- Mathlib.LinearAlgebra.Projection
LinearMap.equivProdOfSurjectiveOfIsCompl_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {G : Type u_4} [inst_5 : AddCommGroup G] [inst_6 : Module R G]
  {f : E →ₗ[R] F} {g : E →ₗ[R] G} (hf : f.range = ⊤) (hg : g.range = ⊤) (hfg : IsCompl f.ker g.ker) (x : E),
  (f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) x = (f x, g x)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_intCast_mul_add : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIcoDiv hp a (↑m * p + b) = m + toIcoDiv hp a b
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.mk.inj : ∀ {stxTrav : Lean.Syntax.Traverser} {contPrec : Option ℕ} {contCat : Lean.Name} {minPrec trailPrec : Option ℕ}
  {trailCat : Lean.Name} {visitedToken : Bool} {stxTrav_1 : Lean.Syntax.Traverser} {contPrec_1 : Option ℕ}
  {contCat_1 : Lean.Name} {minPrec_1 trailPrec_1 : Option ℕ} {trailCat_1 : Lean.Name} {visitedToken_1 : Bool},
  { stxTrav := stxTrav, contPrec := contPrec, contCat := contCat, minPrec := minPrec, trailPrec := trailPrec,
        trailCat := trailCat, visitedToken := visitedToken } =
      { stxTrav := stxTrav_1, contPrec := contPrec_1, contCat := contCat_1, minPrec := minPrec_1,
        trailPrec := trailPrec_1, trailCat := trailCat_1, visitedToken := visitedToken_1 } →
    stxTrav = stxTrav_1 ∧
      contPrec = contPrec_1 ∧
        contCat = contCat_1 ∧
          minPrec = minPrec_1 ∧ trailPrec = trailPrec_1 ∧ trailCat = trailCat_1 ∧ visitedToken = visitedToken_1
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof : Type
-- Mathlib.LinearAlgebra.Matrix.DotProduct
dotProduct_eq : ∀ {n : Type u_2} {R : Type u_4} [inst : Semiring R] [inst_1 : Fintype n] (v w : n → R),
  (∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u) → v = w
-- Mathlib.Order.Lattice
MonotoneOn.of_map_inf : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β],
  (∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊓ f y) → MonotoneOn f s
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instPartialOrder : {G : Type u} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → PartialOrder (OpenNormalAddSubgroup G)
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.commSq : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (self : AlgebraicGeometry.ValuativeCommSq f),
  CategoryTheory.CommSq self.i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap self.R self.K))) f self.i₂
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_Ioi : ∀ {n : ℕ} (m : ℕ) [inst : NeZero m] (i : Fin n), Fin.castAdd m '' Set.Ioi i = Set.Ioo (Fin.castAdd m i) (Fin.natAdd n 0)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_hasFDerivAt_iff : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E},
  HasFDerivAt (⇑iso ∘ f) (↑↑iso ∘SL f') x ↔ HasFDerivAt f f' x
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuousWithinAt_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, UpperHemicontinuousWithinAt (fun x => {f x}) s x ↔ ContinuousWithinAt f s x
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.ofFn_zero' : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] (v : Fin 0 → R), (Polynomial.ofFn 0) v = 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.sum_dite_eq'`.  -/
Fintype.sum_dite_eq' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι)
  (f : (j : ι) → j = i → M), (∑ j, if h : j = i then f j h else 0) = f i ⋯
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_finsetSum_comm : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {s : Finset β}
  (f : α →₀ M) (h : α → M → β → N), (f.sum fun a m => ∑ b ∈ s, h a m b) = ∑ b ∈ s, f.sum fun a m => h a m b
-- Lean.Util.HasConstCache
Lean.HasConstCache.containsUnsafe : {declNames : Array Lean.Name} → Lean.Expr → StateM (Lean.HasConstCache declNames) Bool
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.prod : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] {B₁ : Set (Set α)}
  {B₂ : Set (Set β)},
  TopologicalSpace.IsTopologicalBasis B₁ →
    TopologicalSpace.IsTopologicalBasis B₂ →
      TopologicalSpace.IsTopologicalBasis (Set.image2 (fun x1 x2 => x1 ×ˢ x2) B₁ B₂)
-- Mathlib.Probability.Decision.Risk.Basic
/-- For a bounded loss, the Bayes risk with respect to a prior is bounded by a constant.  -/
ProbabilityTheory.bayesRisk_le_mul : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [Nonempty 𝓨] (P : ProbabilityTheory.Kernel Θ 𝓧)
  [ProbabilityTheory.IsMarkovKernel P] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure π]
  {C : NNReal}, (∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C) → ProbabilityTheory.bayesRisk ℓ P π ≤ ↑C
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.principals_obj : ∀ (X : Type v) [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] (x : X),
  (Alexandrov.principals X).obj x = Opposite.op (Alexandrov.principalOpen x)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_union : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G]
  {B : E →L[ℝ] F →L[ℝ] G},
  Disjoint s t →
    MeasurableSet s →
      MeasurableSet t →
        μ.IntegrableOn f s →
          μ.IntegrableOn f t →
            ∫ᵛ (x : X) in s ∪ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X) in t, f x ∂[B; μ]
-- Mathlib.Tactic.ITauto
/-- * `ak = .and`: `(p₁: A) (p₂: B) ⊢ A ∧ B`
* `ak = .iff`: `(p₁: A → B) (p₁: B → A) ⊢ A ↔ B`
* `ak = .eq`: `(p₁: A → B) (p₁: B → A) ⊢ A = B`
 -/
Mathlib.Tactic.ITauto.Proof.andIntro : Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.convexCombPair_convexCombPair_assoc_left : ∀ {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) {s' t' : R} (hs' : 0 ≤ s')
  (ht' : 0 ≤ t') (h' : s' + t' = 1) {s'' t'' : R} (hs'' : 0 ≤ s'') (ht'' : 0 ≤ t'') (h'' : s'' + t'' = 1),
  t * s'' = s * t' * t'' →
    ∀ (m₁ m₂ m₃ : M),
      Convexity.convexCombPair s t hs ht h (Convexity.convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
        Convexity.convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (Convexity.convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
-- Mathlib.Order.Antichain
/-- **Alias** of `isAntichain_insert_of_symm`. -/
isAntichain_insert_of_symmetric : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} [Std.Symm r],
  IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_basis : ∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
  [inst_3 : CommRing A] [inst_4 : Module A M] (b b' : Module.Basis ι A M),
  LinearMap.det ↑(b'.equiv b (Equiv.refl ι)) = b'.det ⇑b
-- Init.System.IO
/-- Terminates the current process with the provided exit code. `0` indicates success, all other values
indicate failure.

Calling this function is equivalent to calling
[`std::_Exit`](https://en.cppreference.com/w/cpp/utility/program/_Exit.html).
 -/
IO.Process.forceExit : {α : Type} → UInt8 → IO α
-- Mathlib.Analysis.Calculus.Deriv.Inverse
/-- If a function is equal to a constant at a set of points that accumulates to `x` in `s`,
then its derivative within `s` at `x` equals zero,
either because it has derivative zero or because it isn't differentiable at this point.  -/
derivWithin_zero_of_frequently_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} {c : F},
  (∃ᶠ (y : 𝕜) in nhdsWithin x (s \ {x}), f y = c) → derivWithin f s x = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalRing : {R : Type u_1} → {M : Type u_4} → [inst : Ring R] → [Semigroup M] → NonUnitalRing (MonoidAlgebra R M)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.oneToZero_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X Y : CategoryTheory.PreOneHypercover S} (f : X ⟶ Y),
  CategoryTheory.PreOneHypercover.oneToZero.map f = f.toHom
-- Mathlib.Analysis.Complex.Norm
Complex.abs_im_lt_norm : ∀ {z : ℂ}, |z.im| < ‖z‖ ↔ z.re ≠ 0
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.zero_of : ∀ {A : Type u_1} [inst : AddMonoid A], 0 = 0
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.EMem.eq_1 : ∀ {α : Type u_1} (x : α) (t : RBTree.RBNode α), RBTree.RBNode.EMem x t = RBTree.RBNode.Any (fun x_1 => x = x_1) t