mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instIsSubApply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N], IsSubApply (QuadraticMap R M N) M N
-- Lean.Parser.Types
/-- Input context derived from elaboration of previous commands.  -/
Lean.Parser.ParserModuleContext : Type
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.equivOfEq_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S T : Subalgebra R A)
  (h : S = T) (x : ↥S), (S.equivOfEq T h) x = ⟨↑x, ⋯⟩
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.continuousOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X}, HolderOnWith C r f s → 0 < r → ContinuousOn f s
-- Mathlib.Logic.Equiv.Basic
/-- This lemma is impractical to state in the dependent case.  -/
Equiv.piCongrLeft'_symm : ∀ {α : Sort u_1} {β : Sort u_4} (P : Sort u_9) (e : α ≃ β),
  (Equiv.piCongrLeft' (fun x => P) e).symm = Equiv.piCongrLeft' (fun a => P) e.symm
-- Aesop.Forward.LevelIndex
Aesop.instHashableLevelIndex.hash : Aesop.LevelIndex → UInt64
-- Plausible.Testable
/-- Applicative combinator proof carrying test results.  -/
Plausible.TestResult.combine : {p q : Prop} → Unit ⊕' (p → q) → Unit ⊕' p → Unit ⊕' q
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_congr : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f g : α → M},
  Set.EqOn f g s → s.mulIndicator f = s.mulIndicator g
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.IsKolmogorovProcess_mk : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  (h : ProbabilityTheory.IsAEKolmogorovProcess X P p q M),
  ProbabilityTheory.IsKolmogorovProcess (ProbabilityTheory.IsAEKolmogorovProcess.mk X h) P p q M
-- Init.Data.AC
Lean.Data.AC.Context.mergeIdem_head2 : ∀ {x y : ℕ} {ys : List ℕ}, x ≠ y → Lean.Data.AC.mergeIdem (x :: y :: ys) = x :: Lean.Data.AC.mergeIdem (y :: ys)
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- Volume on a 1-dimensional real vector space is equivalent to a scaled volume on ℝ.  -/
MeasureTheory.volume_eq_of_finrank_eq_one : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E],
  Module.finrank ℝ E = 1 →
    ∀ {v : E}, v ≠ 0 → MeasureTheory.volume = ‖v‖ₑ • MeasureTheory.Measure.map (fun x => x • v) MeasureTheory.volume
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.instT3Space : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal]
  [hN : IsClosed ↑N], T3Space (G ⧸ N)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_ne_zero_eval_zero : ∀ (S : Type u) [inst : Semiring S] {n : ℕ}, n ≠ 0 → Polynomial.eval 0 (ascPochhammer S n) = 0
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_of_lcm_left_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c : α}, lcm a b ∣ c → b ∣ c
-- Init.Data.SInt.Bitwise
Int8.and_comm : ∀ (a b : Int8), a &&& b = b &&& a
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminator : Type
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.r_pos : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal}, HasFPowerSeriesOnBall f p x r → 0 < r
-- Lean.Meta.Constructions.SparseCasesOn
/-- This module creates sparse variants of `casesOn` that have arms only for some of the constructors,
offering a catch-all.

The minor arguments come in the order of the given `ctors` array.

The catch-all provides a `Nat.hasNotBit mask x.ctorIdx` hypothesis to express that these constructors
were not matched. Using a single hypothesis like this, rather than many hypotheses of the form
`x.ctorIdx ≠ i`, is important to avoid quadratic overhead in code like match splitter generation.

This function is implemented with a simple call to `.rec`, i.e. no clever branching on the constructor
index. The compiler has native support for these sparse matches anyways, and kernel reduction would
not benefit from a more sophisticated implementation unless it has itself native support for
`.ctorIdx` and constructor elimination functions.
 -/
