mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LocalProperties.Exactness
bijective_of_isLocalized_maximal : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6)
  [inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_6 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_7 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_7 : ∀ (P : Ideal R) [inst_7 : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)]
  (Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7) [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)]
  [inst_9 : (P : Ideal R) → [inst_9 : P.IsMaximal] → Module R (Nₚ P)]
  (g : (P : Ideal R) → [inst_10 : P.IsMaximal] → N →ₗ[R] Nₚ P)
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)] (F : M →ₗ[R] N),
  (∀ (P : Ideal R) [inst_11 : P.IsMaximal], Function.Bijective ⇑((IsLocalizedModule.map P.primeCompl (f P) (g P)) F)) →
    Function.Bijective ⇑F
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instInf : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace β] → [inst_2 : SemilatticeInf β] → [ContinuousInf β] → Min (α →ₘ[μ] β)
-- Mathlib.GroupTheory.Complement
/-- **Alias** of `Subgroup.IsComplement'.card_mul_card`. -/
Subgroup.IsComplement'.card_mul : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K → Nat.card ↥H * Nat.card ↥K = Nat.card G
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.coproducts_le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C),
  CategoryTheory.MorphismProperty.coproducts.{w, v, u} T ≤ T.rlp.llp
-- Mathlib.Topology.Algebra.AsymptoticCone
_private.Mathlib.Topology.Algebra.AsymptoticCone.0.AffineSpace.asymptoticNhds_zero' : ∀ {k : Type u_1} {V : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : TopologicalSpace V] [inst_5 : TopologicalSpace k] [OrderTopology k]
  [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V], AffineSpace.asymptoticNhds k V 0 = ⊤
-- Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
MeasureTheory.Measure.zero_one : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsZeroOneMeasure μ] (s : Set α),
  μ s = 0 ∨ μ s = 1
-- Mathlib.Tactic.CongrExclamation
/-- Like `mkCongrSimp?` but takes in a specific arity.  -/
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.congrSimp?.mkCongrSimpNArgs : Lean.Expr → ℕ → Lean.MetaM (Option Lean.Meta.CongrTheorem)
-- Init.Data.SInt.Basic
Int32.ofUInt32.inj : ∀ {toUInt32 toUInt32_1 : UInt32}, { toUInt32 := toUInt32 } = { toUInt32 := toUInt32_1 } → toUInt32 = toUInt32_1
-- Init.PropLemmas
Decidable.by_contra : ∀ {p : Prop} [Decidable p], (¬p → False) → p
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- At `-n` for `n ∈ ℕ`, the Gamma function is undefined; by convention we assign it the value `0`.
 -/
Real.Gamma_neg_nat_eq_zero : ∀ (n : ℕ), Real.Gamma (-↑n) = 0
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.two_mul_apply_root_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (B : P.InvariantForm)
  (i j : ι), 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * (B.form (P.root j)) (P.root j)
-- Batteries.Data.List.Basic
List.swapTR.go.eq_def : ∀ {α : Type u_1} (l a : List α) (a_1 a_2 : ℕ) (a_3 : Array α),
  List.swapTR.go l a a_1 a_2 a_3 =
    match a, a_1, a_2, a_3 with
    | [], x, x_1, x_2 => l
    | head :: tail, 0, 0, x => l
    | a :: xs, 0, i.succ, acc => acc.toListAppend (Function.uncurry List.cons (xs.swapAt i a))
    | a :: xs, i.succ, 0, acc => acc.toListAppend (Function.uncurry List.cons (xs.swapAt i a))
    | a :: xs, i.succ, j.succ, acc => List.swapTR.go l xs i j (acc.push a)
-- Lean.Meta.AppBuilder
/-- Given a `monad` and `e : α`, makes `pure e`. -/
Lean.Meta.mkPure : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a monoid `M` can be considered as a subsemigroup of that monoid.  -/
Submonoid.toSubsemigroup : {M : Type u_3} → [inst : MulOneClass M] → Submonoid M → Subsemigroup M
-- Mathlib.RingTheory.Nilpotent.Basic
isNilpotent_finsum : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_3} {f : ι → R},
  (∀ (b : ι), IsNilpotent (f b)) → IsNilpotent (finsum f)
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.div_conj_eq_sub_one : ∀ {p q : NNReal}, p.HolderConjugate q → p / q = p - 1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_functorPullback_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.map F (CategoryTheory.Presieve.functorPullback F (CategoryTheory.Presieve.map F R)) =
    CategoryTheory.Presieve.map F R
