mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- The multiset `nthRoots ↑n (1 : R)` has no repeated elements
if there is a primitive root of unity in `R`.  -/
IsPrimitiveRoot.nthRoots_one_nodup : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
  IsPrimitiveRoot ζ n → (Polynomial.nthRoots n 1).Nodup
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap.eq_1 : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j),
  d.transitionMap hij =
    (CategoryTheory.Limits.isColimitOfPreserves (CategoryTheory.MorphismProperty.Over.map ⊤ ⋯) (d.isColimit i)).desc
      (d.transitionCocone hij)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntryD.eq_2 : ∀ {α : Type u} {β : α → Type v} (x : (a : α) × β a) (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxEntryD x = ⟨k, v⟩
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
/-- The invariant measure on the upper half-plane, defined by `dx dy / y ^ 2`.  -/
UpperHalfPlane.instMeasureSpace : MeasureTheory.MeasureSpace UpperHalfPlane
-- Mathlib.GroupTheory.Congruence.Defs
/-- A version of `Quotient.hrecOn₂'` for quotients by `Con`.  -/
Con.hrecOn₂ : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] →
      [inst_1 : Mul N] →
        {cM : Con M} →
          {cN : Con N} →
            {φ : cM.Quotient → cN.Quotient → Sort u_4} →
              (a : cM.Quotient) →
                (b : cN.Quotient) →
                  (f : (x : M) → (y : N) → φ ↑x ↑y) →
                    (∀ (x : M) (y : N) (x' : M) (y' : N), cM x x' → cN y y' → f x y ≍ f x' y') → φ a b
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.hasInterest' : {m : Type → Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Std.AtomicT Std.Http.Body.Channel.State✝ m Bool
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
            (𝒰.f i))
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j))
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).H = h.H
-- Aesop.Tree.Data
Aesop.NodeState.isIrrelevant : Aesop.NodeState → Bool
-- Mathlib.Analysis.Normed.Group.Hom
/-- For normed groups, an operator is zero iff its norm vanishes.  -/
NormedAddGroupHom.opNorm_zero_iff : ∀ {V₁ : Type u_5} {V₂ : Type u_6} [inst : NormedAddCommGroup V₁] [inst_1 : NormedAddCommGroup V₂]
  {f : NormedAddGroupHom V₁ V₂}, ‖f‖ = 0 ↔ f = 0
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_inv_ne_top : ∀ (a : ENNReal), a * a⁻¹ ≠ ⊤
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- We say that a valuation `v` is `Compatible` if the relation `x ≤ᵥ y`
is equivalent to `v x ≤ v y`.  -/
Valuation.Compatible : {R : Type u_1} →
  {Γ : Type u_2} →
    [inst : Ring R] → [inst_1 : LinearOrderedCommMonoidWithZero Γ] → Valuation R Γ → [ValuativeRel R] → Prop
-- Mathlib.CategoryTheory.MorphismProperty.CommaSites
CategoryTheory.MorphismProperty.isContinuous_comap_forget : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {S : C}
  [P.IsStableUnderComposition] (K : CategoryTheory.Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange]
  [K.IsStableUnderComposition] [K.HasPullbacks] [CategoryTheory.Limits.HasFiniteWidePullbacks C]
  [P.HasOfPostcompProperty P] [P.IsStableUnderBaseChange] [P.ContainsIdentities],
  K ≤ P.precoverage →
    (CategoryTheory.MorphismProperty.Over.forget P ⊤ S).IsContinuous
      (CategoryTheory.Precoverage.comap
          ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp (CategoryTheory.Over.forget S)) K).toGrothendieck
      (K.toGrothendieck.over S)
-- Mathlib.ModelTheory.LanguageMap
/-- A language with constants indexed by a type.  -/
FirstOrder.Language.constantsOn : Type u' → FirstOrder.Language
-- Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
MeasureTheory.measurable_embeddingReal : ∀ (Ω : Type u_2) [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω], Measurable (MeasureTheory.embeddingReal Ω)
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.max_eq_eval : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2)
  (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)),
  (Profinite.NobelingProof.Linear_CC' C hsC ho) (Profinite.NobelingProof.Products.eval C ↑l) =
    Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) (↑l).Tail
-- Mathlib.Algebra.Notation.Indicator
/-- `Set.mulIndicator s f a` is `f a` if `a ∈ s`, `1` otherwise.  -/
Set.mulIndicator : {α : Type u_1} → {M : Type u_3} → [One M] → Set α → (α → M) → α → M
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp_app : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₂ F₃]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₃] (j : J),
  (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₂ F₃).app j =
    CategoryTheory.Enriched.FunctorCategory.enrichedComp V ((CategoryTheory.Under.forget j).comp F₁)
      ((CategoryTheory.Under.forget j).comp F₂) ((CategoryTheory.Under.forget j).comp F₃)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instReprAltParamInfo.repr : Lean.Meta.Match.AltParamInfo → ℕ → Std.Format
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
RingHom.FaithfullyFlat.eq_and : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S],
  RingHom.FaithfullyFlat = fun f => f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)
