mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The cosine of the angle between two vectors is 0 if and only if the angle is π / 2.  -/
InnerProductGeometry.cos_eq_zero_iff_angle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  Real.cos (InnerProductGeometry.angle x y) = 0 ↔ InnerProductGeometry.angle x y = Real.pi / 2
-- Std.Time.Internal.UnitVal
/-- Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio. Using the
"T-rounding" (Truncation-rounding) convention
 -/
Std.Time.Internal.UnitVal.tdiv : {a : ℚ} → Std.Time.Internal.UnitVal a → (divisor : ℤ) → Std.Time.Internal.UnitVal (a * ↑divisor)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The composition functor is also the composition on group objects.  -/
CategoryTheory.Functor.mapGrpCompIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.CartesianMonoidalCategory E] →
                  {F : CategoryTheory.Functor C D} →
                    {G : CategoryTheory.Functor D E} →
                      [inst_6 : F.Monoidal] → [inst_7 : G.Monoidal] → (F.comp G).mapGrp ≅ F.mapGrp.comp G.mapGrp
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.piIso_inv : ∀ {I : Type u} (X : I → TopCat),
  (FundamentalGroupoidFunctor.piIso X).inv = CategoryTheory.Functor.pi' (FundamentalGroupoidFunctor.proj X)
-- Mathlib.CategoryTheory.Sites.Pretopology
/-- The trivial pretopology, in which the coverings are exactly singleton isomorphisms. This topology is
also known as the indiscrete, coarse, or chaotic topology.  -/
CategoryTheory.Pretopology.trivial : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Pretopology C
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.commutator_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X Y : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤),
  ⁅X, Y⁆ f = X (Y f) - Y (X f)
-- Mathlib.GroupTheory.Index
AddSubgroup.index_iInf_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_3} [Finite ι] {f : ι → AddSubgroup G},
  (∀ (i : ι), (f i).index ≠ 0) → (⨅ i, f i).index ≠ 0
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The left Kan lift of `g` along `f`.  -/
CategoryTheory.Bicategory.lanLift : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → (f : b ⟶ a) → (g : c ⟶ a) → [CategoryTheory.Bicategory.HasLeftKanLift f g] → c ⟶ b
-- Init.System.IO
IO.FS.FileType.noConfusionType : Sort v✝ → IO.FS.FileType → IO.FS.FileType → Sort v✝
-- Init.Core
/-- A setoid is a type with a distinguished equivalence relation, denoted `≈`.

The `Quotient` type constructor requires a `Setoid` instance.
 -/
Setoid : Sort u → Sort (max 1 u)
-- Init.Data.SInt.Lemmas
Int8.toInt32_div_of_ne_left : ∀ (a b : Int8), a ≠ Int8.minValue → (a / b).toInt32 = a.toInt32 / b.toInt32
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.commandCtx.inj : ∀ {info info_1 : Lean.Elab.CommandContextInfo},
  Lean.Elab.PartialContextInfo.commandCtx info = Lean.Elab.PartialContextInfo.commandCtx info_1 → info = info_1
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β),
  MeasureTheory.Measure.comap f 0 = 0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ofList_nil : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.ExtTreeSet.ofList [] cmp = ∅
-- Mathlib.Algebra.Exact.Basic
LinearMap.surjective_iff_eq_zero_of_exact : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P}, Function.Exact ⇑f ⇑g → (Function.Surjective ⇑f ↔ g = 0)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfc_le_iff : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜)
  (a : A) (c : NNReal),
  autoParam (ContinuousOn f (spectrum 𝕜 a)) nnnorm_cfc_le_iff._auto_1 →
    autoParam (p a) nnnorm_cfc_le_iff._auto_3 → (‖cfc f a‖₊ ≤ c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ ≤ c)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- A section `s` of `V` is `C^k` on `t ⊆ e.baseSet` iff each of its
coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is  -/
contMDiffOn_iff_localFrameCoeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {t : Set M}
  {k : WithTop ℕ∞} [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  IsOpen t →
    t ⊆ e.baseSet →
      (ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) t ↔
        ∀ (i : ι),
          ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) k
            ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) t)
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- `LightCondSet.LocallyConstant.functor` is isomorphic to `LightCondensed.discrete`
(by uniqueness of adjoints).
 -/
LightCondSet.LocallyConstant.iso : LightCondSet.LocallyConstant.functor ≅ LightCondensed.discrete (Type u)
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.instInhabitedColorFocused : {α : Type u_5} →
  {ι : Type u_6} → {κ : Type u_7} → (C : (ι → Option α) → κ) → Inhabited (Combinatorics.Line.ColorFocused C)
