mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Prelude
/-- The typeclass behind the notation `a ^^^ b : γ` where `a : α`, `b : β`.  -/
HXor : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
/-- A right derived functor is a pointwise right derived functor when
there exists a pointwise right derived functor.  -/
CategoryTheory.Functor.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor : {C : Type u₁} →
  {D : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            (F' : CategoryTheory.Functor D H) →
              {F : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (α : F ⟶ L.comp F') →
                    (W : CategoryTheory.MorphismProperty C) →
                      [F.HasPointwiseRightDerivedFunctor W] →
                        [inst_4 : L.IsLocalization W] →
                          [F'.IsRightDerivedFunctor α W] →
                            (CategoryTheory.Functor.LeftExtension.mk F' α).IsPointwiseLeftKanExtension
-- Mathlib.Topology.Homeomorph.Defs
/-- The forward map of a homeomorphism is a continuous function.  -/
Homeomorph.continuous_toFun : ∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (self : X ≃ₜ Y),
  Continuous self.toFun
-- Mathlib.Data.Fin.Tuple.Reflection
/-- Creates the expression `f 0 * f 1 * ... * f (n - 1)`.  -/
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.mkProdEqQ.makeRHS : {u : Lean.Level} →
  {α : Q(Type u)} → Q(CommMonoid «$α») → (n : ℕ) → Q(Fin «$n» → «$α») → Q(NeZero «$n») → ℕ → Lean.MetaM Q(«$α»)
-- Init.Data.List.Lemmas
List.any_eq_false : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, l.any p = false ↔ ∀ x ∈ l, ¬p x = true
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.tacticSeqBracketed.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Sites.Finite
CategoryTheory.Precoverage.mem_finite_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Presieve X},
  s ∈ (CategoryTheory.Precoverage.finite C).coverings X ↔ s.uncurry.Finite
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_zero : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), ↑0 = 0
-- Mathlib.Combinatorics.Graph.Simple
Graph.vertexSet_ofSimpleGraph : ∀ {α : Type u_1} (G : SimpleGraph α), (Graph.ofSimpleGraph G).vertexSet = Set.univ
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_mul : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (x y : WithAbs v), (x * y).ofAbs = x.ofAbs * y.ofAbs
-- Mathlib.Algebra.Star.Unitary
Unitary.instHasDistribNegSubtypeMemSubmonoidUnitary : {R : Type u_1} → [inst : Ring R] → [inst_1 : StarRing R] → HasDistribNeg ↥(unitary R)
-- Std.Async.Signal
Std.Async.instBEqSignal : BEq Std.Async.Signal
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.stupidTruncMap_stupidTruncXIso_hom : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c')
  [inst_3 : e.IsRelIff] {i : ι} {i' : ι'} (hi : e.f i = i'),
  CategoryTheory.CategoryStruct.comp ((HomologicalComplex.stupidTruncMap φ e).f i') (L.stupidTruncXIso e hi).hom =
    CategoryTheory.CategoryStruct.comp (K.stupidTruncXIso e hi).hom (φ.f i')
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_inverseImage_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty D) (F : CategoryTheory.Functor C D), (P.inverseImage F).map F ≤ P.isoClosure
-- Mathlib.Algebra.Lie.Matrix
Matrix.lieConj_apply : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (P A : Matrix n n R)
  (h : Invertible P), (P.lieConj h) A = P * A * P⁻¹
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b}, CurveIntegrable ω γ → CurveIntegrable ω γ.symm
-- Init.Data.UInt.Lemmas
UInt8.add_eq_right : ∀ {a b : UInt8}, a + b = b ↔ a = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.ofColimitCocone_π : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C}
  {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t)
  (j : J),
  (CategoryTheory.Limits.Bicone.ofColimitCocone ht).π j =
    ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun j' => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)
-- Lean.Server.GoTo
Lean.Server.GoToContext.doc : Lean.Server.GoToContext → Lean.Server.DocumentMeta
-- Mathlib.RingTheory.Adjoin.FG
isNoetherianRing_of_fg : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Subalgebra R A},
  S.FG → ∀ [IsNoetherianRing R], IsNoetherianRing ↥S
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.lTensor : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_4)
  {B : Type u_5} {D : Type u_7} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : CommRing D]
  [inst_10 : Algebra R D] {f : B →ₐ[R] D}, f.Flat → (Algebra.TensorProduct.lTensor A f).Flat
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_maxKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β}, (t.modify k f).maxKey?.isSome = !t.isEmpty
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.ιMapBifunctorOrZero_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J)
  (h : c₁.π c₂ c (i₁, i₂) = j), K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j = K₁.ιMapBifunctor K₂ F c i₁ i₂ j h
