mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.coe_constℝ : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} (x : ℝ) [inst : Γ.HasDetPlusMinusOne],
  ⇑(ModularForm.constℝ x) = Function.const UpperHalfPlane ↑x
-- Lean.Elab.Term.TermElabM
/-- Return `some mvarId` if `e` corresponds to a hole that is going to be filled "later" by executing a tactic or resuming elaboration.

We do not save `ofTermInfo` for this kind of node in the `InfoTree`.
 -/
Lean.Elab.Term.isTacticOrPostponedHole? : Lean.Expr → Lean.Elab.TermElabM (Option Lean.MVarId)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associatorNatIsoLeft_inv_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {b c d : B} (a : B) (g : b ⟶ c) (h : c ⟶ d) (X : a ⟶ b),
  (CategoryTheory.Bicategory.associatorNatIsoLeft a g h).inv.app X = (CategoryTheory.Bicategory.associator X g h).inv
-- Mathlib.Analysis.Analytic.IteratedFDeriv
_private.Mathlib.Analysis.Analytic.IteratedFDeriv.0.HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset : ∀ {𝕜 : 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}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    AnalyticOn 𝕜 f s →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          ∀ {n : ℕ} (v : Fin n → E),
            s ⊆ Metric.eball x r → (iteratedFDerivWithin 𝕜 n f s x) v = ∑ σ, (p n) fun i => v (σ i)
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.isZero_of_isLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory C) (n i : ℤ),
  n < i → ∀ [hX : X.IsLE n], CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor C i).obj X)
-- Mathlib.Topology.Order.OrderClosed
iSup_eq_of_forall_le_of_tendsto : ∀ {α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [inst : ConditionallyCompleteLattice α]
  [inst_1 : TopologicalSpace α] [ClosedIicTopology α] {a : α} {f : ι → α},
  (∀ (i : ι), f i ≤ a) → Filter.Tendsto f F (nhds a) → ⨆ i, f i = a
-- Mathlib.Topology.EMetricSpace.Defs
/-- Every `PseudoEMetricSpace` has a `WeakPseudoEMetricSpace` structure by
using the topology induced by `edist`.  -/
PseudoEMetricSpace.toWeakPseudoEMetricSpace : (α : Type u) → [inst : PseudoEMetricSpace α] → WeakPseudoEMetricSpace α
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_three : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), normEDS b c d 3 = c
-- Std.Http.Protocol.H1.Writer
/-- Writes accumulated user data to output using chunked transfer encoding.

Empty chunks are silently discarded. See `Chunk.empty` for the protocol-level rationale.
 -/
