mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq : ∀ (𝕜 : Type u_2) {F : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℂ F]
  [inst_3 : NormedSpace 𝕜 F] (f : SchwartzMap ℝ F),
  (TemperedDistribution.derivCLM F) ((SchwartzMap.toTemperedDistributionCLM ℝ F MeasureTheory.volume) f) =
    (SchwartzMap.toTemperedDistributionCLM ℝ F MeasureTheory.volume) ((SchwartzMap.derivCLM 𝕜 F) f)
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.IsAcc.isSuccLimit : ∀ {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}}, o.IsAcc S → Order.IsSuccLimit o
-- Aesop.Script.CtorNames
Aesop.CtorNames.toInductionAltLHS : Aesop.CtorNames → Lean.TSyntax `Lean.Parser.Tactic.inductionAltLHS
-- Mathlib.Order.RelSeries
RelSeries.mk.injEq : ∀ {α : Type u_1} {r : SetRel α α} (length : ℕ) (toFun : Fin (length + 1) → α)
  (step : ∀ (i : Fin length), (toFun i.castSucc, toFun i.succ) ∈ r) (length_1 : ℕ) (toFun_1 : Fin (length_1 + 1) → α)
  (step_1 : ∀ (i : Fin length_1), (toFun_1 i.castSucc, toFun_1 i.succ) ∈ r),
  ({ length := length, toFun := toFun, step := step } = { length := length_1, toFun := toFun_1, step := step_1 }) =
    (length = length_1 ∧ toFun ≍ toFun_1)
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.instFiniteElemRealSpectrum : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n],
  Finite ↑(spectrum ℝ A)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Multiseries in a basis `basis_hd :: basis_tl`. It is a generalisation of asymptotic expansions.
A multiseries in a basis `[b₁, ..., bₙ]` is a formal series made from monomials
`b₁ ^ e₁ * ... * bₙ ^ eₙ` where `e₁, ..., eₙ` are real numbers. We treat multivariate series in
a basis `[b₁, ..., bₙ]` as a univariate series in the variable `b₁` (`basis_hd`) with coefficients
being multiseries in the basis `[b₂, ..., bₙ]` (`basis_tl`). We represent such a series as a lazy
list (`Seq`) of pairs `(exp, coef)` where `exp` is the exponent of `b₁` and `coef` is the
coefficient (a multiseries in `basis_tl`).

`MultiseriesExpansion` is a `Multiseries` with an attached real function.
 -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries : (ℝ → ℝ) → Tactic.ComputeAsymptotics.Basis → Type
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- A graph is locally finite if every vertex has a finite neighbor set.  -/
SimpleGraph.LocallyFinite : {V : Type u_1} → SimpleGraph V → Type u_1
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.cons_mem_paths : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Z : C}
  {p : Quiver.Path X Y} {f : Y ⟶ Z}, W.paths p → W f → W.paths (p.cons f)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_insertIfNew_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, k ∈ m.insertIfNew k v
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldrM.loop.match_1.eq_2 : ∀ {α : Type u_2} (n : ℕ) (motive : { i // i ≤ n } → α → Sort u_1) (i : ℕ) (h : i + 1 ≤ n) (x : α)
  (h_1 : (property : 0 ≤ n) → (x : α) → motive ⟨0, property⟩ x)
  (h_2 : (i : ℕ) → (h : i + 1 ≤ n) → (x : α) → motive ⟨i.succ, h⟩ x),
  (match ⟨i.succ, h⟩, x with
    | ⟨0, property⟩, x => h_1 property x
    | ⟨i.succ, h⟩, x => h_2 i h x) =
    h_2 i h x
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `continuousWithinAt_sdiff_singleton`.

---

See also `continuousWithinAt_sdiff_self` for the case `y = x` but not requiring `T1Space`.  -/
continuousWithinAt_diff_singleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space X] {x y : X}
  {s : Set X} {f : X → Y}, ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x
-- Mathlib.Order.SupIndep
/-- Composing an independent indexed family with an injective function on the index results in
another independent indexed family.  -/
iSupIndep.comp : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_5} {ι' : Sort u_6} {t : ι → α} {f : ι' → ι},
  iSupIndep t → Function.Injective f → iSupIndep (t ∘ f)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.instMonoidalForget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.Center.forget C).Monoidal
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim_main : ∀ (a b c d : List Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.main = a
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.injective_rangeRestrict_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f
-- Mathlib.Topology.Separation.Basic
/-- In an R₁ space, if a compact set `K` is contained in an open set `U`,
then its closure is also contained in `U`.  -/
IsCompact.closure_subset_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {K : Set X},
  IsCompact K → ∀ {U : Set X}, IsOpen U → K ⊆ U → closure K ⊆ U
-- Mathlib.Logic.Equiv.Defs
Equiv.symmEquiv_symm_apply_apply : ∀ (α : Sort u_1) (β : Sort u_2) (e : β ≃ α) (a : α), ((Equiv.symmEquiv α β).symm e) a = e.invFun a
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.map_expand : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] (p : ℕ) (f : R →+* S)
  (φ : MvPolynomial σ R),
  (MvPolynomial.map f) ((MvPolynomial.expand p) φ) = (MvPolynomial.expand p) ((MvPolynomial.map f) φ)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformly.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] (f : ι → β → α) (g : β → α)
  [inst_1 : UniformSpace α], HasSumUniformly f g = HasSum (⇑UniformFun.ofFun ∘ f) (UniformFun.ofFun g)
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTrans_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.FibrantObject C),
  HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTrans.app X =
    HomotopicalAlgebra.FibrantObject.toHoCat.map
      { hom := HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj (HomotopicalAlgebra.FibrantObject.ι.obj X) }
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_add_measureReal_compl : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure μ],
  MeasurableSet s → μ.real s + μ.real sᶜ = μ.real Set.univ
-- Mathlib.Computability.Reduce
OneOneEquiv.symm : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
  OneOneEquiv p q → OneOneEquiv q p
-- Mathlib.LinearAlgebra.Determinant
/-- The determinants of a `LinearEquiv` and its inverse multiply to 1.  -/
LinearEquiv.det_symm_mul_det : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] (f : M ≃ₗ[A] M),
  LinearMap.det ↑f.symm * LinearMap.det ↑f = 1
-- Mathlib.CategoryTheory.Action.Concrete
/-- The `G`-set `Gⁿ`, acting on itself by left multiplication.  -/
Action.diagonal : (G : Type u) → [inst : Monoid G] → ℕ → Action (Type u) G
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.preimage_smul₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ (t : Set β), (fun x => a • x) ⁻¹' t = a⁻¹ • t
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepSet_iff_indepSets_singleton : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {s t : Set Ω},
  MeasurableSet s →
    MeasurableSet t →
      ∀ (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.indepSet_iff_indepSets_singleton._auto_1)
        [MeasureTheory.IsZeroOrProbabilityMeasure μ],
        ProbabilityTheory.IndepSet s t μ ↔ ProbabilityTheory.IndepSets {s} {t} μ
-- Mathlib.Data.Set.Semiring
SetSemiring.instIdemSemiringOfMonoid : {α : Type u_1} → [Monoid α] → IdemSemiring (SetSemiring α)
-- Mathlib.Algebra.Order.Floor.Div
/-- Do not use this. Use `gc_floorDiv_smul` or `gc_floorDiv_mul` instead.  -/
FloorDiv.floorDiv_gc : ∀ {α : Type u_2} {β : Type u_3} {inst : AddCommMonoid α} {inst_1 : PartialOrder α} {inst_2 : AddCommMonoid β}
  {inst_3 : PartialOrder β} {inst_4 : SMulZeroClass α β} [self : FloorDiv α β] ⦃a : α⦄,
  0 < a → GaloisConnection (fun x => a • x) fun x => x ⌊/⌋ a
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instIntCast : {α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [IntCast β] → IntCast C(α, β)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.eta`.

