mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {b c d : α}, min c d ≤ b → Set.Iic b ∪ Set.Icc c d = Set.Iic (max b d)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.finsetSum_apply : ∀ {α : Type u_1} {ι : Type u_2} {N : Type u_10} [inst : AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) (a : α),
  (∑ i ∈ S, f i) a = ∑ i ∈ S, (f i) a
-- Mathlib.Algebra.Group.Submonoid.Units
/-- An additive subgroup of additive units represented as an additive submonoid of `M`.  -/
AddSubgroup.ofAddUnits : {M : Type u_1} → [inst : AddMonoid M] → AddSubgroup (AddUnits M) → AddSubmonoid M
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.of_subsingleton : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X}, s.Subsingleton → Convexity.IsConvexSet R s
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The object `⦋0⦌` is terminal in `SimplexCategory`.  -/
SimplexCategory.isTerminalZero : CategoryTheory.Limits.IsTerminal { len := 0 }
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
/-- Given a fibered category `p : 𝒳 ⥤ 𝒫`, a morphism `f : R ⟶ S` and an object `a` lying over `S`,
then `pullbackObj` is the domain of some choice of a Cartesian morphism lying over `f` with
codomain `a`.  -/
CategoryTheory.Functor.IsPreFibered.pullbackObj : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} → [p.IsPreFibered] → {R S : 𝒮} → {a : 𝒳} → p.obj a = S → (R ⟶ S) → 𝒳
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.mean_union_eq_add_of_disjoint : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X},
  IsAddFoelner G μ (↑u) F →
    ∀ (s t : Set X),
      MeasurableSet t →
        Disjoint s t → IsAddFoelner.mean μ u F (s ∪ t) = IsAddFoelner.mean μ u F s + IsAddFoelner.mean μ u F t
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
Filter.EventuallyEq.contMDiffWithinAt_iff : ∀ {𝕜 : 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'] {f f₁ : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞},
  f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → (ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x)
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
linearIndepOn_of_finite : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (s : Set ι), (∀ t ⊆ s, t.Finite → LinearIndepOn R v t) → LinearIndepOn R v s
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β} {u : Finset α},
  s -ᵥ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x -ᵥ y ∈ u
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofSubset_parts : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a b : α} (P : Finpartition a) {parts : Finset α}
  (subset : parts ⊆ P.parts) (sup_parts : parts.sup id = b), (P.ofSubset subset sup_parts).parts = parts
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instPartialOrder.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M], Submonoid.instPartialOrder = PartialOrder.ofSetLike (Submonoid M) M
-- Mathlib.Topology.Separation.Regular
T3Space.toRegularSpace : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T3Space X], RegularSpace X
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_def' : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G) [H₁.Normal] [H₂.Normal],
  ⁅H₁, H₂⁆ = Subgroup.normalClosure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.zmultiples_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] {g : G}, AddSubgroup.zmultiples g = ⊥ ↔ g = 0
-- Mathlib.Algebra.Group.Equiv.Defs
AddHom.toAddEquiv_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (g : N →ₙ+ M)
  (h₁ : g.comp f = AddHom.id M) (h₂ : f.comp g = AddHom.id N), ⇑(f.toAddEquiv g h₁ h₂).symm = ⇑g