Std.Http.Protocol.H1.Writer.writeChunkedBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Writer dir
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoc_subset_uIoc_of_uIcc_subset_uIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α}, Set.uIcc a b ⊆ Set.uIcc c d → Set.uIoc a b ⊆ Set.uIoc c d
-- Std.Http.Transport
Std.Http.instTransportClient : Std.Http.Transport Std.Async.TCP.Socket.Client
-- Lean.Meta.Sym.Canon
Lean.Meta.Sym.Canon.instInhabitedShouldCanonResult.default : Lean.Meta.Sym.Canon.ShouldCanonResult✝
-- Mathlib.CategoryTheory.Subobject.Types
Types.monoOverEquivalenceSet_unitIso : ∀ (α : Type u),
  (Types.monoOverEquivalenceSet α).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun f =>
        CategoryTheory.MonoOver.isoMk (Equiv.ofInjective ⇑(CategoryTheory.ConcreteCategory.hom f.obj.hom) ⋯).toIso ⋯)
      ⋯
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.SubarrayIterator.val_step_eq : ∀ {α : Type u_1} {it : Std.Iter α},
  ↑it.step =
    if h : it.internalState.xs.start < it.internalState.xs.stop then
      Std.IterStep.yield
        {
          internalState :=
            {
              xs :=
                {
                  internalRepresentation :=
                    { array := it.internalState.xs.array, start := it.internalState.xs.start + 1,
                      stop := it.internalState.xs.stop, start_le_stop := ⋯, stop_le_array_size := ⋯ } } } }
        it.internalState.xs.array[it.internalState.xs.start]
    else Std.IterStep.done
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightUnshift_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ)
  (hn : n' + a = n) (x : R), (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- Given an `n`-th primitive root of unity `ζ`, where `2 ≤ n`, we have that `ζ - 1` and
`ζ ^ (i + j) - ζ ^ i` are associated for all and `j` coprime with `n` and all `i`. See
`pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one` for the explicit formula of the
unit.  -/
IsPrimitiveRoot.associated_pow_add_sub_sub_one : ∀ {n j : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A],
  IsPrimitiveRoot ζ n → 2 ≤ n → ∀ (i : ℕ), j.Coprime n → Associated (ζ - 1) (ζ ^ (i + j) - ζ ^ i)
-- Init.Data.Nat.Mod
Nat.two_pow_mod_two_eq_one : ∀ {n : ℕ}, 2 ^ n % 2 = 1 ↔ n = 0
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Finset β`.
 -/
Finset.mulActionFinset : {α : Type u_2} → {β : Type u_3} → [DecidableEq β] → [inst : Monoid α] → [MulAction α β] → MulAction α (Finset β)
-- Mathlib.Order.Interval.Basic
Interval.coe_sInf : ∀ {α : Type u_1} [inst : CompleteLattice α] [inst_1 : DecidableLE α] (S : Set (Interval α)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Aesop.Tree.Data
Aesop.TreeSpec.Goal : Aesop.TreeSpec → Type
-- Mathlib.Order.Hom.WithTopBot
WithTop.toDualBotEquiv_symm_top : ∀ {α : Type u_1} [inst : LE α], WithTop.toDualBotEquiv.symm ⊤ = ⊤
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.RwKind.valid.sizeOf_spec : ∀ (motiveTypeCorrect : Bool) (occ : Option ℕ),
  sizeOf (Mathlib.Tactic.ClickSuggestions.RwKind.valid motiveTypeCorrect occ) =
    1 + sizeOf motiveTypeCorrect + sizeOf occ
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor : SimplexCategory.skeletalFunctor.EssSurj
-- Aesop.Script.TacticState
Aesop.Script.instInhabitedTacticState : Inhabited Aesop.Script.TacticState
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- `N`-conjugacy is transitive.  -/
GroupExtension.IsConj.trans : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  (S : GroupExtension N E G) {s₁ s₂ s₃ : S.Splitting}, S.IsConj s₁ s₂ → S.IsConj s₂ s₃ → S.IsConj s₁ s₃
-- Mathlib.Data.Finsupp.Single
/-- If `α` has a unique term, the type of finitely supported functions `α →₀ β` is equivalent to `β`.
 -/
Equiv.finsuppUnique : {M : Type u_5} → [inst : Zero M] → {ι : Type u_13} → [Unique ι] → (ι →₀ M) ≃ M
-- Init.Data.Range.Polymorphic.PRange
Std.Rio.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (upper : α), (sizeOf *...upper) = 1 + sizeOf upper
-- Mathlib.Analysis.Calculus.ParametricIntegral
/-- Differentiation under integral of `x ↦ ∫ F x a` at a given point `x₀`, assuming
`F x₀` is integrable, `x ↦ F x a` is differentiable on a neighborhood of `x₀` for ae `a` with
derivative norm uniformly bounded by an integrable function (the neighborhood is independent
of `a`), and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`.  -/
hasFDerivAt_integral_of_dominated_of_fderiv_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E] {H : Type u_4}
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ} {s : Set H}
  {F' : H → α → H →L[𝕜] E},
  s ∈ nhds x₀ →
    (∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) →
      MeasureTheory.Integrable (F x₀) μ →
        MeasureTheory.AEStronglyMeasurable (F' x₀) μ →
          (∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a) →
            MeasureTheory.Integrable bound μ →
              (∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasFDerivAt (fun x => F x a) (F' x a) x) →
                HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The linear isometry equivalence version of `TensorProduct.comm`.  -/
TensorProduct.commIsometry : (𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : InnerProductSpace 𝕜 F] → TensorProduct 𝕜 E F ≃ₗᵢ[𝕜] TensorProduct 𝕜 F E
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.M : Type → Type
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Restriction.isBase_iff_of_spanning : ∀ {α : Type u_2} {M : Matroid α} {B : Set α} {N : Matroid α},
  N.IsRestriction M → M.Spanning N.E → (N.IsBase B ↔ M.IsBase B ∧ B ⊆ N.E)
-- Lean.Meta.Basic
Lean.Meta.ExprConfigCacheKey : Type
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.flip_flip : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P), f.flip.flip = f
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x` has right cancellative
addition if `β` has right cancellative addition.  -/
FunLike.isRightCancelAdd : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsRightCancelAdd β] [IsAddApply F α β], IsRightCancelAdd F
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.forall : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {P : AddSubgroup ↥H → Prop},
  (∀ (H' : AddSubgroup ↥H), P H') ↔ ∀ H' ≤ H, P (H'.addSubgroupOf H)
-- Mathlib.Topology.FiberBundle.Basic
/-- The projection from a fiber bundle to its base is continuous.  -/
FiberBundle.continuous_proj : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E],
  Continuous Bundle.TotalSpace.proj
-- Mathlib.CategoryTheory.Yoneda
/-- The representing element for the corepresentable functor `F`, sometimes called the universal
element of the functor.
 -/
CategoryTheory.Functor.coreprx : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor C (Type v)) → [hF : F.IsCorepresentable] → F.obj F.coreprX
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_mem_addCommutator : ∀ {G : Type u_1} [inst : AddGroup G] {g₁ g₂ : G} {H₁ H₂ : AddSubgroup G}, g₁ ∈ H₁ → g₂ ∈ H₂ → ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_eq_logHeight_restrict_support : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K),
  Height.logHeight x = Height.logHeight fun i => x ↑i
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.map_eq_iff : ∀ {n d : ℕ} {x₁ x₂ : Fin n.succ → ℕ},
  (∀ (i : Fin n.succ), x₁ i < d) →
    (∀ (i : Fin n.succ), x₂ i < d) →
      ((Behrend.map d) x₁ = (Behrend.map d) x₂ ↔
        x₁ 0 = x₂ 0 ∧ (Behrend.map d) (x₁ ∘ Fin.succ) = (Behrend.map d) (x₂ ∘ Fin.succ))
-- Mathlib.Topology.Spectral.Prespectral
instLocallyCompactSpaceOfPrespectralSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PrespectralSpace X], LocallyCompactSpace X
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_diff_le_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ \ t₂).size ≤ t₁.size
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.intMul.inj : ∀ {k : ℤ} {a : Lean.Grind.Linarith.Expr} {k_1 : ℤ} {a_1 : Lean.Grind.Linarith.Expr},
  Lean.Grind.Linarith.Expr.intMul k a = Lean.Grind.Linarith.Expr.intMul k_1 a_1 → k = k_1 ∧ a = a_1
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies the constructor application `Int.ofNat n` such that
`norm_num` successfully recognizes `n`, returning `n`.  -/
Mathlib.Meta.NormNum.evalIntOfNat : Mathlib.Meta.NormNum.NormNumExt
-- Qq.Macro
Qq.Impl.ExprBackSubstResult.unquoted : Lean.Expr → Qq.Impl.ExprBackSubstResult
-- Std.Internal.Do.WP.Lemmas
StateT.set.eq_1 : ∀ {σ : Type u} {m : Type u → Type v} [inst : Monad m] (s' x : σ), StateT.set s' x = pure (PUnit.unit, s')
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.comp_id : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  (f : A →ₑ+[φ] B), f.comp (DistribMulActionHom.id M) = f
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
IsDedekindDomain.map_differentIdeal_dvd_differentIdeal : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] (R₁ : Type u_5) (R₂ : Type u_6)
  [inst_2 : CommRing R₁] [inst_3 : CommRing R₂] [inst_4 : IsDomain R₁] [inst_5 : Algebra A R₁] [inst_6 : Algebra A R₂]
  [inst_7 : Algebra R₁ B] [inst_8 : Algebra R₂ B] [Module.Finite A R₂] [inst_10 : IsDomain A]
  [inst_11 : IsDedekindDomain B] [inst_12 : IsDedekindDomain R₁] [inst_13 : IsDedekindDomain R₂] [IsIntegrallyClosed A]
  [inst_15 : Module.IsTorsionFree R₁ B] [Module.IsTorsionFree R₂ B] [inst_17 : Algebra A B] [Module.Finite A B]
  [inst_19 : Module.IsTorsionFree A B] [inst_20 : Module.IsTorsionFree A R₁] [inst_21 : Module.IsTorsionFree A R₂]
  [Module.Finite A R₁] [Module.Finite R₂ B] [IsScalarTower A R₂ B] [Module.Finite R₁ B]
  [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [IsScalarTower A R₁ B],
  IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂)) →
    Ideal.map (algebraMap R₂ B) (differentIdeal A R₂) ∣ differentIdeal R₁ B
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The kernel of the cokernel of an epimorphism is an isomorphism  -/
CategoryTheory.Limits.kernel.of_cokernel_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasCokernel f]
  [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Epi f],
  CategoryTheory.IsIso (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π f))
-- Init.Data.Nat.Basic
Nat.succ_ne_zero : ∀ (n : ℕ), n.succ ≠ 0
-- Mathlib.Topology.Compactness.Lindelof
/-- A continuous image of a Lindelöf set is a Lindelöf set within the codomain.  -/
IsLindelof.image : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  IsLindelof s → Continuous f → IsLindelof (f '' s)
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView.ofSyntax : Lean.TSyntax `Lean.Parser.Command.derivingClass → Lean.CoreM Lean.Elab.DerivingClassView
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ext_dual : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [H : SeparatingDual 𝕜₂ F]
  {A B : E →SWOT[σ] F}, (∀ (x : E) (y : StrongDual 𝕜₂ F), y (A x) = y (B x)) → A = B
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint.resolveDeferred : Lean.Elab.InlayHint → Lean.MetaM Lean.Elab.InlayHint
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_sub_Icc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a - x) ⁻¹' Set.Icc b c = Set.Icc (a - c) (a - b)
-- Init.Data.Order.Lemmas
Std.le_max : ∀ {α : Type u} [inst : Max α] [inst_1 : LE α] [Std.IsPreorder α] [Std.LawfulOrderMax α] {a b c : α},
  a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pattern.ForwardSliceSearcher.startsWith_iff : ∀ {pat s : String.Slice},
  String.Slice.Pattern.ForwardSliceSearcher.startsWith pat s = true ↔ ∃ t, s.copy = pat.copy ++ t
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.exists_isBasis' : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), ∃ I, M.IsBasis' I X
-- Mathlib.Topology.Algebra.ConstMulAction
isOpenMap_smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (c : G), IsOpenMap fun x => c • x
-- Mathlib.Data.Int.GCD
/-- **Alias** of `Int.gcd_ediv_gcd_ediv_gcd`. -/
Int.gcd_div_gcd_div_gcd : ∀ {i j : ℤ}, 0 < i.gcd j → (i / ↑(i.gcd j)).gcd (j / ↑(i.gcd j)) = 1
-- Init.Data.SInt.Basic
instReprInt16 : Repr Int16
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.lfpApprox.eq_def : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x : α) (a : Ordinal.{u}),
  OrdinalApprox.lfpApprox f x a = x ⊔ ⨆ b, ⨆ (_ : b < a), f (OrdinalApprox.lfpApprox f x b)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.Measurable.comp_nullMeasurable : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [m : MeasurableSpace α] [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {f : α → β} {μ : MeasureTheory.Measure α} {g : β → γ},
  Measurable g → MeasureTheory.NullMeasurable f μ → MeasureTheory.NullMeasurable (g ∘ f) μ
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ext : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {f g : A₁ ≃ₐ[R] A₂}, (∀ (a : A₁), f a = g a) → f = g
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOnFilter.mul` -/
TendstoUniformlyOnFilter.fun_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformlyOnFilter f g l l' →
    TendstoUniformlyOnFilter f' g' l l' →
      TendstoUniformlyOnFilter (fun i i_1 => f i i_1 * f' i i_1) (fun i => g i * g' i) l l'
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j),
  (d.transitionCocone hij).pt = (d.cocone j).pt
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.reduce_postcondition : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  (c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty →
      Std.Tactic.BVDecide.LRAT.Internal.Incompatible (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) c assignment) ∧
    ∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
      c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l →
        ∀ (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool),
          Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p assignment →
            Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p l
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.quasiIsoAt_ιTruncLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] {j : ι} {j' : ι'}, e.f j = j' → QuasiIsoAt (K.ιTruncLE e) j'
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r_one_zpow : ∀ {n : ℕ} (k : ℤ), DihedralGroup.r 1 ^ k = DihedralGroup.r ↑k
-- Mathlib.Data.Rel
SetRel.inv_mono : ∀ {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β}, R₁ ⊆ R₂ → R₁.inv ⊆ R₂.inv
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The canonical map `R[X₁,...,Xₘ] ⊗ R[X₁,...,Xₙ] → UniversalFactorizationRing`.  -/
Polynomial.UniversalFactorizationRing.fromTensor : {R : Type u_1} →
  [inst : CommRing R] →
    {n : ℕ} →
      (m k : ℕ) →
        (hn : n = m + k) →
          (p : Polynomial.MonicDegreeEq R n) →
            TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R) →ₐ[R]
              Polynomial.UniversalFactorizationRing m k hn p
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isAddCyclic_additive_iff : ∀ {α : Type u_1} [inst : DivInvMonoid α], IsAddCyclic (Additive α) ↔ IsCyclic α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, a ∉ m → m.getKeyD a fallback = fallback
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.const_mul : ∀ {α : Type u_1} {f : α → α} {x : α} {m : ℕ}, Function.IsPeriodicPt f m x → ∀ (n : ℕ), Function.IsPeriodicPt f (n * m) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_empty : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {a : α} {fallback : β},
  Std.DTreeMap.Internal.Impl.Const.getD Std.DTreeMap.Internal.Impl.empty a fallback = fallback
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.centralizer.congr_simp : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A] (s s_1 : Set A),
  s = s_1 → NonUnitalStarSubalgebra.centralizer R s = NonUnitalStarSubalgebra.centralizer R s_1
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.IpcM : Type → Type
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [IsCancelAdd G]
  {x : AddMonoidAlgebra k G} {g : G}, AddMonoidAlgebra.of' k G g ∣ x ↔ x.modOf g = 0
-- Mathlib.RingTheory.Valuation.Archimedean
Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange : ∀ {F : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : CommRing O] [inst_3 : Algebra O F] {v : Valuation F Γ₀} [Nontrivial (↥(MonoidHom.mrange v))ˣ],
  v.Integers O →
    (WellFounded (Function.onFun (fun x1 x2 => x1 > x2) (⇑v ∘ ⇑(algebraMap O F))) ↔
      Nonempty (↥(MonoidHom.mrange v) ≃*o WithZero (Multiplicative ℤ)))
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_order_of_eq_add_single : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_8} [inst_1 : AddCancelCommMonoid R] [inst_2 : Zero Γ]
  {x y : HahnSeries Γ R}, x = y + (HahnSeries.single x.order) x.leadingCoeff → y.coeff x.order = 0