mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piLTProj.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] {X : ι → Type u_5} ⦃i j : ι⦄ (h : i ≤ j) (f f_1 : InverseSystem.piLT X j),
  f = f_1 → ∀ (l : ↑(Set.Iio i)), InverseSystem.piLTProj h f l = InverseSystem.piLTProj h f_1 l
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.throwMissingName : Lean.Name → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Data.Multiset.Count
Multiset.one_le_count_iff_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, 1 ≤ Multiset.count a s ↔ a ∈ s
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSingletonClass.toDiscreteMeasurableSpace : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] [Countable α], DiscreteMeasurableSpace α
-- Init.Data.Iterators.Lemmas.Basic
_private.Init.Data.Iterators.Lemmas.Basic.0.Std.Iter.inductSkips.eq_def : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Productive α Id] (motive : Std.Iter β → Sort x)
  (step :
    (it : Std.Iter β) → ({it' : Std.Iter β} → it.IsPlausibleStep (Std.IterStep.skip it') → motive it') → motive it)
  (it : Std.Iter β), Std.Iter.inductSkips motive step it = step it fun {it'} x => Std.Iter.inductSkips motive step it'
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The variable of the formal power series ring.  -/
PowerSeries.X : {R : Type u_1} → [Semiring R] → PowerSeries R
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_pow_p_pow' : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (m n : ℕ),
  (Perfection.coeffMonoidHom M p (m + n)) f ^ p ^ n = (Perfection.coeffMonoidHom M p m) f
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedMutVar : Inhabited Lean.Elab.Do.MutVar
-- Mathlib.Data.Set.Image
Set.preimage_subset_iff : ∀ {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} {f : α → β}, f ⁻¹' B ⊆ A ↔ ∀ (a : α), f a ∈ B → a ∈ A
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.of_mul_eq_one_right : ∀ {M : Type u_1} [inst : Monoid M] [IsDedekindFiniteMonoid M] {b : M} (a : M), a * b = 1 → IsUnit b
-- Init.Data.Vector.Basic
Vector.foldlM : {m : Type u_1 → Type u_2} → {β : Type u_1} → {α : Type u_3} → {n : ℕ} → [Monad m] → (β → α → m β) → β → Vector α n → m β
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.AbstractCompletion.inhabited : (α : Type u_1) → [inst : UniformSpace α] → Inhabited (AbstractCompletion.{u_1, u_1} α)
-- Init.Data.String.Lemmas.Search
String.back?_eq_get? : ∀ {s : String}, s.back? = s.endPos.prev?.bind String.Pos.get?
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.lift_map_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {C : Type u_4} [inst_5 : CategoryTheory.Category.{v_4, u_4} C]
  (F : CategoryTheory.Functor C (CategoryTheory.Comma L R)) (hP : ∀ (X : C), P (F.obj X).hom)
  (hQ : ∀ {X Y : C} (f : X ⟶ Y), Q (F.map f).left) (hW : ∀ {X Y : C} (f : X ⟶ Y), W (F.map f).right) {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.Comma.Hom.hom ((CategoryTheory.MorphismProperty.Comma.lift F hP hQ hW).map f) =
    F.map f
-- Mathlib.Order.Disjoint
eq_top_of_isCompl_bot : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x : α}, IsCompl x ⊥ → x = ⊤
-- Mathlib.RingTheory.Morita.Basic
MoritaEquivalence.instAdditiveModuleCatFunctorEqv : ∀ (R : Type u₀) [inst : CommSemiring R] {A : Type u₁} [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u₂}
  [inst_3 : Ring B] [inst_4 : Algebra R B] (e : MoritaEquivalence R A B), e.eqv.functor.Additive
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.instBEqTriggerCondition : {ctx : Type u_1} → [BEq ctx] → BEq (Mathlib.TacticAnalysis.TriggerCondition ctx)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `f : X → Y` is Hölder continuous with a positive exponent `r`, then the Hausdorff dimension
of the image of a set `s` is at most `dimH s / r`.  -/
HolderWith.dimH_image_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {C r : NNReal} {f : X → Y},
  HolderWith C r f → 0 < r → ∀ (s : Set X), dimH (f '' s) ≤ dimH s / ↑r
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.comp : ∀ {α : Type u_1} {op op' : Stream'.Seq α → Stream'.Seq α},
  Tactic.ComputeAsymptotics.Seq.FriendlyOperation op →
    Tactic.ComputeAsymptotics.Seq.FriendlyOperation op' → Tactic.ComputeAsymptotics.Seq.FriendlyOperation (op ∘ op')
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
/-- If `τ : G₁ ⟶ G₂` is a natural transformation between two bifunctors
which commute shifts on both variables, this typeclass asserts a compatibility of `τ`
with these shifts.  -/
CategoryTheory.NatTrans.CommShift₂Int : {C₁ : Type u_1} →
  {C₂ : Type u_3} →
    {D : Type u_5} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D] →
            [inst_3 : CategoryTheory.HasShift C₁ ℤ] →
              [inst_4 : CategoryTheory.HasShift C₂ ℤ] →
                [inst_5 : CategoryTheory.HasShift D ℤ] →
                  [inst_6 : CategoryTheory.Preadditive D] →
                    [inst_7 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] →
                      {G₁ G₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} →
                        [G₁.CommShift₂Int] → [G₂.CommShift₂Int] → (G₁ ⟶ G₂) → Prop
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
/-- **Alias** of the reverse direction of `Matrix.fromRows_one_isTotallyUnimodular_iff`. -/
Matrix.IsTotallyUnimodular.fromRows_one : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [inst_1 : DecidableEq n] (A : Matrix m n R),
  A.IsTotallyUnimodular → (A.fromRows 1).IsTotallyUnimodular
-- Init.Data.Sum.Basic
/-- Checks whether a sum is the left injection `inl`.  -/
Sum.isLeft : {α : Type u_1} → {β : Type u_2} → α ⊕ β → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.arithShiftRight.inj : ∀ {m n : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr m} {rhs : Std.Tactic.BVDecide.BVExpr n} {n_1 : ℕ}
  {lhs_1 : Std.Tactic.BVDecide.BVExpr m} {rhs_1 : Std.Tactic.BVDecide.BVExpr n_1},
  lhs.arithShiftRight rhs = lhs_1.arithShiftRight rhs_1 → n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `LeftDistribClass` instance along an injective function.  -/
Function.Injective.leftDistribClass : ∀ {R : Type u_1} {S : Type u_2} (f : S → R),
  Function.Injective f →
    ∀ [inst : Add S] [inst_1 : Mul S] [inst_2 : Mul R] [inst_3 : Add R] [LeftDistribClass R],
      (∀ (x y : S), f (x + y) = f x + f y) → (∀ (x y : S), f (x * y) = f x * f y) → LeftDistribClass S
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- the coherence condition for the right square  -/
CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_assoc : ∀ {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'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ') {Z : CategoryTheory.Functor C B'}
  (h : ψ'.right.comp G' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.right G') h) =
    CategoryTheory.CategoryStruct.comp (G.whiskerLeft self.base)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom h)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasOfPrecompPropertyMin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W P Q : CategoryTheory.MorphismProperty C)
  [P.HasOfPrecompProperty W] [Q.HasOfPrecompProperty W], (P ⊓ Q).HasOfPrecompProperty W
-- Mathlib.Control.Lawful
ExceptT.run_monadLift : ∀ {α ε : Type u} {m : Type u → Type v} {n : Type u → Type u_1} [inst : Monad m] [inst_1 : MonadLiftT n m] (x : n α),
  (monadLift x).run = Except.ok <$> monadLift x
-- Mathlib.Algebra.Ring.Subring.Units
RingHom.isUnit_eqLocus_mk_iff : ∀ {R : Type u_1} {T : Type u_2} [inst : Semiring T] [inst_1 : Ring R] (f g : R →+* T) {r : R} (hr : f r = g r),
  IsUnit ⟨r, hr⟩ ↔ IsUnit r
-- Init.Data.Array.QSort.Basic
/-- Internal implementation of `Array.qsort`.

`qpartition as lt lo hi hlo hhi` returns a pair `(⟨m, h₁, h₂⟩, as')` where
`as'` is a permutation of `as` and `m` is a number such that:
- `lo ≤ m`
- `m < n`
- `∀ i, lo ≤ i → i < m → lt as[i] as[m]`
- `∀ j, m < j → j < hi → !lt as[j] as[m]`

It does so by first swapping the elements at indices `lo`, `mid := (lo + hi) / 2`, and `hi`
if necessary so that the middle (pivot) element is at index `hi`.
We then iterate from `k = lo` to `k = hi`, with a pointer `i` starting at `lo`, and
swapping each element which is less than the pivot to position `i`, and then incrementing `i`.
 -/
Array.qpartition : {α : Type u_1} →
  {n : ℕ} →
    Vector α n →
      (α → α → Bool) →
        (lo hi : ℕ) →
          autoParam (lo ≤ hi) Array.qpartition._auto_1 →
            autoParam (lo < n) Array.qpartition._auto_3 →
              autoParam (hi < n) Array.qpartition._auto_5 → { m // lo ≤ m ∧ m ≤ hi } × Vector α n
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_erase_eq_of_not_compare_eq_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, ¬cmp k (t.max ⋯) = Ordering.eq → (t.erase k).max he = t.max ⋯
-- Std.Time.Zoned.RecurringRule
/-- Recurring DST details for a zone that observes daylight saving time.
 -/
Std.Time.TimeZone.DaylightSavingRule : Type
-- Init.Prelude
/-- A type with a "one" element.  -/
One : Type u → Type u
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_doubleR : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll : Std.DTreeMap.Internal.Impl α β) (lrk : α)
  (lrv : β lrk) (lrl lrr r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.doubleR k v lk lv ll lrk lrv lrl lrr r).size =
    (Std.DTreeMap.Internal.Impl.bin k v
        (Std.DTreeMap.Internal.Impl.bin lk lv ll (Std.DTreeMap.Internal.Impl.bin lrk lrv lrl lrr)) r).size
-- Mathlib.Data.Set.Card
Set.ncard_add_ncard_compl : ∀ {α : Type u_1} (s : Set α),
  autoParam s.Finite Set.ncard_add_ncard_compl._auto_1 →
    autoParam sᶜ.Finite Set.ncard_add_ncard_compl._auto_3 → s.ncard + sᶜ.ncard = Nat.card α
-- Mathlib.Order.Filter.CountablyGenerated
Filter.HasCountableBasis.mk : ∀ {α : Type u_1} {ι : Type u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (Set.ofPred p).Countable → l.HasCountableBasis p s
-- Mathlib.Order.Hom.Lattice
LatticeHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = f
-- Init.Data.Option.Lemmas
Option.join_map_eq_map_join : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : Option (Option α)},
  (Option.map (Option.map f) x).join = Option.map f x.join
-- Mathlib.RingTheory.Idempotents
/-- The corner associated to an idempotent `e` in a semiring without 1
is the semiring with `e` as 1 consisting of all element of the form `e * r * e`.  -/
IsIdempotentElem.Corner : {R : Type u_1} → {e : R} → [inst : Semigroup R] → IsIdempotentElem e → Type u_1
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.measure_sub_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν]
  [MeasureTheory.IsFiniteMeasure μ], μ - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν
-- Mathlib.RingTheory.PowerSeries.GaussNorm
PowerSeries.gaussNorm_eq_zero_iff : ∀ {R : Type u_1} [inst : Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R),
  v 0 = 0 →
    (∀ (a : R), v a ≥ 0) →
      (∀ (x : R), v x = 0 → x = 0) → 0 < c → PowerSeries.HasGaussNorm v c f → (PowerSeries.gaussNorm v c f = 0 ↔ f = 0)
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.forget_createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddMonCat) → CategoryTheory.CreatesLimit F (CategoryTheory.forget AddMonCat)
-- Mathlib.Algebra.MvPolynomial.Funext
_private.Mathlib.Algebra.MvPolynomial.Funext.0.MvPolynomial.funext_fin : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {n : ℕ} {p : MvPolynomial (Fin n) R} (s : Fin n → Set R),
  (∀ (i : Fin n), (s i).Infinite) → (∀ x ∈ Set.univ.pi s, (MvPolynomial.eval x) p = 0) → p = 0
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The equivalence class of `z₁.comp₀ z₂ z₃` does not depend on the choice of `z₃` provided
they satisfy the compatibility `z₂.f ≫ z₃.s = z₁.s ≫ z₃.f`.  -/
CategoryTheory.MorphismProperty.LeftFraction.comp₀_rel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
  (z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'),
  CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f →
    CategoryTheory.CategoryStruct.comp z₂.f z₃'.s = CategoryTheory.CategoryStruct.comp z₁.s z₃'.f →
      CategoryTheory.MorphismProperty.LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice : ∀ {L : PeriodPair} {α β : ℚ}, ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice ↔ α.den = 1 ∧ β.den = 1
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.exists_maximal_ideal_liesOver_of_isIntegral : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] [FaithfulSMul R S] (P : Ideal R) [P.IsMaximal], ∃ Q, Q.IsMaximal ∧ Q.LiesOver P
-- Mathlib.Order.SuccPred.Basic
Order.pred_eq_pred_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  Order.pred a = Order.pred b ↔ a = b
-- Init.Data.Array.OfFn
_private.Init.Data.Array.OfFn.0.Array.ofFn.eq_1 : ∀ {α : Type u} {n : ℕ} (f : Fin n → α), Array.ofFn f = Array.ofFn.go✝ f (Array.emptyWithCapacity n) n ⋯
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.mem_span_of_linear_combination : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y z : V} {kx ky kz : NNReal},
  ky ≠ 0 → ky • y = kx • x + kz • z → y ∈ Submodule.span NNReal {x, z}
