mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.of_cons : ∀ {α : Type u} (a : α) (m : Multiset α),
  FreeAbelianGroup.of (Multiplicative.ofAdd (a ::ₘ m)) =
    FreeCommRing.of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)
-- Mathlib.Order.Directed
DirectedOn.is_bot_of_is_min : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → ∀ {m : α}, m ∈ s → (∀ a ∈ s, a ≤ m → m ≤ a) → ∀ a ∈ s, m ≤ a
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.comp.congr_simp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsStableUnderComposition]
  [inst_4 : W.IsStableUnderComposition] {X Y Z : CategoryTheory.MorphismProperty.Comma L R P Q W} (f f_1 : X.Hom Y),
  f = f_1 → ∀ (g g_1 : Y.Hom Z), g = g_1 → f.comp g = f_1.comp g_1
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_coeff_coeff : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial (Option σ) R) (m : ℕ) (d : σ →₀ ℕ),
  MvPolynomial.coeff d (((MvPolynomial.optionEquivLeft R σ) p).coeff m) = MvPolynomial.coeff (Finsupp.optionElim m d) p
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `MDifferentiable.smul` -/
MDifferentiable.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V}, MDiff f → MDiff g → MDiff fun i => f i • g i
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.rightOp_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D},
  CategoryTheory.NatTrans.rightOp (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.rightOp
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instNontrivial : ∀ {α : Type u} [Nonempty α], Nontrivial (WithZero α)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
tprod_const : ∀ {β : Type u_2} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [IsTopologicalGroup G] [T2Space G]
  (a : G), ∏' (x : β), a = a ^ Nat.card β
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.uliftFunctor_map : ∀ {x x_1 : AddMonCat} (f : x ⟶ x_1),
  AddMonCat.uliftFunctor.map f =
    AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddMonCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom))
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : SizeOf α] (carrier : Set α) (isClosed' : IsClosed carrier),
  sizeOf { carrier := carrier, isClosed' := isClosed' } = 1 + sizeOf isClosed'
-- Init.Grind.Ordered.Int
Lean.Grind.instOrderedRingInt : Lean.Grind.OrderedRing ℤ
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whiskeringEquivalence_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  (CategoryTheory.Limits.Cocone.whiskeringEquivalence e).counitIso =
    CategoryTheory.NatIso.ofComponents'
      (fun s =>
        CategoryTheory.Limits.Cocone.extInv
          (CategoryTheory.Iso.refl
            ((((CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
                        (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv)).comp
                    (CategoryTheory.Limits.Cocone.whiskering e.functor)).obj
                s).pt)
          ⋯)
      ⋯
-- Mathlib.Tactic.Translate.Core
/-- Get the translation for the given name.  -/
Mathlib.Tactic.Translate.findTranslation? : Lean.Environment → Mathlib.Tactic.Translate.TranslateData → Lean.Name → Option Mathlib.Tactic.Translate.TranslationInfo
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_inter_self_eq_sdiff`. -/
Set.diff_inter_self_eq_diff : ∀ {α : Type u_1} {s t : Set α}, s \ (t ∩ s) = s \ t
-- Mathlib.Data.Set.Equitable
/-- A set is equitable if no element value is more than one bigger than another.  -/
Set.EquitableOn : {α : Type u_1} → {β : Type u_2} → [LE β] → [Add β] → [One β] → Set α → (α → β) → Prop
-- Mathlib.Topology.Category.Born
/-- The category of bornologies.  -/
Born : Type (u_1 + 1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
NonUnitalIsometricContinuousFunctionalCalculus.quasispectrum_le : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [StarOrderedRing A]
  [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) ⦃x : NNReal⦄,
  x ∈ quasispectrum NNReal a →
    autoParam (0 ≤ a) NonUnitalIsometricContinuousFunctionalCalculus.quasispectrum_le._auto_1 → x ≤ ‖a‖₊
-- Mathlib.CategoryTheory.Limits.Opposites
/-- If `C` has limits, we can construct colimits for `Cᵒᵖ`.
 -/
CategoryTheory.Limits.hasColimits_op_of_hasLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasLimitsOfSize.{v₂, u₂, v₁, u₁} C],
  CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ
-- Init.Data.BitVec.Bitblast
BitVec.shiftLeftRec.eq_2 : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (s_1 : ℕ),
  x.shiftLeftRec y s_1.succ = x.shiftLeftRec y s_1 <<< (y &&& BitVec.twoPow w₂ s_1.succ)
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.toClopens : {α : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : LE α] → ClopenUpperSet α → TopologicalSpace.Clopens α
-- Mathlib.Analysis.Convex.Body
ConvexBody.hausdorffEDist_ne_top : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] {K L : ConvexBody V},
  Metric.hausdorffEDist ↑K ↑L ≠ ⊤
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfcₙ_le_iff : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : NNReal),
  autoParam (ContinuousOn f (quasispectrum 𝕜 a)) nnnorm_cfcₙ_le_iff._auto_1 →
    autoParam (f 0 = 0) nnnorm_cfcₙ_le_iff._auto_3 →
      autoParam (p a) nnnorm_cfcₙ_le_iff._auto_5 → (‖cfcₙ f a‖₊ ≤ c ↔ ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ ≤ c)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
SimpleGraph.Coloring.even_length_iff_congr : ∀ {α : Type u_1} {G : SimpleGraph α} (c : G.Coloring Bool) {u v : α} (p : G.Walk u v),
  Even p.length ↔ (c u = true ↔ c v = true)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.Abelian D] {C : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} C] [inst_3 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  (P : CategoryTheory.InjectiveResolution X) (Q : CategoryTheory.InjectiveResolution Y) (φ : P.cocomplex ⟶ Q.cocomplex),
  CategoryTheory.CategoryStruct.comp (P.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (Q.ι.f 0) →
    ∀ (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
      CategoryTheory.CategoryStruct.comp (F.map f) (Q.toRightDerivedZero' F) =
        CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F)
          (HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0)
-- Lean.DocString.Parser
/-- We can only start a nestable block if we're immediately after a newline followed by a sequence of
nestable block openers
 -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.onlyBlockOpeners : Lean.Parser.ParserFn
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.zpowers_eq_bot : ∀ {G : Type u_1} [inst : Group G] {g : G}, Subgroup.zpowers g = ⊥ ↔ g = 1
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.pi : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  {X : ι → Type u_7} [inst_3 : (i : ι) → Convexity.ConvexSpace R (X i)] {s : Set ι} {t : (i : ι) → Set (X i)},
  (∀ i ∈ s, Convexity.IsConvexSet R (t i)) → Convexity.IsConvexSet R (s.pi t)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.compare_getKey?_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, Option.all (fun x => decide (compare x k = Ordering.eq)) (t.getKey? k) = true
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_pow_left : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n : ℕ),
  f.leadingCoeff ^ m ≠ 0 → g.natDegree ≤ n → (f ^ m).resultant g (f ^ m).natDegree n = f.resultant g f.natDegree n ^ m
-- Std.Sync.Channel
/-- Consumers that are blocked on a producer providing them a value. They will be resolved to `none`
if the channel closes.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.State.consumers : {α : Type} → Std.CloseableChannel.Unbounded.State✝ α → Std.Queue (Std.CloseableChannel.Consumer✝ α)
-- Mathlib.RingTheory.QuotSMulTop
/-- Reducing a module modulo `r` is the same as left tensoring with `R/(r)`.  -/
QuotSMulTop.equivQuotTensor : {R : Type u_2} →
  [inst : CommRing R] →
    (r : R) →
      (M : Type u_1) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuotSMulTop r M ≃ₗ[R] TensorProduct R (R ⧸ Ideal.span {r}) M
-- Mathlib.Algebra.Order.Field.Basic
mul_le_of_forall_lt_of_nonneg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b c : α},
  0 ≤ a → 0 ≤ c → (∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c) → a * b ≤ c
-- Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
/-- A measure is a zero-one measure if it only takes the values `0` or `1`.  -/
MeasureTheory.IsZeroOneMeasure : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_13 : HSub Std.Time.Second.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Mathlib.Geometry.Convex.Cone.Basic
/-- **Alias** of `ConvexCone.IsReproducing.of_span_eq_top`. -/
ConvexCone.IsGenerating.isReproducing : ∀ {R : Type u_7} {M : Type u_8} [inst : Ring R] [inst_1 : LinearOrder R] [AddLeftStrictMono R] [inst_3 : AddCommGroup M]
  [Nontrivial M] [inst_5 : Module R M] {C : ConvexCone R M}, Submodule.span R ↑C = ⊤ → C.IsReproducing
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.rank_inj : ∀ {x y : ZFSet.{u_1}}, x.IsOrdinal → y.IsOrdinal → (x.rank = y.rank ↔ x = y)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Evaluation at a point as an `AddActionHom`.  -/
Pi.evalAddActionHom : {ι : Type u_1} →
  {M : Type u_2} → {X : ι → Type u_3} → [inst : (i : ι) → VAdd M (X i)] → (i : ι) → ((i : ι) → X i) →ₑ[id] X i
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
SSet.Subcomplex.Pairing.op_p : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (x : ↑P.II),
  P.op.p ⟨SSet.Subcomplex.N.opEquiv.symm ↑x, ⋯⟩ = ⟨SSet.Subcomplex.N.opEquiv.symm ↑(P.p x), ⋯⟩
-- Mathlib.Tactic.Conv
/-- Elaborator for the `discharge` tactic.  -/
Mathlib.Tactic.Conv.elabDischargeConv : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulReflectLT.mk : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α]
  [toContravariantClass : ContravariantClass { x // 0 ≤ x } α (fun x y => ↑x * y) fun x1 x2 => x1 < x2],
  PosMulReflectLT α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.insertMany_append : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {l₁ l₂ : List ((a : α) × β a)},
  t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.iteratedDeriv_two_cgf_eq_integral : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    iteratedDeriv 2 (ProbabilityTheory.cgf X μ) v =
      (∫ (x : Ω), (fun ω => (X ω - deriv (ProbabilityTheory.cgf X μ) v) ^ 2 * Real.exp (v * X ω)) x ∂μ) /
        ProbabilityTheory.mgf X μ v
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_right : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Qₙ : QuadraticForm R N} (f₁ : Q₁ →qᵢ Qₙ)
  (f₂ : Q₂ →qᵢ Qₙ),
  (∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)) →
    ∀ (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₁ : ZMod 2},
      m₁ ∈ CliffordAlgebra.evenOdd Q₁ i₁ →
        m₂ ∈ CliffordAlgebra.evenOdd Q₂ 0 → Commute ((CliffordAlgebra.map f₁) m₁) ((CliffordAlgebra.map f₂) m₂)
-- Mathlib.Analysis.Normed.Group.Bounded
comap_norm_atTop : ∀ {E : Type u_2} [inst : SeminormedAddGroup E], Filter.comap norm Filter.atTop = Bornology.cobounded E
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.Arrows.forkMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type t}
  [inst_1 : Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B),
  CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π = CategoryTheory.Limits.Pi.lift fun i => P.map (π i).op
-- Mathlib.Analysis.Normed.Module.FiniteDimension
isOpen_setOfPred_affineIndependent : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι], IsOpen {p | AffineIndependent 𝕜 p}
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.inr_i_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A A] {Z : C} (h : P.I ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp P.i h) =
    CategoryTheory.CategoryStruct.comp P.i₁ h
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.inclusion_injective : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S T : NonUnitalSubalgebra R A} (h : S ≤ T), Function.Injective ⇑(NonUnitalSubalgebra.inclusion h)
-- Lean.Parser.Term
Lean.Parser.Tactic.quot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The equivalence of quotients by multiples of an integer induced by an additive
group isomorphism.  -/
QuotientAddGroup.equivQuotientZSMulOfEquiv : {A B : Type u} →
  [inst : AddCommGroup A] →
    [inst_1 : AddCommGroup B] → A ≃+ B → (n : ℤ) → A ⧸ (zsmulAddGroupHom n).range ≃+ B ⧸ (zsmulAddGroupHom n).range
-- Mathlib.Analysis.Normed.Lp.ProdLp
_private.Mathlib.Analysis.Normed.Lp.ProdLp.0.WithLp.prod_uniformity_aux : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β], uniformity (WithLp p (α × β)) = uniformity (WithLp p (α × β))
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- An adjunction of monoidal functors lifts to an adjunction of their lifts to group objects.  -/
CategoryTheory.Adjunction.mapGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                (F ⊣ G) → [inst_4 : F.Monoidal] → [inst_5 : G.Monoidal] → F.mapGrp ⊣ G.mapGrp
-- Mathlib.Analysis.Complex.Basic
Complex.ofReal_eq_re_of_isSelfAdjoint : ∀ {x : ℂ} {y : ℝ}, IsSelfAdjoint x → (y = x.re ↔ ↑y = x)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
/-- Construct a term of `FiniteAddGrp` from a type endowed with the structure of a
finite additive group.  -/
FiniteAddGrp.of : (G : Type u) → [AddGroup G] → [Finite G] → FiniteAddGrp.{u}
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.Trivialization.contMDiffAt_iff : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  {f : M → Bundle.TotalSpace F E} {x₀ : M},
  f x₀ ∈ e.source →
    (ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f x₀ ↔
      ContMDiffAt IM IB n (fun x => (f x).proj) x₀ ∧
        ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n (fun x => (↑e (f x)).2) x₀)
-- Std.Sat.AIG.Basic
/-- A vector of references into `aig`. This is the `AIG` analog of `BitVec`.
 -/
Std.Sat.AIG.RefVec : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_le_of_forall_imp : ∀ {V : Type u} {G : SimpleGraph V} {V' : Type u_4} {G' : SimpleGraph V'},
  (∀ (n : ℕ), G'.Colorable n → G.Colorable n) → G.chromaticNumber ≤ G'.chromaticNumber
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.mul_X_sub_intCast_comp : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R} {n : ℕ}, (p * (Polynomial.X - ↑n)).comp q = p.comp q * (q - ↑n)
-- Mathlib.CategoryTheory.ConcreteCategory.Representable
CategoryTheory.Functor.RepresentableBy.homEquiv'_comp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor Cᵒᵖ D} {CD : D → Type u_3}
  {FD : D → D → Type u_4} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {Y : C} (α : (F.comp (CategoryTheory.forget D)).RepresentableBy Y)
  {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
  α.homEquiv' (CategoryTheory.CategoryStruct.comp f g) =
    (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (α.homEquiv' g)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc.congr_simp : ∀ {R : Type u_3} {A : Type u_4} {p p_1 : A → Prop} (e_p : p = p_1) [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A]
  [inst_6 : Ring A] [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p]
  (f f_1 : R → R), f = f_1 → ∀ (a a_1 : A), a = a_1 → cfc f a = cfc f_1 a_1
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvalues₀_antitone : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), Antitone hA.eigenvalues₀
-- Init.Data.List.Lemmas
List.getLastD_eq_getLast? : ∀ {α : Type u_1} {a : α} {l : List α}, l.getLastD a = l.getLast?.getD a
-- Mathlib.Order.Filter.Pointwise
Filter.mul_eq_one_iff : ∀ {α : Type u_2} [inst : DivisionMonoid α] {f g : Filter α}, f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
-- Mathlib.Data.Set.Lattice
Set.biInter_inter : ∀ {ι : Type u_12} {α : Type u_13} {s : Set ι},
  s.Nonempty → ∀ (f : ι → Set α) (t : Set α), ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t
-- Mathlib.Order.SuccPred.Basic
WithBot.instIsEmptySuccOrderOfNonempty : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] [hα : Nonempty α], IsEmpty (SuccOrder (WithBot α))
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_mem_mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a * b ∈ s * t
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- Construct an element of `(F ⨿ G).obj a` from an element of `G.obj a`  -/
CategoryTheory.FunctorToTypes.coprodInr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C (Type w)} → {a : C} → G.obj a → (F ⨿ G).obj a
-- Mathlib.Order.Birkhoff
OrderIso.infIrredUpperSet_apply : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Finite α] (a : α), OrderIso.infIrredUpperSet a = ⟨UpperSet.Ici a, ⋯⟩
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_inter_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t₁ t₂ : Finset α}, s + t₁ ∩ t₂ ⊆ (s + t₁) ∩ (s + t₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The comparison morphism for the pushout of `f,g`.
This is an isomorphism iff `G` preserves the pushout of `f,g`; see
`Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean`
 -/
CategoryTheory.Limits.pushoutComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (G : CategoryTheory.Functor C D) →
            (f : X ⟶ Y) →
              (g : X ⟶ Z) →
                [inst_2 : CategoryTheory.Limits.HasPushout f g] →
                  [inst_3 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] →
                    CategoryTheory.Limits.pushout (G.map f) (G.map g) ⟶ G.obj (CategoryTheory.Limits.pushout f g)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_rev_Ico : ∀ {n : ℕ} (i j : Fin n), Fin.rev ⁻¹' Set.Ico i j = Set.Ioc j.rev i.rev
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.kerLift.eq_1 : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H),
  QuotientGroup.kerLift φ = QuotientGroup.lift φ.ker φ ⋯
-- Mathlib.Order.Filter.SmallSets
/-- **Alias** of the reverse direction of `Filter.eventually_smallSets_forall`. -/
Filter.Eventually.smallSets : ∀ {α : Type u_1} {l : Filter α} {p : α → Prop}, (∀ᶠ (x : α) in l, p x) → ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.ext_iff : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ}
  {s t : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj V)}, s = t ↔ ↑s = ↑t
-- Mathlib.FieldTheory.SeparableClosure
/-- An intermediate field of `E / F` is contained in the separable closure of `F` in `E`
if it is separable over `F`.  -/
le_separableClosure : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  [Algebra.IsSeparable F ↥L], L ≤ separableClosure F E
-- Mathlib.Topology.MetricSpace.Bounded
Metric.tendsto_dist_left_cobounded_atTop : ∀ {α : Type u} [inst : PseudoMetricSpace α] (c : α), Filter.Tendsto (dist c) (Bornology.cobounded α) Filter.atTop
-- Mathlib.Algebra.Field.Opposite
MulOpposite.instNNRatCast.eq_1 : ∀ {α : Type u_1} [inst : NNRatCast α], MulOpposite.instNNRatCast = { nnratCast := fun q => MulOpposite.op ↑q }