mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.smul : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E] (c : T → ℝ),
  ProbabilityTheory.IsGaussianProcess X P → ProbabilityTheory.IsGaussianProcess (fun t ω => c t • X t ω) P
-- Mathlib.CategoryTheory.Action.Limits
/-- `F.mapAction : Action V G ⥤ Action W G` preserves finite colimits if
`V` has finite colimits and `F` preserves finite colimits.  -/
Action.Functor.instPreservesFiniteColimitsMapActionOfHasFiniteColimits : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [inst_2 : Monoid G]
  [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.HasFiniteColimits V],
  CategoryTheory.Limits.PreservesFiniteColimits (F.mapAction G)
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_mul_aux : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p q : Polynomial R},
  gcd (p * q).eraseLead.content p.leadingCoeff = gcd (p.eraseLead * q).content p.leadingCoeff
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.fromOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {S : C} → (X : CategoryTheory.Over S) → CategoryTheory.OverClass X.left S
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact : ∀ {S : AlgebraicGeometry.Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [AlgebraicGeometry.QuasiCompactCover 𝒰]
  {U : S.Opens}, IsCompact ↑U → IsCompactOpenCovered (fun x => ⇑(𝒰.f x)) ↑U
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.rename_comp_toMvPowerSeries : ∀ {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [inst : CommSemiring R] (f : σ → τ) [inst_1 : Filter.TendstoCofinite f]
  (a : σ), (MvPowerSeries.rename f).comp (PowerSeries.toMvPowerSeries a) = PowerSeries.toMvPowerSeries (f a)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).get k h' = m₂.get k ⋯
-- Init.Data.Vector.MapIdx
_private.Init.Data.Vector.MapIdx.0.Vector.mapFinIdxM.map.match_1.splitter : {n : ℕ} →
  (j : ℕ) →
    (motive : (i : ℕ) → i + j = n → Sort u_1) →
      (i : ℕ) →
        (inv : i + j = n) →
          ((inv : 0 + j = n) → motive 0 inv) → ((i : ℕ) → (inv : i + 1 + j = n) → motive i.succ inv) → motive i inv
-- Mathlib.Analysis.Calculus.Deriv.Abs
hasDerivWithinAt_abs : ∀ (s : Set ℝ) {x : ℝ}, x ≠ 0 → HasDerivWithinAt (fun x => |x|) (↑(SignType.sign x)) s x
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.inter_cylinder_longestPrefix_nonempty : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  {s : Set ((n : ℕ) → E n)},
  IsClosed s → s.Nonempty → ∀ (x : (n : ℕ) → E n), (s ∩ PiNat.cylinder x (PiNat.longestPrefix x s)).Nonempty
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_right_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r₁ r₂ : R} {m : M},
  AddMonoidAlgebra.single m r₁ = AddMonoidAlgebra.single m r₂ ↔ r₁ = r₂
-- Mathlib.Order.Filter.Tendsto
Filter.not_tendsto_iff_exists_frequently_notMem : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
  ¬Filter.Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ (x : α) in l₁, f x ∉ s
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.constantsVarsEquivLeft.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1},
  FirstOrder.Language.Term.constantsVarsEquivLeft =
    FirstOrder.Language.Term.constantsVarsEquiv.trans
      (FirstOrder.Language.Term.relabelEquiv (Equiv.sumAssoc γ α β)).symm
-- Lean.Util.NumObjs
Lean.Expr.NumObjs.State.visited : Lean.Expr.NumObjs.State → Lean.PtrSet Lean.Expr
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.skipWhile_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String.Slice} {pos : s.Pos},
  pos.skipWhile pat = (String.Slice.Pattern.Model.matchAt? pat pos).elim pos fun x => x.skipWhile pat
-- Mathlib.NumberTheory.Real.Irrational
Irrational.sub_natCast : ∀ {x : ℝ}, Irrational x → ∀ (m : ℕ), Irrational (x - ↑m)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.comap_equiv_eq_map_symm : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S) (K : Subsemiring S),
  Subsemiring.comap (↑f) K = Subsemiring.map (↑f.symm) K
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SzemerediRegularity.star_subset_chunk : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {V : Finset α},
  SzemerediRegularity.star hP G ε hU V ⊆ (SzemerediRegularity.chunk hP G ε hU).parts
-- Mathlib.FieldTheory.Finiteness
IsNoetherian.coeSort_finsetBasisIndex : ∀ (K : Type u) (V : Type v) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : IsNoetherian K V], ↥(IsNoetherian.finsetBasisIndex K V) = ↑(Module.Basis.ofVectorSpaceIndex K V)
-- Mathlib.Data.Nat.Choose.Central
Nat.two_dvd_centralBinom_of_one_le : ∀ {n : ℕ}, 0 < n → 2 ∣ n.centralBinom
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.instIsCorepresentableCompEvalObjOppositeFunctorTypeCoyonedaOp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_2} (c : ComplexShape ι) [c.HasNoLoop] (X : C) (j : ι),
  ((HomologicalComplex.eval C c j).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).IsCorepresentable
