mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivAt.snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G},
  HasFDerivAt f₂ f₂' x → HasFDerivAt (fun x => (f₂ x).2) (ContinuousLinearMap.snd 𝕜 F G ∘SL f₂') x
-- Std.Time.Format.Modifier
Std.Time.Modifier.q.sizeOf_spec : ∀ (presentation : Std.Time.Number ⊕ Std.Time.Text), sizeOf (Std.Time.Modifier.q presentation) = 1 + sizeOf presentation
-- Std.Http.Protocol.H1
/-- Rejects user-provided framing headers when framing must come from machine state.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.failOnFramingHeaders : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Order.Basic
forall_lt_imp_le_iff_le_of_dense : ∀ {α : Type u_2} [inst : LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α}, (∀ a < a₂, a ≤ a₁) ↔ a₂ ≤ a₁
-- Mathlib.Topology.Algebra.Monoid
/-- If `R` acts on `A` via `A`, then continuous multiplication implies continuous scalar
multiplication by constants.

Notably, this instance applies when `R = A`, or when `[Algebra R A]` is available.  -/
IsScalarTower.continuousConstSMul : ∀ {R : Type u_6} {A : Type u_7} [inst : Monoid A] [inst_1 : SMul R A] [IsScalarTower R A A]
  [inst_3 : TopologicalSpace A] [SeparatelyContinuousMul A], ContinuousConstSMul R A
-- Mathlib.Tactic.Positivity.Core
/-- A variation on `assumption` when the hypothesis is `e ≠ 0` or `0 ≠ e`.  -/
Mathlib.Meta.Positivity.compareHypNonzero : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      {pα? : Option Q(PartialOrder «$α»)} →
        (e : Q(«$α»)) → Lean.LocalDecl → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul : ∀ {k n : ℕ},
  n ≠ 0 → (ArithmeticFunction.sigma k) n = ∏ p ∈ n.primeFactors, ∑ i ∈ Finset.range (n.factorization p + 1), p ^ (i * k)
-- Init.Data.SInt.Bitwise
Int64.toInt16_xor : ∀ (a b : Int64), (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- `(G × H) / (A × B)` is in bijection with `G / A × H / B`.  -/
QuotientGroup.prodEquiv : {G : Type u} →
  [inst : Group G] →
    {H : Type v} → [inst_1 : Group H] → (A : Subgroup G) → (B : Subgroup H) → (G × H) ⧸ A.prod B ≃ (G ⧸ A) × H ⧸ B
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C),
  ((t.triangleLTGE n).obj j).mor₃ = (t.truncGEδLT n).app j
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma_normal : ∀ (N : ℕ), (CongruenceSubgroup.Gamma N).Normal
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] (m m_1 : Std.ExtHashMap α β), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.getKey! a = m_1.getKey! a_1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.iInf.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} [inst : Finite β] (f : β → L.BoundedFormula α n),
  FirstOrder.Language.BoundedFormula.iInf f = List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ (List.map f Finset.univ.toList)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instInfSet.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  AddSubgroup.instInfSet =
    {
      sInf := fun s =>
        let __src := (⨅ S ∈ s, S.toAddSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯;
        { toAddSubmonoid := __src, neg_mem' := ⋯ } }
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instAddMonoid : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → AddMonoid (MonoidAlgebra R M)
-- Mathlib.Data.Rat.Init
NNRat.cast_id : ∀ (n : ℚ≥0), ↑n = n
-- Init.Data.List.Basic
List.modifyTailIdx_succ_nil : ∀ {α : Type u} {f : List α → List α} {i : ℕ}, [].modifyTailIdx (i + 1) f = []
-- Mathlib.Data.Int.LeastGreatest
/-- A computable version of `exists_least_of_bdd`: given a decidable predicate on the
integers, with an explicit lower bound and a proof that it is somewhere true, return
the least value for which the predicate is true.  -/
Int.leastOfBdd : {P : ℤ → Prop} →
  [DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Abelian.Ext.mapExactFunctor_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] {X Y Z : C} {a b : ℕ} (α : CategoryTheory.Abelian.Ext X Y a)
  (β : CategoryTheory.Abelian.Ext Y Z b) {c : ℕ} (h : a + b = c),
  CategoryTheory.Abelian.Ext.mapExactFunctor F (α.comp β h) =
    (CategoryTheory.Abelian.Ext.mapExactFunctor F α).comp (CategoryTheory.Abelian.Ext.mapExactFunctor F β) h
-- Mathlib.Topology.Separation.Basic
eventuallyEq_insert : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s t : Set X} {x y : X},
  s =ᶠ[nhdsWithin x {y}ᶜ] t → insert x s =ᶠ[nhds x] insert x t
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.smul_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_3 : Semiring R] [inst_4 : CategoryTheory.Linear R C]
  [inst_5 : ∀ (n : ℤ), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C n)] (n : R) (f : T₁ ⟶ T₂),
  (n • f).hom₃ = n • f.hom₃
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_inv_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.mop =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor { unmop := X }).inv
-- Lean.Elab.Tactic.ElabTerm
/-- Elaborate `stx` in the current `MVarContext`. If given, the `expectedType` will be used to help
elaboration but not enforced (use `elabTermEnsuringType` to enforce an expected type).  -/
Lean.Elab.Tactic.elabTerm : Lean.Syntax → Option Lean.Expr → optParam Bool false → Lean.Elab.Tactic.TacticM Lean.Expr
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Scheme.toSpecΓ_appTop : ∀ (X : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.Hom.appTop X.toSpecΓ =
    (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op ⊤))).hom
-- Mathlib.Topology.Algebra.Constructions
AddUnits.instTopologicalSpaceAddUnits.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M],
  AddUnits.instTopologicalSpaceAddUnits = TopologicalSpace.induced (⇑(AddUnits.embedProduct M)) inferInstance
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The domain of a normalized 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.NormalizedHom.src : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Obj
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.eq_inv_of_inv_hom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : Y ⟶ X} [inst_1 : CategoryTheory.IsIso f]
  {g : X ⟶ Y}, CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X → g = CategoryTheory.inv f
-- Mathlib.Topology.ContinuousOn
/-- Variant of `ContinuousOn.comp` using the form `fun y ↦ g (f y)` instead of `g ∘ f`.  -/
ContinuousOn.comp' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β},
  ContinuousOn g t → ContinuousOn f s → Set.MapsTo f s t → ContinuousOn (fun x => g (f x)) s
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.instPartialOrder : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} → [inst : Topology.RelCWComplex C D] → PartialOrder (Topology.RelCWComplex.Subcomplex C)
-- Mathlib.Logic.Basic
xor_iff_iff_not : ∀ {a b : Prop}, Xor a b ↔ (a ↔ ¬b)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.instInfSet : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] → {𝒜 : ι → σ} → [inst_5 : GradedRing 𝒜] → InfSet (HomogeneousIdeal 𝒜)
-- Mathlib.Data.Nat.Cast.WithTop
instWellFoundedRelationWithTopNat : WellFoundedRelation (WithTop ℕ)
-- Mathlib.Data.Tree.Get
/-- **Alias** of `BinaryTree.indexOf`.  -/
Tree.indexOf : {α : Type u_1} → (lt : α → α → Prop) → [DecidableRel lt] → α → Tree α → Option PosNum
-- Init.Data.List.ControlImpl
List.flatMapM.loop.induct_unfolding : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (List β))
  (motive : List α → List (List β) → m (List β) → Prop),
  (∀ (bs : List (List β)), motive [] bs (pure bs.reverse.flatten)) →
    (∀ (a : α) (as : List α) (bs : List (List β)),
        (∀ (bs' : List β), motive as (bs' :: bs) (List.flatMapM.loop f as (bs' :: bs))) →
          motive (a :: as) bs do
            let bs' ← f a
            List.flatMapM.loop f as (bs' :: bs)) →
      ∀ (x : List α) (x_1 : List (List β)), motive x x_1 (List.flatMapM.loop f x x_1)
-- Mathlib.Analysis.InnerProductSpace.PiL2
Orthonormal.exists_orthonormalBasis_extension_of_card_eq : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {ι : Type u_7} [inst_4 : Fintype ι],
  Module.finrank 𝕜 E = Fintype.card ι →
    ∀ {v : ι → E} {s : Set ι}, Orthonormal 𝕜 (s.domRestrict v) → ∃ b, ∀ i ∈ s, b i = v i
-- Mathlib.Logic.Equiv.Prod
/-- A subtype of a `Prod` that depends only on the first component is equivalent to the
corresponding subtype of the first type times the second type.  -/
Equiv.prodSubtypeFstEquivSubtypeProd : {α : Type u_9} → {β : Type u_10} → {p : α → Prop} → { s // p s.1 } ≃ { a // p a } × β
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.instNonemptyStrictLimitsClosureStep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] [P.Nonempty],
  (P.strictLimitsClosureStep J).Nonempty
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instFullMonForget₂Mon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.AddGrp.forget₂Mon C).Full
-- Init.Data.Fin.Lemmas
Fin.pred_castSucc_succ : ∀ {n : ℕ} (i : Fin n), i.succ.castSucc.pred ⋯ = i.castSucc
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForDiagnosticsParams.mk : Lean.Lsp.DocumentUri → ℕ → Lean.Lsp.WaitForDiagnosticsParams
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- The submonoid generated by a set includes the set.  -/
Submonoid.subset_closure : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M}, s ⊆ ↑(Submonoid.closure s)
-- Init.Data.String.PosRaw
/-- Decreases the byte offset of the position by `1`. Not to be confused with `Pos.prev`.  -/
String.Pos.Raw.dec : String.Pos.Raw → String.Pos.Raw
-- Mathlib.Analysis.BoxIntegral.Basic
/-- The predicate `HasIntegral I l f vol y` says that `y` is the integral of `f` over `I` along `l`
w.r.t. volume `vol`. This means that integral sums of `f` tend to `𝓝 y` along
`BoxIntegral.IntegrationParams.toFilteriUnion I ⊤`.  -/
BoxIntegral.HasIntegral : {ι : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [Fintype ι] →
                BoxIntegral.Box ι →
                  BoxIntegral.IntegrationParams → ((ι → ℝ) → E) → BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤ → F → Prop
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- The support of a graded object with respect to finite rank:
the set of indices where the rank is nonzero.  -/
GradedObject.finrankSupport : {R : Type u_1} → [inst : Ring R] → {ι : Type u_2} → CategoryTheory.GradedObject ι (ModuleCat R) → Set ι
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.tensor_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {W X Y Z : C} (f : W ⟶ X),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f 0 = 0
-- Mathlib.GroupTheory.Index
AddSubgroup.index.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.index = Nat.card (G ⧸ H)
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.separable_minpoly : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsSeparable K L]
  (c : ConjRootClass K L), c.minpoly.Separable
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.finiteCoproduct.ι_desc_apply : ∀ {P : TopCat → Prop} {α : Type w} [inst : Finite α] (X : α → CompHausLike P)
  [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] {B : CompHausLike P} {π : (a : α) → X a ⟶ B} (a : α)
  (x : (fun X => ↑X.toTop) (X a)),
  (CategoryTheory.ConcreteCategory.hom (CompHausLike.finiteCoproduct.desc X π))
      ((CategoryTheory.ConcreteCategory.hom (CompHausLike.finiteCoproduct.ι X a)) x) =
    (CategoryTheory.ConcreteCategory.hom (π a)) x
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.subsingleton_of_isZero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
  CategoryTheory.Limits.IsZero X → Subsingleton (CategoryTheory.Subobject X)
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → α} {s : Set α},
  MeasureTheory.MeasurePreserving f μ μ →
    MeasureTheory.NullMeasurableSet s μ → ∀ (n : ℕ), μ (symmDiff s (f^[n] ⁻¹' s)) ≤ n • μ (symmDiff s (f ⁻¹' s))
-- Aesop.RuleSet
_private.Aesop.RuleSet.0.Aesop.BaseRuleSet.add.addRulePattern : Aesop.RuleName → Option Aesop.RulePattern → Aesop.BaseRuleSet → Aesop.BaseRuleSet
-- Mathlib.Algebra.Module.Bimodule
Subbimodule.smul_mem' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Module A M] [inst_6 : Module B M]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M] (p : Submodule (TensorProduct R A B) M) (b : B) {m : M}, m ∈ p → b • m ∈ p
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_erase_eq_iff_not_compare_eq_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (t.erase k).maxKey he = t.maxKey ⋯ ↔ ¬cmp k (t.maxKey ⋯) = Ordering.eq
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.toOpenPartialHomeomorph_trivialization_symm_apply : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (v : B × F),
  ↑(Bundle.Trivial.trivialization B F).symm v = ⟨v.1, v.2⟩
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.cofan_inj_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  (n : ℕ),
  (s.cofan (Opposite.op { len := n })).inj
      (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })) =
    s.ι n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ordCompare_maxKey_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtTreeMap α β compare} {k : α}
  {f : β → β} {he : t.modify k f ≠ ∅}, compare ((t.modify k f).maxKey he) (t.maxKey ⋯) = Ordering.eq
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.isNat_minFac_1 : ∀ {a : ℕ}, Mathlib.Meta.NormNum.IsNat a 1 → Mathlib.Meta.NormNum.IsNat a.minFac 1
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- Turn a morphism in `CommAlgCat` back into an `AlgHom`.  -/
CommAlgCat.Hom.hom : {R : Type u} → [inst : CommRing R] → {A B : CommAlgCat R} → A.Hom B → ↑A →ₐ[R] ↑B
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift_comp_zero_cochain : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L M : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n')
  (γ' : CochainComplex.HomComplex.Cochain L M 0), (γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯
-- Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
/-- The recurrence relation for the convergents of the continued fraction expansion
of an element `v` of `K` in terms of the convergents of the inverse of its fractional part.
 -/
GenContFract.convs_succ : ∀ {K : Type u_1} (v : K) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorRing K]
  (n : ℕ), (GenContFract.of v).convs (n + 1) = ↑⌊v⌋ + 1 / (GenContFract.of (Int.fract v)⁻¹).convs n
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.piAntidiag_empty : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] (n : μ), ∅.piAntidiag n = if n = 0 then {0} else ∅
-- Mathlib.ModelTheory.Quotients
FirstOrder.Language.relMap_quotient_mk' : ∀ {L : FirstOrder.Language} {M : Type u_1} (s : Setoid M) [ps : L.Prestructure s] {n : ℕ} (r : L.Relations n)
  (x : Fin n → M), (FirstOrder.Language.Structure.RelMap r fun i => ⟦x i⟧) ↔ FirstOrder.Language.Structure.RelMap r x
