mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- If `M` and `M'` are boundaryless, so is their disjoint union `M ⊔ M'`.  -/
ModelWithCorners.boundaryless_disjointUnion : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_5} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] [hM : BoundarylessManifold I M] [hM' : BoundarylessManifold I M'],
  BoundarylessManifold I (M ⊕ M')
-- Mathlib.Algebra.Opposites
AddOpposite.instInhabited.eq_1 : ∀ {α : Type u_1} [inst : Inhabited α], AddOpposite.instInhabited = { default := AddOpposite.op default }
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_throw_Except_apply_eq : ∀ {ε : Type u_1} {α : Type u_2} {post : α → Prop} {epost : EPost⟨ε → Prop⟩} (e : ε),
  Std.Internal.Do.wp (MonadExceptOf.throw e) post epost = epost.head e
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewFact.fact.injEq : ∀ (prop proof : Lean.Expr) (generation : ℕ) (prop_1 proof_1 : Lean.Expr) (generation_1 : ℕ),
  (Lean.Meta.Grind.NewFact.fact prop proof generation = Lean.Meta.Grind.NewFact.fact prop_1 proof_1 generation_1) =
    (prop = prop_1 ∧ proof = proof_1 ∧ generation = generation_1)
-- Mathlib.Topology.Order.LiminfLimsup
/-- If a number `a` is less than or equal to the `liminf` of a function `f` at some filter
and is greater than or equal to the `limsup` of `f`, then `f` tends to `a` along this filter.  -/
tendsto_of_le_liminf_of_limsup_le : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] {f : Filter β} {u : β → α} {a : α},
  a ≤ Filter.liminf u f →
    Filter.limsup u f ≤ a →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) tendsto_of_le_liminf_of_limsup_le._auto_1 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) tendsto_of_le_liminf_of_limsup_le._auto_3 →
          Filter.Tendsto u f (nhds a)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Variant of `lt_mul_of_lt_one_right` for `a` negative instead of positive.  -/
mul_lt_of_one_lt_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R], a < 0 → 1 < b → a * b < a
-- Mathlib.Algebra.Group.Action.Defs
/-- A vector addition is cancellative if it is pointwise injective on the left and right.

A group action is cancellative in this sense if and only if it is **free**.
See `isCancelVAdd_iff_eq_zero_of_vadd_eq` for a more familiar condition.  -/
IsCancelVAdd : (G : Type u_9) → (P : Type u_10) → [VAdd G P] → Prop
-- Lean.Meta.PPGoal
/-- Given the current values of the options `pp.showLetValues` and `pp.showLetValues.threshold`,
determines whether the local let declaration's value should be omitted.

- `tactic` is whether the goal is for a tactic metavariable.
  In that case, uses the maximum of `pp.showLetValues.tactic.threshold` and `pp.showLetValues.threshold` for the threshold.
  In tactics, we usually want to see let values.
  In contrast, for the "expected type" view we usually do not.
 -/
Lean.Meta.ppGoal.shouldShowLetValue : Bool → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_self_le_prod_self : ∀ {α : Type u_1} [inst : Preorder α] {s₁ s₂ : UpperSet α}, s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instPowNat : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → Pow (CauSeq β abv) ℕ
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
MeasureTheory.Measure.sub_apply_eq_zero_of_isHahnDecomposition : ∀ {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ ν : MeasureTheory.Measure X},
  MeasureTheory.IsHahnDecomposition μ ν s → (μ - ν) s = 0
-- Std.Data.DTreeMap.Raw.Lemmas
/-- Variant of `get_map` that holds without `LawfulEqCmp`.  -/
Std.DTreeMap.Raw.Const.get_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.DTreeMap.Raw.map f t} (h : t.WF),
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.map f t) k h' = f (t.getKey k ⋯) (Std.DTreeMap.Raw.Const.get t k ⋯)
-- Mathlib.Data.Finset.Defs
Finset.le_iff_subset : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ ⊆ s₂ ↔ s₁ ⊆ s₂
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_nnreal_sub : ∀ {a : NNReal}, Continuous fun x => ↑a - x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toList_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.map f t).toList = List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.reduce_flatten_replicate_succ : ∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.IsReduced L →
    ∀ (n : ℕ),
      FreeGroup.reduce (List.replicate (n + 1) L).flatten =
        FreeGroup.reduceCyclically.conjugator L ++ (List.replicate (n + 1) (FreeGroup.reduceCyclically L)).flatten ++
          FreeGroup.invRev (FreeGroup.reduceCyclically.conjugator L)
