mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- Given an open cover `{ Xᵢ }` of `X`, then `X ×[Z] Y` is covered by `Xᵢ ×[Z] Y`.  -/
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft : {X Y Z : AlgebraicGeometry.Scheme} →
  X.OpenCover → (f : X ⟶ Z) → (g : Y ⟶ Z) → (CategoryTheory.Limits.pullback f g).OpenCover
-- Mathlib.RingTheory.WittVector.InitTail
/-- `WittVector.init n x` is the Witt vector of which the first `n` coefficients are those from `x`
and all other coefficients are `0`.
See `WittVector.tail` for the complementary part.
 -/
WittVector.init : {p : ℕ} → {R : Type u_1} → [CommRing R] → ℕ → WittVector p R → WittVector p R
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_of_not_aestronglyMeasurable : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E}, ¬MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.lpNorm f p μ = 0
-- Mathlib.Order.Circular
Set.right_mem_cIcc : ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), b ∈ Set.cIcc a b
-- Init.Data.UInt.Bitwise
UInt64.toUInt32_shiftLeft_mod : ∀ (a b : UInt64), (a <<< (b % 32)).toUInt32 = a.toUInt32 <<< b.toUInt32
-- Mathlib.Order.LatticeIntervals
Set.Iic.orderTop : {α : Type u_1} → {a : α} → [inst : Preorder α] → OrderTop ↑(Set.Iic a)
-- Mathlib.Order.CompleteLattice.Chain
ChainClosure.union : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set (Set α)}, (∀ a ∈ s, ChainClosure r a) → ChainClosure r (⋃₀ s)
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.Weight.coe_toLinear_ne_zero_iff : ∀ {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] [inst_8 : LieModule.LinearWeights R L M] {χ : LieModule.Weight R L M},
  LieModule.Weight.toLinear R L M χ ≠ 0 ↔ χ.IsNonZero
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.TensorBimod.X.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T),
  Bimod.TensorBimod.X P Q =
    CategoryTheory.Limits.coequalizer (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft))
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTι_naturality : ∀ {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) (i : EInt) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj i).map f) ((t.eTruncLTι i).app Y) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app X) f
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Relation.mk'_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {fst snd : S.Arrow} (r : fst.Relation snd),
  (CategoryTheory.GrothendieckTopology.Cover.Relation.mk' r).snd = snd
-- Mathlib.CategoryTheory.Subterminal
/-- If the unique morphism from `A` to a terminal object is a monomorphism, `A` is subterminal.
The converse of `IsSubterminal.mono_isTerminal_from`.
 -/
CategoryTheory.isSubterminal_of_mono_isTerminal_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  [CategoryTheory.Mono (hT.from A)], CategoryTheory.IsSubterminal A
-- Mathlib.Data.FP.Basic
FP.Float.zero : [C : FP.FloatCfg] → Bool → FP.Float
-- Batteries.Tactic.SeqFocus
/-- Assuming there are `n` goals, `map_tacs [t1; t2; ...; tn]` applies each `ti` to the respective
goal and leaves the resulting subgoals. It raises an error if the number of subgoals does not match.
 -/
Batteries.Tactic.«tacticMap_tacs[_;]» : Lean.ParserDescr
-- Lean.Meta.Sym.Eta
_private.Lean.Meta.Sym.Eta.0.Lean.Meta.Sym.etaReduceWithCache.visit : Lean.Expr → StateRefT' IO.RealWorld (Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr) Lean.CoreM Lean.Expr
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.le_valuation_add : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℚ_[p]}, x + y ≠ 0 → min x.valuation y.valuation ≤ (x + y).valuation
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkChainResult.go.match_1.splitter : (motive : Option Lean.SyntaxNodeKind → Sort u_1) →
  (kind? : Option Lean.SyntaxNodeKind) →
    ((kind : Lean.SyntaxNodeKind) → motive (some kind)) →
      ((x : Option Lean.SyntaxNodeKind) → (∀ (kind : Lean.SyntaxNodeKind), x = some kind → False) → motive x) →
        motive kind?
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, (∀ y ∈ s, g y = f y) → g x = f x → (ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x)
-- Init.Core
DoResultSBC.continue.sizeOf_spec : ∀ {α σ : Type u} [inst : SizeOf α] [inst_1 : SizeOf σ] (a : σ), sizeOf (DoResultSBC.continue a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.multicospanIndex_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.Functor Cᵒᵖ A) (j : E.multicospanShape.R),
  (E.multicospanIndex F).right j = F.obj (Opposite.op (E.Y j.snd))
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor_hom_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor α).hom.τl = (CategoryTheory.Bicategory.leftUnitor α.l).hom
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_eq_extract_append_extract : ∀ {a : ByteArray} {i k : ℕ} (j : ℕ), i ≤ j → j ≤ k → a.extract i k = a.extract i j ++ a.extract j k
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.module : Lean.Lsp.CompletionItemKind
-- Batteries.Classes.Order
Std.instOrientedCmpCompareOnOfOrientedOrd_batteries : ∀ {β : Type u_1} {α : Type u_2} [inst : Ord β] [Std.OrientedOrd β] (f : α → β), Std.OrientedCmp (compareOn f)
-- Init.Data.List.Attach
List.flatMap_wfParam : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β},
  List.flatMap f (wfParam xs) = List.flatMap f xs.attach.unattach
