mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.RepresentableBy.isRepresentedBy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  (R : F.RepresentableBy X), F.IsRepresentedBy (R.homEquiv (CategoryTheory.CategoryStruct.id X))
-- Init.Data.Queue
Std.Queue.mk : {α : Type u} → List α → List α → Std.Queue α
-- Std.Async.Signal
Std.Async.Signal.sigio.sizeOf_spec : sizeOf Std.Async.Signal.sigio = 1
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The weights for the Monge point of an (n+2)-simplex, in terms of
`pointsWithCircumcenter`.  -/
Affine.Simplex.mongePointWeightsWithCircumcenter : (n : ℕ) → Affine.Simplex.PointsWithCircumcenterIndex (n + 2) → ℝ
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.allTR.loop.eq_2 : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (m : ℕ) (h : m.succ ≤ n),
  Nat.allTR.loop✝ n f m.succ h = (f (n - m.succ) ⋯ && Nat.allTR.loop✝ n f m ⋯)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.addAction.eq_1 : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] (p : SubAddAction R M),
  p.addAction = p.addAction'
-- Mathlib.Topology.CompactOpen
ContinuousMap.isClopen_setOfPred_mapsTo : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {K : Set X} {U : Set Y},
  IsCompact K → IsClopen U → IsClopen {f | Set.MapsTo (⇑f) K U}
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.closure_insert_zero : ∀ {M : Type u_1} [inst : AddZeroClass M] (s : Set M), AddSubmonoid.closure (insert 0 s) = AddSubmonoid.closure s
-- Mathlib.Logic.Basic
xor_false : Xor False = id
-- Mathlib.Util.AtLocation
Mathlib.Tactic.BehaviorIfUnchanged.silent.sizeOf_spec : sizeOf Mathlib.Tactic.BehaviorIfUnchanged.silent = 1
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Corecursor for `Cofix F`  -/
MvQPF.Cofix.corec'₁ : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] → {α : TypeVec.{u} n} → {β : Type u} → ({X : Type u} → (β → X) → F (α ::: X)) → β → MvQPF.Cofix F α
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAtFilter.comp_hasFDerivAtFilter_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E) {L' : Filter 𝕜'} {L'' : Filter E},
  HasDerivAtFilter h₂ h₂' (L' ×ˢ pure y) →
    HasFDerivAtFilter f f' (L'' ×ˢ pure x) →
      Filter.Tendsto f L'' L' → y = f x → HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') (L'' ×ˢ pure x)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A regular monomorphism in `C` induces a regular epimorphism in `Cᵒᵖ`.  -/
CategoryTheory.RegularMono.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f : X ⟶ Y} → CategoryTheory.RegularMono f → CategoryTheory.RegularEpi f.op
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- The square of the cosine of `π / 6` is `3 / 4` (this is sometimes more convenient than the
result for cosine itself).  -/
Real.sq_cos_pi_div_six : Real.cos (Real.pi / 6) ^ 2 = 3 / 4
-- Mathlib.Order.IsNormal
Order.IsNormal.preimage_Iic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLinearOrder β],
  Order.IsNormal f →
    ∀ {x : β},
      (f ⁻¹' Set.Iic x).Nonempty → BddAbove (f ⁻¹' Set.Iic x) → f ⁻¹' Set.Iic x = Set.Iic (sSup (f ⁻¹' Set.Iic x))
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.zero : {R : Type u} → {M : Type v} → [Zero R] → [Zero M] → Zero (TrivSqZeroExt R M)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- Constructor for morphisms in `LocallyRingedSpace`.  -/
AlgebraicGeometry.LocallyRingedSpace.homMk : {X Y : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X.toSheafedSpace ⟶ Y.toSheafedSpace) →
    autoParam
        (∀ (x : ↑X.toTopCat), IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.hom x)))
        AlgebraicGeometry.LocallyRingedSpace.homMk._auto_1 →
      (X ⟶ Y)