-- Mathlib.Util.Superscript
/-- Applies the alignment mapping to a position.  -/
_private.Mathlib.Util.Superscript.0.Mathlib.Tactic.Superscript.scriptFnNoAntiquot.align : Array (String.Pos.Raw × String.Pos.Raw) → String.Pos.Raw → String.Pos.Raw
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.mk_toNat_of_infinite : ∀ {α : Type u} [h : Infinite α], Cardinal.toNat (Cardinal.mk α) = 0
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.CommGrp C),
  (CategoryTheory.Preadditive.commGrpEquivalenceAux.hom.app X).hom.hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_eq_zero_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ → p ≠ 0 → (MeasureTheory.eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0)
-- Mathlib.Order.Filter.ENNReal
Real.liminf_of_not_isBoundedUnder : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → ℝ}, ¬Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u → Filter.liminf u f = 0
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
/-- For all `ε > 0` and finite families `A`, we can partition the remainders of `A` mod `b`
into `abv.card ε` sets, such that all elements in each part of remainders are close together.  -/
AbsoluteValue.IsAdmissible.exists_partition : ∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} {ι : Type u_2} [Finite ι] {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : ι → R) (h : abv.IsAdmissible), ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
-- Lean.SubExpr
Lean.SubExpr.Pos.pushBindingDomain : Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Std.Time.Time.Unit.Second
Std.Time.Second.instDecidableLtOrdinal : {leap : Bool} → {x y : Std.Time.Second.Ordinal leap} → Decidable (x < y)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A : C)
  [inst_4 : ∀ (B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F],
  (CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso F A).inv =
    CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans F A)
-- Lean.Elab.MutualInductive
/-- Syntax for the whole constructor.  -/
Lean.Elab.Command.CtorView.ref : Lean.Elab.Command.CtorView → Lean.Syntax
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.RationalMap.isOver_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y]
  {S : AlgebraicGeometry.Scheme} [IrreducibleSpace ↥Y] [Nonempty ↥Z] [inst_4 : X.Over S] [inst_5 : Y.Over S]
  [inst_6 : Z.Over S] (f : X.RationalMap Y) [inst_7 : f.IsDominant] [AlgebraicGeometry.Scheme.RationalMap.IsOver S f]
  (g : Y.RationalMap Z) [g.IsDominant] [AlgebraicGeometry.Scheme.RationalMap.IsOver S g],
  AlgebraicGeometry.Scheme.RationalMap.IsOver S (f.comp g)
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The space of paths with both endpoints equal to a specified point `x : X`.
Denoted as `Ω`, within the `Topology.Homotopy` namespace.  -/
Topology.Homotopy.termΩ : Lean.ParserDescr
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.isStandardOpenImmersion_iff : ∀ (R : Type u_4) (S : Type u_5) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.IsStandardOpenImmersion R S ↔ ∃ r, IsLocalization.Away r S
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has strict derivative `NormedSpace.exp x`
at any point `x`.  -/
hasStrictDerivAt_exp : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {x : 𝕂}, HasStrictDerivAt NormedSpace.exp (NormedSpace.exp x) x
-- Mathlib.Computability.Language
Language.reverseIso_symm_apply : ∀ (α : Type u_1) (l' : (Language α)ᵐᵒᵖ), (Language.reverseIso α).symm l' = (MulOpposite.unop l').reverse
-- Mathlib.Topology.MetricSpace.Gluing
/-- Predistance on the disjoint union `Σ n, X n`.  -/
Metric.inductiveLimitDist : {X : ℕ → Type u} → [(n : ℕ) → MetricSpace (X n)] → ((n : ℕ) → X n → X (n + 1)) → (n : ℕ) × X n → (n : ℕ) × X n → ℝ
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.ι₀_desc : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₂.ι₀ (SSet.horn₃₂.desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) = f₀
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Initial state of `LocalContext.numIndices`, to keep track of which variables were introduced
during delaboration.  -/
Lean.PrettyPrinter.Delaborator.Context.lctxInitIndices : Lean.PrettyPrinter.Delaborator.Context → ℕ
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single.eq_1 : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι)
  (x : G i), RestrictedProduct.single A i x = ⟨Pi.single i x, ⋯⟩
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.toSpanSingletonLE.congr_simp : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass R S M] [inst_6 : TopologicalSpace M]
  [inst_7 : ContinuousAdd M] [inst_8 : ContinuousConstSMul S M] [inst_9 : TopologicalSpace R]
  [inst_10 : ContinuousSMul R M],
  ContinuousLinearMap.toSpanSingletonLE R S M = ContinuousLinearMap.toSpanSingletonLE R S M
