mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Setoid.Basic
Setoid.comap_injective : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.Surjective f → Function.Injective (Setoid.comap f)
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpack_packedNaN : ∀ {spec : Float.Model.Format},
  Float.Model.UnpackedFloat.unpack spec (Float.Model.UnpackedFloat.packedNaN spec) =
    Float.Model.UnpackedFloat.notANumber
-- Batteries.Data.List.Basic
/-- Tail-recursive version of `swap`.  -/
List.swapTR : {α : Type u_1} → List α → ℕ → ℕ → List α
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.mk.injEq : ∀ (mainEnv asyncEnv : Lean.Environment) (constName : Lean.Name) (kind : Lean.ConstantKind)
  (exportedKind? : Option Lean.ConstantKind) (sigPromise : IO.Promise Lean.ConstantVal)
  (constPromise : IO.Promise Lean.Environment.ConstPromiseVal✝) (checkedEnvPromise : IO.Promise Lean.Kernel.Environment)
  (allRealizationsPromise : IO.Promise (Lean.NameMap Lean.AsyncConst✝)) (mainEnv_1 asyncEnv_1 : Lean.Environment)
  (constName_1 : Lean.Name) (kind_1 : Lean.ConstantKind) (exportedKind?_1 : Option Lean.ConstantKind)
  (sigPromise_1 : IO.Promise Lean.ConstantVal) (constPromise_1 : IO.Promise Lean.Environment.ConstPromiseVal✝)
  (checkedEnvPromise_1 : IO.Promise Lean.Kernel.Environment)
  (allRealizationsPromise_1 : IO.Promise (Lean.NameMap Lean.AsyncConst✝)),
  ({ mainEnv := mainEnv, asyncEnv := asyncEnv, constName := constName, kind := kind, exportedKind? := exportedKind?,
        sigPromise := sigPromise, constPromise := constPromise, checkedEnvPromise := checkedEnvPromise,
        allRealizationsPromise := allRealizationsPromise } =
      { mainEnv := mainEnv_1, asyncEnv := asyncEnv_1, constName := constName_1, kind := kind_1,
        exportedKind? := exportedKind?_1, sigPromise := sigPromise_1, constPromise := constPromise_1,
        checkedEnvPromise := checkedEnvPromise_1, allRealizationsPromise := allRealizationsPromise_1 }) =
    (mainEnv = mainEnv_1 ∧
      asyncEnv = asyncEnv_1 ∧
        constName = constName_1 ∧
          kind = kind_1 ∧
            exportedKind? = exportedKind?_1 ∧
              sigPromise = sigPromise_1 ∧
                constPromise = constPromise_1 ∧
                  checkedEnvPromise = checkedEnvPromise_1 ∧ allRealizationsPromise = allRealizationsPromise_1)
-- Mathlib.Analysis.RCLike.Basic
RCLike.I_im' : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.im RCLike.I * RCLike.im z = RCLike.im z
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerRight_associator_hom : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (E : Type u_5) [inst_4 : CategoryTheory.Category.{v_5, u_5} E]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D),
  CategoryTheory.Join.mapWhiskerRight (F.associator G H).hom (CategoryTheory.Functor.id E) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft E (F.comp G) H).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.mapCompLeft E F G).hom
          (CategoryTheory.Join.mapPair H (CategoryTheory.Functor.id E)))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id E)).associator
              (CategoryTheory.Join.mapPair G (CategoryTheory.Functor.id E))
              (CategoryTheory.Join.mapPair H (CategoryTheory.Functor.id E))).hom
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id E)).whiskerLeft
              (CategoryTheory.Join.mapCompLeft E G H).inv)
            (CategoryTheory.Join.mapCompLeft E F (G.comp H)).inv)))
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.eq_2 : ∀ {J : CategoryTheory.Limits.MulticospanShape} (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3)
  (i : J.R) (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)),
  (match CategoryTheory.Limits.WalkingMulticospan.right i with
    | CategoryTheory.Limits.WalkingMulticospan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMulticospan.right i => h_2 i) =
    h_2 i
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProduct_le_of_isTriangulatedClosed₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P₁ P₂ Q : CategoryTheory.ObjectProperty C} [Q.IsTriangulatedClosed₂] [Q.IsClosedUnderIsomorphisms],
  P₁ ≤ Q → P₂ ≤ Q → P₁.extensionProduct P₂ ≤ Q
