mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Constructions
pi_generateFrom_eq_finite : ∀ {ι : Type u_5} {X : ι → Type u_9} {g : (a : ι) → Set (Set (X a))} [Finite ι],
  (∀ (a : ι), ⋃₀ g a = Set.univ) →
    Pi.topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.univ.pi s}
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- Every two-sided ideal is also a right ideal.  -/
TwoSidedIdeal.asIdealOpposite : {R : Type u_1} → [inst : Ring R] → TwoSidedIdeal R →o Ideal Rᵐᵒᵖ
-- Mathlib.Tactic.NormNum.IsSquare
/-- `norm_num` extension for `IsSquare` on `ℚ`.  -/
Mathlib.Meta.NormNum.evalIsSquareRat : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Order.Category.BddOrd
BddOrd.mk.injEq : ∀ (toPartOrd : PartOrd) [isBoundedOrder : BoundedOrder ↑toPartOrd] (toPartOrd_1 : PartOrd)
  (isBoundedOrder_1 : BoundedOrder ↑toPartOrd_1),
  ({ toPartOrd := toPartOrd, isBoundedOrder := isBoundedOrder } =
      { toPartOrd := toPartOrd_1, isBoundedOrder := isBoundedOrder_1 }) =
    (toPartOrd = toPartOrd_1 ∧ isBoundedOrder ≍ isBoundedOrder_1)
-- Init.Data.Order.Classes
/-- This typeclass states that `Max.max a b` returns one of its arguments, either `a` or `b`.
 -/
Std.MaxEqOr : (α : Type u) → [Max α] → Prop
-- Init.Data.SInt.Lemmas
BitVec.ofInt_iSizeToInt : ∀ (x : ISize), BitVec.ofInt System.Platform.numBits x.toInt = x.toBitVec
-- Mathlib.Algebra.Group.Action.End
AddAut.vadd_def : ∀ {M : Type u_2} [inst : AddMonoid M] (f : AddAut M) (a : M), f +ᵥ a = f a
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nonneg_of_mem_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.closedBall x ε → 0 ≤ ε
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.comp_apply : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : One M] [inst_1 : One N] [inst_2 : One P] (g : OneHom N P)
  (f : OneHom M N) (x : M), (g.comp f) x = g (f x)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.ext : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} {f g : A.Copy B}, (∀ (a : α), f a = g a) → f = g
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.erase_dup : Lean.Meta.Grind.AC.DiseqCnstr → Lean.Meta.Grind.AC.DiseqCnstrProof
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_zero_ofNat_zero : ∀ {w : ℕ}, (0#(w + 1))[0]? = some false
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.lift.eq_1 : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M],
  FreeMonoid.lift =
    {
      toFun := fun f =>
        { toFun := fun l => FreeMonoid.prodAux (List.map f (FreeMonoid.toList l)), map_one' := ⋯, map_mul' := ⋯ },
      invFun := fun f x => f (FreeMonoid.of x), left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Sum.Lemmas
Sum.swap_swap_eq : ∀ {α : Type u_1} {β : Type u_2}, Sum.swap ∘ Sum.swap = id
-- Mathlib.Topology.UniformSpace.Closeds
/-- The Hausdorff uniformity on the powerset of a uniform space. Used for defining the uniformities
on `Closeds`, `Compacts` and `NonemptyCompacts`.
See note [reducible non-instances].  -/
UniformSpace.hausdorff : (α : Type u_1) → [UniformSpace α] → UniformSpace (Set α)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- The difference of two covariant derivatives, as a one-form taking values in the
endomorphisms of `V`.  -/
CovariantDerivative.difference : {𝕜 : 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] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            [CompleteSpace 𝕜] →
                                              [FiniteDimensional 𝕜 F] →
                                                [inst_17 : VectorBundle 𝕜 F V] →
                                                  [ContMDiffVectorBundle 1 F V I] →
                                                    CovariantDerivative I F V →
                                                      CovariantDerivative I F V →
                                                        (x : M) → V x →L[𝕜] TangentSpace I x →L[𝕜] V x
-- Mathlib.Data.Sum.Basic
Sum.getRight_eq_getRight? : ∀ {α : Type u} {β : Type v} {x : α ⊕ β} (h₁ : x.isRight = true) (h₂ : x.getRight?.isSome = true),
  x.getRight h₁ = x.getRight?.get h₂
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getInt16Value? : Lean.Expr → OptionT Id Int16
-- Mathlib.Topology.VectorBundle.Basic
/-- Topology on the total space that will make the prebundle into a bundle.  -/
VectorPrebundle.totalSpaceTopology : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : (x : B) → TopologicalSpace (E x)] →
                      VectorPrebundle R F E → TopologicalSpace (Bundle.TotalSpace F E)
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- (Possibly multivariate) power series which can be substituted in a `PowerSeries`.  -/
PowerSeries.HasSubst : {τ : Type u_3} → {S : Type u_4} → [CommRing S] → MvPowerSeries τ S → Prop
-- Mathlib.Analysis.Normed.Group.Defs
/-- A seminormed group is a group endowed with a norm for which `dist x y = ‖x⁻¹ * y‖`
defines a pseudometric space structure.  -/
SeminormedCommGroup : Type u_8 → Type u_8
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Grind.Config
-- Mathlib.Computability.TuringDegree
/-- `f` is Turing equivalent to `g` if `f` is reducible to `g` and `g` is reducible to `f`.
 -/