-- Mathlib.Analysis.Convex.StdSimplex
/-- `stdSimplex 𝕜 ι` is the convex hull of the canonical basis in `ι → 𝕜`.  -/
convexHull_basis_eq_stdSimplex : ∀ (R : Type u_1) (ι : Type u_2) [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι], (convexHull R) (Set.range fun i j => if i = j then 1 else 0) = stdSimplex R ι
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.AsSmall.equiv_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.AsSmall.equiv.unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Mathlib.Data.Set.Defs
Set.instUnion : {α : Type u} → Union (Set α)
-- Mathlib.Data.Finmap
Finmap.liftOn_toFinmap : ∀ {α : Type u} {β : α → Type v} {γ : Type u_1} (s : AList β) (f : AList β → γ)
  (H : ∀ (a b : AList β), a.entries.Perm b.entries → f a = f b), s.toFinmap.liftOn f H = f s
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
Ioo_smul_sphere_zero : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b r : ℝ},
  0 ≤ a → 0 < r → Set.Ioo a b • Metric.sphere 0 r = Metric.ball 0 (b * r) \ Metric.closedBall 0 (a * r)
-- Lean.Data.Options
Lean.Option.mk : {α : Type} → Lean.Name → α → Lean.Option α
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.dual_bijective_iff_bijective : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {A' : Type u_1} [inst_2 : AddCommGroup A']
  [inst_3 : Module R A] [inst_4 : Module R A'] {f : A →ₗ[R] A'},
  Function.Bijective ⇑(CharacterModule.dual f) ↔ Function.Bijective ⇑f
-- Mathlib.Data.Finset.Pairwise
instDecidablePairwiseCoeFinsetOfDecidableEqOfDecidableRel : {α : Type u_1} → [DecidableEq α] → {r : α → α → Prop} → [DecidableRel r] → {s : Finset α} → Decidable ((↑s).Pairwise r)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackCone_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g],
  (CategoryTheory.ChosenPullbacksAlong.pullbackCone f g).fst = CategoryTheory.ChosenPullbacksAlong.fst f g
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_toUInt32 : ∀ (n : UInt16), n.toUInt32.toUInt8 = n.toUInt8
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.idealFactorsEquivOfQuotEquiv_symm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J),
  (IsDedekindDomain.idealFactorsEquivOfQuotEquiv f).symm = IsDedekindDomain.idealFactorsEquivOfQuotEquiv f.symm
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentInv_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) (i : σ),
  (Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentInv✝ D) (b i) =
    1 ⊗ₜ[Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D]
      Algebra.Extension.Cotangent.mk (Algebra.Generators.PresentationOfFreeCotangent.Aux.kerGen✝ D i)
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.rightRelDecidable : {α : Type u_1} →
  [inst : Group α] → (s : Subgroup α) → [DecidablePred fun x => x ∈ s] → DecidableRel ⇑(QuotientGroup.rightRel s)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.mul_2 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x y y' : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F y y'),
  CommRingCat.Colimits.Relation.below x_1 → motive y y' x_1 → CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Topology.ShrinkingLemma
/-- **Shrinking lemma**. A point-finite open cover of a closed subset of a normal space can be
"shrunk" to a new open cover so that the closure of each new open set is contained in the
corresponding original open set.  -/
exists_subset_iUnion_closure_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} [NormalSpace X],
  IsClosed s →
    (∀ (i : ι), IsOpen (u i)) →
      (∀ x ∈ s, {i | x ∈ u i}.Finite) →
        s ⊆ ⋃ i, u i → ∃ v, s ⊆ Set.iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.instDecidableRelAdjDeleteIncidenceSet : {V : Type u_1} →
  [DecidableEq V] → {G : SimpleGraph V} → [DecidableRel G.Adj] → {x : V} → DecidableRel (G.deleteIncidenceSet x).Adj
