mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- The multiplicative Roth number of a finset is the cardinality of its biggest 3GP-free subset.  -/
mulRothNumber : {α : Type u_2} → [DecidableEq α] → [Monoid α] → Finset α →o ℕ
-- Mathlib.Order.Interval.Set.Disjoint
IsGLB.biUnion_Ioi_eq : ∀ {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α}, IsGLB s a → ⋃ x ∈ s, Set.Ioi x = Set.Ioi a
-- Mathlib.Order.WithBot
Equiv.withBotCongr_symm : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), e.symm.withBotCongr = e.withBotCongr.symm
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.GeometricallyReduced f] [AlgebraicGeometry.Flat f]
  [AlgebraicGeometry.IsReduced Y] [AlgebraicGeometry.IsLocallyNoetherian Y], AlgebraicGeometry.IsReduced X
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.srange_eq_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N), f.srange = Subsemigroup.map f ⊤
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
/-- A morphism in `C`.  -/
CategoryTheory.Limits.ColimitPresentation.Total.Hom.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u_1} →
      {I : J → Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] →
            {D : CategoryTheory.Functor J C} →
              {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} →
                {k l : CategoryTheory.Limits.ColimitPresentation.Total P} →
                  k.Hom l → ((P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd)
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.right_distrib : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b c : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.mul (Lean.Grind.Ring.OfSemiring.add a b) c =
    Lean.Grind.Ring.OfSemiring.add (Lean.Grind.Ring.OfSemiring.mul a c) (Lean.Grind.Ring.OfSemiring.mul b c)
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instNonemptyShiftOfIsStableUnderShiftBy : ∀ {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) [P.IsStableUnderShiftBy a] [P.Nonempty],
  (P.shift a).Nonempty
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Cnstr.offset.sizeOf_spec : ∀ (gen? : Option Lean.Meta.Grind.GenPatternInfo) (pat : Lean.Expr) (k : ℕ) (e : Lean.Expr),
  sizeOf (Lean.Meta.Grind.EMatch.Cnstr.offset gen? pat k e) = 1 + sizeOf gen? + sizeOf pat + sizeOf k + sizeOf e
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Two left Kan extensions are (canonically) isomorphic.  -/
CategoryTheory.Functor.leftKanExtensionUnique : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : F ⟶ L.comp F') →
                    [F'.IsLeftKanExtension α] →
                      (F'' : CategoryTheory.Functor D H) →
                        (α' : F ⟶ L.comp F'') → [F''.IsLeftKanExtension α'] → F' ≅ F''
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithTop.decidableLT.match_1.eq_3 : ∀ {α : Type u_1} (motive : WithTop α → WithTop α → Sort u_2) (a b : α) (h_1 : (x : WithTop α) → motive x none)
  (h_2 : (a : α) → motive none (some a)) (h_3 : (a b : α) → motive (some a) (some b)),
  (match some a, some b with
    | x, none => h_1 x
    | none, some a => h_2 a
    | some a, some b => h_3 a b) =
    h_3 a b
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.productEquiv_counitIso_inv_app : ∀ {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J × CategoryTheory.Discrete K),
  CategoryTheory.Discrete.productEquiv.counitIso.inv.app X =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_sSup_of_directedOn : ∀ {M : Type u_1} [inst : MulOneClass M] {S : Set (Submonoid M)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib.Algebra.Ring.Defs
mul_one_sub_mul : ∀ {α : Type u} [inst : NonAssocRing α] (a b c : α), a * (1 - b) * c = a * c - a * b * c
-- Mathlib.Analysis.Real.OfDigits
Real.sum_ofDigitsTerm_digits_le : ∀ {x : ℝ} {b : ℕ} [inst : NeZero b],
  x ∈ Set.Ico 0 1 → ∀ (n : ℕ), ∑ i ∈ Finset.range n, Real.ofDigitsTerm (x.digits b) i ≤ x
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.ι₃_desc_assoc : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁)
  {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₂.ι₃
      (CategoryTheory.CategoryStruct.comp (SSet.horn₃₂.desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) h) =
    CategoryTheory.CategoryStruct.comp f₃ h
-- Mathlib.Algebra.Lie.Nilpotent
/-- The lower central series of Lie submodules of a Lie module.  -/
LieModule.lowerCentralSeries : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [LieAlgebra R L] →
            [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → ℕ → LieSubmodule R L M
-- Mathlib.Logic.Basic
BEx.intro : ∀ {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop} (a : α) (h₁ : p a), P a h₁ → ∃ x, ∃ (h : p x), P x h
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Group structure on `HomotopyGroup N X x` for nonempty `N` (in particular `π_(n+1) X x`).  -/
HomotopyGroup.group : {X : Type u_2} →
  [inst : TopologicalSpace X] → {x : X} → (N : Type u_3) → [DecidableEq N] → [Nonempty N] → Group (HomotopyGroup N X x)
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_add_sin : ∀ (x y : ℝ), Real.sin x + Real.sin y = 2 * Real.sin ((x + y) / 2) * Real.cos ((x - y) / 2)
-- Init.Data.Iterators.Basic
Std.PlausibleIterStep.done.congr_simp : ∀ {α : Type u} {β : Type w} {IsPlausibleStep : Std.IterStep α β → Prop} (h : IsPlausibleStep Std.IterStep.done),
  Std.PlausibleIterStep.done h = Std.PlausibleIterStep.done h
-- Aesop.Script.SpecificTactics
Aesop.clearS : Lean.MVarId → Lean.FVarId → Aesop.ScriptM Lean.MVarId
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.iterFromIdx_eq_toIter_iterFromIdxM : ∀ {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ}, xs.iterFromIdx pos = (xs.iterFromIdxM Id pos).toIter
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Compatibility with the structure morphism, for a morphism of algebras.  -/
CategoryTheory.Monad.Algebra.Hom.h_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra}
  (self : A.Hom B) {Z : C} (h : B.A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (T.map self.f) (CategoryTheory.CategoryStruct.comp B.a h) =
    CategoryTheory.CategoryStruct.comp A.a (CategoryTheory.CategoryStruct.comp self.f h)
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.PEquivOn.ext : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {inst : LinearOrder ι} {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  {inst_1 : SuccOrder ι} {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s : Set ι}
  {x y : InverseSystem.PEquivOn f equivSucc s}, x.equiv = y.equiv → x = y
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.MulSubshift.mk : {A : Type u_1} →
  [inst : TopologicalSpace A] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        (carrier : Set (G → A)) →
          IsClosed carrier →
            (∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.mulShift g) carrier carrier) →
              SymbolicDynamics.FullShift.MulSubshift A G
-- Mathlib.Topology.UniformSpace.Ultra.Completion
IsUltraUniformity.separationQuotient_iff : ∀ {X : Type u_1} [inst : UniformSpace X], IsUltraUniformity (SeparationQuotient X) ↔ IsUltraUniformity X
-- Mathlib.Order.Filter.Basic
Filter.Eventually.eq_1 : ∀ {α : Type u_1} (p : α → Prop) (f : Filter α), Filter.Eventually p f = ({x | p x} ∈ f)
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.grade.gradedAlgebra : {ι : Type u_2} →
  {R : Type u_3} →
    [inst : DecidableEq ι] →
      [inst_1 : AddMonoid ι] → [inst_2 : CommSemiring R] → GradedAlgebra (AddMonoidAlgebra.grade R)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.coe_equivMapOfInjective_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₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (f : M →ₛₗ[σ₁₂] M₂)
  (i : Function.Injective ⇑f) (p : Submodule R M) (x : ↥p), ↑((Submodule.equivMapOfInjective f i p) x) = f ↑x
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.fork_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).ι = TopCat.Presheaf.SheafConditionEqualizerProducts.res F U
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_lt_of_left_ne_zero_of_degree_mul_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
  {p p' q : MvPolynomial σ R},
  p ≠ 0 → m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q)) → m.toSyn (m.degree p) < m.toSyn (m.degree p')
-- Mathlib.Algebra.Free
instReprFreeAddMagma : {α : Type u} → [Repr α] → Repr (FreeAddMagma α)
-- Std.Data.DHashMap.Internal.AssocList.Iterator
_private.Std.Data.DHashMap.Internal.AssocList.Iterator.0.Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma.match_1.eq_3 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Std.IterStep (Std.IterM Id ((a : α) × β a)) ((a : α) × β a) → Sort u_3)
  (h_1 : (it' : Std.IterM Id ((a : α) × β a)) → (out : (a : α) × β a) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM Id ((a : α) × β a)) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Init.Data.List.MinMaxIdx
List.minIdxOn_le_of_apply_getElem_le_apply_minOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α} (h : xs ≠ []) {k : ℕ} (hi : k < xs.length), f xs[k] ≤ f (List.minOn f xs h) → List.minIdxOn f xs h ≤ k
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.mulEquivCongr_symm_apply_smul : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : IsDomain B] [inst_5 : Algebra A B] [inst_6 : FaithfulSMul A B]
  [inst_7 : MulSemiringAction G B] [inst_8 : MulSemiringAction G' B] [inst_9 : IsGaloisGroup G A B]
  [inst_10 : IsGaloisGroup G' A B] [inst_11 : Finite G] [inst_12 : Finite G'] (g : G') (x : B),
  (IsGaloisGroup.mulEquivCongr G G' A B).symm g • x = g • x
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The functor which sends `n : SimplexCategoryᵒᵖ` to the evaluation
functor `SSet.{u} ⥤ Type u` on the object `n`.  -/
SSet.evaluation : CategoryTheory.Functor SimplexCategoryᵒᵖ (CategoryTheory.Functor SSet (Type u))
-- Mathlib.RingTheory.SimpleModule.Basic
IsSimpleModule.toIsSimpleOrder : ∀ {R : Type u_2} {inst : Ring R} {M : Type u_4} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  [self : IsSimpleModule R M], IsSimpleOrder (Submodule R M)
-- Mathlib.Order.InitialSeg
InitialSeg.instOrderHomClassLt : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β], OrderHomClass (α ≤i β) α β
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_mul_neg : ∀ {R : Type u_1} [inst : Ring R] (x : R) (n : ℕ), (∑ i ∈ Finset.range n, x ^ i) * (1 - x) = 1 - x ^ n
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarDecl.kind : Lean.Elab.Term.SyntheticMVarDecl → Lean.Elab.Term.SyntheticMVarKind
-- Init.Data.Format.Basic
/-- A node containing a plain string.

If the string contains newlines, the formatter emits them and then indents to the current level.
 -/
Std.Format.text : String → Std.Format
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.limitConeIsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections],
  GrpCat.limitConeIsLimit F =
    CategoryTheory.liftedLimitIsLimit
      (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ GrpCat MonCat)))
-- Mathlib.InformationTheory.Coding.KraftMcMillan
/-- Length of a concatenation of `r` codewords lies in `[r, r*sup length]`
assuming `[] ∉ S`.  -/
_private.Mathlib.InformationTheory.Coding.KraftMcMillan.0.InformationTheory.concatFn_length_mem_Icc : ∀ {α : Type u_1} {S : Finset (List α)} {r : ℕ} {w : Fin r → ↥S},
  (∀ (c : ↥S), ↑c ≠ []) → (InformationTheory.concatFn✝ w).length ∈ Finset.Icc r (r * S.sup List.length)
-- Init.Control.Option
/-- Recovers from failures. Typically used via the `<|>` operator.
 -/
OptionT.orElse : {m : Type u → Type v} → [Monad m] → {α : Type u} → OptionT m α → (Unit → OptionT m α) → OptionT m α
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The `spanPoints` of a set is nonempty if and only if that set is.  -/
spanPoints_nonempty : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), (spanPoints k s).Nonempty ↔ s.Nonempty
-- Mathlib.Order.Concept
Order.isExtent_lowerPolar : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β}, Order.IsExtent r (lowerPolar r t)
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.instHMulInt : HMul ℤ Lean.Omega.LinearCombo Lean.Omega.LinearCombo
-- Mathlib.Data.List.Lookmap
_private.Mathlib.Data.List.Lookmap.0.List.lookmap.go_append : ∀ {α : Type u_1} (f : α → Option α) (l : List α) (acc : Array α),
  List.lookmap.go f l acc = acc.toListAppend (List.lookmap f l)