---

Eta rule for cones.  -/
CategoryTheory.Limits.Cones.eta : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → (c : CategoryTheory.Limits.Cone F) → c ≅ { pt := c.pt, π := c.π }
-- Init.Data.List.Perm
/-- Lemma used to destruct perms element by element.  -/
List.perm_inv_core : ∀ {α : Type u_1} {a : α} {l₁ l₂ r₁ r₂ : List α}, (l₁ ++ a :: r₁).Perm (l₂ ++ a :: r₂) → (l₁ ++ r₁).Perm (l₂ ++ r₂)
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.card : ∀ (α : Type u_1) (n : ℕ), Nat.card ↑(Set.powersetCard α n) = (Nat.card α).choose n
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_subset_Ioc_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Ioo a b ⊆ Finset.Ioc a b
-- Mathlib.GroupTheory.GroupAction.FixedPoints
AddAction.vadd_neg_mem_fixedBy_iff_mem_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : α} {g : G},
  -g +ᵥ a ∈ AddAction.fixedBy α g ↔ a ∈ AddAction.fixedBy α g
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instInsertOfTransCmp : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Insert α (Std.ExtTreeSet α cmp)
-- Mathlib.Data.Multiset.Fintype
Multiset.coeEquiv_symm_apply_snd_val : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (x : ↥m.toEnumFinset), ↑(m.coeEquiv.symm x).snd = (↑x).2
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.instMonoFunctorTypeι_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂),
  CategoryTheory.Mono (CategoryTheory.Subfunctor.equalizer.ι f g)