-- Mathlib.RingTheory.Radical.NatInt
Int.one_lt_radical_iff : ∀ {z : ℤ}, 1 < UniqueFactorizationMonoid.radical z ↔ 1 < z.natAbs
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.nat.injEq : ∀ (val val_1 : ℕ), (Lean.Compiler.LCNF.LitValue.nat val = Lean.Compiler.LCNF.LitValue.nat val_1) = (val = val_1)
-- Lean.Attributes
Lean.getAttributeImpl : Lean.Environment → Lean.Name → Except String Lean.AttributeImpl
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMapZero.elemental_eq_top : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] (s : Set 𝕜) [inst_1 : Fact (0 ∈ s)] [inst_2 : CompactSpace ↑s],
  NonUnitalStarAlgebra.elemental 𝕜 (ContinuousMapZero.id s) = ⊤
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.isoClosure_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C) [Q.RespectsIso],
  P.isoClosure ≤ Q ↔ P ≤ Q
-- Std.Net.Addr
Std.Net.SocketAddressV4.mk.injEq : ∀ (addr : Std.Net.IPv4Addr) (port : UInt16) (addr_1 : Std.Net.IPv4Addr) (port_1 : UInt16),
  ({ addr := addr, port := port } = { addr := addr_1, port := port_1 }) = (addr = addr_1 ∧ port = port_1)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.embedding : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G'), G'.IsAcyclic → G.IsAcyclic
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.associator_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable]
  (x x_1 x_2 : CategoryTheory.WideSubcategory P),
  CategoryTheory.MonoidalCategoryStruct.associator x x_1 x_2 =
    CategoryTheory.WideSubcategory.isoMk (CategoryTheory.MonoidalCategoryStruct.associator x.obj x_1.obj x_2.obj) ⋯ ⋯
-- Init.Data.List.MapIdx
List.getElem_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β} {i : ℕ} {h : i < (List.mapIdx f l).length},
  (List.mapIdx f l)[i] = f i l[i]
-- Mathlib.Tactic.NormNum.Result
/-- The result is `proof : ¬x`, where `x` is a (false) proposition.  -/
Mathlib.Meta.NormNum.Result.isFalse : {x : Q(Prop)} → Q(¬«$x») → Mathlib.Meta.NormNum.Result q(«$x»)
-- Mathlib.Analysis.Calculus.Deriv.Inverse
HasDerivAt.eventually_ne : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {c : F},
  HasDerivAt f f' x → f' ≠ 0 → ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z ≠ c
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.eventually : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → n ≠ ↑⊤ → ∀ᶠ (y : E) in nhdsWithin x (insert x s), ContDiffWithinAt 𝕜 n f s y
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.finite : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f), Module.Finite R S
-- Lean.Elab.DocString
/-- Adds a builtin documentation directive.

