mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.CoextendScalars.map_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {M M' : ModuleCat R} (g : M ⟶ M')
  (x : ↑((ModuleCat.coextendScalars f).obj M)) (s : S),
  ((ModuleCat.CoextendScalars.equiv f M')
        ((CategoryTheory.ConcreteCategory.hom ((ModuleCat.coextendScalars f).map g)) x))
      s =
    (CategoryTheory.ConcreteCategory.hom g) (((ModuleCat.CoextendScalars.equiv f M) x) s)
-- Mathlib.RingTheory.Finiteness.Nakayama
Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (N : Submodule R M), N.FG → N ≤ I • N → ∃ r ∈ I, ∀ n ∈ N, r • n = n
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainLength_zero_right : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L)
  [inst_8 : Nontrivial L], α.IsNonZero → LieAlgebra.IsKilling.chainLength α 0 = 2
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
/-- `ZMod n` is (noncanonically) isomorphic to its group of characters.  -/
AddChar.zmodAddEquiv : {n : ℕ} → [NeZero n] → ZMod n ≃+ AddChar (ZMod n) ℂ
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
/-- If a function vanishes almost everywhere on `sᶜ`, then its integral on `s`
coincides with its integral on the whole space.  -/
MeasureTheory.VectorMeasure.setIntegral_eq_integral_of_ae_compl_eq_zero : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s → (∀ᵐ (x : X) ∂μ.variation, x ∉ s → f x = 0) → ∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.Data.Int.CharZero
RingHom.injective_int : ∀ {α : Type u_3} [inst : NonAssocRing α] (f : ℤ →+* α) [CharZero α], Function.Injective ⇑f
-- Mathlib.SetTheory.Ordinal.Basic
/-- The order type of an element inside a well order.

This is registered as a principal segment embedding into the ordinals, with top `type r`.  -/
Ordinal.typein : {α : Type u} → (r : α → α → Prop) → [IsWellOrder α r] → PrincipalSeg r fun x1 x2 => x1 < x2
-- Std.Time.DateTime
/-- Converts a `DateTime` to a `PlainDateTime`
 -/
Std.Time.DateTime.toPlainDateTime : Std.Time.DateTime → Std.Time.PlainDateTime
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveHypothesisBundle.mk.injEq : ∀ (names : Array String) (fvarIds : Array Lean.FVarId) (type : Lean.Widget.CodeWithInfos)
  (val? : Option Lean.Widget.CodeWithInfos) (isInstance? isType? isInserted? isRemoved? : Option Bool)
  (names_1 : Array String) (fvarIds_1 : Array Lean.FVarId) (type_1 : Lean.Widget.CodeWithInfos)
  (val?_1 : Option Lean.Widget.CodeWithInfos) (isInstance?_1 isType?_1 isInserted?_1 isRemoved?_1 : Option Bool),
  ({ names := names, fvarIds := fvarIds, type := type, val? := val?, isInstance? := isInstance?, isType? := isType?,
        isInserted? := isInserted?, isRemoved? := isRemoved? } =
      { names := names_1, fvarIds := fvarIds_1, type := type_1, val? := val?_1, isInstance? := isInstance?_1,
        isType? := isType?_1, isInserted? := isInserted?_1, isRemoved? := isRemoved?_1 }) =
    (names = names_1 ∧
      fvarIds = fvarIds_1 ∧
        type = type_1 ∧
          val? = val?_1 ∧
            isInstance? = isInstance?_1 ∧ isType? = isType?_1 ∧ isInserted? = isInserted?_1 ∧ isRemoved? = isRemoved?_1)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Probability.Kernel.Disintegration.Unique