-- Aesop.Tracing
Aesop.registerTraceOption : Lean.Name → String → IO Aesop.TraceOption
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.FullyFaithful.homMulEquiv_apply : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.MonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal] (hF : F.FullyFaithful) (a : X ⟶ M),
  (CategoryTheory.Functor.FullyFaithful.homMulEquiv F hF) a = F.map a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.forInStep.match_1.splitter : {δ : Type u_1} →
  (motive : ForInStep δ → Sort u_2) →
    (__do_lift : ForInStep δ) →
      ((d : δ) → motive (ForInStep.done d)) → ((d : δ) → motive (ForInStep.yield d)) → motive __do_lift
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.coe_subtype : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} (H : S) [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G],
  ⇑↑H = Subtype.val
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
RootPairing.GeckConstruction.isSl2Triple : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : IsDomain R] [inst_3 : CharZero R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {b : P.Base} [inst_9 : Fintype ι]
  (i : ↥b.support) [P.IsReduced] [inst_11 : DecidableEq ι],
  IsSl2Triple (RootPairing.GeckConstruction.h i) (RootPairing.GeckConstruction.e i) (RootPairing.GeckConstruction.f i)
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.mk_smul_mk_quotient_map_quotient : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {p : Ideal R} [inst_2 : Algebra R S] (x : R)
  (y : S),
  (Ideal.Quotient.mk p) x • (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) y =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ((algebraMap R S) x * y)
-- Mathlib.Order.Category.BddLat
BddLat.hasForgetToSemilatSup : CategoryTheory.HasForget₂ BddLat SemilatSupCat
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.BuiltinPropagators.mk.injEq : ∀ (up down up_1 down_1 : Lean.Meta.Grind.PropagatorMap),
  ({ up := up, down := down } = { up := up_1, down := down_1 }) = (up = up_1 ∧ down = down_1)
-- Mathlib.Topology.Order
continuous_generateFrom_iff : ∀ {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α} {b : Set (Set β)},
  Continuous f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)
-- Mathlib.RingTheory.Perfection
PerfectionMap.map_map : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₃}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {S : Type u₂} [inst_6 : CommSemiring S]
  [inst_7 : CharP S p] {Q : Type u₄} [inst_8 : CommSemiring Q] [inst_9 : CharP Q p] [inst_10 : PerfectRing Q p]
  {π : P →+* R} (m : PerfectionMap p π) {σ : Q →+* S} (n : PerfectionMap p σ) (φ : R →+* S) (x : P),
  σ ((PerfectionMap.map p m n φ) x) = φ (π x)
-- Mathlib.RingTheory.Flat.Rank
/-- **Alias** of the forward direction of `Module.algebraMap_bijective_iff_rankAtStalk`.

---

