mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.MulAntidiagonal
Set.antidiagonal_mono_left : ∀ {α : Type u_1} [inst : Add α] {s₁ s₂ t : Set α} {a : α}, s₁ ⊆ s₂ → s₁.antidiagonal t a ⊆ s₂.antidiagonal t a
-- Mathlib.Tactic.Linter.Whitespace
Mathlib.Linter.instInhabitedFormatError.default : Mathlib.Linter.FormatError✝
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.isConj_of_support_equiv : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {σ τ : Equiv.Perm α}
  (f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }),
  (∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)) → IsConj σ τ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.filter_equiv_congr : ∀ {α : Type u} {β : α → Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  (↑m₁).Equiv ↑m₂ →
    ∀ {f : (a : α) → β a → Bool},
      (↑(Std.DHashMap.Internal.Raw₀.filter f m₁)).Equiv ↑(Std.DHashMap.Internal.Raw₀.filter f m₂)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.evalBoolStx : Lean.Term → Lean.Elab.TermElabM (Bool × Lean.Expr)
-- Lean.DocString.DeferredCheck
/-- Modules that should be imported for the check to be meaningful (the reference's `scope`).  -/
Lean.Doc.DeferredCheck.imports : Lean.Doc.DeferredCheck → Array Lean.Name
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_eq_iff_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {x₁ x₂ : M} {y₁ y₂ : ↥S}, f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (↑y₂ + x₁) = f (↑y₁ + x₂)
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.instIsScalarTowerSubtypeMemSubringToSubringOfPrime : ∀ {K : Type u_3} [inst : Field K] (A : Subring K) (P : Ideal ↥A) [inst_1 : P.IsPrime],
  IsScalarTower (↥A) (↥(LocalSubring.ofPrime A P).toSubring) K
-- Aesop.Search.SearchM
Aesop.SearchM.instInhabited : {Q : Type} → [inst : Aesop.Queue Q] → {α : Type} → Inhabited (Aesop.SearchM Q α)
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.yoneda_isColimit_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C)
  (s : CategoryTheory.Limits.Cocone ((CategoryTheory.Functor.fromPUnit X).comp CategoryTheory.yoneda)),
  (CategoryTheory.Limits.IndObjectPresentation.yoneda X).isColimit.desc s = s.ι.app { as := PUnit.unit }
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.BodyState.chunkedBody.injEq : ∀ (ext : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)) (remaining : ℕ)
  (ext_1 : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)) (remaining_1 : ℕ),
  (Std.Http.Protocol.H1.Reader.BodyState.chunkedBody ext remaining =
      Std.Http.Protocol.H1.Reader.BodyState.chunkedBody ext_1 remaining_1) =
    (ext = ext_1 ∧ remaining = remaining_1)
-- Mathlib.LinearAlgebra.Matrix.Integer
/-- The denominator of a matrix of rationals (as a `Nat`, defined as the LCM of the denominators of
the entries).  -/
Matrix.den : {m : Type u_1} → {n : Type u_2} → [Fintype m] → [Fintype n] → Matrix m n ℚ → ℕ
-- Mathlib.RingTheory.OreLocalization.Basic
/-- Scalar multiplication by natural numbers on the Ore localization.  -/
OreLocalization.nsmul : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddMonoid X] → [inst_3 : DistribMulAction R X] → ℕ → OreLocalization S X → OreLocalization S X
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.ext : ∀ {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₂] {f f' : MultilinearMap R M₁ M₂}, (∀ (x : (i : ι) → M₁ i), f x = f' x) → f = f'
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.toContinuousMapAddMonoidHom_apply : ∀ (α : Type u) (R : Type u_2) [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddMonoid R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R] (self : BoundedContinuousFunction α R),
  (BoundedContinuousFunction.toContinuousMapAddMonoidHom α R) self = self.toContinuousMap
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instVAddOfVAddAssocClass : {R : Type u_1} →
  {M : Type u_3} →
    {X : Type u_4} →
      [inst : AddMonoid M] →
        {S : AddSubmonoid M} →
          [inst_1 : AddOreLocalization.AddOreSet S] →
            [inst_2 : AddAction M X] →
              [inst_3 : VAdd R X] →
                [inst_4 : VAdd R M] → [VAddAssocClass R M X] → [VAddAssocClass R M M] → VAdd R (AddOreLocalization S X)