-- Mathlib.Algebra.Group.Defs
RightCancelMonoid.toMonoid : {M : Type u} → [self : RightCancelMonoid M] → Monoid M
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mergeAll?.match_1.eq_1 : ∀ (motive : Option (Lean.TSyntax `tactic) → Sort u_1) (tac' : Lean.TSyntax `tactic)
  (h_1 : (tac' : Lean.TSyntax `tactic) → motive (some tac')) (h_2 : (x : Option (Lean.TSyntax `tactic)) → motive x),
  (match some tac' with
    | some tac' => h_1 tac'
    | x => h_2 x) =
    h_1 tac'
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.isUnit_of_orderTop_pos : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x : HahnSeries Γ R}, 0 < (x - 1).orderTop → IsUnit x
-- Std.Data.Iterators.Consumers.Set
/-- Traverses the given iterator and stores the emitted values in a `HashSet`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.toHashSet`.
 -/
Std.Iter.Total.toHashSet : {α β : Type w} →
  [inst : BEq β] →
    [inst_1 : Hashable β] →
      [inst_2 : Std.Iterator α Id β] →
        [Std.Iterators.Finite α Id] → [Std.IteratorLoop α Id Id] → Std.Iter.Total β → Std.HashSet β
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.AnalyzeResult.mk.injEq : ∀ (maxS? : Option FBinopElab.SRec) (hasUncomparable : Bool) (maxS?_1 : Option FBinopElab.SRec)
  (hasUncomparable_1 : Bool),
  ({ maxS? := maxS?, hasUncomparable := hasUncomparable } =
      { maxS? := maxS?_1, hasUncomparable := hasUncomparable_1 }) =
    (maxS? = maxS?_1 ∧ hasUncomparable = hasUncomparable_1)
-- Init.Data.List.Nat.BEq
List.isEqv_eq_decide : ∀ {α : Type u_1} {as bs : List α} {r : α → α → Bool},
  as.isEqv bs r =
    if h : as.length = bs.length then decide (∀ (i : ℕ) (h' : i < as.length), r as[i] bs[i] = true) else false
-- Aesop.Rule.Name
Aesop.RuleName.instBEq : BEq Aesop.RuleName
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_le_one_of_le₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀}
  [ZeroLEOneClass G₀], a ≤ b → 0 ≤ b → a / b ≤ 1
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.sigmaOfIsColimit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d),
  E.sigmaOfIsColimit hc hd =
    { toPreZeroHypercover := E.sigmaOfIsColimit hc, I₁ := fun x x_1 => PUnit.{w + 1}, Y := fun x x_1 x_2 => d.pt,
      p₁ := fun x x_1 x_2 =>
        CategoryTheory.Limits.Cofan.IsColimit.desc hd fun i =>
          CategoryTheory.CategoryStruct.comp (E.p₁ i.snd) (c.inj i.fst.1),
      p₂ := fun x x_1 x_2 =>
        CategoryTheory.Limits.Cofan.IsColimit.desc hd fun i =>
          CategoryTheory.CategoryStruct.comp (E.p₂ i.snd) (c.inj i.fst.2),
      w := ⋯ }
-- Mathlib.Order.Interval.Finset.Defs
Finset.card_Ici_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : LocallyFiniteOrderTop β] [inst_4 : DecidableLE (α × β)] (x : α × β),
  (Finset.Ici x).card = (Finset.Ici x.1).card * (Finset.Ici x.2).card
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.faithfullyFlat_iff : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔ Module.Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isOpen_basicOpen : ∀ {R : Type u} [inst : CommSemiring R] {a : R}, IsOpen ↑(PrimeSpectrum.basicOpen a)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.replaceFVarId : Lean.FVarId → Lean.Expr → Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern
-- Lean.Meta.ArgsPacker
/-- The arities of the functions being packed  -/
Lean.Meta.ArgsPacker.arities : Lean.Meta.ArgsPacker → Array ℕ
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.mem_equalizer : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B]
  [inst_7 : StarRing B] [inst_8 : StarModule R A] [inst_9 : FunLike F A B] [inst_10 : AlgHomClass F R A B]
  [inst_11 : StarHomClass F A B] (f g : F) (x : A), x ∈ StarAlgHom.equalizer f g ↔ f x = g x
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_floor_left' : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto (fun x => ↑⌊x⌋) (nhdsWithin (↑n) (Set.Iio ↑n)) (nhds (↑n - 1))
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.struct.x : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preregular C] →
      [inst_2 : CategoryTheory.FinitaryExtensive C] →
        {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} →
          (self : CategoryTheory.coherentTopology.struct✝ F) →
            (n : ℕ) → (F.obj (Opposite.op n)).obj.obj (Opposite.op (CategoryTheory.coherentTopology.struct.X✝ self n))
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The underlying `ContinuousMonoidHom`.  -/
ProfiniteGrp.Hom.hom : {M N : ProfiniteGrp.{u}} → M.Hom N → ↑M.toProfinite.toTop →ₜ* ↑N.toProfinite.toTop
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.holder_add_right : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G)
  (f : ↥(MeasureTheory.Lp E p μ)) (g₁ g₂ : ↥(MeasureTheory.Lp F q μ)),
  ContinuousLinearMap.holder r B f (g₁ + g₂) = ContinuousLinearMap.holder r B f g₁ + ContinuousLinearMap.holder r B f g₂
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `affineSpan` of a finite affinely independent family is `⊤` iff the
family's cardinality is one more than that of the finite-dimensional space.  -/
AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [FiniteDimensional k V] [inst_5 : Fintype ι] {p : ι → P},
  AffineIndependent k p → (affineSpan k (Set.range p) = ⊤ ↔ Fintype.card ι = Module.finrank k V + 1)