If `S` is a finite, flat `R`-algebra, `S` is of constant rank `1` if and only if
`S` is isomorphic to `R`.  -/
Module.algebraMap_bijective_of_rankAtStalk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Module.Finite R S], Module.rankAtStalk S = 1 → Function.Bijective ⇑(algebraMap R S)
-- Mathlib.Algebra.Order.Archimedean.Basic
Nonneg.instArchimedean : ∀ {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [inst_2 : IsOrderedAddMonoid M] [Archimedean M],
  Archimedean { x // 0 ≤ x }
-- Mathlib.Algebra.Module.Defs
/-- Scalar multiplication by zero gives zero.  -/
Module.zero_smul : ∀ {R : Type u} {M : Type v} {inst : Semiring R} {inst_1 : AddCommMonoid M} [self : Module R M] (x : M), 0 • x = 0
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.isValid : Nat.Internal.Linear.PolyCnstr → Bool
-- Init.Data.UInt.Bitwise
UInt64.toNat_not : ∀ (a : UInt64), (~~~a).toNat = UInt64.size - 1 - a.toNat
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_subset_self : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {C : Set X}, (Convexity.convexHull R) C ⊆ C ↔ Convexity.IsConvexSet R C
-- Lean.Meta.Tactic.Grind.Util
/-- Adds `reducePreMatchCond` to `s`  -/
Lean.Meta.Grind.addPreMatchCondSimproc : Lean.Meta.Simprocs → Lean.CoreM Lean.Meta.Simprocs
-- Std.Http.Server.Handler
/-- Called when a request includes an `Expect: 100-continue` header. Return `true` to send a
`100 Continue` response and accept the body. If `false` is returned the server sends
`417 Expectation Failed`, disables keep-alive, and closes the request body reader.
This function is guarded by `Config.lingeringTimeout` and may be cancelled on server shutdown.
The default implementation always returns `true`.
 -/
Std.Http.Server.Handler.onContinue : {σ : Type} → [self : Std.Http.Server.Handler σ] → σ → Std.Http.Request.Head → Std.Async.Async Bool
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeft_obj_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeft R l).obj X).left = X.left
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- the coherence condition for the right square  -/
CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
      (CategoryTheory.Functor.whiskerRight self.right G') =
    CategoryTheory.CategoryStruct.comp (G.whiskerLeft self.base)
      (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom
-- Init.Data.Option.Lemmas
Option.some_beq_none : ∀ {α : Type u_1} [inst : BEq α] (a : α), (some a == none) = false
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_natCast_eq_lift : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.aleph ↑n = Cardinal.lift.{v, u} c ↔ Cardinal.aleph ↑n = c
-- Mathlib.RingTheory.FiniteType
/-- An element of `R[M]` is in the subalgebra generated by its support.  -/
AddMonoidAlgebra.mem_adjoin_support : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddMonoid M] (f : AddMonoidAlgebra R M),
  f ∈ Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ↑f.coeff.support)
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasStrictFDerivAt.continuousAlternatingMap_apply_const : ∀ {𝕜 : 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] {x : E} {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G}
  {c' : E →L[𝕜] F [⋀^ι]→L[𝕜] G} [inst_7 : Fintype ι],
  HasStrictFDerivAt c c' x → ∀ (u : ι → F), HasStrictFDerivAt (fun x => (c x) u) (c'.flipAlternating u) x
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.toEquiv_sigmaProdDistrib : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] {ι : Type u_7} {X : ι → Type u_8}
  [inst_1 : (i : ι) → TopologicalSpace (X i)], Homeomorph.sigmaProdDistrib.toEquiv = Equiv.sigmaProdDistrib X Y
-- Aesop.RuleTac.RuleTerm
Aesop.instInhabitedRuleTerm.default : Aesop.RuleTerm
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Quotient.linearMap_ext_iff : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {f f' : relations.Quotient →ₗ[A] M},
  f = f' ↔ ∀ (g : relations.G), f (relations.toQuotient fun₀ | g => 1) = f' (relations.toQuotient fun₀ | g => 1)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getToIntId? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.Data.ENNReal.Basic
ENNReal.instTop : Top ENNReal
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.div_const : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {𝕜 : Type u_8} {f : ℝ → 𝕜} [inst : NormedDivisionRing 𝕜],
  IntervalIntegrable f μ a b → ∀ (c : 𝕜), IntervalIntegrable (fun x => f x / c) μ a b
-- Mathlib.Analysis.Fourier.Notation
FourierInvModule.fourierInv_smul : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} [inst : Add E] [inst_1 : Add F] [inst_2 : SMul R E]
  [inst_3 : SMul R F] (self : FourierInvModule R E F) (r : R) (f : E),
  FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.sq_apply : ∀ {R : Type u_3} {A : Type u_7} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] (a : A), QuadraticMap.sq a = a * a
-- Std.Sat.AIG.CachedLemmas
/-- If we find a cached atom declaration in the AIG, denoting it is equivalent to denoting `AIG.mkAtom`.
 -/
Std.Sat.AIG.denote_mkAtom_cached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {v : α} {assign : α → Bool} {aig : Std.Sat.AIG α}
  {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.atom v)},
  aig.cache.get? (Std.Sat.AIG.Decl.atom v) = some hit →
    ⟦assign, { aig := aig, ref := { gate := hit.idx, invert := false, hgate := ⋯ } }⟧ = ⟦assign, aig.mkAtom v⟧
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.dist_iConvexComb_right_le : ∀ {I : Type u_1} {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X]
  (x : X) (f : Convexity.StdSimplex ℝ I) (g : I → X),
  dist x (Convexity.iConvexComb f g) ≤ Convexity.iConvexComb f fun i => dist x (g i)
