mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Iio_add_one_comm : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : LinearOrder α] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : Add α] [inst_4 : One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M),
  ∏ i < a + 1, f i = f a * ∏ i < a, f i
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.one_le_of_lt_one : ∀ {K : Type u_1} [inst : Field K] [NumberField K] {w : NumberField.InfinitePlace K} {a : NumberField.RingOfIntegers K},
  a ≠ 0 → (∀ ⦃z : NumberField.InfinitePlace K⦄, z ≠ w → z ↑a < 1) → 1 ≤ w ↑a
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.tmul_add : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M) (n₁ n₂ : N),
  m ⊗ₜ[R] (n₁ + n₂) = m ⊗ₜ[R] n₁ + m ⊗ₜ[R] n₂
-- Std.Data.TreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than or equal to the given key.
 -/
Std.TreeMap.getEntryGE : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.TreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → α × β
-- Init.Data.List.Sublist
List.prefix_of_prefix_length_le : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → l₁.length ≤ l₂.length → l₁ <+: l₂
-- Lean.Setup
Lean.instToJsonModuleArtifacts.toJson : Lean.ModuleArtifacts → Lean.Json
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.totalDegree : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ},
  φ.IsHomogeneous n → φ ≠ 0 → φ.totalDegree = n
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.iterate_le_of_map_le_add_int : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ}, f x ≤ x + ↑m → ∀ (n : ℕ), (⇑f)^[n] x ≤ x + ↑n * ↑m
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.equivFnOfDiscrete_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : DiscreteTopology α]
  (f : α → β), ⇑(ContinuousMap.equivFnOfDiscrete.symm f) = f
-- Mathlib.RingTheory.SimpleModule.Isotypic
bot_lt_isotypicComponent : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submodule R M)
  [IsSimpleModule R ↥S], ⊥ < isotypicComponent R M ↥S
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- The additive `p`-adic valuation on `ℚ_[p]`, as an `addValuation`.  -/
Padic.addValuation : {p : ℕ} → [hp : Fact (Nat.Prime p)] → AddValuation ℚ_[p] (WithTop ℤ)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_union : ∀ {α : Type u} [inst : Semiring α] (s t : Set α), Ideal.span (s ∪ t) = Ideal.span s ⊔ Ideal.span t
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
/-- The Iwasawa structure of `alternatingGroup α` acting on `Set.powersetCard α 3`.  -/
alternatingGroup.iwasawaStructure_three : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] → MulAction.IwasawaStructure ↥(alternatingGroup α) ↑(Set.powersetCard α 3)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sub_eq_of_lt_left : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v y < v x → v (x - y) = v x
-- Init.Data.Int.DivMod.Lemmas
Int.emod_minus_one : ∀ (a : ℤ), a % -1 = 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- An isomorphism `S ≅ S'` induces an equivalence `StructuredArrow S T ≌ StructuredArrow S' T`.  -/
CategoryTheory.StructuredArrow.mapIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S S' : D} →
          {T : CategoryTheory.Functor C D} →
            (S ≅ S') → (CategoryTheory.StructuredArrow S T ≌ CategoryTheory.StructuredArrow S' T)
-- Mathlib.Topology.Algebra.Module.Star
starL.congr_simp : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousStar A], starL R = starL R
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseQuarterShort : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Month.Quarter
-- Mathlib.Algebra.Group.NatPowAssoc
npow_one : ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [NatPowAssoc M] (x : M), x ^ 1 = x
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumInl_onFunction : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ℕ) (val : L.Functions _n),
  FirstOrder.Language.LHom.sumInl.onFunction val = Sum.inl val
-- Init.Data.Array.Subarray
/-- The starting index of the region of interest (inclusive).  -/
Subarray.start : {α : Type u_1} → Subarray α → ℕ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_erase_le_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (cmp ((t.erase k).max he) (t.max ⋯)).isLE = true
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ico_add_Ioc_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α),
  Set.Ico a b + Set.Ioc c d ⊆ Set.Ioo (a + c) (b + d)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Structure containing the minimal axioms required to check that an order is a completely
distributive. Do NOT use, except for implementing `CompletelyDistribLattice` via
`CompletelyDistribLattice.ofMinimalAxioms`.

This structure omits the `himp`, `compl`, `sdiff`, `hnot` fields, which can be recovered using
`CompletelyDistribLattice.ofMinimalAxioms`.  -/
CompletelyDistribLattice.MinimalAxioms : (α : Type u) → [CompleteLattice α] → Prop
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.IsSwap.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (f f_1 : Equiv.Perm α), f = f_1 → f.IsSwap = f_1.IsSwap
-- Std.Data.DHashMap.Raw
/-- Equivalent to (but potentially faster than) calling `Const.get?` followed by `insertIfNew`.

Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.
 -/