Computability.«term_≡ᵀ_» : Lean.TrailingParserDescr
-- Init.Data.Vector.Lemmas
Vector.push_inj_left : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs ys : Vector α n}, xs.push a = ys.push a ↔ xs = ys
-- Lean.Util.PtrSet
Lean.mkPtrSet : {α : Type} → optParam ℕ 64 → Lean.PtrSet α
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- This is the equivalence relation on linear maps such that `u ≈ v` precisely
when `u - v` is a linear map with noetherian range. We allow ourself this slightly abusive name
because the more natural definition (`u - v` has finitely generated range) only yields a
well-behaved relation (more precisely, an additive congruence relation compatible with composition
on both sides) over a noetherian ring, in which case the two notions agree.

This setoid is declared as an instance in scope `LinearMap.FiniteRangeSetoid`.  -/
LinearMap.FiniteRangeSetoid.setoid : {K : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_4} →
      [inst : CommRing K] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module K V] → [inst_3 : AddCommGroup V₂] → [inst_4 : Module K V₂] → Setoid (V →ₗ[K] V₂)
-- Mathlib.RingTheory.WittVector.Defs
WittVector.nsmul_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (m : ℕ) (x : WittVector p R) (n : ℕ),
  (m • x).coeff n = WittVector.peval (WittVector.wittNSMul p m n) ![x.coeff]
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The topology of convergence in distribution on a separable Borel space is metrizable.  -/
MeasureTheory.instMetrizableSpaceProbabilityMeasure : ∀ (X : Type u_2) [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X]
  [TopologicalSpace.SeparableSpace X] [inst_3 : MeasurableSpace X] [inst_4 : BorelSpace X],
  TopologicalSpace.MetrizableSpace (MeasureTheory.ProbabilityMeasure X)
-- Mathlib.Data.Set.Image
Subtype.forall_set_subtype : ∀ {α : Type u_1} {t : Set α} (p : Set α → Prop), (∀ (s : Set ↑t), p (Subtype.val '' s)) ↔ ∀ s ⊆ t, p s
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceSignatureHelpParams : Lean.Lsp.FileSource Lean.Lsp.SignatureHelpParams
-- Mathlib.Computability.TuringDegree
_private.Mathlib.Computability.TuringDegree.0.instPreorderPFunNat : Preorder (ℕ →. ℕ)
-- Init.Data.Option.Lemmas
Option.filter_some : ∀ {α : Type u_1} {p : α → Bool} {a : α}, Option.filter p (some a) = if p a = true then some a else none
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.contains_char_eq_contains_beq : ∀ {c : Char} {s : String.Slice}, s.contains c = s.contains fun x => x == c
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.instInv : {σ : Type u_1} → {k : Type u_3} → [Field k] → Inv (MvPowerSeries σ k)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The distinguished element in `Splitting.IndexSet Δ` which corresponds to the
identity of `Δ`.  -/
CategoryTheory.SimplicialObject.Splitting.IndexSet.id : (Δ : SimplexCategoryᵒᵖ) → CategoryTheory.SimplicialObject.Splitting.IndexSet Δ
-- Lean.Elab.Tactic.Basic
/-- Closes main goal using the given expression.
If `checkUnassigned == true`, then `val` must not contain unassigned metavariables.
Returns `true` if `val` was successfully used to close the goal.
 -/