-- Mathlib.Topology.Algebra.MulAction
/-- The additive action `(+ᵥ)` is continuous.  -/
ContinuousVAdd.continuous_vadd : ∀ {M : Type u_1} {X : Type u_2} {inst : VAdd M X} {inst_1 : TopologicalSpace M} {inst_2 : TopologicalSpace X}
  [self : ContinuousVAdd M X], Continuous fun p => p.1 +ᵥ p.2
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqCtorInfo.beq : Lean.IR.CtorInfo → Lean.IR.CtorInfo → Bool
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varFinset.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : L.Term α → Sort u_4) (l : ℕ) (_f : L.Functions l)
  (ts : Fin l → L.Term α) (h_1 : (i : α) → motive (FirstOrder.Language.var i))
  (h_2 : (l : ℕ) → (_f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func _f ts)),
  (match FirstOrder.Language.func _f ts with
    | FirstOrder.Language.var i => h_1 i
    | FirstOrder.Language.func _f ts => h_2 l _f ts) =
    h_2 l _f ts
-- Mathlib.Data.List.Destutter
List.destutter'_eq_self_iff : ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α),
  List.destutter' R a l = a :: l ↔ List.IsChain R (a :: l)
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_neg_right : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, c < 0 → (a * c ≤ b * c ↔ b ≤ a)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.forget_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget TopCat)
-- Init.Data.List.Lemmas
List.head?_tail : ∀ {α : Type u_1} {l : List α}, l.tail.head? = l[1]?
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_toUSize : ∀ (n : UInt64), n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the next continuants `⟨Aₙ, Bₙ⟩` using `nextNum` and `nextDen`, where `pred`
is `⟨Aₙ₋₁, Bₙ₋₁⟩`, `ppred` is `⟨Aₙ₋₂, Bₙ₋₂⟩`, `a` is `aₙ₋₁`, and `b` is `bₙ₋₁`.
 -/
GenContFract.nextConts : {K : Type u_2} → [DivisionRing K] → K → K → GenContFract.Pair K → GenContFract.Pair K → GenContFract.Pair K
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g)
  (p : ↥(AlgebraicGeometry.Spec T.tensor)), (CategoryTheory.Limits.pullback.fst f g) (T.SpecTensorTo p) = T.x
-- Mathlib.Order.DirSupClosed
DirSupClosed.union : ∀ {α : Type u_1} {s t : Set α} [inst : Preorder α], DirSupClosed s → DirSupClosed t → DirSupClosed (s ∪ t)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsInvInvariant.inv_eq_self : ∀ {G : Type u_1} {inst : MeasurableSpace G} {inst_1 : Inv G} {μ : MeasureTheory.Measure G} [self : μ.IsInvInvariant],
  μ.inv = μ
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.of_equiv : ∀ {R : Type u} {A : Type v} {B : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallyEtale R A] (e : A ≃ₐ[R] B), Algebra.FormallyEtale R B
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.neg : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M}, x ≡ y [SMOD U] → -x ≡ -y [SMOD U]
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.Forall₂.prod_le_prod' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M},
  List.Forall₂ (fun x1 x2 => x1 ≤ x2) l₁ l₂ → l₁.prod ≤ l₂.prod
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ]
  (g : EsakiaHom β γ) (f : EsakiaHom α β), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- A move left or right corresponds to `n` moves across the super-cell.  -/
Turing.TM1to1.move : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      ℕ → Turing.Dir → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `G` acts on `X` properly, the set `s +ᵥ t` is closed when `s : Set G` is *closed* and
`t : Set X` is *compact*. In particular, this applies when the action comes from an
`IsTopologicalAddTorsor`.

