mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_ac : Bool → Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.neg_intCast_of_neg : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R], ∀ a < 0, ↑a < 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_minKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insert k v).minKey?.isSome = true
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.mk.inj : ∀ {V : Type u_1} {Adj Adj_1 : V → V → Prop}, { Adj := Adj } = { Adj := Adj_1 } → Adj = Adj_1
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Set.Finite.multipliable : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {s : Set β},
  s.Finite → ∀ (f : β → α), Multipliable (f ∘ Subtype.val)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Set.pow_mul_subgroupClosure : ∀ {G : Type u_2} [inst : Group G] {s : Set G},
  s.Nonempty → ∀ (n : ℕ), s ^ n * ↑(Subgroup.closure s) = ↑(Subgroup.closure s)
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- The global ref for looking up `rw` lemmas.  -/
Mathlib.Tactic.ClickSuggestions.rwRef : IO.Ref (Option (Lean.Meta.RefinedDiscrTree Mathlib.Tactic.ClickSuggestions.RwLemma))
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G H : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_5 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  {Y : CategoryTheory.Functor C V},
  (CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂ F G H).homEquiv =
    (CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy F
            (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).homEquiv.trans
      ((CategoryTheory.MonoidalCategory.externalProduct F
            (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).homEquivOfIsLeftKanExtension
        (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight
          (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)
          (CategoryTheory.MonoidalCategory.DayConvolution.unit G H) F)
        (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj (CategoryTheory.MonoidalCategory.tensor C)).obj Y))
-- Mathlib.Algebra.Homology.Precylinder
HomologicalComplex.precylinder_I : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} [inst_2 : DecidableRel c.Rel] (K : HomologicalComplex C c)
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  K.precylinder.I = K.cylinder
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getDₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [LawfulBEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → β a
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The whole group `G` is normal.  -/
AddSubgroup.normal_top : ∀ {G : Type u_1} [inst : AddGroup G], ⊤.Normal
-- Init.Data.Array.Perm
Array.Perm.symm : ∀ {α : Type u_1} {xs ys : Array α}, xs.Perm ys → ys.Perm xs
-- Init.Data.UInt.Lemmas
UInt32.le_or_lt : ∀ (a b : UInt32), a ≤ b ∨ b < a
-- Mathlib.RingTheory.LocalRing.ResidueField.Instances
IsLocalRing.instFiniteResidueField_1 : ∀ {R : Type u_4} {k : Type u_5} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : Field k] [inst_3 : Algebra R k]
  [inst_4 : Module.Finite R k], Module.Finite (IsLocalRing.ResidueField R) k
-- Aesop.Search.Expansion
Aesop.runUnsafeRule : {Q : Type} →
  [inst : Aesop.Queue Q] → Aesop.GoalRef → Aesop.IndexMatchResult Aesop.UnsafeRule → Aesop.SearchM Q Aesop.RuleResult
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipSuffixWhile_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.copy.skipSuffixWhile pat = (s.skipSuffixWhile pat).copy
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.AffineScheme.Γ.eq_1 : AlgebraicGeometry.AffineScheme.Γ = AlgebraicGeometry.AffineScheme.forgetToScheme.op.comp AlgebraicGeometry.Scheme.Γ
-- Mathlib.RingTheory.Nilpotent.Defs
IsUnit.isNilpotent_mul_unit_of_commute_iff : ∀ {R : Type u_1} [inst : MonoidWithZero R] {r u : R}, IsUnit u → Commute r u → (IsNilpotent (r * u) ↔ IsNilpotent r)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.of_mem_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G}, IsOfFinAddOrder x → y ∈ AddSubgroup.zmultiples x → IsOfFinAddOrder y
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_union_Ici_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Iio b ∪ Set.Ici a = Set.univ
-- Mathlib.Computability.Partrec
/-- Find the smallest `n` satisfying `p n`, where all `p k` for `k < n` are defined as false.
Returns a `Part`.  -/
Nat.rfind : (ℕ →. Bool) → Part ℕ
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_eq_iSup_eapprox_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → ∫⁻ (a : α), f a ∂μ = ⨆ n, (MeasureTheory.SimpleFunc.eapprox f n).lintegral μ
-- Init.Data.Array.Count
Array.count_filterMap : ∀ {β : Type u_1} {α : Type u_2} [inst : BEq β] {b : β} {f : α → Option β} {xs : Array α},
  Array.count b (Array.filterMap f xs) = Array.countP (fun a => f a == some b) xs
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.funUnique_symm_apply : ∀ (ι : Type u_2) (α : Type u) [inst : PseudoEMetricSpace α] [inst_1 : Unique ι] [inst_2 : Fintype ι] (x : α) (i : ι),
  (IsometryEquiv.funUnique ι α).symm x i = x
