mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.homEquiv_symm_rightAdjointUniq_hom_app : ∀ {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 G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D),
  (adj2.homEquiv (G.obj x) x).symm ((adj1.rightAdjointUniq adj2).hom.app x) = adj1.counit.app x
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadCheck.other.inj : ∀ {pat pat_1 : Lean.Syntax},
  Lean.Elab.Term.Quotation.HeadCheck.other pat = Lean.Elab.Term.Quotation.HeadCheck.other pat_1 → pat = pat_1
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.star_self_mem_adjoin_singleton : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (x : A), star x ∈ StarAlgebra.adjoin R {x}
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
/-- `log` is analytic away from nonpositive reals  -/
AnalyticOnNhd.clog : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E},
  AnalyticOnNhd ℂ f s → (∀ z ∈ s, f z ∈ Complex.slitPlane) → AnalyticOnNhd ℂ (fun z => Complex.log (f z)) s
-- Mathlib.Tactic.NormNum.BigOperators
/-- Evaluate a big operator applied to a finset by repeating `proveEmptyOrCons` until
we exhaust all elements of the set.  -/
Mathlib.Meta.NormNum.evalFinsetBigop : {u v : Lean.Level} →
  {α : Q(Type u)} →
    {β : Q(Type v)} →
      (op : Q(Finset «$α» → («$α» → «$β») → «$β»)) →
        (f : Q(«$α» → «$β»)) →
          Mathlib.Meta.NormNum.Result q(«$op» Finset.empty «$f») →
            ({a : Q(«$α»)} →
                {s' : Q(Finset «$α»)} →
                  {h : Q(«$a» ∉ «$s'»)} →
                    Mathlib.Meta.NormNum.Result q(«$f» «$a») →
                      Mathlib.Meta.NormNum.Result q(«$op» «$s'» «$f») →
                        Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$op» (Finset.cons «$a» «$s'» «$h») «$f»))) →
              (s : Q(Finset «$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$op» «$s» «$f»))
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.min_val : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : LinearOrder α] (a b : AddUnits α), ↑(min a b) = min ↑a ↑b
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The submonoid `Δ` lies in the commensurator of the left subgroup.  -/
IsHeckeTriple.le_commensurator_left : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ : Subgroup G} (H₂ : Subgroup G) [h : IsHeckeTriple Δ H₁ H₂],
  Δ ≤ (Subgroup.Commensurable.commensurator H₁).toSubmonoid
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_iff_map_le : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.map ϕ.toAddMonoidHom H ≤ H
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.G.eq_1 : ∀ (L : PeriodPair) (n : ℕ), L.G n = ∑' (l : ↥L.lattice), (↑l ^ n)⁻¹
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- If `F` preserves the initial object and binary coproducts then it preserves finite products.  -/
CategoryTheory.PreservesFiniteCoproducts.of_preserves_binary_and_initial : ∀ {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.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F]
  [CategoryTheory.Limits.HasFiniteCoproducts C] (J : Type u_1) [Finite J],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.rightUnitorImpl_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  X.rightUnitorImpl.hom.f = CategoryTheory.Limits.prod.fst
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.coe_mul : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [IsTopologicalRing α] (a b : α), ↑(a * b) = ↑a * ↑b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α],
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity []) =
    Std.DHashMap.Internal.Raw₀.emptyWithCapacity
-- Mathlib.Order.SupClosed
latticeClosure_eq_self : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, latticeClosure s = s ↔ IsSublattice s
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.integral_sub_left_eq_self : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : AddGroup G] [MeasurableAdd G] [MeasurableNeg G] (f : G → E) (μ : MeasureTheory.Measure G) [μ.IsNegInvariant]
  [μ.IsAddLeftInvariant] (x' : G), ∫ (x : G), f (x' - x) ∂μ = ∫ (x : G), f x ∂μ
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.cast.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig1 aig2 : Std.Sat.AIG α} (s : aig1.RefVec len)
  (h : aig1.decls.size ≤ aig2.decls.size), s.cast h = s.cast' ⋯
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstFieldDeclParser.parenthesizer : optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Invertible.Defs
/-- If `r` is invertible and `s = r`, then `s` is invertible.  -/
Invertible.copy : {α : Type u} → [inst : MulOneClass α] → {r : α} → Invertible r → (s : α) → s = r → Invertible s
-- Mathlib.Data.ULift
PLift.up_injective : ∀ {α : Sort u}, Function.Injective PLift.up
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective.  -/
AffineSubspace.gciMapComap : {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 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : AddCommGroup V₂] →
                    [inst_5 : Module k V₂] →
                      [inst_6 : AddTorsor V₂ P₂] →
                        {f : P₁ →ᵃ[k] P₂} →
                          Function.Injective ⇑f → GaloisCoinsertion (AffineSubspace.map f) (AffineSubspace.comap f)
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.image_source_inter_eq' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (s : Set X), ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s
-- Init.Data.List.Control
/-- Applies the monadic action `f` to every element in the list, left-to-right, and returns the list of
results.

