mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- `arsinh` is the left inverse of `sinh`.  -/
Real.arsinh_sinh : ∀ (x : ℝ), Real.arsinh (Real.sinh x) = x
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_mul_C_leadingCoeff : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R),
  p.integralNormalization * Polynomial.C p.leadingCoeff = p.scaleRoots p.leadingCoeff
-- Init.Control.ExceptCps
ExceptCpsT.run_throw : ∀ {m : Type u_1 → Type u_2} {ε β : Type u_1} {e : ε} [inst : Monad m], (throw e).run = pure (Except.error e)
-- Mathlib.CategoryTheory.Join.Pseudofunctor
_private.Mathlib.CategoryTheory.Join.Pseudofunctor.0.CategoryTheory.Join.id.match_1.eq_2 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] (motive : CategoryTheory.Join C D → Sort u_5) (x : D)
  (h_1 : (x : C) → motive (CategoryTheory.Join.left x)) (h_2 : (x : D) → motive (CategoryTheory.Join.right x)),
  (match CategoryTheory.Join.right x with
    | CategoryTheory.Join.left x => h_1 x
    | CategoryTheory.Join.right x => h_2 x) =
    h_2 x
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point.  -/
ContDiffAt.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {E' : Type u_3} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {F' : Type u_4}
  [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] {f : E → F} {g : E' → F'} {x : E} {y : E'},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g y → ContDiffAt 𝕜 n (Prod.map f g) (x, y)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_lt_of_lt_one_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosStrictMono α],
  0 < b → a < 1 → a * b < b
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.failure? : Lean.Meta.Grind.Result → Option Lean.Meta.Grind.Goal
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
fderivWithin_ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E},
  DifferentiableWithinAt ℂ f s x →
    UniqueDiffWithinAt ℂ s x →
      fderivWithin ℂ (fun x => Complex.cosh (f x)) s x = Complex.sinh (f x) • fderivWithin ℂ f s x
-- Mathlib.Data.Sym.Sym2
Sym2.congr_left : ∀ {α : Type u_1} {a b c : α}, s(b, a) = s(c, a) ↔ b = c
-- Mathlib.NumberTheory.Bertrand
/-- Proves that **Bertrand's postulate** holds for all sufficiently large `n`.
 -/