Should be run during initialization.
 -/
Lean.Doc.addBuiltinDocDirective : Lean.Name → Lean.Name → Lean.Doc.DocDirectiveExpander → IO Unit
-- Lean.Parser.Term
Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean : Coe (Lean.TSyntax `Lean.Parser.Term.matchAltExpr) (Lean.TSyntax `Lean.Parser.Term.matchAlt)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α},
  k ∈ m.keys ↔ k ∈ m
-- Mathlib.Order.DirSupClosed
IsUpperSet.dirSupClosed : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], IsUpperSet s → DirSupClosed s
-- Mathlib.Combinatorics.Graph.Delete
Graph.induce_le : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α}, X ⊆ G.vertexSet → G.induce X ≤ G
-- Mathlib.GroupTheory.DivisibleHull
/-- The Archimedean classes of `DivisibleHull M` are the same as those of `M`.  -/
DivisibleHull.archimedeanClassOrderIso : (M : Type u_2) →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] → ArchimedeanClass M ≃o ArchimedeanClass (DivisibleHull M)
-- Init.Data.Iterators.Consumers.Loop
Std.instForMTotalOfMonadOfIteratorLoopOfFiniteId : {m : Type x → Type x'} →
  {α β : Type w} →
    [Monad m] →
      [inst : Std.Iterator α Id β] →
        [Std.IteratorLoop α Id m] → [Std.Iterators.Finite α Id] → ForM m (Std.Iter.Total β) β
-- Std.Time.Date.Unit.Year
Std.Time.Year.instTransOrdOffset : Std.TransOrd Std.Time.Year.Offset
-- Mathlib.Algebra.Algebra.Operations
Submodule.pow_toAddSubmonoid : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A) {n : ℕ}, n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
-- Mathlib.Order.Filter.AtTopBot.Finset
Filter.tendsto_finset_Iic_atTop_atTop : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α],
  Filter.Tendsto Finset.Iic Filter.atTop Filter.atTop
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.IsPrimitive.dvd_of_fraction_map_dvd_fraction_map : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsDomain R] [IsGCDMonoid R] {p q : Polynomial R},
  p.IsPrimitive → Polynomial.map (algebraMap R K) p ∣ Polynomial.map (algebraMap R K) q → p ∣ q