-- Lean.DocString.Syntax
Lean.Doc.Syntax.desc_item.quot : Lean.ParserDescr
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  {e e' : F.RepresentableBy Y},
  e = e' ↔ e.homEquiv (CategoryTheory.CategoryStruct.id Y) = e'.homEquiv (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.coe_ofIsClosedGraph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {g : E →ₗ[𝕜] F} (hg : IsClosed ↑g.graph),
  ↑(ContinuousLinearMap.ofIsClosedGraph hg) = g
-- Mathlib.Topology.Maps.Basic
/-- **Alias** of `Topology.IsEmbedding.of_leftInverse`. -/
Function.LeftInverse.isEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {g : Y → X},
  Function.LeftInverse f g → Continuous f → Continuous g → Topology.IsEmbedding g
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
/-- **Alias** of `TensorProduct.restrictScalar_directSumRight`. -/
TensorProduct.directSumRight'_restrict : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_2) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₂ : Type v₂}
  [inst_3 : DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [inst_4 : AddCommMonoid M₁']
  [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [inst_6 : Module R M₁'] [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_8 : Module S M₁'] [inst_9 : IsScalarTower R S M₁'] (S₀ : Type u_1) [inst_10 : CommSemiring S₀]
  [inst_11 : Algebra R S₀] [inst_12 : Algebra S₀ S] [inst_13 : Module S₀ M₁'] [inst_14 : IsScalarTower R S₀ M₁']
  [inst_15 : IsScalarTower S₀ S M₁'],
  LinearEquiv.restrictScalars S₀ (TensorProduct.directSumRight R S M₁' M₂) = TensorProduct.directSumRight R S₀ M₁' M₂
-- Mathlib.Data.List.Basic
List.map_rightInverse_iff : ∀ {α : Type u} {β : Type v} {f : α → β} {g : β → α},
  Function.RightInverse (List.map f) (List.map g) ↔ Function.RightInverse f g
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Given a bijective function, there is an isomorphism from a graph into the mapped graph.  -/
SimpleGraph.Iso.map : {V : Type u_1} → {W : Type u_2} → (f : V ≃ W) → (G : SimpleGraph V) → G ≃g SimpleGraph.map (⇑f) G
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn : ∀ {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M]
  (φ : OpenPartialHomeomorph M H),
  ContMDiffOn I I n (↑φ) φ.source → ContMDiffOn I I n (↑φ.symm) φ.target → φ ∈ IsManifold.maximalAtlas I n M
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- `lp.single` as a continuous linear map.  -/
lp.singleContinuousLinearMap : (𝕜 : Type u_1) →
  {α : Type u_3} →
    (E : α → Type u_4) →
      (p : ENNReal) →
        [inst : (i : α) → NormedAddCommGroup (E i)] →
          [inst_1 : NormedRing 𝕜] →
            [inst_2 : (i : α) → Module 𝕜 (E i)] →
              [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] →
                [DecidableEq α] → [inst_5 : Fact (1 ≤ p)] → (i : α) → E i →L[𝕜] ↥(lp E p)
-- Mathlib.Tactic.Simps.Basic
/-- `update nm s isPrefix` adds `s` to the last component of `nm`,
either as prefix or as suffix (specified by `isPrefix`).
Used by `simps_add_projections`.  -/
_private.Mathlib.Tactic.Simps.Basic.0.NameStruct.update : NameStruct✝ → String → optParam Bool false → NameStruct✝
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_iSup : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] {ι : Sort u_2}
  {I : Submodule R A} {t : ι → Submodule R M}, I • ⨆ i, t i = ⨆ i, I • t i
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.exp_decay_sub_atImInfty : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f →
        UpperHalfPlane.IsBoundedAtImInfty f →
          (fun τ => f τ - UpperHalfPlane.valueAtInfty f) =O[UpperHalfPlane.atImInfty] fun τ =>
            Real.exp (-2 * Real.pi * τ.im / h)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁],
  (CategoryTheory.Pretriangulated.productTriangle T).obj₃ = ∏ᶜ fun j => (T j).obj₃