-- Init.Data.Nat.Lemmas
Nat.add_lt_of_lt_sub' : ∀ {a b c : ℕ}, b < c - a → a + b < c
-- Mathlib.Topology.UniformSpace.Ultra.Basic
IsUltraUniformity.mk : ∀ {X : Type u_1} [inst : UniformSpace X],
  (uniformity X).HasBasis (fun s => s ∈ uniformity X ∧ s.IsSymm ∧ s.IsTrans) id → IsUltraUniformity X
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- **Alias** of `Subgroup.range_subtype`. -/
Subgroup.subtype_range : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.subtype.range = H
-- Init.Data.List.MinMax
_private.Init.Data.List.MinMax.0.List.min?_attach : ∀ {α : Type u_1} [inst : Min α] [inst_1 : Std.MinEqOr α] {xs : List α},
  xs.attach.min? = Option.pmap (fun m hm => ⟨m, ⋯⟩) xs.min? ⋯
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.supOfBasis_nonneg : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], 0 ≤ NumberField.house.supOfBasis✝ K
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_monotone : ∀ {V : Type u} {G : SimpleGraph V}, Monotone SimpleGraph.Subgraph.verts
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation)
The index `i'` such that `a` and `b` restricted onto `i'` maps into the diagonal components.
See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.i' : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            [∀ (i : I), CompactSpace ↥(D.obj i)] →
              [CategoryTheory.IsCofiltered I] →
                [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] →
                  AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f → I
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLEIrreflOpposite : ∀ {α : Type u_1} {i : LE α} [Std.Irrefl fun x1 x2 => x1 ≤ x2], Std.Irrefl fun x1 x2 => x1 ≤ x2
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_of_le : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ}, a ≤ b → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in Set.Ioc a b, f x ∂μ
-- Mathlib.Algebra.Star.RingQuot
_private.Mathlib.Algebra.Star.RingQuot.0.RingQuot.star'.congr_simp : ∀ {R : Type u} [inst : Semiring R] (r : R → R → Prop) [inst_1 : StarRing R]
  (hr : ∀ (a b : R), r a b → r (star a) (star b)) (a a_1 : RingQuot r),
  a = a_1 → RingQuot.star'✝ r hr a = RingQuot.star'✝ r hr a_1
-- Mathlib.RingTheory.WittVector.Verschiebung
/-- `verschiebungFun x` shifts the coefficients of `x` up by one,
by inserting 0 as the 0th coefficient.
`x.coeff i` then becomes `(verschiebungFun x).coeff (i + 1)`.