-- Lean.Util.SCC
Lean.SCC.M : (α : Type) → [BEq α] → [Hashable α] → Type → Type
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The distance is induced by the norm.  -/
NormedRing.dist_eq : ∀ {α : Type u_5} [self : NormedRing α] (x y : α), dist x y = ‖-x + y‖
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.prod_rightl : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
  [inst_2 : SeminormedAddCommGroup G'] {c : ℝ} {f : α → E} {g' : α → F'} (k' : α → G') {l : Filter α},
  Asymptotics.IsBigOWith c l f g' → 0 ≤ c → Asymptotics.IsBigOWith c l f fun x => (g' x, k' x)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_C : ∀ {R : Type u_1} {a b : R} (r : R) [inst : Zero R], (QuadraticAlgebra.C r).im = 0
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_functorPushforward_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} {S : CategoryTheory.Sieve X} [F.Full] [F.Faithful],
  CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.functorPushforward F S) = S
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_iUnion₂ : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : VAdd α β] (s : Set α)
  (t : (i : ι) → κ i → Set β), s +ᵥ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s +ᵥ t i j
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_filter_lt_of_le_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}
  [inst_2 : DecidablePred fun x => x < c], c ≤ a → Multiset.filter (fun x => x < c) (Multiset.Ico a b) = ∅
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- If `g` is surjective, then `rTensor Q g` is surjective  -/
LinearMap.rTensor_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} (Q : Type u_5) [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] {g : N →ₗ[R] P}, Function.Surjective ⇑g → Function.Surjective ⇑(LinearMap.rTensor Q g)
-- Batteries.Data.List.Lemmas
List.dropInfix?_nil : ∀ {α : Type u_1} [inst : BEq α] {s : List α}, s.dropInfix? [] = some ([], s)
-- Mathlib.Combinatorics.Quiver.Path.Weight
/-- The weight of a path, where the weight of an edge is defined by a function on its endpoints.  -/
Quiver.Path.weightOfEPs : {V : Type u_1} → [inst : Quiver V] → {R : Type u_2} → [Monoid R] → (V → V → R) → {i j : V} → Quiver.Path i j → R
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Composition of tensor products is tensor product of compositions:
`(f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂)`
 -/
CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C}
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
      (CategoryTheory.CategoryStruct.comp f₂ g₂)
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.of_inheritedFromSource : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  (Q : CategoryTheory.MorphismProperty C) [P.InheritedFromSource Q] [Q.RespectsIso] [Q.ContainsIdentities],
  P.IsClosedUnderIsomorphisms
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.snd_darts_getElem : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {i : ℕ} (hi : i < p.darts.length),
  p.darts[i].toProd.2 = p.support.tail[i]
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.mk.inj : ∀ {V : Type u_1} {G : SimpleGraph V} {toProd : V × V} {adj : G.Adj toProd.1 toProd.2} {toProd_1 : V × V}
  {adj_1 : G.Adj toProd_1.1 toProd_1.2},
  { toProd := toProd, adj := adj } = { toProd := toProd_1, adj := adj_1 } → toProd = toProd_1
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domLCongr_apply : ∀ (R : Type u_1) [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (ι : Type u_7) {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (S : Type u_12) [inst_7 : Semiring S] [inst_8 : Module S N] [inst_9 : SMulCommClass R S N]
  (e : M ≃ₗ[R] M₂) (f : M [⋀^ι]→ₗ[R] N), (AlternatingMap.domLCongr R N ι S e) f = f.compLinearMap ↑e.symm
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.ofι.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} (ι ι_1 : P ⟶ X) (e_ι : ι = ι_1)
  (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g),
  CategoryTheory.Limits.Fork.ofι ι w = CategoryTheory.Limits.Fork.ofι ι_1 ⋯
-- Init.Data.UInt.Basic
instNegUSize : Neg USize
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.eq_neg_add_iff_add_eq : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b c : α}, IsAddUnit b → (a = -b + c ↔ b + a = c)
-- Batteries.Logic
eqRec_eq_cast : ∀ {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a ⋯) {a' : α} (e : a = a'),
  e ▸ x = cast ⋯ x
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Given a model with corners `(E, H)`, we define the pregroupoid of `C^n` transformations of `H`
as the maps that are `C^n` when read in `E` through `I`.  -/
contDiffPregroupoid : WithTop ℕ∞ →
  {𝕜 : 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] → ModelWithCorners 𝕜 E H → Pregroupoid H
-- Mathlib.Tactic.Convert
/-- Configuration elaborator for the `convert`/`convert!` family of tactics.

If `expensive` is true, we're elaborating for `convert!`, and will configure to run at default
transparency (unless explicitly overridden by the user saying e.g. `(transparency := .instances)`.)
 -/