-- Mathlib.Tactic.Ring.Basic
/-- Constructs the expression corresponding to `.const (-n)`.
(The `.const` constructor does not check that the expression is correct.)
 -/
Mathlib.Tactic.Ring.ExProd.mkNegNat : {u : Lean.Level} →
  {α : Q(Type u)} → (sα : Q(CommSemiring «$α»)) → Q(Ring «$α») → ℕ → (e : Q(«$α»)) × Mathlib.Tactic.Ring.ExProd sα e
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.NatTrans.CommShift₂.instCompFunctor : ∀ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D] {M : Type u_6}
  [inst_3 : AddCommMonoid M] [inst_4 : CategoryTheory.HasShift C₁ M] [inst_5 : CategoryTheory.HasShift C₂ M]
  [inst_6 : CategoryTheory.HasShift D M] {G₁ G₂ G₃ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)}
  (τ : G₁ ⟶ G₂) (τ' : G₂ ⟶ G₃) (h : CategoryTheory.CommShift₂Setup D M) [inst_7 : G₁.CommShift₂ h]
  [inst_8 : G₂.CommShift₂ h] [inst_9 : G₃.CommShift₂ h] [CategoryTheory.NatTrans.CommShift₂ τ h]
  [CategoryTheory.NatTrans.CommShift₂ τ' h],
  CategoryTheory.NatTrans.CommShift₂ (CategoryTheory.CategoryStruct.comp τ τ') h
-- Mathlib.Algebra.Algebra.Spectrum.Pi
isQuasiregular_pi_iff : ∀ {ι : Type u_1} {κ : ι → Type u_5} [inst : (i : ι) → NonUnitalSemiring (κ i)] (x : (i : ι) → κ i),
  IsQuasiregular x ↔ ∀ (i : ι), IsQuasiregular (x i)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The definition of a Grothendieck topology: a set of sieves `J X` on each object `X` satisfying
three axioms:
1. For every object `X`, the maximal sieve is in `J X`.
2. If `S ∈ J X` then its pullback along any `h : Y ⟶ X` is in `J Y`.
3. If `S ∈ J X` and `R` is a sieve on `X`, then provided that the pullback of `R` along any arrow
   `f : Y ⟶ X` in `S` is in `J Y`, we have that `R` itself is in `J X`.

A sieve `S` on `X` is referred to as `J`-covering, (or just covering), if `S ∈ J X`.

See also [nlab] or [MM92] Chapter III, Section 2, Definition 1.  -/
CategoryTheory.GrothendieckTopology : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_snd' : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B],
  ⇑(ContinuousAlgHom.snd R A B) = Prod.snd
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.Slice.toList_splitToSubslice_of_isEmpty : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {σ : String.Slice → Type}
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [inst_3 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_4 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id]
  [String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat] {s : String.Slice},
  s.isEmpty = true → (s.splitToSubslice pat).toList = [s.subsliceFrom s.endPos]
-- Init.Omega.Constraint
/-- Shorthand for the first component of `normalize`.  -/
Lean.Omega.normalizeConstraint : Lean.Omega.Constraint → Lean.Omega.Coeffs → Lean.Omega.Constraint
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H2Iso_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.π
      (groupHomology.H2Iso A).inv =
    groupHomology.H2π A
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.baseChange : ∀ {R : Type u_3} {V : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (A : Type u_5)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (f : Module.Dual R V) (v : V),
  LinearMap.baseChange A (LinearMap.transvection f v) =
    LinearMap.transvection ((Module.Dual.baseChange A) f) (1 ⊗ₜ[R] v)
-- Mathlib.Topology.Algebra.MulAction
continuousSMul_inf : ∀ {M : Type u_2} {X : Type u_3} [inst : TopologicalSpace M] [inst_1 : SMul M X] {t₁ t₂ : TopologicalSpace X}
  [ContinuousSMul M X] [ContinuousSMul M X], ContinuousSMul M X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filterMap!_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filterMap! f t).isEmpty = false ↔
      ∃ k, ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true), (f k (t.get k h)).isSome = true)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Subgroup G}
  {x : MulAction.orbitRel.Quotient G α} {a b : ↑x.orbit}, ↑a ∈ MulAction.orbit ↥H ↑b ↔ a ∈ MulAction.orbit (↥H) b
