mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert.match_1.eq_1 : ∀ {n : ℕ} (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Sort u_1)
  (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (h_1 :
    (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) →
      (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
        (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
          motive { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }),
  (match { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } with
    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
      h_1 clauses rupUnits ratUnits assignments) =
    h_1 clauses rupUnits ratUnits assignments
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.le_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false → ∀ {k fallback : α}, (cmp k (t.minKeyD fallback)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryLE!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)] {k : α}, t₁.Equiv t₂ → t₁.getEntryLE! k = t₂.getEntryLE! k
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instForMProdOfMonad : {α : Type u} → {β : Type v} → {m : Type w → Type w'} → [Monad m] → ForM m (Std.HashMap.Raw α β) (α × β)
-- Mathlib.Topology.Algebra.Order.Field
/-- In a linearly ordered semifield with the order topology, if `f` tends to a positive constant `C`
and `g` tends to `Filter.atTop` then `f * g` tends to `Filter.atTop`.  -/
Filter.Tendsto.pos_mul_atTop : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜},
  0 < C →
    Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
_private.Mathlib.Analysis.InnerProductSpace.Projection.Basic.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_cons : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (a : α) (s : Multiset α), (a ::ₘ s).inf = a ⊓ s.inf
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ_one : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ψ 1 = 1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_eq_isEmpty_erase_and_not_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] (k : α),
  t.isEmpty = ((t.erase k).isEmpty && !t.contains k)
-- Mathlib.Data.ENNReal.Basic
ENNReal.csupr_ne_top : ∀ {α : Type u_1} [inst : SupSet α] (f : ENNReal → α), ⨆ x, f ↑x = ⨆ x, f ↑x
-- Mathlib.Topology.Algebra.LinearTopology
IsLinearTopology.hasBasis_open_submodule : ∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [ContinuousAdd M] [IsLinearTopology R M],
  (nhds 0).HasBasis (fun N => IsOpen ↑N) fun N => ↑N
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.hasColimitsOfSize : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, u₁} A]
  [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G],
  CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, max u₁ v₃} (CategoryTheory.CostructuredArrow G X)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' fallback : α} {f : β → β},
  (m.modify k f).getKeyD k' fallback = if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckHygieneInfo : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_mod_opow_log_lt_log_self : ∀ {b o : Ordinal.{u_1}}, 1 < b → b ≤ o → Ordinal.log b (o % b ^ Ordinal.log b o) < Ordinal.log b o
-- Init.Grind.AC
Lean.Grind.AC.eq_simp_rhs_suffix : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ head lhs₂ rhs₂ rhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_suffix_cert lhs₁ rhs₁ head rhs₂ rhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂'
-- Mathlib.Data.Set.NAry
/-- Symmetric statement to `Set.image_image2_right_anticomm`.  -/
Set.image_image2_antidistrib_right : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : Set α} {t : Set β}
  {g : γ → δ} {f' : β → α' → δ} {g' : α → α'},
  (∀ (a : α) (b : β), g (f a b) = f' b (g' a)) → g '' Set.image2 f s t = Set.image2 f' t (g' '' s)
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
/-- Extend `Set α → (F →L[ℝ] F')` to `(α →ₛ F) → F'`.  -/
MeasureTheory.SimpleFunc.setToSimpleFunc : {α : Type u_1} →
  {F : Type u_3} →
    {F' : Type u_4} →
      [inst : NormedAddCommGroup F] →
        [inst_1 : NormedSpace ℝ F] →
          [inst_2 : NormedAddCommGroup F'] →
            [inst_3 : NormedSpace ℝ F'] →
              {x : MeasurableSpace α} → (Set α → F →L[ℝ] F') → MeasureTheory.SimpleFunc α F → F'
-- Mathlib.GroupTheory.OrderOfElement
nsmul_eq_nsmul_of_modEq : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n a b : ℕ}, a ≡ b [MOD n] → n • x = 0 → a • x = b • x
-- Lean.Meta.Basic
/-- Given a monadic function `f` that takes a type and a term of that type and produces a new term,
lifts this to the monadic function that opens a `∀` telescope, applies `f` to the body,
and then builds the lambda telescope term for the new term.
 -/
Lean.Meta.mapForallTelescope' : (Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Normed.Group.Uniform
dist_add_add_le_of_le : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ},
  dist a₁ b₁ ≤ r₁ → dist a₂ b₂ ≤ r₂ → dist (a₁ + a₂) (b₁ + b₂) ≤ r₁ + r₂
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- The componentwise uniformity on `MvPowerSeries`  -/
MvPowerSeries.WithPiTopology.instUniformSpace : {σ : Type u_1} → {R : Type u_2} → [UniformSpace R] → UniformSpace (MvPowerSeries σ R)
-- Mathlib.Topology.Algebra.Module.Cardinality
/-- In a topological vector space over a nontrivially normed field, any neighborhood of a point has
the same cardinality as the whole space.  -/
cardinal_eq_of_mem_nhds : ∀ {E : Type u_1} (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : AddGroup E]
  [inst_2 : MulActionWithZero 𝕜 E] [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E}
  {x : E}, s ∈ nhds x → Cardinal.mk ↑s = Cardinal.mk E
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.map.eq_1 : ∀ {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] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.RightFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L),
  φ.map L hL = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (L.map φ.s)) (L.map φ.f)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Verify that `grind?` suggestions actually work.  -/