-- Mathlib.Data.List.Cycle
List.prev.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] (l l_1 : List α) (e_l : l = l_1) (x x_1 : α) (e_x : x = x_1) (a : x ∈ l),
  l.prev x a = l_1.prev x_1 ⋯
-- Std.Http.Protocol.H1.Event
/-- Events emitted during HTTP message processing.
 -/
Std.Http.Protocol.H1.Event : Std.Http.Protocol.H1.Direction → Type
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Zipper α β → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : Std.DTreeMap.Internal.Zipper α β)
  (h_1 : (it : Std.DTreeMap.Internal.Zipper α β) → motive Std.DTreeMap.Internal.Impl.leaf it)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (it : Std.DTreeMap.Internal.Zipper α β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) it)
  (it : Std.DTreeMap.Internal.Zipper α β),
  x = Std.DTreeMap.Internal.Impl.leaf →
    x_1 = it →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.leaf, it => h_1 it
        | Std.DTreeMap.Internal.Impl.inner size k v l r, it => h_2 size k v l r it) ≍
        h_1 it
-- Std.Tactic.Do.Syntax
/-- `mreplace` is like `replace`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ
  mexact HPQ
```
 -/
Lean.Parser.Tactic.mreplace : Lean.ParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.coe_freeObj : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] (X : TopCat),
  ↑(TopModuleCat.freeObj R X).toModuleCat = (↑X →₀ R)
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.lift.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] {C : Sort u_9}
  (ih ih_1 : (i : ι) → F i → C) (e_ih : ih = ih_1)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)) (z z_1 : DirectLimit F f),
  z = z_1 → DirectLimit.lift f ih compat z = DirectLimit.lift f ih_1 ⋯ z_1
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G)
  [CategoryTheory.Monad.PreservesColimitOfIsReflexivePair G] (X : adj.toMonad.Algebra),
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (F.map X.a) (adj.counit.app (F.obj X.A))) G
-- Mathlib.ModelTheory.DirectLimit
/-- The isomorphism between limits of isomorphic systems.  -/
FirstOrder.Language.DirectLimit.equiv_lift : (L : FirstOrder.Language) →
  (ι : Type v) →
    [inst : Preorder ι] →
      (G : ι → Type w) →
        [inst_1 : (i : ι) → L.Structure (G i)] →
          (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) →
            [inst_2 : IsDirectedOrder ι] →
              [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] →
                [inst_4 : Nonempty ι] →
                  (G' : ι → Type w') →
                    [inst_5 : (i : ι) → L.Structure (G' i)] →
                      (f' : (i j : ι) → i ≤ j → L.Embedding (G' i) (G' j)) →
                        (g : (i : ι) → L.Equiv (G i) (G' i)) →
                          [inst_6 : DirectedSystem G' fun i j h => ⇑(f' i j h)] →
                            (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)) →
                              L.Equiv (FirstOrder.Language.DirectLimit G f) (FirstOrder.Language.DirectLimit G' f')
-- Mathlib.Algebra.BigOperators.Finprod
finprod_def : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) [inst_1 : Decidable (Function.HasFiniteMulSupport f)],
  ∏ᶠ (i : α), f i = if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset h, f i else 1
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.isPrincipal_iff_exists_isGreatest : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ {I : Ideal O}, Submodule.IsPrincipal I ↔ ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- A `p`-th root of unity that is not `1`, with `p` prime, is a primitive `p`-th root of unity.  -/
mem_primitiveRoots_of_mem_nthRootsFinset : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ},
  Nat.Prime p → ∀ {η : R}, η ∈ Polynomial.nthRootsFinset p 1 → η ≠ 1 → η ∈ primitiveRoots p R
-- Mathlib.CategoryTheory.MarkovCategory.Basic
/-- Copy-discard category where discard is natural.  -/
CategoryTheory.MarkovCategory : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- the pushout  -/
CategoryTheory.Functor.PushoutObjObj.pt : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {X₁ Y₁ : C₁} → {f₁ : X₁ ⟶ Y₁} → {X₂ Y₂ : C₂} → {f₂ : X₂ ⟶ Y₂} → F.PushoutObjObj f₁ f₂ → C₃
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Finite.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [inst : Std.Iterator α m β] → Std.IterM m β → Std.IterM.TerminationMeasures.Finite α m
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation.sum_le : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s : Set X} (hs : MeasurableSet s)
  (P : Finpartition ⟨s, hs⟩), ∑ p ∈ P.parts, f ↑p ≤ MeasureTheory.preVariationFun f s