mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Slice.Array.Lemmas
Array.toSubarray_eq_min : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  xs.toSubarray lo hi =
    {
      internalRepresentation :=
        { array := xs, start := min lo (min hi xs.size), stop := min hi xs.size, start_le_stop := ⋯,
          stop_le_array_size := ⋯ } }
-- Mathlib.Analysis.Convex.EGauge
egauge_anti : ∀ (𝕜 : Type u_1) [inst : NNNorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] {s t : Set E},
  s ⊆ t → ∀ (x : E), egauge 𝕜 t x ≤ egauge 𝕜 s x
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f]
  (U : { U // U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f }),
  (AlgebraicGeometry.IsOpenImmersion.opensEquiv f).symm U = (TopologicalSpace.Opens.map f.base).obj ↑U
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  IsOpen s → x ∈ s → (HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
/-- A faithful additive monoidal functor to a monoidal preadditive category
ensures that the domain is monoidal preadditive.  -/
CategoryTheory.monoidalPreadditive_of_faithful : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {D : Type u_2}
  [inst_4 : CategoryTheory.Category.{v_2, u_2} D] [inst_5 : CategoryTheory.Preadditive D]
  [inst_6 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor D C) [F.Monoidal] [F.Faithful] [F.Additive],
  CategoryTheory.MonoidalPreadditive D
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.mk : Lean.AssocList Lean.FVarId Lean.Expr → Lean.Meta.FVarSubst
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Subgraph.IsInduced.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph),
  G'.IsInduced = ∀ ⦃v : V⦄, v ∈ G'.verts → ∀ ⦃w : V⦄, w ∈ G'.verts → G.Adj v w → G'.Adj v w
-- Init.Data.Int.DivMod.Bootstrap
_private.Init.Data.Int.DivMod.Bootstrap.0.Int.ediv.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) →
      ((m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) →
        ((a : ℕ) → motive (Int.negSucc a) 0) →
          ((m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ)) →
            ((m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)) → motive x x_1
-- Mathlib.Algebra.Group.Pi.Units
IsAddUnit.val_neg_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)] {x : (i : ι) → M i} (hx : IsAddUnit x) (i : ι),
  ↑(-hx.addUnit) i = ↑(-⋯.addUnit)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isInvInvariant : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → Group (α i)] [∀ (i : ι), MeasurableInv (α i)] [∀ (i : ι), (μ i).IsInvInvariant],
  (MeasureTheory.Measure.pi μ).IsInvInvariant
-- Mathlib.Data.FunLike.Fintype
/-- All `DFunLike`s are finite if their domain and codomain are.

This is not an instance because specific `DFunLike` types might have a better-suited definition.

See also `DFunLike.finite`.
 -/
DFunLike.fintype : (F : Type u_1) →
  {α : Type u_3} →
    {β : α → Type u_5} → [DFunLike F α β] → [DecidableEq α] → [Fintype α] → [(i : α) → Fintype (β i)] → Fintype F
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- An auxiliary lemma for manipulating sequence indices.  -/
PadicSeq.lift_index_left : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) (v1 v3 : ℕ),
  padicNorm p (↑f (PadicSeq.stationaryPoint hf)) = padicNorm p (↑f (max v1 (max (PadicSeq.stationaryPoint hf) v3)))
-- Mathlib.Topology.Order.Basic
induced_orderTopology : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [ta : TopologicalSpace β] [inst_1 : Preorder β] [OrderTopology β]
  (f : α → β), (∀ {x y : α}, f x < f y ↔ x < y) → (∀ {x y : β}, x < y → ∃ a, f a ∈ Set.Ioo x y) → OrderTopology α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_eq_some_getKeyD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α}, a ∈ m → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_map_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Mon C} (f : X ⟶ Y) (x : CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.inverse.map f).hom.app x = f.hom
-- Mathlib.Topology.UniformSpace.Cauchy
completeSpace_prod_of_nonempty : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] [Nonempty α] [Nonempty β],
  CompleteSpace (α × β) ↔ CompleteSpace α ∧ CompleteSpace β
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.isOpen_left_of_isOpen_union : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → IsOpen (s ∪ t) → IsOpen s
-- Mathlib.Data.Finset.Interval
/-- Cardinality of an `Ico` of finsets.  -/
Finset.card_Ico_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊆ t → (Finset.Ico s t).card = 2 ^ (t.card - s.card) - 1
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection],
  Uᗮ.starProjection = ContinuousLinearMap.id 𝕜 E - U.starProjection
