mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.Hom
/-- Consider a continuous map `v : M → E₁` to a vector bundle, over a base map `b₁ : M → B₁`, and
another basemap `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending
continuously on `m`, one can apply `ϕ m` to `g m`, and the resulting map is continuous.

Note that the continuity of `ϕ` cannot be always be stated as continuity of a map into a bundle,
as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` only have a nice topology when `b₁` and `b₂` are
globally continuous, but we want to apply this lemma with only local information. Therefore, we
formulate it using continuity of `ϕ` read in coordinates.

Version for `ContinuousAt`. We also give a version for `ContinuousWithinAt`, but no version for
`ContinuousOn` or `Continuous` as our assumption, written in coordinates, only makes sense around
a point.

For a version with `B₁ = B₂` and `b₁ = b₂`, in which continuity can be expressed without
`inCoordinates`, see `ContinuousWithinAt.clm_bundle_apply`
 -/
ContinuousAt.clm_apply_of_inCoordinates : ∀ {𝕜 : Type u_8} {F₁ : Type u_9} {F₂ : Type u_10} {B₁ : Type u_11} {B₂ : Type u_12} {M : Type u_13}
  {E₁ : B₁ → Type u_14} {E₂ : B₂ → Type u_15} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (x : B₁) → AddCommGroup (E₁ x)] [inst_2 : (x : B₁) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁]
  [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B₁) → TopologicalSpace (E₁ x)] [inst_7 : (x : B₂) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B₂) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B₂) → TopologicalSpace (E₂ x)]
  [inst_13 : TopologicalSpace B₁] [inst_14 : TopologicalSpace B₂] [inst_15 : TopologicalSpace M]
  [inst_16 : FiberBundle F₁ E₁] [inst_17 : VectorBundle 𝕜 F₁ E₁] [inst_18 : FiberBundle F₂ E₂]
  [inst_19 : VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)}
  {v : (m : M) → E₁ (b₁ m)},
  ContinuousAt (fun m => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀ →
    ContinuousAt (fun m => ⟨b₁ m, v m⟩) m₀ → ContinuousAt b₂ m₀ → ContinuousAt (fun m => ⟨b₂ m, (ϕ m) (v m)⟩) m₀
-- Mathlib.Algebra.Group.Units.Defs
Units.mul_inv_cancel_left : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) (b : α), ↑a * (↑a⁻¹ * b) = b
-- Mathlib.CategoryTheory.Galois.Equivalence
CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (CategoryTheory.PreGaloisCategory.functorToContAction F).Faithful
-- Mathlib.Algebra.Quaternion
Quaternion.imI_ratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ), (↑q).imI = 0
-- Mathlib.Logic.Function.FromTypes
Function.FromTypes.const_zero : ∀ (p : Fin 0 → Type u) {τ : Type u} (t : τ), Function.FromTypes.const p t = t
-- Mathlib.Topology.UniformSpace.Cauchy
IsCompact.isComplete : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, IsCompact s → IsComplete s
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.ofInjective_toHom : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective ⇑f),
  (FirstOrder.Language.Embedding.ofInjective hf).toHom = f
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.linearMap_apply_apply : ∀ (R : Type u_5) (M : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {X : Type u_7}
  {Y : Type u_8} [inst_3 : Fintype X] [inst_4 : Finite Y] [inst_5 : DecidableEq Y] (f : X → Y) (s : X → M) (y : Y),
  (FunOnFinite.linearMap R M f) s y = {x | f x = y}.sum s
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.instCommMonoid.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommMonoid N],
  MonoidHom.instCommMonoid =
    { toMul := MonoidHom.mul, mul_assoc := ⋯, toOne := instOneMonoidHom, one_mul := ⋯, mul_one := ⋯,
      toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The image of a functor injective on objects  -/
CategoryTheory.Subgroupoid.im : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Groupoid D] →
        (φ : CategoryTheory.Functor C D) → Function.Injective φ.obj → CategoryTheory.Subgroupoid D
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_eq_nil_iff_eq_zero : ∀ {b n : ℕ}, b.digits n = [] ↔ n = 0
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.ShrinkHoms.preadditive : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v_1, u_1} C] →
      [CategoryTheory.Preadditive C] → CategoryTheory.Preadditive (CategoryTheory.ShrinkHoms.{u_1} C)
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.instSetLike : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → SetLike (ClopenUpperSet α) α
-- Mathlib.Geometry.Manifold.Notation
/-- Try to find a `ModelWithCorners` instance on a type (represented by an expression `e`),
using the local context to infer the appropriate instance.
This supports all `ModelWithCorners` instances that are currently defined in mathlib.
Further cases can be added as necessary.