-- Lean.Linter.Init
Lean.Linter.EnvLinterSnapshot : Type
-- Init.Tactics
/-- A dsimp args list is a list of `dsimpArg`. This is the main argument to `dsimp`.  -/
Lean.Parser.Tactic.dsimpArgs : Lean.ParserDescr
-- Init.Control.Lawful.Instances
ExceptT.run_control : ∀ {m : Type u → Type u_1} {ε α : Type u} [inst : Monad m] [LawfulMonad m]
  (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)),
  (control f).run = f fun {β} x => x.run
-- Init.Data.Nat.Coprime
Nat.Coprime.mul_right : ∀ {k m n : ℕ}, k.Coprime m → k.Coprime n → k.Coprime (m * n)
-- Lean.MetavarContext
/-- Modify the declaration of a metavariable. If the metavariable is not declared,
nothing happens.

You must ensure that the modification is legal. In particular, expressions may
only be replaced with defeq expressions.
 -/
Lean.MVarId.modifyDecl : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → (Lean.MetavarDecl → Lean.MetavarDecl) → m Unit
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.neg_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x x' : RingCat.Colimits.Prequotient F) (x_1 : RingCat.Colimits.Relation F x x'),
  RingCat.Colimits.Relation.below x_1 → motive x x' x_1 → RingCat.Colimits.Relation.below ⋯
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.instHasInitial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.Limits.HasInitial (CategoryTheory.Factorisation f)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The radius of the circumsphere is the circumradius.  -/
Affine.Simplex.circumsphere_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n), s.circumsphere.radius = s.circumradius
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_functor_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} {t₁ t₂ : CategoryTheory.Limits.Cone K} (f : t₁ ⟶ t₂),
  (CategoryTheory.WithTerminal.coneEquiv.functor.map f).hom = CategoryTheory.Over.Hom.left f.hom
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatUInt64UintOfNatNat : Lean.Grind.ToInt.OfNat UInt64 (Lean.Grind.IntInterval.uint 64)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
_private.Init.Data.String.Lemmas.Pattern.TakeDrop.Basic.0.String.Slice.Pos.revSkipWhile.eq_1 : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  pos.revSkipWhile pat =
    match pos.revSkip? pat with
    | some nextCurr => if nextCurr < pos then nextCurr.revSkipWhile pat else pos
    | none => pos