-- Mathlib.Order.Hom.Lattice
/-- Reinterpret an order homomorphism to a linear order as a `LatticeHom`.  -/
OrderHomClass.toLatticeHom : {F : Type u_1} →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : LinearOrder α] → [inst_2 : Lattice β] → [OrderHomClass F α β] → F → LatticeHom α β
-- Init.Data.SInt.Bitwise
ISize.toBitVec_not : ∀ {a : ISize}, (~~~a).toBitVec = ~~~a.toBitVec
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.ω_pow_formula : ∀ (p' : ℕ),
  lucasLehmerResidue (p' + 2) = 0 →
    ∃ k, LucasLehmer.X.ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * LucasLehmer.X.ω ^ 2 ^ p' - 1
-- Mathlib.Algebra.Group.Indicator
Set.indicator_add_eq_right : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] {f g : α → M},
  Disjoint (Function.support f) (Function.support g) → (Function.support g).indicator (f + g) = g
-- Mathlib.Data.DFinsupp.Sigma
/-- The natural bijection between `Π₀ (i : Σ i, α i), δ i.1 i.2` and `Π₀ i (j : α i), δ i j`.

This is the dfinsupp version of `Equiv.piCurry`.  -/
DFinsupp.sigmaCurryEquiv : {ι : Type u} →
  {α : ι → Type u_2} →
    {δ : (i : ι) → α i → Type v} →
      [DecidableEq ι] →
        [inst : (i : ι) → (j : α i) → Zero (δ i j)] →
          (Π₀ (i : (x : ι) × α x), δ i.fst i.snd) ≃ Π₀ (i : ι) (j : α i), δ i j
-- Mathlib.Order.Filter.Prod
Filter.coprod_neBot_left : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} [f.NeBot] [Nonempty β], (f.coprod g).NeBot
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        {S : Type u_3} →
          [inst_2 : Field K] →
            [inst_3 : CommSemiring S] →
              [inst_4 : Algebra R K] →
                [inst_5 : IsFractionRing R K] →
                  (v : IsDedekindDomain.HeightOneSpectrum R) →
                    [Algebra S K] → Algebra S (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.Analysis.Calculus.FDeriv.Defs
fderivWithin_univ : ∀ {𝕜 : 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}, fderivWithin 𝕜 f Set.univ = fderiv 𝕜 f
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- Choose a partial isomorphism witnessing that `X` and `Y` are birational.  -/
AlgebraicGeometry.Scheme.Birational.partialIso : {X Y : AlgebraicGeometry.Scheme} → X.Birational Y → X.PartialIso Y
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- The embedding of the category of `κ`-directed
partially ordered types in the category of partially
ordered types.  -/
CategoryTheory.CardinalDirectedPoset.ι : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] → CategoryTheory.Functor (CategoryTheory.CardinalDirectedPoset κ) PartOrdEmb
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.fun_neg : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E],
  ProbabilityTheory.HasGaussianLaw X P → ProbabilityTheory.HasGaussianLaw (fun ω => -X ω) P
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.mem_sInf : ∀ {M : Type u_1} [inst : Add M] {S : Set (AddSubsemigroup M)} {x : M}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofLeftInverse_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₁] M} [inst_4 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_5 : RingHomInvPair σ₂₁ σ₁₂] (h : Function.LeftInverse ⇑g ⇑f) (x : ↥f.range),
  (LinearEquiv.ofLeftInverse h).symm x = g ↑x
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.weakFEPair_f₀ : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : ModularFormClass F Γ k],
  (ModularForm.weakFEPair hk f).f₀ = UpperHalfPlane.valueAtInfty ⇑f
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given two lines intersecting at a common point lying strictly between the defining points on
each line. Fixing one point from each line as the endpoints, choosing either remaining point as the
vertex yields oriented angles with the same sign.  -/
Sbtw.oangle_sign_eq_of_sbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ p₄ : P},
  Sbtw ℝ p₁ p p₃ → Sbtw ℝ p₂ p p₄ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₃ p₂).sign
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1CoresCoinfOfTrivial_X₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal]
  [inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)],
  (groupHomology.H1CoresCoinfOfTrivial A S).X₁ = groupHomology.H1 (Rep.res S.subtype A)
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer.eq_1 : ∀ (R : Type u) [inst : Ring R], descPochhammer R 0 = 1
-- Mathlib.Topology.UniformSpace.Matrix
Matrix.instIsUniformAddGroup : ∀ (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [inst : UniformSpace 𝕜] [inst_1 : AddGroup 𝕜] [IsUniformAddGroup 𝕜],
  IsUniformAddGroup (Matrix m n 𝕜)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctorAssociatorX_hom_D₂ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] [inst_9 : CategoryTheory.Preadditive C₁₂]
  [inst_10 : CategoryTheory.Preadditive C₂₃] [inst_11 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_12 : F₁₂.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_14 : G.Additive]
  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [inst_16 : G₂₃.PreservesZeroMorphisms]
  [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_18 : F.PreservesZeroMorphisms]
  [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7}
  {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_20 : DecidableEq ι₄]
  {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃)
  (c₄ : ComplexShape ι₄) [inst_21 : TotalComplexShape c₁ c₂ c₁₂] [inst_22 : TotalComplexShape c₁₂ c₃ c₄]
  [inst_23 : TotalComplexShape c₂ c₃ c₂₃] [inst_24 : TotalComplexShape c₁ c₂₃ c₄], ⋯