-- Mathlib.FieldTheory.SeparableClosure
Function.argminOn.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (f f_1 : α → β),
  f = f_1 →
    ∀ [inst : LT β] [inst_1 : WellFoundedLT β] (s s_1 : Set α) (e_s : s = s_1) (hs : s.Nonempty),
      Function.argminOn f s hs = Function.argminOn f_1 s_1 ⋯
-- Lean.Linter.UnusedVariables
/-- The collection of all local declarations, organized by the span of the declaration.
We collapse all declarations declared at the same position into a single record using
`FVarDefinition.aliases`.  -/
Lean.Linter.UnusedVariables.References.fvarDefs : Lean.Linter.UnusedVariables.References → Std.HashMap Lean.Syntax.Range Lean.Linter.UnusedVariables.FVarDefinition
-- Mathlib.GroupTheory.Exponent
/-- The exponent of an additive group is the smallest positive integer `n` such that
`n • g = 0` for all `g ∈ G` if it exists, otherwise it is zero by convention.  -/
AddMonoid.exponent : (G : Type u) → [AddMonoid G] → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCircuit.three_le_length : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v}, p.IsCircuit → 3 ≤ p.length
-- Aesop.Saturate
Aesop.SaturateM.Context.options : Aesop.SaturateM.Context → Aesop.Options'
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instSMulCommClass : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] {S : Type u_5} {T : Type u_6}
  [inst_8 : DistribSMul S F] [inst_9 : SMulCommClass 𝕜₂ S F] [inst_10 : ContinuousConstSMul S F]
  [inst_11 : DistribSMul T F] [inst_12 : SMulCommClass 𝕜₂ T F] [inst_13 : ContinuousConstSMul T F]
  [SMulCommClass S T F], SMulCommClass S T (E →SWOT[σ] F)
-- Mathlib.GroupTheory.GroupAction.Jordan
Equiv.Perm.isMultiplyPretransitive_of_nontrivial : ∀ {α : Type u_1} {K : Type u_2} [inst : Group K] [inst_1 : MulAction K α],
  Nat.card α = 2 → MulAction.fixedPoints K α ≠ Set.univ → ∀ (n : ℕ), MulAction.IsMultiplyPretransitive K α n
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `UniqueMDiffOn` using the custom elaborator.  -/
Manifold.delabUniqueMDiffOn : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** with the Lagrange form of the remainder.