Lean.Meta.mkSparseCasesOn : Lean.Name → Array Lean.Name → Lean.MetaM Lean.Name
-- Init.Data.Vector.Basic
/-- Custom eliminator for `Vector α n` through `Array α`  -/
Vector.elimAsArray : {α : Type u_1} →
  {n : ℕ} →
    {motive : Vector α n → Sort u} →
      ((xs : Array α) → (ha : xs.size = n) → motive (Vector.mk xs ha)) → (xs : Vector α n) → motive xs
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.FindSplitImpl.visit : Lean.Expr → OptionT Lean.Meta.FindSplitImpl.FindM Lean.Expr
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_abs : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : ℤ}, ↑|a| = |↑a|
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₂ → (t₁ ∩ t₂).get! k = default
-- Mathlib.Analysis.Normed.Group.Continuity
Filter.Tendsto.nnnorm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] {a : E} {l : Filter α} {f : α → E},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => ‖f x‖₊) l (nhds ‖a‖₊)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_himp : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α}, ↑(U ⇨ V) = interior (↑U ⇨ ↑V)
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- The conjugate transpose of a Hadamard matrix is Hadamard.  -/
Matrix.IsHadamard.conjTranspose : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  {A : Matrix n n R}, A.IsHadamard → A.conjTranspose.IsHadamard
-- Mathlib.Algebra.Polynomial.Bivariate
/-- `evalEval x y` as a ring homomorphism.  -/
Polynomial.evalEvalRingHom : {R : Type u_1} → [inst : CommSemiring R] → R → R → Polynomial (Polynomial R) →+* R
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
/-- The sigmoid function from `ℝ` to `ℝ`.  -/
Real.sigmoid : ℝ → ℝ
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_right_comm : ∀ {a b c : ENNReal}, a / b / c = a / c / b
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_le_sup : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G), ⁅H₁, H₂⁆ ≤ H₁ ⊔ H₂
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.forget₂Mon_obj_X : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (R : CategoryTheory.RingObjCat C),
  ((CategoryTheory.RingObjCat.forget₂Mon C).obj R).X = R.X
-- Mathlib.Data.Set.Basic
Set.powerset_univ : ∀ {α : Type u}, 𝒫 Set.univ = Set.univ
-- Lean.Elab.Tactic.Omega.Frontend
/-- Apply a rewrite rule to an expression, and interpret the result as a `LinearCombo`.
(We're not rewriting any subexpressions here, just the top level, for efficiency.)
 -/
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.asLinearComboImpl.rewrite : Lean.Expr →
  Lean.Expr →
    Lean.Elab.Tactic.Omega.OmegaM (Lean.Omega.LinearCombo × Lean.Elab.Tactic.Omega.OmegaM Lean.Expr × List Lean.Expr)
-- Mathlib.Order.Heyting.Basic
sdiff_inf_self_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a \ (a ⊓ b) = a \ b
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.instInhabitedSymExtension : {a : Type} → Inhabited (Lean.Meta.Sym.SymExtension a)
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.setLIntegral_preimage_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {s : Set Ω} {t : Set β},
  Measurable X →
    AEMeasurable Y μ →
      MeasurableSet s →
        MeasurableSet t →
          ∫⁻ (a : α) in X ⁻¹' t, ((ProbabilityTheory.condDistrib Y X μ) (X a)) s ∂μ = μ (X ⁻¹' t ∩ Y ⁻¹' s)
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorInt64 : LawfulXor Int64
-- Init.Data.SInt.Lemmas
Int16.toNat_toBitVec : ∀ (x : Int16), x.toBitVec.toNat = x.toUInt16.toNat
-- Mathlib.Order.Interval.Finset.Nat
Nat.multiset_Ico_map_mod : ∀ (n a : ℕ), Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = Multiset.range a
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddCommGrpCat.FilteredColimits.forget₂AddGroup_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)
-- Mathlib.Order.Filter.NAry
Filter.map_map₂_antidistrib : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {m : α → β → γ}
  {f : Filter α} {g : Filter β} {n : γ → δ} {m' : β' → α' → δ} {n₁ : β → β'} {n₂ : α → α'},
  (∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)) →
    Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' (Filter.map n₁ g) (Filter.map n₂ f)
-- Mathlib.Algebra.Ring.Equiv
/-- A ring isomorphism sends one to one.  -/
RingEquiv.map_one : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S), f 1 = 1
-- Mathlib.Order.Extension.Well
/-- "Identity" equivalence between a well-founded order and its well-order extension.  -/
toWellOrderExtension : {α : Type u} → α ≃ WellOrderExtension α
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_tensorHom_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C}
  [inst_3 : X₁.HasTensor X₂] [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃]
  [inst_5 : Y₁.HasTensor Y₂] [inst_6 : (CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃]
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) {Z : C}
  (h_1 :
    CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂) Y₃ j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ f₂) f₃ j)
        h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (f₁ i₁) (f₂ i₂))
        (f₃ i₃))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h) h_1)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.action : Lean.Syntax → Lean.Elab.Term.Do.Code
-- Mathlib.Order.Comparable
IncompRel.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (a b : α), IncompRel r a b = (¬r a b ∧ ¬r b a)
-- Init.Data.Slice.List.Lemmas
List.size_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.size (Std.Rco.Sliceable.mkSlice xs lo...hi) = min hi xs.length - lo
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
HasStrictDerivAt.to_local_left_inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜},
  HasStrictDerivAt f f' a → f' ≠ 0 → ∀ {g : 𝕜 → 𝕜}, (∀ᶠ (x : 𝕜) in nhds a, g (f x) = x) → HasStrictDerivAt g f'⁻¹ (f a)