Return an expression describing the found model with corners.

Note that the matching on `e` does not see through reducibility (e.g. we distinguish the `abbrev`
`TangentBundle` from its definition), so `whnfR` should not be run on `e` prior to calling
`findModel` on it.

This implementation is not maximally robust yet.
 -/
Manifold.Elab.findModel : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.GroupTheory.Index
Subgroup.index_comap : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) (f : G' →* G),
  (Subgroup.comap f H).index = H.relIndex f.range
-- Mathlib.Data.Finset.Card
Finset.card_insert_le : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), (insert a s).card ≤ s.card + 1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_equiv_eq_map_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : N ≃* M) (K : Subsemigroup M),
  Subsemigroup.comap (↑f) K = Subsemigroup.map (↑f.symm) K
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSliceTR.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (m : ℕ) (h_1 : Unit → motive 0) (h_2 : (m : ℕ) → motive m.succ),
  (match m.succ with
    | 0 => h_1 ()
    | m.succ => h_2 m) =
    h_2 m
-- Mathlib.RingTheory.AdicCompletion.Noetherian
IsHausdorff.of_isLocalRing : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsNoetherianRing R] [Module.Finite R M] [IsLocalRing R], I ≠ ⊤ → IsHausdorff I M
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.isSubmersionAtOfComplement_complement : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x), Manifold.IsSubmersionAtOfComplement h.complement I J n f x
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.iterate_derivative_interpolate : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F),
  Set.InjOn v ↑s →
    ∀ {k : ℕ},
      k < s.card →
        (⇑Polynomial.derivative)^[k] ((Lagrange.interpolate s v) r) =
          ↑k.factorial *
            ∑ i ∈ s,
              Polynomial.C (r i / ∏ j ∈ s.erase i, (v i - v j)) *
                ∑ t ∈ Finset.powersetCard (s.card - (k + 1)) (s.erase i), ∏ a ∈ t, (Polynomial.X - Polynomial.C (v a))
-- Mathlib.SetTheory.Cardinal.Finite
Cardinal.toENat_lt_natCast_iff : ∀ {n : ℕ} {c : Cardinal.{u_3}}, Cardinal.toENat c < ↑n ↔ c < ↑n
-- Std.Internal.Parsec.ByteArray
/-- Scans while `pred` is satisfied. Returns `(count, iterator, hitEof)`.
 -/