/-- For `fst κ a`-almost all `b`, the conditional kernel `Kernel.condKernel κ` applied to `(a, b)`
is equal to the conditional kernel of the measure `κ a` applied to `b`.  -/
ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : ProbabilityTheory.Kernel α (β × Ω))
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] (a : α), (fun b => κ.condKernel (a, b)) =ᵐ[κ.fst a] ⇑(κ a).condKernel
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- `LinearIndepOn R v s` states that the vectors in the family `v` that are indexed
by the elements of `s` are linearly independent over `R`.  -/
LinearIndepOn : {ι : Type u'} →
  (R : Type u_2) →
    {M : Type u_4} → (ι → M) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Set ι → Prop
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- As the thickening radius δ tends to 0, the δ-thickened indicator of a set E (in α) tends
pointwise to the indicator function of the closure of E.

Note: This version is for the bundled bounded continuous functions, but the topology is not
the topology on `α →ᵇ ℝ≥0`. Coercions to functions `α → ℝ≥0` are done first, so the topology
instance is the product topology (the topology of pointwise convergence).  -/
thickenedIndicator_tendsto_indicator_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δseq : ℕ → ℝ} (δseq_pos : ∀ (n : ℕ), 0 < δseq n),
  Filter.Tendsto δseq Filter.atTop (nhds 0) →
    ∀ (E : Set α),
      Filter.Tendsto (fun n => ⇑(thickenedIndicator ⋯ E)) Filter.atTop (nhds ((closure E).indicator fun x => 1))
-- Mathlib.Topology.Spectral.Hom
SpectralMap.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : SpectralMap α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Order.Category.BddLat
BddLat.mk.sizeOf_spec : ∀ (toLat : Lat) [isBoundedOrder : BoundedOrder ↑toLat],
  sizeOf { toLat := toLat, isBoundedOrder := isBoundedOrder } = 1 + sizeOf toLat + sizeOf isBoundedOrder
-- Mathlib.LinearAlgebra.Dual.Defs
Module.evalEquiv.congr_simp : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.IsReflexive R M], Module.evalEquiv R M = Module.evalEquiv R M
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
sInf_ne_bot : ∀ {α : Type u_5} [inst : CompleteLinearOrder α] [Nontrivial α] {s : Set α}, s.Finite → ⊥ ∉ s → sInf s ≠ ⊥
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding.latticeBasis.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.canonicalEmbedding.latticeBasis K =
    (basisOfPiSpaceOfLinearIndependent ⋯).reindex (Fintype.equivOfCardEq ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.isPath_of_append_left : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u}, ¬q.Nil → (p.append q).IsCycle → p.IsPath
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.of_smul_left : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β}, (s • t).Nonempty → s.Nonempty
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
/-- a polynomial is `monic_at` if its trailing coefficient is 1  -/
Polynomial.TrailingMonic : {R : Type u} → [inst : Semiring R] → Polynomial R → Prop
-- Init.Data.SInt.Bitwise
Int16.toUInt16_and : ∀ (a b : Int16), (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toUnder_π_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (j : J),
  c.toUnder.π.app j = CategoryTheory.Under.homMk (c.π.app j) ⋯
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.isEmpty = false → ∀ {km fallback : α}, t.maxD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Lean.Meta.Tactic.NormCast
/-- Assuming `e` is an application, returns the list of subterms that `simp` will rewrite in.  -/
Lean.Meta.NormCast.getSimpArgs : Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Lean.Elab.InfoTree.Types
Lean.Elab.OptionInfo.optionName : Lean.Elab.OptionInfo → Lean.Name
-- Init.Data.Array.Lemmas
Array.getElem_eq_getD : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {h : i < xs.size} (fallback : α), xs[i] = xs.getD i fallback
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.invRev_invRev : ∀ {α : Type u} {L₁ : List (α × Bool)}, FreeGroup.invRev (FreeGroup.invRev L₁) = L₁
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- A function is a Schwartz function if it is smooth and all derivatives decay faster than
any power of `‖x‖`.  -/
SchwartzMap : (E : Type u_5) →
  (F : Type u_6) →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → Type (max u_5 u_6)
-- Mathlib.Data.Sum.Basic
Sum.update_inl_apply_inl : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ}
  {i j : α} {x : γ}, Function.update f (Sum.inl i) x (Sum.inl j) = Function.update (f ∘ Sum.inl) i x j
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `FunLike.coeAddMonoidHom_apply`. -/
QuadraticMap.coeFnAddMonoidHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β] (f : F), (FunLike.coeAddMonoidHom F α β) f = ⇑f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    P 2 ≠ 0 →
      Q 2 ≠ 0 →
        P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P 1 * Q 2 = W.negY Q * P 2 → W.add P Q = W.dblU P • ![0, 1, 0]
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Adding an analytic function does not change the logarithmic counting function for the poles.
 -/