-- Mathlib.Data.EReal.Inv
EReal.mul_div_mul_cancel : ∀ {a b c : EReal}, c ≠ ⊥ → c ≠ ⊤ → c ≠ 0 → a * c / (b * c) = a / b
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instToStringPurity : ToString Lean.Compiler.LCNF.Purity
-- Mathlib.Data.List.Basic
List.getLast?_append_cons : ∀ {α : Type u} (l₁ : List α) (a : α) (l₂ : List α), (l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The duality isomorphism `S.P ≅ Opposite.unop S.op.P'`.  -/
CategoryTheory.ShortComplex.SnakeInput.PIsoUnopOpP' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex.SnakeInput C) → S.P ≅ Opposite.unop S.op.P'
-- Lean.Util.PPExt
Lean.FormatWithInfos.mk.sizeOf_spec : ∀ (fmt : Std.Format) (infos : Lean.PrettyPrinter.InfoPerPos),
  sizeOf { fmt := fmt, infos := infos } = 1 + sizeOf fmt + sizeOf infos
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_swap_mul_swap_of_nodup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {x y z t : α},
  [x, y, z, t].Nodup → (Equiv.swap x y * Equiv.swap z t).cycleType = {2, 2}
-- Mathlib.SetTheory.Ordinal.Notation
ONote.add_nf : ∀ (o₁ o₂ : ONote) [o₁.NF] [o₂.NF], (o₁ + o₂).NF
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- If `g` generates the additive group `G` and `g'` is an element of another additive group `G'`
whose order divides that of `g`, then there is a homomorphism `G →+ G'` mapping `g` to `g'`.  -/
addMonoidHomOfForallMemZMultiples : {G : Type u_2} →
  {G' : Type u_3} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup G'] →
        {g : G} → (∀ (x : G), x ∈ AddSubgroup.zmultiples g) → {g' : G'} → addOrderOf g' ∣ addOrderOf g → G →+ G'
-- Init.Data.Nat.Basic
Nat.beq.eq_3 : ∀ (n : ℕ), n.succ.beq Nat.zero = false
-- Mathlib.RingTheory.HopfAlgebra.TensorProduct
TensorProduct.antipode_def : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : HopfAlgebra R A]
  [inst_6 : HopfAlgebra S B] [inst_7 : Algebra R B] [inst_8 : IsScalarTower R S B],
  HopfAlgebraStruct.antipode S =
    TensorProduct.AlgebraTensorModule.map (HopfAlgebraStruct.antipode S) (HopfAlgebraStruct.antipode R)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findM?_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id m] [LawfulMonad m] [Std.Iterators.Finite α Id] [Std.LawfulIteratorLoop α Id m]
  {it : Std.Iter β} {f : β → m (ULift.{w, 0} Bool)},
  it.findM? f =
    match ↑it.step with
    | Std.IterStep.yield it' out => do
      let __do_lift ← f out
      if __do_lift.down = true then pure (some out) else it'.findM? f
    | Std.IterStep.skip it' => it'.findM? f
    | Std.IterStep.done => pure none
-- Mathlib.Algebra.Group.Semiconj.Defs
SemiconjBy.eq_1 : ∀ {M : Type u_2} [inst : Mul M] (a x y : M), SemiconjBy a x y = (a * x = y * a)
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} (self : CategoryTheory.PresheafOfGroups.OneCocycle G U) (i j k : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j)
  (c : T ⟶ U k), self.ev i j a b * self.ev j k b c = self.ev i k a c
-- Init.Data.Array.Lemmas
Array.reverse.loop.eq_1 : ∀ {α : Type u} (as : Array α) (i : ℕ) (j : Fin as.size),
  Array.reverse.loop as i j =
    if h : i < ↑j then
      have this := ⋯;
      let as_1 := as.swap i ↑j ⋯ ⋯;
      have this := ⋯;
      Array.reverse.loop as_1 (i + 1) ⟨↑j - 1, this⟩
    else as
-- Mathlib.LinearAlgebra.Matrix.Cartan
/-- The Cartan matrix of type G₂. See [bourbaki1968] plate IX, page 290.
We use the transpose of Bourbaki's matrix for consistency with F₄.  -/
CartanMatrix.G₂ : Matrix (Fin 2) (Fin 2) ℤ
-- Mathlib.AlgebraicGeometry.Sites.Affine
CategoryTheory.Sieve.coverByImage.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (U : D),
  CategoryTheory.Sieve.coverByImage G U = { arrows := CategoryTheory.Presieve.coverByImage G U, downward_closed := ⋯ }