-- Mathlib.Order.Hom.Basic
Equiv.prodAssoc.eq_1 : ∀ (α : Type u_9) (β : Type u_10) (γ : Type u_11),
  Equiv.prodAssoc α β γ =
    { toFun := fun p => (p.1.1, p.1.2, p.2), invFun := fun p => ((p.1, p.2.1), p.2.2), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.Rat.Lemmas
Rat.den_inv_of_ne_zero : ∀ {q : ℚ}, q ≠ 0 → q⁻¹.den = q.num.natAbs
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The canonical map from a component to the direct limit.  -/
DirectLimit.NonUnitalAlgebra.of : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      (G : ι → Type u_3) →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : CommSemiring R] →
                    [inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)] →
                      [inst_6 : (i : ι) → DistribMulAction R (G i)] →
                        [inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] →
                          [inst_8 : Nonempty ι] → (i : ι) → G i →ₙₐ[R] DirectLimit G f
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.topologicalClosure_minimal : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : Star A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A] [inst_5 : ContinuousStar A] [inst_6 : ContinuousConstSMul R A]
  [inst_7 : IsSemitopologicalSemiring A] (s : NonUnitalStarSubalgebra R A) {t : NonUnitalStarSubalgebra R A},
  s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- In a preadditive category `C`, when an object `X` decomposes as `X ≅ P ⨿ Q`, one may
consider `P` as a direct factor of `X` and up to unique isomorphism, it is determined by the
obvious idempotent `X ⟶ P ⟶ X` which is the projection onto `P` with kernel `Q`. More generally,
one may define a formal direct factor of an object `X : C` : it consists of an idempotent
`p : X ⟶ X` which is thought as the "formal image" of `p`. The type `Karoubi C` shall be the
type of the objects of the karoubi envelope of `C`. It makes sense for any category `C`.  -/
CategoryTheory.Idempotents.Karoubi : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Type (max u_1 v_1)
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C), T ≤ T.rlp.llp
-- Mathlib.Algebra.Colimit.Module
/-- Consider direct limits `lim G` and `lim G'` with direct system `f` and `f'` respectively, any
family of group homomorphisms `gᵢ : Gᵢ ⟶ G'ᵢ` such that `g ∘ f = f' ∘ g` induces a group
homomorphism `lim G ⟶ lim G'`.
 -/