-- Mathlib.Data.EReal.Inv
EReal.inv_bot : ⊥⁻¹ = 0
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.isoMk_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e₁ : S₁.X₁ ≅ S₂.X₁) (e₂ : S₁.X₂ ≅ S₂.X₂) (e₃ : S₁.X₃ ≅ S₂.X₃)
  (comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom)
      CategoryTheory.ShortComplex.isoMk._auto_1)
  (comm₂₃ :
    autoParam (CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom)
      CategoryTheory.ShortComplex.isoMk._auto_3),
  (CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).inv =
    CategoryTheory.ShortComplex.homMk e₁.inv e₂.inv e₃.inv ⋯ ⋯
-- Mathlib.Data.PNat.Interval
PNat.instLocallyFiniteOrder : LocallyFiniteOrder ℕ+
-- Mathlib.Combinatorics.SimpleGraph.Tutte
SimpleGraph.universalVerts.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V), G.universalVerts = {v | G.IsUniversal v}
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasDerivWithinAt.fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → ∀ (n : ℕ), HasDerivWithinAt (fun x => f x ^ n) (↑n * f x ^ (n - 1) * f') s x
-- Init.Data.Rat.Lemmas
Rat.neg_neg : ∀ (a : ℚ), - -a = a
-- Mathlib.RingTheory.Noetherian.Defs
Ideal.fg_of_isNoetherianRing : ∀ {R : Type u_1} [inst : Semiring R] [IsNoetherianRing R] (I : Ideal R), I.FG
-- Lean.AuxRecursor
Lean.NoConfusionInfo.arity : Lean.NoConfusionInfo → ℕ
-- Mathlib.Algebra.Field.Defs
/-- `a ^ 0 = 1`  -/
DivisionRing.zpow_zero' : ∀ {K : Type u_2} [self : DivisionRing K] (a : K), a ^ 0 = 1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_subset_edgeFinset : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet],
  G₁.edgeFinset ⊆ G₂.edgeFinset ↔ G₁ ≤ G₂
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.whiskerRight : ∀ {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 D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) [inst_6 : F₁.LaxMonoidal] [inst_7 : F₂.LaxMonoidal]
  {G₁ : CategoryTheory.Functor D E} [inst_8 : G₁.LaxMonoidal] [CategoryTheory.NatTrans.IsMonoidal τ],
  CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.Functor.whiskerRight τ G₁)
-- Mathlib.Control.Fix
Part.fix_def : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) {x : α}
  (h' : ∃ i, (Part.Fix.approx f i x).Dom), Part.fix f x = Part.Fix.approx f (Nat.find h').succ x
-- Mathlib.Data.Fintype.EquivFin
Fintype.false : ∀ {α : Type u_1} [Infinite α] (_h : Fintype α), False
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.instFaithfulSkeletonFromSkeleton : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.fromSkeleton C).Faithful
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instToJsonAbsoluteLspSemanticToken.toJson : Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Json
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_inter_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLEMk_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ A₃ : C} (f : A₁ ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (g : A₂ ⟶ B) [inst_2 : CategoryTheory.Mono g] (h : A₃ ⟶ B)
  [inst_3 : CategoryTheory.Mono h] (h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
  (h₂ : CategoryTheory.Subobject.mk g ≤ CategoryTheory.Subobject.mk h) {Z : C} (h_1 : A₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk g h h₂) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f h ⋯) h_1
-- Mathlib.Algebra.Star.Pi
Pi.instStarModuleForall : ∀ {I : Type u} {f : I → Type v} {R : Type w} [inst : (i : I) → SMul R (f i)] [inst_1 : Star R]
  [inst_2 : (i : I) → Star (f i)] [∀ (i : I), StarModule R (f i)], StarModule R ((i : I) → f i)
-- Mathlib.Util.PPOptions
/-- Gets whether `pp.mathlib.binderPredicates` is enabled.  -/
Mathlib.getPPBinderPredicates : Lean.Options → Bool
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.translate.congr_simp : ∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] (f f_1 : F),
  f = f_1 →
    ∀ [inst_1 : ModularFormClass F Γ k] (g : GL (Fin 2) ℝ), ModularForm.translate f g = ModularForm.translate f_1 g
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.dual_symm_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] (f : sSupHom αᵒᵈ βᵒᵈ) (a : α),
  (sInfHom.dual.symm f) a = (⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual) a