-- Mathlib.Order.RelClasses
/-- Set notation form of `ge_antisymm` -/
superset_antisymm : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, b ⊆ a → a ⊆ b → a = b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.getKey? (t.minKey he) = some (t.minKey he)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isDetector_iff_reflectsIsomorphisms_coyoneda_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsDetector G ↔ (CategoryTheory.coyoneda.obj (Opposite.op G)).ReflectsIsomorphisms
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_eq_none : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α}, a ∉ m → m.get? a = none
-- Mathlib.Analysis.Calculus.TangentCone.Seq
mem_tangentConeAt_of_pow_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} {x y : E} {r : 𝕜},
  r ≠ 0 → ‖r‖ < 1 → (∀ᶠ (n : ℕ) in Filter.atTop, x + r ^ n • y ∈ s) → y ∈ tangentConeAt 𝕜 s x
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongrLeft_apply_snd : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (ab : β₁ × α₁),
  ((Equiv.prodCongrLeft e) ab).2 = ab.2
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Equivalence.CommShift.instCommShiftInverseSymm : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (E : C ≌ D) →
          (A : Type u_3) →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] → [E.functor.CommShift A] → E.symm.inverse.CommShift A
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instZeroCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → Zero (CauSeq.Completion.Cauchy abv)
-- Init.Data.UInt.Bitwise
UInt16.toUSize_xor : ∀ (a b : UInt16), (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize
-- Mathlib.GroupTheory.Order.Min
/-- The minimum order of a non-identity element. Also the minimum size of a nontrivial
subgroup, see `AddMonoid.le_minOrder_iff_forall_addSubgroup`. Returns `∞` if the monoid is
torsion-free.  -/
AddMonoid.minOrder : (α : Type u_2) → [AddMonoid α] → ℕ∞
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.fork_π_app_zero : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g],
  (CategoryTheory.Limits.equalizer.fork f g).π.app CategoryTheory.Limits.WalkingParallelPair.zero =
    CategoryTheory.Limits.equalizer.ι f g
-- Mathlib.Data.Seq.Basic
Stream'.Seq.dropn_tail : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ), s.tail.drop n = s.drop (n + 1)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.Adj.degree_pos_left : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V} [inst : Fintype ↑(G.neighborSet v)] {w : V}, G.Adj v w → 0 < G.degree v
-- Mathlib.Data.Set.Semiring
SetSemiring.instAdd : {α : Type u_1} → Add (SetSemiring α)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedSimprocOLeanEntry : Inhabited Lean.Meta.Simp.SimprocOLeanEntry
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The canonical `S`-algebra inclusion `R → TrivSqZeroExt R M`.  -/
TrivSqZeroExt.inlAlgHom : (S : Type u_1) →
  (R : Type u) →
    (M : Type v) →
      [inst : CommSemiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra S R] →
              [inst_4 : Module S M] →
                [inst_5 : Module R M] →
                  [inst_6 : Module Rᵐᵒᵖ M] →
                    [inst_7 : SMulCommClass R Rᵐᵒᵖ M] →
                      [inst_8 : IsScalarTower S R M] → [inst_9 : IsScalarTower S Rᵐᵒᵖ M] → R →ₐ[S] TrivSqZeroExt R M
