mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Functor.createsColimitsOfIsEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (H : CategoryTheory.Functor D C) →
          [H.IsEquivalence] → CategoryTheory.CreatesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} H
-- Mathlib.Algebra.Group.Shrink
Shrink.instGroup : {α : Type u_2} → [inst : Small.{v, u_2} α] → [Group α] → Group (Shrink.{v, u_2} α)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- A functor that preserves the colimit of `CostructuredArrow.proj L c ⋙ F` preserves
the pointwise left Kan extension of `F` along `L` at `c`.  -/
CategoryTheory.Functor.preservesPointwiseLeftKanExtensionAtOfPreservesColimit : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (c : C)
  [CategoryTheory.Limits.PreservesColimit ((CategoryTheory.CostructuredArrow.proj L c).comp F) G],
  G.PreservesPointwiseLeftKanExtensionAt F L c
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The degree of a product of polynomials is equal to
the sum of the degrees, provided that the product of leading coefficients is nonzero.

See `Polynomial.natDegree_multiset_prod` (without the `'`) for a version for integral domains,
where this condition is automatically satisfied.
 -/
Polynomial.natDegree_multiset_prod' : ∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)),
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instPow : {ι : Type u_1} → {α : Type u_2} → {M : ι → Type u_5} → [(i : ι) → Pow (M i) α] → Pow ((i : ι) → M i) α
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.induction_on_exists_not : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : {m : ℕ} → L.BoundedFormula α m → Prop}
  (φ : L.BoundedFormula α n),
  (∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ) →
    (∀ {m : ℕ} {φ : L.BoundedFormula α m}, P φ → P φ.not) →
      (∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex) →
        (∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) → P φ
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_mono : ∀ {x y : ZFSet.{u}}, x ⊆ y → x.rank ≤ y.rank
-- Mathlib.Dynamics.Flow
Flow.map_zero' : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (self : Flow τ α) (x : α), self.toFun 0 x = x
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.mk.sizeOf_spec : ∀ (content : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (priorParts : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty))
  (context : Array Lean.VersoModuleDocs.DocFrame✝),
  sizeOf { content := content, priorParts := priorParts, context := context } =
    1 + sizeOf content + sizeOf priorParts + sizeOf context
-- Mathlib.Logic.Basic
iff_iff_not_or_and_or_not : ∀ {a b : Prop}, (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)
-- Init.Prelude
/-- A way to interpret a fully-polymorphic function in `m` into `n`. Such a function can be thought of
as one that may change the effects in `m`, but can't do so based on specific values that are
provided.

Clients of `MonadFunctor` should typically use `MonadFunctorT`, which is the reflexive, transitive
closure of `MonadFunctor`. New instances should be defined for `MonadFunctor.`
 -/
MonadFunctor : semiOutParam (Type u → Type v) → (Type u → Type w) → Type (max (max (u + 1) v) w)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.neg_hom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B),
  Rep.Hom.hom (-f) = -Rep.Hom.hom f
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
isSquare_mabs : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] {a : α}, IsSquare |a|ₘ ↔ IsSquare a
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instCommMonoid : {α : Type u_1} → [CommMonoid α] → CommMonoid αᵒᵈ
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `getD` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.getDₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → [Std.OrientedOrd α] → [Std.LawfulEqOrd α] → (k : α) → Std.DTreeMap.Internal.Impl α β → β k → β k
-- Mathlib.Tactic.Eval
/-- `eval% x` evaluates the term `x : X` in the interpreter, and then injects the resulting expression.

As an example:
```lean
example : 2^10 = eval% 2^10 := by
  -- goal is `2^10 = 1024`
  sorry
```
This only works if a `Lean.ToExpr X` instance is available.

Tip: you can use `show_term eval% x` to see the value of `eval% x`.
 -/