See also `IsClosed.vadd_left_of_isCompact` for a version with the assumptions on `s` and `t`
reversed.  -/
IsClosed.vadd_right_of_isCompact : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperVAdd G X] {s : Set G} {t : Set X}, IsClosed s → IsCompact t → IsClosed (s +ᵥ t)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet.eq_1 : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (s : ι → Set Ω)
  (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.iIndepSet s κ μ =
    ProbabilityTheory.Kernel.iIndep (fun i => MeasurableSpace.generateFrom {s i}) κ μ
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  {x y : CategoryTheory.Bicategory.Adjunction f g}, x.unit = y.unit → x.counit = y.counit → x = y
-- Mathlib.Algebra.FiniteSupport.Defs
Function.hasFiniteSupport_zero : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M], Function.HasFiniteSupport fun x => 0
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.isUnit_mk'_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (x : R) (y : ↥I.primeCompl),
  IsUnit (IsLocalization.mk' S x y) ↔ x ∈ I.primeCompl
-- Mathlib.Algebra.MvPolynomial.Degrees
/-- Note that `degreeOf_prod_eq` proves equality with `NoZeroDivisors R` and nonzero polynomials.
 -/
MvPolynomial.degreeOf_mul_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (i : σ) (f g : MvPolynomial σ R),
  MvPolynomial.degreeOf i (f * g) ≤ MvPolynomial.degreeOf i f + MvPolynomial.degreeOf i g
-- Mathlib.Data.Vector.Basic
/-- Construct a `Vector β (n + 1)` from a `Vector α n` by scanning `f : β → α → β`
from the "left", that is, from 0 to `Fin.last n`, using `b : β` as the starting value.
 -/
List.Vector.scanl : {α : Type u_1} → {n : ℕ} → {β : Type u_6} → (β → α → β) → β → List.Vector α n → List.Vector β (n + 1)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommMagma.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : CommMagma M] [inst_2 : ContinuousMul M],
  SeparationQuotient.instCommMagma = { toMul := SeparationQuotient.instMul, mul_comm := ⋯ }
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.of_zero_ofNat : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] (n : ℕ) [inst_4 : n.AtLeastTwo],
  (DirectSum.of A 0) (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Topology.Order.OrderClosed
Continuous.if_le : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α]
  {f g : β → α} [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ] [inst_5 : (x : β) → Decidable (f x ≤ g x)]
  {f' g' : β → γ},
  Continuous f' →
    Continuous g' →
      Continuous f →
        Continuous g → (∀ (x : β), f x = g x → f' x = g' x) → Continuous fun x => if f x ≤ g x then f' x else g' x
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.length : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red L₁ L₂ → ∃ n, L₁.length = L₂.length + 2 * n
-- Mathlib.Algebra.Star.Subalgebra
/-- The star subalgebra `StarSubalgebra.adjoin R {x}` generated by a single `x : A` is commutative
if `x` is normal.  -/
StarAlgebra.adjoinCommRingOfIsStarNormal : (R : Type u) →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : StarRing R] →
        [inst_2 : Ring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : StarRing A] →
              [inst_5 : StarModule R A] → (x : A) → [IsStarNormal x] → CommRing ↥(StarAlgebra.adjoin R {x})
-- Mathlib.Topology.Instances.ZMultiples
/-- The subgroup "multiples of `a`" (`zmultiples a`) is a discrete subgroup of `ℝ`, i.e. its
intersection with compact sets is finite.  -/
AddSubgroup.tendsto_zmultiples_subtype_cofinite : ∀ (a : ℝ), Filter.Tendsto (⇑(AddSubgroup.zmultiples a).subtype) Filter.cofinite (Filter.cocompact ℝ)
-- Mathlib.Data.Set.Defs
/-- Set builder syntax. This can be elaborated to either a `Set` or a `Finset` depending on context.

The elaborators for this syntax are located in:
* `Data.Set.Defs` for the `Set` builder notation elaborator for syntax of the form `{x | p x}`,
  `{x : α | p x}`, `{binder x | p x}`.
* `Data.Finset.Basic` for the `Finset` builder notation elaborator for syntax of the form
  `{x ∈ s | p x}`.
* `Data.Fintype.Basic` for the `Finset` builder notation elaborator for syntax of the form
  `{x | p x}`, `{x : α | p x}`, `{x ∉ s | p x}`, `{x ≠ a | p x}`.
* `Order.LocallyFinite.Basic` for the `Finset` builder notation elaborator for syntax of the form
  `{x ≤ a | p x}`, `{x ≥ a | p x}`, `{x < a | p x}`, `{x > a | p x}`.
 -/