-- Mathlib.Tactic.Use
/-- Returns a `TacticM Unit` that either runs the tactic sequence from `discharger?` if it's
non-`none`, or it does `try with_reducible use_discharger`.  -/
Mathlib.Tactic.mkUseDischarger : Option (Lean.TSyntax `Lean.Parser.Tactic.discharger) → Lean.Elab.Tactic.TacticM (Lean.Elab.Tactic.TacticM Unit)
-- Mathlib.Analysis.Complex.Order
/-- We put a partial order on ℂ so that `z ≤ w` exactly if `w - z` is real and nonnegative.
Complex numbers with different imaginary parts are incomparable.
 -/
Complex.partialOrder : PartialOrder ℂ
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- For any `f : Arrow C` and `j : κ.ord.ToType`, the morphism
`((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f` identifies
to a morphism given by `SmallObject.ε I.homFamily`.  -/
CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              (f : CategoryTheory.Arrow C) →
                (j : κ.ord.ToType) →
                  CategoryTheory.Arrow.mk
                      (((CategoryTheory.SmallObject.iterationFunctor I κ).map (CategoryTheory.homOfLE ⋯)).app f) ≅
                    CategoryTheory.Arrow.mk
                      ((CategoryTheory.SmallObject.ε I.homFamily).app
                        (((CategoryTheory.SmallObject.iterationFunctor I κ).obj j).obj f))
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.toAdditionalLocalRules : Aesop.Frontend.RuleExpr → Lean.MetaM (Array Aesop.Frontend.RuleConfig)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.ReflectsFiniteColimits.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  [reflects :
    ∀ (J : Type) [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
      CategoryTheory.Limits.ReflectsColimitsOfShape J F],
  CategoryTheory.Limits.ReflectsFiniteColimits F
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.instCoeFunConnectedForallForallReachable : {V : Type u} → (G : SimpleGraph V) → CoeFun G.Connected fun x => ∀ (u v : V), G.Reachable u v
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_objs_of_tgt : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c d : C} {f : c ⟶ d},
  f ∈ S.arrows c d → d ∈ S.objs
-- Init.PropLemmas
and_not_self_iff : ∀ (a : Prop), a ∧ ¬a ↔ False
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.modify' : (Lean.Meta.Grind.Arith.CommRing.State → Lean.Meta.Grind.Arith.CommRing.State) → Lean.Meta.Grind.GoalM Unit
-- Lean.Environment
Lean.throwAlreadyImported : {α : Type} → Lean.ImportState → Std.HashMap Lean.Name Lean.ModuleIdx → ℕ → Lean.Name → IO α
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_eq_some_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α}, t.contains k = true → t.get? k = some k
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : β k → β k}, k' ∈ m.modify k f ↔ k' ∈ m
-- Mathlib.Analysis.Normed.Ring.Basic
/-- If `α` is a seminormed ring, then `‖a ^ n‖₊ ≤ ‖a‖₊ ^ n` for `n > 0`.
See also `nnnorm_pow_le`.  -/
nnnorm_pow_le' : ∀ {α : Type u_2} [inst : SeminormedRing α] (a : α) {n : ℕ}, 0 < n → ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n
-- Std.Time.DateTime
Std.Time.DateTime.instHSubOffset_4 : HSub Std.Time.DateTime Std.Time.Second.Offset Std.Time.DateTime
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.MethodsRef.toMethods : Lean.Meta.Sym.DSimp.MethodsRef → Lean.Meta.Sym.DSimp.Methods
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.of_algEquiv : ∀ {F : Type u} {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Field F] [inst_3 : Algebra K L]
  [inst_4 : Algebra K F] (p : Polynomial K) (f : F ≃ₐ[K] L) [Polynomial.IsSplittingField K F p],
  Polynomial.IsSplittingField K L p
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.instCompl : {α : Type u_1} → [inst : HeytingAlgebra α] → Compl (Heyting.Regular α)
-- Mathlib.Order.Minimal
Maximal.eq_of_le : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : PartialOrder α], Maximal P x → P y → x ≤ y → x = y