This implementation is tail recursive. `List.mapM'` is a non-tail-recursive variant that may be
more convenient to reason about. `List.forM` is the variant that discards the results and
`List.mapA` is the variant that works with `Applicative`.
 -/
List.mapM : {m : Type u → Type v} → [Monad m] → {α : Type w} → {β : Type u} → (α → m β) → List α → m (List β)
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instZero : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : Module R M] → Zero (ConvexCone R M)
-- Mathlib.Topology.Order.WithTop
WithTop.continuous_untop : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  Continuous fun x => (↑x).untop ⋯
-- Mathlib.Algebra.Order.Floor.Div
Finsupp.floorDiv_def : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : AddCommMonoid β] [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : FloorDiv α β] (f : ι →₀ β)
  (a : α), f ⌊/⌋ a = Finsupp.mapRange (fun x => x ⌊/⌋ a) ⋯ f
-- Mathlib.Algebra.Group.Prod
Prod.instDivisionCommMonoid : {G : Type u_1} → {H : Type u_2} → [DivisionCommMonoid G] → [DivisionCommMonoid H] → DivisionCommMonoid (G × H)
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.derivative_zero : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.derivative (bernsteinPolynomial R n 0) = -↑n * bernsteinPolynomial R (n - 1) 0
-- Std.Data.ExtDHashMap.Basic
/-- Inserts multiple mappings into the hash map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.ExtDHashMap.insertMany : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] →
          [LawfulHashable α] →
            {ρ : Type w} → [ForIn Id ρ ((a : α) × β a)] → Std.ExtDHashMap α β → ρ → Std.ExtDHashMap α β
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The functor which sends `⦋n⦌ : SimplexCategory` to the partially ordered
type `{0, 1, ..., n}` (ulifted to `Type u`).  -/
SimplexCategory.toPartOrd : CategoryTheory.Functor SimplexCategory PartOrd
-- Batteries.Lean.EStateM
EStateM.Result.map_ok : ∀ {ε σ α β : Type u_1} (f : α → β) (a : α) (s : σ),
  EStateM.Result.map f (EStateM.Result.ok a s) = EStateM.Result.ok (f a) s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKey ⋯ =
    t.maxKey?.elim k fun k' => if (compare k' k).isLE = true then k else k'
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.exists_mem_zpowers : ∀ {G : Type u_1} [inst : Group G] {x : G} {p : G → Prop}, (∃ g ∈ Subgroup.zpowers x, p g) ↔ ∃ m, p (x ^ m)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.MemLp.re : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [inst : RCLike 𝕜]
  {f : α → 𝕜}, MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => RCLike.re (f x)) p μ
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal.lastExpandedInIteration : Aesop.BestFirstQueue.ActiveGoal → Aesop.Iteration
-- Mathlib.Algebra.Order.Nonneg.Lattice
/-- If `sSup ∅ ≤ a` then `{x : α // a ≤ x}` is a `ConditionallyCompleteLinearOrderBot`.

