mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_coe : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (k : K),
  Valued.v { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm k) } =
    (IsDedekindDomain.HeightOneSpectrum.valuation K v) k
-- Mathlib.Algebra.Module.ZMod
/-- In an elementary abelian `p`-group, every finite subgroup `H` contains a further subgroup of
cardinality between `k` and `p * k`, if `k ≤ |H|`.  -/
ZModModule.exists_submodule_subset_card_le : ∀ {p : ℕ} {G : Type u_5} [inst : AddCommGroup G],
  Nat.Prime p →
    ∀ [inst_1 : Module (ZMod p) G] (H : Submodule (ZMod p) G) {k : ℕ},
      k ≤ Nat.card ↥H → k ≠ 0 → ∃ H', Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.hp₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  (self : CategoryTheory.Limits.ChosenPullback f₁ f₂), CategoryTheory.CategoryStruct.comp self.p₁ f₁ = self.p
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K)
  (w : NumberField.InfinitePlace K), 0 < ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x w
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_eq_false : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr),
  (lhs.sub rhs).norm.isUnsatEq_k = true →
    (Int.Internal.Linear.Expr.denote ctx lhs = Int.Internal.Linear.Expr.denote ctx rhs) = False
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instIsConcreteLEFinset : ∀ (ι : Type u_1), IsConcreteLE (PreAbstractSimplicialComplex ι) (Finset ι)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.tensorBimod_actRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z),
  (M.tensorBimod N).actRight = Bimod.TensorBimod.actRight M N
-- Mathlib.Order.Directed
isBot_iff_isMin : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [IsCodirectedOrder α], IsBot a ↔ IsMin a
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_epi₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₂ = 0 ↔ CategoryTheory.Epi T.mor₁
-- Mathlib.Data.Option.Basic
Option.map_coe' : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : α → β}, Option.map f (some a) = some (f a)
-- Mathlib.Algebra.Ring.GeomSum
zero_geom_sum : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ}, ∑ i ∈ Finset.range n, 0 ^ i = if n = 0 then 0 else 1
-- Mathlib.Logic.Equiv.Multiset
_private.Mathlib.Logic.Equiv.Multiset.0.enle : {α : Type u_1} → [Encodable α] → α → α → Prop
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleSets.mk.sizeOf_spec : ∀ (ruleSets : Array Aesop.RuleSetName), sizeOf { ruleSets := ruleSets } = 1 + sizeOf ruleSets
-- Mathlib.Data.Rel
SetRel.isTrans_id : ∀ {α : Type u_1}, SetRel.id.IsTrans
-- Mathlib.NumberTheory.Multiplicity
Int.two_pow_two_pow_sub_pow_two_pow : ∀ {x y : ℤ} (n : ℕ), 4 ∣ x - y → ¬2 ∣ x → emultiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = emultiplicity 2 (x - y) + ↑n
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.toENat_cRank_eq : ∀ {α : Type u} (M : Matroid α), Cardinal.toENat M.cRank = M.eRank
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.ball x ε ↔ dist y x < ε
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.iIndepFun.mgf_sum₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : ι → Ω → ℝ},
  ProbabilityTheory.iIndepFun X μ →
    (∀ (i : ι), AEMeasurable (X i) μ) →
      ∀ (s : Finset ι), ProbabilityTheory.mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, ProbabilityTheory.mgf (X i) μ t
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- A morphism in `D` is a morphism of `A`-additive module objects if it commutes with
the action maps  -/
CategoryTheory.IsAddModHom : {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] →
            {M' N' : D} →
              (A : C) →
                [inst_4 : CategoryTheory.AddMonObj A] →
                  [CategoryTheory.AddModObj A M'] → [CategoryTheory.AddModObj A N'] → (M' ⟶ N') → Prop
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.strAux.parse : String → String → String.Pos.Raw → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.isOpen_iff : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (U : Set ↥D.glued), IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(D.ι i) ⁻¹' U)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.save : Lean.Syntax → Lean.Meta.Grind.EMatchTheorem → Bool → Bool → Lean.Meta.Grind.SelectM✝ Unit
-- Mathlib.Data.List.Forall2
List.Forall₂.imp : ∀ {α : Type u_1} {β : Type u_2} {R S : α → β → Prop},
  (∀ (a : α) (b : β), R a b → S a b) → ∀ {l₁ : List α} {l₂ : List β}, List.Forall₂ R l₁ l₂ → List.Forall₂ S l₁ l₂
