mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.match_1.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β) (out : β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.internalState.inner.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.CompleteSublattice
/-- The range of a `CompleteLatticeHom` is a `CompleteSublattice`.

See Note [range copy pattern].  -/
CompleteLatticeHom.range : {α : Type u_1} →
  {β : Type u_2} →
    [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → CompleteLatticeHom α β → CompleteSublattice β
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.IsStableUnderShiftBy.le_shift : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.ObjectProperty C} {A : Type u_2}
  {inst_1 : AddMonoid A} {inst_2 : CategoryTheory.HasShift C A} {a : A} [self : P.IsStableUnderShiftBy a], P ≤ P.shift a
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsRegular.toIsWeaklyRegular : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {rs : List R},
  RingTheory.Sequence.IsRegular M rs → RingTheory.Sequence.IsWeaklyRegular M rs
-- Mathlib.LinearAlgebra.Dimension.Finite
natCast_le_rank_iff : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R] {n : ℕ},
  ↑n ≤ Module.rank R M ↔ ∃ f, LinearIndependent R f
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.term.eq_1 : ∀ (f : ℕ → ℂ) (s : ℂ) (n : ℕ), LSeries.term f s n = if n = 0 then 0 else f n / ↑n ^ s
-- Mathlib.Algebra.Category.Grp.Zero
AddGrpCat.isZero_iff_subsingleton : ∀ {G : AddGrpCat}, CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- Delta-generated spaces are sequential.  -/
DeltaGeneratedSpace.instSequentialSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [DeltaGeneratedSpace X], SequentialSpace X
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instCompactSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [CompactSpace α], CompactSpace (TopologicalSpace.Compacts α)
-- Lean.Meta.PPGoal
Lean.Meta.pp.inaccessibleNames : Lean.Option Bool
-- Mathlib.Order.Fin.Basic
Fin.castLE_le_castLE_iff : ∀ {m n : ℕ} {i j : Fin n} (h : n ≤ m), Fin.castLE h i ≤ Fin.castLE h j ↔ i ≤ j
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.BackwardPattern.mk : {ρ : Type} →
  {pat : ρ} →
    ((s : String.Slice) → Option s.Pos) →
      ((s : String.Slice) → s.isEmpty = false → Option s.Pos) →
        (String.Slice → Bool) → String.Slice.Pattern.BackwardPattern pat
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_singleton_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  (f : X ⟶ Y) (x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.singleton f))
  (y : P.obj (Opposite.op Y)), x.IsAmalgamation y ↔ (CategoryTheory.ConcreteCategory.hom (P.map f.op)) y = x f ⋯
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mem_support : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} [inst_1 : P.HasIdealSupport] {x : R},
  x ∈ P.support ↔ x ∈ P ∧ -x ∈ P
-- Mathlib.Order.Shrink
equivShrink_le_equivShrink : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Preorder α] {x y : α},
  (equivShrink α) x ≤ (equivShrink α) y ↔ x ≤ y
-- Mathlib.Logic.Encodable.Basic
Encodable.decode₂_eq_some : ∀ {α : Type u_1} [inst : Encodable α] {n : ℕ} {a : α}, Encodable.decode₂ α n = some a ↔ Encodable.encode a = n
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closed thickening with radius zero is the closure of the set.  -/
Metric.cthickening_zero : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α), Metric.cthickening 0 E = closure E
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Ordering.swap.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 ()
-- Init.Data.List.Lemmas
List.append_inj_left : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- Equivalence relation on W-types that represent the same `Fix F`
value  -/
MvQPF.WEquiv : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → (MvQPF.P F).W α → (MvQPF.P F).W α → Prop
-- Init.System.IOError
_private.Init.System.IOError.0.IO.Error.downCaseFirst : String → String
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstr.h : Lean.Meta.Grind.Arith.Linear.EqCnstr → Lean.Meta.Grind.Arith.Linear.EqCnstrProof
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Zoomed.toRootOrdered : ∀ {α : Type u_1} {v : α} {cmp : α → α → Ordering} {path : RBTree.RBNode.Path α},
  RBTree.RBNode.Path.Zoomed (cmp v) path → RBTree.RBNode.Path.RootOrdered cmp path v
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.comp_tendsto : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β} {lb : Filter β} {g : β → γ},
  Filter.EventuallyConst g lb → Filter.Tendsto f l lb → Filter.EventuallyConst (g ∘ f) l