AddCommGroup.DirectLimit.map : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      [inst_1 : (i : ι) → AddCommMonoid (G i)] →
        {f : (i j : ι) → i ≤ j → G i →+ G j} →
          [inst_2 : DecidableEq ι] →
            {G' : ι → Type u_5} →
              [inst_3 : (i : ι) → AddCommMonoid (G' i)] →
                {f' : (i j : ι) → i ≤ j → G' i →+ G' j} →
                  (g : (i : ι) → G i →+ G' i) →
                    (∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)) →
                      AddCommGroup.DirectLimit G f →+ AddCommGroup.DirectLimit G' f'
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_sub_right : ∀ {M : Type u} [inst : SubNegMonoid M] [inst_1 : PseudoMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M),
  nndist (a - c) (b - c) = nndist a b
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoe_le_of_le : ∀ {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph}, H ≤ H' → H.spanningCoe ≤ H'.spanningCoe
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- Two measures at vanishing Lévy-Prokhorov distance from each other assign the same values to all
closed sets.  -/
MeasureTheory.measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  {μ ν : MeasureTheory.Measure Ω},
  MeasureTheory.levyProkhorovEDist μ ν = 0 →
    ∀ {s : Set Ω},
      IsClosed s → (∃ δ > 0, μ (Metric.thickening δ s) ≠ ⊤) → (∃ δ > 0, ν (Metric.thickening δ s) ≠ ⊤) → μ s = ν s
-- Mathlib.RingTheory.Etale.Kaehler
/-- The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]` for `T` a formally étale `S`-algebra.
Also see `S ⊗[R] Ω[A⁄R] ≃ₗ[S] Ω[S ⊗[R] A⁄S]` at `KaehlerDifferential.tensorKaehlerEquiv`.
 -/
KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale : (R : Type u_1) →
  (S : Type u_2) →
    (T : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [IsScalarTower R S T] → [Algebra.FormallyEtale S T] → TensorProduct S T Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]
-- Mathlib.Data.List.Sigma
List.lookupAll_length_le_one : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) {l : List (Sigma β)},
  l.NodupKeys → (List.lookupAll a l).length ≤ 1
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_le_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup N),
  f.ker ≤ Subgroup.comap f H
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.SatelliteConfig.exists_normalized_aux2 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {N : ℕ} {τ : ℝ}
  (a : Besicovitch.SatelliteConfig E N τ),
  a.c (Fin.last N) = 0 →
    a.r (Fin.last N) = 1 →
      1 ≤ τ →
        ∀ (δ : ℝ),
          τ ≤ 1 + δ / 4 →
            δ ≤ 1 → ∀ (i j : Fin N.succ), i ≠ j → ‖a.c i‖ ≤ 2 → 2 < ‖a.c j‖ → 1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.dist_ne_of_adj : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → ∀ {u v w : V}, G.Adj v w → G.Reachable u v → G.dist u v ≠ G.dist u w
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Coerce continuous linear equivs to continuous linear maps.  -/
ContinuousLinearEquiv.instCoeContinuousLinearMap : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M₁ : Type u_4} →
                  [inst_4 : TopologicalSpace M₁] →
                    [inst_5 : AddCommMonoid M₁] →
                      {M₂ : Type u_5} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₁ M₁] → [inst_9 : Module R₂ M₂] → Coe (M₁ ≃SL[σ₁₂] M₂) (M₁ →SL[σ₁₂] M₂)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- All n-simplices among cospherical points in an n-dimensional
subspace have the same circumradius.  -/
EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
  ps ⊆ ↑s →
    ∀ [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction],
      Module.finrank ℝ ↥s.direction = n →
        EuclideanGeometry.Cospherical ps →
          ∃ r, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
/-- The 1-morphism in `LocallyDiscrete C` associated to a given morphism `f : a ⟶ b` in `C`  -/
Quiver.Hom.toLoc : {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → {a b : C} → (a ⟶ b) → ({ as := a } ⟶ { as := b })
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.lt_one_of_floor_lt_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}, ⌊a⌋₊ < 1 → a < 1
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Truncated.instInhabited : {n : ℕ} → Inhabited (SimplexCategory.Truncated n)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.isSymm_toMatrix : ∀ {R : Type u_3} {N : Type u_5} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : Invertible 2] [inst_4 : AddCommGroup N] [inst_5 : Module R N] (b : Module.Basis n R N)
  (Q : QuadraticForm R N), (QuadraticForm.toMatrix b Q).IsSymm
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- The image of the modular group `SL(2, ℤ)`, as a subgroup of `GL(2, ℝ)`.  -/
MatrixGroups.term𝒮ℒ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Dimension.Torsion.Finite
/-- The `StrongRankCondition` is automatic. See `commRing_strongRankCondition`.  -/
Module.finrank_eq_zero_iff_isTorsion : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [StrongRankCondition R] [Module.Finite R M], Module.finrank R M = 0 ↔ Module.IsTorsion R M
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.prod_apply : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G}
  [h : μ.HasProd ν B] {s : Set X} {t : Set Y}, (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)
-- Mathlib.Data.Nat.Count
Nat.count.congr_simp : ∀ (p p_1 : ℕ → Prop),
  p = p_1 →
    ∀ {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (n n_1 : ℕ), n = n_1 → Nat.count p n = Nat.count p_1 n_1
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- A morphism of reflexive quivers called a `ReflPrefunctor`.  -/
CategoryTheory.ReflPrefunctor : (V : Type u₁) →
  [CategoryTheory.ReflQuiver V] → (W : Type u₂) → [CategoryTheory.ReflQuiver W] → Type (max (max (max u₁ u₂) v₁) v₂)
-- Init.Data.List.Basic
/-- If two lists have the same head, then their tails determine their lexicographic order. If the tail
of the first list is lexicographically smaller than the tail of the second list, then the entire
first list is lexicographically smaller than the entire second list.
 -/
List.Lex.cons : ∀ {α : Type u} {r : α → α → Prop} {a : α} {l₁ l₂ : List α}, List.Lex r l₁ l₂ → List.Lex r (a :: l₁) (a :: l₂)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.lift_comp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') [inst_7 : IsLocalizedModule S f] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)), IsLocalizedModule.lift S f g h ∘ₗ f = g
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.eq_div_iff_mul_eq_of_dvd : ∀ {R : Type u} [inst : EuclideanDomain R] (x y z : R), z ≠ 0 → z ∣ y → (x = y / z ↔ z * x = y)
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The extra goals created by the rewrite  -/
Mathlib.Tactic.LibraryRewrite.Rewrite.extraGoals : Mathlib.Tactic.LibraryRewrite.Rewrite → Array (Lean.MVarId × Lean.BinderInfo)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.box.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {ty : Lean.Expr} {fvarId : Lean.FVarId}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_21} {ty_1 : Lean.Expr}
  {fvarId_1 : Lean.FVarId}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_21},
  Lean.Compiler.LCNF.LetValue.box ty fvarId h = Lean.Compiler.LCNF.LetValue.box ty_1 fvarId_1 h_1 →
    ty = ty_1 ∧ fvarId = fvarId_1
-- Mathlib.Analysis.Normed.Group.Real
Real.nnnorm_abs : ∀ (r : ℝ), ‖|r|‖₊ = ‖r‖₊
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationDirac : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : NormedAddCommGroup V] {x : X} {v : V},
  MeasureTheory.IsFiniteMeasure (MeasureTheory.VectorMeasure.dirac x v).variation
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.tendsto_arctan_atTop : Filter.Tendsto Real.arctan Filter.atTop (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2)))
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Build a `MulEquiv` from an isomorphism in the category `Semigroup`.  -/
CategoryTheory.Iso.semigrpIsoToMulEquiv : {X Y : Semigrp} → (X ≅ Y) → ↑X ≃* ↑Y
-- Init.Tactics
/-- This is a "finishing" tactic modification of `simp`. It has two forms.

* `simpa [rules, ⋯] using e` will simplify the goal and the type of
  `e` using `rules`, then try to close the goal using `e`.

  Simplifying the type of `e` makes it more likely to match the goal
  (which has also been simplified). This construction also tends to be
  more robust under changes to the simp lemma set.

  The final match between the simplified `e` and the simplified goal uses
  **reducible** transparency, so it does not unfold semireducible definitions.
  Write `simpa [rules, ⋯] using! e` to perform the match at the ambient
  (default/semireducible) transparency instead.

* `simpa [rules, ⋯]` will simplify the goal and the type of a
  hypothesis `this` if present in the context, then try to close the goal using
  the `assumption` tactic.

As with `simp`, the `!` modifier after `simpa` enables auto-unfolding of
definitions in the simp set.
 -/
Lean.Parser.Tactic.tacticSimpa!_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.w : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.LeftLift f g} (h : s ⟶ t),
  CategoryTheory.CategoryStruct.comp s.unit
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.StructuredArrow.Hom.right h) f) =
    t.unit
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- Via `S.iCycles : S.cycles ⟶ S.X₂`, the object `S.cycles` identifies to the
kernel of `S.g : S.X₂ ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.cyclesIsKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasLeftHomology] → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.iCycles ⋯)
-- Mathlib.Algebra.Algebra.Opposite
/-- The 'unopposite' of an algebra iso `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. Inverse to `AlgEquiv.op`.  -/
AlgEquiv.unop : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) ≃ A ≃ₐ[R] B
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.toOpens : {α : Type u_2} → [inst : TopologicalSpace α] → {x : α} → TopologicalSpace.OpenNhdsOf x → TopologicalSpace.Opens α
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.nonempty : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] {u : β → α}, CauchySeq u → Nonempty β
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_comp : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R} {x : R},
  Polynomial.eval x (p.comp q) = Polynomial.eval (Polynomial.eval x q) p
-- Mathlib.Topology.MetricSpace.Algebra
TendstoLocallyUniformly.smul₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] {X : Type u_3} {ι : Type u_4} [inst_6 : TopologicalSpace X]
  {F : ι → X → α} {G : ι → X → β} {f : X → α} {g : X → β} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l → Continuous f → Continuous g → TendstoLocallyUniformly (F • G) (f • g) l
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.trivializationAt_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (x : M),
  (trivializationAt E (TangentSpace I) x).source = Bundle.TotalSpace.proj ⁻¹' (chartAt H x).source
-- Init.Data.UInt.Lemmas
UInt64.toNat_toUInt32 : ∀ (x : UInt64), x.toUInt32.toNat = x.toNat % 2 ^ 32
-- Mathlib.GroupTheory.Coset.Card
AddSubgroup.card_eq_card_quotient_mul_card_addSubgroup : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s
-- Mathlib.Analysis.Convex.Cone.Basic
/-- Any proper cone can be seen as a pointed cone.

This is an alias of `ClosedSubmodule.toSubmodule` for convenience and discoverability.  -/
ProperCone.toPointedCone : {R : Type u_2} →
  {E : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] →
            [inst_4 : TopologicalSpace E] → [inst_5 : Module R E] → ProperCone R E → PointedCone R E
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.coe_translate : ∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] (f : F)
  [inst_1 : CuspFormClass F Γ k] (g : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  ⇑(CuspForm.translate f (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g))) =
    SlashAction.map k g ⇑f
-- Mathlib.NumberTheory.Padics.WithVal
Padic.isUniformInducing_cast_withVal : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)],
  IsUniformInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)
-- Mathlib.Algebra.Group.Int.Defs
Int.instAddCommGroup : AddCommGroup ℤ
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₁₃Functor_map_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  {X Y : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))} (f : X ⟶ Y) (X_1 : C₃)
  (Y_1 : C₂) (Z : C₁),
  (((CategoryTheory.Functor.flip₁₃Functor.map f).app X_1).app Y_1).app Z = ((f.app Z).app Y_1).app X_1