Lean.Elab.Tactic.closeMainGoal : Lean.Name → Lean.Expr → optParam Bool true → Lean.Elab.Tactic.TacticM Unit
-- Lean.Server.InfoUtils
Lean.Elab.GoalsAtResult : Type
-- Mathlib.Order.OmegaCompletePartialOrder
Function.IsFixedPt.eq_1 : ∀ {α : Type u₁} (f : α → α) (x : α), Function.IsFixedPt f x = (f x = x)
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.BoundedFormula.all_iff_not_ex_not : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α (n + 1)),
  T.Iff φ.all φ.not.ex.not
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonChangeAnnotation.toJson : Lean.Lsp.ChangeAnnotation → Lean.Json
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyPrepareParams.fromJson : Lean.Json → Except String Lean.Lsp.CallHierarchyPrepareParams
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.XIsoBiprod.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel i j)
  [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)],
  HomologicalComplex.homotopyCofiber.XIsoBiprod φ i j hij = HomologicalComplex.homotopyCofiber.XIsoBiprod φ i j hij
-- Mathlib.RingTheory.QuasiFinite.Weakly
/-- Use `Algebra.QuasiFinite.of_quasiFiniteAt_residueField` instead
for `Algebra.QuasiFiniteAt R q`.  -/
Algebra.WeaklyQuasiFiniteAt.of_quasiFiniteAt_residueField : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [inst_3 : q.IsPrime] [inst_4 : p.IsPrime] [q.LiesOver p] (Q : Ideal (p.Fiber S)) [inst_6 : Q.IsPrime],
  Ideal.comap Algebra.TensorProduct.includeRight.toRingHom Q = q →
    ∀ [Algebra.QuasiFiniteAt p.ResidueField Q], Algebra.WeaklyQuasiFiniteAt R q
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.WF → t.isEmpty = false → ∀ {km fallback : α}, t.maxD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Order.Interval.Set.Monotone
AntitoneOn.Ico : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β} {s : Set α},
  AntitoneOn f s → MonotoneOn g s → MonotoneOn (fun x => Set.Ico (f x) (g x)) s