-- Mathlib.Topology.UniformSpace.Cauchy
le_nhds_iff_adhp_of_cauchy : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α}, Cauchy f → (f ≤ nhds x ↔ ClusterPt x f)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.Integrable.piecewise : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f g : α → ε'}
  [inst_2 : DecidablePred fun x => x ∈ s],
  MeasurableSet s →
    MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn g sᶜ μ → MeasureTheory.Integrable (s.piecewise f g) μ
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The inverse of a bijective `MulSemiringActionHom` is a `MulSemiringActionHom`.  -/
MulSemiringActionHom.inverse' : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {φ' : N →* M} →
            {R : Type u_10} →
              [inst_2 : Semiring R] →
                [inst_3 : MulSemiringAction M R] →
                  {S : Type u_12} →
                    [inst_4 : Semiring S] →
                      [inst_5 : MulSemiringAction N S] →
                        (f : R →ₑ+*[φ] S) →
                          (g : S → R) →
                            Function.RightInverse ⇑φ' ⇑φ →
                              Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → S →ₑ+*[φ'] R
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.mulLeftReflectLT : ∀ {α : Type u} [inst : LT α] [inst_1 : Mul α] [c : MulLeftReflectLT α], MulLeftReflectLT αᵒᵈ
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.scalar_eq : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [Nontrivial A] (k : 𝕜),
  spectrum 𝕜 ((algebraMap 𝕜 A) k) = {k}
-- Mathlib.LinearAlgebra.FreeModule.PID
generator_maximal_submoduleImage_dvd : ∀ {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsPrincipalIdealRing R] {N O : Submodule R M} (hNO : N ≤ O) {ϕ : ↥O →ₗ[R] R},
  (∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N) →
    ∀ [inst_4 : (ϕ.submoduleImage N).IsPrincipal] (y : M) (yN : y ∈ N),
      ϕ ⟨y, ⋯⟩ = Submodule.IsPrincipal.generator (ϕ.submoduleImage N) →
        ∀ (ψ : ↥O →ₗ[R] R), Submodule.IsPrincipal.generator (ϕ.submoduleImage N) ∣ ψ ⟨y, ⋯⟩
-- Mathlib.NumberTheory.Modular
ModularGroup.re_T_zpow_smul : ∀ (z : UpperHalfPlane) (n : ℤ), (ModularGroup.T ^ n • z).re = z.re + ↑n
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_mul_transpose_self : ∀ {α : Type u_1} {n : Type u_3} [inst : Fintype n] [inst_1 : NonUnitalCommSemiring α] (A : Matrix n n α),
  (A * A.transpose).IsSymm
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.iteratedFDeriv_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x₀ : E}
  {m n : WithTop ℕ∞} {i : ℕ}, ContDiffAt 𝕜 n f x₀ → m + ↑i ≤ n → ContDiffAt 𝕜 m (iteratedFDeriv 𝕜 i f) x₀
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_monomial_one : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] (n : ℕ), ((Polynomial.monomial n) 1).IsMonicOfDegree n
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.sectionsMap_freeHomEquiv_symm_freeSection : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {I : Type u} {M : SheafOfModules R} (f : I → M.sections) (i : I),
  SheafOfModules.sectionsMap (M.freeHomEquiv.symm f) (SheafOfModules.freeSection i) = f i
