mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_4.congr_eq_4 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) (a b : Lean.Grind.CommRing.Expr),
  x = a.mul b →
    (match x with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | a.add b => h_3 a b
      | a.mul b => h_4 a b
      | a.pow k => h_5 a k
      | Lean.Grind.CommRing.Expr.natCast n => h_6 n
      | a.sub b => h_7 a b
      | a.neg => h_8 a
      | Lean.Grind.CommRing.Expr.intCast k => h_9 k) ≍
      h_4 a b
-- Mathlib.Analysis.Normed.Module.Completion
UniformSpace.Completion.instNormedRing : (A : Type u_3) → [inst : SeminormedRing A] → NormedRing (UniformSpace.Completion A)
-- Std.Tactic.Do.Syntax
/-- `mpure_intro` operates on a stateful `Std.Do.SPred` goal of the form `P ⊢ₛ ⌜φ⌝`.
It leaves the stateful proof mode (thereby discarding `P`), leaving the regular goal `φ`.
```lean
theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by
  mpure_intro
  exact True.intro
```
 -/
Lean.Parser.Tactic.mpureIntro : Lean.ParserDescr
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalApply : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_span : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A},
  Algebra.adjoin R ↑(Submodule.span R s) = Algebra.adjoin R s
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.norm_def : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F),
  ‖f‖ = sInf {c | 0 ≤ c ∧ ∀ (m : ι → E), ‖f m‖ ≤ c * ∏ i, ‖m i‖}
-- Mathlib.Tactic.Order.Graph.Tarjan
Mathlib.Tactic.Order.Graph.TarjanState.toDFSState : Mathlib.Tactic.Order.Graph.TarjanState → Mathlib.Tactic.Order.Graph.DFSState
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RooSliceData.mk : {α : Type u} →
  [inst : Ord α] → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Std.Roo α → Std.DTreeMap.Internal.Unit.RooSliceData α
-- Init.Data.Nat.Gcd
Nat.gcd_pos_iff : ∀ {m n : ℕ}, 0 < m.gcd n ↔ 0 < m ∨ 0 < n
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.mk.injEq : ∀ {R : Type u_1} (val val_1 : R), ({ val := val } = { val := val_1 }) = (val = val_1)
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_lt_iff_slt : ∀ (a b : BitVec System.Platform.numBits), ISize.ofBitVec a < ISize.ofBitVec b ↔ a.slt b = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (List.map Sigma.fst l).contains k = false → (t.insertMany l).getKey! k = t.getKey! k
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The difference of two `C^n` functions at a point is `C^n` at this point.  -/
ContDiffAt.sub : ∀ {𝕜 : 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] {x : E}
  {n : WithTop ℕ∞} {f g : E → F}, ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → ContDiffAt 𝕜 n (fun x => f x - g x) x
-- Batteries.Data.HashMap.Basic
/-- Combines two hashmaps using function `f` to combine two values at a key.
```
mergeWith (fun _ v₁ v₂ => v₁ + v₂ )
  (ofList [("one", 1), ("two", 2)]) (ofList [("two", 2), ("three", 3)]) =
    {"one" => 1, "two" => 4, "three" => 3}
```
 -/
Batteries.HashMap.mergeWith : {α : Type u_1} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {β : Type u_2} → (α → β → β → β) → Batteries.HashMap α β → Batteries.HashMap α β → Batteries.HashMap α β
-- Mathlib.Analysis.RCLike.Extend
StrongDual.im_extendRCLike_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (g : StrongDual ℝ F) (x : F), RCLike.im (g.extendRCLike x) = -g (RCLike.I • x)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.rankPos : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsNonloop e → M.RankPos
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.continuous_coe : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)],
  Continuous DFunLike.coe
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.toMultiplicative : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_4)
  [inst_2 : AddGroup G] [inst_3 : AddAction G E],
  IsAddQuotientCoveringMap f G → IsQuotientCoveringMap f (Multiplicative G)
