mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_sub_const_Ioi : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x - a) ⁻¹' Set.Ioi b = Set.Ioi (b + a)
-- Mathlib.Algebra.Lie.InvariantForm
LinearMap.BilinForm.lieInvariant_iff : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (Φ : LinearMap.BilinForm R M) [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M],
  LinearMap.BilinForm.lieInvariant L Φ ↔ Φ ∈ LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
/-- The canonical morphism from a seminormed group `V` to its completion.  -/
SemiNormedGrp.completion.incl : {V : SemiNormedGrp} → V ⟶ SemiNormedGrp.completion.obj V
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.maxLiteral.eq_1 : ∀ (f : Std.Sat.CNF ℕ), f.maxLiteral = (Array.filterMap Std.Sat.CNF.Clause.maxLiteral f.clauses).max?
-- Mathlib.Analysis.Convolution
/-- The convolution of `f` and `g` exists when the function `t ↦ L (f t) (g (x - t))` is integrable
for all `x : G`. There are various conditions on `f` and `g` to prove this.  -/
MeasureTheory.ConvolutionExists : {𝕜 : Type u𝕜} →
  {G : Type uG} →
    {E : Type uE} →
      {E' : Type uE'} →
        {F : Type uF} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedAddCommGroup E'] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NontriviallyNormedField 𝕜] →
                  [inst_4 : NormedSpace 𝕜 E] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      [inst_6 : NormedSpace 𝕜 F] →
                        [inst_7 : MeasurableSpace G] →
                          [Sub G] →
                            (G → E) →
                              (G → E') →
                                (E →L[𝕜] E' →L[𝕜] F) →
                                  autoParam (MeasureTheory.Measure G) MeasureTheory.ConvolutionExists._auto_1 → Prop
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- `GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  -/
Matrix.GeneralLinearGroup : (n : Type u) → (R : Type v) → [DecidableEq n] → [Fintype n] → [Semiring R] → Type (max v u)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
/-- `TopModuleCat.ker` is indeed the kernel in `TopModuleCat R`.  -/
TopModuleCat.isLimitKer : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {M N : TopModuleCat R} →
        (φ : M ⟶ N) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (TopModuleCat.kerι φ) ⋯)
-- Mathlib.Order.Filter.Extr
IsMaxFilter.filter_inf : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → ∀ (l' : Filter α), IsMaxFilter f (l ⊓ l') a
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mk_le_mk : ∀ {G : Type u_1} [inst : Group G] {s t : Submonoid G} (h_inv : ∀ {x : G}, x ∈ s.carrier → x⁻¹ ∈ s.carrier)
  (h_inv' : ∀ {x : G}, x ∈ t.carrier → x⁻¹ ∈ t.carrier),
  { toSubmonoid := s, inv_mem' := h_inv } ≤ { toSubmonoid := t, inv_mem' := h_inv' } ↔ s ≤ t
-- Mathlib.Data.List.ProdSigma
List.nil_product : ∀ {α : Type u_1} {β : Type u_2} (l : List β), [] ×ˢ l = []
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Given a linearly ordered type `ι`, this is the shape of multicoequalizer diagrams
corresponding to situations where we want to coequalize two families of maps
`V ⟨i, j⟩ ⟶ U i` and `V ⟨i, j⟩ ⟶ U j` with `i < j`.  -/
CategoryTheory.Limits.MultispanShape.ofLinearOrder : (ι : Type w) → [LinearOrder ι] → CategoryTheory.Limits.MultispanShape
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.ae_eq_of_ae_le_of_lintegral_le : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  f ≤ᵐ[μ] g → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → AEMeasurable g μ → ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ → f =ᵐ[μ] g
-- Mathlib.Topology.Constructions.SumProd
/-- `X × (Y ⊕ Z)` is homeomorphic to `X × Y ⊕ X × Z`.  -/
Homeomorph.prodSumDistrib : {X : Type u} →
  {Y : Type v} →
    {Z : Type u_2} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] → [inst_2 : TopologicalSpace Z] → X × (Y ⊕ Z) ≃ₜ X × Y ⊕ X × Z
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Inverse images along equal morphisms are isomorphic.  -/
AlgebraicGeometry.Scheme.Modules.pullbackCongr : {X Y : AlgebraicGeometry.Scheme} →
  {f g : X ⟶ Y} → f = g → (AlgebraicGeometry.Scheme.Modules.pullback f ≅ AlgebraicGeometry.Scheme.Modules.pullback g)
-- Init.Data.UInt.Lemmas
UInt64.toUInt64_toUInt32 : ∀ (n : UInt64), n.toUInt32.toUInt64 = n % 4294967296
-- Mathlib.Order.Category.LinOrd
LinOrd.instConcreteCategoryOrderHomCarrier : CategoryTheory.ConcreteCategory LinOrd fun x1 x2 => ↑x1 →o ↑x2
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingsBefore_bot : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] {a b : ℝ} {f : ι → Ω → ℝ}
  {ω : Ω}, MeasureTheory.upcrossingsBefore a b f ⊥ ω = ⊥
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.of_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {m n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → m ≤ n → ContDiffOn 𝕜 m f s
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.instHasLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {K : Type z} [inst_2 : CategoryTheory.Category.{z', z} K]
  [CategoryTheory.Limits.HasLimitsOfShape K D], CategoryTheory.Limits.HasLimitsOfShape K (CategoryTheory.Sheaf J D)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_trans_isoWhiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H K : CategoryTheory.Functor D E} (α : F ≅ G) (β : H ≅ K),
  F.isoWhiskerLeft β ≪≫ CategoryTheory.Functor.isoWhiskerRight α K =
    CategoryTheory.Functor.isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instIsScalarTowerSubtypeMem : ∀ {R' : Type u'} {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) [inst_3 : Semiring R'] [inst_4 : SMul R' R] [inst_5 : Module R' A]
  [inst_6 : IsScalarTower R' R A], IsScalarTower R' R ↥S
-- Mathlib.Analysis.Complex.Basic
RCLike.I_to_complex : RCLike.I = Complex.I
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The `n`-th homology of the alternating constant complex is `X` for `n = 0`.  -/
ChainComplex.alternatingConstHomologyZero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        (X : C) → HomologicalComplex.homology (ChainComplex.alternatingConst.obj X) 0 ≅ X
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.isoMk_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory}
  (e : X.obj ≅ Y.obj), (P.isoMk e).inv = CategoryTheory.ObjectProperty.homMk e.inv
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prod.etaIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C × D),
  (CategoryTheory.prod.etaIso X).hom =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
-- Mathlib.Topology.Clopen
Set.Finite.isClopen_biUnion : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type u_2} {s : Set Y} {f : Y → Set X},
  s.Finite → (∀ i ∈ s, IsClopen (f i)) → IsClopen (⋃ i ∈ s, f i)
-- Mathlib.Topology.EMetricSpace.Diam
/-- The extended diameter of a union is controlled by the diameter of the sets,
and the edistance between two points in the sets.  -/
Metric.ediam_union_le_add_edist : ∀ {X : Type u_2} {s t : Set X} {x y : X} [inst : PseudoEMetricSpace X],
  x ∈ s → y ∈ t → Metric.ediam (s ∪ t) ≤ Metric.ediam s + edist x y + Metric.ediam t
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.compLeft.eq_1 : ∀ {α : Type u_5} {β : Type u_6} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] (f : α →+ β) (I : Type u_7),
  f.compLeft I = { toFun := fun h => ⇑f ∘ h, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.addRatCaseSound : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : DecidableEq α]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ]
  [inst_3 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
      ∀ (c : β) (pivot : Std.Sat.Literal α) (f' : σ) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ)),
        Std.Tactic.BVDecide.LRAT.Internal.Limplies α pivot c →
          Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c pivot rupHints ratHints = (f', true) →
            ∀ (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)),
              (∀ a ∈ restPrf, Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction a) →
                (Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f' →
                    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f' →
                      (∀ a ∈ restPrf, Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction a) →
                        Std.Tactic.BVDecide.LRAT.Internal.lratChecker f' restPrf =
                            Std.Tactic.BVDecide.LRAT.Internal.Result.success →
                          Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f') →
                  Std.Tactic.BVDecide.LRAT.Internal.lratChecker f' restPrf =
                      Std.Tactic.BVDecide.LRAT.Internal.Result.success →
                    Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f
-- Mathlib.Analysis.Convolution
HasCompactSupport.convolutionExists_right : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [inst_9 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G],
  HasCompactSupport g → MeasureTheory.LocallyIntegrable f μ → Continuous g → MeasureTheory.ConvolutionExists f g L μ
-- Mathlib.Tactic.Variable
/-- The `variable?` command has the same syntax as `variable`, but it will auto-insert
missing instance arguments wherever they are needed.
It does not add variables that can already be deduced from others in the current context.
By default the command checks that variables aren't implied by earlier ones, but it does *not*
check that earlier variables aren't implied by later ones.
Unlike `variable`, the `variable?` command does not support changing variable binder types.

The `variable?` command will give a suggestion to replace itself with a command of the form
`variable? ...binders... => ...binders...`.  The binders after the `=>` are the completed
list of binders. When this `=>` clause is present, the command verifies that the expanded
binders match the post-`=>` binders.  The purpose of this is to help keep code that uses
`variable?` resilient against changes to the typeclass hierarchy, at least in the sense
that this additional information can be used to debug issues that might arise.
One can also replace `variable? ...binders... =>` with `variable`.

The core algorithm is to try elaborating binders one at a time, and whenever there is a
typeclass instance inference failure, it synthesizes binder syntax for it and adds it to
the list of binders and tries again, recursively. There are no guarantees that this
process gives the "correct" list of binders.

Structures tagged with the `variable_alias` attribute can serve as aliases for a collection
of typeclasses. For example, given
```lean
@[variable_alias]
structure VectorSpace (k V : Type*) [Field k] [AddCommGroup V] [Module k V]
```
then `variable? [VectorSpace k V]` is
equivalent to `variable {k V : Type*} [Field k] [AddCommGroup V] [Module k V]`, assuming
that there are no pre-existing instances on `k` and `V`.
Note that this is not a simple replacement: it only adds instances not inferable
from others in the current scope.

A word of warning: the core algorithm depends on pretty printing, so if terms that appear
in binders do not round trip, this algorithm can fail. That said, it has some support
for quantified binders such as `[∀ i, F i]`.  -/
Mathlib.Command.Variable.variable? : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_iff_forall_nat_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : ℕ∞}, ContDiffWithinAt 𝕜 (↑n) f s x ↔ ∀ (m : ℕ), ↑m ≤ n → ContDiffWithinAt 𝕜 (↑m) f s x
-- Mathlib.RingTheory.Localization.Integral
/-- If `t` is `R`-integral in `S[M⁻¹]` where `M` is a submonoid of `R`,
then `m • t` is integral in `S` for some `m ∈ M`.  -/
IsLocalization.exists_isIntegral_smul_of_isIntegral_map : ∀ {R : Type u_5} {S : Type u_6} {Sₘ : Type u_7} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing Sₘ]
  [inst_3 : Algebra R S] [inst_4 : Algebra S Sₘ] [inst_5 : Algebra R Sₘ] [IsScalarTower R S Sₘ] (M : Submonoid R)
  [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] {x : S},
  IsIntegral R ((algebraMap S Sₘ) x) → ∃ m ∈ M, IsIntegral R (m • x)
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_mono : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R}, I ≤ J → I.height ≤ J.height
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_hom_app_app_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type}
  [inst_1 : CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) (X : J)
  (X_1 : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
  (a :
    ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K).obj
          X).obj
      X_1),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso A
                    K).hom.app
              X).app
          X_1))
      a =
    a
-- Mathlib.Probability.Kernel.Disintegration.Unique
ProbabilityTheory.Kernel.apply_eq_measure_condKernel_of_compProd_eq : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  {ρ : ProbabilityTheory.Kernel α (β × Ω)} [inst_3 : ProbabilityTheory.IsFiniteKernel ρ]
  {κ : ProbabilityTheory.Kernel (α × β) Ω} [ProbabilityTheory.IsFiniteKernel κ],
  ρ.fst.compProd κ = ρ → ∀ (a : α), (fun b => κ (a, b)) =ᵐ[ρ.fst a] ⇑(ρ a).condKernel
-- Mathlib.Order.Zorn
zorn_subset_nonempty : ∀ {α : Type u_1} (S : Set (Set α)),
  (∀ c ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub) →
    ∀ x ∈ S, ∃ m, x ⊆ m ∧ Maximal (fun x => x ∈ S) m
-- Mathlib.Data.Sym.Basic
Sym.mem_cons_self : ∀ {α : Type u_1} {n : ℕ} (a : α) (s : Sym α n), a ∈ a ::ₛ s
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace_trans : ∀ (F : Type u_3) (E : Type u_4) (K : Type u_5) [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra E K] [inst_5 : Algebra F K] [inst_6 : IsScalarTower F E K]
  [inst_7 : Algebra.IsIntegral F E] [inst_8 : Algebra.IsIntegral F K] [inst_9 : CharZero F]
  [inst_10 : Algebra.IsIntegral E K] [inst_11 : CharZero E],
  Algebra.normalizedTrace F E ∘ₗ ↑F (Algebra.normalizedTrace E K) = Algebra.normalizedTrace F K
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.toFinite_eq_zero_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ],
  μ.toFinite = 0 ↔ μ = 0
-- Mathlib.Data.Rel
/-- Image of a set under a relation.  -/
SetRel.image : {α : Type u_1} → {β : Type u_2} → SetRel α β → Set α → Set β
-- Init.Data.UInt.Lemmas
USize.toFin_sub : ∀ (a b : USize), (a - b).toFin = a.toFin - b.toFin
-- Aesop.Tree.Data
Aesop.Goal.firstProvenRapp? : Aesop.Goal → BaseIO (Option Aesop.RappRef)
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `wbtw_const_add_iff`. -/
Wbtw.const_add : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Wbtw R x y z → Wbtw R (v + x) (v + y) (v + z)
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.nhds_zero_eq : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G), nhds 0 = B.filter
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.mkBreak : Lean.Elab.Do.ControlStack → Bool → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instFunLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β],
  sInfHom.instFunLike = { coe := sInfHom.toFun, coe_injective := ⋯ }
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {inst_2 : DecidableEq (K →+* ℂ)}
  [inst_3 : DecidableEq (K →+* ℂ)], NumberField.house.c✝ K = NumberField.house.c✝ K
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem!_push : ∀ (data : ByteArray) (b : UInt8) (i : ℕ), (data.push b)[i]! = if i = data.size then b else data[i]!
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.IsColimit.inj_desc_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X}
  (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β) {Z : C} (h : d.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (hc.desc d) h) =
    CategoryTheory.CategoryStruct.comp (d.inj i) h
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If a sequence `v` of real numbers satisfies `k * v n ≤ v (n+1)` with `1 < k`,
then it goes to +∞.  -/
tendsto_atTop_of_geom_le : ∀ {v : ℕ → ℝ} {c : ℝ}, 0 < v 0 → 1 < c → (∀ (n : ℕ), c * v n ≤ v (n + 1)) → Filter.Tendsto v Filter.atTop Filter.atTop
-- Init.Data.Bool
Bool.ite_eq_false : ∀ {b : Bool} {p q : Prop}, (if b = false then p else q) ↔ if b = true then q else p
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.continuousAt : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {x : P}, ContinuousAt (⇑e) x
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.toPartialEquiv_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), ↑e.toPartialEquiv.symm = ⇑e.symm
-- Init.Data.Int.Lemmas
Int.zero_ne_negSucc : ∀ (n : ℕ), 0 ≠ Int.negSucc n
-- Mathlib.Analysis.Convex.EGauge
/-- If `c • x ∈ s` and `c ≠ 0`, then `egauge 𝕜 s x` is at most `(‖c‖₊⁻¹ : ℝ≥0)`.

See also `egauge_le_of_smul_mem`.  -/
egauge_le_of_smul_mem_of_ne : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {c : 𝕜}
  {s : Set E} {x : E}, c • x ∈ s → c ≠ 0 → egauge 𝕜 s x ≤ ↑‖c‖₊⁻¹
-- Mathlib.Data.Part
Part.left_dom_of_union_dom : ∀ {α : Type u_1} [inst : Union α] {a b : Part α}, (a ∪ b).Dom → a.Dom
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.neg : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E},
  IntervalIntegrable f μ a b → IntervalIntegrable (-f) μ a b
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality
version: if the total weight of a finite set of pigeons is greater than or equal to `n • b`, and
they are sorted into `n > 0` pigeonholes, then for some pigeonhole, the total weight of the pigeons
in this pigeonhole is greater than or equal to `b`.  -/
Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M}
  {b : M} [inst_1 : AddCommMonoid M] [inst_2 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  (∀ a ∈ s, f a ∈ t) → t.Nonempty → t.card • b ≤ ∑ x ∈ s, w x → ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, w x
-- Init.Data.BitVec.Bitblast
Bool.atLeastTwo_true_mid : ∀ {a c : Bool}, a.atLeastTwo true c = (a || c)
-- Mathlib.Data.TypeVec
/-- `repeat n t` is a `n-length` type vector that contains `n` occurrences of `t`  -/
TypeVec.repeat : (n : ℕ) → Type u → TypeVec.{u} n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (fallback : (a : α) × β a),
  Std.DTreeMap.Internal.Impl.leaf.getEntryD k fallback = fallback
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_isBasis'_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {I X : Set α},
  (N.comap f).IsBasis' I X ↔ N.IsBasis' (f '' I) (f '' X) ∧ Set.InjOn f I ∧ I ⊆ X
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_inf_eq : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f g : ι → α},
  BddBelow (Set.range f) → BddBelow (Set.range g) → ⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ ⨅ x, g x
-- Mathlib.Tactic.Linarith.Datatypes
/-- The coefficients of the comparison, stored as list of pairs `(i, a)`,
where `i` is the index of a recorded atom, and `a` is the coefficient.  -/
Mathlib.Tactic.Linarith.Comp.coeffs : Mathlib.Tactic.Linarith.Comp → Mathlib.Tactic.Linarith.Linexp
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_le_map_iff_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f → ∀ (p q : Submodule R M), Submodule.map f p ≤ Submodule.map f q ↔ p ≤ q
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
List.step_iterM_nil : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w},
  ([].iterM m).step = pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_Iic : ∀ {n : ℕ} (i : Fin n), Fin.castSucc '' Set.Iic i = Set.Iic i.castSucc
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_div' : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a b : ℚ},
  ↑a.den ≠ 0 →
    ↑b.num ≠ 0 →
      Lean.Grind.Field.NormNum.ofRat (a / b) = Lean.Grind.Field.NormNum.ofRat a / Lean.Grind.Field.NormNum.ofRat b
-- Mathlib.Data.Finset.SymmDiff
/-- See `symmDiff_subset_sdiff'` for the swapped version of this.  -/
Finset.symmDiff_subset_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s \ t ⊆ symmDiff s t
-- Mathlib.Data.Num.Lemmas
PosNum.linearOrder : LinearOrder PosNum