-- Lean.Data.Lsp.Basic
Lean.Lsp.StaticRegistrationOptions.mk.inj : ∀ {id? id?_1 : Option String}, { id? := id? } = { id? := id?_1 } → id? = id?_1
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.count_span_normalizedFactors_eq`.

---

The bijection between the set of prime factors of the ideal `⟨r⟩` and the set of prime factors
of `r` preserves `count` of the corresponding multisets. See
`multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity` for the version
stated in terms of multiplicity.  -/
count_span_normalizedFactors_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] [inst_4 : DecidableEq R] {r X : R},
  r ≠ 0 →
    Prime X →
      Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) =
        Multiset.count (normalize X) (UniqueFactorizationMonoid.normalizedFactors r)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
DifferentiableWithinAt.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x → DifferentiableWithinAt ℝ (fun x => Real.exp (f x)) s x
-- Mathlib.CategoryTheory.Equivalence
/-- A quasi-inverse `D ⥤ C` to a functor that `F : C ⥤ D` that is an equivalence,
i.e. faithful, full, and essentially surjective.  -/
CategoryTheory.Functor.inv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → [F.IsEquivalence] → CategoryTheory.Functor D C
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Entry.mk.sizeOf_spec : ∀ (declName optionName : Lean.Name),
  sizeOf { declName := declName, optionName := optionName } = 1 + sizeOf declName + sizeOf optionName
-- Lean.Meta.Instances
Lean.Meta.InstanceEntry.priority : Lean.Meta.InstanceEntry → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.cons_tail_eq : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : ¬p.Nil), SimpleGraph.Walk.cons ⋯ p.tail = p
-- Init.PropLemmas
exists_congr : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∃ a, p a) ↔ ∃ a, q a)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.id_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] (M : CategoryTheory.AddMod D A),
  (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.mul_right : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r b c → RingQuot.Rel r (a * b) (a * c)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.isUniformEmbedding_toContinuousMap : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : Zero R]
  [inst_3 : UniformSpace R], IsUniformEmbedding toContinuousMap
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.ofSimplex_le_skeleton : ∀ (X : SSet) {i : ℕ} (x : X.obj (Opposite.op { len := i })) {n : ℕ}, i < n → SSet.Subcomplex.ofSimplex x ≤ X.skeleton n
-- Mathlib.Computability.DFA
DFA.mk.inj : ∀ {α : Type u} {σ : Type v} {step : σ → α → σ} {start : σ} {accept : Set σ} {step_1 : σ → α → σ} {start_1 : σ}
  {accept_1 : Set σ},
  { step := step, start := start, accept := accept } = { step := step_1, start := start_1, accept := accept_1 } →
    step = step_1 ∧ start = start_1 ∧ accept = accept_1
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F] [T2Space F],
  HasFDerivWithinAt f f' s x → UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 f s x = f'
-- Mathlib.Algebra.DirectSum.LinearMap
/-- The trace of an endomorphism of a direct sum is the sum of the traces on each component.

See also `LinearMap.trace_restrict_eq_sum_trace_restrict`.  -/
LinearMap.trace_eq_sum_trace_restrict : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : ι → Submodule R M} [inst_3 : DecidableEq ι] [∀ (i : ι), Module.Finite R ↥(N i)]
  [∀ (i : ι), Module.Free R ↥(N i)],
  DirectSum.IsInternal N →
    ∀ [inst_6 : Fintype ι] {f : M →ₗ[R] M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)),
      (LinearMap.trace R M) f = ∑ i, (LinearMap.trace R ↥(N i)) (f.restrict ⋯)
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_def_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (xPoly p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_def_cert x xPoly p = p.beq' (Int.Internal.Linear.Poly.add (-1) x xPoly)
-- Mathlib.Computability.RecursiveIn
/-- A binary partial function is recursive in `O` if the curried form is.  -/
RecursiveIn₂ : {α : Type u_5} →
  {β : Type u_6} →
    {σ : Type u_7} → [Primcodable α] → [Primcodable β] → [Primcodable σ] → Set (ℕ →. ℕ) → (α → β →. σ) → Prop
-- Mathlib.Algebra.Group.Indicator
Set.indicator_union_of_disjoint : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] {s t : Set α},
  Disjoint s t → ∀ (f : α → M), (s ∪ t).indicator f = fun a => s.indicator f a + t.indicator f a
-- Mathlib.Data.List.TakeWhile
List.length_dropWhile_le : ∀ {α : Type u_1} (p : α → Bool) (l : List α), (List.dropWhile p l).length ≤ l.length
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insert.match_3.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Mathlib.Tactic.Widget.CommDiag
/-- Given composed homs `g ≫ h`, return `(g, h)`. Otherwise `none`.  -/
Mathlib.Tactic.Widget.homComp? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)}
  {hc : k' ∈ Std.DTreeMap.Internal.Impl.alter! k f t},
  (Std.DTreeMap.Internal.Impl.alter! k f t).get k' hc =
    if heq : compare k k' = Ordering.eq then cast ⋯ ((f (t.get? k)).get ⋯) else t.get k' ⋯
-- Mathlib.Topology.NhdsKer
nhdsKer_iUnion : ∀ {ι : Sort u_1} {X : Type u_2} [inst : TopologicalSpace X] (s : ι → Set X), nhdsKer (⋃ i, s i) = ⋃ i, nhdsKer (s i)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.Rel.add : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  {a b : M},
  DividedPowerAlgebra.Rel R M (MvPolynomial.X (n, a + b))
    (∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, MvPolynomial.X (k.1, a) * MvPolynomial.X (k.2, b))
-- Lean.PrettyPrinter.Delaborator.FieldNotation
/-- If this constant is a structure projection that could delaborate using dot notation, returns
- the field name,
- the number of parameters before the structure argument,
- whether this is a "true" projection (or else a non-subobject parent projection),
- whether this is a parent projection, and
- whether this is a class projection.
Otherwise it returns `none`.
 -/
_private.Lean.PrettyPrinter.Delaborator.FieldNotation.0.Lean.PrettyPrinter.Delaborator.projInfo : Lean.Name → Lean.MetaM (Option (Lean.Name × ℕ × Bool × Bool × Bool))
-- Lean.Compiler.LCNF.Basic
/-- Return `some i` if `decl` is of the form
```
def f (a_0 ... a_i ...) :=
  ...
  cases a_i
  | ...
  | ...