-- Mathlib.Order.Interval.Set.Monotone
/-- A function `ψ` on a `SuccOrder` is strictly monotone before some `n` if for all `m` such that
`m < n`, we have `ψ m < ψ (succ m)`.  -/
strictMonoOn_Iic_of_lt_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {ψ : α → β} [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {n : α}, (∀ m < n, ψ m < ψ (Order.succ m)) → StrictMonoOn ψ (Set.Iic n)
-- Lean.Data.Json.Basic
Lean.JsonNumber.lt : Lean.JsonNumber → Lean.JsonNumber → Bool
-- Mathlib.Algebra.Lie.Extension
/-- The equivalence from the kernel of the projection.  -/
LieAlgebra.IsExtension.kerEquivRange : {R : Type u_1} →
  {N : Type u_2} →
    {L : Type u_3} →
      {M : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : LieRing N] →
                [inst_4 : LieAlgebra R N] →
                  [inst_5 : LieRing M] →
                    [inst_6 : LieAlgebra R M] →
                      (i : N →ₗ⁅R⁆ L) → (p : L →ₗ⁅R⁆ M) → [LieAlgebra.IsExtension i p] → ↥p.ker ≃ₗ[R] ↥i.range
-- Init.Data.BitVec.Bootstrap
BitVec.toNat_append : ∀ {m n : ℕ} (x : BitVec m) (y : BitVec n), (x ++ y).toNat = x.toNat <<< n ||| y.toNat
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_mem_convexHull : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {s : Set E} [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (t : Finset ι) {w : ι → R},
  (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → ∀ {z : ι → E}, (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ (convexHull R) s
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Functor.mapHomologicalComplex_map_f : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂)
  [inst_4 : F.PreservesZeroMorphisms] (c : ComplexShape ι) {X Y : HomologicalComplex W₁ c} (f : X ⟶ Y) (i : ι),
  ((F.mapHomologicalComplex c).map f).f i = F.map (f.f i)
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_ne_zero : ∀ {c : Cardinal.{u}}, Cardinal.toNat c ≠ 0 ↔ c ≠ 0 ∧ c < Cardinal.aleph0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₂ → k ∈ m₁
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M`, the Localization of `M` at the Submonoid generated by `x`, as a quotient.  -/
AddLocalization.Away : {M : Type u_1} → [AddCommMonoid M] → M → Type u_1
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.clear.injEq : ∀ (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ')
  (p_1 : Turing.PartrecToTM2.Γ' → Bool) (k_1 : Turing.PartrecToTM2.K') (q_1 : Turing.PartrecToTM2.Λ'),
  (Turing.PartrecToTM2.Λ'.clear p k q = Turing.PartrecToTM2.Λ'.clear p_1 k_1 q_1) = (p = p_1 ∧ k = k_1 ∧ q = q_1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.PRange.LawfulUpwardEnumerable α], r.isEmpty = true ↔ ∀ (a : α), a ∉ r
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypicOfType.isIsotypic : ∀ {R : Type u_2} {M : Type u} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S], IsIsotypicOfType R M S → IsIsotypic R M
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.liftOfLE_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M₁ : Type u_7}
  {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁] [inst_6 : Module R M₂]
  (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) (f₁ : M →ₗ[R] M₁) (f₂ : M →ₗ[R] M₂) [inst_7 : IsLocalizedModule S₁ f₁]
  [inst_8 : IsLocalizedModule S₂ f₂], IsLocalizedModule.liftOfLE S₁ S₂ h f₁ f₂ ∘ₗ f₁ = f₂
-- Mathlib.GroupTheory.Focal
AddSubgroup.focalAddSubgroupOf_def : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.focalAddSubgroupOf = H.focalAddSubgroup.addSubgroupOf H
-- Mathlib.Analysis.CStarAlgebra.Classes
instCStarAlgebraSubtypeMemStarSubalgebraComplexElemental : {A : Type u_1} → [inst : CStarAlgebra A] → (x : A) → CStarAlgebra ↥(StarAlgebra.elemental ℂ x)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractLeft_mul_algebraMap : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d : Module.Dual R M) (a : CliffordAlgebra Q) (r : R),
  (CliffordAlgebra.contractLeft d) (a * (algebraMap R (CliffordAlgebra Q)) r) =
    (CliffordAlgebra.contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Identity chain map.  -/
HomologicalComplex.id : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (A : HomologicalComplex V c) → A.Hom A
-- Mathlib.Algebra.Order.SuccPred.TypeTags
instSuccOrderMultiplicative : {X : Type u_1} → [inst : Preorder X] → [h : SuccOrder X] → SuccOrder (Multiplicative X)
-- Mathlib.Order.WithBot
WithBot.some_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} {v : WithBot α}, ↑y = WithBot.map f v ↔ ∃ x, v = ↑x ∧ f x = y
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
/-- The center of a non-unital non-associative semiring `R` is the set of elements that
commute and associate with everything in `R`, here realized as a non-unital star
subsemiring.  -/
NonUnitalStarSubsemiring.center : (R : Type u_1) → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : StarRing R] → NonUnitalStarSubsemiring R
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- `H` is closed under additive conjugation  -/
AddSubgroup.Normal.conj_mem : ∀ {A : Type u_2} [inst : AddGroup A] {H : AddSubgroup A}, H.Normal → ∀ n ∈ H, ∀ (g : A), g + n + -g ∈ H
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.add : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {u v : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} [inst_1 : Add β]
  [MeasurableAdd₂ β],
  MeasureTheory.IsProgressive f u →
    MeasureTheory.IsProgressive f v → MeasureTheory.IsProgressive f fun i ω => u i ω + v i ω
-- ImportGraph.Tools.FindHome
GoToModuleLinkProps.mk.injEq : ∀ (modName modName_1 : Lean.Name), ({ modName := modName } = { modName := modName_1 }) = (modName = modName_1)
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendsto : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing E] [inst_2 : NormedAlgebra 𝕜 E]
  (c : ℕ → 𝕜) {r : NNReal},
  r ≠ 0 →
    Filter.Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) Filter.atTop (nhds ↑r) →
      ↑r⁻¹ ≤ (FormalMultilinearSeries.ofScalars E c).radius
-- Mathlib.Data.Finset.Sum
Finset.toRight_sdiff : ∀ {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (u \ v).toRight = u.toRight \ v.toRight