-- Mathlib.Data.Real.Basic
Real.instCommMonoid : CommMonoid ℝ
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.has_good_supp_iff : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (x : F α),
  (∀ (p : (i : Fin2 n) → α i → Prop), MvFunctor.LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ MvFunctor.supp x i, p i u) ↔
    ∃ a f,
      MvQPF.abs ⟨a, f⟩ = x ∧
        ∀ (i : Fin2 n) (a' : (MvQPF.P F).A) (f' : ((MvQPF.P F).B a').Arrow α),
          MvQPF.abs ⟨a', f'⟩ = x → f i '' Set.univ ⊆ f' i '' Set.univ
-- Init.Prelude
/-- Hashes a value into a `UInt64`.  -/
Hashable.hash : {α : Sort u} → [self : Hashable α] → α → UInt64
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal.sizeOf_spec : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  [inst_2 : SizeOf R] [inst_3 : SizeOf Γ₀] (ofVal : R), sizeOf (WithVal.toVal v ofVal) = 1 + sizeOf ofVal
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_eq_singleton : ∀ {m n : ℕ}, n = m → (m...=n).toArray = #[m]
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.degree_eq_of_le_of_coeff_ne_zero' : ∀ {R : Type u_1} [inst : Semiring R] {deg m o : WithBot ℕ} {c : R} {p : Polynomial R},
  p.degree ≤ m → p.coeff (WithBot.unbotD 0 deg) = c → c ≠ 0 → m = deg → o = deg → p.degree = deg
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  (S : J.MayerVietorisSquare),
  S.shortComplex.X₂ =
    ((CategoryTheory.presheafToSheaf J AddCommGrpCat).obj ((CategoryTheory.yoneda.obj S.X₂).comp AddCommGrpCat.free) ⊞
      (CategoryTheory.presheafToSheaf J AddCommGrpCat).obj ((CategoryTheory.yoneda.obj S.X₃).comp AddCommGrpCat.free))
-- Mathlib.Order.Basic
ne_iff_gt_iff_ge : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, (a ≠ b ↔ b < a) ↔ b ≤ a
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.monotone_sizeUpTo : ∀ {n : ℕ} (c : Composition n), Monotone c.sizeUpTo
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffOn.mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s t : Set M}
  {n : WithTop ℕ∞}, ContMDiffOn I I' n f s → t ⊆ s → ContMDiffOn I I' n f t
-- Mathlib.Order.Defs.LinearOrder
lt_min : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a < b → a < c → a < min b c
-- Std.Time.Date.Unit.Weekday
/-- Wednesday.  -/
Std.Time.Weekday.wednesday : Std.Time.Weekday
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.toField : {α : Type u_5} → [self : NormedField α] → Field α
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_list_sum : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (l : List (Polynomial R)) (x : S),
  Polynomial.eval₂ f x l.sum = (List.map (Polynomial.eval₂ f x) l).sum
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.dist_fst_le : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : PseudoMetricSpace α]
  [inst_1 : PseudoMetricSpace β] (x y : WithLp p (α × β)), dist x.fst y.fst ≤ dist x y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' fallback : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).getKeyD k' fallback =
        if compare k k' = Ordering.eq then
          if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then k else fallback
        else t.getKeyD k' fallback
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- The fraction ring of the space of `p`-Witt vectors on `k`  -/
Isocrystal.«termK(_,_)» : Lean.ParserDescr
-- Mathlib.Algebra.Lie.OfAssociative
LieRing.lie_apply : ∀ {A : Type v} [inst : Ring A] {α : Type u_1} (f g : α → A) (a : α), ⁅f, g⁆ a = ⁅f a, g a⁆
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_prod_X_sub_C : ∀ {R : Type u} [inst : CommRing R] {k : ℕ} {S : Finset R},
  k ≤ S.card →
    (⇑Polynomial.derivative)^[k] (∏ a ∈ S, (Polynomial.X - Polynomial.C a)) =
      ↑k.factorial * ∑ T ∈ Finset.powersetCard (S.card - k) S, ∏ a ∈ T, (Polynomial.X - Polynomial.C a)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape)
  [inst_1 : Unique J.L] [inst_2 : Unique J.R] {X Y : C} (f g : X ⟶ Y),
  CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork J f g =
    ((CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g).multiforkEquivPiForkOfIsLimit
          (CategoryTheory.Limits.Fan.isLimitMkOfUnique (CategoryTheory.Iso.refl X) J.L)
          (CategoryTheory.Limits.Fan.isLimitMkOfUnique (CategoryTheory.Iso.refl Y) J.R)).trans
      (CategoryTheory.Limits.Fork.equivOfIsos
        (CategoryTheory.Iso.refl (CategoryTheory.Limits.Fan.mk X fun x => (CategoryTheory.Iso.refl X).hom).pt)
        (CategoryTheory.Iso.refl (CategoryTheory.Limits.Fan.mk Y fun x => (CategoryTheory.Iso.refl Y).hom).pt) ⋯ ⋯)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