-- Mathlib.Algebra.Order.CauSeq.Completion
/-- A class stating that a ring with an absolute value is complete, i.e. every Cauchy
sequence has a limit.  -/
CauSeq.IsComplete : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [IsStrictOrderedRing α] → (β : Type u_2) → [inst_3 : Ring β] → (abv : β → α) → [IsAbsoluteValue abv] → Prop
-- Mathlib.Tactic.Linter.GlobalAttributeIn
/-- Gets the value of the `linter.globalAttributeIn` option.  -/
_private.Mathlib.Tactic.Linter.GlobalAttributeIn.0.Mathlib.Linter.globalAttributeInLinter.getLinterGlobalAttributeIn : Lean.Linter.LinterOptions → Bool
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.declaration.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenModifier.declaration = 1
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_mul_cancel_of_dvd : ∀ {a b : ℤ}, b ∣ a → a.fdiv b * b = a
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- A pair of morphisms `h : W ⟶ X` and `k : W ⟶ Y` satisfying `h ≫ f = k ≫ g` induces a morphism
`l : W ⟶ weakPullback f g` such that `l ≫ weakPullback.fst = h` and `l ≫ weakPullback.snd = k`.  -/
CategoryTheory.Limits.weakPullback.lift' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] →
            (h : W ⟶ X) →
              (k : W ⟶ Y) →
                CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g →
                  { l //
                    CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.weakPullback.fst f g) = h ∧
                      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.weakPullback.snd f g) = k }
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.formula1 : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.X✝ S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁✝ S) *
          (hζ.toInteger - 1) ^ (3 * FermatLastTheoremForThreeGen.Solution.multiplicity✝ S - 2) +
        FermatLastTheoremForThreeGen.Solution.Y✝ S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₂✝ S) *
            (hζ.toInteger - 1) *
          ↑⋯.unit +
      FermatLastTheoremForThreeGen.Solution.Z✝ S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃✝ S) *
          (hζ.toInteger - 1) *
        ↑⋯.unit ^ 2 =
    0
-- Mathlib.Logic.Function.Basic
eq_mpr_bijective : ∀ {α β : Sort u_3} (h : α = β), Function.Bijective h.mpr
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.nodup_aroots_minpoly : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsSeparable K L]
  (c : ConjRootClass K L), (c.minpoly.aroots L).Nodup
-- Lean.Elab.Tactic.Try
/-- Converts a declaration name into an identifier.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.toIdent : Lean.Name → Lean.MetaM Lean.Ident
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.quotKerTotalEquiv_apply : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (a : (S →₀ S) ⧸ (KaehlerDifferential.kerTotal R S).toAddSubgroup),
  (KaehlerDifferential.quotKerTotalEquiv R S) a =
    (QuotientAddGroup.lift (KaehlerDifferential.kerTotal R S).toAddSubgroup
        (Finsupp.linearCombination S ⇑(KaehlerDifferential.D R S)).toAddMonoidHom ⋯)
      a
-- Mathlib.Order.Lattice.Congruence
LatticeCon.r_inf_sup_iff : ∀ {α : Type u_2} [inst : Lattice α] (c : LatticeCon α) {x y : α}, c.toSetoid (x ⊓ y) (x ⊔ y) ↔ c.toSetoid x y
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
MeasureTheory.IntegrableOn.continuousWithinAt_Iic_primitive_Iio : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  {a₀ : ℝ},
  MeasureTheory.IntegrableOn f (Set.Iio a₀) μ →
    ContinuousWithinAt (fun b => ∫ (x : ℝ) in Set.Iio b, f x ∂μ) (Set.Iic a₀) a₀
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW.unshift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] {X₁ X₂ : C} {f : X₁ ⟶ X₂} {n : ℤ},
  P.trW ((CategoryTheory.shiftFunctor C n).map f) → P.trW f
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State.mk.injEq : ∀ (bottomUps higherOrders funBinders provideds : Array Bool) (namedArgs : Array Lean.Name)
  (bottomUps_1 higherOrders_1 funBinders_1 provideds_1 : Array Bool) (namedArgs_1 : Array Lean.Name),
  ({ bottomUps := bottomUps, higherOrders := higherOrders, funBinders := funBinders, provideds := provideds,
        namedArgs := namedArgs } =
      { bottomUps := bottomUps_1, higherOrders := higherOrders_1, funBinders := funBinders_1, provideds := provideds_1,
        namedArgs := namedArgs_1 }) =
    (bottomUps = bottomUps_1 ∧
      higherOrders = higherOrders_1 ∧ funBinders = funBinders_1 ∧ provideds = provideds_1 ∧ namedArgs = namedArgs_1)
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `Continuous.inv` -/
Continuous.fun_inv : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Inv G]
  [ContinuousInv G] {f : X → G}, Continuous f → Continuous fun i => (f i)⁻¹
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.hasLineDerivAt' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {s : Set E} {x v : E},
  HasLineDerivWithinAt 𝕜 f f' s x v → (∀ᶠ (t : 𝕜) in nhds 0, x + t • v ∈ s) → HasLineDerivAt 𝕜 f f' x v
-- Lean.Exception
/-- Return syntax object providing position information for the exception.
Recall that internal exceptions do not have position information.
 -/