-- Mathlib.Data.Num.Bitwise
NzsNum.msb.injEq : ∀ (a a_1 : Bool), (NzsNum.msb a = NzsNum.msb a_1) = (a = a_1)
-- Mathlib.Data.Num.Bitwise
Num.shiftl_eq_shiftLeft : ∀ (p : Num) (n : ℕ), p.shiftl n = p <<< n
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- Comultiplication as a bialgebra hom.  -/
Bialgebra.comulBialgHom : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → [Coalgebra.IsCocomm R A] → A →ₐc[R] TensorProduct R A A
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Given a multilinear map `f` on `(i : ι) → M i`, a (decidable) predicate `P` on `ι` and
an element `z` of `(i : {a // ¬ P a}) → M₁ i`, construct a multilinear map on
`(i : {a // P a}) → M₁ i)` whose value at `x` is `f` evaluated at the vector with `i`th coordinate
`x i` if `P i` and `z i` otherwise.

The naming is similar to `MultilinearMap.domDomCongr`: here we are applying the restriction to the
domain of the domain.

For a linear map version, see `MultilinearMap.domDomRestrictₗ`.
 -/
MultilinearMap.domDomRestrict : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  MultilinearMap R M₁ M₂ →
                    (P : ι → Prop) →
                      [DecidablePred P] → ((i : { a // ¬P a }) → M₁ ↑i) → MultilinearMap R (fun i => M₁ ↑i) M₂
-- Mathlib.Topology.UniformSpace.Uniformizable
CompletelyRegularSpace.exists_uniformSpace : ∀ {X : Type u_1} [t : TopologicalSpace X] [CompletelyRegularSpace X], ∃ u, u.toTopologicalSpace = t
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
UniformContinuous.comp_tendstoLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [inst_2 : UniformSpace γ] {g : β → γ},
  UniformContinuous g → TendstoLocallyUniformlyOn F f p s → TendstoLocallyUniformlyOn (fun x => g ∘ F x) (g ∘ f) p s
-- Mathlib.Analysis.Analytic.Constructions
/-- Scalar multiplication of one analytic function by another.  -/
AnalyticWithinAt.smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {A : Type u_7}
  [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F] [IsBoundedSMul A F] [IsScalarTower 𝕜 A F]
  {f : E → A} {g : E → F} {s : Set E} {z : E},
  AnalyticWithinAt 𝕜 f s z → AnalyticWithinAt 𝕜 g s z → AnalyticWithinAt 𝕜 (fun x => f x • g x) s z
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.isAddUnit : ∀ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M), IsAddUnit ↑u
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcConnected : Lean.ToJson Lean.Lsp.RpcConnected
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A convenience variant of `LinearMap.BilinForm.nondegenerate_iff` characterising nondegeneracy as
positive definiteness.  -/
LinearMap.BilinForm.nondegenerate_iff' : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M),
  (∀ (x : M), 0 ≤ (B x) x) → LinearMap.IsSymm B → (LinearMap.Nondegenerate B ↔ ∀ (x : M), x ≠ 0 → 0 < (B x) x)
-- Mathlib.Order.Iterate
/-- If `f ≤ g` and `g` is monotone, then `f^[n] ≤ g^[n]`.  -/
Monotone.le_iterate_of_le : ∀ {α : Type u_1} [inst : Preorder α] {f g : α → α}, Monotone f → g ≤ f → ∀ (n : ℕ), g^[n] ≤ f^[n]
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multispanMapIso_inv_app : ∀ {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] {J : CategoryTheory.Limits.MultispanShape}
  (d : CategoryTheory.Limits.MultispanIndex J C) (F : CategoryTheory.Functor C D)
  (X : CategoryTheory.Limits.WalkingMultispan J),
  (d.multispanMapIso F).inv.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.Iso.refl (F.obj (d.left a))
      | CategoryTheory.Limits.WalkingMultispan.right a => CategoryTheory.Iso.refl (F.obj (d.right a))).inv
-- Init.Core
/-- Substitution with heterogeneous equality.  -/
HEq.subst : ∀ {α β : Sort u} {a : α} {b : β} {p : (T : Sort u) → T → Prop}, a ≍ b → p α a → p β b
-- Mathlib.Algebra.Order.Star.Basic
IsSelfAdjoint.of_ge : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x y : R}, x ≤ y → IsSelfAdjoint x → IsSelfAdjoint y
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.coeff_rename_ne_zero : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ),
  MvPolynomial.coeff d ((MvPolynomial.rename f) φ) ≠ 0 → ∃ u, Finsupp.mapDomain f u = d ∧ MvPolynomial.coeff u φ ≠ 0
