mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.FibrantObject.homMk_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] (X : C) [inst_3 : HomotopicalAlgebra.IsFibrant X],
  HomotopicalAlgebra.FibrantObject.homMk (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id (HomotopicalAlgebra.FibrantObject.mk X)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_inv : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α), Equiv.Perm.sign f⁻¹ = Equiv.Perm.sign f
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.hahnCoeff_apply : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R) {x : ↥seed.baseDomain}
  {f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)},
  (↑x = f.sum fun c => ⇑(seed.stratum c).subtype) →
    ∀ (c : FiniteArchimedeanClass M), (seed.hahnCoeff x) c = (seed.coeff c) (f c)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.bypass_eq_self : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {p : G.Walk u v}, p.IsPath → p.bypass = p
-- Std.Data.TreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the largest key that is
less than the given key.
 -/
Std.TreeMap.getKeyLT : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.TreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → α
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.induction_on : ∀ {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] {motive : TensorProduct R M N → Prop}
  (z : TensorProduct R M N),
  motive 0 →
    (∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)) →
      (∀ (x y : TensorProduct R M N), motive x → motive y → motive (x + y)) → motive z
-- Mathlib.Data.Finset.MulAntidiagonal
/-- **Alias** of `Finset.isPWO_support_antidiagonal`. -/
Finset.isPWO_support_addAntidiagonal : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO}, {a | (Finset.antidiagonal hs ht a).Nonempty}.IsPWO
-- Mathlib.Data.Set.Sups
Set.sups_assoc : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s t u : Set α), s ⊻ t ⊻ u = s ⊻ (t ⊻ u)
-- Mathlib.Algebra.Order.Kleene
natCast_eq_one : ∀ {α : Type u_1} [inst : IdemSemiring α] {n : ℕ}, n ≠ 0 → ↑n = 1
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits : ∀ {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.HasFiniteLimits D]
  [CategoryTheory.Limits.CreatesFiniteLimits F], CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.CategoryTheory.Comma.Basic
/-- Composing `unopFunctor L R` with `(fst L R).op` is isomorphic to `snd L.op R.op`.  -/
CategoryTheory.Comma.unopFunctorCompFst : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (CategoryTheory.Comma.unopFunctor L R).comp (CategoryTheory.Comma.fst R L).op ≅
                  CategoryTheory.Comma.snd L.op R.op
-- Mathlib.Order.Filter.Map
Filter.image_mem_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {s : Set α},
  Function.Injective m → (m '' s ∈ Filter.map m f ↔ s ∈ f)
-- Std.Time.Date.Basic
/-- Convert `Day.Offset` into `Hour.Offset`.
 -/
Std.Time.Hour.Offset.ofDays : Std.Time.Day.Offset → Std.Time.Hour.Offset
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.finite_of_hasDimensionLT : ∀ (X : SSet) (d : ℕ) [X.HasDimensionLT d], (∀ i < d, Finite ↑(X.nonDegenerate i)) → X.Finite
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.coeff_mul_add_eq_of_natDegree_le : ∀ {R : Type u} [inst : Semiring R] {df dg : ℕ} {f g : Polynomial R},
  f.natDegree ≤ df → g.natDegree ≤ dg → (f * g).coeff (df + dg) = f.coeff df * g.coeff dg