Lean.Exception.getRef : Lean.Exception → Lean.Syntax
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.map_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
  [inst_2 : Fintype J] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] {f g : J → C} {h : (j : J) → f j ⟶ g j},
  CategoryTheory.Limits.biproduct.map h =
    ∑ j,
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j)
        (CategoryTheory.CategoryStruct.comp (h j) (CategoryTheory.Limits.biproduct.ι g j))
-- Mathlib.Algebra.Notation.Support
Function.compl_mulSupport : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M}, (Function.mulSupport f)ᶜ = {x | f x = 1}
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.FixedTermElab.toFixedTermElabRef : Lean.Elab.Term.FixedTermElab → Lean.Elab.Term.FixedTermElabRef
-- Mathlib.CategoryTheory.MorphismProperty.IsSmall
CategoryTheory.MorphismProperty.IsSmall.small_toSet : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : CategoryTheory.MorphismProperty.IsSmall.{w, v, u} W], Small.{w, max u v} ↑W.toSet
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.of_pow : ∀ {G : Type u_1} [inst : Monoid G] {a : G} {n : ℕ}, IsOfFinOrder (a ^ n) → n ≠ 0 → IsOfFinOrder a
-- Init.Data.BitVec.Lemmas
BitVec.zero_xor : ∀ {w : ℕ} {x : BitVec w}, 0#w ^^^ x = x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.norm_or_neg_norm_mem_spectrum : ∀ {A : Type u_1} [inst : CStarAlgebra A] [Nontrivial A] {a : A},
  autoParam (IsSelfAdjoint a) CStarAlgebra.norm_or_neg_norm_mem_spectrum._auto_1 →
    ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a
-- Init.Data.BitVec.Lemmas
BitVec.toFin_srem : ∀ {w : ℕ} {x y : BitVec w},
  (x.srem y).toFin =
    match x.msb, y.msb with
    | false, false => x.toFin % y.toFin
    | false, true => x.toFin % (-y).toFin
    | true, false => (-(-x % y)).toFin
    | true, true => (-(-x % -y)).toFin
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.eq_zero_iff_forall_coeff_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R},
  f = 0 ↔ ∀ (d : σ →₀ ℕ), (MvPowerSeries.coeff d) f = 0
-- Aesop.Tree.Data
Aesop.Rapp.mk : Aesop.RappData Aesop.Goal Aesop.MVarCluster → Aesop.Rapp
-- Init.Data.Vector.Lemmas
Vector.count_mk : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Array α} (h : xs.size = n) {a : α},
  Vector.count a (Vector.mk xs h) = Array.count a xs
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.integral_piecewise : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f g : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  [inst_6 : DecidablePred fun x => x ∈ s],
  MeasurableSet s →
    μ.IntegrableOn f s →
      μ.IntegrableOn g sᶜ →
        ∫ᵛ (x : X), s.piecewise f g x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X) in sᶜ, g x ∂[B; μ]
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α} {k : α},
  (t.insertManyIfNewUnit l)[k]! = ()
-- Init.Data.Array.Range
Array.range'_succ_left : ∀ {s n step : ℕ}, Array.range' (s + 1) n step = Array.map (fun x => x + 1) (Array.range' s n step)
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
SSet.prodStdSimplex.nonDegenerateEquiv₁_snd : ∀ {p : ℕ} (i : Fin (p + 1)), (↑(SSet.prodStdSimplex.nonDegenerateEquiv₁ i)).2 = SSet.stdSimplex.objMk₁ i.castSucc.succ
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Iio_of_Ico : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {b c : ι → α}
  {B : α},
  Filter.Tendsto b l (nhds B) →
    Filter.Tendsto c l Filter.atBot → MeasureTheory.AECover (μ.restrict (Set.Iio B)) l fun i => Set.Ico (c i) (b i)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Fintype σ] [inst_4 : DecidableEq σ],
  LinearMap.toMatrix' P.aevalDifferential = (MvPolynomial.aeval P.val).mapMatrix P.jacobiMatrix
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.mateEquiv_apply : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F}
  {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F}
  {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (α : CategoryTheory.TwoSquare G L₁ L₂ H),
  (CategoryTheory.mateEquiv adj₁ adj₂) α =
    CategoryTheory.TwoSquare.mk R₁ H G R₂
      (CategoryTheory.CategoryStruct.comp (R₁.comp G).rightUnitor.inv
        (CategoryTheory.CategoryStruct.comp ((R₁.comp G).whiskerLeft adj₂.unit)
          (CategoryTheory.CategoryStruct.comp (R₁.associator G (L₂.comp R₂)).hom
            (CategoryTheory.CategoryStruct.comp (R₁.whiskerLeft (G.associator L₂ R₂).inv)
              (CategoryTheory.CategoryStruct.comp (R₁.whiskerLeft (CategoryTheory.Functor.whiskerRight α.natTrans R₂))
                (CategoryTheory.CategoryStruct.comp (R₁.whiskerLeft (L₁.associator H R₂).hom)
                  (CategoryTheory.CategoryStruct.comp (R₁.associator L₁ (H.comp R₂)).inv
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight adj₁.counit (H.comp R₂))
                      (H.comp R₂).leftUnitor.hom))))))))