Mathlib.Meta.elabEvalExpr : Lean.Elab.Term.TermElab
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_terminates_of_get?_terminates : ∀ {α : Type u} {s : Stream'.WSeq α} {n : ℕ}, (s.get? n).Terminates → s.destruct.Terminates
-- Mathlib.Order.Interval.Multiset
Multiset.Ioc.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), Multiset.Ioc a b = (Finset.Ioc a b).val
-- Mathlib.Algebra.Free
FreeAddMagma.length.eq_1 : ∀ {α : Type u} (x_1 : α), (FreeAddMagma.of x_1).length = 1
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (state : Std.Mutex (Std.Bounded.State✝ α)) (id : ℕ),
  sizeOf { state := state, id := id } = 1 + sizeOf state + sizeOf id
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Icc_sub_one_right_eq_Ico_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {b : α}, ¬IsMin b → ∀ (a : α), Finset.Icc a (b - 1) = Finset.Ico a b
-- Mathlib.Data.Finite.Defs
Set.Infinite.not_finite : ∀ {α : Type u} {s : Set α}, s.Infinite → ¬s.Finite
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.multisetProd_map : ∀ {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Multiset α},
  (∀ x ∈ s, f x ≡ g x [MOD n]) → (Multiset.map f s).prod ≡ (Multiset.map g s).prod [MOD n]
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- This is a specific lemma used in the proof of `partialTraj_eq_prod`. It is the main rewrite step
and stating it as a separate lemma avoids using extensionality of kernels, which would generate
a lot of measurability subgoals.  -/
_private.Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj.0.ProbabilityTheory.Kernel.fst_prod_comp_id_prod : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} (κ : ProbabilityTheory.Kernel X Y) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (X × Y) Z) [ProbabilityTheory.IsSFiniteKernel η],
  ((ProbabilityTheory.Kernel.deterministic Prod.fst ⋯).prod η).comp (ProbabilityTheory.Kernel.id.prod κ) =
    ProbabilityTheory.Kernel.id.prod (η.comp (ProbabilityTheory.Kernel.id.prod κ))
-- Mathlib.Data.Fintype.Order
Finite.map_iSup_of_monotone : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] (f : ι → α) {g : α → β},
  Monotone g → g (⨆ i, f i) = ⨆ i, g (f i)
-- Mathlib.CategoryTheory.FinCategory.Basic
CategoryTheory.instFiniteDiscrete : ∀ {α : Type u_1} [Finite α], Finite (CategoryTheory.Discrete α)
-- Mathlib.Topology.Bases
/-- A second-countable space is one with a countable basis.  -/
SecondCountableTopology : (α : Type u) → [t : TopologicalSpace α] → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.edgeMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x y : C}, Function.Surjective CategoryTheory.nerve.edgeMk
-- Aesop.Tree.Data
Aesop.Rapp.setAppliedRule : Aesop.RegularRule → Aesop.Rapp → Aesop.Rapp
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedInfoState : Inhabited Lean.Elab.InfoState
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.DTreeMap.Const.minEntryD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α × β → α × β
-- Mathlib.Algebra.Order.Floor.Div
Pi.ceilDiv_def : ∀ {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : (i : ι) → AddCommMonoid (π i)] [inst_3 : (i : ι) → PartialOrder (π i)]
  [inst_4 : (i : ι) → SMulZeroClass α (π i)] [inst_5 : (i : ι) → CeilDiv α (π i)] (f : (i : ι) → π i) (a : α),
  f ⌈/⌉ a = fun i => f i ⌈/⌉ a
-- Lean.Parser.Term
Lean.Parser.Term.letPatDecl : optParam Bool false → Lean.Parser.Parser
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.quotient : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FormallyUnramified R A] (I : Ideal A), Algebra.FormallyUnramified R (A ⧸ I)
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
AffineMap.restrict.injective : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂},
  Function.Injective ⇑φ →
    ∀ {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} [inst_7 : Nonempty ↥E] [inst_8 : Nonempty ↥F]
      (hEF : AffineSubspace.map φ E ≤ F), Function.Injective ⇑(φ.restrict hEF)