-- Init.Data.UInt.Lemmas
USize.lt_iff_toNat_lt : ∀ {a b : USize}, a < b ↔ a.toNat < b.toNat
-- Lean.Compiler.LCNF.Types
_private.Lean.Compiler.LCNF.Types.0.Lean.Compiler.LCNF.toLCNFType.go : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Nat.Power2.Basic
Nat.pos_of_isPowerOfTwo : ∀ {n : ℕ}, n.isPowerOfTwo → n > 0
-- Init.PropLemmas
forall_imp : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∀ (a : α), p a) → ∀ (a : α), q a
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.CG.range : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : Type u_2} [inst_1 : L.Structure N],
  FirstOrder.Language.Structure.CG L M → ∀ (f : L.Hom M N), f.range.CG
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.comp_id : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᴬ[R] Q),
  f.comp (ContinuousAffineMap.id R P) = f
-- Mathlib.Topology.Algebra.Monoid
Topology.IsInducing.separatelyContinuousMul : ∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N] [SeparatelyContinuousMul N] (f : F),
  Topology.IsInducing ⇑f → SeparatelyContinuousMul M
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- The `apply at` discrimination tree root.  -/
Mathlib.Tactic.ClickSuggestions.PreDiscrTrees.appAt : Mathlib.Tactic.ClickSuggestions.PreDiscrTrees →
  Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyAtLemma
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- Class expressing the fact that a `RingHom` is surjective. This is needed in the context
of semilinear maps, where some lemmas require this.  -/
RingHomSurjective : {R₁ : Type u_1} → {R₂ : Type u_2} → [inst : Semiring R₁] → [inst_1 : Semiring R₂] → (R₁ →+* R₂) → Prop
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.precoverage_mono : ∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  P ≤ Q → AlgebraicGeometry.Scheme.precoverage P ≤ AlgebraicGeometry.Scheme.precoverage Q
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.diagramOfConesInhabited : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              [CategoryTheory.Limits.HasLimitsOfShape K C] → Inhabited (CategoryTheory.Limits.DiagramOfCones F)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.comapEquiv_inverse : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {β γ : Type w} (e : β ≃ γ),
  (CategoryTheory.GradedObject.comapEquiv C e).inverse = CategoryTheory.GradedObject.comap C ⇑e