-- Mathlib.Algebra.BrauerGroup.Defs
IsBrauerEquivalent.symm : ∀ {K : Type u} [inst : Field K] {A : CSA K} {B : CSA K}, IsBrauerEquivalent A B → IsBrauerEquivalent B A
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.balanceR : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      ((∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨
          ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r') →
        Ordnode.Valid' o₁ (l.balanceR x r) o₂
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.hom_ext_iff : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {Z : C} {g h : Z ⟶ ⨁ f},
  g = h ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.π f j) =
        CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.biproduct.π f j)
-- Init.Core
/-- `==` is reflexive, that is, `(a == a) = true`.  -/
ReflBEq.rfl : ∀ {α : Type u_1} {inst : BEq α} [self : ReflBEq α] {a : α}, (a == a) = true
-- Mathlib.Tactic.FunProp.Decl
/-- Register new function property.  -/
Mathlib.Meta.FunProp.addFunPropDecl : Lean.Name → Lean.MetaM Unit
-- Mathlib.Topology.Specialization
/-- A preorder is isomorphic to the specialisation order of its upper set topology.  -/
orderIsoSpecializationWithUpperSetTopology : (α : Type u_1) → [inst : Preorder α] → α ≃o Specialization (Topology.WithUpperSet α)
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousSubmodule_mul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (m n : ℕ),
  MvPolynomial.homogeneousSubmodule σ R m * MvPolynomial.homogeneousSubmodule σ R n ≤
    MvPolynomial.homogeneousSubmodule σ R (m + n)
-- Mathlib.Analysis.Calculus.LogDeriv
/-- The logarithmic derivative of a function defined as `deriv f /f`. Note that it will be zero
at `x` if `f` is not DifferentiableAt `x`.  -/
logDeriv : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] → [NormedAlgebra 𝕜 𝕜'] → (𝕜 → 𝕜') → 𝕜 → 𝕜'
-- Mathlib.Order.Interval.Basic
NonemptyInterval.pure_fst : ∀ {α : Type u_1} [inst : Preorder α] (a : α), (NonemptyInterval.pure a).toProd.1 = a
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.smul_compAlternatingMap : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {S : Type u_10} {N₂ : Type u_11}
  [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Monoid S] [inst_8 : DistribMulAction S N₂]
  [inst_9 : SMulCommClass R S N₂] (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N),
  (s • g).compAlternatingMap f = s • g.compAlternatingMap f
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.semilatticeSup : {E : Type u_3} → [inst : Group E] → SemilatticeSup (GroupSeminorm E)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.restoreM_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (x : m (Option α)),
  (Std.Do.wp (MonadControl.restoreM x)).apply Q =
    (Std.Do.wp x).apply (fun o => Option.casesOn o (Q.2.1 PUnit.unit) Q.1, Q.2.2)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instNonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C},
  Nonempty (HomotopicalAlgebra.Cylinder A)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
DirectedOn.ciInf_set_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderInf α] {f : β → α} {s : Set β},
  DirectedOn (fun x1 x2 => x2 ≤ x1) (f '' s) → BddBelow (f '' s) → ∀ {c : β}, c ∈ s → ⨅ i, f ↑i ≤ f c
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.argPos : Lean.Elab.Tactic.ElimApp.State✝ → ℕ
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsTensorFreeLEquiv_symm_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (α : Type u) [inst_2 : DecidableEq α]
  (a : α →₀ ↑A), (A.coinvariantsTensorFreeLEquiv α).symm a = (A.finsuppToCoinvariantsTensorFree α) a
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.conductor_eq_zero_iff_level_eq_zero : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n}, χ.conductor = 0 ↔ n = 0
-- Mathlib.Lean.Expr.Basic
/-- Inspects `body`, and if it is a `.forallE` of an instance with type `type` such that `p type`
is `true` and the remainder of the type does not depend on it, pushes the `current` index onto
the accumulated array.  -/
_private.Mathlib.Lean.Expr.Basic.0.Lean.Expr.getUnusedForallInstanceBinderIdxsWhere.go : (Lean.Expr → Bool) → Lean.Expr → ℕ → Array ℕ → Array ℕ
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  {J : CategoryTheory.GrothendieckTopology C} [F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j),
  CategoryTheory.Sieve.ofArrows X' f' ∈ J S → (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).Full
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J J_1 : CategoryTheory.GrothendieckTopology C} (e_J : J = J_1) {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : CategoryTheory.Presheaf.IsSheaf J P) {I : Type u_1} {S : C} {X : I → C} (f f_1 : (i : I) → X i ⟶ S)
  (e_f : f = f_1) (hf : CategoryTheory.Sieve.ofArrows X f ∈ J S) {E : A}
  (x x_1 : (i : I) → E ⟶ P.obj (Opposite.op (X i))) (e_x : x = x_1)
  (hx :
    ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j),
      CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j) →
        CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) = CategoryTheory.CategoryStruct.comp (x j) (P.map b.op)),
  hP.amalgamateOfArrows f hf x hx = ⋯.amalgamateOfArrows f_1 ⋯ x_1 ⋯
