mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.toFun.congr_simp : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : FiniteDimensional ℝ E] {c : M} (f f_1 : SmoothBumpFunction I c),
  f = f_1 → ∀ (a a_1 : M), a = a_1 → ↑f a = ↑f_1 a_1
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.linearOrder : (A : Type u) →
  [inst : CommRing A] →
    (K : Type v) →
      [inst_1 : Field K] →
        [inst_2 : Algebra A K] →
          [inst_3 : IsDomain A] → [ValuationRing A] → [IsFractionRing A K] → LinearOrder (ValuationRing.ValueGroup A K)
-- Mathlib.Analysis.Convex.Basic
/-- **Alias** of the forward direction of `convex_iff_pointwise_add_subset`.

---

Alternative definition of set convexity, in terms of pointwise set operations.  -/
Convex.set_combo_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q)
      ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.π =
    CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π✝ f n₀
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKey_eq_minEntry_fst : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β} {he : l.isEmpty = false},
  l.minKey he = (l.minEntry he).fst
-- Init.Data.UInt.Bitwise
UInt64.ofFin_rev : ∀ (a : Fin UInt64.size), UInt64.ofFin a.rev = ~~~UInt64.ofFin a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry?.eq_2 : ∀ {α : Type u} {β : Type v} (size : ℕ) (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.minEntry?
      (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) =
    some (k, v)
-- Mathlib.Topology.Compactness.CountablyCompact
IsSeqCompact.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X),
  IsSeqCompact s =
    ∀ ⦃x : ℕ → X⦄, (∀ (n : ℕ), x n ∈ s) → ∃ a ∈ s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
-- Mathlib.Algebra.DirectSum.Ring
/-- A graded version of `CommSemiring`.  -/
DirectSum.GCommSemiring : {ι : Type u_1} → (A : ι → Type u_2) → [AddCommMonoid ι] → [(i : ι) → AddCommMonoid (A i)] → Type (max u_1 u_2)
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.comp_obj : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] {W : Type u_3} [inst_2 : Quiver W] (F : U ⥤q V)
  (G : V ⥤q W) (X : U), (F ⋙q G).obj X = G.obj (F.obj X)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.extraction_forall_of_eventually : ∀ {P : ℕ → ℕ → Prop}, (∀ (n : ℕ), ∀ᶠ (k : ℕ) in Filter.atTop, P n k) → ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
-- Mathlib.Analysis.Analytic.CPolynomial
hasFiniteFPowerSeriesAt_const : ∀ {𝕜 : 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] {c : F} {e : E},
  HasFiniteFPowerSeriesAt (fun x => c) (constFormalMultilinearSeries 𝕜 E c) e 1
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_mono : Monotone Chebyshev.theta
-- Init.Data.Order.Factories
/-- This lemma derives a `LawfulOrderBEq α` instance from a property involving an `LE α` instance.
 -/
Std.LawfulOrderBEq.of_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : LE α], (∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a) → Std.LawfulOrderBEq α
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run a custom tactic at each proof step, configured via environment variables.

Reads from environment variables:
- `TRY_AT_EACH_STEP_TACTIC`: Tactic syntax to try (e.g., "grind +suggestions") - required
- `TRY_AT_EACH_STEP_LABEL`: Human-readable label for output (optional, defaults to tactic)

If `TRY_AT_EACH_STEP_TACTIC` is missing, this linter does nothing.