We assume that `f` is `n`-times continuously differentiable in the closed set `uIcc x₀ x` and
`n+1`-times differentiable on the open set `uIoo x₀ x`. Then there exists an `x' ∈ uIoo x₀ x` such
that
$$f(x) - (P_n f)(x₀, x) = \frac{f^{(n+1)}(x') (x - x₀)^{n+1}}{(n+1)!},$$
where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated
derivative.  -/
taylor_mean_remainder_lagrange : ∀ {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ},
  x₀ ≠ x →
    ContDiffOn ℝ (↑n) f (Set.uIcc x₀ x) →
      DifferentiableOn ℝ (iteratedDerivWithin n f (Set.uIcc x₀ x)) (Set.uIoo x₀ x) →
        ∃ x' ∈ Set.uIoo x₀ x,
          f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x =
            iteratedDerivWithin (n + 1) f (Set.uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1).factorial
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.coe_mk : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : M → N) (h1 : f 0 = 0),
  ⇑{ toFun := f, map_zero' := h1 } = f
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (f : E →SL[σ] F),
  (↑f).range = ⊤ → ∃ fsymm, 0 < fsymm.nnnorm
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.div : ∀ {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] {l : Filter α}
  {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'}, f₁ =Θ[l] g₁ → f₂ =Θ[l] g₂ → (fun x => f₁ x / f₂ x) =Θ[l] fun x => g₁ x / g₂ x
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
CommSemiring.mul_comm : ∀ {R : Type u} [self : CommSemiring R] (a b : R), a * b = b * a
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Return the possible `Trie α` that match with `keys`.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.getMatchLoop : {α : Type} →
  Array Lean.Meta.RefinedDiscrTree.PartialMatch✝ →
    Lean.Meta.RefinedDiscrTree.MatchResult α →
      Bool → Lean.Meta.RefinedDiscrTree.TreeM✝ α (Lean.Meta.RefinedDiscrTree.MatchResult α)
-- Mathlib.Tactic.FailIfNoProgress
_private.Mathlib.Tactic.FailIfNoProgress.0.Mathlib.Tactic.lctxIsDefEq.match_1.eq_4 : ∀ (motive : List (Option Lean.LocalDecl) → List (Option Lean.LocalDecl) → Sort u_1)
  (h_1 : (l₁ l₂ : List (Option Lean.LocalDecl)) → motive (none :: l₁) l₂)
  (h_2 : (l₁ l₂ : List (Option Lean.LocalDecl)) → motive l₁ (none :: l₂))
  (h_3 :
    (d₁ : Lean.LocalDecl) →
      (l₁ : List (Option Lean.LocalDecl)) →
        (d₂ : Lean.LocalDecl) → (l₂ : List (Option Lean.LocalDecl)) → motive (some d₁ :: l₁) (some d₂ :: l₂))
  (h_4 : Unit → motive [] []) (h_5 : (x x_1 : List (Option Lean.LocalDecl)) → motive x x_1),
  (match [], [] with
    | none :: l₁, l₂ => h_1 l₁ l₂
    | l₁, none :: l₂ => h_2 l₁ l₂
    | some d₁ :: l₁, some d₂ :: l₂ => h_3 d₁ l₁ d₂ l₂
    | [], [] => h_4 ()
    | x, x_1 => h_5 x x_1) =
    h_4 ()
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
ContinuousMap.toLp_injective : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  {𝕜 : Type u_3} [inst_6 : Fact (1 ≤ p)] [inst_7 : NormedRing 𝕜] [inst_8 : Module 𝕜 E] [inst_9 : IsBoundedSMul 𝕜 E]
  [μ.IsOpenPosMeasure], Function.Injective ⇑(ContinuousMap.toLp p μ 𝕜)
-- Mathlib.Order.Heyting.Basic
hnot_sup_eq_top : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α}, ￢a ⊔ a = ⊤
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_one_lt_norm : ∀ (α : Type u_2) [inst : NontriviallyNormedField α], ∃ x, 1 < ‖x‖
-- Mathlib.Topology.Category.Profinite.Basic
/-- Construct a term of `Profinite` from a type endowed with the structure of a
compact, Hausdorff and totally disconnected topological space.
 -/
Profinite.of : (X : Type u_1) → [inst : TopologicalSpace X] → [CompactSpace X] → [T2Space X] → [TotallyDisconnectedSpace X] → Profinite
-- Init.Data.Array.Basic
Array.isPrefixOfAux : {α : Type u} → [BEq α] → (as bs : Array α) → as.size ≤ bs.size → ℕ → Bool
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k fallback : α},
      (List.map Prod.fst l).contains k = false →
        (Std.DHashMap.Raw.Const.insertMany m l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vaddCommClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α γ] [inst_1 : VAdd β γ] [VAddCommClass α β γ],
  VAddCommClass (Set α) (Set β) (Set γ)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instContinuousConstSMul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : SMul M X] [inst_2 : ContinuousConstSMul M X],
  ContinuousConstSMul M (SeparationQuotient X)