This instance uses data fields from `Subtype.linearOrder` to help type-class inference.
The `Set.Ici` data fields are definitionally equal, but that requires unfolding semireducible
definitions, so type-class inference won't see this.  -/
Nonneg.conditionallyCompleteLinearOrderBot : {α : Type u_1} →
  [inst : ConditionallyCompleteLinearOrder α] → (a : α) → ConditionallyCompleteLinearOrderBot { x // a ≤ x }
-- Std.Time.Format.Modifier
Std.Time.Modifier.F.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.F presentation = Std.Time.Modifier.F presentation_1) = (presentation = presentation_1)
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_inj : ∀ {a b : BitVec 8}, Int8.ofBitVec a = Int8.ofBitVec b ↔ a = b
-- Init.MetaTypes
Lean.Meta.Occurrences.neg.injEq : ∀ (idxs idxs_1 : List ℕ), (Lean.Meta.Occurrences.neg idxs = Lean.Meta.Occurrences.neg idxs_1) = (idxs = idxs_1)
-- Init.Data.Array.Basic
Array.zipWithMAux : {α : Type u} →
  {β : Type u_1} →
    {γ : Type v} → {m : Type v → Type w} → [Monad m] → Array α → Array β → (α → β → m γ) → ℕ → Array γ → m (Array γ)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopEquiv_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.MonoidalOpposite.mopEquiv C).inverse = CategoryTheory.unmopFunctor C
-- Mathlib.Data.List.NatAntidiagonal
/-- The antidiagonal of a natural number `n` is the list of pairs `(i, j)` such that `i + j = n`.  -/
List.Nat.antidiagonal : ℕ → List (ℕ × ℕ)
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instHImp : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → HImp (L.DefinableSet A α)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.lift_unique : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A)
  (cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)) (g : CliffordAlgebra Q →ₐ[R] A),
  g.toLinearMap ∘ₗ CliffordAlgebra.ι Q = f ↔ g = (CliffordAlgebra.lift Q) ⟨f, cond⟩
-- Mathlib.Data.DFinsupp.BigOperators
Trunc.lift.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (c : ∀ (a b : α), f a = f b), Trunc.lift f c = Quot.lift f ⋯
-- Mathlib.Data.List.Sublists
List.sublistsLenAux_eq : ∀ {α : Type u} {β : Type v} (l : List α) (n : ℕ) (f : List α → β) (r : List β),
  List.sublistsLenAux n l f r = List.map f (List.sublistsLen n l) ++ r
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Graded ring homomorphisms preserve additive inverse.  -/
GradedRingHom.map_neg : ∀ {ι : Type u_1} {A : Type u_10} {B : Type u_11} {σ : Type u_12} {τ : Type u_13} [inst : Ring A] [inst_1 : Ring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] (𝒜 : ι → σ) (ℬ : ι → τ) (f : 𝒜 →+*ᵍ ℬ) (x : A), f (-x) = -f x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_intCast : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Algebra ℝ A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [StarModule ℝ A] (n : ℤ), CFC.abs ↑n = ↑|n|
-- Lean.Parser.Types
/-- Reports given 'expected' message at range of top stack element (assumed to be a single token).
Replaces the element with `missing` and resets position to the token position.
`iniPos` can be specified to avoid this position lookup but still must be identical to the token position.  -/
Lean.Parser.ParserState.mkUnexpectedTokenError : Lean.Parser.ParserState → String → optParam String.Pos.Raw 0 → Lean.Parser.ParserState
-- Mathlib.Algebra.Group.Defs
isAddRightRegular_iff_isAddRegular : ∀ {G : Type u_1} [inst : AddCommMagma G] {a : G}, IsAddRightRegular a ↔ IsAddRegular a
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.minimalPeriod_single_dvd_minimalPeriod_piMap : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i} (i : ι),
  Function.minimalPeriod (f i) (x i) ∣ Function.minimalPeriod (Pi.map f) x