-- Mathlib.Data.Set.Function
Set.BijOn.image_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → f '' s = t
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.of_mul : ∀ {α : Type u} [inst : Mul α] (x y : α), FreeAbelianGroup.of (x * y) = FreeAbelianGroup.of x * FreeAbelianGroup.of y
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.ind : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {motive : ArchimedeanClass.FiniteResidueField K → Prop},
  (∀ (x : ArchimedeanClass.FiniteElement K), motive (ArchimedeanClass.FiniteResidueField.mk x)) →
    ∀ (x : ArchimedeanClass.FiniteResidueField K), motive x
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.doublingGamma_one : Real.doublingGamma 1 = 1
-- Mathlib.Algebra.Group.Basic
zsmul_neg : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℤ), n • -a = -(n • a)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.incSteps : optParam ℕ 1 → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_X : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.X.eraseLead = 0
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.instIsEmptyOfSubsingleton : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [Subsingleton M], IsEmpty (LieModule.Weight R L M)
-- Mathlib.Algebra.Group.End
Equiv.Perm.trans_one : ∀ {α : Sort u_7} {β : Type u_8} (e : α ≃ β), e.trans 1 = e
-- Mathlib.GroupTheory.Nilpotent
/-- A sequence of additive subgroups of `G` is a descending central series if `H 0` is
`G` and `⁅H n, G⁆ ⊆ H (n + 1)` for all `n`. We do not require that `H n = {1}` for some `n`.  -/
AddSubgroup.IsDescendingCentralSeries : {G : Type u_1} → [inst : AddGroup G] → (ℕ → AddSubgroup G) → Prop
-- Mathlib.GroupTheory.Perm.Centralizer
/-- Given `a : g.Basis` and a permutation of `g.cycleFactorsFinset` that
preserve the lengths of the cycles, a permutation of `α` that
moves the `Basis` and commutes with `g`  -/
Equiv.Perm.Basis.ofPermHom : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] →
      {g : Equiv.Perm α} → g.Basis → ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g) →* Equiv.Perm α
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.isNilpotent_iff_mem_nonunits : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] [IsLocalRing R] {x : R}, IsNilpotent x ↔ x ∈ nonunits R
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit_desc_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra}
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor]
  [inst_3 : CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor]
  (s : CategoryTheory.Limits.Cocone D),
  ((CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit c t).desc s).f = t.desc (T.forget.mapCocone s)
-- Init.Data.Iterators.Consumers.Monadic.Collect
/-- Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.

This function is deprecated. Instead of `it.allowNontermination.toListRev`, use `it.toListRev`.
 -/
