mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
/-- Produces an `R`-algebra map from `U.restrictScalars R` given an `S`-algebra map from `U`.

This is a special case of `AlgHom.restrictScalars` that can be helpful in elaboration.  -/
Subalgebra.ofRestrictScalars : (R : Type u) →
  {S : Type v} →
    {A : Type w} →
      {B : Type u₁} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Algebra S A] →
                    [inst_6 : Algebra R A] →
                      [inst_7 : Algebra S B] →
                        [inst_8 : Algebra R B] →
                          [inst_9 : IsScalarTower R S A] →
                            [IsScalarTower R S B] →
                              (U : Subalgebra S A) → (↥U →ₐ[S] B) → ↥(Subalgebra.restrictScalars R U) →ₐ[R] B
-- Mathlib.Topology.EMetricSpace.Defs
instEMetricSpaceAddOpposite.eq_1 : ∀ {α : Type u_2} [inst : EMetricSpace α], instEMetricSpaceAddOpposite = EMetricSpace.induced AddOpposite.unop ⋯ inst
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E},
  MeromorphicAt f x ↔ ∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = (z - x) ^ n • g z
-- Std.Data.TreeSet.Basic
Std.TreeSet.mk.injEq : ∀ {α : Type u} {cmp : autoParam (α → α → Ordering) Std.TreeSet._auto_1} (inner inner_1 : Std.TreeMap α Unit cmp),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Probability.Kernel.Disintegration.Unique
ProbabilityTheory.condKernel_const : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] (ρ : MeasureTheory.Measure (β × Ω))
  [inst_4 : MeasureTheory.IsFiniteMeasure ρ] (a : α),
  (fun b => (ProbabilityTheory.Kernel.const α ρ).condKernel (a, b)) =ᵐ[ρ.fst] ⇑ρ.condKernel
-- Mathlib.Topology.LocallyFinsupp
/-- Functions with locally finite support within `U` form an ordered commutative group.
 -/
Function.locallyFinsuppWithin.instIsOrderedAddMonoid : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y]
  [inst_2 : LinearOrder Y] [IsOrderedAddMonoid Y], IsOrderedAddMonoid (Function.locallyFinsuppWithin U Y)
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.Hom.ext : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₂} D} {F : C → D}
  {P : CategoryTheory.MorphismProperty D} {inst_1 : P.IsMultiplicative} {X Y : CategoryTheory.InducedWideCategory D F P}
  {x y : X.Hom Y}, x.hom = y.hom → x = y
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `MulHom.pi`.

---

A family of MulHom's `f a : γ →ₙ* β a` defines a MulHom `MulHom.pi f : γ →ₙ* Π a, β a`
given by `MulHom.pi f x b = f b x`.  -/
Pi.mulHom : {I : Type u} →
  {f : I → Type v} →
    [inst : (i : I) → Mul (f i)] → {γ : Type w} → [inst_1 : Mul γ] → ((i : I) → γ →ₙ* f i) → γ →ₙ* (i : I) → f i
-- Lean.Meta.Constructions.NoConfusion
/-- Variant of `withEqTelescope`, but when `xi = yi`, no variable is introduced, and `Eq.refl` is used
for the expression, unless this is the last one. (This special case could be dropped if we do not
generate no-confusion principles for constructors with only prop-valued fields.)
 -/
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.withNeededEqTelescope : {α : Type} →
  [Inhabited α] → Array Lean.Expr → Array Lean.Expr → (Array Lean.Expr → Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Lean.Parser.Do
Lean.Parser.Term.doLetArrow.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.SetLike.Basic
SetLike.coe_mem : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} (x : ↥p), ↑x ∈ p
-- Mathlib.NumberTheory.NumberField.Units.Basic
/-- The group homomorphism `(𝓞 K)ˣ →* ℂˣ` induced by a complex embedding of `K`.
 -/