-- Mathlib.Data.Multiset.Dedup
Multiset.count_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (a : α), Multiset.count a m.dedup = if a ∈ m then 1 else 0
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.associated_gcd_gcd : ∀ (R : Type u) [inst : CommRing R] {x y : R} [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})]
  [inst_2 : GCDMonoid R], Associated (IsBezout.gcd x y) (gcd x y)
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetsExtEntry : Type
-- Init.System.IO
/-- Types of files that may be found on a filesystem.  -/
IO.FS.FileType : Type
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coeff_comapDomain : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f)
  (x : AddMonoidAlgebra R N), (AddMonoidAlgebra.comapDomain f hf x).coeff = Finsupp.comapDomain f x.coeff ⋯
-- Lean.LabelAttribute
/-- An environment extension that just tracks an array of names.  -/
Lean.LabelExtension : Type
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.flippingIso_inv_toFunctor_map_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  {F₁ F₂ : CategoryTheory.Functor D (CategoryTheory.Functor C E)} (φ : F₁ ⟶ F₂) (Y : C) (X : D),
  ((CategoryTheory.flippingIso.inv.toFunctor.map φ).app Y).app X = (φ.app X).app Y
-- Std.Http.Internal.Char
_private.Std.Http.Internal.Char.0.Std.Http.Internal.Char.qdtext.match_1.eq_1 : ∀ (motive : Char → Sort u_1) (h_1 : Unit → motive '\t') (h_2 : Unit → motive ' ') (h_3 : Unit → motive '!')
  (h_4 : (x : Char) → motive x),
  (match '\t' with
    | '\t' => h_1 ()
    | ' ' => h_2 ()
    | '!' => h_3 ()
    | x => h_4 x) =
    h_1 ()
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExcept_neg : ∀ (L : PeriodPair) (l₀ z : ℂ), L.weierstrassPExcept l₀ (-z) = L.weierstrassPExcept (-l₀) z
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.iso_symm_comp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f], ↑(IsLocalizedModule.iso S f).symm ∘ₗ f = LocalizedModule.mkLinearMap S M
-- Lean.Server.FileWorker.InlayHints
Lean.Elab.InlayHintLinkLocation.toLspLocation : Lean.FileMap → Lean.Elab.InlayHintLinkLocation → IO (Option Lean.Lsp.Location)
-- Init.Data.ByteArray.Basic
ByteArray.findIdx?.loop : ByteArray → (UInt8 → Bool) → ℕ → Option ℕ
-- Init.Data.String.Decode
List.utf8DecodeChar?_utf8Encode_singleton : ∀ {c : Char}, [c].utf8Encode.utf8DecodeChar? 0 = some c
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.functorPushforward_overForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {S : C} {X : CategoryTheory.Over S}
  (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.functorPushforward (CategoryTheory.Over.forget S) R =
    (CategoryTheory.Sieve.generate (CategoryTheory.Presieve.map (CategoryTheory.Over.forget S) R)).arrows
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- If `adj : F ⊣ G`, and `Y : D`, then `G.obj Y` represents `X ↦ (F.obj X ⟶ Y)`.  -/
CategoryTheory.Adjunction.representableBy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) → (Y : D) → (F.op.comp (CategoryTheory.yoneda.obj Y)).RepresentableBy (G.obj Y)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.SeparatingLeft.ne_zero : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} [Nontrivial M₁] {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M}, B.SeparatingLeft → B ≠ 0
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.eq_symm_apply : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) {x : α} {y : β},
  x = h.symm y ↔ h x = y
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
deriv_exp : ∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → deriv (fun x => Real.exp (f x)) x = Real.exp (f x) * deriv f x
-- Mathlib.Order.Hom.Basic
OrderIso.ofSurjective_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (f : α ↪o β) (hf : Function.Surjective ⇑f) (b : β),
  (RelIso.symm (OrderIso.ofSurjective f hf)) b = Function.surjInv ⋯ b