Convert.elabConfig : Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM Congr!.Config
-- Mathlib.SetTheory.Ordinal.Notation
ONote.instPreorder : Preorder ONote
-- Mathlib.Analysis.ODE.PicardLindelof
/-- A key step in the base case of `exists_forall_closedBall_funSpace_dist_le_mul`  -/
ODE.FunSpace.dist_next_next : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x y : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r) (hy : y ∈ Metric.closedBall x₀ ↑r) (α : ODE.FunSpace t₀ x₀ r L),
  dist (ODE.FunSpace.next hf hx α) (ODE.FunSpace.next hf hy α) = dist x y
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.smul_mem_pointwise_smul_iff₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ (S : Subsemiring R) (x : R), a • x ∈ a • S ↔ x ∈ S
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.const_smul_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedRing R] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : Module R E'] [IsBoundedSMul R E'],
  f' =O[l] g → ∀ (c : R), (c • f') =O[l] g
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.mapsTo_span : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  {f : M →ₛₗ[σ₁₂] M₂} {s : Set M} {t : Set M₂},
  Set.MapsTo (⇑f) s t → Set.MapsTo ⇑f ↑(Submodule.span R s) ↑(Submodule.span R₂ t)
-- Mathlib.Data.Multiset.Dedup
Multiset.nodup_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s.dedup.Nodup
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] {x : Lex (HahnSeries Γ R)} (h : x ≠ 0),
  ↑(ofLex ((HahnSeries.finiteArchimedeanClassOrderIsoLex Γ R) (FiniteArchimedeanClass.mk x h))).2 =
    ArchimedeanClass.mk (ofLex x).leadingCoeff
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
/-- The map `Zⁿ(G, X) ⟶ Zⁿ(H, Y)` on cocycles induced by a continuous group homomorphism
`φ : H →ₜ* G` and a morphism of topological `H`-representations `f : res φ X ⟶ Y`.  -/
ContinuousCohomology.cocyclesMap : {k : Type u} →
  {G H : Type v} →
    [inst : Ring k] →
      [inst_1 : TopologicalSpace k] →
        [inst_2 : Group G] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] →
              [inst_5 : Group H] →
                [inst_6 : TopologicalSpace H] →
                  [inst_7 : IsTopologicalGroup H] →
                    {X : TopRep k G} →
                      {Y : TopRep k H} →
                        (φ : H →ₜ* G) →
                          (TopRep.res (↑φ) X ⟶ Y) →
                            (n : ℕ) → ContinuousCohomology.cocycles X n ⟶ ContinuousCohomology.cocycles Y n
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.finsetProd'`. -/
MeasureTheory.ProgMeasurable.finset_prod' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : CommMonoid β]
  [ContinuousMul β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) → MeasureTheory.IsStronglyProgressive f (∏ c ∈ s, U c)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
/-- The singular part between a complex measure `c` and a positive measure `μ` is the complex
measure satisfying `c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c`. This property is given
by `MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq`.  -/
MeasureTheory.ComplexMeasure.singularPart : {α : Type u_1} →
  {m : MeasurableSpace α} → MeasureTheory.ComplexMeasure α → MeasureTheory.Measure α → MeasureTheory.ComplexMeasure α
-- Mathlib.CategoryTheory.Limits.Types.End
/-- The wedge corresponding to the explicit end in `Type` is limiting.  -/
CategoryTheory.Limits.Types.wedgeIsLimit : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))) →
      CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Types.wedge F)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.subset_generated : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)) (c d : C),
  X c d ⊆ (CategoryTheory.Subgroupoid.generated X).arrows c d
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The definition of `Collinear`.  -/
collinear_iff_rank_le_one : ∀ (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] (s : Set P), Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
-- Mathlib.Order.BoundedOrder.Basic
ULift.up_bot : ∀ {α : Type u} [inst : Bot α], { down := ⊥ } = ⊥
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_finset_inter₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {s t : Finset β} {a : α}, a ≠ 0 → a • (s ∩ t) = a • s ∩ a • t
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.p_pos : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {X : T → Ω → E} {P : MeasureTheory.Measure Ω} {p q : ℝ} {M : NNReal},
  ProbabilityTheory.IsKolmogorovProcess X P p q M → 0 < p
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.unit_inv : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α} (h : IsUnit a), ⋯.unit = h.unit⁻¹
-- Mathlib.Analysis.Calculus.FDeriv.Comp
/-- Eta-expanded form of `fderivWithin_comp` -/
fderivWithin_fun_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G} {t : Set F},
  DifferentiableWithinAt 𝕜 g t (f x) →
    DifferentiableWithinAt 𝕜 f s x →
      Set.MapsTo f s t →
        UniqueDiffWithinAt 𝕜 s x →
          fderivWithin 𝕜 (fun x => g (f x)) s x = fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkSeq : Lean.Syntax → Lean.Elab.Term.Do.CodeBlock → Lean.Elab.Term.Do.CodeBlock
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- If for all `j` and `k : ℕ`, `a j ≠ -k`, then the coefficients of the hypergeometric series
are eventually non-vanishing.  -/
Complex.eventually_atTop_regularizedHGFunCoeff_ne_zero : ∀ {a : Multiset ℂ} (b : Multiset ℂ),
  (∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k) → ∀ᶠ (n : ℕ) in Filter.atTop, Complex.regularizedHGFunCoeff a b n ≠ 0
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.ξ_ne_0 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {β : Type u_3} (x : β × (K →+* ℂ) → ℤ),
  x ≠ 0 → NumberField.house.ξ✝ K x ≠ 0
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- The map from the restriction of a presheafed space.
 -/