Std.DHashMap.Raw.Const.getThenInsertIfNew? : {α : Type u} →
  {β : Type v} →
    [BEq α] → [Hashable α] → (Std.DHashMap.Raw α fun x => β) → α → β → Option β × Std.DHashMap.Raw α fun x => β
-- Lean.Parser.Command
Lean.Parser.Command.declVal.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousWithinAt.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → Set β) (s : Set α)
  (x : α), UpperHemicontinuousWithinAt f s x = SemicontinuousWithinAt (fun x t => t ∈ nhdsSet (f x)) s x
-- Mathlib.RingTheory.Ideal.Operations
Submodule.smul_comap_le_comap_smul : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type w}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') (S : Submodule R M') (I : Ideal R),
  I • Submodule.comap f S ≤ Submodule.comap f (I • S)
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt64HOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.isCentralScalar : ∀ (α : Type u_1) (M : Type u_5) {R : Type u_11} [inst : Zero M] [inst_1 : SMulZeroClass R M]
  [inst_2 : SMulZeroClass Rᵐᵒᵖ M] [IsCentralScalar R M], IsCentralScalar R (α →₀ M)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- If the angle between two vectors is 0, the norm of their sum equals
the sum of their norms.  -/
InnerProductGeometry.norm_add_eq_add_norm_of_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  InnerProductGeometry.angle x y = 0 → ‖x + y‖ = ‖x‖ + ‖y‖
-- Init.Data.Ord.Basic
/-- Swaps less-than and greater-than ordering results.

Examples:
* `Ordering.lt.swap = Ordering.gt`
* `Ordering.eq.swap = Ordering.eq`
* `Ordering.gt.swap = Ordering.lt`
 -/
Ordering.swap : Ordering → Ordering
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Alt pu →
    Array (Lean.Compiler.LCNF.Param pu) → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Alt pu
-- Std.Data.DHashMap.Raw
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.

Note: this replacement behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insert` function on `HashSet` and `HashSet.Raw` behaves differently: it will return the set
unchanged if a matching key is already present.
 -/
Std.DHashMap.Raw.insert : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → (a : α) → β a → Std.DHashMap.Raw α β
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_injective_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Injective ⇑f → Function.Injective (Subsemigroup.map f)
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
instIsContMDiffRiemannianBundleOfNatWithTopENat_2 : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {B : Type u_3} [inst_3 : TopologicalSpace B]
  [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_8 : (x : B) → NormedAddCommGroup (E x)]
  [inst_9 : (x : B) → InnerProductSpace ℝ (E x)] [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E]
  [IsContMDiffRiemannianBundle IB 3 F E], IsContMDiffRiemannianBundle IB 2 F E
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_roots_sub_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R} {a : R},
  0 < p.degree → ↑(p - Polynomial.C a).roots.card ≤ p.degree
-- Batteries.Data.Fin.Coding
/-- Encode `Ordering` into `Fin 3`.  -/
Fin.encodeOrdering : Ordering → Fin 3
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves colimits, then `F : C ⥤ Dᵒᵖ` preserves limits.  -/
CategoryTheory.Limits.preservesLimitsOfSize_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Probability.Process.Predictable
/-- The inclusion map from [0,i] × Ω with the subtype × 𝓕 i σ-algebra) to ι × Ω with the
predictable σ-algebra is measurable  -/
MeasureTheory.measurable_inclusion_predictable : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : LinearOrder ι] [inst_1 : OrderBot ι]
  [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι] [OpensMeasurableSpace ι] [OrderClosedTopology ι]
  {𝓕 : MeasureTheory.Filtration ι m} {i : ι}, Measurable fun x => (↑x.1, x.2)
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- The relation between `χ₄`, `χ₈` and `χ₈'`  -/
ZMod.χ₈'_eq_χ₄_mul_χ₈ : ∀ (a : ZMod 8), ZMod.χ₈' a = ZMod.χ₄ a.cast * ZMod.χ₈ a
-- Init.Data.Iterators.Basic
Std.IterM.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {internalState internalState_1 : α},
  { internalState := internalState } = { internalState := internalState_1 } → internalState = internalState_1
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.holdsForLocalization : RingHom.HoldsForLocalization fun {R S} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
-- Mathlib.GroupTheory.Coset.Basic
leftCoset_mem_leftCoset : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → a • ↑s = ↑s
-- Init.Data.SInt.Lemmas
Int8.minValue_le_toInt : ∀ (x : Int8), Int8.minValue.toInt ≤ x.toInt
-- Mathlib.Topology.Homeomorph.Lemmas
/-- Continuous equivalences from a compact space to a T2 space are homeomorphisms.