-- Lean.Server.References
/-- Location and parent declaration of a reference.  -/
Lean.Server.References.DocumentRefInfo : Type
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.continuous_toContinuousMultilinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F],
  Continuous ContinuousAlternatingMap.toContinuousMultilinearMap
-- Lean.Data.FuzzyMatching
/-- Match the given pattern with the given word. The algorithm uses dynamic
programming to find the best scores.

In addition to the current characters in the pattern and the word, the
algorithm uses different scores for the last operation (miss/match). This is
necessary to give consecutive character matches a bonus.  -/
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.fuzzyMatchCore : String → String → Array Lean.FuzzyMatching.CharRole → Array Lean.FuzzyMatching.CharRole → Option ℤ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.dropPrefix?_slice_of_isEmpty : ∀ {pat s : String.Slice}, pat.isEmpty = true → s.dropPrefix? pat = some s
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.adjoin_ext : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {s : Set A} ⦃φ₁ φ₂ : ↥(Algebra.adjoin R s) →ₐ[R] B⦄,
  (∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩) → φ₁ = φ₂
-- Mathlib.Order.Max
/-- `a` is a minimal element of `α` if no element is strictly less than it. We spell it without `<`
to avoid having to convert between `≤` and `<`. Instead, `isMin_iff_forall_not_lt` does the
conversion.  -/
IsMin : {α : Type u_1} → [LE α] → α → Prop
-- Mathlib.Topology.Algebra.Group.Basic
/-- A version of `Pi.continuousInv` for non-dependent functions. It is needed because sometimes
Lean fails to use `Pi.continuousInv` for non-dependent functions.  -/
Pi.has_continuous_inv' : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G] {ι : Type u_1}, ContinuousInv (ι → G)
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- Smooth of relative dimension `n` is stable under base change.  -/
AlgebraicGeometry.smoothOfRelativeDimension_isStableUnderBaseChange : ∀ (n : ℕ), CategoryTheory.MorphismProperty.IsStableUnderBaseChange (@AlgebraicGeometry.SmoothOfRelativeDimension n)
-- Mathlib.Topology.Algebra.Ring.Basic
/-- Given `f : R → S` and a topology on `R`, the coinduced ring topology on `S` is the finest
topology such that `f` is continuous and `S` is a topological ring.  -/
RingTopology.coinduced : {R : Type u_2} → {S : Type u_3} → [t : TopologicalSpace R] → [inst : Ring S] → (R → S) → RingTopology S
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.support_eq_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.support = u :: p.support.tail
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddZeroClassOfAddMonoidHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddZeroClass (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)],
  DirectLimit.instAddZeroClassOfAddMonoidHomClass =
    { toZero := DirectLimit.instZero, toAdd := DirectLimit.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.supDegree_eq_natDegree : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Construct a coframe instance using the minimal amount of work needed.

This sets `a \ b := sInf {c | a ≤ b ⊔ c}` and `￢a := ⊤ \ a`.  -/
Order.Coframe.ofMinimalAxioms : {α : Type u} → [inst : CompleteLattice α] → Order.Coframe.MinimalAxioms α → Order.Coframe α
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_dirac' : ∀ {α : Type u_1} [inst : MeasurableSpace α] (a : α) {f : α → ENNReal},
  Measurable f → ∫⁻ (a : α), f a ∂MeasureTheory.Measure.dirac a = f a
-- Init.Data.Ord.Vector
Vector.instOrientedOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.OrientedOrd α] {n : ℕ}, Std.OrientedOrd (Vector α n)
-- Mathlib.Data.Multiset.Powerset
Multiset.mem_powersetCard : ∀ {α : Type u_1} {n : ℕ} {s t : Multiset α}, s ∈ Multiset.powersetCard n t ↔ s ≤ t ∧ s.card = n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_eq_get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {a : α}
  {h' : a ∈ t}, t.get a h' = (t.get? a).get ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.Smooth f],
  AlgebraicGeometry.Scheme.Hom.smoothLocus f = ⊤