verifyGrind : Mathlib.TacticAnalysis.Config
-- Mathlib.Order.Minimal
maximal_eq_iff : ∀ {α : Type u_2} {x y : α} [inst : LE α], Maximal (fun x => x = y) x ↔ x = y
-- Mathlib.Data.List.Duplicate
List.Duplicate.cons_mem : ∀ {α : Type u_1} {x : α} {l : List α}, x ∈ l → List.Duplicate x (x :: l)
-- Mathlib.RingTheory.SimpleModule.Isotypic
mem_isotypicComponents_iff : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  {m : Submodule R M}, m ∈ isotypicComponents R M ↔ IsIsotypic R ↥m ∧ m.IsFullyInvariant ∧ m ≠ ⊥
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.mem_factorSet_some : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {p : Associates α} {hp : Irreducible p}
  {l : Multiset { a // Irreducible a }}, p ∈ ↑l ↔ ⟨p, hp⟩ ∈ l
-- Mathlib.RingTheory.Congruence.Hom
RingCon.quotientQuotientEquivQuotient_symm_mk : ∀ {M : Type u_1} [inst : NonAssocSemiring M] (c d : RingCon M) (h : c ≤ d) (x : M),
  (c.quotientQuotientEquivQuotient d h).symm ⟦x⟧ = ⟦⟦x⟧⟧
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- Construction of a colimit cocone for a functor `J ⥤ ShortComplex C` using the colimits
of the three components `J ⥤ C`.  -/
CategoryTheory.ShortComplex.colimitCocone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) →
            [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] →
              [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] →
                [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] →
                  CategoryTheory.Limits.Cocone F
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.mem_imp : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f.Disjoint g → ∀ {x : α}, x ∈ f.support → x ∉ g.support
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preRight_map_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B)
  (R : CategoryTheory.Functor B T) {Y X : CategoryTheory.Comma L (F.comp R)} (f : Y ⟶ X),
  ((CategoryTheory.Comma.preRight L F R).map f).left = f.left
-- Aesop.Options.Public
/-- (aesop) Only for use by Aesop developers. Enables dynamic script structuring.
 -/
Aesop.aesop.dev.dynamicStructuring : Lean.Option Bool
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.card_conjClasses_odd : ∀ {n : ℕ}, Odd n → Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Norm of `const α b` is less than or equal to `‖b‖`. If `α` is nonempty,
then it is equal to `‖b‖`.  -/
BoundedContinuousFunction.norm_const_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] (b : β),
  ‖BoundedContinuousFunction.const α b‖ ≤ ‖b‖
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- Inverse of a continuous affine equivalence as a continuous affine equivalence.  -/
ContinuousAffineEquiv.symm : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] → [inst_8 : TopologicalSpace P₂] → (P₁ ≃ᴬ[k] P₂) → P₂ ≃ᴬ[k] P₁
-- Mathlib.Computability.Encoding
Computability.Encoding.encode_injective : ∀ {α : Type u_1} {Γ : Type u_2} (e : Computability.Encoding α Γ), Function.Injective e.encode
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.map_hom_ofInv_id : ∀ {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] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X)
  (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L),
  CategoryTheory.CategoryStruct.comp (L.map s) ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL) =
    CategoryTheory.CategoryStruct.id (L.obj Y)