-- Init.Data.List.Sort.Basic
List.merge_right : ∀ {α : Type u_1} {le : α → α → Bool} (xs : List α), xs.merge [] le = xs
-- Init.Data.List.Erase
List.eraseP_nil : ∀ {α : Type u_1} {p : α → Bool}, List.eraseP p [] = []
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.replaceFTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : Array α) →
        ((acc : Array α) → motive [] acc) →
          ((x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc) → motive x x_1
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The function `AddOpposite.op` is a multiplicative equivalence.  -/
AddOpposite.opMulEquiv : {α : Type u_2} → [inst : Mul α] → α ≃* αᵃᵒᵖ
-- Mathlib.FieldTheory.SplittingField.Construction
/-- Divide a polynomial f by `X - C r` where `r` is a root of `f` in a bigger field extension.  -/
Polynomial.removeFactor : {K : Type v} → [inst : Field K] → (f : Polynomial K) → Polynomial (AdjoinRoot f.factor)
-- Mathlib.Data.List.MinMax
List.minimum_of_length_pos_le_of_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {a : α},
  a ∈ l → ∀ (w : 0 < l.length), List.minimum_of_length_pos w ≤ a
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.sqFrom_left : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) (i : ι), CategoryTheory.Arrow.Hom.left (f.sqFrom i) = f.f i
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_omega0`. -/
Ordinal.principal_add_omega0 : Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) Ordinal.omega0
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.refl_snd : ∀ {X Y : TopPair} (f : X ⟶ Y), (TopPair.Homotopy.refl f).snd = TopCat.Homotopy.refl (TopPair.Hom.snd f)
-- Lean.Elab.PreDefinition.Main
_private.Lean.Elab.PreDefinition.Main.0.Lean.Elab.collectMVarsAtPreDef : Lean.Elab.PreDefinition → StateRefT' IO.RealWorld Lean.CollectMVars.State Lean.MetaM Unit
-- Init.Data.Nat.Div.Basic
Nat.mul_div_cancel_left : ∀ (m : ℕ) {n : ℕ}, 0 < n → n * m / n = m
-- Aesop.RuleTac.RuleTerm
Aesop.instInhabitedElabRuleTerm : Inhabited Aesop.ElabRuleTerm
-- Mathlib.Algebra.Category.Semigrp.Basic
AddEquiv.toAddMagmaCatIso_inv : ∀ {X Y : Type u} [inst : Add X] [inst_1 : Add Y] (e : X ≃+ Y),
  e.toAddMagmaCatIso.inv = AddMagmaCat.ofHom e.symm.toAddHom
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.η_ε : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.Monoidal],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F)
      (CategoryTheory.Functor.LaxMonoidal.ε F) =
    CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.RingTheory.Localization.FractionRing
/-- `IsFractionRing R K` states `K` is the ring of fractions of a commutative ring `R`.  -/
IsFractionRing : (R : Type u_6) → [inst : CommSemiring R] → (K : Type u_7) → [inst_1 : CommSemiring K] → [Algebra R K] → Prop
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.subset : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M → N.E ⊆ M.E
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
FiniteDimensional.of_finrank_pos : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  0 < Module.finrank K V → FiniteDimensional K V
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.apply_eq_iff : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {b : Module.Basis ι R M} {x : M} {i : ι}, b i = x ↔ b.repr x = fun₀ | i => 1
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_pow_succ : ∀ {R : Type u} [inst : CommSemiring R] (p : Polynomial R) (n : ℕ),
  Polynomial.derivative (p ^ (n + 1)) = Polynomial.C (↑n + 1) * p ^ n * Polynomial.derivative p
-- Init.Data.List.Sublist
_private.Init.Data.List.Sublist.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeUnopOfIsClosedUnderLimitsOfShapeOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] (Q : CategoryTheory.ObjectProperty Cᵒᵖ)
  [Q.IsClosedUnderLimitsOfShape Jᵒᵖ], Q.unop.IsClosedUnderColimitsOfShape J
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.dvd_X_mul_iff : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {i : σ} {p q : MvPolynomial σ R} [IsCancelMulZero R],
  p ∣ MvPolynomial.X i * q ↔ p ∣ q ∨ MvPolynomial.X i ∣ p ∧ (p.divMonomial fun₀ | i => 1) ∣ q
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackSnd_apply : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z)
  (x : ↑(TopCat.of { p // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 })),
  (CategoryTheory.ConcreteCategory.hom (TopCat.pullbackSnd f g)) x = (↑x).2
-- Mathlib.Topology.Order.OrderClosed
Filter.tendsto_nhds_min_right : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f : β → α}
  {l : Filter β} {a : α},
  Filter.Tendsto f l (nhdsWithin a (Set.Iio a)) → Filter.Tendsto (fun i => min a (f i)) l (nhdsWithin a (Set.Iio a))
-- Mathlib.GroupTheory.Congruence.Defs
Con.liftOn.eq_1 : ∀ {M : Type u_1} [inst : Mul M] {β : Sort u_4} {c : Con M} (q : c.Quotient) (f : M → β)
  (h : ∀ (a b : M), c a b → f a = f b), Con.liftOn q f h = Quotient.liftOn' q f h
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Analytic functions are meromorphic in normal form.  -/
AnalyticOnNhd.meromorphicNFOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, AnalyticOnNhd 𝕜 f U → MeromorphicNFOn f U
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeAction.toPartialResultParams : Lean.Lsp.CodeAction → Lean.Lsp.PartialResultParams
-- Mathlib.GroupTheory.Exponent
/-- The exponent of a group is the smallest positive integer `n` such that `g ^ n = 1` for all
`g ∈ G` if it exists, otherwise it is zero by convention.  -/
Monoid.exponent : (G : Type u) → [Monoid G] → ℕ
-- Init.Data.Array.Attach
Array.unattach_attachWith : ∀ {α : Type u_1} {p : α → Prop} {xs : Array α} {H : ∀ a ∈ xs, p a}, (xs.attachWith p H).unattach = xs
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.prod_right_ae : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite μ] ⦃f : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) → ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun y => f (x, y)) ν
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.ae_ae_of_ae_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {p : α × β → Prop},
  (∀ᵐ (x : α × β) ∂μ.compProd κ, p x) → ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)
-- Mathlib.RingTheory.Binomial
Ring.multichoose_zero_succ : ∀ {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Pow R ℕ] [NatPowAssoc R] [inst_3 : BinomialRing R] (k : ℕ),
  Ring.multichoose 0 (k + 1) = 0
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.ext : ∀ {G : Type u_3} [inst : Group G] {u v : UniformSpace G}, IsUniformGroup G → IsUniformGroup G → nhds 1 = nhds 1 → u = v
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.mk : {R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} →
      [inst_1 : Ring S] →
        [inst_2 : Algebra R S] →
          (toRingNorm : RingNorm S) →
            (∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x) → AlgebraNorm R S
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- The universal property of open immersions:
For an open immersion `f : X ⟶ Z`, given any morphism of schemes `g : Y ⟶ Z` whose topological
image is contained in the image of `f`, we can lift this morphism to a unique `Y ⟶ X` that
commutes with these maps.
 -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift : {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) →
            Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆
                Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) →
              (Y ⟶ X)