-- Mathlib.Data.Finset.Sups
/-- **Alias** of `Finset.empty_sdiffs`. -/
Finset.empty_diffs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {t : Finset α}, ∅.diffs t = ∅
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.oneLE.hasMemOrInvMem : ∀ {H : Type u_2} [inst : CommGroup H] [inst_1 : LinearOrder H] [inst_2 : IsOrderedMonoid H],
  HasMemOrInvMem (GroupCone.oneLE H)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.mk_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (x y : CochainComplex.HomComplex.Cocycle K L n),
  CochainComplex.HomComplex.CohomologyClass.mk (x - y) =
    CochainComplex.HomComplex.CohomologyClass.mk x - CochainComplex.HomComplex.CohomologyClass.mk y
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Build an isomorphism in the category `AddMagmaCat` from an `AddEquiv` between `Add`s.  -/
AddEquiv.toAddMagmaCatIso : {X Y : Type u} → [inst : Add X] → [inst_1 : Add Y] → X ≃+ Y → (AddMagmaCat.of X ≅ AddMagmaCat.of Y)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.ordered_modify : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {a : α}
  {f : β → β}, t.Balanced → t.Ordered → (Std.DTreeMap.Internal.Impl.Const.modify a f t).Ordered
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion.torsion_eq_top`.

---

The torsion submonoid of a torsion monoid is `⊤`.  -/
Monoid.IsTorsion.torsion_eq_top : ∀ {G : Type u_1} [inst : CommMonoid G], IsMulTorsion G → CommMonoid.torsion G = ⊤
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonSnippetString.toJson : Lean.Lsp.SnippetString → Lean.Json
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.mem_incidenceFinset : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] [inst_1 : DecidableEq V] (e : Sym2 V),
  e ∈ G.incidenceFinset v ↔ e ∈ G.incidenceSet v
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (D : F.DescentData' sq sq₃) (i₁ i₂ : ι), CategoryTheory.IsIso (D.hom i₁ i₂)
-- Mathlib.Tactic.CategoryTheory.Reassoc
/-- Reassociates the morphisms in the type of `pf` using the registered handlers,
using `reassocExprHom` as the default.

Returns the proof of the lemma along with instance metavariables that need synthesis.
 -/
Mathlib.Tactic.Reassoc.reassocExpr : Lean.Expr → Lean.MetaM (Lean.Expr × Array Lean.MVarId)
-- Mathlib.Topology.Algebra.UniformConvergence
instCommMonoidUniformFun : {α : Type u_1} → {β : Type u_2} → [CommMonoid β] → CommMonoid (UniformFun α β)
-- Mathlib.Analysis.Calculus.Deriv.Star
/-- If `f` is differentiable at `conj z`, then `star ∘ f ∘ conj` is differentiable at `z`.  -/
DifferentiableAt.star_conj : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {x : 𝕜} [NormedStarGroup 𝕜]
  {f : 𝕜 → F}, DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (star ∘ f ∘ ⇑(starRingEnd 𝕜)) ((starRingEnd 𝕜) x)
-- Mathlib.Analysis.Normed.Operator.CompleteCodomain
SeparatingDual.completeSpace_continuousMultilinearMap_iff : ∀ (𝕜 : Type u_1) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_4} [Finite ι] {M : ι → Type u_5} [inst_4 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_5 : (i : ι) → NormedSpace 𝕜 (M i)] [∀ (i : ι), SeparatingDual 𝕜 (M i)] {m : (i : ι) → M i},
  (∀ (i : ι), m i ≠ 0) → (CompleteSpace (ContinuousMultilinearMap 𝕜 M F) ↔ CompleteSpace F)
-- Mathlib.Logic.Function.Basic
Function.const_injective : ∀ {α : Sort u_1} {β : Sort u_2} [Nonempty α], Function.Injective (Function.const α)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.SizedBalancedTree.mk.injEq : ∀ {α : Type u} {β : α → Type v} {lb ub : ℕ} (impl : Std.DTreeMap.Internal.Impl α β) (balanced_impl : impl.Balanced)
  (lb_le_size_impl : lb ≤ impl.size) (size_impl_le_ub : impl.size ≤ ub) (impl_1 : Std.DTreeMap.Internal.Impl α β)
  (balanced_impl_1 : impl_1.Balanced) (lb_le_size_impl_1 : lb ≤ impl_1.size) (size_impl_le_ub_1 : impl_1.size ≤ ub),
  ({ impl := impl, balanced_impl := balanced_impl, lb_le_size_impl := lb_le_size_impl,
        size_impl_le_ub := size_impl_le_ub } =
      { impl := impl_1, balanced_impl := balanced_impl_1, lb_le_size_impl := lb_le_size_impl_1,
        size_impl_le_ub := size_impl_le_ub_1 }) =
    (impl = impl_1)
-- Std.Data.TreeMap.Basic
Std.TreeMap.instDecidableMem : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → {m : Std.TreeMap α β cmp} → {a : α} → Decidable (a ∈ m)
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.topologically.eq_1 : ∀ (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop) (x x_1 : AlgebraicGeometry.Scheme)
  (f : x ⟶ x_1), AlgebraicGeometry.topologically P f = P ⇑f
-- Init.Control.Lawful.Instances
ExceptT.seq_eq : ∀ {m : Type u → Type u_1} {α β ε : Type u} [inst : Monad m] (mf : ExceptT ε m (α → β)) (x : ExceptT ε m α),
  mf <*> x = do
    let f ← mf
    f <$> x
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}),
  IsTopologicalGroup ↑(Profinite.limitCone (F.comp (CategoryTheory.forget₂ ProfiniteGrp.{max u v} Profinite))).pt.toTop
-- Mathlib.Tactic.Translate.GuessName
/-- Decapitalize the first element of a list if `s` starts with a lower-case letter.
Note that we need to decapitalize multiple characters in some cases,
in examples like `HMul` or `HAdd`.  -/
Mathlib.Tactic.GuessName.decapitalizeFirstLike : String → List String → List String
-- Init.Data.Vector.Lemmas
Vector.back.eq_1 : ∀ {n : ℕ} {α : Type u_1} [inst : NeZero n] (xs : Vector α n), xs.back = xs[n - 1]
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Given a list of length `n` and a composition `[i₁, ..., iₖ]` of `n`, split `l` into a list of
`k` lists corresponding to the blocks of the composition, of respective lengths `i₁`, ..., `iₖ`.
This makes sense mostly when `n = l.length`, but this is not necessary for the definition.  -/
List.splitWrtComposition : {n : ℕ} → {α : Type u_1} → List α → Composition n → List (List α)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.add_iInter₂_subset : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Add α] (s : Set α) (t : (i : ι) → κ i → Set α),
  s + ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s + t i j
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.δ'.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (self : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁), self.δ' n₀ n₁ h = self.δ' n₀ n₁ h