-- Mathlib.Topology.Separation.CompletelyRegular
injective_stoneCechUnit_of_t35Space : ∀ {X : Type u} [inst : TopologicalSpace X] [T35Space X], Function.Injective stoneCechUnit
-- Init.Data.Array.MapIdx
Array.mapFinIdx_reverse : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.reverse.size → β},
  xs.reverse.mapFinIdx f = (xs.mapFinIdx fun i a h => f (xs.size - 1 - i) a ⋯).reverse
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.support_coeff_divOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G] (g : G)
  (x : AddMonoidAlgebra k G), (x.divOf g).coeff.support = x.coeff.support.preimage (fun x => g + x) ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (t.insertMany l).contains k = (t.contains k || (List.map Sigma.fst l).contains k)
-- Mathlib.Data.List.TakeDrop
List.take_eq_self_iff : ∀ {α : Type u} (x : List α) {n : ℕ}, List.take n x = x ↔ x.length ≤ n
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_zpow_comm : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ) (n : ℤ), (x ^ y) ^ n = (x ^ n) ^ y
-- Init.Control.State
StateT.instAlternative : {σ : Type u} → {m : Type u → Type v} → [Monad m] → [Alternative m] → Alternative (StateT σ m)
-- Batteries.Tactic.Congr
/-- Apply congruence (recursively) to goals of the form `⊢ f as = f bs` and `⊢ f as ≍ f bs`.
* `congr n` controls the depth of the recursive applications.
  This is useful when `congr` is too aggressive in breaking down the goal.
  For example, given `⊢ f (g (x + y)) = f (g (y + x))`,
  `congr` produces the goals `⊢ x = y` and `⊢ y = x`,
  while `congr 2` produces the intended `⊢ x + y = y + x`.
* If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
* You can use `congr with p (: n)?` to call `ext p (: n)?` to all subgoals generated by `congr`.
  For example, if the goal is `⊢ f '' s = g '' s` then `congr with x` generates the goal
  `x : α ⊢ f x = g x`.
 -/
Batteries.Tactic.congrConfigWith : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_of_isEmpty_insertMany : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {l : ρ}, (↑↑(m.insertMany l)).isEmpty = true → (↑m).isEmpty = true
-- Mathlib.Order.Fin.Tuple
StrictMono.removeNth : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin (n + 1) → α},
  StrictMono f → ∀ (i : Fin (n + 1)), StrictMono (i.removeNth f)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.hom_inv_id_triangle_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B),
  CategoryTheory.CategoryStruct.comp e.hom.hom₃ e.inv.hom₃ = CategoryTheory.CategoryStruct.id A.obj₃