Nat.exists_prime_lt_and_le_two_mul_eventually : ∀ (n : ℕ), 512 ≤ n → ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
-- Init.Data.UInt.Bitwise
UInt32.toUInt16_shiftLeft_mod : ∀ (a b : UInt32), (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.integralAgainstBilinCLM_eq_integral : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : SMulCommClass ℝ 𝕜 F₁]
  [inst_12 : NormedSpace ℝ F₃] [inst_13 : SMulCommClass ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂},
  MeasureTheory.IntegrableOn φ (↑K) μ →
    ∀ {f : ContDiffMapSupportedIn E F₁ n K},
      (ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ) f = ∫ (x : E), (B (f x)) (φ x) ∂μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_minKey?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.minKey?.isSome = !t.isEmpty
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_const_mul_right_iff' : ∀ {α : Type u_1} {E : Type u_3} {R : Type u_13} [inst : Norm E] [inst_1 : SeminormedRing R] {f : α → E} {l : Filter α}
  {g : α → R} {c : R}, IsUnit c → ((f =O[l] fun x => c * g x) ↔ f =O[l] g)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.transIsLittleOEventuallyEq : {α : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : Norm E] →
        [inst_1 : Norm F] →
          {l : Filter α} → Trans (fun x1 x2 => x1 =o[l] x2) (fun x1 x2 => x1 =ᶠ[l] x2) fun x1 x2 => x1 =o[l] x2
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
/-- The binary bicone associated to the biproduct of functors `F` and `G`  -/
CategoryTheory.Limits.pointwiseBinaryBicone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] →
        {D : Type u_2} →
          [inst_3 : CategoryTheory.Category.{v_2, u_2} D] →
            (F G : CategoryTheory.Functor D C) → CategoryTheory.Limits.BinaryBicone F G
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.getToIntId?.toIntInterval? : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.coe_copy : ∀ {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsLocallyArtinian.mk : ∀ {X : AlgebraicGeometry.Scheme},
  autoParam (∀ (U : ↑X.affineOpens), IsArtinianRing ↑(X.presheaf.obj (Opposite.op ↑U)))
      AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj._autoParam →
    AlgebraicGeometry.IsLocallyArtinian X
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator : Type
-- Mathlib.FieldTheory.AbelRuffini
gal_prod_isSolvable : ∀ {F : Type u_1} [inst : Field F] {s : Multiset (Polynomial F)},
  (∀ p ∈ s, Group.IsSolvable p.Gal) → Group.IsSolvable s.prod.Gal
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.writes.eq_def : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Fintype Γ] (x : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.writes x =
    match x with
    | Turing.TM1.Stmt.move a q => Turing.TM1to1.writes q
    | Turing.TM1.Stmt.write a q =>
      Finset.image (fun a => Turing.TM1to1.Λ'.write a q) Finset.univ ∪ Turing.TM1to1.writes q
    | Turing.TM1.Stmt.load a q => Turing.TM1to1.writes q
    | Turing.TM1.Stmt.branch a q₁ q₂ => Turing.TM1to1.writes q₁ ∪ Turing.TM1to1.writes q₂
    | Turing.TM1.Stmt.goto a => ∅
    | Turing.TM1.Stmt.halt => ∅
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.iInter_Iic_rat : ⋂ r, Set.Iic ↑r = ∅
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.val_equivUnitsAffineMap_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁), ↑(AffineEquiv.equivUnitsAffineMap e) = ↑e
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_comp_pow : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [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]
  [ContinuousMap.UniqueHom R A] (f : R → R) (n : ℕ) (a : A),
  autoParam (ContinuousOn f ((fun x => x ^ n) '' spectrum R a)) cfc_comp_pow._auto_1 →
    autoParam (p a) cfc_comp_pow._auto_3 → cfc (fun x => f (x ^ n)) a = cfc f (a ^ n)
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.instSetLike : (R : Type u_1) → [inst : Ring R] → SetLike (RingCone R) R
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.hom_comp : ∀ {X Y Z : FinBddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z),
  FinBddDistLat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) =
    (FinBddDistLat.Hom.hom g).comp (FinBddDistLat.Hom.hom f)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpenToSpec.eq_1 : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A),
  AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen 𝒜 f).toSpecΓ
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Proj.awayToSection 𝒜 f))
-- Mathlib.Order.SuccPred.CompleteLinearOrder
iSup_succ : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] [inst_1 : SuccOrder α] (x : α), ⨆ a, Order.succ ↑a = x
-- Mathlib.Topology.Sets.VietorisTopology
/-- Given a basis `B` on a topological space `α`, the topology of `NonemptyCompacts α` has a basis
consisting of sets of the form `{K | K ⊆ U₁ ∪ … ∪ Uₙ, K ∩ U₁ ≠ ∅, …, K ∩ Uₙ ≠ ∅}`, where
`U₁, …, Uₙ ∈ B` and `n > 0`.  -/
TopologicalSpace.IsTopologicalBasis.nonemptyCompacts : ∀ {α : Type u_1} [inst : TopologicalSpace α] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B →
    TopologicalSpace.IsTopologicalBasis
      ((fun u => {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.comp_homeomorph : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X},
  IsEvenlyCovered f x I → ∀ {E' : Type u_4} [inst_3 : TopologicalSpace E'] (g : E' ≃ₜ E), IsEvenlyCovered (f ∘ ⇑g) x I
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.comp : Turing.ToPartrec.Code → Turing.ToPartrec.Code → Turing.ToPartrec.Code
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_monadMap_OptionT_apply_eq : ∀ {Pred : Type u} {EPred : Type u_1} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  (f : {β : Type u} → m β → m β) {α : Type u} (x : OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  Std.Internal.Do.wp (MonadFunctor.monadMap (fun {β} => f) x) post epost =
    Std.Internal.Do.wp (f x.run) (Std.Internal.Do.EPost.Cons.pushOption post epost) epost.tail
-- Batteries.Tactic.HelpCmd
/-- The command `#help term` shows all term syntaxes that have been defined in the current environment.
See `#help cat` for more information.
 -/
Batteries.Tactic.«command#help_Term+____» : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.ExprWithAnchor.mk.injEq : ∀ (e : Lean.Expr) (anchor : UInt64) (e_1 : Lean.Expr) (anchor_1 : UInt64),
  ({ e := e, anchor := anchor } = { e := e_1, anchor := anchor_1 }) = (e = e_1 ∧ anchor = anchor_1)
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom α β), f.toFun = ⇑f
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorObj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [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} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (I₂ : Type u_8) (I₃ : Type u_9) {X₂ Y₂ : CategoryTheory.GradedObject I₂ C₂}
  (φ : X₂ ⟶ Y₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (x : I₁ × I₂ × I₃),
  ((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).map φ).app X₃ x =
    ((F.obj (X₁ x.1)).map (φ x.2.1)).app (X₃ x.2.2)
-- Init.Data.String.Basic
String.Slice.Pos.prevAux.go.congr_simp : ∀ {s s_1 : String.Slice} (e_s : s = s_1) (off off_1 : ℕ) (e_off : off = off_1) (h₁ : off < s.utf8ByteSize),
  String.Slice.Pos.prevAux.go off h₁ = String.Slice.Pos.prevAux.go off_1 ⋯
-- Lean.Util.PPExt
Lean.ppExt : Lean.EnvExtension Lean.PPFns
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α} {h' : k ∈ Std.DTreeMap.Raw.map f t} (h : t.WF),
  (Std.DTreeMap.Raw.map f t).getKey k h' = t.getKey k ⋯
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.insertMany_ind : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {ρ : Type v} [inst : ForIn Id ρ α] [inst_1 : EquivBEq α]
  [inst_2 : LawfulHashable α] {motive : Std.ExtHashSet α → Prop} (m : Std.ExtHashSet α) {l : ρ},
  motive m → (∀ (m : Std.ExtHashSet α) (a : α), motive m → motive (m.insert a)) → motive (m.insertMany l)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.findEntry?_congr : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k₁ k₂ : α} [Std.TransCmp cmp] (t : RBTree.RBMap α β cmp),
  cmp k₁ k₂ = Ordering.eq → t.findEntry? k₁ = t.findEntry? k₂
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.isOpen_extend_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H}, IsOpen (f.extend I).source
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.norm_integral_le_abs_of_norm_le : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} {g : ℝ → ℝ},
  (∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ‖f t‖ ≤ g t) →
    IntervalIntegrable g μ a b → ‖∫ (t : ℝ) in a..b, f t ∂μ‖ ≤ |∫ (t : ℝ) in a..b, g t ∂μ|
-- Mathlib.Data.Nat.Nth
/-- If a predicate `p : ℕ → Prop` is true for infinitely many numbers, then `Nat.count p` and
`Nat.nth p` form a Galois insertion.  -/
Nat.giCountNth : {p : ℕ → Prop} → [inst : DecidablePred p] → (Set.ofPred p).Infinite → GaloisInsertion (Nat.count p) (Nat.nth p)
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.instFunLikeAddContentSet : {α : Type u_1} →
  {C : Set (Set α)} → {G : Type u_2} → [inst : AddCommMonoid G] → FunLike (MeasureTheory.AddContent G C) (Set α) G
-- Mathlib.Topology.UniformSpace.Defs
UniformContinuousOn.eq_1 : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] (f : α → β) (s : Set α),
  UniformContinuousOn f s =
    Filter.Tendsto (fun x => (f x.1, f x.2)) (uniformity α ⊓ Filter.principal (s ×ˢ s)) (uniformity β)