-- Init.Data.Rat.Lemmas
Rat.intCast_neg : ∀ (a : ℤ), ↑(-a) = -↑a
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.image_preimage : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β) (s : Set β),
  ⇑h '' ⇑h ⁻¹' s = s
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.rfind' : Nat.Partrec.Code → Nat.Partrec.Code
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- The image of an element `m : M` in `R[M]` belongs to the submodule generated by
`s : Set M` if and only if `m ∈ s`.  -/
MonoidAlgebra.of_mem_span_of_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : MulOneClass M] {s : Set M} {m : M} [Nontrivial R],
  (MonoidAlgebra.of R M) m ∈ Submodule.span R (⇑(MonoidAlgebra.of R M) '' s) ↔ m ∈ s
-- Batteries.Data.Float.Lemmas
Float32.beq_nan_eq_false : ∀ (f : Float32), (f == Float32.nan) = false
-- Mathlib.Analysis.CStarAlgebra.Extreme
/-- The star projections in a non-unital C⋆-algebra are exactly the extreme points of
the nonnegative closed unit ball.  -/
isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {e : A},
  IsStarProjection e ↔ e ∈ Set.extremePoints ℝ ({x | 0 ≤ x} ∩ Metric.closedBall 0 1)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- The identity morphism of a `PresheafedSpace`.  -/
AlgebraicGeometry.PresheafedSpace.id : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → (X : AlgebraicGeometry.PresheafedSpace C) → X.Hom X
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Subtype.inf : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} → [inst_1 : Ring M] → [inst_2 : Module M X] → [FaithfulSMul M X] → Min { P // IsLprojection X P }
-- Mathlib.Order.Category.Lat
Lat.comp_apply : ∀ {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Tactic.Translate.Reorder
/-- Reorder the given metavariables using the given `ArgReorder`.  -/
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.reorderMVars : Array Lean.Expr → Mathlib.Tactic.Translate.ArgReorder → Lean.MetaM (Array Lean.Expr)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.keyAtIdx?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {i : ℕ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keyAtIdx? i = t₂.keyAtIdx? i
-- Mathlib.Algebra.Module.Torsion.Basic
_private.Mathlib.Algebra.Module.Torsion.Basic.0.Submodule.disjoint_torsionBySet_ideal.match_1_1.splitter : (motive : Fin 2 → Sort u_1) → (x : Fin 2) → (Unit → motive 0) → (Unit → motive 1) → motive x
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An additive submonoid of an additive monoid `M` can be considered as an
additive subsemigroup of that additive monoid.  -/
AddSubmonoid.toAddSubsemigroup : {M : Type u_3} → [inst : AddZeroClass M] → AddSubmonoid M → AddSubsemigroup M
-- Mathlib.Order.Hom.Basic
OrderIso.funUnique_apply : ∀ (α : Type u_6) (β : Type u_7) [inst : Unique α] [inst_1 : Preorder β] (f : (i : α) → (fun a => β) i),
  (OrderIso.funUnique α β) f = f default
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.coe_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] (g : β →ᵈ γ) (f : α →ᵈ β), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Lean.Parser
Lean.PrettyPrinter.Parenthesizer.charLit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.ContinuousOn
/-- A function is continuous on two closed sets iff it is also continuous on their union.  -/
continuousOn_union_iff_of_isClosed : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s t : Set α} {f : α → β},
  IsClosed s → IsClosed t → (ContinuousOn f (s ∪ t) ↔ ContinuousOn f s ∧ ContinuousOn f t)
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.presheafEquivOfIso_functor_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) {X_1 Y_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ}
  (f : X_1 ⟶ Y_1),
  ((TopCat.Presheaf.presheafEquivOfIso C H).functor.obj G).map f =
    G.map ((TopologicalSpace.Opens.map H.hom).map f.unop).op
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.anyLTTR.loop.eq_1 : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (x_2 : 0 ≤ n), Nat.anyLTTR.loop✝ n f 0 x_2 = false
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.add_iff_left : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M N : Matrix m m R} {b : m → α} [inst : LT α] [inst_1 : AddGroup R],
  N.BlockTriangular b → ((M + N).BlockTriangular b ↔ M.BlockTriangular b)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.iteratedFDeriv_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {m n : WithTop ℕ∞}
  {i : ℕ}, ContDiff 𝕜 n f → m + ↑i ≤ n → ContDiff 𝕜 m (iteratedFDeriv 𝕜 i f)