-- Init.Control.Lawful.Basic
monadLift_self : ∀ {α : Type u} {m : Type u → Type v} (x : m α), monadLift x = x
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.K'.elim.match_1.eq_3 : ∀ (motive : Turing.PartrecToTM2.K' → Sort u_1) (h_1 : Unit → motive Turing.PartrecToTM2.K'.main)
  (h_2 : Unit → motive Turing.PartrecToTM2.K'.rev) (h_3 : Unit → motive Turing.PartrecToTM2.K'.aux)
  (h_4 : Unit → motive Turing.PartrecToTM2.K'.stack),
  (match Turing.PartrecToTM2.K'.aux with
    | Turing.PartrecToTM2.K'.main => h_1 ()
    | Turing.PartrecToTM2.K'.rev => h_2 ()
    | Turing.PartrecToTM2.K'.aux => h_3 ()
    | Turing.PartrecToTM2.K'.stack => h_4 ()) =
    h_3 ()
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.lift_neg : ∀ {α : Type u} {G : Type u_1} [inst : AddCommGroup G] (f : α → G), FreeAbelianGroup.lift (-f) = -FreeAbelianGroup.lift f
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateParamCoreImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Param pu → Lean.Expr → Lean.Compiler.LCNF.Param pu
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Translating a `ModularForm` by `GL(2, ℝ)`, to obtain a new `ModularForm`.  -/
ModularForm.translate : {k : ℤ} →
  {Γ : Subgroup (GL (Fin 2) ℝ)} →
    {F : Type u_1} →
      [inst : FunLike F UpperHalfPlane ℂ] →
        F → [ModularFormClass F Γ k] → (g : GL (Fin 2) ℝ) → ModularForm (ConjAct.toConjAct g⁻¹ • Γ) k
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mk.injEq : ∀ {R : Type u_1} [inst : CommRing R] (toSubsemiring : Subsemiring R)
  (mem_of_isSquare' :
    autoParam (∀ {x : R}, IsSquare x → x ∈ toSubsemiring.carrier) RingPreordering.mem_of_isSquare'._autoParam)
  (neg_one_notMem' : autoParam (-1 ∉ toSubsemiring.carrier) RingPreordering.neg_one_notMem'._autoParam)
  (toSubsemiring_1 : Subsemiring R)
  (mem_of_isSquare'_1 :
    autoParam (∀ {x : R}, IsSquare x → x ∈ toSubsemiring_1.carrier) RingPreordering.mem_of_isSquare'._autoParam)
  (neg_one_notMem'_1 : autoParam (-1 ∉ toSubsemiring_1.carrier) RingPreordering.neg_one_notMem'._autoParam),
  ({ toSubsemiring := toSubsemiring, mem_of_isSquare' := mem_of_isSquare', neg_one_notMem' := neg_one_notMem' } =
      { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := mem_of_isSquare'_1,
        neg_one_notMem' := neg_one_notMem'_1 }) =
    (toSubsemiring = toSubsemiring_1)
-- Init.PropLemmas
and_congr_left_eq : ∀ {c a b : Prop}, (c → a = b) → (a ∧ c) = (b ∧ c)
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The coercion `↑ : WeakDual 𝕜 E → (E → 𝕜)` sends bounded closed sets to closed sets.  -/
WeakDual.isClosed_image_coe_of_bounded_of_closed : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set (WeakDual 𝕜 E)}, Bornology.IsBounded s → IsClosed s → IsClosed (DFunLike.coe '' s)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support_single_of_ne : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R},
  r ≠ 0 → ((HahnSeries.single a) r).support = {a}
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` and `β` are arbitrary types and there is a bijection between them,
then the induced map on their additive free groups is also bijective.  -/
FreeAddGroup.map_bijective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Bijective f → Function.Bijective ⇑(FreeAddGroup.map f)
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_comp_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) (f : σ → MvPolynomial τ R),
  (MvPolynomial.expand p).comp (MvPolynomial.bind₁ f) = MvPolynomial.bind₁ fun i => (MvPolynomial.expand p) (f i)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyMin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C)
  [P.HasTwoOutOfThreeProperty] [Q.HasTwoOutOfThreeProperty], (P ⊓ Q).HasTwoOutOfThreeProperty
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.mk : {L : FirstOrder.Language} →
  {T : L.Theory} →
    {α : Type w} →
      (toTheory : (L.withConstants α).Theory) →
        (L.lhomWithConstants α).onTheory T ⊆ toTheory → toTheory.IsMaximal → T.CompleteType α
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The product in `CommRingCat` is the Cartesian product. This is the binary fan.  -/
CommRingCat.prodFan : (A B : CommRingCat) → CategoryTheory.Limits.BinaryFan A B
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
instIsDecompositionFieldOfIsGaloisGroupSubtypeAlgEquivMemSubgroupStabilizerIdeal : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (D : Type u_5) [inst_4 : Field D] [inst_5 : Algebra D L]
  [inst_6 : MulSemiringAction Gal(L/K) B] [h : IsGaloisGroup (↥(MulAction.stabilizer Gal(L/K) P)) D L],
  IsDecompositionField K L P D
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → k ∉ t₁ ∩ t₂
-- Mathlib.Algebra.Order.Group.Synonym
pow_toDual : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β), a ^ OrderDual.toDual b = a ^ b
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.toContinuousMap_injective : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R], Function.Injective toContinuousMap
-- Init.Data.Nat.Div.Lemmas
Nat.succ_div_of_not_dvd : ∀ {a b : ℕ}, ¬b ∣ a + 1 → (a + 1) / b = a / b
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- The natural non-unital ring hom from a non-unital subsemiring of a non-unital semiring `R` to
`R`.  -/
NonUnitalSubsemiringClass.subtype : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : SetLike S R] → [inst_2 : NonUnitalSubsemiringClass S R] → (s : S) → ↥s →ₙ+* R
-- Init.Data.String.Iterate
/-- Folds a function over a string from the start, accumulating a value starting with `init`. The
accumulated value is combined with each character in order, using `f`.

Examples:

* `"coffee tea water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2`

* `"coffee tea and water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3`

* `"coffee tea water".foldl (·.push ·) "" = "coffee tea water"`
 -/
String.foldl : {α : Type u} → (α → Char → α) → α → String → α
-- Init.Data.List.Basic
List.dropLast_cons_cons : ∀ {α : Type u_1} {x y : α} {zs : List α}, (x :: y :: zs).dropLast = x :: (y :: zs).dropLast
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.eq_div_of_mul_eq_right : ∀ {R : Type u} [inst : EuclideanDomain R] {a b c : R}, a ≠ 0 → a * b = c → b = c / a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termW : Lean.ParserDescr
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- A module `M` is `I`-adically complete if it is Hausdorff and precomplete.  -/
IsAdicComplete : {R : Type u_1} → [inst : CommRing R] → Ideal R → (M : Type u_4) → [inst_1 : AddCommGroup M] → [Module R M] → Prop
-- Mathlib.Order.Atoms
OrderDual.instIsCoatomic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] [IsAtomic α], IsCoatomic αᵒᵈ
-- Mathlib.Probability.Kernel.MeasurableLIntegral
Measurable.lintegral_kernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {f : β → ENNReal}, Measurable f → Measurable fun a => ∫⁻ (b : β), f b ∂κ a
-- Mathlib.Data.Set.Defs
/-- The intersection of two sets `s` and `t` is the set of elements contained in both `s` and `t`.

Note that you should **not** use this definition directly, but instead write `s ∩ t`.  -/
Set.inter : {α : Type u} → Set α → Set α → Set α
-- Mathlib.Data.Finset.Grade
Finset.covBy_iff_exists_insert : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s ⋖ t ↔ ∃ a ∉ s, insert a s = t
-- Lean.Parser.Term
Lean.Parser.Term.panic.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Batteries.Data.PairingHeap
/-- `O(n log n)`. Convert the heap to a list in increasing order.  -/
Batteries.PairingHeap.toList : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le → List α
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNonUnitalCommSemiringOfIsTopologicalSemiring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalCommSemiring β] → [IsTopologicalSemiring β] → NonUnitalCommSemiring C(α, β)
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.isConnected_iff : ∀ (X : SSet), X.IsConnected ↔ X.IsPreconnected ∧ X.Nonempty
-- Mathlib.Data.Stream.Defs
/-- A constant stream, same as `Stream'.const`.  -/
Stream'.pure : {α : Type u} → α → Stream' α
-- Mathlib.Algebra.Group.Action.Pi
Pi.addAction' : {ι : Type u_1} →
  {α : ι → Type u_4} →
    {β : ι → Type u_5} →
      {m : (i : ι) → AddMonoid (α i)} → [(i : ι) → AddAction (α i) (β i)] → AddAction ((i : ι) → α i) ((i : ι) → β i)
-- Lean.Meta.TryThis
/-- Style as an error. By default, decorates the text with an undersquiggle; providing the argument
`decorated := false` turns this off.  -/
Lean.Meta.Tactic.TryThis.SuggestionStyle.error : optParam Bool true → Lean.Meta.Tactic.TryThis.SuggestionStyle
-- Mathlib.Algebra.Order.SuccPred
/-- A typeclass for `pred x = x - 1`.  -/
PredSubOrder : (α : Type u_1) → [Preorder α] → [Sub α] → [One α] → Type u_1
-- Mathlib.NumberTheory.LSeries.Convolution
/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
equals the product of their L-series in their common half-plane of absolute convergence.  -/
LSeries_convolution : ∀ {f g : ℕ → ℂ} {s : ℂ},
  LSeries.abscissaOfAbsConv f < ↑s.re →
    LSeries.abscissaOfAbsConv g < ↑s.re → LSeries (LSeries.convolution f g) s = LSeries f s * LSeries g s
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_f_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℕ)
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) (AlgebraicTopology.DoldKan.QInfty.f n) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) (f.app (Opposite.op { len := n }))
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
_private.Mathlib.NumberTheory.NumberField.Cyclotomic.Basic.0.IsCyclotomicExtension.Rat.adjoin_singleton_eq_top_aux : ∀ (K : Type u) [inst : Field K] [inst_1 : CharZero K] [NumberField K] (F₁ F₂ : IntermediateField ℚ K) {n₁ n₂ : ℕ}
  [inst_3 : NeZero n₁] [inst_4 : NeZero n₂] [IsCyclotomicExtension {n₁} ℚ ↥F₁] [IsCyclotomicExtension {n₂} ℚ ↥F₂]
  {ζ₁ : ↥F₁} (hζ₁ : IsPrimitiveRoot ζ₁ n₁),
  ℤ[hζ₁.toInteger] = ⊤ →
    ∀ {ζ₂ : ↥F₂} (hζ₂ : IsPrimitiveRoot ζ₂ n₂),
      ℤ[hζ₂.toInteger] = ⊤ →
        n₁.Coprime n₂ → F₁ ⊔ F₂ = ⊤ → ∀ {ζ : K} (hζ : IsPrimitiveRoot ζ (n₁ * n₂)), ℤ[hζ.toInteger] = ⊤
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Induction principle for an unfolded `W`  -/
MvPFunctor.wpInd : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u_1} n} →
      {C : (x : P.last.W) → TypeVec.Arrow (P.WPath x) α → Sort v} →
        ((a : P.A) →
            (f : P.last.B a → P.last.W) →
              (f' : TypeVec.Arrow (P.WPath (WType.mk a f)) α) →
                ((i : P.last.B a) → C (f i) (P.wPathDestRight f' i)) → C (WType.mk a f) f') →
          (x : P.last.W) → (f' : TypeVec.Arrow (P.WPath x) α) → C x f'
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- The functor `hoFunctor : SSet ⥤ Cat` preserves limits of functors out of
`Discrete WalkingPair`.  -/
CategoryTheory.hoFunctor.preservesBinaryProducts : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) SSet.hoFunctor
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReprPoly : Repr Lean.Grind.CommRing.Poly
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_1.eq_1 : ∀ {β : Type u_3} {γ : Type u_1} {init : γ} (PlausibleForInStep : β → γ → ForInStep γ → Prop) (out : β)
  (motive : Subtype (PlausibleForInStep out init) → Sort u_2) (c : γ)
  (property : PlausibleForInStep out init (ForInStep.yield c))
  (h_1 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.yield c)) → motive ⟨ForInStep.yield c, property⟩)
  (h_2 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.done c)) → motive ⟨ForInStep.done c, property⟩),
  (match ⟨ForInStep.yield c, property⟩ with
    | ⟨ForInStep.yield c, property⟩ => h_1 c property
    | ⟨ForInStep.done c, property⟩ => h_2 c property) =
    h_1 c property
