mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.TypeVec
/-- introduce a product where both components are the same  -/
TypeVec.prod.diag : {n : ℕ} → {α : TypeVec.{u} n} → α.Arrow (α.prod α)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instNonempty : ∀ {M : Type u_1} [Nonempty M], Nonempty (ArchimedeanOrder M)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.hom_inl_inr_false : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} {Y : D} (f : Sum.inl X ⟶ Sum.inr Y), False
-- Lean.Elab.Command
Lean.Elab.Command.addLinter : Lean.Linter → IO Unit
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.codRestrict.congr_simp : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (p : L.Substructure N) (f f_1 : L.Embedding M N) (e_f : f = f_1) (h : ∀ (c : M), f c ∈ p),
  FirstOrder.Language.Embedding.codRestrict p f h = FirstOrder.Language.Embedding.codRestrict p f_1 ⋯
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context : Type
-- Batteries.Data.List.Lemmas
List.count_getElem_take_lt_count : ∀ {α : Type u_1} [inst : BEq α] [EquivBEq α] {xs : List α} {i : ℕ} {hi : i < xs.length},
  List.count xs[i] (List.take i xs) < List.count xs[i] xs
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
Group.is_simple_iff_prime_card : ∀ {α : Type u_1} [inst : Group α] [IsMulCommutative α], IsSimpleGroup α ↔ Nat.Prime (Nat.card α)
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.forget_map : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F G : C ⥤+ D) (α : F ⟶ G),
  (CategoryTheory.AdditiveFunctor.forget C D).map α = α.hom
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffVAdd.contMDiff_vadd : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  {inst_4 : TopologicalSpace H'} {E' : Type u_5} {inst_5 : NormedAddCommGroup E'} {inst_6 : NormedSpace 𝕜 E'}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_6} {inst_7 : TopologicalSpace G}
  {inst_8 : ChartedSpace H G} {M : Type u_7} {inst_9 : TopologicalSpace M} {inst_10 : ChartedSpace H' M}
  {inst_11 : VAdd G M} [self : ContMDiffVAdd I I' n G M], ContMDiff (I.prod I') I' n fun p => p.1 +ᵥ p.2
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.SMulMemClass.toMulAction.eq_1 : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : SMulMemClass A R M] (S' : A),
  SubMulAction.SMulMemClass.toMulAction S' = Function.Injective.mulAction Subtype.val ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.Hom.mk.congr_simp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (fst fst_1 : x.fst ⟶ y.fst) (e_fst : fst = fst_1)
  (snd snd_1 : x.snd ⟶ y.snd) (e_snd : snd = snd_1)
  (w :
    CategoryTheory.CategoryStruct.comp (F.map fst) y.iso.hom =
      CategoryTheory.CategoryStruct.comp x.iso.hom (G.map snd)),
  { fst := fst, snd := snd, w := w } = { fst := fst_1, snd := snd_1, w := ⋯ }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.CofilteredSystem
/-- The sections of the functor `F : J ⥤ Type v` are in bijection with the sections of
`F.toEventualRanges`.  -/
CategoryTheory.Functor.toEventualRangesSectionsEquiv : {J : Type u} →
  [inst : CategoryTheory.Category.{v_1, u} J] →
    (F : CategoryTheory.Functor J (Type v)) →
      [inst_1 : CategoryTheory.IsCofilteredOrEmpty J] → ↑F.toEventualRanges.sections ≃ ↑F.sections
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle' : ∀ {n : Type u_1} {R : Type u₂} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j k : n) (r : R),
  (LieAlgebra.SpecialLinear.singleSubSingle i k) r - (LieAlgebra.SpecialLinear.singleSubSingle j k) r =
    (LieAlgebra.SpecialLinear.singleSubSingle i j) r
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.mem_range_toPermHom'_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} {τ : Equiv.Perm ↥g.cycleFactorsFinset},
  τ ∈ Equiv.Perm.OnCycleFactors.range_toPermHom' g ↔
    ∀ (c : ↥g.cycleFactorsFinset), (↑(τ c)).support.card = (↑c).support.card
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Applying `weightedVSub` with given weights.  This is for the case
where a result involving a default base point is OK (for example, when
that base point will cancel out later); a more typical use case for
`weightedVSub` would involve selecting a preferred base point with
`weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero` and then
using `weightedVSubOfPoint_apply`.  -/
Finset.weightedVSub_apply : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
  (s.weightedVSub p) w = ∑ i ∈ s, w i • (p i -ᵥ Classical.choice ⋯)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_zero_iff : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R], LinearIndepOn R 0 s ↔ s = ∅