-- Mathlib.Data.List.ReduceOption
List.reduceOption_cons_of_some : ∀ {α : Type u_1} (x : α) (l : List (Option α)), (some x :: l).reduceOption = x :: l.reduceOption
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₂_gamma : ∀ (o : Ordinal.{u_1}), o.gamma.invVeblen₂ = 0
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂),
  (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 0 = f₁
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.lift_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  (f : { a // a ≠ 0 } → α)
  (h : ∀ (a b : { a // a ≠ 0 }), FiniteArchimedeanClass.mk ↑a ⋯ = FiniteArchimedeanClass.mk ↑b ⋯ → f a = f b) {a : M}
  (ha : a ≠ 0), FiniteArchimedeanClass.lift f h (FiniteArchimedeanClass.mk a ha) = f ⟨a, ha⟩
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.isInt_lcm : ∀ {x y nx ny : ℤ} {z : ℕ},
  Mathlib.Meta.NormNum.IsInt x nx →
    Mathlib.Meta.NormNum.IsInt y ny → nx.lcm ny = z → Mathlib.Meta.NormNum.IsNat (x.lcm y) z
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Sentence.cardGe.eq_1 : ∀ (L : FirstOrder.Language) (n : ℕ),
  FirstOrder.Language.Sentence.cardGe L n =
    (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤
        (List.map
          (fun ij =>
            (((FirstOrder.Language.var ∘ Sum.inr) ij.1).bdEqual ((FirstOrder.Language.var ∘ Sum.inr) ij.2)).not)
          (List.filter (fun ij => decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))).exs
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.instEncodableS : Encodable Mathlib.Deriving.Encodable.S✝
-- Mathlib.Order.CompleteLattice.Basic
iSup_subtype' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α},
  ⨆ i, ⨆ (h : p i), f i h = ⨆ x, f ↑x ⋯
-- Init.Data.BitVec.Lemmas
BitVec.msb_twoPow : ∀ {i w : ℕ}, (BitVec.twoPow w i).msb = (decide (i < w) && decide (i = w - 1))
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
/-- In the permutation group, the stabilizer of any set
acts primitively on that set.  -/
MulAction.isPreprimitive_stabilizer_of_surjective : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (s : Set α),
  Function.Surjective MulAction.toPerm → MulAction.IsPreprimitive ↥(MulAction.stabilizer M s) ↑s
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.dFrom_eq : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
  (r : c.Rel i j), C.dFrom i = CategoryTheory.CategoryStruct.comp (C.d i j) (C.xNextIso r).inv
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx?.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_1 ()
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Move elements from `k₁` to `k₂` without reversion, by performing a double move via the `rev`
stack.  -/
Turing.PartrecToTM2.move₂ : (Turing.PartrecToTM2.Γ' → Bool) →
  Turing.PartrecToTM2.K' → Turing.PartrecToTM2.K' → Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ'
-- Mathlib.Util.Notation3
/-- Create a `Term` that represents a matcher for `scoped` notation.
Fails in the `OptionT` sense if a matcher couldn't be constructed.
Also returns a delaborator key like in `mkExprMatcher`.
Reminder: `$lit:ident : (scoped $scopedId:ident => $scopedTerm:Term)`  -/
Mathlib.Notation3.mkScopedMatcher : Lean.Name →
  Lean.Name → Lean.Term → Array Lean.Name → OptionT Lean.Elab.TermElabM (List Mathlib.Notation3.DelabKey × Lean.Term)
-- Mathlib.SetTheory.Cardinal.Aleph
/-- The `omega` function gives the infinite initial ordinals listed by their ordinal index.
`omega 0 = ω`, `omega 1 = ω₁` is the first uncountable ordinal, and so on.

This is not to be confused with the first infinite ordinal `Ordinal.omega0`.

For a version including finite ordinals, see `Ordinal.preOmega`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ω_` in identifiers is `omega`. -/
Ordinal.omega : Ordinal.{u_1} ↪o Ordinal.{u_1}
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_sup_comap_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S],
  Function.Surjective ⇑f → ∀ (I J : Ideal S), Ideal.map f (Ideal.comap f I ⊔ Ideal.comap f J) = I ⊔ J
-- Lean.Parser.Term
Lean.Parser.Term.subst.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.Group.Basic
/-- Multiplication from the right in a topological group as a homeomorphism.  -/
Homeomorph.mulRight : {G : Type w} → [inst : TopologicalSpace G] → [inst_1 : Group G] → [SeparatelyContinuousMul G] → G → G ≃ₜ G
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_PInfty_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] {Z : ChainComplex C ℕ}
  (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom.f
      (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) =
    CategoryTheory.CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom.f h
-- Batteries.Tactic.Lint.Basic
/-- Returns true if `decl` is an automatically generated declaration.

Also returns true if `decl` is an internal name or created during macro
expansion.

See `Lean.Environment.isAutoDecl` for an identical pure version of this function on the environment.
 -/
Batteries.Tactic.Lint.isAutoDecl : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.tensorUnit_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.MonObj.mul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStmts₁.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (f : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trStmts₁ (Turing.TM2.Stmt.pop k f q) =
    {Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.pop f) q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Real.cos` is real analytic.  -/
Real.analyticOn_cos : ∀ {s : Set ℝ}, AnalyticOn ℝ Real.cos s
-- Mathlib.GroupTheory.Coset.Basic
/-- The natural bijection between a right coset `s * g` and `s`.  -/
Subgroup.rightCosetEquivSubgroup : {α : Type u_1} → [inst : Group α] → {s : Subgroup α} → (g : α) → ↑(MulOpposite.op g • ↑s) ≃ ↥s
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.go.induct_unfolding : ∀ (pat : String.Slice)
  (motive :
    (table : Array ℕ) →
      0 < table.size →
        table.size ≤ pat.utf8ByteSize →
          (∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) → Vector ℕ pat.utf8ByteSize → Prop),
  (∀ (table : Array ℕ) (ht₀ : 0 < table.size) (ht : table.size ≤ pat.utf8ByteSize)
      (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) (h_1 : table.size < pat.utf8ByteSize),
      let patByte := pat.getUTF8Byte { byteIdx := table.size } h_1;
      let dist :=
        String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat patByte table ht h
          table[table.size - 1] ⋯;
      motive (table.push ↑dist) ⋯ ⋯ ⋯
          (String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat (table.push ↑dist) ⋯ ⋯ ⋯) →
        motive table ht₀ ht h (String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat (table.push ↑dist) ⋯ ⋯ ⋯)) →
    (∀ (table : Array ℕ) (ht₀ : 0 < table.size) (ht : table.size ≤ pat.utf8ByteSize)
        (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) (h_1 : ¬table.size < pat.utf8ByteSize),
        motive table ht₀ ht h (Vector.mk table ⋯)) →
      ∀ (table : Array ℕ) (ht₀ : 0 < table.size) (ht : table.size ≤ pat.utf8ByteSize)
        (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i),
        motive table ht₀ ht h (String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat table ht₀ ht h)
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instIsScalarTower : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] {V : Type u_8} [inst_1 : Monoid R] [inst_2 : AddMonoid V]
  [inst_3 : DistribMulAction R V] {S : Type u_9} [inst_4 : Monoid S] [inst_5 : DistribMulAction S V] [inst_6 : SMul R S]
  [IsScalarTower R S V], IsScalarTower R S (HahnSeries Γ V)
-- Init.Data.Float.Model.Format.Basic
Float.Model.Format.mk : (mantissaBitsWithoutImplicit : ℕ) →
  autoParam (0 < mantissaBitsWithoutImplicit) Float.Model.Format.hm._autoParam →
    (exponentBits : ℕ) → autoParam (0 < exponentBits) Float.Model.Format.he._autoParam → Float.Model.Format
-- Lean.Parser.Module
Lean.Parser.testParseFile : Lean.Environment → System.FilePath → IO Lean.Syntax
-- Mathlib.Data.Set.Card
Set.Finite.eq_insert_of_subset_of_encard_eq_succ : ∀ {α : Type u_1} {s t : Set α}, s.Finite → s ⊆ t → t.encard = s.encard + 1 → ∃ a, t = insert a s
-- Mathlib.Data.Set.Prod
Set.pi.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) (t : (i : ι) → Set (α i)), s.pi t = {f | ∀ i ∈ s, f i ∈ t i}
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.homologyι_singleObjOpcyclesSelfIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).homologyι j)
      (HomologicalComplex.singleObjOpcyclesSelfIso c j A).inv =
    (HomologicalComplex.singleObjHomologySelfIso c j A).hom
-- Init.Data.Array.Count
Array.countP_push_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α}, ¬p a = true → Array.countP p (xs.push a) = Array.countP p xs
-- Mathlib.Analysis.Complex.Hadamard
/-- Useful rewrite for the absolute value of `invInterpStrip`  -/
Complex.HadamardThreeLines.norm_invInterpStrip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (z : ℂ) {ε : ℝ},
  ε > 0 →
    ‖Complex.HadamardThreeLines.invInterpStrip f z ε‖ =
      (ε + Complex.HadamardThreeLines.sSupNormIm f 0) ^ (z.re - 1) *
        (ε + Complex.HadamardThreeLines.sSupNormIm f 1) ^ (-z.re)
-- Mathlib.Data.Set.Card
Set.ncard_lt_card : ∀ {α : Type u_1} {s : Set α} [Finite α], s ≠ Set.univ → s.ncard < Nat.card α
-- Lean.Elab.MacroArgUtil
_private.Lean.Elab.MacroArgUtil.0.Lean.Elab.Command.expandMacroArg.mkSyntaxAndPat : Option Lean.Ident → Lean.Term → Lean.TSyntax `stx → Lean.Elab.Command.CommandElabM (Lean.TSyntax `stx × Lean.Term)
-- Mathlib.Algebra.Order.Ring.Basic
Odd.pow_injective : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : ℕ},
  Odd n → Function.Injective fun x => x ^ n