This is not true when T2 is weakened to T1
(see `Continuous.homeoOfEquivCompactToT2.t1_counterexample`).  -/
Continuous.homeoOfEquivCompactToT2 : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → [CompactSpace X] → [T2Space Y] → {f : X ≃ Y} → Continuous ⇑f → X ≃ₜ Y
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.slice_lt_iff : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁},
  q.slice p₀ p₁ h₀ h₁ < p ↔ q < String.Slice.Pos.ofSlice p
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.hasFDerivWithinAt_iff : ∀ {𝕜 : 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] {f₀ f₁ : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  f₀ =ᶠ[nhdsWithin x s] f₁ → f₀ x = f₁ x → (HasFDerivWithinAt f₀ f' s x ↔ HasFDerivWithinAt f₁ f' s x)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.LaurentSeries_coe : ∀ (K : Type u_2) [inst : Field K] (x : RatFunc K),
  (LaurentSeries.LaurentSeriesPkg K).coe (WithVal.toVal (RatFunc.polynomialValuationX K) x) =
    (algebraMap (RatFunc K) (LaurentSeries K)) x
-- Mathlib.Data.Holor
/-- Right associator for `Holor`  -/
Holor.assocRight : {α : Type} → {ds₁ ds₂ ds₃ : List ℕ} → Holor α (ds₁ ++ ds₂ ++ ds₃) → Holor α (ds₁ ++ (ds₂ ++ ds₃))
-- Mathlib.Algebra.Star.StarProjection
isStarProjection_iff' : ∀ {R : Type u_1} {p : R} [inst : Mul R] [inst_1 : Star R], IsStarProjection p ↔ p * p = p ∧ star p = p
-- Mathlib.Logic.Equiv.Multiset
_private.Mathlib.Logic.Equiv.Multiset.0.Denumerable.lower.match_1.eq_1 : ∀ (motive : List ℕ → ℕ → Sort u_1) (x : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (m : ℕ) → (l : List ℕ) → (n : ℕ) → motive (m :: l) n),
  (match [], x with
    | [], x => h_1 x
    | m :: l, n => h_2 m l n) =
    h_1 x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
PresheafOfModules.epi_of_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} {f : M₁ ⟶ M₂},
  (∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))) → CategoryTheory.Epi f
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The data which allows to construct an `E₂`-homological spectral sequence
indexed by `ℕ × ℕ` from a spectral object indexed by `EInt`. (Note: additional
assumptions on the spectral object are required for the construction of
the spectral sequence from this.)  -/
CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore EInt
  (fun r => ComplexShape.spectralSequenceNat (-r, r - 1)) 2
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.listToPath_pathToList : ∀ {α : Type u_1} {x : Quiver.SingleObj α} (p : Quiver.Path (Quiver.SingleObj.star α) x),
  Quiver.SingleObj.listToPath (Quiver.SingleObj.pathToList p) = Quiver.Path.cast ⋯ ⋯ p
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.add_log_le_log_mul : ∀ {x y : Ordinal.{u_1}} (b : Ordinal.{u_1}), x ≠ 0 → y ≠ 0 → Ordinal.log b x + Ordinal.log b y ≤ Ordinal.log b (x * y)
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_congr : ∀ {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero S]
  {x : HahnSeries Γ R} {y : HahnSeries Γ S}, x.support = y.support → x.cardSupp = y.cardSupp