-- Mathlib.Analysis.Analytic.Linear
_private.Mathlib.Analysis.Analytic.Linear.0.ContinuousLinearMap.fpowerSeriesBilinear.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : (x : ℕ) → motive x),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | x => h_4 x) =
    h_1 ()
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.comap_map : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (f : L →ₐ[K] L') (S : IntermediateField K L),
  IntermediateField.comap f (IntermediateField.map f S) = S
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.tsum_pos : ∀ {α : Type u_1} {g : α → NNReal}, Summable g → ∀ (i : α), 0 < g i → 0 < ∑' (b : α), g b
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
/-- **Alias** of the reverse direction of `MeasureTheory.integrable_pi_iff`. -/
MeasureTheory.Integrable.of_eval : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {ι : Type u_2} [inst : Fintype ι]
  {E : ι → Type u_3} [inst_1 : (i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i},
  (∀ (i : ι), MeasureTheory.Integrable (fun x => f x i) μ) → MeasureTheory.Integrable f μ
-- Mathlib.Algebra.Group.Units.Hom
/-- A map `f` between monoids is *local* if any `a` in the domain is a unit
whenever `f a` is a unit. See `IsLocalRing.local_hom_TFAE` for other equivalent
definitions in the local ring case - from where this concept originates, but it is useful in
other contexts, so we allow this generalisation in mathlib.  -/
IsLocalHom : {R : Type u_2} → {S : Type u_3} → {F : Type u_5} → [Monoid R] → [Monoid S] → [FunLike F R S] → F → Prop
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- A rewrite lemma that has been applied to an expression.  -/
Mathlib.Tactic.LibraryRewrite.Rewrite : Type
-- Std.Data.ExtHashSet.Basic
/-- Internal implementation detail of the hash set.  -/
Std.ExtHashSet.inner : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.ExtHashSet α → Std.ExtHashMap α Unit
-- Mathlib.CategoryTheory.Action.Continuous
DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  (X : DiscreteContAction V G), DiscreteTopology ↑((CategoryTheory.forget₂ (DiscreteContAction V G) TopCat).obj X)
-- Mathlib.Order.KrullDimension
Order.coheight_pos : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, 0 < Order.coheight x ↔ ¬IsMax x
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- the coproduct of the maps `g (π i) : A (π i) ⟶ B (π i)` for all `i : ι`.  -/
HomotopicalAlgebra.AttachCells.m : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} → {f : X₁ ⟶ X₂} → (self : HomotopicalAlgebra.AttachCells g f) → self.cofan₁.pt ⟶ self.cofan₂.pt
-- Lean.Meta.AppBuilder
/-- Returns `a = b`.  -/
Lean.Meta.mkEq : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.sset.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i offset : ℕ) (y : Lean.FVarId) (ty : Lean.Expr)
  (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_11) (fvarId_1 : Lean.FVarId)
  (i_1 offset_1 : ℕ) (y_1 : Lean.FVarId) (ty_1 : Lean.Expr) (k_1 : Lean.Compiler.LCNF.Code pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_11),
  (Lean.Compiler.LCNF.Code.sset fvarId i offset y ty k h =
      Lean.Compiler.LCNF.Code.sset fvarId_1 i_1 offset_1 y_1 ty_1 k_1 h_1) =
    (fvarId = fvarId_1 ∧ i = i_1 ∧ offset = offset_1 ∧ y = y_1 ∧ ty = ty_1 ∧ k = k_1)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- If a type carries an involutive star, then any star-closed subset does too.  -/
StarMemClass.instInvolutiveStar : {S : Type u_1} →
  {R : Type u_2} → [inst : InvolutiveStar R] → [inst_1 : SetLike S R] → [StarMemClass S R] → (s : S) → InvolutiveStar ↥s
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_cancel : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (a : M) (b c : ↥S), f.mk' (a * ↑c) (b * c) = f.mk' a b
-- Init.Data.UInt.Lemmas
UInt64.toUSize_mod_of_toNat_lt : ∀ (a b : UInt64), a.toNat < USize.size → b.toNat < USize.size → (a % b).toUSize = a.toUSize % b.toUSize
-- Std.Time.DateTime.PlainDateTime
/-- Represents a date and time with components for Year, Month, Day, Hour, Minute, Second, and Nanosecond.
 -/
Std.Time.PlainDateTime : Type
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  CategoryTheory.IsPullback (AlgebraicGeometry.Spec.map T.tensorInl) (AlgebraicGeometry.Spec.map T.tensorInr)
    (AlgebraicGeometry.Spec.map
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv
        (AlgebraicGeometry.Scheme.Hom.residueFieldMap f T.x)))
    (AlgebraicGeometry.Spec.map
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv
        (AlgebraicGeometry.Scheme.Hom.residueFieldMap g T.y)))