-- Mathlib.Data.Num.Basic
/-- Converts a `ZNum` to a `PosNum`, mapping all out of range values to `1`.  -/
PosNum.ofZNum : ZNum → PosNum
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_sub_cancel_left : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {a : α}, IsAddUnit a → ∀ (b : α), a + b - a = b
-- Std.Async.Process
/-- Size of unshared stack segment (kilobytes)
 -/
Std.IO.Process.ResourceUsageStats.unsharedStackSizeKb : Std.IO.Process.ResourceUsageStats → UInt64
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_insert_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  Submodule.span R (insert 0 s) = Submodule.span R s
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_bind_getKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((Std.Internal.List.maxKey? l).bind fun k => Std.Internal.List.getKey? k l) = Std.Internal.List.maxKey? l
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.eqToHom_comp_homOfLE_op : ∀ {X : Type u} [inst : Preorder X] {a b c : X} (hab : Opposite.op a = Opposite.op b) (hbc : c ≤ b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.homOfLE hbc).op =
    (CategoryTheory.homOfLE ⋯).op
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_div : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (x y : ↥S), ↑(x / y) = ↑x / ↑y
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_add_eq_bot_iff : ∀ {α : Type u} [inst : Add α] {y : WithBot α} {a : α}, ↑a + y = ⊥ ↔ y = ⊥
-- Mathlib.Order.SuccPred.Limit
IsGLB.mem_of_not_isPredLimit : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α] {s : Set α}, IsGLB s a → s.Nonempty → ¬Order.IsPredLimit a → a ∈ s
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.instPreservesLimitsOfShapeOpensWalkingCospanOpensFunctor : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan
    (AlgebraicGeometry.Scheme.Hom.opensFunctor f)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.lowerCrossingTime_stabilize' : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n m : ℕ} {ω : Ω},
  n ≤ m → N ≤ MeasureTheory.lowerCrossingTime a b f N n ω → MeasureTheory.lowerCrossingTime a b f N m ω = N
-- Mathlib.FieldTheory.Galois.Profinite
/-- The projection map from `lim Gal(L/k)` to a specific `Gal(L/k)`.  -/
InfiniteGalois.proj : {k : Type u_3} →
  {K : Type u_4} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          (L : FiniteGaloisIntermediateField k K) →
            ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop →*
              Gal(↥L.toIntermediateField/k)