_private.Std.Internal.Parsec.ByteArray.0.Std.Internal.Parsec.ByteArray.scanWhile : (UInt8 → Bool) → ℕ → ByteArray.Iterator → ℕ × ByteArray.Iterator × Bool
-- Mathlib.Order.JordanHolder
/-- Every modular lattice is a Jordan Hölder lattice.  -/
JordanHolderLattice.instOfIsModularLattice : (X : Type u) → [inst : Lattice X] → [IsModularLattice X] → JordanHolderLattice X
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.Functor.mapAddHom.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {X Y : C},
  F.mapAddHom = F.mapAddHom
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- The results of the theorems that threw an error when trying to apply them.
Usually, errors will be caught, except for when using `click_suggestions.debug`.  -/
Mathlib.Tactic.ClickSuggestions.SectionState.errors : {α : Type} → Mathlib.Tactic.ClickSuggestions.SectionState α → Array ProofWidgets.Html
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.opEquivOpUnder_inverse_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T) (Y : (CategoryTheory.Under X)ᵒᵖ),
  (CategoryTheory.Over.opEquivOpUnder X).inverse.obj Y = CategoryTheory.Over.mk (Opposite.unop Y).hom.op
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.box_lower : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] (ν : ι → ℤ), (BoxIntegral.unitPartition.box n ν).lower = fun i => ↑(ν i) / ↑n
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- Underlying continuous linear isomorphism of an equivalence of continuous representations.  -/
ContRepresentation.Equiv.toContinuousLinearEquiv : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} → {π₂ : ContRepresentation R G W} → π₁.Equiv π₂ → V ≃L[R] W
-- Mathlib.Data.Part
Part.right_dom_of_sub_dom : ∀ {α : Type u_1} [inst : Sub α] {a b : Part α}, (a - b).Dom → b.Dom
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun_iff_Indep : ∀ {Ω : Type u_1} {β : Type u_3} {γ : Type u_4} {x : MeasurableSpace Ω} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ]
  (f : Ω → β) (g : Ω → γ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.IndepFun f g μ ↔ ProbabilityTheory.Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.snd_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → w₂ ∉ t
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.cocycleOfDegreewiseSplit.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting),
  CochainComplex.cocycleOfDegreewiseSplit S σ =
    CochainComplex.HomComplex.Cocycle.mk
      (CochainComplex.HomComplex.Cochain.mk fun p q x =>
        CategoryTheory.CategoryStruct.comp (σ p).s (CategoryTheory.CategoryStruct.comp (S.X₂.d p q) (σ q).r))
      2 CochainComplex.cocycleOfDegreewiseSplit._proof_2 ⋯
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.overEquivOfIsInitial_counitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.overEquivOfIsInitial.{w, v_1, u_1} X h).counitIso =
    CategoryTheory.Iso.refl
      ((CategoryTheory.Functor.fromPUnit (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))).comp
        (CategoryTheory.Functor.star (CategoryTheory.Over X)))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulC_nc.eq_1 : ∀ (p₁ p₂ : Lean.Grind.CommRing.Poly) (c : ℕ),
  p₁.mulC_nc p₂ c = Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c p₁ (Lean.Grind.CommRing.Poly.num 0)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Functor composition induces a functor on cosimplicial objects.  -/
CategoryTheory.CosimplicialObject.whiskering : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : Type u_1) →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor (CategoryTheory.Functor C D)
          (CategoryTheory.Functor (CategoryTheory.CosimplicialObject C) (CategoryTheory.CosimplicialObject D))
