mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  (t : CategoryTheory.Limits.ColimitCocone F) (j : J) {Z : C} (h : t.cocone.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.isoColimitCocone t).hom h) =
    CategoryTheory.CategoryStruct.comp (t.cocone.ι.app j) h
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.mapDomain_smul : ∀ {α : Type u_1} {β : Type u_2} {R : Type u_4} {M : Type u_5} (f : α → β) [inst : AddCommMonoid M]
  [inst_1 : Filter.TendstoCofinite f] [inst_2 : DistribSMul R M] (r : R) (v : α → M),
  Filter.TendstoCofinite.mapDomain f (r • v) = r • Filter.TendstoCofinite.mapDomain f v
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tanh.eq_1 : ∀ (z : ℂ), Complex.tanh z = Complex.sinh z / Complex.cosh z
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.norm_integral_eq_norm_integral_uIoc : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  (f : ℝ → E), ‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Set.uIoc a b, f x ∂μ‖
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncFinset_monomial_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} {x : σ →₀ ℕ} (r : R),
  x ∉ s → (MvPowerSeries.truncFinset R s) ((MvPowerSeries.monomial x) r) = 0
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk_assoc : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (V : (TopologicalSpace.Opens ↑Y)ᵒᵖ) (x : ↑X)
  (hx : (CategoryTheory.ConcreteCategory.hom f) x ∈ Opposite.unop V) {Z : C}
  (h : F.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app V)
      (CategoryTheory.CategoryStruct.comp
        (TopCat.Presheaf.germToPullbackStalk C f F ((TopologicalSpace.Opens.map f).obj (Opposite.unop V)) x hx) h) =
    CategoryTheory.CategoryStruct.comp (F.germ (Opposite.unop V) ((CategoryTheory.ConcreteCategory.hom f) x) hx) h
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Three points are collinear if and only if they are not affinely independent.  -/
collinear_iff_not_affineIndependent_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p : Fin 3 → P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → (Collinear k {p i₁, p i₂, p i₃} ↔ ¬AffineIndependent k p)
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- Construct a profunctor from a `ProfunctorCore`.  -/
CategoryTheory.Profunctor.ofCore : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D → CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.congr_left : ∀ {α : Type u} {β : Type v} {m₁ m₂ m₃ : Std.HashMap.Raw α β}, m₁.Equiv m₂ → (m₁.Equiv m₃ ↔ m₂.Equiv m₃)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.all.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (p : (a : α) → β a → Bool),
  t.all p = t.inner.all p
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.RankLeOneStruct.mk : {R : Type u_1} →
  [inst : Semiring R] →
    [inst_1 : ValuativeRel R] →
      (emb : ValuativeRel.ValueGroupWithZero R →*₀ NNReal) → StrictMono ⇑emb → ValuativeRel.RankLeOneStruct R
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The sum over the values of the quadratic character is zero when the characteristic is odd.  -/
quadraticChar_sum_zero : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 → ∑ a, (quadraticChar F) a = 0
-- Mathlib.Topology.LocallyConstant.Basic
/-- The underlying function.  -/
LocallyConstant.toFun : {X : Type u_5} → {Y : Type u_6} → [inst : TopologicalSpace X] → LocallyConstant X Y → X → Y
-- Mathlib.Topology.Instances.Real.Lemmas
Real.totallyBounded_ball : ∀ (x ε : ℝ), TotallyBounded (Metric.ball x ε)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
IsGLB.ciInf_eq : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {a : α} [Nonempty ι] {f : ι → α},
  IsGLB (Set.range f) a → ⨅ i, f i = a
-- Init.Data.Rat.Lemmas
Rat.add_lt_add_left : ∀ {a b c : ℚ}, c + a < c + b ↔ a < b
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instPseudoEMetricSpace : {X : Type u_1} →
  {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [PseudoEMetricSpace X] → PseudoEMetricSpace (Metric.Snowflaking X α hα₀ hα₁)
-- Mathlib.Topology.Compactness.Lindelof
/-- A filter with the countable intersection property that is finer than the principal filter on
a Lindelöf set `s` contains any open set that contains all cluster points of `s`.  -/
IsLindelof.adherence_nhdset : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} {f : Filter X} [CountableInterFilter f],
  IsLindelof s → f ≤ Filter.principal s → IsOpen t → (∀ x ∈ s, ClusterPt x f → x ∈ t) → t ∈ f