-- Lean.Setup
Lean.Import.mk.inj : ∀ {module : Lean.Name} {importAll isExported isMeta : Bool} {module_1 : Lean.Name}
  {importAll_1 isExported_1 isMeta_1 : Bool},
  { module := module, importAll := importAll, isExported := isExported, isMeta := isMeta } =
      { module := module_1, importAll := importAll_1, isExported := isExported_1, isMeta := isMeta_1 } →
    module = module_1 ∧ importAll = importAll_1 ∧ isExported = isExported_1 ∧ isMeta = isMeta_1
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Notation for the monoidal `associator`: `(X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)`  -/
CategoryTheory.MonoidalCategory.termα_ : Lean.ParserDescr
-- Mathlib.Topology.Order.LeftRightLim
Monotone.rightLim_le : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f → ∀ {x y : α}, x < y → Function.rightLim f x ≤ f y
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.ofCommaObject_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (c : CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D)))
  {X Y : CategoryTheory.WithInitial C} (f : X ⟶ Y),
  (CategoryTheory.WithInitial.ofCommaObject c).map f =
    match X, Y, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f =>
      c.right.map (CategoryTheory.WithInitial.down f)
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => c.hom.app a
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id c.left
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- Every edge in a walk's edge list is an edge of the graph.
It is written in this form (rather than using `⊆`) to avoid unsightly coercions.  -/
SimpleGraph.Walk.edges_subset_edgeSet : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) ⦃e : Sym2 V⦄, e ∈ p.edges → e ∈ G.edgeSet
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.size.eq_1 : ∀ {α : Type u} [inst : Std.Rxo.HasSize α] [inst_1 : Std.PRange.Least? α] (r : Std.Rio α),
  r.size =
    match Std.PRange.least? with
    | none => 0
    | some least => Std.Rxo.HasSize.size least r.upper
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- When the representation on `A` is trivial, then `H⁰(G, A)` is all of `A.`  -/
groupCohomology.H0IsoOfIsTrivial : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → [A.IsTrivial] → groupCohomology.H0 A ≅ ModuleCat.of k ↑A
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.not_le_norm' : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α]
  (ctx : Lean.Grind.Linarith.Context α) (lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.norm_cert lhs rhs p = true →
    ¬Lean.Grind.Linarith.Expr.denote ctx lhs ≤ Lean.Grind.Linarith.Expr.denote ctx rhs →
      ¬Lean.Grind.Linarith.Poly.denote' ctx p ≤ 0
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flipFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (K : HomologicalComplex₂ C c₁ c₂),
  (HomologicalComplex₂.flipFunctor C c₁ c₂).obj K = K.flip
-- Init.Data.Int.Gcd
Int.pow_lcm_pow : ∀ {n m : ℤ} {k : ℕ}, (n ^ k).lcm (m ^ k) = n.lcm m ^ k
-- Mathlib.NumberTheory.Primorial
squarefree_primorial : ∀ (n : ℕ), Squarefree (primorial n)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- if `f` is integrable, then `g + f` is integrable iff `g` is.
See `integrable_add_iff_integrable_left'` for the same statement with `fun x ↦ g x + f x` instead
of `g + f`.  -/
MeasureTheory.integrable_add_iff_integrable_left : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g : α → β}, MeasureTheory.Integrable f μ → (MeasureTheory.Integrable (g + f) μ ↔ MeasureTheory.Integrable g μ)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.cyclotomic_pos_and_nonneg : ∀ (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] (x : R),
  (1 < x → 0 < Polynomial.eval x (Polynomial.cyclotomic n R)) ∧
    (1 ≤ x → 0 ≤ Polynomial.eval x (Polynomial.cyclotomic n R))
-- Mathlib.Data.Multiset.Range
Multiset.mem_range : ∀ {m n : ℕ}, m ∈ Multiset.range n ↔ m < n
-- Mathlib.Combinatorics.Colex
Finset.Colex.cons_le_cons : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a b : α} (ha : a ∉ s) (hb : b ∉ s),
  toColex (Finset.cons a s ha) ≤ toColex (Finset.cons b s hb) ↔ a ≤ b
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.norm_lift_apply_le : ∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  {S : AddSubgroup M} (f : NormedAddGroupHom M N) (hf : ∀ x ∈ S, f x = 0) (x : M ⧸ S),
  ‖(QuotientAddGroup.lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