NumberField.Units.complexEmbedding : {K : Type u_1} → [inst : Field K] → (K →+* ℂ) → (NumberField.RingOfIntegers K)ˣ →* ℂˣ
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
/-- Upgraded of `CategoryTheory.Abelian.Ext.mapExactFunctor` into an additive homomorphism.  -/
CategoryTheory.Functor.mapExtAddHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {D : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} D] →
          [inst_3 : CategoryTheory.Abelian D] →
            (F : CategoryTheory.Functor C D) →
              [F.Additive] →
                [CategoryTheory.Limits.PreservesFiniteLimits F] →
                  [CategoryTheory.Limits.PreservesFiniteColimits F] →
                    [inst_7 : CategoryTheory.HasExt C] →
                      [inst_8 : CategoryTheory.HasExt D] →
                        (X Y : C) →
                          (n : ℕ) → CategoryTheory.Abelian.Ext X Y n →+ CategoryTheory.Abelian.Ext (F.obj X) (F.obj Y) n
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- A column partitioned matrix in a Star ring when conjugate transposed gives a row partitioned
matrix with the columns of the initial matrix conjugate transposed to become rows.  -/
Matrix.conjTranspose_fromCols_eq_fromRows_conjTranspose : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Star R] (A₁ : Matrix m n₁ R)
  (A₂ : Matrix m n₂ R), (A₁.fromCols A₂).conjTranspose = A₁.conjTranspose.fromRows A₂.conjTranspose