-- Mathlib.Algebra.Lie.Basic
LieEquiv.surjective : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂), Function.Surjective ⇑e.toLieHom
-- Init.Data.Nat.Lemmas
Nat.pow_dvd_of_le_of_pow_dvd : ∀ {p m n k : ℕ}, m ≤ n → p ^ n ∣ k → p ^ m ∣ k
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_counitIso_inv_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T'),
  ((CategoryTheory.StructuredArrow.mapNatIso i).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.isQuotientMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f → Function.Surjective f → Topology.IsQuotientMap f
-- Mathlib.Order.Concept
Concept.ofObjects_extent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r}, Concept.ofObjects r c.extent = c
-- Lean.Data.NameMap.Basic
Lean.NameSet.instForInNameOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m Lean.NameSet Lean.Name
-- Mathlib.Data.Set.Lattice
Set.sUnion_eq_compl_sInter_compl : ∀ {α : Type u_1} (S : Set (Set α)), ⋃₀ S = (⋂₀ (compl '' S))ᶜ
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_smul_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] (A : Type u_5) [inst_3 : CommSemiring A] [inst_4 : Algebra R A] [inst_5 : Module A M']
  [inst_6 : IsLocalization S A] [inst_7 : Module R M] [inst_8 : Module R M'] [IsScalarTower R A M'] (f : M →ₗ[R] M')
  [inst_10 : IsLocalizedModule S f] (x : R) (m : M) (s t : ↥S),
  IsLocalization.mk' A x s • IsLocalizedModule.mk' f m t = IsLocalizedModule.mk' f (x • m) (s * t)
-- Lean.Meta.Instances
Lean.Meta.instInhabitedInstanceEntry : Inhabited Lean.Meta.InstanceEntry
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.ofTree.eq_def : ∀ (x : BinaryTree Unit),
  DyckWord.ofTree x =
    match x with
    | BinaryTree.nil => 0
    | BinaryTree.node value l r => (DyckWord.ofTree l).nest + DyckWord.ofTree r
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_inf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : α → M},
  (φ ⊓ ψ).Realize v ↔ φ.Realize v ∧ ψ.Realize v
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.rightUnitor_hom_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : SemimoduleCat R} (m : ↑M) (r : R),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom) (m ⊗ₜ[R] r) = r • m
-- Mathlib.Combinatorics.Quiver.Arborescence
/-- A path from `r` of minimal length.  -/
Quiver.shortestPath : {V : Type u} → [inst : Quiver V] → (r : V) → [Quiver.RootedConnected r] → (b : V) → Quiver.Path r b
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Hom.ext : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} {x y : X.Hom Y}, x.base = y.base → x.c ≍ y.c → x = y
-- Init.Data.List.TakeDrop
List.dropWhile.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α),
  List.dropWhile p (a :: as) =
    match p a with
    | true => List.dropWhile p as
    | false => a :: as
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.isUnit_addZ_of_X_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P → W.Equation Q → P 0 * Q 2 ≠ Q 0 * P 2 → IsUnit (W.addZ P Q)
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ico_succ_right_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Finset.Ico a (Order.succ b) = Finset.Icc a b
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