-- Init.Coe
CoeT.mk : {α : Sort u} → {x : α} → {β : Sort v} → β → CoeT α x β
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.id_pushforward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id I)],
  CategoryTheory.ExponentiableMorphism.pushforward (CategoryTheory.CategoryStruct.id I) =
    CategoryTheory.Functor.id (CategoryTheory.Over I)
-- Mathlib.Order.SuccPred.Basic
Order.le_succ_iff_eq_or_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α}, a ≤ Order.succ b ↔ a = Order.succ b ∨ a ≤ b
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.isG2_iff : ∀ {ι : 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)
  [inst_5 : P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible], P.IsG2 ↔ ∃ i j, P.pairingIn ℤ i j = -3
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
AlternatingMap.mkContinuous.congr_simp : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f f_1 : E [⋀^ι]→ₗ[𝕜] F) (e_f : f = f_1) (C C_1 : ℝ) (e_C : C = C_1)
  (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖), f.mkContinuous C H = f_1.mkContinuous C_1 ⋯
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.maybeSetExplicit : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
/-- Given a continuous function which is linear in the first argument
and is alternating in the other `n` arguments,
build a continuous alternating form in `n + 1` arguments.

The function is given by
```
alternatizeUncurryFin f v = ∑ i : Fin (n + 1), (-1) ^ (i : ℕ) • f (v i) (removeNth i v)
```

Note that the round-trip with `curryLeft` multiplies the form by `n + 1`,
since we want to avoid division in this definition.  -/
ContinuousAlternatingMap.alternatizeUncurryFin : {𝕜 : 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] → {n : ℕ} → (E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] F
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
ZMod.χ₈'_apply : ∀ (a : ZMod 8),
  ZMod.χ₈' a =
    match a with
    | 0 => 0
    | 2 => 0
    | 4 => 0
    | 6 => 0
    | 1 => 1
    | 3 => 1
    | 5 => -1
    | 7 => -1
-- Mathlib.Control.Fold
Traversable.foldl.unop_ofFreeMonoid : ∀ {α β : Type u} (f : β → α → β) (xs : FreeMonoid α) (a : β),
  (CategoryTheory.ConcreteCategory.hom (MulOpposite.unop ((Monoid.Foldl.ofFreeMonoid f) xs))) a =
    List.foldl f a (FreeMonoid.toList xs)
-- Init.Data.Vector.Lemmas
Vector.set_comm : ∀ {α : Type u_1} {n i j : ℕ} (a b : α) {xs : Vector α n} {hi : i < n} {hj : j < n},
  i ≠ j → (xs.set i a hi).set j b hj = (xs.set j b hj).set i a hi
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_shiftFunctorCompIsoId_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (n m : A) (h : n + m = 0) (X : C),
  (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n m h).hom.app X) =
    (CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app ((CategoryTheory.shiftFunctor C n).obj X)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.logMap.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K)
  (w : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
  NumberField.mixedEmbedding.logMap x w =
    ↑(↑w).mult *
      (Real.log ((NumberField.mixedEmbedding.normAtPlace ↑w) x) -
        Real.log (NumberField.mixedEmbedding.norm x) * (↑(Module.finrank ℚ K))⁻¹)
-- Mathlib.Data.List.Cycle
Cycle.chain_ne_nil : ∀ {α : Type u_1} (r : α → α → Prop) {l : List α} (hl : l ≠ []), Cycle.Chain r ↑l ↔ List.IsChain r (l.getLast hl :: l)
-- Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization
instUniqueFactorizationMonoidLocalization : ∀ {M : Type u_1} [inst : CommSemiring M] (S : Submonoid M) [UniqueFactorizationMonoid M],
  UniqueFactorizationMonoid (Localization S)
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_right_injective : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M}, IsAddUnit a → Function.Injective fun x => a + x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.compare_maxKey!_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, cmp (Std.DTreeMap.Raw.Const.modify t k f).maxKey! t.maxKey! = Ordering.eq
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, panicking if no such pair exists.
 -/
Std.TreeMap.getEntryGE! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap α β cmp → α → α × β
-- Qq.Macro
Qq.Impl.ExprBackSubstResult.quoted : Lean.Expr → Qq.Impl.ExprBackSubstResult
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_iInf_map_of_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_3}
  {f : L.Hom M N},
  Function.Injective ⇑f →
    ∀ (S : ι → L.Substructure M),
      FirstOrder.Language.Substructure.comap f (⨅ i, FirstOrder.Language.Substructure.map f (S i)) = ⨅ i, S i