-- Mathlib.Computability.Language
Language.one_add_self_mul_kstar_eq_kstar : ∀ {α : Type u_1} (l : Language α), 1 + l * KStar.kstar l = KStar.kstar l
-- Mathlib.Algebra.Group.Units.Defs
Units.Simps.val_inv.eq_1 : ∀ {α : Type u} [inst : Monoid α] (u : αˣ), Units.Simps.val_inv u = ↑u⁻¹
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_eq_getKey! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α} {h : a ∈ m}, m.getKey a h = m.getKey! a
-- Init.Data.SInt.Bitwise
Int8.toInt16_xor : ∀ (a b : Int8), (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16
-- Mathlib.Algebra.Group.Units.Basic
divp_mul_eq_mul_divp : ∀ {α : Type u} [inst : CommMonoid α] (x y : α) (u : αˣ), x /ₚ u * y = x * y /ₚ u
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsPure : ∀ {φ : Prop} {σ : Type u_1} {s : σ} (σs : List (Type u_1)) (P : Std.Do.SPred (σ :: σs))
  [inst : Std.Do.SPred.Tactic.IsPure P φ], Std.Do.SPred.Tactic.IsPure (P s) φ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} {h₁ : a ∈ Std.DTreeMap.Internal.Impl.insertIfNew! k v t},
  (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).get a h₁ =
    if h₂ : compare k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.get a ⋯
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.delete_iff : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (l l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  l' ∈ (c.delete l).toList ↔ l' ≠ l ∧ l' ∈ c.toList
-- Init.Data.Nat.Div.Lemmas
Nat.add_div : ∀ {a b c : ℕ}, 0 < c → (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.toRingHom_mapRingEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  (e : R ≃+* S), (AddMonoidAlgebra.mapRingEquiv M e).toRingHom = AddMonoidAlgebra.mapRingHom M ↑e
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- Less general version of `lift`.  -/
_private.Mathlib.FieldTheory.IsAlgClosed.Basic.0.IsAlgClosed.liftAux : (K : Type u) →
  [inst : Field K] →
    (L : Type v) →
      (M : Type w) →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            [inst_3 : Field M] → [inst_4 : Algebra K M] → [IsAlgClosed M] → [Algebra.IsAlgebraic K L] → L →ₐ[K] M
-- Init.Core
/-- Modus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`.  -/
Iff.mpr : ∀ {a b : Prop}, (a ↔ b) → b → a
-- Mathlib.Logic.Relation
Relation.transGen_le_reflTransGen : ∀ {α : Type u_1} {r : α → α → Prop}, Relation.TransGen r ≤ Relation.ReflTransGen r
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_zero_left : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : Zero α] [inst_1 : Zero γ] (f : α → β → γ),
  (∀ (b : β), f 0 b = 0) → ∀ (B : Matrix n p β), Matrix.kroneckerMap f 0 B = 0
-- Lean.Level
/-- Auxiliary function for `normalize`.
`maxExplicit` is the maximum explicit universe level at `lvls`.
Return true if it finds a level with offset ≥ maxExplicit.
`i` starts at the first non explicit level.
It assumes `lvls` has been sorted using `normLt`.
 -/
_private.Lean.Level.0.Lean.Level.isExplicitSubsumedAux : Array Lean.Level → ℕ → ℕ → Bool
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- Given families of morphisms `f : X i ⟶ S` and `f' : X' j ⟶ S'`, suitable
commutative diagrams `w j : p' j ≫ f (α j) = f' j ≫ p`, this is the natural
isomorphism between the descent data relative to `f'` that are obtained either:
* by considering the obvious descent data relative to `f` given by an object `M : F.obj (op S)`,
  followed by the application of `pullFunctor F w : F.DescentData f ⥤ F.DescentData f'`;
* by considering the obvious descent data relative to `f'` given by pulling
  back the object `M` to `S'`.
 -/
CategoryTheory.Pseudofunctor.DescentData.toDescentDataCompPullFunctorIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {S' : C} →
                {p : S' ⟶ S} →
                  {ι' : Type t'} →
                    {X' : ι' → C} →
                      {f' : (j : ι') → X' j ⟶ S'} →
                        {α : ι' → ι} →
                          {p' : (j : ι') → X' j ⟶ X (α j)} →
                            (w :
                                ∀ (j : ι'),
                                  CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) =
                                    CategoryTheory.CategoryStruct.comp (f' j) p) →
                              (F.toDescentData f).comp (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w) ≅
                                (F.map p.op.toLoc).toFunctor.comp (F.toDescentData f')
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The characterization of weak convergence of probability measures by the usual (defining)
condition that the integrals of every continuous bounded function are continuous.  -/
MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuousMap_continuous_integral : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {X : Type u_2} [inst_3 : TopologicalSpace X] {μs : X → MeasureTheory.ProbabilityMeasure Ω} [CompactSpace Ω],
  Continuous μs ↔ ∀ (f : C(Ω, ℝ)), Continuous fun x => ∫ (ω : Ω), f ω ∂↑(μs x)
-- Mathlib.Topology.MetricSpace.Thickening
Metric.frontier_thickening_disjoint : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (A : Set α),
  Pairwise (Function.onFun Disjoint fun r => frontier (Metric.thickening r A))
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict : ∀ {X : TopCat} (Y : AlgebraicGeometry.LocallyRingedSpace) {f : X ⟶ ↑Y.toPresheafedSpace}
  (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (Y.ofRestrict hf)
-- Mathlib.RingTheory.DividedPowers.Basic
/-- If J is another ideal of A with divided powers,
then the divided powers of I and J coincide on I • J

[Berthelot-1974], 1.6.1 (ii)  -/
DividedPowers.coincide_on_smul : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {a : A} (hI : DividedPowers I) {J : Ideal A}
  (hJ : DividedPowers J) {n : ℕ}, a ∈ I • J → hI.dpow n a = hJ.dpow n a
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coind₁.congr_simp : ∀ {R : Type u_1} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] {G : Type u_7} [inst_5 : Group G]
  [inst_6 : TopologicalSpace G] [inst_7 : TopologicalSpace R] [inst_8 : ContinuousSMul R V]
  [inst_9 : IsTopologicalGroup G] (π π_1 : ContRepresentation R G V), π = π_1 → π.coind₁ = π_1.coind₁
-- Mathlib.GroupTheory.ArchimedeanDensely
denselyOrdered_multiplicative_iff : ∀ {X : Type u_2} [inst : LT X], DenselyOrdered (Multiplicative X) ↔ DenselyOrdered X
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.method.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.method = 1
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [v.IsRankOneDiscrete] [Valuation.IsTrivialOn K v],
  v RatFunc.X ≤ 1 → ∃ u, v.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) u)
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift for groups preserves limits of arbitrary size.
 -/
GrpCat.uliftFunctor_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} GrpCat.uliftFunctor
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.regular_inv_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G], μ.inv.Regular ↔ μ.Regular
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.alter.match_3.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.eq = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.eq = Ordering.gt → motive Ordering.gt) (h_3 : Ordering.eq = Ordering.eq → motive Ordering.eq),
  (match h : Ordering.eq with
    | Ordering.lt => h_1 h
    | Ordering.gt => h_2 h
    | Ordering.eq => h_3 h) =
    h_3 ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.inv_whiskerRight : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ')
  [inst_9 : CategoryTheory.IsIso η] {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''},
  CategoryTheory.inv (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ) =
    CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (CategoryTheory.inv η) φ
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableWithinAt_comp_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} (a : E),
  DifferentiableWithinAt 𝕜 (fun x => f (x - a)) s x ↔ DifferentiableWithinAt 𝕜 f (-a +ᵥ s) (x - a)
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d_negSucc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n m : ℕ),
  h.d (Int.negSucc n) (Int.negSucc m) = K.d n m