-- Init.Grind.Norm
Lean.Grind.not_or : ∀ (p q : Prop), (¬(p ∨ q)) = (¬p ∧ ¬q)
-- Mathlib.Topology.Order
isOpen_induced : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set β}, IsOpen s → IsOpen (f ⁻¹' s)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- See also `ENNReal.limsup_mul_le`.  -/
ENNReal.limsup_mul_le' : ∀ {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal},
  Filter.limsup u f ≠ 0 ∨ Filter.limsup v f ≠ ⊤ →
    Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ 0 → Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
-- Mathlib.Data.Set.Basic
Set.decidableUnion : {α : Type u} → (s t : Set α) → (a : α) → [Decidable (a ∈ s)] → [Decidable (a ∈ t)] → Decidable (a ∈ s ∪ t)
-- Mathlib.Control.Monad.Cont
MonadCont.Label.mk.injEq : ∀ {α : Type w} {m : Type u → Type v} {β : Type u} (apply apply_1 : α → m β),
  ({ apply := apply } = { apply := apply_1 }) = (apply = apply_1)
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.lsum_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R A] [inst_4 : Module R M] (f : ℕ → A →ₗ[R] M) (p : Polynomial A),
  (Polynomial.lsum f) p = p.sum fun x1 x2 => (f x1) x2
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.intEquivalence_inverse_map_hom : ∀ {X Y : RingCat} (f : X ⟶ Y), AlgCat.Hom.hom (AlgCat.intEquivalence.inverse.map f) = (RingCat.Hom.hom f).toIntAlgHom
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.id.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), Algebra.Generators.Hom.id P = { val := MvPolynomial.X, aeval_val := ⋯ }
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.IndepFun (∑ j ∈ s, f j) (f i) μ
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofNat.inj : ∀ {n n_1 : ℕ}, Lean.LeanOptionValue.ofNat n = Lean.LeanOptionValue.ofNat n_1 → n = n_1
-- Mathlib.Algebra.WithConv
WithConv.ofConv_toConv : ∀ {A : Type u_2} (x : A), (WithConv.toConv x).ofConv = x
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.rank_empty : ∀ {a : ℕ}, Batteries.UnionFind.empty.rank a = 0
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain.addMonoidHom_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α → β) (v : α →₀ M),
  (Finsupp.mapDomain.addMonoidHom f) v = Finsupp.mapDomain f v
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.eval_eq_πJ : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I) (l : Profinite.NobelingProof.Products I),
  Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun x => x ∈ s) l →
    Profinite.NobelingProof.Products.eval C l =
      (Profinite.NobelingProof.πJ C s)
        (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => x ∈ s) l)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstr.mk.sizeOf_spec : ∀ (p : Lean.Grind.Linarith.Poly) (h : Lean.Meta.Grind.Arith.Linear.EqCnstrProof),
  sizeOf { p := p, h := h } = 1 + sizeOf p + sizeOf h
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- An action of a group is quasipreprimitive if any normal subgroup
that has no fixed point acts pretransitively  -/
MulAction.IsQuasiPreprimitive : (G : Type u_1) → (X : Type u_2) → [inst : Group G] → [MulAction G X] → Prop
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `NormedAddCommGroup E` instance from a `NormedSpace.Core` on a type
that already has an existing topology. This requires a proof that the uniformity
induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances].  -/
NormedAddCommGroup.ofCoreReplaceTopology : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : Norm E] →
            [T : TopologicalSpace E] →
              (core : NormedSpace.Core 𝕜 E) →
                T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace → NormedAddCommGroup E
-- Mathlib.Algebra.Polynomial.Basic
/-- The set of all `n` such that `X^n` has a non-zero coefficient.  -/
Polynomial.support : {R : Type u} → [inst : Semiring R] → Polynomial R → Finset ℕ
-- Mathlib.Data.Finset.Image
Finset.coe_map_subset_range : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α), ↑(Finset.map f s) ⊆ Set.range ⇑f
-- Mathlib.Order.Interval.Set.ProjIcc
Set.strictMonoOn_projIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b), StrictMonoOn (Set.projIcc a b h) (Set.Icc a b)
-- Mathlib.RingTheory.Derivation.Basic
/-- Pushing a derivation forward through a linear equivalence is an equivalence.  -/
LinearEquiv.compDer : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] →
                  {N : Type u_5} →
                    [inst_6 : AddCommMonoid N] →
                      [inst_7 : Module A N] →
                        [inst_8 : Module R N] →
                          [inst_9 : IsScalarTower R A M] →
                            [inst_10 : IsScalarTower R A N] → (M ≃ₗ[A] N) → Derivation R A M ≃ₗ[A] Derivation R A N
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.Monad C) (x_1 : C),
  ((CategoryTheory.Monad.monadMonEquiv C).unitIso.inv.app x).app x_1 =
    CategoryTheory.CategoryStruct.id
      ((((CategoryTheory.Monad.monadToMon C).comp (CategoryTheory.Monad.monToMonad C)).obj x).obj x_1)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.sub.match_3.splitter : (motive : ONote → ONote → Sort u_1) →
  (x x_1 : ONote) →
    ((x : ONote) → motive ONote.zero x) →
      ((o : ONote) → (o = ONote.zero → False) → motive o ONote.zero) →
        ((e₁ : ONote) →
            (n₁ : ℕ+) → (a₁ e₂ : ONote) → (n₂ : ℕ+) → (a₂ : ONote) → motive (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)) →
          motive x x_1
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_one_is_mod : ∀ (x : ℕ), x &&& 1 = x % 2