ValueDistribution.logCounting_add_analyticOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f g : 𝕜 → E},
  Meromorphic f → AnalyticOn 𝕜 g Set.univ → ValueDistribution.logCounting (f + g) ⊤ = ValueDistribution.logCounting f ⊤
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote : {α : Type u_1} → [Lean.Grind.Semiring α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Mon → α
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.tendsto_log_nhdsNE_zero : Filter.Tendsto Real.log (nhdsWithin 0 {0}ᶜ) Filter.atBot
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
iteratedDeriv_succ_log : ∀ {n : ℕ} {x : ℂ}, x ∈ Complex.slitPlane → iteratedDeriv (n + 1) Complex.log x = (-1) ^ n * ↑n.factorial * x ^ (-↑n - 1)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.isoZeroOfMonoZero_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (x : CategoryTheory.Mono 0),
  (CategoryTheory.Limits.isoZeroOfMonoZero x).hom = 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalClosedEmbeddingContinuousFunctionalCalculus.mk : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : CommSemiring R] [inst_1 : Nontrivial R]
  [inst_2 : StarRing R] [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A]
  [inst_10 : IsScalarTower R A A] [inst_11 : SMulCommClass R A A]
  [toNonUnitalContinuousFunctionalCalculus : NonUnitalContinuousFunctionalCalculus R A p],
  (∀ (a : A) (ha : p a), Topology.IsClosedEmbedding ⇑(cfcₙHom ha)) →
    NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (n : ℤ) {Z : C} (h : S.X₃.X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr S.f).f n)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.descShortComplex S).f n) h) =
    CategoryTheory.CategoryStruct.comp (S.g.f n) h
-- Mathlib.Data.ZMod.Coprime
/-- If an integer `a` and a prime `p` satisfy `gcd a p ≠ 1`, then `a : ZMod p` is zero.  -/
ZMod.eq_zero_of_gcd_ne_one : ∀ {a : ℤ} {p : ℕ}, Nat.Prime p → a.gcd ↑p ≠ 1 → ↑a = 0
-- Mathlib.Geometry.Manifold.DerivationBundle
Derivation.evalAt_apply : ∀ {𝕜 : 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]
  (X :
    Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤))
  (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) (x : M), ((Derivation.evalAt x) X) f = (X f) x
-- Mathlib.Analysis.Convex.Segment
segment_translate_preimage : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (a b c : E), (fun x => a + x) ⁻¹' segment 𝕜 (a + b) (a + c) = segment 𝕜 b c
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.maxDepth : USize
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.comp_eq_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ V₂ : CategoryTheory.Endofunctor.Coalgebra F} (f : V₀ ⟶ V₁) (g : V₁ ⟶ V₂),
  CategoryTheory.Endofunctor.Coalgebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Data.List.AList
AList.lookup_insert_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {b' : β a'} {s : AList β},
  a ≠ a' → AList.lookup a (AList.insert a' b' s) = AList.lookup a s
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det.eq_1 : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R),
  M.det = Matrix.detRowAlternating M
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- The finite rank support is contained in a set if and only if
the rank vanishes outside that set.  -/
GradedObject.finrankSupport_subset_iff : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_2} (X : CategoryTheory.GradedObject ι (ModuleCat R)) (s : Set ι),
  GradedObject.finrankSupport X ⊆ s ↔ ∀ i ∉ s, Module.finrank R ↑(X i) = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.keyAtIdx_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {h' : i < t₁.size} (h : t₁.Equiv t₂), t₁.keyAtIdx i h' = t₂.keyAtIdx i ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM_toList : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldrM f init t = List.foldrM (fun a b => f a.fst a.snd b) init t.toList
-- Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit
SSet.N.toSemiSimplexCategory_map : ∀ (X : SSet) [inst : X.Nonsingular] {X_1 Y : X.N} (f : X_1 ⟶ Y),
  (SSet.N.toSemiSimplexCategory X).map f = SemiSimplexCategory.homOfMono (SSet.N.monoOfLE ⋯)
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- The `δ`-thickened indicator of a set `E` is the function that equals `1` on `E`
and `0` outside a `δ`-thickening of `E` and interpolates (continuously) between
these values using `infEDist _ E`.

`thickenedIndicator` is the (bundled) bounded continuous function with `ℝ≥0`-values.
See `thickenedIndicatorAux` for the unbundled `ℝ≥0∞`-valued function.  -/
thickenedIndicator : {α : Type u_1} → [inst : PseudoEMetricSpace α] → {δ : ℝ} → 0 < δ → Set α → BoundedContinuousFunction α NNReal
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyδOfTriangle.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  CochainComplex.homologyδOfTriangle T n₀ n₁ h = CochainComplex.homologyδOfTriangle T n₀ n₁ h
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (t.insertMany l).getKey? k' = some k
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.LeftHomologyData) (H₂ : S₂.LeftHomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁)
  (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  CategoryTheory.ShortComplex.leftHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} {fallback : β}, t.contains a = false → Std.ExtDTreeMap.Const.getD t a fallback = fallback