Mathlib.Meta.setBuilder : Lean.ParserDescr
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_expand : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ} [inst_2 : ExpChar R p] {f : Polynomial R}
  [inst_3 : PerfectRing R p], ((Polynomial.expand R p) f).roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.GammaAux_recurrence1 : ∀ (s : ℂ) (n : ℕ), -s.re < ↑n → Complex.GammaAux✝ n s = Complex.GammaAux✝ n (s + 1) / s
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedCancelVAdd.toIsOrderedVAdd : ∀ {G : Type u_3} {P : Type u_4} {inst : LE G} {inst_1 : LE P} {inst_2 : VAdd G P} [self : IsOrderedCancelVAdd G P],
  IsOrderedVAdd G P
-- Mathlib.Algebra.Group.Finsupp
Finsupp.single_sub : ∀ {ι : Type u_1} {G : Type u_6} [inst : AddGroup G] (a : ι) (b₁ b₂ : G),
  (fun₀ | a => b₁ - b₂) = (fun₀ | a => b₁) - fun₀ | a => b₂
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.multicospanShape_L : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S),
  E.multicospanShape.L = E.I₀
-- Mathlib.Topology.Order.Bornology
IsOrderBornology.cobounded_eq : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : LinearOrder α] [IsOrderBornology α] [NoMaxOrder α] [NoMinOrder α],
  Bornology.cobounded α = Filter.atBot ⊔ Filter.atTop
-- Lean.Parser.Syntax
Lean.Parser.Command.catBehaviorBoth.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Module.SpanRank
/-- A submodule is finitely generated if and only if its `spanRank` is equal to its `spanFinrank`.
 -/
Submodule.fg_iff_spanRank_eq_spanFinrank : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  p.spanRank = ↑p.spanFinrank ↔ p.FG
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.produceMotive : Lean.Meta.RecursorInfo → List Bool
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_liftH : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData),
  CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ =
    h₂.liftH (h₁.descH (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) ⋯) ⋯
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- If `R` is the integral closure of `S` in `A`, then it is integrally closed in `A`.  -/
IsIntegrallyClosedIn.of_isIntegralClosure : ∀ (R : Type u_1) {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_3}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] [IsIntegralClosure A R B],
  IsIntegrallyClosedIn A B
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.PseudoCore.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F : CategoryTheory.LaxFunctor B C}
  (mapIdIso : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a))
  (mapCompIso :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g))
  (mapIdIso_inv :
    autoParam (∀ {a : B}, (mapIdIso a).inv = F.mapId a) CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv._autoParam)
  (mapCompIso_inv :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso f g).inv = F.mapComp f g)
      CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv._autoParam)
  (mapIdIso_1 : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a))
  (mapCompIso_1 :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g))
  (mapIdIso_inv_1 :
    autoParam (∀ {a : B}, (mapIdIso_1 a).inv = F.mapId a) CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv._autoParam)
  (mapCompIso_inv_1 :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso_1 f g).inv = F.mapComp f g)
      CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv._autoParam),
  ({ mapIdIso := mapIdIso, mapCompIso := mapCompIso, mapIdIso_inv := mapIdIso_inv, mapCompIso_inv := mapCompIso_inv } =
      { mapIdIso := mapIdIso_1, mapCompIso := mapCompIso_1, mapIdIso_inv := mapIdIso_inv_1,
        mapCompIso_inv := mapCompIso_inv_1 }) =
    (mapIdIso = mapIdIso_1 ∧ mapCompIso = mapCompIso_1)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.exists_partialMap_over : ∀ {X Y : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [inst : X.Over S] [inst_1 : Y.Over S]
  (f : X.RationalMap Y) [AlgebraicGeometry.Scheme.RationalMap.IsOver S f],
  ∃ g, AlgebraicGeometry.Scheme.PartialMap.IsOver S g ∧ g.toRationalMap = f
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- `trim` is additive.  -/
MeasureTheory.OuterMeasure.trim_add : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m₁ m₂ : MeasureTheory.OuterMeasure α), (m₁ + m₂).trim = m₁.trim + m₂.trim
-- Mathlib.Algebra.Order.Floor.Semifield
Mathlib.Meta.NormNum.IsNat.natFloor : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] (r : R)
  (m : ℕ), Mathlib.Meta.NormNum.IsNat r m → Mathlib.Meta.NormNum.IsNat ⌊r⌋₊ m