To enable, add to the `mathlibOnlyLinters` array in `lakefile.lean`:
```lean
⟨`linter.tacticAnalysis.tryAtEachStepFromEnv, true⟩,
```

Then run with the environment variable:
```bash
TRY_AT_EACH_STEP_TACTIC="grind +suggestions" lake build Mathlib
```

This generic entry point is used by the hammer-bench benchmarking tool
(https://github.com/leanprover-community/hammer-bench) to test arbitrary tactics
without requiring Mathlib code changes for each new tactic variant.
 -/
Mathlib.TacticAnalysis.tryAtEachStepFromEnvImpl : Mathlib.TacticAnalysis.Config
-- Mathlib.Order.CompactlyGenerated.Basic
/-- A compact element `k` has the property that any directed set lying strictly below `k` has
its `sSup` strictly below `k`.  -/
CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt : ∀ {α : Type u_3} [inst : CompleteLattice α] {k : α},
  IsCompactElement k → ∀ {s : Set α}, s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → (∀ x ∈ s, x < k) → sSup s < k
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableAt.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  DifferentiableAt ℂ f x → DifferentiableAt ℂ (fun x => Complex.sinh (f x)) x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], k ∈ m₂ → (m₁ ∩ m₂).get! k = m₁.get! k
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_one_subset : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddCommMonoidWithOne k], SkewMonoidAlgebra.support 1 ⊆ 1
-- Mathlib.Algebra.Free
/-- The canonical additive morphism from `FreeAddMagma α` to `FreeAddSemigroup α`.  -/
FreeAddMagma.toFreeAddSemigroup : {α : Type u} → FreeAddMagma α →ₙ+ FreeAddSemigroup α
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.card_withConstants : ∀ (L : FirstOrder.Language) (α : Type w'),
  (L.withConstants α).card = Cardinal.lift.{w', max u v} L.card + Cardinal.lift.{max u v, w'} (Cardinal.mk α)
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
/-- If the operation `Φ` on sections of a vector bundle `V` is tensorial at `x`, then it depends
only on the germ of the section at `x`.

This is later superseded by `TensorialAt.pointwise`, showing that `Φ` depends only on the value at
`x` itself.  -/
TensorialAt.local : ∀ {𝕜 : 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 : FiberBundle F V] {A : Type u_9} [inst_13 : AddCommGroup A]
  [inst_14 : Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M},
  TensorialAt I F Φ x →
    ∀ {σ σ' : (x : M) → V x}, MDiffAt (T% σ) x → MDiffAt (T% σ') x → (∀ᶠ (x' : M) in nhds x, σ x' = σ' x') → Φ σ = Φ σ'
-- Lean.Linter.Init
Lean.Linter.LinterSetsState.mk : Lean.Linter.LinterSets → Array (Lean.Name × Lean.NameSet) → Lean.Linter.LinterSetsState
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.hasDerivAt_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R 𝕜]
  (q : Polynomial R) (x : 𝕜),
  HasDerivAt (fun x => (Polynomial.aeval x) q) ((Polynomial.aeval x) (Polynomial.derivative q)) x
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.mk.injEq : ∀ {R : Type u_2} [inst : NonUnitalNonAssocRing R] (toRingSeminorm : RingSeminorm R)
  (eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0) (toRingSeminorm_1 : RingSeminorm R)
  (eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toRingSeminorm_1.toFun x = 0 → x = 0),
  ({ toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
      { toRingSeminorm := toRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }) =
    (toRingSeminorm = toRingSeminorm_1)
-- Mathlib.RingTheory.LocalRing.Length
CovBy.length_restrictScalars : ∀ (A : Type u_1) {B : Type u_2} {M : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsLocalRing A]
  [inst_3 : IsLocalRing B] [inst_4 : Algebra A B] [inst_5 : IsLocalHom (algebraMap A B)] [inst_6 : AddCommGroup M]
  [inst_7 : Module A M] [inst_8 : Module B M] [inst_9 : IsScalarTower A B M] {p q : Submodule B M},
  p ⋖ q →
    Module.length A ↥q = Module.length A ↥p + Module.length (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
_private.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation.0.Real.integrableOn_rpowIntegrand₀₁_Ioc : ∀ {p x : ℝ},
  p ∈ Set.Ioo 0 1 →
    0 ≤ x → MeasureTheory.IntegrableOn (fun x_1 => p.rpowIntegrand₀₁ x_1 x) (Set.Ioc 0 1) MeasureTheory.volume
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_zero_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → MeasureTheory.Measure β),
  MeasureTheory.Measure.bind 0 f = 0
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.norm_natCast_zmodRepr_eq_iff : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {x : ℤ_[p]}, ‖↑x.zmodRepr‖ = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- All `F : J ⥤ C` have colimits for a fixed `J`  -/
CategoryTheory.Limits.HasColimitsOfShape.has_colimit : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  [self : CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.HasColimit F
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α]
  (l : Std.DTreeMap.Internal.Impl α β) (k : α) (h : (l.get?ₘ k).isSome = true), l.getₘ k h = (l.get?ₘ k).get h
-- Aesop.Script.SScript
Aesop.Script.SScript.focusAndSolve.sizeOf_spec : ∀ (goalPos : ℕ) (here tail : Aesop.Script.SScript),
  sizeOf (Aesop.Script.SScript.focusAndSolve goalPos here tail) = 1 + sizeOf goalPos + sizeOf here + sizeOf tail
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
/-- Internal state of the `takeWhile` combinator. Do not depend on its internals.
 -/
Std.Iterators.Types.TakeWhile : Type w → (m : Type w → Type w') → (β : Type w) → (β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)) → Type w
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.pullSub_adjunction : ∀ {A : Type u_1} (S T : ↥(Descriptive.tree A)) (x : List A),
  Descriptive.Tree.pullSub S x ≤ T ↔ S ≤ Descriptive.Tree.subAt T x
-- Init.Data.String.Lemmas.FindPos
String.posLT_eq_prev : ∀ {s : String} {p : String.Pos.Raw} {h : 0 < p} (h' : String.Pos.Raw.IsValid s p), s.posLT p h = (s.pos p h').prev ⋯
-- Init.Data.UInt.Bitwise
UInt32.toNat_not : ∀ (a : UInt32), (~~~a).toNat = UInt32.size - 1 - a.toNat
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtPlace_real : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (c : ℝ),
  (NumberField.mixedEmbedding.normAtPlace w) (fun x => c, fun x => ↑c) = |c|
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- The constructed pullback cone is indeed the pullback.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : AlgebraicGeometry.PresheafedSpace C} →
      (f : X ⟶ Z) →
        [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] →
          (g : Y ⟶ Z) →
            CategoryTheory.Limits.IsLimit (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f g)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that a type has `MeasurableSub₂` if `uncurry (· - ·)` is a measurable function.
For a typeclass assuming measurability of `(c - ·)` and `(· - c)` see `MeasurableSub`.  -/
MeasurableSub₂ : (G : Type u_2) → [MeasurableSpace G] → [Sub G] → Prop
-- Mathlib.Tactic.Order.Graph.Tarjan
/-- A time counter that increments each time the algorithm visits an unvisited vertex.  -/
Mathlib.Tactic.Order.Graph.TarjanState.time : Mathlib.Tactic.Order.Graph.TarjanState → ℕ
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.galAction_isPretransitive : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Fact (Polynomial.map (algebraMap F E) p).Splits],
  Irreducible p → MulAction.IsPretransitive p.Gal ↑(p.rootSet E)
-- Mathlib.Data.List.Map2
List.map₂Right'_nil_right : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α), List.map₂Right' f as [] = ([], as)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.eq_1 : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (n : WithTop ℕ∞) (f : M → M')
  (s : Set M) (x : M),
  ContMDiffWithinAt I I' n f s x = ChartedSpace.LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x
-- Mathlib.FieldTheory.Galois.Basic
FixedPoints.mem_intermediateField_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {M : Type u_3}
  [inst_3 : Monoid M] [inst_4 : MulSemiringAction M E] [inst_5 : SMulCommClass M F E] {x : E},
  x ∈ FixedPoints.intermediateField M ↔ ∀ (m : M), m • x = x
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π_assoc : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D}
  (h : E.IsPointwiseRightKanExtensionAt Y)
  [inst_3 : CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)]
  (g : CategoryTheory.StructuredArrow Y L) {Z : H} (h_1 : F.obj ((CategoryTheory.StructuredArrow.proj Y L).obj g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.isoLimit.hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y L).comp F) g) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map g.hom)
        ((CategoryTheory.CostructuredArrow.hom E).app g.right))
      h_1
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.continuousSMul : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [RingHomSurjective σ] [RingHomIsometric σ]
  [inst_9 : TopologicalSpace F] [inst_10 : IsTopologicalAddGroup F] [inst_11 : ContinuousSMul 𝕜₂ F] (𝔖 : Set (Set E)),
  (∀ S ∈ 𝔖, Bornology.IsVonNBounded 𝕜₁ S) → ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.Order.Bounds.Basic
nonempty_of_not_bddAbove : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [ha : Nonempty α], ¬BddAbove s → s.Nonempty
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : a ≤ b)
  (a' b' : EInt) (hab' : a' ≤ b')
  (φ :
    CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hab) ⟶
      CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hab'))
  (X : C),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X))
      (CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X))
        ((t.eTruncLTGEIsoGELT a' b').hom.app X)) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X))
        ((t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)))
-- Mathlib.SetTheory.Ordinal.Family
/-- Converts a family indexed by a `Type u` to one indexed by an `Ordinal.{u}` using a well-ordering
given by the axiom of choice.  -/
Ordinal.bfamilyOfFamily : {α : Type u_1} → {ι : Type u} → (ι → α) → (a : Ordinal.{u}) → a < Ordinal.type WellOrderingRel → α
-- Batteries.Data.Fin.Fold
Fin.dfoldrM_eq_foldrM : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α),
  Fin.dfoldrM n (fun x => α) f x = Fin.foldrM n f x
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_pure : ∀ {α β : Type u} (f : α → β) (x : α), f <$> pure x = pure (f x)
-- Std.Do.SPred.SVal
Std.Do.SVal.instInhabitedStateTupleCons : {σ : Type u_1} →
  {σs : List (Type u_1)} →
    [Inhabited σ] → [Inhabited (Std.Do.SVal.StateTuple σs)] → Inhabited (Std.Do.SVal.StateTuple (σ :: σs))
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsEisensteinAt.coeff_mem : ∀ {R : Type u} [inst : CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R},
  f.IsEisensteinAt 𝓟 → ∀ {n : ℕ}, n ≠ f.natDegree → f.coeff n ∈ 𝓟
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.brecOn_2.go : {motive_1 : Lean.Lsp.Ipc.ModuleHierarchy → Sort u} →
  {motive_2 : Array Lean.Lsp.Ipc.ModuleHierarchy → Sort u} →
    {motive_3 : List Lean.Lsp.Ipc.ModuleHierarchy → Sort u} →
      (t : List Lean.Lsp.Ipc.ModuleHierarchy) →
        ((t : Lean.Lsp.Ipc.ModuleHierarchy) → t.below → motive_1 t) →
          ((t : Array Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_1 t → motive_2 t) →
            ((t : List Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_2 t → motive_3 t) →
              motive_3 t ×' Lean.Lsp.Ipc.ModuleHierarchy.below_2 t
-- Lean.Elab.Tactic.Simp
/-- Extract the arguments from a `simpArgs` syntax as an array of syntaxes  -/
Lean.Parser.Tactic.getSimpArgs? : Lean.Syntax → Option (Array Lean.Syntax)
-- Mathlib.Order.Heyting.Hom
HeytingHom.toLatticeHom : {α : Type u_6} →
  {β : Type u_7} → [inst : HeytingAlgebra α] → [inst_1 : HeytingAlgebra β] → HeytingHom α β → LatticeHom α β
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.BackwardRule.mk.injEq : ∀ (expr : Lean.Expr) (pattern : Lean.Meta.Sym.Pattern) (resultPos : List ℕ) (expr_1 : Lean.Expr)
  (pattern_1 : Lean.Meta.Sym.Pattern) (resultPos_1 : List ℕ),
  ({ expr := expr, pattern := pattern, resultPos := resultPos } =
      { expr := expr_1, pattern := pattern_1, resultPos := resultPos_1 }) =
    (expr = expr_1 ∧ pattern = pattern_1 ∧ resultPos = resultPos_1)
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
/-- Let `A ⊆ B` be a finite extension of Dedekind domains and assume that `A ⊆ R₁, R₂ ⊆ B` are two
subrings such that `Frac R₁ ⊔ Frac R₂ = Frac B`, `Frac R₁` and `Frac R₂` are linearly disjoint
over `Frac A`, and that `𝓓(R₁/A)` and `𝓓(R₂/A)` are coprime where `𝓓` denotes the different ideal
and `Frac R` denotes the fraction field of a domain `R`.
Then `B` is generated (as an `A`-algebra) by `R₁` and `R₂`.
 -/
IsDedekindDomain.range_sup_range_eq_top_of_isCoprime_differentIdeal : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [FiniteDimensional K L] [inst_10 : IsScalarTower A K L] (R₁ : Type u_5)
  (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [IsDomain R₁] [inst_14 : Algebra A R₁]
  [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B] [inst_18 : Algebra R₁ L]
  [inst_19 : Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂]
  {F₁ F₂ : IntermediateField K L} [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂] [Module.IsTorsionFree R₁ ↥F₁]
  [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L]
  [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [inst_33 : IsDomain A] [inst_34 : IsDedekindDomain B]
  [inst_35 : IsDedekindDomain R₁] [inst_36 : IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁]
  [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [Module.IsTorsionFree R₁ B]
  [Module.IsTorsionFree R₂ B], ⋯
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mk.injEq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (toNonUnitalSubalgebra : NonUnitalSubalgebra R A)
  (star_mem' : ∀ {a : A}, a ∈ toNonUnitalSubalgebra.carrier → star a ∈ toNonUnitalSubalgebra.carrier)
  (toNonUnitalSubalgebra_1 : NonUnitalSubalgebra R A)
  (star_mem'_1 : ∀ {a : A}, a ∈ toNonUnitalSubalgebra_1.carrier → star a ∈ toNonUnitalSubalgebra_1.carrier),
  ({ toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := star_mem' } =
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := star_mem'_1 }) =
    (toNonUnitalSubalgebra = toNonUnitalSubalgebra_1)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [CompleteSpace E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {f : α → E}
  (fmeas : Measurable f),
  MeasureTheory.Integrable f μ →
    ∀ (s : Set E) [inst_5 : TopologicalSpace.SeparableSpace ↑s] (hs : Set.range f ∪ {0} ⊆ s),
      Filter.Tendsto (fun n => MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.approxOn f fmeas s 0 ⋯ n))
        Filter.atTop (nhds (∫ (x : α), f x ∂μ))
-- Std.Http.Data.Status
/-- 306 Unused
 -/
Std.Http.Status.unused : Std.Http.Status
-- Mathlib.Data.Matrix.Reflection
Matrix.Forall.eq_1 : ∀ {α : Type u_1} (x : ℕ) (x_1 : Matrix (Fin 0) (Fin x) α → Prop), Matrix.Forall x_1 = x_1 (Matrix.of ![])
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_mul_C : ∀ {R : Type u} {a b : R} {n : ℕ} [inst : Semiring R],
  (Polynomial.monomial n) a * Polynomial.C b = (Polynomial.monomial n) (a * b)
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.exists_isRoot_of_odd_natDegree : ∀ {R : Type u_1} {inst : Field R} [self : IsRealClosed R] {f : Polynomial R}, Odd f.natDegree → ∃ x, f.IsRoot x
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElabM.saveState : Lean.Elab.Do.DoElabM Lean.Elab.Do.SavedState