mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instAddGroup : {R : Type u_3} → {A : Type u_4} → [AddGroup R] → [AddGroup A] → AddGroup (Unitization R A)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.union_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₃.WF → t₂.Equiv t₃ → (t₁ ∪ t₂).Equiv (t₁ ∪ t₃)
-- Mathlib.Order.Antichain
setOfPred_maximal_antichain : ∀ {α : Type u_1} [inst : PartialOrder α] (P : α → Prop), IsAntichain (fun x1 x2 => x1 ≤ x2) {x | Maximal P x}
-- Mathlib.Topology.Constructions.SumProd
prod_mem_nhds_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y} {x : X}
  {y : Y}, s ×ˢ t ∈ nhds (x, y) ↔ s ∈ nhds x ∧ t ∈ nhds y
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.InnerFibration.mem : ∀ {X Y : SSet} {q : X ⟶ Y} [self : SSet.InnerFibration q], SSet.innerFibrations q
-- Mathlib.Logic.Basic
fact_iff : ∀ {p : Prop}, Fact p ↔ p
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.mkSuggestion : Lean.Syntax → Lean.MessageData → Array (String × Option String × Option String) → Lean.Doc.DocM Lean.MessageData
-- Mathlib.Algebra.Ring.Defs
CommRing.toNonUnitalCommRing : {α : Type u} → [s : CommRing α] → NonUnitalCommRing α
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instMonoid : {α : Type u_1} → [Monoid α] → Monoid αᵒᵈ
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getKeyD : {α : Type u} → {β : α → Type v} → [BEq α] → α → List ((a : α) × β a) → α → α
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isPrime : ∀ (R : Type u_1) [inst : CommSemiring R] [Ring.KrullDimLE 0 R], minimalPrimes R = {I | I.IsPrime}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Real.sin` is real analytic.  -/
Real.analyticOn_sin : ∀ {s : Set ℝ}, AnalyticOn ℝ Real.sin s
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.foldM_mapM : ∀ {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [LawfulMonad o] [inst_8 : Std.IteratorLoop α Id n] [inst_9 : Std.IteratorLoop α Id o]
  [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o] [inst_12 : MonadLiftT n o] [LawfulMonadLiftT n o]
  {f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : Std.Iter β},
  Std.IterM.foldM g init (Std.Iter.mapM f it) =
    Std.Iter.foldM
      (fun d b => do
        let c ← liftM (f b)
        g d c)
      init it
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_inter_coloops_eq : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.closure X ∩ M.coloops = X ∩ M.coloops
-- Mathlib.Algebra.Group.Action.Pi
Pi.addAction.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_4} (M : Type u_7) {m : AddMonoid M} [inst : (i : ι) → AddAction M (α i)],
  Pi.addAction M = { toVAdd := Pi.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.max!.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (x : α) → motive (some x)),
  (match none with
    | none => h_1 ()
    | some x => h_2 x) =
    h_1 ()
-- Mathlib.Algebra.Order.Interval.Basic
Interval.subtractionCommMonoid : {α : Type u} →
  [inst : AddCommGroup α] → [inst_1 : PartialOrder α] → [IsOrderedAddMonoid α] → SubtractionCommMonoid (Interval α)
-- Mathlib.RingTheory.Etale.QuasiFinite
Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂ : ∀ {R : Type u_2} {S : Type u_3} {R' : Type u_4} {R'' : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [Algebra.FiniteType R S] [inst_4 : CommRing R'] [inst_5 : Algebra R R'] [inst_6 : CommRing R'']
  [inst_7 : Algebra R R''] [inst_8 : Algebra R'' S] [Algebra.IsIntegral R R''] [inst_10 : IsScalarTower R R'' S]
  (q : Ideal S) (P : Ideal R') [P.IsPrime] (e : TensorProduct R R' S) (e₀ : TensorProduct R R' R''),
  IsIdempotentElem e₀ →
    (Algebra.TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e →
      ∀ (P' : Ideal (TensorProduct R R' S)),
        Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = q →
          (∀ (P'' : Ideal (TensorProduct R R' R'')),
              P''.IsPrime →
                P''.LiesOver P →
                  e₀ ∉ P'' →
                    P'' =
                      Ideal.comap
                        (Algebra.TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P') →
            ∀ (g : R''),
              (algebraMap R'' S) g ∉ q →
                Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g) →
                  ∃ f ∉ P,
                    Module.Finite (Localization.Away f)
                      (Localization.Away
                        ((Algebra.TensorProduct.map (Algebra.ofId R' (Localization.Away f)) (AlgHom.id R S)) e))
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_eq_top : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {S : Subsemiring Rᵐᵒᵖ}, S.unop = ⊤ ↔ S = ⊤
-- Mathlib.RingTheory.Radical.NatInt
Int.radical_pos : ∀ (z : ℤ), 0 < UniqueFactorizationMonoid.radical z
-- Batteries.Tactic.Alias
/-- An alias can be in one of three forms  -/
Batteries.Tactic.Alias.AliasInfo : Type
-- Mathlib.Order.Filter.Extr
isMinOn_const : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsMinOn (fun x => b) s a
-- Mathlib.Data.List.Lookmap
_private.Mathlib.Data.List.Lookmap.0.List.lookmap.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (b : α) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.NumberTheory.SmoothNumbers
/-- The sets of `s`-factored and of `s ∪ {N}`-factored numbers are the same when `N` is not prime.
See `Nat.equivProdNatFactoredNumbers` for when `N` is prime.  -/
Nat.factoredNumbers_insert : ∀ (s : Finset ℕ) {N : ℕ}, ¬Nat.Prime N → Nat.factoredNumbers (insert N s) = Nat.factoredNumbers s
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueSums.of_addHom : ∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H] (f : H →ₙ+ G),
  (∀ ⦃a b c d : H⦄, a + b = c + d → f a = f c ∧ f b = f d → a = c ∧ b = d) → ∀ [TwoUniqueSums G], TwoUniqueSums H
-- Mathlib.Order.Category.BddLat
BddLat.hasForgetToSemilatInf : CategoryTheory.HasForget₂ BddLat SemilatInfCat
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l →
        k ∈ l → (Std.DHashMap.Const.insertManyIfNewUnit m l).getKey! k' = k
-- Mathlib.CategoryTheory.Adjunction.Parametrized
/-- The bijection `((F.obj X₁).obj X₂ ⟶ X₃) ≃ (X₂ ⟶ (G.obj (op X₁)).obj X₃)`
given by an adjunction with a parameter `adj₂ : F ⊣₂ G`.  -/
CategoryTheory.ParametrizedAdjunction.homEquiv : {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₃)} →
              {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
                (F ⊣₂ G) →
                  {X₁ : C₁} → {X₂ : C₂} → {X₃ : C₃} → ((F.obj X₁).obj X₂ ⟶ X₃) ≃ (X₂ ⟶ (G.obj (Opposite.op X₁)).obj X₃)
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Expression of `bilinearIteratedFDerivWithinTwo` in terms of `iteratedFDerivWithin`.
 -/
bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv : ∀ {𝕜 : 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] {e : E}
  {s : Set E} (f : E → F),
  UniqueDiffOn 𝕜 s →
    e ∈ s →
      ∀ (e₁ e₂ : E), ((bilinearIteratedFDerivWithinTwo 𝕜 f s e) e₁) e₂ = (iteratedFDerivWithin 𝕜 2 f s e) ![e₁, e₂]
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_inter_self : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω},
  s.Finite → (ProbabilityTheory.uniformOn s) (s ∩ t) = (ProbabilityTheory.uniformOn s) t
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.removeNumLeadingSpaces.consumeSpaces.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.restrict_Ioi_eq_restrict_Ici : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a : α}, μ.restrict (Set.Ioi a) = μ.restrict (Set.Ici a)
-- Lean.EnvExtension
Lean.instInhabitedMapDeclarationExtension.default : {α : Type} → Lean.MapDeclarationExtension α
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_le_ker_dual : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  (b : Module.Basis (Fin n) R M) (k : Fin n), b.flag k.castSucc ≤ LinearMap.ker (b.dualBasis k)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommMonoidWithZero.toIsBotZeroClass : ∀ {α : Type u_3} [self : LinearOrderedCommMonoidWithZero α], IsBotZeroClass α
-- Mathlib.Topology.Separation.CompletelyRegular
unitInterval.eq_1 : unitInterval = Set.Icc 0 1
-- Mathlib.RepresentationTheory.Rep.Res
Rep.res_obj_V : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G)
  (M : Rep.{u_1, u, v1} k G), ↑(Rep.res f M) = ↑M
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal : {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → NatCast (SlashInvariantForm Γ 0)
-- Lean.Elab.Term.TermElabM
/-- Fixed term elaborators for supporting `elabToSyntax`.
 -/
Lean.Elab.Term.Context.fixedTermElabs : Lean.Elab.Term.Context → Array Lean.Elab.Term.FixedTermElabRef
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toStructuredArrow_comp_toUnder_comp_forget : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F),
  c.toStructuredArrow.comp ((CategoryTheory.StructuredArrow.toUnder c.pt F).comp (CategoryTheory.Under.forget c.pt)) = F
-- Mathlib.Data.Fintype.EquivFin
Equiv.ofLeftInverseOfCardLE_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (hβα : Fintype.card β ≤ Fintype.card α)
  (f : α → β) (g : β → α) (h : Function.LeftInverse g f) (a : α), (Equiv.ofLeftInverseOfCardLE hβα f g h) a = f a
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.instRespectsIsoScheme : ∀ {W P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [W.IsStableUnderBaseChange]
  [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving W] [P.RespectsIso],
  (AlgebraicGeometry.sourceLocalClosure W P).RespectsIso
-- Mathlib.Condensed.TopCatAdjunction
/-- The functor from topological spaces to condensed sets restricted to compactly generated spaces
is fully faithful.
 -/
CondensedSet.fullyFaithfulCompactlyGeneratedToCondensedSet : CondensedSet.compactlyGeneratedToCondensedSet.FullyFaithful
-- Std.Do.Internal.Ensures.Lemmas
/-- Weaken an `Ensures`-witness via predicate implication.  -/
Std.Do.Internal.Ensures.weaken : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {α : Type u} {P Q : α → Prop} {x : m α},
  Std.Do.Internal.Ensures P x → (∀ (a : α), P a → Q a) → Std.Do.Internal.Ensures Q x
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment.eq_3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.addNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- `f` is a mono if the pullback cone `(𝟙 X, 𝟙 X)` is a limit for the pair `(f, f)`. The converse is
given in `PullbackCone.is_id_of_mono`.
 -/
CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  (t :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)
        ⋯)),
  CategoryTheory.Mono f
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSets_zero_left : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure α}
  {s1 s2 : Set (Set Ω)}, ProbabilityTheory.Kernel.IndepSets s1 s2 0 μ
-- Lean.Parser.Syntax
Lean.Parser.Command.mixfix.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.WithBot
WithBot.not_lt_bot : ∀ {α : Type u_1} [inst : LT α] (a : WithBot α), ¬a < ⊥
-- Mathlib.RingTheory.Polynomial.Basic
/-- Given a polynomial, return the polynomial whose coefficients are in
the ring closure of the original coefficients.  -/
Polynomial.restriction : {R : Type u} → [inst : Ring R] → (p : Polynomial R) → Polynomial ↥(Subring.closure ↑p.coeffs)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.of_tendsto_div_atTop : ∀ {α : Type u_1} {𝕜 : Type u_17} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜}, Filter.Tendsto (fun x => g x / f x) l Filter.atTop → f =o[l] g
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Functor.coconeTypesEquiv_apply_ι_app : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) (c : F.CoconeTypes)
  (j : J), (F.coconeTypesEquiv c).ι.app j = TypeCat.ofHom (c.ι j)
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.instInhabitedOfSigmaCompactSpaceOfWeaklyLocallyCompactSpace : {X : Type u_1} →
  [inst : TopologicalSpace X] → [SigmaCompactSpace X] → [WeaklyLocallyCompactSpace X] → Inhabited (CompactExhaustion X)
-- Mathlib.Data.List.Rotate
List.map_rotate : ∀ {α : Type u} {β : Type u_1} (f : α → β) (l : List α) (n : ℕ), List.map f (l.rotate n) = (List.map f l).rotate n
-- Mathlib.Algebra.Group.Prod
AddHom.prod_unique : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : M →ₙ+ N × P),
  ((AddHom.fst N P).comp f).prod ((AddHom.snd N P).comp f) = f
-- Mathlib.FieldTheory.Normal.Defs
IsScalarTower.AlgEquiv.restrictNormalHom_comp_apply : ∀ (K₁ : Type u_6) (K₂ : Type u_7) {F : Type u_8} {K₃ : Type u_9} [inst : Field F] [inst_1 : Field K₁]
  [inst_2 : Field K₂] [inst_3 : Field K₃] [inst_4 : Algebra F K₁] [inst_5 : Algebra F K₂] [inst_6 : Algebra F K₃]
  [inst_7 : Algebra K₁ K₂] [inst_8 : Algebra K₁ K₃] [inst_9 : Algebra K₂ K₃] [inst_10 : IsScalarTower F K₁ K₃]
  [inst_11 : IsScalarTower F K₁ K₂] [inst_12 : IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃] [inst_14 : Normal F K₁]
  [inst_15 : Normal F K₂] (f : Gal(K₃/F)),
  (AlgEquiv.restrictNormalHom K₁) f = (AlgEquiv.restrictNormalHom K₁) ((AlgEquiv.restrictNormalHom K₂) f)
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.instTransOrd : ∀ {rel : ℤ → ℤ → Prop} {n m : ℤ}, Std.TransOrd (Std.Time.Internal.Bounded rel n m)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryingEquiv_symm_apply_map_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (G : CategoryTheory.Functor (C × D) E) {X Y : C}
  (f : X ⟶ Y) (Y_1 : D),
  ((CategoryTheory.Functor.curryingEquiv.symm G).map f).app Y_1 =
    G.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y_1))
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- The `withOverApp` combinator allows delaborators to handle "over-application" by using the core
application delaborator to handle additional arguments.

For example, suppose `f : {A : Type} → Foo A → A` and we want to implement a delaborator for
applications `f x` to pretty print as `F[x]`. Because `A` is a type variable we might encounter
a term of the form `@f (A → B) x y`, which has an additional argument `y`.
With this combinator one can use an arity-2 delaborator to pretty print this as `F[x] y`.

* `arity`: the expected number of arguments to `f`.
  The combinator will fail if fewer than this number of arguments are passed,
  and if more than this number of arguments are passed the arguments are handled using
  the standard application delaborator.
* `x`: delaborates the head application of the expected arity (`f x` in the example).
  The value of `pp.tagAppFns` for the whole application is propagated to the expression that `x` sees.

In the event of overapplication, the delaborator `x` is wrapped in
`Lean.PrettyPrinter.Delaborator.withAnnotateTermInfo` to register `TermInfo` for the resulting term.
The effect of this is that the term is hoverable in the Infoview.

If the application would require inserting `@` around the result of `x`, the delaborator fails
since we cannot be sure that this insertion will be well-formed.
 -/
Lean.PrettyPrinter.Delaborator.withOverApp : ℕ → Lean.PrettyPrinter.Delaborator.Delab → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : TopologicalSpace α} {inst_1 : TopologicalSpace β} {toContinuousMap : C(α, β)}
  {map_open' : IsOpenMap toContinuousMap.toFun} {toContinuousMap_1 : C(α, β)}
  {map_open'_1 : IsOpenMap toContinuousMap_1.toFun},
  { toContinuousMap := toContinuousMap, map_open' := map_open' } =
      { toContinuousMap := toContinuousMap_1, map_open' := map_open'_1 } →
    toContinuousMap = toContinuousMap_1
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- Create the application `.app f a`, inserting some casts if necessary.  -/
_private.Mathlib.Tactic.Translate.UnfoldBoundary.0.Mathlib.Tactic.UnfoldBoundary.mkAppWithCast : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.Expr → Lean.Expr → Lean.Meta.SimpM Lean.Expr
-- Mathlib.Data.Nat.Bits
/-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2`  -/
Nat.div2 : ℕ → ℕ
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.maxLevels : Array Lean.Expr → Lean.MetaM Lean.Level
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take_of_length_le : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
-- Lean.Language.Basic
Lean.Language.TransformedSnap.mk.inj : ∀ {α : Type} {raw : α} {transform : Lean.Language.SnapshotTreeTransform} {raw_1 : α}
  {transform_1 : Lean.Language.SnapshotTreeTransform},
  { raw := raw, transform := transform } = { raw := raw_1, transform := transform_1 } →
    raw = raw_1 ∧ transform = transform_1
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldRev.match_1.eq_1 : ∀
  (motive :
    (n : ℕ) →
      {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldRev._auto_1 → Type u_1} →
        ((i : ℕ) → (h : i < n) → α (i + 1) ⋯ → α i ⋯) → α n ⋯ → Sort u_2)
  (α : (i : ℕ) → autoParam (i ≤ 0) Nat.dfoldRev._auto_1 → Type u_1) (f : (i : ℕ) → (h : i < 0) → α (i + 1) ⋯ → α i ⋯)
  (init : α 0 ⋯)
  (h_1 :
    (α : (i : ℕ) → autoParam (i ≤ 0) Nat.dfoldRev._auto_1 → Type u_1) →
      (f : (i : ℕ) → (h : i < 0) → α (i + 1) ⋯ → α i ⋯) → (init : α 0 ⋯) → motive 0 f init)
  (h_2 :
    (n : ℕ) →
      (α : (i : ℕ) → autoParam (i ≤ n + 1) Nat.dfoldRev._auto_1 → Type u_1) →
        (f : (i : ℕ) → (h : i < n + 1) → α (i + 1) ⋯ → α i ⋯) → (init : α (n + 1) ⋯) → motive n.succ f init),
  (match 0, α, f, init with
    | 0, α, f, init => h_1 α f init
    | n.succ, α, f, init => h_2 n α f init) =
    h_1 α f init
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        {w : ℕ} →
          (aig : Std.Sat.AIG α) →
            ℕ →
              ℕ →
                aig.RefVec w →
                  aig.RefVec w →
                    old.decls.size ≤ aig.decls.size →
                      Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput old w
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_symm_apply_coe : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [inst : AlgebraicGeometry.GeometricallyIrreducible f] (hf : IsOpenMap ⇑f)
  (a : ↑(irreducibleComponents ↥S)),
  ↑((AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv f hf).symm a) = ⇑f ⁻¹' ↑a
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.trivial_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.CommGrp.trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Logic.Function.Basic
Function.comp_surjInv : ∀ {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Surjective f), f ∘ Function.surjInv hf = id
-- Init.Data.List.TakeDrop
List.head?_takeWhile : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.takeWhile p l).head? = Option.filter p l.head?
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- A topological additive group that has a `ContinuousAddEquiv` to a
profinite additive group is profinite.  -/
ProfiniteAddGrp.ofContinuousAddEquiv : {G : ProfiniteAddGrp.{u}} →
  {H : Type v} →
    [inst : TopologicalSpace H] →
      [inst_1 : AddGroup H] → [IsTopologicalAddGroup H] → ↑G.toProfinite.toTop ≃ₜ+ H → ProfiniteAddGrp.{v}