Std.IterM.Partial.toListRev : {α : Type w} →
  {m : Type w → Type w'} → [Monad m] → {β : Type w} → [Std.Iterator α m β] → Std.IterM.Partial m β → m (List β)
-- Aesop.Tree.ExtractProof
Aesop.Goal.extractSafePrefix : Aesop.Goal → Lean.MetaM (Array Lean.MVarId)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_isBasis_iff : ∀ {α : Type u_1} {E I X : Set α}, (Matroid.freeOn E).IsBasis I X ↔ I = X ∧ X ⊆ E
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ModuleDocstringState.mk.sizeOf_spec : ∀ (toState : Lean.Doc.State)
  (scopedExts : Array (Lean.ScopedEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState)),
  sizeOf { toState := toState, scopedExts := scopedExts } = 1 + sizeOf toState + sizeOf scopedExts
-- Mathlib.Data.Rel
SetRel.core_inter : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t₁ t₂ : Set β), R.core (t₁ ∩ t₂) = R.core t₁ ∩ R.core t₂
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.brecOn.eq : ∀ {motive : Nat.Internal.SOM.Expr → Sort u} (t : Nat.Internal.SOM.Expr)
  (F_1 : (t : Nat.Internal.SOM.Expr) → Nat.Internal.SOM.Expr.below t → motive t),
  Nat.Internal.SOM.Expr.brecOn t F_1 = F_1 t (Nat.Internal.SOM.Expr.brecOn.go t F_1).2
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.Over.over : {S : AlgebraicGeometry.Scheme} →
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
    {inst : P.IsStableUnderBaseChange} →
      {inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P} →
        {X : AlgebraicGeometry.Scheme} →
          {inst_2 : X.Over S} →
            {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X} →
              [self : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] → (j : 𝒰.I₀) → (𝒰.X j).Over S
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Push forward a `CommGroupWithZero` along a surjective function.
See note [reducible non-instances].  -/
Function.Surjective.commGroupWithZero : {G₀ : Type u_2} →
  {G₀' : Type u_4} →
    [inst : CommGroupWithZero G₀] →
      [inst_1 : Zero G₀'] →
        [inst_2 : Mul G₀'] →
          [inst_3 : One G₀'] →
            [inst_4 : Inv G₀'] →
              [inst_5 : Div G₀'] →
                [inst_6 : Pow G₀' ℕ] →
                  [inst_7 : Pow G₀' ℤ] →
                    0 ≠ 1 →
                      (f : G₀ → G₀') →
                        Function.Surjective f →
                          f 0 = 0 →
                            f 1 = 1 →
                              (∀ (x y : G₀), f (x * y) = f x * f y) →
                                (∀ (x : G₀), f x⁻¹ = (f x)⁻¹) →
                                  (∀ (x y : G₀), f (x / y) = f x / f y) →
                                    (∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n) →
                                      (∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n) → CommGroupWithZero G₀'
-- Mathlib.Order.Hom.WithTopBot
OrderHom.withBotMap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β),
  f.withBotMap = { toFun := WithBot.map ⇑f, monotone' := ⋯ }
-- Mathlib.GroupTheory.GroupExtension.Defs
SemidirectProduct.toGroupExtension_rightHom : ∀ {N : Type u_1} {G : Type u_3} [inst : Group G] [inst_1 : Group N] (φ : G →* MulAut N),
  (SemidirectProduct.toGroupExtension φ).rightHom = SemidirectProduct.rightHom
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.inter : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsLocalMinOn f s a → ∀ (t : Set α), IsLocalMinOn f (s ∩ t) a
-- Mathlib.Topology.Order.Monotone
/-- An antitone function `f` sending `top` to `bot` and continuous at the infimum of a set sends
this infimum to the supremum of the image of this set.  -/
AntitoneOn.map_sInf_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α},
  ContinuousWithinAt f s (sInf s) → AntitoneOn f s → f ⊤ = ⊥ → f (sInf s) = sSup (f '' s)
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.State.mk.injEq : ∀ (seen : Lean.NameMap (Array Lean.Name)) (axioms : Lean.NameSet) (seen_1 : Lean.NameMap (Array Lean.Name))
  (axioms_1 : Lean.NameSet),
  ({ seen := seen, axioms := axioms } = { seen := seen_1, axioms := axioms_1 }) = (seen = seen_1 ∧ axioms = axioms_1)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.not_rankFinite_iff : ∀ {α : Type u_1} (M : Matroid α), ¬M.RankFinite ↔ M.RankInfinite
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_hom_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : C) (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_hom_app._auto_1) {Z : Cᵒᵖᵒᵖ}
  (h : (CategoryTheory.shiftFunctor Cᵒᵖᵒᵖ n).obj ((CategoryTheory.opOp C).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso C n).hom.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app (Opposite.op X)).op
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app (Opposite.op (Opposite.op X))) h)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instMin.eq_1 : ∀ {M : Type u_1} [inst : Add M],
  AddSubsemigroup.instMin = { min := fun S₁ S₂ => { carrier := ↑S₁ ∩ ↑S₂, add_mem' := ⋯ } }
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.cancel_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {g₁ g₂ : β →ᵈ γ} {f : α →ᵈ β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Data.Fintype.Sort
finSumEquivOfFinset_inr : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] [inst_2 : LinearOrder α] {m n : ℕ} {s : Finset α}
  (hm : s.card = m) (hn : sᶜ.card = n) (i : Fin n), (finSumEquivOfFinset hm hn) (Sum.inr i) = (sᶜ.orderEmbOfFin hn) i
-- Mathlib.CategoryTheory.DifferentialObject
/-- The shift by zero is naturally isomorphic to the identity.  -/
CategoryTheory.DifferentialObject.shiftZero : {S : Type u_1} →
  [inst : AddCommGroupWithOne S] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            CategoryTheory.DifferentialObject.shiftFunctor C 0 ≅
              CategoryTheory.Functor.id (CategoryTheory.DifferentialObject S C)
-- Mathlib.Geometry.Convex.Cone.Basic
Submodule.mem_toConvexCone : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {C : Submodule R M} {x : M}, x ∈ C.toConvexCone ↔ x ∈ C
-- Mathlib.Topology.Path
/-- Pointwise negation of paths in a topological group.  -/
Path.neg : {X : Type u_1} →
  [inst : TopologicalSpace X] → {a b : X} → [inst_1 : Neg X] → [ContinuousNeg X] → Path a b → Path (-a) (-b)
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the forward direction of `isMinOn_dual_iff`. -/
IsMinOn.undual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMinOn (⇑OrderDual.toDual ∘ f) s a → IsMaxOn f s a
-- Init.Core
Std.LawfulIdentity.toIdentity : ∀ {α : Sort u} {op : α → α → α} {o : outParam α} [self : Std.LawfulIdentity op o], Std.Identity op o
-- Mathlib.Order.RelSeries
RelSeries.tail.congr_simp : ∀ {α : Type u_1} {r : SetRel α α} (p p_1 : RelSeries r) (e_p : p = p_1) (len_pos : p.length ≠ 0),
  p.tail len_pos = p_1.tail ⋯
-- Mathlib.Topology.VectorBundle.Hom
continuousAt_hom_bundle : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] [inst_13 : (x : B) → TopologicalSpace (E₁ x)] [inst_14 : FiberBundle F₁ E₁]
  [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂]
  [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ] {M : Type u_8}
  [inst_22 : TopologicalSpace M] (f : M → Bundle.TotalSpace (F₁ →SL[σ] F₂) fun x => E₁ x →SL[σ] E₂ x) {x₀ : M},
  ContinuousAt f x₀ ↔
    ContinuousAt (fun x => (f x).proj) x₀ ∧
      ContinuousAt
        (fun x => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
        x₀
-- Mathlib.Computability.NFA
NFA.Path.supp.eq_1 : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} [inst : DecidableEq σ] {t : σ}, (NFA.Path.nil t).supp = {t}
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.map_comp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι}
  (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') {i'' j'' k'' l'' : ι} (f₁'' : i'' ⟶ j'') (f₂'' : j'' ⟶ k'')
  (f₃'' : k'' ⟶ l'')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃' ⟶ CategoryTheory.ComposableArrows.mk₃ f₁'' f₂'' f₃'')
  (n₀ n₁ n₂ : ℤ) (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.map_comp._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.map_comp._auto_3),
  X.map f₁ f₂ f₃ f₁'' f₂'' f₃'' (CategoryTheory.CategoryStruct.comp α β) n₀ n₁ n₂ hn₁ hn₂ =
    CategoryTheory.CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)
      (X.map f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂)
-- Lean.Meta.Sym.SymM
/-- Returns initial state for all registered extensions.  -/
Lean.Meta.Sym.SymExtensions.mkInitialStates : IO (Array Lean.Meta.Sym.SymExtensionState)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.uncurry.obj F)]
  [inst_5 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C}
  (h : (F.obj j).obj k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.uncurry.obj F) (j, k)) h
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- If `Q` is a property of ring maps that can be checked on prime ideals, the
associated property of scheme morphisms can be checked on stalks.  -/
AlgebraicGeometry.HasRingHomProperty.of_stalkMap : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (RingHom.OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] => Q) →
    (∀ (x : ↥X), Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))) → P f
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
/-- A set is called stationary when it intersects all club sets.  -/
IsStationary : {α : Type v} → [LinearOrder α] → Set α → Prop
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.conjTranspose : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {M : Matrix n n R},
  M.PosDef → M.conjTranspose.PosDef
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `Left.inv_lt_one_iff`.