-- ProofWidgets.Component.Basic
ProofWidgets.MarkdownDisplay.instFromJsonProps.fromJson : Lean.Json → Except String ProofWidgets.MarkdownDisplay.Props
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_natCast : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : Mul R] (c : RingCon R) (n : ℕ), ↑↑n = ↑n
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_uIoo_succ : ∀ {n : ℕ} (i j : Fin n), Fin.succ ⁻¹' Set.uIoo i.succ j.succ = Set.uIoo i j
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_inv_le : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L), (FractionalIdeal.dual A K I)⁻¹ ≤ I
-- Init.Data.SInt.Basic
instDivInt8 : Div Int8
-- Mathlib.Data.EReal.Basic
EReal.image_coe_Iic : ∀ (x : ℝ), Real.toEReal '' Set.Iic x = Set.Ioc ⊥ ↑x
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.instLattice : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] → {ρ : Representation A G W} → Lattice (Subrepresentation ρ)
-- Init.Data.Nat.ToString
Nat.toDigits_eq_if : ∀ {b n : ℕ}, 1 < b → b.toDigits n = if n < b then [n.digitChar] else b.toDigits (n / b) ++ [(n % b).digitChar]
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.pow_mul_term_eq : ∀ (f : ℕ → ℂ) (s : ℂ) (n : ℕ), (↑n + 1) ^ s * LSeries.term f s (n + 1) = f (n + 1)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.strictMono_rpow_of_pos : ∀ {z : ℝ}, 0 < z → StrictMono fun x => x ^ z
-- Mathlib.Order.MinMax
lt_max_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < max b c ↔ a < b ∨ a < c
-- Aesop.RulePattern
Aesop.RulePattern.elab : Lean.Term → Lean.Expr → Lean.Elab.TermElabM Aesop.RulePattern
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
IsStrictlyPositive.nonneg_add : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  0 ≤ a → IsStrictlyPositive b → IsStrictlyPositive (a + b)
-- Mathlib.Order.Interval.Set.OrdConnectedLinear
Set.Nonempty.eq_Icc_iff_int : ∀ {I : Set ℤ},
  I.Nonempty →
    BddBelow I → BddAbove I → (I = Set.Icc (sInf I) (sSup I) ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Set.Ioo x y) I → y ≤ x + 1)
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_eq`. -/
Ideal.inertiaDeg'_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [inst_3 : q.LiesOver p] [inst_4 : q.IsPrime] [inst_5 : p.IsPrime]
  [inst_6 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_7 : Localization.AtPrime.IsLiesOverAlgebra p q], q.inertiaDeg R = Module.finrank p.ResidueField q.ResidueField
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonHover : Lean.ToJson Lean.Lsp.Hover
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarRight_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {ι : Type u_5}
  [inst_7 : DecidableEq ι] (t : TensorProduct R M (ι →₀ R)) (i : ι),
  ((TensorProduct.finsuppScalarRight R S M ι) t) i =
    (TensorProduct.AlgebraTensorModule.rid R S M) ((LinearMap.lTensor M (Finsupp.lapply i)) t)
-- Lean.Environment
Lean.Kernel.Exception.typeExpected.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (expr : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.typeExpected env lctx expr) = 1 + sizeOf env + sizeOf lctx + sizeOf expr
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- If `f : X → Z` is a Borel measurable map from a standard Borel space
to a countably separated measurable space,
then for any measurable space `β` and `g : Z → β`, the composition `g ∘ f` is
measurable if and only if the restriction of `g` to the range of `f` is measurable.  -/
Measurable.measurable_comp_iff_restrict : ∀ {X : Type u_3} {Z : Type u_5} {β : Type u_6} [inst : MeasurableSpace X] [StandardBorelSpace X]
  [inst_2 : MeasurableSpace β] [inst_3 : MeasurableSpace Z] {f : X → Z}
  [MeasurableSpace.CountablySeparated ↑(Set.range f)],
  Measurable f → ∀ {g : Z → β}, Measurable (g ∘ f) ↔ Measurable ((Set.range f).domRestrict g)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.not.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n), φ.not = φ.imp ⊥
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.proj.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (typeName : Lean.Name) (idx : ℕ) (struct : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_1) (typeName_1 : Lean.Name)
  (idx_1 : ℕ) (struct_1 : Lean.FVarId)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_1),
  (Lean.Compiler.LCNF.LetValue.proj typeName idx struct h =
      Lean.Compiler.LCNF.LetValue.proj typeName_1 idx_1 struct_1 h_1) =
    (typeName = typeName_1 ∧ idx = idx_1 ∧ struct = struct_1)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.contDiff' : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (self : TestFunction Ω F n),
  ContDiff ℝ (↑n) self.toFun
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.linearMapLeftRightHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {P : Type u_5} [inst_7 : AddCommMonoid P] [inst_8 : Module R P] {Q : Type u_6} [inst_9 : AddCommMonoid Q]
  [inst_10 : Module R Q] [inst_11 : Module S P] [inst_12 : IsScalarTower R S P] [inst_13 : Module S Q]
  [inst_14 : IsScalarTower R S Q] {α : M →ₗ[R] P} (j : IsBaseChange S α) (β : N →ₗ[R] Q) (f : M →ₗ[R] N) (p : P),
  ((j.linearMapLeftRightHom β) f) p = ((LinearMap.liftBaseChangeEquiv S) (β ∘ₗ f)) (j.equiv.symm p)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.comp_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal],
  CategoryTheory.Functor.LaxMonoidal.ε (F.comp G) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε G)
      (G.map (CategoryTheory.Functor.LaxMonoidal.ε F))
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Out of three elements of a linearly ordered semiring, two must have the same sign.  -/
mul_nonneg_of_three : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R]
  [AddLeftMono R] [AddLeftReflectLE R] (a b c : R), 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.toLieModule : ∀ {R : Type u_1} {A : Type u_2} {L : Type u_3} {inst : CommRing A} {inst_1 : LieRing L} {inst_2 : Module A L}
  {inst_3 : LieRingModule L A} {inst_4 : LieRinehartRing A L} {inst_5 : CommRing R} {inst_6 : Algebra R A}
  {inst_7 : LieAlgebra R L} [self : LieRinehartAlgebra R A L], LieModule R L A