The monadic effects of `f` are interleaved with potential effects caused by the iterator's step
function. Therefore, it may *not* be equivalent to `it.toList.foldlM`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.foldM`.
 -/
Std.IterM.Total.foldM : {m n : Type w → Type w'} →
  [Monad n] →
    {α β γ : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m n] →
          [MonadLiftT m n] → [Std.Iterators.Finite α m] → (γ → β → n γ) → γ → Std.IterM.Total m β → n γ
-- Mathlib.Algebra.Order.Group.PosPart
posPart_zero : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α], 0⁺ = 0
-- Batteries.Data.UnionFind.Basic
_private.Batteries.Data.UnionFind.Basic.0.Batteries.UnionFind.rank'_lt_rankMax.go : ∀ {l : List Batteries.UFNode} {x : Batteries.UFNode}, x ∈ l → x.rank ≤ List.foldr (fun x => max x.rank) 0 l
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.cast_blocks : ∀ {n m : ℕ} (c : Composition m) (hmn : m = n), (c.cast hmn).blocks = c.blocks
-- Init.Data.Array.Erase
Array.eraseIdx_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {k : ℕ} {h : k < (Array.replicate n a).size},
  (Array.replicate n a).eraseIdx k h = Array.replicate (n - 1) a
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_add_cancel_right : ∀ {m n k : ℤ} (i : ℤ), (m + i) % n = (k + i) % n ↔ m % n = k % n
-- Std.Time.DateTime.Timestamp
/-- Subtracts a `Millisecond.Offset` from the given `Timestamp`.
 -/
Std.Time.Timestamp.subMilliseconds : Std.Time.Timestamp → Std.Time.Millisecond.Offset → Std.Time.Timestamp
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.SMul.sigmaFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (c : NNReal),
  MeasureTheory.SigmaFinite (c • μ)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.fun_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} {𝓨 : Type u_3} {m𝓨 : MeasurableSpace 𝓨}
  {ν : MeasureTheory.Measure 𝓨} {Y : 𝓧 → 𝓨},
  ProbabilityTheory.HasLaw Y ν μ → ProbabilityTheory.HasLaw X μ P → ProbabilityTheory.HasLaw (fun ω => Y (X ω)) ν P
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E]
  {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → ∀ [SMulCommClass 𝕜 R E] (c : R), MeromorphicOn (c • f) U
-- Mathlib.Data.Finset.Sups
Finset.diffs_subset_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t₁ t₂ : Finset α},
  t₁ ⊆ t₂ → s.diffs t₁ ⊆ s.diffs t₂
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from additive groups to types creates all limits.  -/
AddGrpCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddGrpCat)
-- Std.Async.Basic
/-- Converts a `EAsync` to a `ETask`.
 -/
Std.Async.EAsync.toBaseIO : {ε α : Type} → Std.Async.EAsync ε α → BaseIO (Std.Async.ETask ε α)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.trivial_grp_inv : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.GrpObj.inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.bot_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M), ⊥ ∈ f.invtSubmodule
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.support_eq_inter_preimage : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E],
  Function.support ↑f = (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' Metric.ball (↑(extChartAt I c) c) f.rOut
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.mul_comul : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul))
-- Init.Data.Order.Classes
Std.LawfulOrderSup.max_le_iff : ∀ {α : Type u} {inst : Max α} {inst_1 : LE α} [self : Std.LawfulOrderSup α] (a b c : α), a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.eq_of_adj_left : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v w : V}, M.IsMatching → M.Adj u v → M.Adj u w → v = w
-- Mathlib.LinearAlgebra.LinearPMap
LinearMap.compPMap_apply : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Ring T] {σ : R →+* S}
  {τ : S →+* T} {E : Type u_4} [inst_3 : AddCommGroup E] [inst_4 : Module R E] {F : Type u_5} [inst_5 : AddCommGroup F]
  [inst_6 : Module S F] {G : Type u_6} [inst_7 : AddCommGroup G] [inst_8 : Module T G] (g : F →ₛₗ[τ] G)
  (f : E →ₛₗ.[σ] F) (x : ↥(g.compPMap f).domain), ↑(g.compPMap f) x = g (↑f x)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_injective : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q], Function.Injective DFunLike.coe
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.apply.congr_simp : ∀ (𝕜 : Type u_1) {ι : Type u_2} (E : ι → Type u_3) (F : Type u_4) [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : ∀ (i : ι), ContinuousSMul 𝕜 (E i)] [inst_9 : ContinuousConstSMul 𝕜 F]
  (m m_1 : (i : ι) → E i), m = m_1 → ContinuousMultilinearMap.apply 𝕜 E F m = ContinuousMultilinearMap.apply 𝕜 E F m_1
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.mk'.hcongr_4 : ∀ (X X' : SSet),
  X = X' →
    ∀ (A : X.Subcomplex) (A' : X'.Subcomplex),
      A ≍ A' →
        ∀ (toN : X.N) (toN' : X'.N),
          toN ≍ toN' →
            ∀ (notMem : toN.simplex ∉ A.obj (Opposite.op { len := toN.dim }))
              (notMem' : toN'.simplex ∉ A'.obj (Opposite.op { len := toN'.dim })),
              notMem ≍ notMem' → { toN := toN, notMem := notMem } ≍ { toN := toN', notMem := notMem' }
-- Lean.DocString.Types
Lean.Doc.Inline.code.injEq : ∀ {i : Type u} (string string_1 : String),
  (Lean.Doc.Inline.code string = Lean.Doc.Inline.code string_1) = (string = string_1)
-- Lean.Compiler.MetaAttr
/-- Whether a declaration should be exported for interpretation.  -/
Lean.isDeclMeta : Lean.Environment → Lean.Name → Bool
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.limitConeComp_isLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone G),
  (CategoryTheory.Functor.Initial.limitConeComp F t).isLimit =
    (CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F t.cone).symm t.isLimit
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
Irreducible.addVal_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {ϖ : R},
  Irreducible ϖ → ∀ (n : ℕ), (IsDiscreteValuationRing.addVal R) (ϖ ^ n) = ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- The monomorphism condition on `f`  -/
CategoryTheory.StrongMono.mono : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongMono f],
  CategoryTheory.Mono f
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- If two morphisms on `G` coincide on the elements of a basis, then they coincide.  -/
FreeAddGroupBasis.ext_hom : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H] (b : FreeAddGroupBasis ι G)
  (f g : G →+ H), (∀ (i : ι), f (b i) = g (b i)) → f = g
-- Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
MeasureTheory.FinStronglyMeasurable.exists_measurableSet_measure_pos_lt_top : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → E}, MeasureTheory.FinStronglyMeasurable f μ → ¬f =ᵐ[μ] 0 → ∃ s, MeasurableSet s ∧ 0 < μ s ∧ μ s < ⊤
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.instOneWithConv : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Semiring C] → [inst_3 : Bialgebra R C] → [inst_4 : Algebra R A] → One (WithConv (C →ₐ[R] A))
-- Mathlib.Algebra.Module.ZLattice.Basic
Module.Basis.ofZLatticeComap_repr_apply : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E)
  (e : F ≃ₗ[K] E) {ι : Type u_4} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (i : ι),
  ((Module.Basis.ofZLatticeComap K L e b).repr ((ZLattice.comap_equiv K L e) x)) i = (b.repr x) i
-- Init.Data.UInt.Lemmas
UInt8.toNat_toBitVec : ∀ (x : UInt8), x.toBitVec.toNat = x.toNat
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.two_le_natDegree_subalgebra : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_4} [inst_1 : CommRing B] [inst_2 : Algebra A B] [Nontrivial B]
  {S : Subalgebra A B} {x : B}, IsIntegral (↥S) x → (2 ≤ (minpoly (↥S) x).natDegree ↔ x ∉ S)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_unitOfList_le : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  (Std.TreeMap.Raw.unitOfList l cmp).size ≤ l.length
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.instUnique : {M : Type u_7} →
  {N : Type u_8} →
    [Unique M] → [Unique N] → [inst : Add M] → [inst_1 : Mul M] → [inst_2 : Add N] → [inst_3 : Mul N] → Unique (M ≃+* N)
-- Init.Data.UInt.Lemmas
UInt32.pow_succ : ∀ (x : UInt32) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Batteries.Data.Fin.Coding
/-- Encode `Option (Fin n)` into `Fin (n+1)`.  -/
Fin.encodeOption : {n : ℕ} → Option (Fin n) → Fin (n + 1)
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The canonical map from `Z` to the pushout of `D₁.t W Z` and `D₁.l W Z`.  -/
CategoryTheory.OrthogonalReflection.toStep : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
            [inst_3 : CategoryTheory.Limits.HasPushouts C] → Z ⟶ CategoryTheory.OrthogonalReflection.step W Z
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.containsThenInsert_fst : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m.containsThenInsert k).1 = m.contains k
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
/-- A greatest element of a set is the supremum of this set.  -/
IsGreatest.csSup_eq : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α}, IsGreatest s a → sSup s = a
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_mapIso_hom : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.Sigma.mapIso p).hom =
    CategoryTheory.CategoryStruct.comp (p b).hom (CategoryTheory.Limits.Sigma.ι g b)
-- Aesop.RuleTac.GoalDiff
Aesop.GoalDiff.check : Aesop.GoalDiff → Lean.MVarId → Lean.MVarId → Aesop.BaseM (Option Lean.MessageData)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.forIn_eq_forIn_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  (forIn t init fun a d => f a.1 d) = forIn t.keys init f
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_lt_typein : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {a b : α},
  (Ordinal.typein r).toRelEmbedding a < (Ordinal.typein r).toRelEmbedding b ↔ r a b
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.eventually_mem_spanningSets : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] (x : α),
  ∀ᶠ (n : ℕ) in Filter.atTop, x ∈ MeasureTheory.spanningSets μ n
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- If `P` is local at the target, to show that `P` is stable under base change, it suffices to
check this for base change along a morphism of affine schemes.  -/
AlgebraicGeometry.AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isZariskiLocalAtTarget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtTarget P],
  (AlgebraicGeometry.AffineTargetMorphismProperty.of P).IsStableUnderBaseChange → P.IsStableUnderBaseChange