SSet.RelativeMorphism.botEquiv_symm_apply_map : ∀ {X Y : SSet} (f : X ⟶ Y), (SSet.RelativeMorphism.botEquiv.symm f).map = f
-- Mathlib.CategoryTheory.Triangulated.Yoneda
CategoryTheory.Pretriangulated.instShiftSequenceAddCommGrpCatObjOppositeFunctorPreadditiveCoyonedaInt : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] → (A : Cᵒᵖ) → (CategoryTheory.preadditiveCoyoneda.obj A).ShiftSequence ℤ
-- Mathlib.Algebra.BigOperators.Fin
List.alternatingProd.eq_1 : ∀ {G : Type u_4} [inst : One G] [inst_1 : Mul G] [inst_2 : Inv G], [].alternatingProd = 1
-- Aesop.Search.Main
Aesop.searchLoop : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q (Array Lean.MVarId)
-- Mathlib.Algebra.Star.Basic
/-- **Alias** of `starRingEnd_self_apply`. -/
RCLike.conj_conj : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] (x : R), (starRingEnd R) ((starRingEnd R) x) = x
-- Mathlib.Analysis.Convex.Topology
Convex.nhdsWithin_sdiff_eq_nhdsNE : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜},
  Convex 𝕜 s →
    ∀ {a : 𝕜},
      a ∈ closure s → (s ∩ Set.Iio a).Nonempty → (s ∩ Set.Ioi a).Nonempty → nhdsWithin a (s \ {a}) = nhdsWithin a {a}ᶜ
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.toSubmodule_injective : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  Function.Injective LieSubalgebra.toSubmodule
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.instMulActionVariableChange : {R : Type u} → [inst : CommRing R] → MulAction (WeierstrassCurve.VariableChange R) (WeierstrassCurve R)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.extendIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {X : C} (i : X ⟶ s.pt)
  [inst_2 : CategoryTheory.IsIso i] (hs : CategoryTheory.Limits.IsLimit s),
  CategoryTheory.Limits.IsLimit.extendIso i hs = hs.ofIsoLimit (s.extendIso (CategoryTheory.asIso' i))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ},
  (Std.ExtHashMap.filterMap f m).getD k fallback = (m[k]?.pbind fun x_2 h' => f (m.getKey k ⋯) x_2).getD fallback
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.M : Type → Type
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opMap.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  CategoryTheory.ShortComplex.opMap φ = { τ₁ := φ.τ₃.op, τ₂ := φ.τ₂.op, τ₃ := φ.τ₁.op, comm₁₂ := ⋯, comm₂₃ := ⋯ }
-- Init.Grind.Offset
Lean.Grind.Nat.ro_le : ∀ (u w v k : ℕ), u ≤ w + k → w ≤ v → u ≤ v + k
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsCyclotomicExtension.Rat.adjoin_singleton_eq_top : ∀ {n : ℕ} {K : Type u} [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n] [hK : IsCyclotomicExtension {n} ℚ K]
  {ζ : K} (hζ : IsPrimitiveRoot ζ n), ℤ[hζ.toInteger] = ⊤
-- Mathlib.Topology.Algebra.Algebra
instCommRingSubtypeMemSubalgebraElementalOfT2Space : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u} →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Ring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : IsSemitopologicalRing A] → [T2Space A] → {x : A} → CommRing ↥(Algebra.elemental R x)
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) {Z : CategoryTheory.Functor C E}
  (h : (G.obj j).comp F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.limit.π G j) F)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j) h
-- Lean.Meta.Tactic.Grind.Intro
Lean.Meta.Grind.Action.intro : ℕ → Lean.Meta.Grind.Action
-- Mathlib.Data.Multiset.Find
Multiset.find?_add : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s t : Multiset α) (hp : {x | x ∈ s + t ∧ p x}.Subsingleton),
  Multiset.find? p (s + t) hp = (Multiset.find? p s ⋯).or (Multiset.find? p t ⋯)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.modify_equiv_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      (↑m₁).Equiv ↑m₂ →
        ∀ {k : α} (f : β → β),
          (↑(Std.DHashMap.Internal.Raw₀.Const.modify m₁ k f)).Equiv ↑(Std.DHashMap.Internal.Raw₀.Const.modify m₂ k f)
-- Mathlib.Order.Monotone.Odd
/-- An odd function on a linear ordered additive commutative group is monotone on the whole group
provided that it is monotone on `Set.Ici 0`.  -/
monotone_of_odd_of_monotoneOn_nonneg : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G]
  [inst_3 : AddCommGroup H] [inst_4 : PartialOrder H] [IsOrderedAddMonoid H] {f : G → H},
  (∀ (x : G), f (-x) = -f x) → MonotoneOn f (Set.Ici 0) → Monotone f
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_mul_rexp_neg : ∀ (x : ℝ), x.sigmoid * Real.exp (-x) = (-x).sigmoid
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_le_iff_one_le_mul' : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b : α}, a⁻¹ ≤ b ↔ 1 ≤ a * b
-- Lean.Parser.Extra
/-- No-op parser combinator that advises the pretty printer to dedent the given syntax,
if it was grouped by the category parser.
Dedenting can in particular be used to counteract automatic indentation.  -/
Lean.Parser.ppDedentIfGrouped : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtr.congr : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f g : α → β} {a : α},
  IsLocalExtr f a → f =ᶠ[nhds a] g → IsLocalExtr g a
-- Mathlib.Topology.Constructions.SumProd
Topology.IsEmbedding.sumElim_of_separatedNhds : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z},
  Topology.IsEmbedding f →
    Topology.IsEmbedding g → SeparatedNhds (Set.range f) (Set.range g) → Topology.IsEmbedding (Sum.elim f g)
-- Lean.Elab.Do.Legacy
/-- Generate `CodeBlock` for `doUnless; doElems`
`doUnless` is of the form
```
"unless " >> termParser >> "do " >> doSeq
```   -/
Lean.Elab.Term.Do.ToCodeBlock.doUnlessToCode : Lean.Syntax → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock