mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.lift_app : ∀ {X Y U : AlgebraicGeometry.Scheme} (f : U ⟶ Y) (g : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f]
  (H : Set.range ⇑g ⊆ Set.range ⇑f) (V : U.Opens),
  AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.IsOpenImmersion.lift f g H) V =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f V).inv
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.app g ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj V))
        (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopic.prodMk : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(X, Z)},
  f₀.Homotopic f₁ → g₀.Homotopic g₁ → (f₀.prodMk g₀).Homotopic (f₁.prodMk g₁)
-- Mathlib.Algebra.Group.Submonoid.Finite
Submonoid.pi_mem_of_mulSingle_mem : ∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → MulOneClass (f i)] {S : Type u_3}
  [inst_1 : SetLike S ((i : η) → f i)] [SubmonoidClass S ((i : η) → f i)] [Finite η] [inst_4 : DecidableEq η] {H : S}
  (x : (i : η) → f i), (∀ (i : η), Pi.mulSingle i (x i) ∈ H) → x ∈ H
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.add_sum_Ioc_eq_sum_Icc : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a ≤ b → f a + ∑ x ∈ Finset.Ioc a b, f x = ∑ x ∈ Finset.Icc a b, f x
-- Init.Data.Bool
Bool.bne_not : ∀ (a b : Bool), (a != !b) = !a != b
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanIso.add_eq_add : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsAddFreimanIso 2 A B f → ∀ {a b c d : α}, a ∈ A → b ∈ A → c ∈ A → d ∈ A → (f a + f b = f c + f d ↔ a + b = c + d)
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.foldlM : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type w'} → [Monad m] → (δ → (a : α) → β a → m δ) → δ → Std.DHashMap.Internal.AssocList α β → m δ
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.assignGeneralizedPatternProof : Lean.MVarId →
  Lean.Expr → Lean.Meta.Grind.Origin → OptionT (StateT Lean.Meta.Grind.EMatch.Choice Lean.Meta.Grind.EMatch.M) Unit
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instNormedStarGroupSubtypePreLpMemAddSubgroup : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : (i : α) → StarAddMonoid (E i)] [inst_2 : ∀ (i : α), NormedStarGroup (E i)] [hp : Fact (1 ≤ p)],
  NormedStarGroup ↥(lp E p)
-- Init.Control.ExceptCps
ExceptCpsT.runK_throw : ∀ {m : Type u_1 → Type u_2} {ε β : Type u_1} {e s : ε} {a : Type u_1} {ok : β → m a} {error : ε → m a} [Monad m],
  (throw e).runK s ok error = error e
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Multiset.Nat.antidiagonalTuple_two : ∀ (n : ℕ), Multiset.Nat.antidiagonalTuple 2 n = Multiset.map (fun i => ![i.1, i.2]) (Multiset.Nat.antidiagonal n)
-- Mathlib.Combinatorics.Quiver.SingleObj
/-- Equip `SingleObj α` with an involutive reverse operation.  -/
Quiver.SingleObj.hasInvolutiveReverse : {α : Type u_1} → (rev : α → α) → Function.Involutive rev → Quiver.HasInvolutiveReverse (Quiver.SingleObj α)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {f g : 𝕜 → F},
        ContDiffWithinAt 𝕜 (↑n) f s x →
          ContDiffWithinAt 𝕜 (↑n) g s x →
            iteratedDerivWithin n (fun z => f z + g z) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Given a fork `s` on morphisms `f, g : X ⟶ Y` and a pullback cone `c` on `s.ι : s.pt ⟶ X` and a
morphism `h : Z ⟶ X`, the projection `c.snd : c.pt ⟶ Z` induces a fork on `h ≫ f` and `h ≫ g`.
```
c.pt → Z
|      |
v      v
s.pt → X ⇉ Y
```
 -/
CategoryTheory.Limits.precompFork : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {Z : C} →
          (h : Z ⟶ X) →
            (s : CategoryTheory.Limits.Fork f g) →
              CategoryTheory.Limits.PullbackCone s.ι h →
                CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.comp h f)
                  (CategoryTheory.CategoryStruct.comp h g)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_I : Complex.I.arg = Real.pi / 2
-- Lean.Util.Trace
/-- Thread ID, used by `trace.profiler.output`.  -/
Lean.TraceState.tid : Lean.TraceState → UInt64
-- Init.Data.BitVec.Lemmas
BitVec.toFin_sshiftRight_of_msb_true : ∀ {w : ℕ} {x : BitVec w} {n : ℕ},
  x.msb = true → (x.sshiftRight n).toFin = Fin.ofNat (2 ^ w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n)
-- Init.Data.List.Nat.InsertIdx
List.eraseIdx_insertIdx_self : ∀ {α : Type u} {i : ℕ} {l : List α} (a : α), (l.insertIdx i a).eraseIdx i = l
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNorm_mul_le : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R],
  ‖ContinuousLinearMap.mul 𝕜 R‖ ≤ 1
-- Mathlib.Tactic.TacticAnalysis
/-- This tactic is allowed to fail because it is in a `try`/`anyGoals`/etc block.  -/
Mathlib.TacticAnalysis.TacticNode.mayFail : Mathlib.TacticAnalysis.TacticNode → Bool
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.mk.congr_simp : ∀ (coe coe_1 : ℂ) (e_coe : coe = coe_1) (coe_im_pos : 0 < coe.im),
  { coe := coe, coe_im_pos := coe_im_pos } = { coe := coe_1, coe_im_pos := ⋯ }
-- Mathlib.RingTheory.Adjoin.Field
/-- The `RingHom` version of `IsIntegral.minpoly_splits_tower_top`.  -/
IsIntegral.minpoly_splits_tower_top' : ∀ {R : Type u_1} {K : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : CommRing M] [inst_4 : Algebra R K] [inst_5 : Algebra R M] [inst_6 : Algebra K M] [IsScalarTower R K M]
  {x : M},
  IsIntegral R x →
    ∀ {f : K →+* L},
      (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits → (Polynomial.map f (minpoly K x)).Splits
-- Mathlib.Lean.Expr.Basic
/-- Checks whether this `ConstantInfo` is a definition.  -/
Lean.ConstantInfo.isDef : Lean.ConstantInfo → Bool
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.comap_symm : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₁),
  AffineSubspace.comap (↑e.symm) s = AffineSubspace.map (↑e) s
-- Mathlib.LinearAlgebra.Matrix.Orthogonal
/-- `A.HasOrthogonalCols` means matrix `A` has orthogonal columns (with respect to
`dotProduct`).  -/
Matrix.HasOrthogonalCols : {α : Type u_1} → {n : Type u_2} → {m : Type u_3} → [Mul α] → [AddCommMonoid α] → Matrix m n α → [Fintype m] → Prop
-- Mathlib.Topology.Compactness.CompactSystem
IsCompactSystem.nonempty_iInter : ∀ {α : Type u_1} {S : Set (Set α)},
  IsCompactSystem S →
    ∀ {C : ℕ → Set α}, (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (Set.dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.neg_toLeftFun_add_mem : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : AddSubgroup.IsComplement S ↑H) (g : G),
  -↑(hS.toLeftFun g) + g ∈ H
-- Mathlib.Analysis.Complex.IntegerCompl
/-- The complement of the integers in `ℂ`  -/
Complex.integerComplement : Set ℂ
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_add : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) (x y : ↥s), ↑(x + y) = ↑x + ↑y
-- Mathlib.Order.Concept
/-- One half of the **fundamental theorem of concept lattices**: every concept lattice is a complete
lattice.

See `DedekindCut.principalIso` for the second half.  -/
Concept.instCompleteLattice : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → CompleteLattice (Concept α β r)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).hom.app T))
      (CategoryTheory.Limits.pullback.snd T.hom g) =
    CategoryTheory.ChosenPullbacksAlong.snd T.hom g
-- Init.Grind.Interactive
/-- Shows propositions known to be `False`.  -/
Lean.Parser.Tactic.Grind.showFalse : Lean.ParserDescr
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.center_im : ∀ (z : UpperHalfPlane) (r : ℝ), (z.center r).im = z.im * Real.cosh r
-- Init.Control.ExceptCps
ExceptCpsT.instMonadLiftOfMonad : {m : Type u_1 → Type u_2} → {σ : Type u_1} → [Monad m] → MonadLift m (ExceptCpsT σ m)
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.projectLeftAssign_property : ∀ {aig : Std.Sat.AIG ℕ} {assign : ℕ → Bool} {x : ℕ},
  Std.Sat.AIG.toCNF.projectLeftAssign✝ aig assign x = assign (x + aig.decls.size)
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- The localization of the fiber `p.Fiber S` is isomorphic to a quotient of a localization.  -/
Ideal.Fiber.algEquivAux₂ : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            [inst_3 : p.IsPrime] →
              (q : Ideal (p.Fiber S)) →
                [inst_4 : q.IsPrime] →
                  Localization.AtPrime q ≃ₐ[R]
                    Localization.AtPrime (Ideal.comap Algebra.TensorProduct.includeRight q) ⧸
                      Ideal.map (algebraMap S (Localization.AtPrime (Ideal.comap Algebra.TensorProduct.includeRight q)))
                        (Ideal.map (algebraMap R S) p)
-- Mathlib.Data.Set.Lattice
Set.biInter_singleton : ∀ {α : Type u_1} {β : Type u_2} (a : α) (s : α → Set β), ⋂ x ∈ {a}, s x = s a
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.hasPullbacks_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPushouts C],
  CategoryTheory.Limits.HasPullbacks Cᵒᵖ
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
/-- For any `Semiring A`, we collect the homogeneous submodule of `A`-modules into a type.  -/
HomogeneousSubmodule : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {σA : Type u_3} →
      {σM : Type u_4} →
        {A : Type u_5} →
          {M : Type u_6} →
            [inst : Semiring A] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module A M] →
                  (𝒜 : ιA → σA) →
                    (ℳ : ιM → σM) →
                      [inst_3 : DecidableEq ιA] →
                        [inst_4 : AddMonoid ιA] →
                          [inst_5 : SetLike σA A] →
                            [inst_6 : AddSubmonoidClass σA A] →
                              [GradedRing 𝒜] →
                                [inst_8 : DecidableEq ιM] →
                                  [inst_9 : SetLike σM M] →
                                    [inst_10 : AddSubmonoidClass σM M] →
                                      [DirectSum.Decomposition ℳ] →
                                        [inst_12 : VAdd ιA ιM] → [SetLike.GradedSMul 𝒜 ℳ] → Type u_6
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_eq_bot_iff : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G}, AddSubgroup.closure k = ⊥ ↔ k ⊆ {0}
-- Mathlib.RingTheory.Ideal.NatInt
Nat.coe_maximalIdeal : ↑(IsLocalRing.maximalIdeal ℕ) = {1}ᶜ
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.renameRule : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.bypass_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {u' v' : V} (p : G.Walk u v) (hu : u = u')
  (hv : v = v'), (p.copy hu hv).bypass = p.bypass.copy hu hv
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
ContinuousAlternatingMap.curryLeft_apply_apply : ∀ {𝕜 : 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] {n : ℕ}
  (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E) (v : Fin n → E), (f.curryLeft x) v = f (Matrix.vecCons x v)
-- Plausible.Gen
/-- Monad to generate random examples to test properties with.
It has a `Nat` parameter so that the caller can decide on the
size of the examples. It allows failure to generate via the `Except` monad  -/
Plausible.Gen : Type u → Type u
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.mk : Lean.Grind.CommRing.Poly → Lean.Meta.Grind.Arith.CommRing.EqCnstrProof → ℕ → ℕ → Lean.Meta.Grind.Arith.CommRing.EqCnstr
-- Mathlib.Order.Filter.CountableInter
CountableInterFilter.curry : ∀ {α : Type u_4} {β : Type u_5} {l : Filter α} {m : Filter β} [CountableInterFilter l] [CountableInterFilter m],
  CountableInterFilter (l.curry m)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Consumer.mk.inj : ∀ {α : Type} {promise : IO.Promise Bool} {waiter : Option (Std.Async.Waiter (Option α))} {promise_1 : IO.Promise Bool}
  {waiter_1 : Option (Std.Async.Waiter (Option α))},
  { promise := promise, waiter := waiter } = { promise := promise_1, waiter := waiter_1 } →
    promise = promise_1 ∧ waiter = waiter_1
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
LieGroup.of_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {m n : WithTop ℕ∞},
  m ≤ n → ∀ [h : LieGroup I n G], LieGroup I m G
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_one : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α], Matrix.cramer 1 = 1
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Sheaf.mono_of_isLocallyInjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {J : CategoryTheory.GrothendieckTopology C}
  {F₁ F₂ : CategoryTheory.Sheaf J D} (φ : F₁ ⟶ F₂) [J.HasSheafCompose (CategoryTheory.forget D)]
  [CategoryTheory.Sheaf.IsLocallyInjective φ], CategoryTheory.Mono φ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKey?.isSome = true
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree_mono : ∀ {σ : Type u_1} {R : Type u_5} [inst : AddCommMonoid R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R],
  Monotone ⇑Finsupp.degree
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.fun : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.FunDecl pu →
    autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.CodeDecl._auto_1 → Lean.Compiler.LCNF.CodeDecl pu
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_pow : ∀ {R : Type u} {σ : Type u_1} {a : R} {e : ℕ} {s : σ →₀ ℕ} [inst : CommSemiring R],
  (MvPolynomial.monomial s) a ^ e = (MvPolynomial.monomial (e • s)) (a ^ e)
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.domCongr_refl : ∀ (k : Type u_1) {G : Type u_2} (A : Type u_4) [inst : Monoid G] [inst_1 : Semiring A] [inst_2 : CommSemiring k]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G k A],
  SkewMonoidAlgebra.domCongrAlg k A ⋯ = AlgEquiv.refl
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instBoundedOrder : {α : Type u_1} → [inst : LE α] → [OrderTop α] → BoundedOrder (WithZero α)
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.disjoint_ker_iff_injOn : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M}, Disjoint p f.ker ↔ Set.InjOn ⇑f ↑p
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Given a function `f : M → N` between magmas, return the corresponding map `R[M] → R[N]` obtained
by summing the coefficients along each fiber of `f`.  -/
AddMonoidAlgebra.mapDomain : {R : Type u_3} →
  {M : Type u_6} → {N : Type u_7} → [inst : Semiring R] → (M → N) → AddMonoidAlgebra R M → AddMonoidAlgebra R N
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- Construct for morphisms from the tensor product of two objects in `SemimoduleCat`.  -/
SemimoduleCat.MonoidalCategory.tensorLift : {R : Type u} →
  [inst : CommSemiring R] →
    {M₁ M₂ M₃ : SemimoduleCat R} →
      (f : ↑M₁ → ↑M₂ → ↑M₃) →
        (∀ (m₁ m₂ : ↑M₁) (n : ↑M₂), f (m₁ + m₂) n = f m₁ n + f m₂ n) →
          (∀ (a : R) (m : ↑M₁) (n : ↑M₂), f (a • m) n = a • f m n) →
            (∀ (m : ↑M₁) (n₁ n₂ : ↑M₂), f m (n₁ + n₂) = f m n₁ + f m n₂) →
              (∀ (a : R) (m : ↑M₁) (n : ↑M₂), f m (a • n) = a • f m n) →
                (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₃)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_inv_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {X : Type u₇} {Y : Type u₈} [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (U : CategoryTheory.Functor X Y) (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x : X),
  ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).inv.app
            X_1).snd.app
      x =
    CategoryTheory.CategoryStruct.id (ψ.right.obj (X_1.snd.obj (U.obj x)))
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.le_iff_isLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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) (X : C) (n : ℤ), t.le n X ↔ t.IsLE X n
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Given an affine open U and some `f : U`,
this is the canonical map `Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(f))`
This is an isomorphism, as witnessed by an `IsIso` instance.  -/
AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine : {X : AlgebraicGeometry.Scheme} →
  {U : X.Opens} →
    AlgebraicGeometry.IsAffineOpen U →
      (f : ↑(X.presheaf.obj (Opposite.op U))) →
        X.presheaf.obj (Opposite.op (X.basicOpen f)) ⟶
          (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).presheaf.obj
            (Opposite.op (PrimeSpectrum.basicOpen f))
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- Given `NonUnitalSubring`s `s`, `t` of rings `R`, `S` respectively, `s.prod t` is `s ×ˢ t`
as a `NonUnitalSubring` of `R × S`.  -/
NonUnitalSubring.prod : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocRing R] →
      [inst_1 : NonUnitalNonAssocRing S] → NonUnitalSubring R → NonUnitalSubring S → NonUnitalSubring (R × S)
-- Lean.Server.Rpc.Basic
Lean.Lsp.instHashableRpcRef.hash : Lean.Lsp.RpcRef → UInt64
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableWithinAt.clm_precomp : ∀ {𝕜 : 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_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {f : M → F₁ →L[𝕜] F₂} {s : Set M}
  {x : M}, MDiffAt[s] f x → (MDiffAt[s] fun y => ContinuousLinearMap.precomp F₃ (f y)) x
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instAdd : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Add (AdicCompletion I M)
-- Mathlib.Order.Circular
/-- Open-open circular interval  -/
Set.cIoo : {α : Type u_1} → [CircularPreorder α] → α → α → Set α
-- Mathlib.Data.PNat.Interval
PNat.card_Icc : ∀ (a b : ℕ+), (Finset.Icc a b).card = ↑b + 1 - ↑a
-- Mathlib.Data.Fintype.Sets
Set.toFinset_symmDiff : ∀ {α : Type u_1} (s t : Set α) [inst : DecidableEq α] [inst_1 : Fintype ↑s] [inst_2 : Fintype ↑t]
  [inst_3 : Fintype ↑(symmDiff s t)], (symmDiff s t).toFinset = symmDiff s.toFinset t.toFinset
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyEq.eventuallyConst_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β},
  f =ᶠ[l] g → (Filter.EventuallyConst f l ↔ Filter.EventuallyConst g l)
-- Mathlib.Logic.IsEmpty.Defs
Function.Surjective.isEmpty : ∀ {α : Sort u} {β : Sort v} [IsEmpty α] {f : α → β}, Function.Surjective f → IsEmpty β
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DTreeMap.Const.ofList l cmp).getKey! k = default
-- Mathlib.Analysis.Convex.Caratheodory
/-- If `x` is in the convex hull of some finset `t` whose elements are not affine-independent,
then it is in the convex hull of a strict subset of `t`.  -/
Caratheodory.mem_convexHull_erase : ∀ {𝕜 : Type u_1} {E : Type u} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : DecidableEq E] {t : Finset E},
  ¬AffineIndependent 𝕜 Subtype.val → ∀ {x : E}, x ∈ (convexHull 𝕜) ↑t → ∃ y, x ∈ (convexHull 𝕜) ↑(t.erase ↑y)
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.instFullSheafTypeUliftYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical], (CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).Full
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLT_map_ofDual`. -/
List.SortedGT.of_map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, l.SortedGT → (List.map (⇑OrderDual.ofDual) l).SortedLT
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map.id : ∀ {α : Type u} (x : FreeGroup α), (FreeGroup.map id) x = x