```
That is, `f` is a sequence of declarations followed by a `cases` on the parameter `i`.
We use this function to decide whether we should inline a declaration tagged with
`[inline_if_reduce]` or not.
 -/
Lean.Compiler.LCNF.Decl.isCasesOnParam? : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Option ℕ
-- Mathlib.GroupTheory.Congruence.Defs
/-- The infimum of a set of additive congruence relations is the same as the infimum
of the set's image under the map to the underlying equivalence relation.  -/
AddCon.sInf_toSetoid : ∀ {M : Type u_1} [inst : Add M] (S : Set (AddCon M)), (sInf S).toSetoid = sInf (AddCon.toSetoid '' S)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Pull back a symmetric braiding along a fully faithful monoidal functor.  -/
CategoryTheory.SymmetricCategory.ofFullyFaithful : {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.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [F.Monoidal] →
                [F.Full] → [F.Faithful] → [CategoryTheory.SymmetricCategory D] → CategoryTheory.SymmetricCategory C
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHomClass.toNonUnitalRingHom.congr_simp : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : FunLike F α β] [inst_3 : NonUnitalRingHomClass F α β] (f f_1 : F),
  f = f_1 → ↑f = ↑f_1
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
LocallyConstant.piecewise'.congr_simp : ∀ {X : Type u_1} {Z : Type u_3} [inst : TopologicalSpace X] {C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁)
  (h₂ : IsClosed C₂) (f₁ f₁_1 : LocallyConstant (↑C₁) Z) (e_f₁ : f₁ = f₁_1) (f₂ f₂_1 : LocallyConstant (↑C₂) Z)
  (e_f₂ : f₂ = f₂_1) {inst_1 : DecidablePred fun x => x ∈ C₁} [inst_2 : DecidablePred fun x => x ∈ C₁]
  (hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩),
  LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf = LocallyConstant.piecewise' h₀ h₁ h₂ f₁_1 f₂_1 ⋯
-- Mathlib.Algebra.Regular.Basic
/-- An additive unit in an additive monoid is add-regular.  -/
IsAddUnit.isAddRegular : ∀ {R : Type u_1} [inst : AddMonoid R] {a : R}, IsAddUnit a → IsAddRegular a
-- Mathlib.Analysis.Calculus.FDeriv.Defs
hasFDerivAtFilter_iff_isLittleOTVS : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E → F) (f' : E →L[𝕜] F) (L : Filter (E × E)),
  HasFDerivAtFilter f f' L ↔ (fun p => f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝕜; L] fun p => p.1 - p.2
-- Mathlib.Topology.LocallyFinsupp
/-- Simplifier lemma: `single x y` takes the value `y` at `x` and is zero otherwise.
 -/
Function.locallyFinsuppWithin.single_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : DecidableEq X] [inst_2 : Zero Y] {x₁ x₂ : X}
  {y : Y}, (Function.locallyFinsuppWithin.single x₁ y) x₂ = if x₂ = x₁ then y else 0