-- Lean.Compiler.IR.CompilerM
Lean.IR.tracePrefixOptionName : Lean.Name
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioc_sub_one_right_eq_Ioo : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] (a b : α), Finset.Ioc a (b - 1) = Finset.Ioo a b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  (t₁ \ t₂).getD k fallback = if k ∈ t₂ then fallback else t₁.getD k fallback
-- Init.Data.Int.Order
Int.natAbs_eq_natAbs_iff : ∀ {a b : ℤ}, a.natAbs = b.natAbs ↔ a = b ∨ a = -b
-- Mathlib.Order.Hom.Set
OrderIso.subsingleton_of_wellFoundedLT : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : Preorder β], Subsingleton (α ≃o β)
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- An open ball centred at the origin in a valued ring is closed.  -/
Valued.isClosed_ball : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  (r : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀), IsClosed {x | Valued.v.restrict x < r}
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {V : (x : M') → TangentSpace I' x}, VectorField.mpullbackWithin I I' f V s x = (mfderiv[s] f x).inverse (V (f x))
-- Init.Data.SInt.Lemmas
Int32.toInt8_toInt64 : ∀ (n : Int32), n.toInt64.toInt8 = n.toInt8
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.instNegOreLocalization : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [inst_2 : AddGroup X] → [inst_3 : DistribMulAction R X] → Neg (OreLocalization S X)
-- Mathlib.ModelTheory.Definability
/-- A `TermDefinable` function postcomposed with `TermDefinable₁` is `TermDefinable`.  -/
Set.TermDefinable₁.comp_termDefinable : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {f : M → M} {g : (α → M) → M},
  Set.TermDefinable₁ L f → A.TermDefinable L g → A.TermDefinable L (f ∘ g)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
/-- A version of `ExteriorAlgebra.ι` that maps directly into the graded structure. This is
primarily an auxiliary construction used to provide `ExteriorAlgebra.gradedAlgebra`.  -/
ExteriorAlgebra.GradedAlgebra.ι : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → M →ₗ[R] DirectSum ℕ fun i => ↥(⋀[R]^i M)
-- Init.Data.Iterators.Combinators.Monadic.Take
_private.Init.Data.Iterators.Combinators.Monadic.Take.0.Std.Iterators.Types.Take.instFinitenessRelation : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Monad m] →
        [inst_1 : Std.Iterator α m β] →
          [Std.Iterators.Productive α m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.Take α m) m
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.coe_update : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (f : Π₀ (i : ι), β i) (i : ι)
  (b : β i), ⇑(f.update i b) = Function.update (⇑f) i b
-- Init.Data.Int.Lemmas
Int.neg_add_cancel_right : ∀ (a b : ℤ), a + -b + b = a
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.finTwoArrow_symm_apply : ∀ (α : Type u_4) [inst : UniformSpace α], ⇑(UniformEquiv.finTwoArrow α).symm = fun x => ![x.1, x.2]
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.ratAdd_sound : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (f : σ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ)) (f' : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
    p ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
      Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c p rupHints ratHints = (f', true) →
        Std.Tactic.BVDecide.LRAT.Internal.Equisat α f f'
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.inv_eq_iff_mul_eq_one : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] {φ ψ : MvPowerSeries σ k},
  MvPowerSeries.constantCoeff ψ ≠ 0 → (ψ⁻¹ = φ ↔ φ * ψ = 1)
-- Mathlib.Topology.Separation.Regular
CompletelyNormalSpace.mk : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ ⦃s t : Set X⦄, Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (nhdsSet s) (nhdsSet t)) →
    CompletelyNormalSpace X
-- Lean.Elab.Term
/-- Checks whether a declaration is annotated with `[builtin_incremental]` or `[incremental]`.  -/
Lean.Elab.isIncrementalElab : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [MonadLiftT IO m] → Lean.Name → m Bool
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_0 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.C 0 = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_δ''_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ j.castSucc) {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ j.succ) (CategoryTheory.CategoryStruct.comp (X.δ (i.castLT ⋯)) h) =
    CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.δ j) h)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nontrivial.mul : ∀ {α : Type u_2} [inst : Mul α] [IsLeftCancelMul α] [inst_2 : DecidableEq α] {s t : Finset α},
  s.Nontrivial → t.Nontrivial → (s * t).Nontrivial
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.finite_quotient : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S}, φ.IsArithFrobAt Q → Finite (R ⧸ Ideal.under R Q)
-- Mathlib.Logic.Equiv.Defs
/-- If `α` is equivalent to `β` and `γ` is equivalent to `δ`, then the type of equivalences `α ≃ γ`
is equivalent to the type of equivalences `β ≃ δ`.  -/
Equiv.equivCongr : {α : Sort u} → {β : Sort v} → {γ : Sort w} → {δ : Sort u_1} → α ≃ β → γ ≃ δ → α ≃ γ ≃ (β ≃ δ)