-- Mathlib.Data.EReal.Inv
EReal.abs_def : ∀ (x : ℝ), (↑x).abs = ENNReal.ofReal |x|
-- Mathlib.Algebra.GroupWithZero.Defs
mul_ne_zero_iff_left : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → (a * b ≠ 0 ↔ b ≠ 0)
-- Lean.Parser.Do
Lean.Parser.Term.doLetRec.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
OrthonormalBasis.tensorProduct_repr_tmul_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {ι₁ : Type u_6}
  {ι₂ : Type u_7} [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E)
  (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : E) (y : F) (i : ι₁) (j : ι₂),
  ((b₁.tensorProduct b₂).repr (x ⊗ₜ[𝕜] y)).ofLp (i, j) = (b₂.repr y).ofLp j * (b₁.repr x).ofLp i
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (X : C) → [mon : CategoryTheory.MonObj X] → CategoryTheory.Mon C
-- Mathlib.Algebra.Module.LinearMap.End
/-- Applying a linear map at `v : M`, seen as `S`-linear map from `M →ₗ[R] M₂` to `M₂`.

See `LinearMap.applyₗ` for a version where `S = R`.  -/
LinearMap.applyₗ' : {R : Type u_1} →
  (S : Type u_3) →
    {M : Type u_4} →
      {M₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module S M₂] → [inst_7 : SMulCommClass R S M₂] → M →+ (M →ₗ[R] M₂) →ₗ[S] M₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cosh θ` to the
value `sinh ((n + 1) * θ) / sinh θ`.  -/
Polynomial.Chebyshev.U_real_cosh : ∀ (θ : ℝ) (n : ℤ), Polynomial.eval (Real.cosh θ) (Polynomial.Chebyshev.U ℝ n) * Real.sinh θ = Real.sinh ((↑n + 1) * θ)