-- Lean.Elab.DeprecatedArg
Lean.Elab.instInhabitedDeprecatedArgEntry.default : Lean.Elab.DeprecatedArgEntry
-- Lean.Meta.Tactic.Ext
/-- The environment extension to track `@[ext]` theorems.  -/
Lean.Meta.Ext.extExtension : Lean.SimpleScopedEnvExtension Lean.Meta.Ext.ExtTheorem Lean.Meta.Ext.ExtTheorems
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft : {C : Type u} →
  (X : CategoryTheory.FreeMonoidalCategory C) →
    {Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C} → Y₁.Hom Y₂ → (X.tensor Y₁).Hom (X.tensor Y₂)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.prod : ∀ {𝕜 : 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] {z : M} {F' : Type u_21} [inst_6 : NormedCommRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {ι : Type} {t : Finset ι} {f : ι → M → F'} {f' : ι → TangentSpace I z →L[𝕜] F'}
  [inst_8 : DecidableEq ι],
  (∀ i ∈ t, HasMFDerivAt% (f i) z (f' i)) → HasMFDerivAt% (∏ i ∈ t, f i) z (∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i)
-- Mathlib.RingTheory.Discriminant
/-- If `b` is a basis of a finite separable field extension `L/K`, then `Algebra.discr K b ≠ 0`.  -/
Algebra.discr_not_zero_of_basis : ∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} [inst_2 : Field K]
  [inst_3 : Field L] [inst_4 : Algebra K L] [Module.Finite K L] [Algebra.IsSeparable K L] (b : Module.Basis ι K L),
  Algebra.discr K ⇑b ≠ 0
-- Init.Data.String.Termination
String.Pos.remainingBytes_toSlice : ∀ {s : String} {p : s.Pos}, p.toSlice.remainingBytes = p.remainingBytes