-- Mathlib.Logic.Function.Defs
Function.prod_id_id : ∀ {α : Type u_1}, Function.prod id id = Function.diag
-- Init.Internal.Order.Basic
Lean.Order.iterates.step : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {f : α → α} {x : α}, Lean.Order.iterates f x → Lean.Order.iterates f (f x)
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.Monadic.modifyStep : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {P : β → Prop} →
          (it : Std.IterM m { out // P out }) →
            it.internalState.inner.Step → Std.IterStep (Std.IterM m { out // P out }) { out // P out }
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
ofAdd_list_prod : ∀ {M : Type u_3} [inst : AddMonoid M] (s : List M),
  Multiplicative.ofAdd s.sum = (List.map (⇑Multiplicative.ofAdd) s).prod
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `+` is an additive commutative semigroup, if it admits
a surjective map that preserves `+` from an additive commutative semigroup.  -/
Function.Surjective.addCommMagma : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₂] →
      [inst_1 : AddCommMagma M₁] →
        (f : M₁ → M₂) → Function.Surjective f → (∀ (x y : M₁), f (x + y) = f x + f y) → AddCommMagma M₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionOptions : Lean.FromJson Lean.Lsp.CompletionOptions
-- Mathlib.Algebra.Order.Monovary
antivary_iff_forall_smul_nonpos : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β}, Antivary f g ↔ ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- Auxiliary definition for `equivalence`.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso : (X Y : SSet.Truncated 2) →
  (SSet.Truncated.HomotopyCategory.BinaryProduct.functor X Y).comp
      (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y) ≅
    CategoryTheory.Functor.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeMonoid.equivWithOneFreeSemigroup_apply : ∀ {α : Type u_1} (a : FreeMonoid α),
  FreeMonoid.equivWithOneFreeSemigroup a = (FreeMonoid.lift fun x => ↑(FreeSemigroup.of x)) a
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.ι.eq_1 : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g),
  t.ι = t.π.app CategoryTheory.Limits.WalkingParallelPair.zero
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- If you add multiples of row `B k` to other rows, the determinant doesn't change.  -/
Matrix.det_eq_of_forall_row_eq_smul_add_const : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A B : Matrix n n R}
  (c : n → R) (k : n), c k = 0 → (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- The measure `μ.restrict μ.sigmaFiniteSetᶜ` takes only two values: 0 and ∞ .  -/
MeasureTheory.restrict_compl_sigmaFiniteSet_eq_zero_or_top : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (s : Set α),
  (μ.restrict μ.sigmaFiniteSetᶜ) s = 0 ∨ (μ.restrict μ.sigmaFiniteSetᶜ) s = ⊤
-- Mathlib.RingTheory.SimpleModule.Isotypic
instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (c : ↑(isotypicComponents R M)), IsSemisimpleModule R ↥↑c
-- Init.Prelude
MProd.mk : {α β : Type u} → α → β → MProd α β
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_zero : ∀ {n : ℕ} [inst : NeZero n] {i : Fin (n + 1)}, Fin.predAbove 0 i = if hi : i = 0 then 0 else i.pred hi
-- Mathlib.Data.Holor
Holor.instSMulOfMul : {α : Type} → {ds : List ℕ} → [Mul α] → SMul α (Holor α ds)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_univ : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], ProjectiveSpectrum.zeroLocus 𝒜 Set.univ = ∅
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_closure_range_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {e : β → α} {a : α},
  a ∈ closure (Set.range e) ↔ ∀ ε > 0, ∃ k, dist a (e k) < ε
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {he : t.isEmpty = false} {km : α}, t.min he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.CategoryTheory.Sites.Sieves
/-- an object in the source category  -/
CategoryTheory.Presieve.FunctorPushforwardStructure.preobj : {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.Presieve X} →
              {Y : D} → {f : Y ⟶ F.obj X} → CategoryTheory.Presieve.FunctorPushforwardStructure F S f → C