---

Uses `left` co(ntra)variant.  -/
one_lt_of_inv_lt_one : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a : α}, a⁻¹ < 1 → 1 < a
-- Init.Data.Order.Ord
Std.OrientedCmp.isGE_antisymm : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α},
  (cmp a b).isGE = true → (cmp b a).isGE = true → cmp a b = Ordering.eq
-- Aesop.Rule
Aesop.RegularRule.successProbability : Aesop.RegularRule → Aesop.Percent
-- Init.Data.Array.Extract
Array.popWhile_replicate_eq_filter_not : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool},
  Array.popWhile p (Array.replicate n a) = Array.filter (fun a => !p a) (Array.replicate n a)
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WP.mk : {Prog : Type u} →
  {Value : outParam (Type v)} →
    {Pred : outParam (Type w)} →
      {EPred : outParam (Type w')} →
        [inst : Std.Internal.Do.Assertion Pred] →
          [inst_1 : Std.Internal.Do.Assertion EPred] →
            (wpTrans : Prog → Std.Internal.Do.PredTrans Pred EPred Value) →
              (∀ (x : Prog), (wpTrans x).monotone) → Std.Internal.Do.WP Prog Value Pred EPred
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
/-- Abbreviation for face maps in the 2-truncated simplex category.  -/
SimplexCategory.Truncated.σ₂ : {n : ℕ} →
  Fin (n + 1) →
    (hn : autoParam ({ len := n + 1 }.len ≤ 2) SimplexCategory.Truncated.σ₂._auto_1) →
      (hn' : autoParam ({ len := n }.len ≤ 2) SimplexCategory.Truncated.σ₂._auto_3) →
        { obj := { len := n + 1 }, property := hn } ⟶ { obj := { len := n }, property := hn' }
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- The morphism of modules `(free R).obj X ⟶ M` corresponding
to a map `f : X ⟶ M`.  -/
ModuleCat.freeDesc : {R : Type u} → [inst : Ring R] → {X : Type u} → {M : ModuleCat R} → (X ⟶ ↑M) → ((ModuleCat.free R).obj X ⟶ M)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- The functor from `C` to `Under X` which sends `Y : C` to `in₁ : X ⟶ X ⨿ Y`.  -/
CategoryTheory.Under.costar : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) → [CategoryTheory.Limits.HasBinaryCoproducts C] → CategoryTheory.Functor C (CategoryTheory.Under X)