-- Init.Data.SInt.Lemmas
Int16.toInt_bmod_two_pow_numBits : ∀ (x : Int16), x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` is closed under addition.  -/
AddSubmonoid.add_mem : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) {x y : M}, x ∈ S → y ∈ S → x + y ∈ S
-- Mathlib.Analysis.Normed.Field.Basic
/-- A densely normed field is a normed field for which the image of the norm is dense in `ℝ≥0`,
which means it is also nontrivially normed. However, not all nontrivially normed fields are densely
normed; in particular, the `Padic`s exhibit this fact.  -/
DenselyNormedField : Type u_5 → Type u_5
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.zeckendorf_sum_fib : ∀ {l : List ℕ}, l.IsZeckendorfRep → (List.map Nat.fib l).sum.zeckendorf = l
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, (m.erase k).getKey! k = default
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `none` if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryGT? : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → Option (α × β)
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_smul_right : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F) {r : 𝕜}, inner 𝕜 x (r • y) = r * inner 𝕜 x y
-- Init.Data.SInt.Lemmas
Int16.le_antisymm_iff : ∀ {a b : Int16}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.Algebra.BigOperators.Group.Finset.Interval
Finset.prod_Ico_int_div : ∀ (b : ℕ) {α : Type u_1} [inst : CommGroup α] (f : ℤ → α), ∏ n ∈ Finset.Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
-- Init.Data.UInt.Basic
/-- Converts 32-bit unsigned integers to word-sized unsigned integers.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.toUSize : UInt32 → USize
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
/-- A Serre class in an abelian category consists of a predicate which
holds for the zero object and is closed under subobjects, quotients, extensions.  -/
CategoryTheory.ObjectProperty.IsSerreClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.of_le_isUnit_of_bijective : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M : Submonoid R},
  Algebra.algebraMapSubmonoid S M ≤ IsUnit.submonoid S → Function.Bijective ⇑(algebraMap R S) → IsLocalization M S
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is
empty.
 -/
Std.DTreeMap.minEntry! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap α β cmp → (a : α) × β a
-- Mathlib.Order.Filter.CardinalInter
Filter.EventuallyLE.cardinal_bInter : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι},
  Cardinal.mk ↑S < c →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) → ⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_map_equiv : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {β : Type u_6} [inst_2 : MeasurableSpace β] (e : α ≃ᵐ β) (f : β → G),
  ∫ (y : β), f y ∂MeasureTheory.Measure.map (⇑e) μ = ∫ (x : α), f (e x) ∂μ
-- Mathlib.Algebra.Group.Finsupp
Finsupp.support_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {g₁ g₂ : ι →₀ M} [inst_1 : DecidableEq ι],
  (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
/-- The commutative square associated to a bi-Cartesian square in a lattice.  -/
Lattice.BicartSq.commSq : ∀ {T : Type u} {x₁ x₂ x₃ x₄ : T} [inst : Lattice T] (sq : Lattice.BicartSq x₁ x₂ x₃ x₄),
  CategoryTheory.CommSq (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
    (CategoryTheory.homOfLE ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasStrongEpiImages.strong_factorThruImage : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasImages C}
  [self : CategoryTheory.Limits.HasStrongEpiImages C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)
-- Mathlib.Algebra.Module.Lattice
Submodule.IsLattice.mk : ∀ {R : Type u_1} [inst : CommRing R] {A : outParam (Type u_2)} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {V : Type u_3} [inst_3 : AddCommMonoid V] [inst_4 : Module R V] [inst_5 : Module A V] [inst_6 : IsScalarTower R A V]
  [inst_7 : IsScalarTower R A V] {M : Submodule R V}, M.FG → Submodule.span A ↑M = ⊤ → Submodule.IsLattice A M
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_modify_EStateM_apply_eq : ∀ {σ ε : Type} {post : PUnit.{1} → σ → Prop} {epost : ε → σ → Prop} (f : σ → σ),
  Std.Internal.Do.wp (modify f) post epost =
    Std.Internal.Do.wp (MonadStateOf.modifyGet fun s => (PUnit.unit, f s)) post epost
-- Mathlib.GroupTheory.Congruence.Defs
/-- The infimum of a set of additive congruence relations is the same as the infimum
of the set's image under the map to the underlying binary relation.  -/
AddCon.coe_sInf : ∀ {M : Type u_1} [inst : Add M] (S : Set (AddCon M)), ⇑(sInf S) = sInf (DFunLike.coe '' S)
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeFunctorPreservesLimitsOfShapeOfPreservesLimitsOfShapeColim : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) (K' : Type u_6) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_2, u_6} K'] [inst_2 : CategoryTheory.Category.{v_3, u_1} J]
  [inst_3 : CategoryTheory.Category.{v_5, u_3} C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K' C]
  [CategoryTheory.Limits.PreservesLimitsOfShape K CategoryTheory.Limits.colim],
  (CategoryTheory.ObjectProperty.preservesLimitsOfShape K).IsClosedUnderColimitsOfShape K'
-- Mathlib.Analysis.Analytic.Composition
/-- The identity formal multilinear series, with all coefficients equal to `0` except for `n = 1`
where it is (the continuous multilinear version of) the identity. We allow an arbitrary
constant coefficient `x`.  -/
FormalMultilinearSeries.id : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → E → FormalMultilinearSeries 𝕜 E E
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_sub : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D1 D2 : Derivation R A M),
  ⇑(D1 - D2) = ⇑D1 - ⇑D2
-- Mathlib.Algebra.Star.StarAlgHom
/-- A *⋆-algebra* equivalence is an equivalence preserving addition, multiplication, scalar
multiplication and the star operation, which allows for considering both unital and non-unital
equivalences with a single structure.  -/
«term_≃⋆ₐ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.isLUB_norm : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [Nonempty α] (f : ↥(lp E ⊤)),
  IsLUB (Set.range fun i => ‖↑f i‖) ‖f‖
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal.mk.sizeOf_spec : ∀ (goal : Aesop.GoalRef) (priority : Aesop.Percent) (lastExpandedInIteration addedInIteration : Aesop.Iteration),
  sizeOf
      { goal := goal, priority := priority, lastExpandedInIteration := lastExpandedInIteration,
        addedInIteration := addedInIteration } =
    1 + sizeOf goal + sizeOf priority + sizeOf lastExpandedInIteration + sizeOf addedInIteration
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.TextDocumentClientCapabilities.mk.sizeOf_spec : ∀ (completion? : Option Lean.Lsp.CompletionClientCapabilities)
  (codeAction? : Option Lean.Lsp.CodeActionClientCapabilities)
  (inlayHint? : Option Lean.Lsp.InlayHintClientCapabilities),
  sizeOf { completion? := completion?, codeAction? := codeAction?, inlayHint? := inlayHint? } =
    1 + sizeOf completion? + sizeOf codeAction? + sizeOf inlayHint?
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_apply_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.kahler x) y = ↑(inner ℝ x y) + (o.areaForm x) y • Complex.I
-- Init.Classical
Classical.not_forall : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
-- Lean.Meta.Tactic.Util
Lean.MVarId.inferInstance : Lean.MVarId → Lean.MetaM Unit
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceOfIntLE : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPullback.inl_snd' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y}
  (h : b.IsBilimit), CategoryTheory.IsPullback b.inl 0 b.snd 0
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgebra.instCommSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {S : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Algebra R S] →
              [inst_3 : DecidableEq ι] →
                [inst_4 : AddMonoid ι] →
                  [inst_5 : CommSemiring A] →
                    [inst_6 : Algebra R A] →
                      (𝒜 : ι → Submodule R A) → [GradedAlgebra 𝒜] → CommSemiring ↥(Submodule.baseChange S (𝒜 0))
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.affineAnd.congr_simp : ∀ (Q Q_1 : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  Q = Q_1 →
    ∀ ⦃X Y : AlgebraicGeometry.Scheme⦄ (x x_1 : X ⟶ Y),
      x = x_1 →
        ∀ [inst : AlgebraicGeometry.IsAffine Y], AlgebraicGeometry.affineAnd Q x = AlgebraicGeometry.affineAnd Q_1 x_1
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.smoothOfRelativeDimension_iff : ∀ (n : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.SmoothOfRelativeDimension n f ↔
    ∀ (x : ↥X),
      ∃ U,
        ∃ (_ : AlgebraicGeometry.IsAffineOpen U),
          ∃ V,
            ∃ (_ : AlgebraicGeometry.IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              RingHom.IsStandardSmoothOfRelativeDimension n
                (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e))
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_lt : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {p q : ℚ≥0}, ↑p < ↑q ↔ p < q
-- Mathlib.Tactic.Linter.DocString
/-- Currently, this function simply removes `currIndent` spaces after each `\n`
in the input string `docString`.

If/when the `docString` linter expands, it may take on more string processing.
 -/
_private.Mathlib.Tactic.Linter.DocString.0.Mathlib.Linter.deindentString : ℕ → String → String
-- Aesop.RuleSet
_private.Aesop.RuleSet.0.Aesop.BaseRuleSet.isErased : Aesop.BaseRuleSet → Aesop.RuleName → Bool
-- Mathlib.Order.RelIso.Basic
RelEmbedding.isLinearOrder : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [IsLinearOrder β s],
  IsLinearOrder α r
-- Init.Data.List.Lemmas
List.mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ List.replicate n a ↔ n ≠ 0 ∧ b = a
-- Mathlib.ModelTheory.Syntax
/-- Substitutes the free variables in a bounded formula with terms, leaving bound variables
unchanged.  -/
FirstOrder.Language.BoundedFormula.subst : {L : FirstOrder.Language} →
  {α : Type u'} → {β : Type v'} → {n : ℕ} → L.BoundedFormula α n → (α → L.Term β) → L.BoundedFormula β n
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_self : ∀ {α : Type u_1} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst_3 : MeasureTheory.IsFiniteMeasure μ] (Y : α → Ω),
  ⇑(ProbabilityTheory.condDistrib Y Y μ) =ᵐ[MeasureTheory.Measure.map Y μ] ⇑ProbabilityTheory.Kernel.id
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.finite_iUnion_left_iff : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ι : Type u_3} {I : Set ι},
  I.Finite → ∀ {s : ι → Set X} {t : Set X}, Metric.AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, Metric.AreSeparated (s i) t
-- Init.Data.Int.Order
Int.eq_zero_of_dvd_of_natAbs_lt_natAbs : ∀ {d n : ℤ}, d ∣ n → n.natAbs < d.natAbs → n = 0
-- Mathlib.Geometry.Manifold.PoincareConjecture
_private.Mathlib.Geometry.Manifold.PoincareConjecture.0.exists_homeomorph_isEmpty_diffeomorph_sphere_seven : ProofWanted
  (∃ M x x_1,
    ∃ (_ : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 7))) (↑⊤) M),
      ∃ _homeo,
        IsEmpty
          (Diffeomorph (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 7)))
            (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 7))) M ↑(Metric.sphere 0 1) ↑⊤))
-- Mathlib.ModelTheory.Substructures
/-- The substructure generated by a set includes the set.  -/
FirstOrder.Language.Substructure.subset_closure : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M},
  s ⊆ ↑((FirstOrder.Language.Substructure.closure L).toFun s)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_sSup : ∀ {x : ℝ*}, ¬x.Infinite → x.IsSt (sSup {y | ↑y < x})
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.hom_inv_leftUnitor : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R},
  ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv = ↑(TensorProduct.lid R ↑M).symm
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.of_subsingleton_cod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [Subsingleton β], MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.Order.SupIndep
iSupIndep.injOn : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {t : ι → α}, iSupIndep t → Set.InjOn t {i | t i ≠ ⊥}
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.sumEquiv_functor_map : ∀ {J : Type u_1} {K : Type u_2} {X Y : CategoryTheory.Discrete (J ⊕ K)} (f : X ⟶ Y),
  CategoryTheory.Discrete.sumEquiv.functor.map f = ULift.rec (fun down => CategoryTheory.eqToHom ⋯) f
-- Mathlib.Analysis.Convex.Basic
Antitone.convex_gt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Antitone f → ∀ (r : β), Convex 𝕜 {x | r < f x}
-- Mathlib.Topology.Order.Bornology
OrderDual.instIsOrderBornology : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α], IsOrderBornology αᵒᵈ
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.div_eq_iff_eq_mul_of_dvd : ∀ {R : Type u} [inst : EuclideanDomain R] (x y z : R), y ≠ 0 → y ∣ x → (x / y = z ↔ x = y * z)
-- Mathlib.Analysis.Convex.Between
Wbtw.rotate_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {x y z : P},
  Wbtw R x y z → (Wbtw R z x y ↔ x = y)
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypePerm_pow : ∀ {α : Type u_4} {p : α → Prop} (f : Equiv.Perm α) (n : ℕ) (hf : ∀ (x : α), p (f x) ↔ p x),
  f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.restrict_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb →
    ∀ {s : Set β}, MeasurableSet s → MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.left : Nat.Primrec fun n => (Nat.unpair n).1
-- Mathlib.LinearAlgebra.DFinsupp
Submodule.mem_iSup_finset_iff_exists_sum : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  {s : Finset ι} (p : ι → Submodule R N) (a : N), a ∈ ⨆ i ∈ s, p i ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_eq_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered → ∀ {fallback : α}, l.minKeyD fallback = Std.Internal.List.minKeyD l.toListModel fallback
-- Init.Data.UInt.Lemmas
UInt32.toNat_neg : ∀ (a : UInt32), (-a).toNat = (UInt32.size - a.toNat) % UInt32.size
-- Mathlib.Analysis.Complex.Basic
Complex.conj_mul' : ∀ (z : ℂ), (starRingEnd ℂ) z * z = ↑‖z‖ ^ 2
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_sub_const_Iio : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x - a) '' Set.Iio b = Set.Iio (b - a)
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Irreducible.maximalIdeal_eq_closedBall : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K]
  [IsDiscreteValuationRing ↥(Valued.integer K)] {ϖ : ↥(Valued.integer K)},
  Irreducible ϖ → ↑(Valued.maximalIdeal K) = Metric.closedBall 0 ‖ϖ‖
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.coe_id : ∀ {M : Type u_10} [inst : Add M], ⇑(AddHom.id M) = id
-- Mathlib.Algebra.BigOperators.Intervals
/-- Gauss' summation formula  -/
Finset.sum_range_id_mul_two : ∀ (n : ℕ), (∑ i ∈ Finset.range n, i) * 2 = n * (n - 1)