-- Init.Prelude
/-- Extracts the information in the state that should be rolled back if an exception is handled.
 -/
EStateM.Backtrackable.save : {δ : outParam (Type u)} → {σ : Type u} → [self : EStateM.Backtrackable δ σ] → σ → δ
-- Mathlib.Data.TypeVec
/-- `const x α` is an arrow that ignores its source and constructs a `TypeVec` that
contains nothing but `x`  -/
TypeVec.const : {β : Type u_1} → β → {n : ℕ} → (α : TypeVec.{u_2} n) → α.Arrow (TypeVec.repeat n β)
-- Lean.Environment
/-- Sets the extension state to the given value. See `AsyncMode` for details on how modifications from
different environment branches are reconciled.
 -/
Lean.EnvExtension.setState : {σ : Type} →
  (ext : Lean.EnvExtension σ) →
    Lean.Environment → σ → optParam Lean.EnvExtension.AsyncMode ext.asyncMode → Lean.Environment
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The fan constructed of the projections from the product is limiting.  -/
CategoryTheory.Limits.productIsProduct : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f : β → C) →
        [inst_1 : CategoryTheory.Limits.HasProduct f] →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (∏ᶜ f) (CategoryTheory.Limits.Pi.π f))
-- Lean.Server.Utils
/-- Constructs a `textDocument/publishDiagnostics` notification.  -/
Lean.Server.mkPublishDiagnosticsNotification : Lean.Server.DocumentMeta →
  Array Lean.Lsp.Diagnostic → optParam (Option Bool) none → Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams
-- Mathlib.Algebra.Free
FreeAddMagma.lift_of : ∀ {α : Type u} {β : Type v} [inst : Add β] (f : α → β) (x : α), (FreeAddMagma.lift f) (FreeAddMagma.of x) = f x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalAddGroup.tendstoLocallyUniformlyOn_iff : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : AddGroup G] [u : UniformSpace G]
  [inst_1 : IsTopologicalAddGroup G] [inst_2 : TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι)
  (s : Set α),
  IsTopologicalAddGroup.rightUniformSpace G = u →
    (TendstoLocallyUniformlyOn F f p s ↔
      ∀ u_1 ∈ nhds 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u_1)
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Lean.Omega.instAppendString : Append String
-- Std.Internal.Parsec.String
/-- Skip whitespace: tabs, newlines, carriage returns, and spaces.
 -/