-- Mathlib.Data.Nat.Cast.Defs
AddCommMonoidWithOne.mk : {R : Type u_2} → [toAddMonoidWithOne : AddMonoidWithOne R] → (∀ (a b : R), a + b = b + a) → AddCommMonoidWithOne R
-- Mathlib.Combinatorics.Graph.Simple
Graph.edgeSet_ofSimpleGraph : ∀ {α : Type u_1} (G : SimpleGraph α), (Graph.ofSimpleGraph G).edgeSet = G.edgeSet
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.diff_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₂.Equiv m₃ → (m₁ \ m₂).Equiv (m₁ \ m₃)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_inv_rightUnitor : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X : Rep.{u, u, v} k G},
  Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv = ↑(Representation.TensorProduct.rid k X.ρ).symm
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry?.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxEntry? = some ⟨k, v⟩
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsPrimitiveRoot.powerBasis_dim : ∀ {n : ℕ} [inst : NeZero n] (K : Type u) {L : Type v} [inst_1 : Field K] [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n),
  (IsPrimitiveRoot.powerBasis K hζ).dim = (minpoly K ζ).natDegree
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.mk.inj : ∀ {F : Type u → Type v} {inst : Applicative F} {G : Type u → Type w} {inst_1 : Applicative G}
  {app : (α : Type u) → F α → G α} {preserves_pure' : ∀ {α : Type u} (x : α), app α (pure x) = pure x}
  {preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app β (x <*> y) = app (α → β) x <*> app α y}
  {app_1 : (α : Type u) → F α → G α} {preserves_pure'_1 : ∀ {α : Type u} (x : α), app_1 α (pure x) = pure x}
  {preserves_seq'_1 : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app_1 β (x <*> y) = app_1 (α → β) x <*> app_1 α y},
  { app := app, preserves_pure' := preserves_pure', preserves_seq' := preserves_seq' } =
      { app := app_1, preserves_pure' := preserves_pure'_1, preserves_seq' := preserves_seq'_1 } →
    app = app_1
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_eq_mapL : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →L[𝕜] F),
  ContinuousLinearMap.rTensor G f = TensorProduct.mapL f (ContinuousLinearMap.id 𝕜 G)
-- Mathlib.Analysis.Analytic.Basic
FormalMultilinearSeries.congr_simp : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F],
  FormalMultilinearSeries 𝕜 E F = FormalMultilinearSeries 𝕜 E F
-- Mathlib.RepresentationTheory.Basic
Representation.apply_eq_of_coe_eq : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (S : Subgroup G)
  [Representation.IsTrivial (MonoidHom.comp ρ S.subtype)] (g h : G), ↑g = ↑h → ρ g = ρ h
-- Mathlib.Combinatorics.HalesJewett
/-- The proposition that all lines in a color-focused collection of lines have distinct colors.  -/
Combinatorics.Line.ColorFocused.distinct_colors : ∀ {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ι → Option α) → κ} (self : Combinatorics.Line.ColorFocused C),
  (Multiset.map Combinatorics.Line.AlmostMono.color self.lines).Nodup
-- Mathlib.RingTheory.WittVector.IsPoly
/-- The composition of polynomial functions is polynomial.  -/
WittVector.IsPoly₂.comp : ∀ {p : ℕ} {h : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R → WittVector p R}
  {f g : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R} [hh : WittVector.IsPoly₂ p h]
  [hf : WittVector.IsPoly p f] [hg : WittVector.IsPoly p g], WittVector.IsPoly₂ p fun x _Rcr x_1 y => h (f x_1) (g y)
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev?_eq_some_prev : ∀ {s : String.Slice} {p : s.Pos} (h : p ≠ s.startPos), p.prev? = some (p.prev h)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.iUnion_skeleton_eq_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  ⋃ n, ↑(Topology.RelCWComplex.skeleton C ↑n) = C
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- Right multiplying by an invertible matrix does not change the rank  -/
Matrix.rank_mul_eq_left_of_isUnit_det : ∀ {m : Type um} {n : Type un} [inst : Fintype n] {R : Type u_1} [inst_1 : CommRing R] [inst_2 : DecidableEq n]
  (A : Matrix n n R) (B : Matrix m n R), IsUnit A.det → (B * A).rank = B.rank
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.commShiftIso_hom_app_counit_app_shift_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (Y : D) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (G.comp F) a).hom.app Y)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (adj.counit.app Y)) h) =
    CategoryTheory.CategoryStruct.comp (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj Y)) h
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_neg : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {s : Set M} {g : M → F} {x : M}, UniqueMDiffAt[s] x → d[s] (-g) x = -d[s] g x
-- Mathlib.Topology.Order.LowerUpperTopology
/-- Type synonym for a preorder equipped with the upper topology.  -/
Topology.WithUpper : Type u_3 → Type u_3
-- Init.Data.Option.Lemmas
Option.merge_none_left : ∀ {α : Type u_1} {f : α → α → α} {b : Option α}, Option.merge f none b = b
-- Mathlib.Algebra.Algebra.Rat
RingHom.map_rat_algebraMap : ∀ {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R →+* S) (r : ℚ), f ((algebraMap ℚ R) r) = (algebraMap ℚ S) r