-- Aesop.Forward.RuleInfo
Aesop.ForwardRuleInfo.mk.injEq : ∀ (numPremises numLevelParams : ℕ) (slotClusters : Array (Array Aesop.Slot)) (conclusionDeps : Array Aesop.PremiseIndex)
  (rulePatternInfo? : Option (Aesop.RulePattern × Aesop.PremiseIndex)) (numPremises_1 numLevelParams_1 : ℕ)
  (slotClusters_1 : Array (Array Aesop.Slot)) (conclusionDeps_1 : Array Aesop.PremiseIndex)
  (rulePatternInfo?_1 : Option (Aesop.RulePattern × Aesop.PremiseIndex)),
  ({ numPremises := numPremises, numLevelParams := numLevelParams, slotClusters := slotClusters,
        conclusionDeps := conclusionDeps, rulePatternInfo? := rulePatternInfo? } =
      { numPremises := numPremises_1, numLevelParams := numLevelParams_1, slotClusters := slotClusters_1,
        conclusionDeps := conclusionDeps_1, rulePatternInfo? := rulePatternInfo?_1 }) =
    (numPremises = numPremises_1 ∧
      numLevelParams = numLevelParams_1 ∧
        slotClusters = slotClusters_1 ∧ conclusionDeps = conclusionDeps_1 ∧ rulePatternInfo? = rulePatternInfo?_1)
-- Mathlib.Algebra.Polynomial.FieldDivision
/-- An irreducible polynomial over a field must have positive degree.  -/
Irreducible.natDegree_pos : ∀ {F : Type u_1} [inst : DivisionSemiring F] {f : Polynomial F}, Irreducible f → 0 < f.natDegree
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_add_expect_comm : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι} (f₁ f₂ g₁ g₂ : ι → M),
  ((s.expect fun i => f₁ i + f₂ i) + s.expect fun i => g₁ i + g₂ i) =
    (s.expect fun i => f₁ i + g₁ i) + s.expect fun i => f₂ i + g₂ i
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.numParams : Lean.Meta.RecursorInfo → ℕ
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_castPred_of_lt : ∀ {n : ℕ} (p i : Fin (n + 1)) (h : i < p), p.succAbove (i.castPred ⋯) = i
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_zero_of_ne_zero : ∀ {n : ℕ} [inst : NeZero n] {i : Fin (n + 1)} (hi : i ≠ 0), Fin.predAbove 0 i = i.pred hi
-- Mathlib.SetTheory.ZFC.PSet
/-- The pre-set union operator  -/
PSet.«term⋃₀_» : Lean.ParserDescr
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- Any element of the spectrum of a selfadjoint is real.  -/
selfAdjoint.mem_spectrum_eq_re : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : ↥(selfAdjoint A)) {z : ℂ}, z ∈ spectrum ℂ ↑a → z = ↑z.re
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.differentiableAt_binEntropy_iff_ne_zero_one : ∀ {p : ℝ}, DifferentiableAt ℝ Real.binEntropy p ↔ p ≠ 0 ∧ p ≠ 1
-- Mathlib.Analysis.Normed.Operator.Prod
/-- The operator norm of the second projection `E × F → F` is at most 1. (It is 0 if `F` is zero, so
the inequality cannot be improved without further assumptions.)  -/
ContinuousLinearMap.norm_snd_le : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F],
  ‖ContinuousLinearMap.snd 𝕜 E F‖ ≤ 1
-- Init.Data.Vector.Attach
Vector.toArray_unattach : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n}, xs.unattach.toArray = xs.toArray.unattach
-- Mathlib.RingTheory.Smooth.Quotient
_private.Mathlib.RingTheory.Smooth.Quotient.0.mul_le_ker_of_range_le_mul_of_sq_zero : ∀ {R : Type u_1} [inst : CommRing R] {J I : Ideal R},
  I ^ 2 = ⊥ →
    ∀ (f : J.Cotangent →ₗ[R] J.Cotangent),
      f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) →
        Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.abelian_radical_iff_solvable_is_abelian : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsNoetherian R L],
  IsLieAbelian ↥(LieAlgebra.radical R L) ↔ ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable ↥I → IsLieAbelian ↥I
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.finsetProd' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : CommMonoid β]
  [ContinuousMul β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) → MeasureTheory.IsStronglyProgressive f (∏ c ∈ s, U c)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {r : Std.Rco α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxo.HasSize α] [Std.Rxo.LawfulHasSize α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α], r.isEmpty = true ↔ ∀ (a : α), a ∉ r
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `α →+o β` is the type of monotone functions `α → β` that preserve the ordered additive monoid
structure.