-- Mathlib.Topology.Path
Continuous.path_trans : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y z : X} {f : Y → Path x y}
  {g : Y → Path y z}, Continuous f → Continuous g → Continuous fun t => (f t).trans (g t)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.min_δ : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  {hd : x.dim = d + 1} {l : Fin (d + 1)} (hl : SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ),
  SSet.prodStdSimplex.pairingCore.min hl.δ ⋯ = l
-- Mathlib.Control.LawfulFix
Part.fix_eq_ωSup_of_ωScottContinuous : ∀ {α : Type u_1} {β : α → Type u_2} {g : ((a : α) → Part (β a)) → (a : α) → Part (β a)}
  (hc : OmegaCompletePartialOrder.ωScottContinuous g),
  Part.fix g = OmegaCompletePartialOrder.ωSup (Part.Fix.approxChain { toFun := g, monotone' := ⋯ })
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.starRing : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Algebra R A] → [inst_5 : StarModule R A] → (s : StarSubalgebra R A) → StarRing ↥s
-- Mathlib.Data.Set.Operations
Set.mem_seq_iff : ∀ {α : Type u} {β : Type v} {s : Set (α → β)} {t : Set α} {b : β}, b ∈ s.seq t ↔ ∃ f ∈ s, ∃ a ∈ t, f a = b
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_right_inj₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {m n : ℕ}
  [ZeroLEOneClass M₀], 0 < a → a ≠ 1 → (a ^ m = a ^ n ↔ m = n)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- If a function is defined piecewise in terms of functions which are continuous on their
respective pieces, then it is measurable.  -/
ContinuousOn.measurable_piecewise : ∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ] [BorelSpace γ] {f g : α → γ} {s : Set α}
  [inst_6 : (j : α) → Decidable (j ∈ s)],
  ContinuousOn f s → ContinuousOn g sᶜ → MeasurableSet s → Measurable (s.piecewise f g)
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.boundaries_nonempty : ∀ {n : ℕ} (c : CompositionAsSet n), c.boundaries.Nonempty
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Presheaf.classifier_truth : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.Presheaf.classifier C).truth = CategoryTheory.Presheaf.truth C
-- Mathlib.Algebra.Jordan.Basic
commute_lmul_rmul : ∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [IsJordan A] (a : A),
  Commute (AddMonoid.End.mulLeft a) (AddMonoid.End.mulRight a)
-- Mathlib.Topology.Continuous
/-- If `f` has dense range and `s` is an open set in the codomain of `f`, then the image of the
preimage of `s` under `f` is dense in `s`.  -/
DenseRange.subset_closure_image_preimage_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X} {s : Set X},
  DenseRange f → IsOpen s → s ⊆ closure (f '' f ⁻¹' s)
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- The definition of conjugate roots.
 -/
isConjRoot_def : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x y : A},
  IsConjRoot R x y ↔ minpoly R x = minpoly R y
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃_inv_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₃ : T₁.obj₃ ≅ T₂.obj₃)
  (comm :
    CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map e₁.hom) =
      CategoryTheory.CategoryStruct.comp e₃.hom T₂.mor₃),
  (CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃ T₁ T₂ hT₁ hT₂ e₁ e₃ comm).inv.hom₃ = e₃.inv
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft.sizeOf_spec : ∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η : Mathlib.Tactic.BicategoryLike.Mor₂),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e isoLift? f g h η) =
    1 + sizeOf e + sizeOf isoLift? + sizeOf f + sizeOf g + sizeOf h + sizeOf η