-- Mathlib.Data.EReal.Inv
EReal.abs_neg : ∀ (x : EReal), (-x).abs = x.abs
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], k ∈ m₂ → (m₁ ∩ m₂).get! k = m₁.get! k
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitDiagInfo.c : Lean.Meta.Grind.SplitDiagInfo → Lean.Expr
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.toIntInst : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Lean.Expr
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_norm_replicateRow : ∀ {m : Type u_3} {α : Type u_5} {ι : Type u_7} [inst : Fintype m] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : m → α), ‖Matrix.replicateRow ι v‖ = ‖WithLp.toLp 2 v‖
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (𝒱 : (i : 𝒰.I₀) → (CategoryTheory.Limits.pullback f (𝒰.f i)).OpenCover),
  Set.range ⇑(CategoryTheory.Limits.pullback.diagonal f) ⊆
    ↑(AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.map_top : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] (f : A →ₙₐ[R] B), NonUnitalSubalgebra.map f ⊤ = NonUnitalAlgHom.range f
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySum.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B B_1 : ℝ),
  B = B_1 →
    ∀ (a a_1 : NumberField.mixedEmbedding.mixedSpace K),
      a = a_1 → NumberField.mixedEmbedding.convexBodySum K B a = NumberField.mixedEmbedding.convexBodySum K B_1 a_1
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.MkSimpContextResult : Type
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovaryOn_neg_left`. -/
AntivaryOn.neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f g s → MonovaryOn (-f) g s
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial_le : ∀ (k : ℕ) {n m : ℕ}, n ≤ m → n.ascFactorial k ≤ m.ascFactorial k
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.iSup₂ : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {κ : Sort u_4}
  {κ' : κ → Sort u_5} {f : (i : κ) → κ' i → Ideal A},
  (∀ (i : κ) (j : κ' i), Ideal.IsHomogeneous 𝒜 (f i j)) → Ideal.IsHomogeneous 𝒜 (⨆ i, ⨆ j, f i j)
-- Init.Data.List.MinMax
List.max?.eq_1 : ∀ {α : Type u} [inst : Max α], [].max? = none
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBasis.cardinalMk_le_cRk : ∀ {α : Type u} {M : Matroid α} {I X : Set α}, M.IsBasis I X → Cardinal.mk ↑I ≤ M.cRk X
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toList_ne_singleton : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : Equiv.Perm α) (x y : α), p.toList x ≠ [y]
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.forIn'_eq_forIn'_toArray : ∀ {α : Type u} {r : Std.Rco α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toArray init fun a ha acc => f a ⋯ acc
-- Mathlib.RingTheory.Fintype
natCard_units_lt : ∀ (M₀ : Type u_1) [inst : MonoidWithZero M₀] [Nontrivial M₀] [Finite M₀], Nat.card M₀ˣ < Nat.card M₀
-- Mathlib.Data.Fin.Basic
/-- `a ≤ b` as natural numbers if and only if `a ≤ b` in `Fin n`.  -/
Fin.val_fin_le : ∀ {n : ℕ} {a b : Fin n}, ↑a ≤ ↑b ↔ a ≤ b
-- Mathlib.Data.Matrix.Basic
Submodule.coe_matrix : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_14} {M : Type u_15} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (S : Submodule R M), ↑S.matrix = (↑S).matrix
-- Mathlib.Order.Lattice
/-- **Alias** of the forward direction of `inf_eq_left`. -/
le_of_inf_eq : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = a → a ≤ b
-- Lean.Structure
/-- Given a structure `structName` and a parent projection name `projName` (e.g. `toParentStructName`),
returns the corresponding parent structure name.
The parent projection name is a single-component name.

Note: this relies on the fact that projection names are checked to be consistent across all parents.
 -/
Lean.findParentProjStruct? : Lean.Environment → Lean.Name → Lean.Name → Option Lean.Name
-- Mathlib.Data.Set.Operations
/-- If `h : a ∈ {x | p x}` then `h.out : p x`. These are definitionally equal, but this can
nevertheless be useful for various reasons, e.g. to apply further projection notation or in an
argument to `simp`.  -/
Membership.mem.out : ∀ {α : Type u} {a : α} {p : α → Prop}, a ∈ {x | p x} → p a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfLeftIso_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.Limits.pullbackConeOfLeftIso f g).fst = CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv f)
-- Mathlib.Data.Sign.Defs
SignType.ofNat : ℕ → SignType
-- Lean.Elab.DocString
Lean.Doc.instMonadStateOfInternalStateDocM : MonadStateOf Lean.Doc.InternalState Lean.Doc.DocM
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- If `F i → f` in `L1`, then `∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ`.  -/
MeasureTheory.tendsto_setIntegral_of_L1 : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_6} (f : α → G),
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {F : ι → α → G} {l : Filter ι},
      (∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) →
        Filter.Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (nhds 0) →
          ∀ (s : Set α), Filter.Tendsto (fun i => ∫ (x : α) in s, F i x ∂μ) l (nhds (∫ (x : α) in s, f x ∂μ))
-- Mathlib.Algebra.Module.LinearMap.Index
LinearMap.index_of_subsingleton : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {R : Type u_3} [inst_2 : Ring R]
  [inst_3 : Module R M] [inst_4 : Module R N] {f : M →ₗ[R] N} [Subsingleton R], f.index = 0
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R] [Module.Finite ℤ R]
  {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K] [IsFractionRing R K]
  {I : FractionalIdeal (nonZeroDivisors R) K} (a : ↥(nonZeroDivisors R)) (I₀ : Ideal R),
  a • ↑I = Submodule.map (Algebra.linearMap R K) I₀ →
    ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.ofFinset.congr_simp : ∀ {α : Type u_1} (f f_1 : α → ENNReal) (e_f : f = f_1) (s s_1 : Finset α) (e_s : s = s_1) (h : ∑ a ∈ s, f a = 1)
  (h' : ∀ a ∉ s, f a = 0), PMF.ofFinset f s h h' = PMF.ofFinset f_1 s_1 ⋯ ⋯
-- Mathlib.Topology.Algebra.Algebra
continuous_algebraMap_iff_smul : ∀ (R : Type u_1) (A : Type u) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace A] [ContinuousMul A],
  Continuous ⇑(algebraMap R A) ↔ Continuous fun p => p.1 • p.2
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tmod_left : ∀ (a b : ℤ), (a * b).tmod b = 0
-- Lean.LocalContext
/-- Whether a local declaration should be found by type class search, tactics, etc.
and shown in the goal display.
 -/
Lean.LocalDeclKind : Type
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.isRegularAtInfty_of_neg_one_mem : ∀ {R : Type u_1} [inst : Ring R] {𝒢 : Subgroup (GL (Fin 2) R)}, -1 ∈ 𝒢 → 𝒢.IsRegularAtInfty