-- Mathlib.Dynamics.OmegaLimit
/-- An element `y` is in the ω-limit set of `s` w.r.t. `f` if the
preimages of an arbitrary neighbourhood of `y` frequently (w.r.t. `f`) intersects of `s`.  -/
mem_omegaLimit_iff_frequently : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  (y : β), y ∈ omegaLimit f ϕ s ↔ ∀ n ∈ nhds y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty
-- Lean.Parser.Term
Lean.Parser.Term.dynamicQuot : Lean.Parser.Parser
-- Init.Data.Rat.Basic
Rat.instLT : LT ℚ
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMapₛₗ₂'_toMatrix' : ∀ {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring R₁]
  [inst_4 : Semiring R₂] [inst_5 : Semiring S₁] [inst_6 : Semiring S₂] [inst_7 : Module S₁ N₂] [inst_8 : Module S₂ N₂]
  [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂] [inst_11 : SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁)
  (σ₂ : R₂ →+* S₂) [inst_12 : Fintype n] [inst_13 : Fintype m] [inst_14 : DecidableEq n] [inst_15 : DecidableEq m]
  (B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂), (Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) ((LinearMap.toMatrixₛₗ₂' R) B) = B
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- **Alias** of the reverse direction of `differentiableWithinAt_insert_self`. -/
DifferentiableWithinAt.insert : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 f (insert x s) x
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
stronglyMeasurable_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [CompleteSpace F] [inst_4 : MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜]
  [h : SecondCountableTopologyEither 𝕜 F] (f : 𝕜 → F), MeasureTheory.StronglyMeasurable (deriv f)
-- Mathlib.Order.Hom.CompleteLattice
/-- The underlying function of an `sInfHom`.  -/
sInfHom.toFun : {α : Type u_8} → {β : Type u_9} → [inst : InfSet α] → [inst_1 : InfSet β] → sInfHom α β → α → β
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.coe_eq_univ : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, ↑H = Set.univ ↔ H = ⊤
-- Mathlib.Data.PNat.Factors
/-- Factoring gives a homomorphism from the multiplicative
monoid ℕ+ to the additive monoid of multisets.  -/
PNat.factorMultiset_one : PNat.factorMultiset 1 = 0
-- Mathlib.Algebra.Group.Invertible.Defs
mul_right_eq_iff_eq_mul_invOf : ∀ {α : Type u} [inst : Monoid α] {a b c : α} [inst_1 : Invertible c], a * c = b ↔ a = b * ⅟c
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.Opens.IsBasis.isOpenCover : ∀ {X : Type u_3} [inst : TopologicalSpace X] {S : Set (TopologicalSpace.Opens X)},
  TopologicalSpace.Opens.IsBasis S → TopologicalSpace.IsOpenCover fun U => ↑U
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.dvd_of_mem_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {p a : α},
  p ∈ UniqueFactorizationMonoid.factors a → p ∣ a
-- Mathlib.Algebra.Category.Grp.LeftExactFunctor
/-- Implementation, see `leftExactFunctorForgetEquivalence`.
This is the complicated bit, where we show that forgetting the group structure in the image of
`F` and then reconstructing it recovers the group structure we started with.  -/
AddCommGrpCat.leftExactFunctorForgetEquivalence.unitIsoAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] →
        (F : CategoryTheory.Functor C AddCommGrpCat) →
          [inst_3 : CategoryTheory.Limits.PreservesFiniteLimits F] →
            (X : C) →
              commGrpTypeEquivalenceCommGrp.inverse.obj (AddCommGrpCat.toCommGrp.obj (F.obj X)) ≅
                (F.comp (CategoryTheory.forget AddCommGrpCat)).mapCommGrp.obj
                  (CategoryTheory.Preadditive.commGrpEquivalence.functor.obj X)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The natural transformation `t.eTruncGE.obj b ⟶ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b`
for all `a` and `b` in `EInt`.  -/
CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE : {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) →
                (a b : EInt) → t.eTruncGE.obj b ⟶ (t.eTruncGE.obj a).comp (t.eTruncGE.obj b)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.det : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {n : Type u_5}
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] {M : Matrix n n A},
  (∀ (i j : n), IsIntegral R (M i j)) → IsIntegral R M.det
-- Mathlib.RingTheory.Morita.Matrix
/-- The natural isomorphism showing that `toMatrixModCat` is the right inverse of `toModuleCat`.  -/
MatrixModCat.counitIso : (R : Type u) →
  {ι : Type v} →
    [inst : Ring R] →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] →
          (i : ι) →
            (MatrixModCat.toModuleCat R i).comp (ModuleCat.toMatrixModCat R ι) ≅
              CategoryTheory.Functor.id (ModuleCat (Matrix ι ι R))
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Algebra.adjoin.powerBasis'.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x : S}
  (hx : IsIntegral R x), Algebra.adjoin.powerBasis' hx = Algebra.adjoin.powerBasis' hx
