mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.StateTransition
StateTransition.EvalsTo.mk.inj : ∀ {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} {steps : ℕ}
  {evals_in_steps : (flip bind f)^[steps] (some a) = b} {steps_1 : ℕ}
  {evals_in_steps_1 : (flip bind f)^[steps_1] (some a) = b},
  { steps := steps, evals_in_steps := evals_in_steps } = { steps := steps_1, evals_in_steps := evals_in_steps_1 } →
    steps = steps_1
-- Mathlib.CategoryTheory.Limits.IsConnected
CategoryTheory.Limits.Types.instSubsingletonColimitPUnit : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsPreconnected C]
  [inst_2 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.Types.constPUnitFunctor C)],
  Subsingleton (CategoryTheory.Limits.colimit (CategoryTheory.Limits.Types.constPUnitFunctor C))
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResultCore : Type
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_mul_single_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] (x : AddMonoidAlgebra R M) (r : R)
  (m : M), (x * AddMonoidAlgebra.single 0 r).coeff m = x.coeff m * r
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_map_prod : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {B : Type u_2} [inst_12 : PartialOrder B] [inst_13 : NonUnitalRing B]
  [inst_14 : TopologicalSpace B] [inst_15 : StarRing B] [inst_16 : Module ℝ B] [inst_17 : SMulCommClass ℝ B B]
  [inst_18 : IsScalarTower ℝ B B] [inst_19 : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint]
  [inst_20 : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsSemitopologicalRing B] [T2Space B]
  [inst_23 : NonnegSpectrumClass ℝ B] [inst_24 : NonnegSpectrumClass ℝ (A × B)] [inst_25 : StarOrderedRing B] {a : A}
  {b : B} {x : NNReal},
  autoParam (0 ≤ a) CFC.nnrpow_map_prod._auto_1 →
    autoParam (0 ≤ b) CFC.nnrpow_map_prod._auto_3 → CFC.nnrpow (a, b) x = (a ^ x, b ^ x)
-- Lean.Server.Requests
Lean.Server.RequestContext.mk : Std.TreeMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare →
  Lean.Server.FileWorker.EditableDocument →
    IO.FS.Stream →
      Lean.Lsp.InitializeParams →
        Lean.Server.RequestCancellationToken → Lean.Server.ServerRequestEmitter → Lean.Server.RequestContext