Std.Internal.Parsec.String.ws : Std.Internal.Parsec.String.Parser Unit
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- A variant of `app_inv_app` that gives an `eqToHom` instead of `homOfLe`.  -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (U : TopologicalSpace.Opens ↑Y.toTopCat) (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))
  {Z : CommRingCat}
  (h :
    Y.presheaf.obj
        (Opposite.op
          ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj
            ((TopologicalSpace.Opens.map f.base).obj U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U)) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_sum : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α},
  (∀ (i : ℕ), m.IsCaratheodory (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      ∀ {t : Set α} {n : ℕ}, ∑ i ∈ Finset.range n, m (t ∩ s i) = m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabByTactic : Lean.Elab.Term.TermElab
-- Mathlib.Order.Lattice
/-- Transfer `PartialOrder` across an `Equiv`.  -/
Equiv.partialOrder : {α : Type u} → {β : Type v} → α ≃ β → [PartialOrder β] → PartialOrder α
-- Mathlib.Data.Matrix.Diagonal
Matrix.transpose_eq_intCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddGroupWithOne α] {M : Matrix n n α} {d : ℤ},
  M.transpose = ↑d ↔ M = ↑d
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- The function `Complex.exp` is complex analytic.  -/
analyticAt_cexp : ∀ {z : ℂ}, AnalyticAt ℂ Complex.exp z
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_insert_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E) (x : E),
  IntermediateField.adjoin F (insert x ↑(IntermediateField.adjoin F S)) = IntermediateField.adjoin F (insert x S)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.instStarModuleId : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E], StarModule 𝕜 (E →L[𝕜] E)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_inverse_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (c : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C))
  (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.equivComma.inverse.obj c).obj X =
    match X with
    | CategoryTheory.WithTerminal.of x => c.left.obj x
    | CategoryTheory.WithTerminal.star => c.right
-- Mathlib.Algebra.Group.Conj
AddConjClasses.mk_eq_mk_iff_isAddConj : ∀ {α : Type u} [inst : AddMonoid α] {a b : α}, AddConjClasses.mk a = AddConjClasses.mk b ↔ IsAddConj a b
-- Mathlib.FieldTheory.Perfect
not_irreducible_expand : ∀ (R : Type u_2) (p : ℕ) [inst : CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (f : Polynomial R),
  ¬Irreducible ((Polynomial.expand R p) f)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul_subset_nsmul_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α} {m n : ℕ}, 0 ∈ s → m ≤ n → m • s ⊆ n • s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.toAddTorsor : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] →
            [inst_3 : AddTorsor V P] → (s : AffineSubspace k P) → [Nonempty ↥s] → AddTorsor ↥s.direction ↥s
-- Mathlib.Computability.Primrec.List
Primrec.nat_omega_rec : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  (f : α → β → σ) {m : α → β → ℕ} {l : α → β → List β} {g : α → β × List σ → Option σ},
  Primrec₂ m →
    Primrec₂ l →
      Primrec₂ g →
        (∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b) →
          (∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)) → Primrec₂ f
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.mapFunctor_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) (a b : B) {X Y : a ⟶ b} (η : X ⟶ Y), (F.mapFunctor a b).map η = F.map₂ η
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.linearEquiv.congr_simp : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M], Module.Invertible.linearEquiv R M = Module.Invertible.linearEquiv R M
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  (F : CategoryTheory.Functor C (Type w)) {X₁ X₂ : C} (f : X₁ ⟶ X₂) (u : F.Elements),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shrinkYoneda.{w, v₁, u₁}.map f).app (Opposite.op u.fst))
      (TypeCat.ofHom fun t =>
        (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.shrinkYonedaObjObjEquiv t))) u.snd) =
    CategoryTheory.CategoryStruct.comp
      (TypeCat.ofHom fun t =>
        (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.shrinkYonedaObjObjEquiv t))) u.snd)
      (F.map f)
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.right_algebraMap_apply : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (b : B), (algebraMap B (TensorProduct R A B)) b = 1 ⊗ₜ[R] b
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.mulActionHom_of_embedding_surjective : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α],
  Function.Surjective ⇑(Set.powersetCard.mulActionHom_of_embedding G α n)
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.pathELength_eq_lintegral_mfderivWithin_Icc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ : ℝ → M},
  Manifold.pathELength I γ a b = ∫⁻ (t : ℝ) in Set.Icc a b, ‖(mfderiv[Set.Icc a b] γ t) 1‖ₑ