`verschiebungFun` is the underlying function of the additive monoid hom `WittVector.verschiebung`.
 -/
WittVector.verschiebungFun : {p : ℕ} → {R : Type u_1} → [CommRing R] → WittVector p R → WittVector p R
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.keys_filter_key : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {f : α → Bool},
  m.WF → (Std.HashMap.Raw.filter (fun k x => f k) m).keys.Perm (List.filter f m.keys)
-- Mathlib.Tactic.Translate.GuessName
/-- Environment extension used for guessing the translation of a name.  -/
Mathlib.Tactic.GuessName.GuessNameExt : Type
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.not_isCycle_nil`. -/
SimpleGraph.Walk.IsCycle.not_of_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, ¬SimpleGraph.Walk.nil.IsCycle
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.HasDetPlusMinusOne.abs_det : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  {Γ : Subgroup (GL n R)} [inst_3 : LinearOrder R] [IsOrderedRing R] [Γ.HasDetPlusMinusOne] {g : GL n R},
  g ∈ Γ → |↑(Matrix.GeneralLinearGroup.det g)| = 1
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.induced_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  TopologicalSpace.induced (⇑h) inst_1 = inst
-- Aesop.RuleSet
Aesop.GlobalRuleSet.mk.sizeOf_spec : ∀ (toBaseRuleSet : Aesop.BaseRuleSet) (simpTheorems : Lean.Meta.SimpTheorems) (simprocs : Lean.Meta.Simprocs),
  sizeOf { toBaseRuleSet := toBaseRuleSet, simpTheorems := simpTheorems, simprocs := simprocs } =
    1 + sizeOf toBaseRuleSet + sizeOf simpTheorems + sizeOf simprocs
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.instDiv : {K : Type u_1} → [Field K] → {a b : K} → Div (QuadraticAlgebra K a b)
-- Init.Data.Option.Lemmas
Option.all_join : ∀ {α : Type u_1} {p : α → Bool} {x : Option (Option α)}, Option.all p x.join = Option.all (Option.all p) x
-- Mathlib.Order.OrderDual
OrderDual.instInhabited : {α : Type u_1} → [h : Inhabited α] → Inhabited αᵒᵈ
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.VAddInvariantMeasure.mk : ∀ {M : Type u_1} {α : Type u_2} [inst : VAdd M α] {x : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  (∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s) →
    MeasureTheory.VAddInvariantMeasure M α μ
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- A map between normed spaces is linear and continuous if and only if it is bounded.  -/
IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F),
  IsLinearMap 𝕜 f ∧ Continuous f ↔ IsBoundedLinearMap 𝕜 f
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.isPartialCorrectnessName : Lean.Environment → Lean.Name → Bool
-- Mathlib.Data.List.Sort
List.sortedLE_replicate : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (n : ℕ), (List.replicate n a).SortedLE
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.augment_hom_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C)
  (f : X.obj (Opposite.op { len := 0 }) ⟶ X₀)
  (w :
    ∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
      CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f),
  (X.augment X₀ f w).hom.app (Opposite.op { len := 0 }) = f
-- Mathlib.Data.Rel
SetRel.preimage_sUnion : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (T : Set (Set β)), R.preimage (⋃₀ T) = ⋃ t ∈ T, R.preimage t
-- Init.Data.FloatArray.Basic
FloatArray.size : FloatArray → ℕ
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.listEncode_injective : ∀ {L : FirstOrder.Language} {α : Type u'}, Function.Injective FirstOrder.Language.Term.listEncode
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Approximate membership in the set, that is, whether some element in the
set is equivalent to this one in the preorder. This is useful primarily for stating
correctness properties; use `∈` for a version that actually uses the BST property
of the tree.

```
Amem 2 {1, 2, 3} = true
Amem 4 {1, 2, 3} = false
```

To see the difference with `Emem`, we need a preorder that is not a partial order.
For example, suppose we compare pairs of numbers using only their first coordinate. Then:
-- TODO: Verify below example
```
Emem (0, 1) {(0, 0), (1, 2)} = false
Amem (0, 1) {(0, 0), (1, 2)} = true
(0, 1) ∈ {(0, 0), (1, 2)} = true
```

The `∈` relation is equivalent to `Amem` as long as the `Ordnode` is well formed,
and should always be used instead of `Amem`.  -/
Ordnode.Amem : {α : Type u_1} → [LE α] → α → Ordnode α → Prop
-- Mathlib.Order.WithBot
WithBot.comp_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (x : WithBot α),
  WithBot.map (h ∘ g) x = WithBot.map h (WithBot.map g x)
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme} {ι : Type u_1}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → X i ⟶ S},
  CategoryTheory.Presieve.ofArrows X f ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings S ↔
    (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
-- Mathlib.Algebra.Category.Grp.Basic
/-- The type of morphisms in `CommGrpCat R`.  -/
CommGrpCat.Hom : CommGrpCat → CommGrpCat → Type u
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.go_eq_of_forall_le : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : α} {i j : ℕ} {xs : List α},
  (∀ y ∈ xs, f x ≤ f y) → List.minIdxOn.go✝ f x i j xs = i
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring is closed under multiplication.  -/
NonUnitalSubring.mul_mem : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x y : R}, x ∈ s → y ∈ s → x * y ∈ s
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WOppSide.trans : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.WOppSide x y → s.WOppSide y z → y ∉ s → s.WSameSide x z
-- Mathlib.FieldTheory.Relrank
Subfield.lift_relrank_comap : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A : Subfield E) (f : L →+* E) (B : Subfield L),
  Cardinal.lift.{v, w} ((Subfield.comap f A).relrank B) = Cardinal.lift.{w, v} (A.relrank (Subfield.map f B))
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.toColex_monotone : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LinearOrder ι]
  [inst_2 : (i : ι) → PartialOrder (α i)], Monotone ⇑toColex
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- `reduce` is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the
maximal reduction of the word.  -/
FreeGroup.reduce.idem : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.reduce (FreeGroup.reduce L) = FreeGroup.reduce L
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
ContinuousMap.range_toLp : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  {𝕜 : Type u_3} [inst_6 : Fact (1 ≤ p)] [inst_7 : NormedRing 𝕜] [inst_8 : Module 𝕜 E] [inst_9 : IsBoundedSMul 𝕜 E],
  (↑(ContinuousMap.toLp p μ 𝕜)).range.toAddSubgroup = MeasureTheory.Lp.boundedContinuousFunction E p μ
-- Mathlib.NumberTheory.PrimeCounting
/-- The prime counting function: Returns the number of primes less than or equal to the input.

With `open scoped Nat.Prime`, this has notation `π`.  -/
Nat.primeCounting : ℕ → ℕ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C),
  (CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans F A).app B =
    CategoryTheory.CartesianMonoidalCategory.prodComparison F A B
-- Lean.Elab.Do.Basic
/-- The expression ``Bind.bind (α:=α) (β:=β) e k``.  -/
Lean.Elab.Do.mkBindApp : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Std.Data.HashSet.Lemmas
Std.HashSet.union_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α}, m₁.union m₂ = m₁ ∪ m₂
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.ne_bot_iff_nonempty : ∀ {α : Type u_2} [inst : TopologicalSpace α] (U : TopologicalSpace.Opens α), U ≠ ⊥ ↔ (↑U).Nonempty
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toListRev.match_1.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Mathlib.Order.SuccPred.Basic
WithTop.succ_coe : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : (a : α) → Decidable (Order.succ a = a)]
  [NoMaxOrder α] {a : α}, Order.succ ↑a = ↑(Order.succ a)
-- Mathlib.Tactic.NormNum.Parity
/-- `norm_num` extension for `Even`.

Works for `ℕ` and `ℤ`.  -/
Mathlib.Meta.NormNum.evalEven : Mathlib.Meta.NormNum.NormNumExt