-- Init.Data.List.Basic
/-- Appends two lists. Normally used via the `++` operator.

Appending lists takes time proportional to the length of the first list: `O(|xs|)`.

This is a tail-recursive version of `List.append`.

Examples:
* `[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]`.
* `[] ++ [4, 5] = [4, 5]`.
* `[1, 2, 3] ++ [] = [1, 2, 3]`.
 -/
List.appendTR : {α : Type u} → List α → List α → List α
-- Lean.Expr
/-- Return true if the given expression is a target for (head) beta reduction.
If `useZeta = true`, then `let`-expressions are visited. That is, it assumes
that zeta-reduction (aka let-expansion) is going to be used.
 -/
Lean.Expr.isHeadBetaTarget : Lean.Expr → optParam Bool false → Bool
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
/-- **Alias** of the forward direction of `isTranscendenceBasis_subtype_range`. -/
IsTranscendenceBasis.of_subtype_range : ∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {ι : Type u_7}
  {f : ι → A}, Function.Injective f → IsTranscendenceBasis R Subtype.val → IsTranscendenceBasis R f
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.baseChange_relation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (T : Type u_1) [inst_3 : CommRing T] [inst_4 : Algebra R T] (P : Algebra.Presentation R S ι σ) (i : σ),
  (Algebra.Presentation.baseChange T P).relation i = (MvPolynomial.map (algebraMap R T)) (P.relation i)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.coe_congrOrderIso_apply : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {N : Type u_2}
  [inst_3 : AddCommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedAddMonoid N]
  (e : ArchimedeanClass M ≃o ArchimedeanClass N) (a : FiniteArchimedeanClass M),
  ↑((FiniteArchimedeanClass.congrOrderIso e) a) = e ↑a
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.moment_truncation_eq_intervalIntegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {A : ℝ},
      0 ≤ A →
        ∀ {n : ℕ},
          n ≠ 0 →
            ∫ (x : α), ProbabilityTheory.truncation f A x ^ n ∂μ =
              ∫ (y : ℝ) in -A..A, y ^ n ∂MeasureTheory.Measure.map f μ