`OrderAddMonoidHom` is also used for ordered group homomorphisms.

When possible, instead of parametrizing results over `(f : α →+o β)`,
you should parametrize over
`(F : Type*) [FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N] (f : F)`.  -/
OrderAddMonoidHom : (α : Type u_6) → (β : Type u_7) → [Preorder α] → [Preorder β] → [AddZeroClass α] → [AddZeroClass β] → Type (max u_6 u_7)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_insertIfNew_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, k ∈ t.insertIfNew k v
-- Mathlib.Data.Setoid.Partition
/-- On a unique index set there is the obvious trivial partition  -/
IndexedPartition.instInhabitedUnivOfUnique : {ι : Type u_1} → {α : Type u_2} → [Unique ι] → [Inhabited α] → Inhabited (IndexedPartition fun _i => Set.univ)
-- Mathlib.Analysis.Normed.Order.Hom.Basic
AddGroupNormClass.toNormedAddCommGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : AddCommGroup α] [inst_2 : AddGroupNormClass F α ℝ]
  (f : F),
  AddGroupNormClass.toNormedAddCommGroup f =
    { toNorm := (AddGroupNormClass.toNormedAddGroup f).toNorm,
      toAddGroup := (AddGroupNormClass.toNormedAddGroup f).toAddGroup, add_comm := ⋯,
      toMetricSpace := (AddGroupNormClass.toNormedAddGroup f).toMetricSpace, dist_eq := ⋯ }
-- Mathlib.Algebra.Module.ULift
ULift.distribMulAction' : {R : Type u} →
  {M : Type v} →
    [inst : Monoid R] → [inst_1 : AddMonoid M] → [DistribMulAction R M] → DistribMulAction R (ULift.{u_1, v} M)
-- Mathlib.Data.ENat.Pow
ENat.zero_epow_top : 0 ^ ⊤ = 0
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- **Alias** of `FreeAddGroup.reduce.eq_of_red`.

---

If a word reduces to another word, then they have a common maximal reduction.  -/
FreeGroup.freeAddGroup.red.reduce_eq : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.Red L₁ L₂ → FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂
-- Mathlib.NumberTheory.ADEInequality
/-- `A' q r := {1,q,r}` is a `Multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.  -/
ADEInequality.A' : ℕ+ → ℕ+ → Multiset ℕ+
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_var_const : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (x : Int.Internal.Linear.Var) (k : ℤ),
  Int.Internal.Linear.norm_eq_var_const_cert lhs rhs x k = true →
    (Int.Internal.Linear.Expr.denote ctx lhs = Int.Internal.Linear.Expr.denote ctx rhs) =
      (Int.Internal.Linear.Var.denote ctx x = k)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformlyOn.comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] {γ : Type u_4} [inst_3 : TopologicalSpace γ] {t : Set γ},
  HasProdLocallyUniformlyOn f g s →
    ∀ (h' : γ → β), Set.MapsTo h' t s → ContinuousOn h' t → HasProdLocallyUniformlyOn (fun i y => f i (h' y)) (g ∘ h') t
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  {x y : CategoryTheory.Bicategory.Adjunction f g}, x = y ↔ x.unit = y.unit ∧ x.counit = y.counit
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.coord_unitsSMul : ∀ {ι : Type u_1} {R₂ : Type u_3} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : CommSemiring R₂]
  [inst_2 : Module R₂ M] (e : Module.Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι), (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i
-- Std.Data.ExtDTreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.ExtDTreeMap.toArray : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → Array ((a : α) × β a)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.nonempty : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → C.Nonempty
-- Mathlib.Data.Set.Function
Set.mapsTo_univ_iff : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β}, Set.MapsTo f Set.univ t ↔ ∀ (x : α), f x ∈ t
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp (a - p) b = toIocMod hp a b - p