-- Mathlib.Tactic.Widget.StringDiagram
/-- The vertical position of a strand in a string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.Strand.vPos : Mathlib.Tactic.Widget.StringDiagram.Strand → ℕ
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.const.match_1.splitter : (motive : (x : ℕ) → TypeVec.{u_1} x → Fin2 x → Sort u_2) →
  (x : ℕ) →
    (x_1 : TypeVec.{u_1} x) →
      (x_2 : Fin2 x) →
        ((n : ℕ) → (α : TypeVec.{u_1} n.succ) → (a : Fin2 n) → motive n.succ α a.fs) →
          ((n : ℕ) → (x : TypeVec.{u_1} n.succ) → motive n.succ x Fin2.fz) → motive x x_1 x_2
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.transportStruct_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : D),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor X =
    e.functor.mapIso
        (CategoryTheory.MonoidalCategory.whiskerRightIso
            (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).symm (e.inverse.obj X) ≪≫
          CategoryTheory.MonoidalCategoryStruct.leftUnitor (e.inverse.obj X)) ≪≫
      e.counitIso.app X
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_id_comp_right_apply : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {l : a ⟶ b} {r : b ⟶ a}
  (adj : CategoryTheory.Bicategory.Adjunction l r) {l' : a ⟶ b} {r' : b ⟶ a}
  (adj' : CategoryTheory.Bicategory.Adjunction l' r') (φ : l' ⟶ l),
  (CategoryTheory.Bicategory.conjugateEquiv adj ((CategoryTheory.Bicategory.Adjunction.id a).comp adj'))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor l').hom φ) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.conjugateEquiv adj adj') φ)
      (CategoryTheory.Bicategory.rightUnitor r').inv
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalNonAssocSemiring : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → (S : NonUnitalSubalgebra R A) → NonUnitalNonAssocSemiring ↥S
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushoutComparison_map_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] [inst_3 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  {W : C} {h : Y ⟶ W} {k : Z ⟶ W} (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
  {Z_1 : D} (h_1 : G.obj W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g)
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.desc h k w)) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.desc (G.map h) (G.map k) ⋯) h_1
-- Mathlib.Logic.Equiv.Option
Equiv.optionCongr_symm : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), e.symm.optionCongr = e.optionCongr.symm
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.coe_val_equivUnits_apply : ∀ {G : Type u_1} [inst : Add G] {a : G} (a_1 : AddConstEquiv G G a a) (a_2 : G),
  ↑(AddConstEquiv.equivUnits a_1) a_2 = a_1 a_2
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.ByteSlice.size.eq_1 : ∀ (s : ByteSlice), s.size = s.stop - s.start
-- Mathlib.Data.W.Basic
WType.equivSigma_apply : ∀ {α : Type u_1} (β : α → Type u_2) (a : WType β), (WType.equivSigma β) a = a.toSigma
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toListRev.go.aux₁ : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {it : Std.IterM m β} {b : β} {bs : List β},
  Std.IterM.toListRev.go it (bs ++ [b]) = (fun x => x ++ [b]) <$> Std.IterM.toListRev.go it bs
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tsnd_comp_tsnd : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] {F G : Type u → Type u} [inst_1 : Applicative F]
  [inst_2 : Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α β₀ β₁ β₂ : Type u}
  (g : β₀ → F β₁) (g' : β₁ → G β₂),
  Functor.Comp.mk ∘ Functor.map (Bitraversable.tsnd g') ∘ Bitraversable.tsnd g =
    Bitraversable.tsnd (Functor.Comp.mk ∘ Functor.map g' ∘ g)
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- **Alias** of the reverse direction of `dvd_neg`.

---

An element `a` of a semigroup with a distributive negation divides the negation of an element
`b` iff `a` divides `b`.  -/
Dvd.dvd.neg_right : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, a ∣ b → a ∣ -b
-- Mathlib.Data.Finsupp.Option
Finsupp.some_optionElim : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (y : M) (f : α →₀ M), (Finsupp.optionElim y f).some = f
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length_eq_three : ∀ {α : Type u_1} {v : FreeMonoid α}, v.length = 3 ↔ ∃ a b c, v = FreeMonoid.of a * FreeMonoid.of b * FreeMonoid.of c
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_le_enumOrd : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → ∀ {a b : Ordinal.{u}}, Ordinal.enumOrd s a ≤ Ordinal.enumOrd s b ↔ a ≤ b
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_eq_ker : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {H : Subgroup N},
  Subgroup.comap f H = f.ker ↔ Disjoint H f.range
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.fderivCLM_apply_of_le : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  k + 1 ≤ n → ⇑((ContDiffMapSupportedIn.fderivCLM 𝕜 n k) f) = fderiv ℝ ⇑f
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.maxEntry! : {α : Type u} → {β : Type v} → [Inhabited (α × β)] → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_eq_headD_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {fallback : α},
  t.minKeyD fallback = t.keys.headD fallback
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- Möbius inversion for functions to a `CommGroup`, where the equalities only hold on a
well-behaved set.  -/
ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on : ∀ {R : Type u_1} [inst : CommGroup R] {f g : ℕ → R} (s : Set ℕ),
  (∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) →
    ((∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔
      ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The `s -ᵥ s` lies within the `vectorSpan k s`.  -/
vsub_set_subset_vectorSpan : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), s -ᵥ s ⊆ ↑(vectorSpan k s)