-- Mathlib.NumberTheory.Height.Projectivization
Projectivization.mulHeight_ne_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [inst_2 : Finite ι]
  (x : Projectivization K (ι → K)), x.mulHeight ≠ 0
-- Mathlib.GroupTheory.NoncommPiCoprod
AddMonoidHom.noncommPiCoprod_mrange : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → AddMonoid (N i)] (ϕ : (i : ι) → N i →+ M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)},
  AddMonoidHom.mrange (AddMonoidHom.noncommPiCoprod ϕ hcomm) = ⨆ i, AddMonoidHom.mrange (ϕ i)
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyFaithful.jointlyReflectMonomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyFaithful F → CategoryTheory.JointlyReflectMonomorphisms F
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring is closed under multiplication.  -/
Subsemiring.mul_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {x y : R}, x ∈ s → y ∈ s → x * y ∈ s
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt.0.Int32.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option Int32)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.tensorUnit_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Center.tensorUnit.fst = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.GaloisCategory C}
  {F : CategoryTheory.Functor C FintypeCat} {obj : C} {pt : (F.obj obj).obj}
  {isGalois :
    autoParam (CategoryTheory.PreGaloisCategory.IsGalois obj)
      CategoryTheory.PreGaloisCategory.PointedGaloisObject.isGalois._autoParam}
  {obj_1 : C} {pt_1 : (F.obj obj_1).obj}
  {isGalois_1 :
    autoParam (CategoryTheory.PreGaloisCategory.IsGalois obj_1)
      CategoryTheory.PreGaloisCategory.PointedGaloisObject.isGalois._autoParam},
  { obj := obj, pt := pt, isGalois := isGalois } = { obj := obj_1, pt := pt_1, isGalois := isGalois_1 } →
    obj = obj_1 ∧ pt ≍ pt_1
-- Mathlib.Topology.Order.IsLUB
isGLB_of_mem_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {s : Set α} {a : α}
  {f : Filter α}, a ∈ lowerBounds s → s ∈ f → ∀ [(f ⊓ nhds a).NeBot], IsGLB s a
-- Mathlib.RingTheory.KrullDimension.Regular
ringKrullDim_le_ringKrullDim_quotSMulTop_succ : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] {x : R},
  x ∈ IsLocalRing.maximalIdeal R → ringKrullDim R ≤ ringKrullDim (R ⧸ x • ⊤) + 1
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int64.natCast : NatCast Int64