-- Lean.AddDecl
_private.Lean.AddDecl.0.Lean.addDeclCore.addAsAxiom : Lean.Declaration → Lean.CoreM Unit
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.visitAtom : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.OrderOfElement
orderOf_eq_orderOf_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {H : Type u_6} [inst_1 : Monoid H] {y : H},
  orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_eq_get!_get? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} [inst_3 : Inhabited (β a)], m.get! a = (m.get? a).get!
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMap_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology]
  [inst_4 : S₃.HasRightHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃),
  CategoryTheory.ShortComplex.rightHomologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ₁)
      (CategoryTheory.ShortComplex.rightHomologyMap φ₂)
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.FG.cg : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M],
  FirstOrder.Language.Structure.FG L M → FirstOrder.Language.Structure.CG L M
-- Mathlib.Data.ZMod.Basic
ZModModule.add_add_add_cancel : ∀ {G : Type u_2} [inst : AddCommGroup G] [Module (ZMod 2) G] (x y z : G), x + y + (y + z) = x + z
-- Mathlib.Combinatorics.Additive.Energy
Finset.card_sq_le_card_mul_mulEnergy : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] (s t u : Finset α),
  {xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u}.card ^ 2 ≤ u.card * s.mulEnergy t
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.IsStandardSmoothOfRelativeDimension.id : ∀ (R : Type u) [inst : CommRing R], RingHom.IsStandardSmoothOfRelativeDimension 0 (RingHom.id R)
-- Init.Data.Vector.Attach
Vector.getElem?_attachWith : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {P : α → Prop} {H : ∀ a ∈ xs, P a},
  (xs.attachWith P H)[i]? = Option.pmap Subtype.mk xs[i]? ⋯
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- For every `n ∈ ℕ` and every ideal `I`, `val_v(I^n) = n*val_v(I)`.  -/
FractionalIdeal.count_pow : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℕ)
  (I : FractionalIdeal (nonZeroDivisors R) K), FractionalIdeal.count K v (I ^ n) = ↑n * FractionalIdeal.count K v I
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSum_isBasis_iff : ∀ {α : Type u_1} {M N : Matroid α} {h : Disjoint M.E N.E} {I X : Set α},
  (M.disjointSum N h).IsBasis I X ↔
    M.IsBasis (I ∩ M.E) (X ∩ M.E) ∧ N.IsBasis (I ∩ N.E) (X ∩ N.E) ∧ I ⊆ X ∧ X ⊆ M.E ∪ N.E
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_natCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) [inst_3 : NatCast F] (n : ℕ), HasDerivAt (↑n) 0 x
-- Lean.Server.Completion.CompletionUtils
_private.Lean.Server.Completion.CompletionUtils.0.Lean.Server.Completion.getDotCompletionTypeNames.visit : Lean.Expr → StateRefT' IO.RealWorld (Array Lean.Name) Lean.MetaM Unit
-- Mathlib.Algebra.BigOperators.Fin
finFunctionFinEquiv_single : ∀ {m n : ℕ} [inst : NeZero m] (i : Fin n) (j : Fin m), ↑(finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i
-- Mathlib.Analysis.Normed.Lp.PiLp
instCoeFunPiLpForall : (p : ENNReal) → {ι : Type u_1} → (α : ι → Type u_2) → CoeFun (PiLp p α) fun x => (i : ι) → α i
-- Mathlib.Order.Monotone.Monovary
Monovary.dual_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Monovary f g → Antivary (⇑OrderDual.toDual ∘ f) g
-- Mathlib.RingTheory.LocalRing.Pullback
AlgHom.pullback_comm_sq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] C) (g : B →ₐ[R] C), f.comp (f.pullbackFst g) = g.comp (f.pullbackSnd g)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_const' : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  [CompleteSpace E] (c : E), ∫ (x : ℝ) in a..b, c ∂μ = (μ.real (Set.Ioc a b) - μ.real (Set.Ioc b a)) • c
-- Init.Core
/-- `x != y` is boolean not-equal. It is the negation of `x == y` which is supplied by
the `BEq` typeclass.

Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead of
`Prop` valued. It is mainly intended for programming applications.


Conventions for notations in identifiers:

 * The recommended spelling of `!=` in identifiers is `bne`. -/
bne : {α : Type u} → [BEq α] → α → α → Bool
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.CategoryWithCofibrations.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → HomotopicalAlgebra.CategoryWithCofibrations C