-- Lean.Level
Lean.Level.addOffsetAux : ℕ → Lean.Level → Lean.Level
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₂ → (t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Submonoid.LocalizationMap.lift₀.congr_simp : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  {P : Type u_3} [inst_2 : CommMonoidWithZero P] (f f_1 : S.LocalizationMap N),
  f = f_1 → ∀ (g g_1 : M →*₀ P) (e_g : g = g_1) (hg : ∀ (y : ↥S), IsUnit (g ↑y)), f.lift₀ g hg = f_1.lift₀ g_1 ⋯
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- The structure sheaf (valued in `Type`, not yet `CommRing`) is the subsheaf consisting of
functions satisfying `isLocallyFraction`.  -/
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) → [inst_3 : GradedRing 𝒜] → TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top 𝒜)
-- Mathlib.Data.Nat.Log
Nat.clog_pos : ∀ {b n : ℕ}, 1 < b → 1 < n → 0 < Nat.clog b n
-- Mathlib.Analysis.Matrix.Normed
/-- This applies to the Frobenius norm.  -/
Matrix.frobeniusNormSMulClass : ∀ {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedRing R] [inst_3 : SeminormedAddCommGroup α] [inst_4 : Module R α] [NormSMulClass R α],
  NormSMulClass R (Matrix m n α)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α}
  {h' : k ∈ Std.DHashMap.Raw.filterMap f m} (h : m.WF),
  Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.filterMap f m) k h' =
    (f (m.getKey k ⋯) (Std.DHashMap.Raw.Const.get m k ⋯)).get ⋯
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkPushforward.id : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (ℱ : TopCat.Presheaf C X) (x : ↑X),
  TopCat.Presheaf.stalkPushforward C (CategoryTheory.CategoryStruct.id X) ℱ x =
    (TopCat.Presheaf.stalkFunctor C x).map (TopCat.Presheaf.Pushforward.id ℱ).hom
-- Init.Data.Int.Pow
Int.toNat_pow_of_nonneg : ∀ {x : ℤ}, 0 ≤ x → ∀ (k : ℕ), (x ^ k).toNat = x.toNat ^ k
-- Mathlib.Topology.Algebra.UniformMulAction
IsUnit.smul_uniformity : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : Monoid M] [inst_2 : MulAction M X]
  [UniformContinuousConstSMul M X] {c : M}, IsUnit c → c • uniformity X = uniformity X
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuousAt_add_bot_bot : ContinuousAt (fun p => p.1 + p.2) (⊥, ⊥)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_div_cancel₀ : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {b : G₀} (a : G₀), b ≠ 0 → b * (a / b) = a
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.norm_eq_integral : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (f : ↥(α →₁ₛ[μ] E)),
  ‖f‖ =
    MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map norm (MeasureTheory.Lp.simpleFunc.toSimpleFunc f))
-- Lean.DocString.Syntax
/-- Description list  -/
Lean.Doc.Syntax.dl : Lean.ParserDescr
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_2 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (idx : α)
  (h_1 : Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx_1 : α) → Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.atom idx_1 → motive (Std.Sat.AIG.Decl.atom idx_1))
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match elem : Std.Sat.AIG.Decl.atom idx with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx_1 => h_2 idx_1 elem
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs elem) =
    h_2 idx ⋯
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.TreeMap.Raw.get! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited β] → Std.TreeMap.Raw α β cmp → α → β
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
CategoryTheory.Limits.PreservesProduct.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasProduct f]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => G.obj (f j)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G],
  (CategoryTheory.Limits.PreservesProduct.iso G f).hom = CategoryTheory.Limits.piComparison G f
-- Init.Control.Lawful.MonadAttach.Instances
instLawfulMonadAttachStateRefT'OfLawfulMonad : ∀ {m : Type → Type} {ω σ : Type} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m],
  LawfulMonadAttach (StateRefT' ω σ m)