-- Init.Data.Option.Attach
Option.toArray_attach : ∀ {α : Type u_1} (o : Option α), o.attach.toArray = Array.map (fun x => ⟨↑x, ⋯⟩) o.toArray.attach
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.laxMonoidalPi_μ : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u₂}
  [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)]
  (F : (i : I) → CategoryTheory.Functor (D i) (C i)) [inst_4 : (i : I) → (F i).LaxMonoidal] (X Y : (i : I) → D i)
  (i : I),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Functor.pi F) X Y i =
    CategoryTheory.Functor.LaxMonoidal.μ (F i) (X i) (Y i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  {a : α}, ∅.get? a = none
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} [inst_3 : Inhabited (β k)], m₁.contains k = false → (m₁.diff m₂).get! k = default
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Fintype.card (NumberField.InfinitePlace K) =
    NumberField.InfinitePlace.nrRealPlaces K + NumberField.InfinitePlace.nrComplexPlaces K
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.mk : Lean.Meta.Simp.Simproc →
  Lean.Meta.Simp.Simproc →
    Lean.Meta.Simp.DSimproc →
      Lean.Meta.Simp.DSimproc → (Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) → Bool → Lean.Meta.Simp.Methods
-- Mathlib.Algebra.FreeMonoid.Count
FreeAddMonoid.countP_of : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (x : α),
  (FreeAddMonoid.countP p) (FreeAddMonoid.of x) = if p x then 1 else 0
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.isIntertwiningMap_of_mem_center : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V), ∀ g ∈ Submonoid.center G, ρ.IsIntertwiningMap ρ (ρ g)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase_dup_rhs : Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.funLike : {E : Type u_3} → [inst : AddGroup E] → FunLike (NonarchAddGroupNorm E) E ℝ
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftComp_hom_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (hl' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l'.app X.left) X.hom))
  (hll' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
      P (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp l l').app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftComp R l l' hl hl' hll').hom.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.isIso_snd_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    autoParam (CategoryTheory.IsIso f) CategoryTheory.IsPullback.isIso_snd_of_isIso._auto_1 → CategoryTheory.IsIso snd
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.diseq_split_cert : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.letVarTypes : Lean.Option Bool
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries_one_eq_top_iff : ∀ {G : Type u_1} [inst : Group G], Subgroup.upperCentralSeries G 1 = ⊤ ↔ IsMulCommutative G
-- Init.Data.Array.Lemmas
Array.map_eq_foldl : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α},
  Array.map f xs = Array.foldl (fun bs a => bs.push (f a)) #[] xs
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Iio_subset : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a : { x // p x }), Subtype.val '' Set.Iio a ⊆ Set.Iio ↑a
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.ringModuleOf_bracket : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : IsLieAbelian M] (E : LieAlgebra.Extension R M L) (x : L)
  (y : M), ⁅x, y⁆ = E.toKer.symm ⁅Exists.choose ⋯ x, E.toKer y⁆
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toContinuousLinearEquiv_inj : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  {f g : E ≃ₛₗᵢ[σ₁₂] E₂}, ↑f = ↑g ↔ f = g
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map_map : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] (f : S →+ T) (g : R →+ S) (x : MonoidAlgebra R M),
  MonoidAlgebra.map f (MonoidAlgebra.map g x) = MonoidAlgebra.map (f.comp g) x
-- Aesop.Script.UScriptToSScript
Aesop.Script.orderedUScriptToSScript : Aesop.Script.UScript → Aesop.Script.TacticState → Lean.CoreM Aesop.Script.SScript
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.extensionValuation_coe_apply : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  {x : UniformSpace.Completion K},
  (MonoidWithZeroHom.ofClass Valued.extensionValuation) x = MonoidWithZeroHom.ValueGroup₀.embedding (Valued.extension x)
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_of_one : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} [inst : MulOneClass α] (A : Matrix m n α), A.hadamard (Matrix.of 1) = A
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.instIsProbabilityMeasureGaussianReal : ∀ (μ : ℝ) (v : NNReal), MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.gaussianReal μ v)
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_div_oneLePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] (a : α), a⁻ᵐ / a⁺ᵐ = a⁻¹
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.of_ringEquiv : ∀ (G : Type u_1) (A : Type u_2) (A' : Type u_3) (B : Type u_4) [inst : Group G] [inst_1 : CommSemiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [hG : IsGaloisGroup G A B]
  [inst_5 : CommSemiring A'] [inst_6 : Algebra A' B] (e : A ≃+* A'),
  (∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a) → IsGaloisGroup G A' B