AlgebraicGeometry.SheafedSpace.ofRestrict : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {U : TopCat} →
      (X : AlgebraicGeometry.SheafedSpace C) →
        {f : U ⟶ ↑X.toPresheafedSpace} →
          (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) → X.restrict h ⟶ X
-- Init.Data.Array.Lemmas
Array.foldr_push : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {init : β} {xs : Array α} {a : α},
  Array.foldr f init (xs.push a) = Array.foldr f (f a init) xs
-- Aesop.Rule.Name
Aesop.PhaseName.noConfusionType : Sort v✝ → Aesop.PhaseName → Aesop.PhaseName → Sort v✝
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- Constructor for morphisms in `CofibrantObject C`.  -/
HomotopicalAlgebra.CofibrantObject.homMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        {X Y : C} →
          [inst_3 : HomotopicalAlgebra.IsCofibrant X] →
            [inst_4 : HomotopicalAlgebra.IsCofibrant Y] →
              (X ⟶ Y) → (HomotopicalAlgebra.CofibrantObject.mk X ⟶ HomotopicalAlgebra.CofibrantObject.mk Y)
-- Mathlib.Data.Fintype.Sets
Set.toFinset_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Set α} [inst_1 : Fintype ↑(insert a s)] [inst_2 : Fintype ↑s],
  (insert a s).toFinset = insert a s.toFinset
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ici_bot : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : OrderBot α] [inst_3 : Fintype α],
  Finset.Ici ⊥ = Finset.univ
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.submatrix_empty : ∀ {α : Type u} {m' : Type uₘ} {n' : Type uₙ} {o' : Type uₒ} (A : Matrix m' n' α) (row : Fin 0 → m') (col : o' → n'),
  A.submatrix row col = Matrix.of ![]
-- Mathlib.Data.Set.BoolIndicator
Set.preimage_boolIndicator_false : ∀ {α : Type u_1} (s : Set α), s.boolIndicator ⁻¹' {false} = sᶜ
-- Mathlib.GroupTheory.FiniteAbelian.Basic
/-- **Alias** of `AddCommGroup.finite_of_fg_isAddTorsion`. -/
AddCommGroup.finite_of_fg_torsion : ∀ (G : Type u) [inst : AddCommGroup G] [hG' : AddGroup.FG G], IsAddTorsion G → Finite G
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_le_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup G),
  Subgroup.map f H ≤ f.range
-- Mathlib.CategoryTheory.Action.Monoidal
Action.diagonalOneIsoLeftRegular.eq_1 : ∀ (G : Type u_1) [inst : Monoid G],
  Action.diagonalOneIsoLeftRegular G = Action.mkIso (Equiv.funUnique (Fin 1) G).toIso ⋯
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiableOn_zeroSection : ∀ (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {t : Set B},
  MDiff[t] (Bundle.zeroSection F E)
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.instSubsingleton : ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [h : IsCyclotomicExtension ∅ A B], Subsingleton (Subalgebra A B)
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.map.match_1.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_3 x
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.toHom_one : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N), ↑1 = 1
-- Mathlib.Data.Matrix.Basic
Matrix.scalar_commute_iff : ∀ {n : Type u_3} {α : Type u_11} [inst : Semiring α] [inst_1 : DecidableEq n] [inst_2 : Fintype n] {r : α}
  {M : Matrix n n α}, Commute ((Matrix.scalar n) r) M ↔ r • M = MulOpposite.op r • M
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.HasKernels.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  autoParam (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasKernel f)
      CategoryTheory.Limits.HasKernels.has_limit._autoParam →
    CategoryTheory.Limits.HasKernels C