-- Init.Data.Int.Order
Int.le_sub_left_of_add_le : ∀ {a b c : ℤ}, a + b ≤ c → b ≤ c - a
-- Mathlib.Topology.Algebra.GroupWithZero
map_mul_left_nhds_one₀ : ∀ {G₀ : Type u_3} [inst : TopologicalSpace G₀] [inst_1 : GroupWithZero G₀] [SeparatelyContinuousMul G₀] {a : G₀},
  a ≠ 0 → Filter.map (fun x => a * x) (nhds 1) = nhds a
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigOWith.const_smul_self : ∀ {α : Type u_1} {E' : Type u_6} {R : Type u_13} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedRing R]
  {f' : α → E'} {l : Filter α} [inst_2 : Module R E'] [IsBoundedSMul R E'] (c' : R),
  Asymptotics.IsBigOWith ‖c'‖ l (fun x => c' • f' x) f'
-- Mathlib.NumberTheory.LSeries.Dirichlet
ArithmeticFunction.not_LSeriesSummable_moebius_at_one : ¬LSeriesSummable (fun n => ↑(ArithmeticFunction.moebius n)) 1
-- Mathlib.Analysis.Normed.Group.Hom
/-- Normed group homomorphisms themselves form a seminormed group with respect to
the operator norm.  -/
NormedAddGroupHom.toSeminormedAddCommGroup : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] →
      [inst_1 : SeminormedAddCommGroup V₂] → SeminormedAddCommGroup (NormedAddGroupHom V₁ V₂)
-- Mathlib.Data.SetLike.Basic
SetLike.coe_ne_coe : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, ↑p ≠ ↑q ↔ p ≠ q
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.zeta_pos : ∀ {x : ℕ}, 0 < ArithmeticFunction.zeta x ↔ 0 < x
-- Mathlib.Data.Fintype.Sets
Set.toFinset_union : ∀ {α : Type u_1} (s t : Set α) [inst : DecidableEq α] [inst_1 : Fintype ↑s] [inst_2 : Fintype ↑t]
  [inst_3 : Fintype ↑(s ∪ t)], (s ∪ t).toFinset = s.toFinset ∪ t.toFinset
-- Init.Data.Nat.Basic
Nat.beq.eq_1 : Nat.zero.beq Nat.zero = true
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_C_lt_degree_C_mul_X : ∀ {R : Type u} {a b : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C b).degree < (Polynomial.C a * Polynomial.X).degree
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An isometric version of `Submodule.quotEquivOfEq`.  -/
Submodule.quotLIEOfEq : {M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {R : Type u_3} → [inst_1 : Ring R] → [inst_2 : Module R M] → (S T : Submodule R M) → S = T → M ⧸ S ≃ₗᵢ[R] M ⧸ T
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmopEquiv_inverse_map_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.MonoidalOpposite.unmopEquiv C).inverse.map f).unmop = f
-- Mathlib.Order.BoundedOrder.Basic
OrderBot.lift.eq_1 : ∀ {α : Type u} {β : Type v} [inst : LE α] [inst_1 : Bot α] [inst_2 : LE β] [inst_3 : OrderBot β] (f : α → β)
  (map_le : ∀ (b a : α), f b ≤ f a → b ≤ a) (map_top : f ⊥ = ⊥),
  OrderBot.lift f map_le map_top = { toBot := inst_1, bot_le := ⋯ }
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.StrongHomClass.elementarilyEquivalent : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {F : Type u_4}
  [inst_2 : EquivLike F M N] [L.StrongHomClass F M N] (g : F), L.ElementarilyEquivalent M N
-- Init.Data.Nat.Coprime
Nat.Coprime.gcd_right : ∀ {m n : ℕ} (k : ℕ), m.Coprime n → m.Coprime (k.gcd n)
-- Mathlib.GroupTheory.Nilpotent
/-- A group `G` is nilpotent iff there exists a descending central series which reaches the
trivial group in a finite time.  -/
Subgroup.nilpotent_iff_finite_descending_central_series : ∀ (G : Type u_1) [inst : Group G], Group.IsNilpotent G ↔ ∃ n H, Subgroup.IsDescendingCentralSeries H ∧ H n = ⊥
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {km : α}, t.minKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- For an infinite place `w`, return an embedding `φ` such that `w = infinite_place φ` .  -/
NumberField.InfinitePlace.embedding : {K : Type u_1} → [inst : Field K] → NumberField.InfinitePlace K → K →+* ℂ
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.instToStringFourierMotzkinData : ToString Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData
-- Mathlib.RingTheory.RootsOfUnity.Lemmas
/-- If `μ` is a primitive `n`th root of unity in `R` and `k < n`, then `n` is divisible
by `(μ-1)^k` in `ℤ[μ] ⊆ R`.  -/
IsPrimitiveRoot.self_sub_one_pow_dvd_order : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {k n : ℕ},
  k < n → ∀ {μ : R}, IsPrimitiveRoot μ n → ∃ z ∈ ℤ[μ], ↑n = z * (μ - 1) ^ k