-- Mathlib.Order.Lattice
Lattice.ext : ∀ {α : Type u_1} {A B : Lattice α}, (∀ (x y : α), x ≤ y ↔ x ≤ y) → A = B
-- Lean.Elab.Attributes
Lean.Elab.instInhabitedAttribute.default : Lean.Elab.Attribute
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_roc_eq_add : ∀ {m n i : ℕ}, i < n - m → (m<...=n).toArray[i]! = m + 1 + i
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.l_sup_u : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  (gi : GaloisInsertion l u) (a b : β), l (u a ⊔ u b) = a ⊔ b
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (r : ↑((↑U).presheaf.obj (Opposite.op ⊤))),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ((↑U).basicOpen r) = X.basicOpen r
-- Mathlib.FieldTheory.Minpoly.Field
/-- The minimal polynomial of an element `x` is uniquely characterized by its defining property:
if there is another monic polynomial of minimal degree that has `x` as a root, then this polynomial
is equal to the minimal polynomial of `x`. See also `minpoly.IsIntegrallyClosed.Minpoly.unique`
which relaxes the assumptions on `A` in exchange for stronger assumptions on `B`.  -/
minpoly.unique : ∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) {p : Polynomial A},
  p.Monic →
    (Polynomial.aeval x) p = 0 →
      (∀ (q : Polynomial A), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree) → p = minpoly A x
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  (i : (Module.rank F E).ord.ToType),
  FiniteDimensional
    ↥(IntermediateField.adjoin F
        (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio i))
    ↥(↥(IntermediateField.adjoin F
            (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
              Set.Iio i)))⟮(Field.Emb.Cardinal.wellOrderedBasis F E) (Field.Emb.Cardinal.leastExt F E i)⟯
-- Mathlib.Data.Fin.SuccPred
Fin.succ_succAbove_zero : ∀ {n : ℕ} [inst : NeZero n] (i : Fin n), i.succ.succAbove 0 = 0
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.LocallyOfFinitePresentation.iff_locallyOfFiniteType : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsLocallyNoetherian Y],
  AlgebraicGeometry.LocallyOfFinitePresentation f ↔ AlgebraicGeometry.LocallyOfFiniteType f
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSigma_isBasis_iff : ∀ {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {h : Pairwise (Function.onFun Disjoint fun i => (M i).E)}
  {I X : Set α},
  (Matroid.disjointSigma M h).IsBasis I X ↔
    (∀ (i : ι), (M i).IsBasis (I ∩ (M i).E) (X ∩ (M i).E)) ∧ I ⊆ X ∧ X ⊆ ⋃ i, (M i).E
-- Mathlib.Order.IsNormal
/-- **Alias** of `Order.IsNormal.ext_iff`. -/
Order.IsNormal.ext : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : SuccOrder α]
  [inst_3 : LinearOrder β] [inst_4 : OrderBot α] {g : α → β},
  Order.IsNormal f → Order.IsNormal g → (f = g ↔ f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (Order.succ a) = g (Order.succ a))
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.one_le_primesOver_ncard`. -/
one_le_primesOver_ncard : ∀ {A : Type u_4} [inst : CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [IsDedekindDomain B] [inst_3 : Algebra A B] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B],
  1 ≤ (p.primesOver B).ncard
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instIsSMulApplyReal : ∀ {R : Type u_1} {E : Type u_3} [inst : Group E] [inst_1 : SMul R ℝ] [inst_2 : SMul R NNReal]
  [inst_3 : IsScalarTower R NNReal ℝ], IsSMulApply R (GroupSeminorm E) E ℝ
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_id_left : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b),
  CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f)
      (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (F.map f)) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom)
      (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.pairMap_ne_self : ∀ (σ : Type u_1) [inst : DecidableEq σ] (t : Finset σ × σ), MvPolynomial.NewtonIdentities.pairMap✝ σ t ≠ t
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
/-- the underlying map of a `X`-continuous map  -/
Topology.ContinuousMapGeneratedBy.toFun : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} →
        [inst_1 : TopologicalSpace Y] →
          {Z : Type v'} → [inst_2 : TopologicalSpace Z] → Topology.ContinuousMapGeneratedBy X Y Z → Y → Z
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
/-- The composition of two isometries between quadratic forms.  -/
QuadraticMap.Isometry.comp : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {M₃ : Type u_5} →
        {N : Type u_7} →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M₁] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Module R M₁] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module R M₃] →
                          [inst_8 : Module R N] →
                            {Q₁ : QuadraticMap R M₁ N} →
                              {Q₂ : QuadraticMap R M₂ N} →
                                {Q₃ : QuadraticMap R M₃ N} → (Q₂ →qᵢ Q₃) → (Q₁ →qᵢ Q₂) → Q₁ →qᵢ Q₃