-- Mathlib.Order.Filter.Cofinite
Filter.cofinite_neBot : ∀ {α : Type u_2} [Infinite α], Filter.cofinite.NeBot
-- Mathlib.Topology.Separation.Basic
/-- A point with a finite neighborhood has to be isolated.  -/
isOpen_singleton_of_finite_mem_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] (x : X) {s : Set X}, s ∈ nhds x → s.Finite → IsOpen {x}
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sign_excenterWeights_singleton_neg : ∀ {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 : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), SignType.sign (s.excenterWeights {i} i) = -1
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'}
  {c' : 𝕜'}, HasDerivAt c c' x → HasDerivAt f f' x → HasDerivAt (c • f) (c x • f' + c' • f x) x
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- `nthRoots n` as a `Finset` is equal to the union of `primitiveRoots i R` for `i ∣ n`.  -/
IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DecidableEq R] {n : ℕ},
  Polynomial.nthRootsFinset n 1 = n.divisors.biUnion fun i => primitiveRoots i R
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.isValidPercentEncoding.loop.eq_def : ∀ (ba : ByteArray) (i : ℕ),
  Std.Http.URI.isValidPercentEncoding.loop✝ ba i =
    if h : i < ba.size then
      have c := ba[i];
      if c = '%'.toUInt8 then
        if h₂ : i + 2 < ba.size then
          have d1 := ba[i + 1];
          have d2 := ba[i + 2];
          if (Std.Http.Internal.Char.isHexDigitByte d1 && Std.Http.Internal.Char.isHexDigitByte d2) = true then
            Std.Http.URI.isValidPercentEncoding.loop✝ ba (i + 3)
          else false
        else false
      else Std.Http.URI.isValidPercentEncoding.loop✝ ba (i + 1)
    else true
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.revMatchesAt_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt p pos ↔ ∃ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯)
-- Mathlib.Order.Atoms
isAtom_dual_iff_isCoatom : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, IsAtom (OrderDual.toDual a) ↔ IsCoatom a
-- Mathlib.Tactic.ClickSuggestions.FindPremises
Mathlib.Tactic.ClickSuggestions.Choice.mk.injEq : ∀ (rw grw app appAt rw_1 grw_1 app_1 appAt_1 : Bool),
  ({ rw := rw, grw := grw, app := app, appAt := appAt } =
      { rw := rw_1, grw := grw_1, app := app_1, appAt := appAt_1 }) =
    (rw = rw_1 ∧ grw = grw_1 ∧ app = app_1 ∧ appAt = appAt_1)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instUniqueOfSubsingleton : {M : Type u_1} → [inst : AddZeroClass M] → [Subsingleton M] → Unique (AddSubmonoid M)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.sum_single_index : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid N] {m : M} {r : R}
  {h : M → R → N}, h m 0 = 0 → (AddMonoidAlgebra.single m r).coeff.sum h = h m r
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.δ_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex (n + 1) x) (i : Fin (n + 2)),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i) f.map = SSet.const x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.neg.eq_1 : ∀ (E : Type u_6) [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E],
  ContinuousAddMonoidHom.neg E = { toAddMonoidHom := negAddMonoidHom, continuous_toFun := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.rightUnitorNatIso_inv_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitorNatIso a b).inv.app X = (CategoryTheory.Bicategory.rightUnitor X).inv
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.rightOp_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 Y : C} (f : X ⟶ Y), F.rightOp.map f = (F.map f.op).op
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.eq_empty_iff_forall_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t = ∅ ↔ ∀ (a : α), t.contains a = false
-- Mathlib.CategoryTheory.Sites.Sieves
/-- `Sieve.shrinkFunctor` is compatible with universe lifting.  -/
CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (S : CategoryTheory.Sieve X) →
        [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
          [inst_2 : CategoryTheory.LocallySmall.{max w' w, v₁, u₁} C] →
            (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor.comp CategoryTheory.uliftFunctor.{w', w} ≅
              (CategoryTheory.Sieve.shrinkFunctor.{max w' w, v₁, u₁} S).toFunctor
-- Init.Data.Slice.Array.Lemmas
Array.toList_mkSlice_rci : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ},
  Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = List.drop lo xs.toList
-- Init.Data.Array.Subarray
/-- Shrinks the subarray by incrementing its starting index if possible, returning it unchanged if not.

Examples:
* `#[1,2,3].toSubarray.popFront.toArray = #[2, 3]`
* `#[1,2,3].toSubarray.popFront.popFront.toArray = #[3]`
* `#[1,2,3].toSubarray.popFront.popFront.popFront.toArray = #[]`
* `#[1,2,3].toSubarray.popFront.popFront.popFront.popFront.toArray = #[]`
 -/
Subarray.popFront : {α : Type u_1} → Subarray α → Subarray α
-- Mathlib.RepresentationTheory.Maschke
/-- This also implies instances `ComplementedLattice (Submodule k[G] V)` and
`IsSemisimpleRing k[G]`.  -/
MonoidAlgebra.Submodule.instIsSemisimpleModule : ∀ {k : Type u_1} [inst : Field k] {G : Type u_2} [Finite G] [NeZero ↑(Nat.card G)] [inst_3 : Group G] {V : Type u_3}
  [inst_4 : AddCommGroup V] [inst_5 : Module (MonoidAlgebra k G) V], IsSemisimpleModule (MonoidAlgebra k G) V
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α}
  {h' : k ∈ Std.DTreeMap.map f t}, (Std.DTreeMap.map f t).get k h' = f k (t.get k ⋯)
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.iterateKer_coe : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f : M →ₗ[R] M)
  (n : ℕ), f.iterateKer n = (f ^ n).ker
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Over.instCreatesLimitsOfShapeTopOverDiscretePEmptyForgetOfContainsIdentitiesOfRespectsIso : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      (X : T) →
        [P.ContainsIdentities] →
          [P.RespectsIso] →
            CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
              (CategoryTheory.MorphismProperty.Over.forget P ⊤ X)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length_one : ∀ {α : Type u_1}, FreeMonoid.length 1 = 0
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.shiftMap_homologyFunctor_map_Qh : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : HomotopyCategory C (ComplexShape.up ℤ)} {n : ℤ}
  (f : K ⟶ (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj L) (a a' : ℤ)
  (h : autoParam (n + a = a') DerivedCategory.shiftMap_homologyFunctor_map_Qh._auto_1),
  (DerivedCategory.homologyFunctor C 0).shiftMap (CategoryTheory.ShiftedHom.map f DerivedCategory.Qh) a a' h =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactorsh C a).hom.app K)
      (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
        ((DerivedCategory.homologyFunctorFactorsh C a').inv.app L))
-- Init.Data.BitVec.Bitblast
/-- Addition of bitvectors is the same as bitwise or, if bitwise and is zero.  -/
BitVec.add_eq_or_of_and_eq_zero : ∀ {w : ℕ} (x y : BitVec w), x &&& y = 0#w → x + y = x ||| y
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
/-- Alternative formulation of `covariant_sequence_exact₂`  -/
CategoryTheory.Abelian.Ext.covariant_sequence_exact₂' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (n : ℕ),
      { X₁ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext X S.X₁ n),
          X₂ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext X S.X₂ n),
          X₃ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext X S.X₃ n),
          f := AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.f).postcomp X ⋯),
          g := AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.g).postcomp X ⋯), zero := ⋯ }.Exact
-- Mathlib.Topology.Separation.Basic
minimal_nonempty_closed_subsingleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X},
  IsClosed s → (∀ t ⊆ s, t.Nonempty → IsClosed t → t = s) → s.Subsingleton
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'_one : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS' b c d 1 = 1
-- Mathlib.Order.Basic
Preorder.toLE_injective_iff : ∀ {α : Type u_2} {a₁ a₂ : Preorder α}, a₁ = a₂ ↔ a₁.toLE = a₂.toLE
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.mkIso_inv_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S S' : CategoryTheory.Span Wₗ Wᵣ c c'} (e : S.apex ≅ S'.apex)
  (hₗ : autoParam (CategoryTheory.CategoryStruct.comp e.hom S'.l = S.l) CategoryTheory.Span.mkIso._auto_1)
  (hᵣ : autoParam (CategoryTheory.CategoryStruct.comp e.hom S'.r = S.r) CategoryTheory.Span.mkIso._auto_3),
  (CategoryTheory.Span.mkIso e hₗ hᵣ).inv.hom = e.inv
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_mk : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] (f : α → β) (h : Continuous f)
  (h' :
    ∃ C,
      ∀ (x y : α),
        dist ({ toFun := f, continuous_toFun := h }.toFun x) ({ toFun := f, continuous_toFun := h }.toFun y) ≤ C),
  ⇑{ toFun := f, continuous_toFun := h, map_bounded' := h' } = f
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {a b c : α},
  a ≠ b → a ≠ c → Equiv.swap a b * Equiv.swap a c ∈ Subgroup.closure {σ | σ.IsThreeCycle}
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAtFilter_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : One F] (L : Filter (E × E)), HasFDerivAtFilter 1 0 L
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instFullKaroubiToKaroubi : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C], (CategoryTheory.Idempotents.toKaroubi C).Full
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.logEmbedding_fundSystem : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (i : Fin (NumberField.Units.rank K)),
  (NumberField.Units.logEmbedding K) (Additive.ofMul (NumberField.Units.fundSystem K i)) =
    ↑((NumberField.Units.basisUnitLattice K) i)
-- Mathlib.NumberTheory.Dioph
/-- A set `S ⊆ ℕ^α` is Diophantine if there exists a polynomial on
`α ⊕ β` such that `v ∈ S` iff there exists `t : ℕ^β` with `p (v, t) = 0`.  -/
Dioph : {α : Type u} → Set (α → ℕ) → Prop
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toContinuousAddMonoidHom_sub : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_8 : IsTopologicalAddGroup M₂]
  (f g : M →SL[σ₁₂] M₂), ↑(f - g) = ↑f - ↑g
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Subrings of a ring form a complete lattice.  -/
Subring.instCompleteLattice : {R : Type u} → [inst : NonAssocRing R] → CompleteLattice (Subring R)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Complex.slitPlane.eq_1 : Complex.slitPlane = {z | 0 < z.re ∨ z.im ≠ 0}
-- Init.Data.Fin.Lemmas
Fin.val_castLE : ∀ {n m : ℕ} (h : n ≤ m) (i : Fin n), ↑(Fin.castLE h i) = ↑i
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.Monadic.isPlausibleOutput_next : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  {it : Std.IterM Id α}, it.internalState.next = some a → a < it.internalState.upperBound → it.IsPlausibleOutput a
-- Mathlib.Data.Nat.Totient
Nat.totient_even : ∀ {n : ℕ}, 2 < n → Even n.totient
-- Mathlib.Topology.Homotopy.HSpaces
IsTopologicalAddGroup.hSpace : (G : Type u) → [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [IsTopologicalAddGroup G] → HSpace G
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Filter.Tendsto.congr_dist : ∀ {α : Type u} {ι : Type u_2} [inst : PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α},
  Filter.Tendsto f₁ p (nhds a) → Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0) → Filter.Tendsto f₂ p (nhds a)
-- Mathlib.FieldTheory.Galois.Infinite
/-- The Galois correspondence from intermediate fields to closed subgroups.  -/
InfiniteGalois.IntermediateFieldEquivClosedSubgroup : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] → [IsGalois k K] → IntermediateField k K ≃o (ClosedSubgroup Gal(K/k))ᵒᵈ
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- Multiplying a polynomial by a linear term `X - η` adds at least one sign change. This is the
basis for the induction in `roots_countP_pos_le_signVariations`.  -/
Polynomial.succ_signVariations_le_X_sub_C_mul : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {P : Polynomial R} {η : R},
  0 < η → P ≠ 0 → P.signVariations + 1 ≤ ((Polynomial.X - Polynomial.C η) * P).signVariations
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_obj : ∀ {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]
  [inst_4 : CategoryTheory.MonoidalClosed V] (F G : CategoryTheory.Functor C V) (c : C) (X : Cᵒᵖ) (X_1 : C),
  ((((CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj X).obj X_1 =
    (F.obj (Opposite.unop X) ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1 c))
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.liftLinear_apply₀ : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β}
  (hf : ∀ (μ : MeasureTheory.Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory) {s : Set β},
  MeasureTheory.NullMeasurableSet s ((MeasureTheory.Measure.liftLinear f hf) μ) →
    ((MeasureTheory.Measure.liftLinear f hf) μ) s = (f μ.toOuterMeasure) s
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one : ∀ {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [inst : SeminormedGroup G] {f : ι → κ → G} {l : Filter ι}
  {l' : Filter κ},
  UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun n z => (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_le_size_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  m.size ≤ (m.erase k).size + 1
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.sigmaImp.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (m : ℕ) (φ : L.BoundedFormula α m) (n : ℕ) (ψ : L.BoundedFormula α n),
  FirstOrder.Language.BoundedFormula.sigmaImp ⟨m, φ⟩ ⟨n, ψ⟩ = if h : m = n then ⟨m, φ.imp (⋯.mp ψ)⟩ else default
-- Lean.Syntax
Lean.Syntax.modifyArgs : Lean.Syntax → (Array Lean.Syntax → Array Lean.Syntax) → Lean.Syntax
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
schwartz_withSeminorms : ∀ (𝕜 : Type u_2) (E : Type u_5) (F : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F], WithSeminorms (schwartzSeminormFamily 𝕜 E F)
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- Special case of `MeromorphicOn.intervalIntegrable_log`: The function `log ∘ sin` is interval
integrable over every interval.
 -/
intervalIntegrable_log_sin : ∀ {a b : ℝ}, IntervalIntegrable (Real.log ∘ Real.sin) MeasureTheory.volume a b
-- Mathlib.Algebra.Tropical.Basic
Tropical.injective_untrop : ∀ {R : Type u}, Function.Injective Tropical.untrop
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The inclusion `X₁ i₁ ⊗ X₂ i₂ ⊗ X₃ i₃ ⟶ tensorObj (tensorObj X₁ X₂) X₃ j`
when `i₁ + i₂ + i₃ = j`.  -/
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) →
            [inst_3 : X₁.HasTensor X₂] →
              [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] →
                (i₁ i₂ i₃ j : I) →
                  i₁ + i₂ + i₃ = j →
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj
                        (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂)) (X₃ i₃) ⟶
                      CategoryTheory.GradedObject.Monoidal.tensorObj
                        (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- Stitching together limiting cones gives a limiting cone.  -/
CategoryTheory.Limits.combinedIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.combineCones F c)
-- Mathlib.Algebra.Lie.Weights.Basic
/-- The proposition that a weight of a Lie module is zero.

We make this definition because we cannot define a `Zero (Weight R L M)` instance since the weight
space of the zero function can be trivial.  -/
LieModule.Weight.IsZero : {R : Type u_2} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] → [inst_7 : LieRing.IsNilpotent L] → LieModule.Weight R L M → Prop
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.comm : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β}, m₁.Equiv m₂ ↔ m₂.Equiv m₁