-- Mathlib.RingTheory.Binomial
Polynomial.descPochhammer_smeval_eq_descFactorial : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [NatPowAssoc R] (n k : ℕ),
  (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.leftUnitor_def : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor M = (TensorProduct.lid R ↑M).toModuleIso
-- Batteries.Util.ProofWanted
/-- For a *transparent* (derived) `nm`, the inlined replacement term: `nm` applied to its user
arguments and to all of its surfaced leaf-hole binders, η-abstracted over the user arguments so
that `❰nm❱ x y` βι-reduces to `nm`'s body. When `some`, `rewriteRefs` splices this in directly and
adds no `d_nm` binder (`nm` is not a hole); `binderType`/`isClass`/`kind` are then unused.  -/
_private.Batteries.Util.ProofWanted.0.WantedRefInfo.transparent : WantedRefInfo✝ → Option (Lean.TSyntax `term)
-- Mathlib.LinearAlgebra.Basis.Basic
/-- Given a basis, the `i`th element of the dual basis evaluates to 1 on the `i`th element of the
basis.  -/
Module.Basis.mk_coord_apply_eq : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} {hli : LinearIndependent R v} {hsp : ⊤ ≤ Submodule.span R (Set.range v)} (i : ι),
  ((Module.Basis.mk hli hsp).coord i) (v i) = 1
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.SigmaFinite.withDensity_of_ne_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → ENNReal},
  (∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → MeasureTheory.SigmaFinite (μ.withDensity f)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntry_eq_getEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [instBEq : BEq α] [inst_2 : Std.LawfulBEqOrd α]
  {k : α} {t : Std.DTreeMap.Internal.Impl α β} {h : k ∈ t} (hto : t.Ordered),
  t.getEntry k h = Std.Internal.List.getEntry k t.toListModel ⋯
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
prodIsoPullback_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X)
        (CategoryTheory.Limits.terminal.from Y)) =
    CategoryTheory.Limits.prod.fst
-- Mathlib.CategoryTheory.Action.Monoidal
/-- Upgrading the functor `Action V G ⥤ (SingleObj G ⥤ V)` to a monoidal functor.  -/
Action.FunctorCategoryEquivalence.functorMonoidal : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        [inst_2 : CategoryTheory.MonoidalCategory V] → Action.FunctorCategoryEquivalence.functor.Monoidal
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_add_single_eq_single_add_single : ∀ {I : Type u} [inst : DecidableEq I] {M : Type u_5} [inst_1 : AddCommMonoid M] {k l m n : I} {u v : M},
  u ≠ 0 →
    v ≠ 0 →
      (Pi.single k u + Pi.single l v = Pi.single m u + Pi.single n v ↔
        k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n)
-- Init.Data.Nat.Fold
/-- Checks whether a predicate holds for any natural number in a range.

In particular, `(start, stop).allI f` returns true if `f` is true for any natural number from
`start` (inclusive) to `stop` (exclusive).

Examples:
 * `(5, 8).anyI (fun j _ _ => j == 6) = (5 == 6) || (6 == 6) || (7 == 6)`
 * `(5, 8).anyI (fun j _ _ => j % 2 = 0) = true`
 * `(6, 6).anyI (fun j _ _ => j % 2 = 0) = false`
 -/
Prod.anyI : (i : ℕ × ℕ) → ((j : ℕ) → i.1 ≤ j → j < i.2 → Bool) → Bool
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.instGroupoid : {X : Type u} →
  {G : Type u_2} →
    [inst : Group G] → [inst_1 : MulAction G X] → CategoryTheory.Groupoid (CategoryTheory.ActionCategory G X)
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.HasAffineProperty.diagonal_iff : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}
  [inst : AlgebraicGeometry.IsAffine Y], Q.diagonal f ↔ P.diagonal f
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearMap.det_toContinuousLinearMap : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E]
  [inst_5 : CompleteSpace 𝕜] [inst_6 : T2Space E] [inst_7 : FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] E),
  (LinearMap.toContinuousLinearMap f).det = LinearMap.det f
-- Mathlib.Analysis.SpecialFunctions.Sqrt
HasDerivWithinAt.sqrt : ∀ {f : ℝ → ℝ} {s : Set ℝ} {f' x : ℝ},
  HasDerivWithinAt f f' s x → f x ≠ 0 → HasDerivWithinAt (fun y => √(f y)) (f' / (2 * √(f x))) s x
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.hId_app : ∀ {C₁ : Type u₁} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₃, u₃} C₃] (L : CategoryTheory.Functor C₁ C₃) (X : C₁),
  (CategoryTheory.TwoSquare.hId L).app X = CategoryTheory.CategoryStruct.id (L.obj X)
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.mem_smul_pointwise_iff_exists : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] (a : A) (m : M)
  (S : AddSubmonoid A), a ∈ m • S ↔ ∃ s ∈ S, m • s = a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- a morphism `S₁.X₁ ⟶ S₂.X₁`  -/
CategoryTheory.ShortComplex.Homotopy.h₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} → CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ → (S₁.X₁ ⟶ S₂.X₁)
-- Mathlib.Tactic.Ring.Common
/-- Attempts to prove that a polynomial expression in `ℕ` is positive.

* Atoms are not (necessarily) positive
* Sums defer to `ExSum.evalPos`
 -/
Mathlib.Tactic.Ring.Common.ExBaseNat.evalPos : {a : Q(ℕ)} → Mathlib.Tactic.Ring.Common.ExBaseNat a → Option Q(0 < «$a»)
-- Mathlib.Topology.ApproximateUnit
/-- In a topological unital magma, `𝓝 1` is the largest approximate unit.  -/
Filter.IsApproximateUnit.iff_neBot_and_le_nhds_one : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MulOneClass α] [SeparatelyContinuousMul α] {l : Filter α},
  l.IsApproximateUnit ↔ l.NeBot ∧ l ≤ nhds 1
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.below.refl : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {motive : (a a_1 : M) → AddConGen.Rel r a a_1 → Prop} (x : M),
  AddConGen.Rel.below ⋯
-- Mathlib.LinearAlgebra.Determinant
/-- The determinant of a basis constructed by `unitsSMul` is the product of the given units.  -/
Module.Basis.det_unitsSMul_self : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M) (w : ι → Rˣ),
  e.det ⇑(e.unitsSMul w) = ∏ i, ↑(w i)
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_zero : ∀ {α : Type u_3} [inst : DivisionSemiring α], ↑0 = 0
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- `Under.map` preserves identities.  -/
CategoryTheory.MorphismProperty.Under.mapId : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) →
        [inst_1 : Q.IsMultiplicative] →
          [inst_2 : P.IsStableUnderComposition] →
            [inst_3 : P.IsMultiplicative] →
              [Q.RespectsIso] →
                (X : T) →
                  (f : optParam (X ⟶ X) (CategoryTheory.CategoryStruct.id X)) →
                    (hf :
                        autoParam (f = CategoryTheory.CategoryStruct.id X)
                          CategoryTheory.MorphismProperty.Under.mapId._auto_1) →
                      CategoryTheory.MorphismProperty.Under.map Q ⋯ ≅ CategoryTheory.Functor.id (P.Under Q X)
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.ext_iff : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] {h h' : α ≃ᵤ β},
  h = h' ↔ ∀ (x : α), h x = h' x
-- Init.Data.String.Lemmas.Basic
String.slice_eq_toSlice_iff : ∀ {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂}, s.slice p₁ p₂ h = s.toSlice ↔ p₁ = s.startPos ∧ p₂ = s.endPos
-- Mathlib.RingTheory.Ideal.Operations
/-- `Submonoid.map` as an `AlgEquiv`, when applied to an `AlgEquiv`.  -/
Submodule.mapAlgEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A ≃ₐ[R] B) → Submodule R A ≃ₐ[Ideal R] Submodule R B
-- Mathlib.Algebra.BrauerGroup.Defs
IsBrauerEquivalent.trans : ∀ {K : Type u} [inst : Field K] {A : CSA K} {B : CSA K} {C : CSA K},
  IsBrauerEquivalent A B → IsBrauerEquivalent B C → IsBrauerEquivalent A C
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.natCast_add_one_cpow_ne_zero : ∀ (n : ℕ) (z : ℂ), (↑n + 1) ^ z ≠ 0
-- Aesop.Stats.Basic
Aesop.profilingForwardState : {m : Type → Type} → [Monad m] → [Aesop.MonadStats m] → [MonadLiftT BaseIO m] → {α : Type} → m α → m α
-- Mathlib.Util.AtomM
Mathlib.Tactic.AtomM.State.mk.injEq : ∀ (atoms atoms_1 : Array Lean.Expr), ({ atoms := atoms } = { atoms := atoms_1 }) = (atoms = atoms_1)
-- Lean.Util.Path
Lean.SearchPath.findAllWithExt : Lean.SearchPath → String → IO (Array System.FilePath)
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.instInhabitedEntry : Inhabited Lean.Compiler.CSimp.Entry
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instAdditiveFunctorOppositeAbToPresheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat},
  (PresheafOfModules.toPresheaf R).Additive
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.nhds_eq_update : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀],
  nhds = Function.update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), Filter.principal (Set.Iio γ))