mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.isOpenMap_re : IsOpenMap UpperHalfPlane.re
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom''_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
        (CategoryTheory.CategoryStruct.id Y))
      h
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toPoly.go.eq_1 : ∀ (coeff k : ℕ),
  Nat.Internal.Linear.Expr.toPoly.go coeff (Nat.Internal.Linear.Expr.num k) =
    bif k == 0 then id else fun x => (coeff * k, Nat.Internal.Linear.fixedVar) :: x
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated : ∀ (X : AlgebraicGeometry.Scheme),
  QuasiSeparatedSpace ↥X ↔ AlgebraicGeometry.QuasiSeparated (CategoryTheory.Limits.terminal.from X)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_bot : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (x : M), x ∈ ⊥ ↔ x = 0
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubMulAction.fg_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : SMul R M] {p : SubMulAction R M}, p.FG ↔ ∃ s, p = SubMulAction.closure R ↑s
-- Mathlib.GroupTheory.Coset.Basic
leftAddCoset_eq_iff : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {x y : α}, x +ᵥ ↑s = y +ᵥ ↑s ↔ -x + y ∈ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.c_relation_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3], W.c₄ ^ 3 = W.c₆ ^ 2
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_C_add : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (t : R),
  (Polynomial.C t + p).reverse = Polynomial.C t * Polynomial.X ^ p.natDegree + p.reverse
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symmEquiv_symm_apply_symm_apply : ∀ (P : Type u_9) (Q : Type u_10) [inst : Mul P] [inst_1 : Mul Q] (h : Q ≃* P) (a : Q),
  ((MulEquiv.symmEquiv P Q).symm h).symm a = h a
-- Std.Data.HashMap.Lemmas
Std.HashMap.toList_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {c : ℕ}, (Std.HashMap.emptyWithCapacity c).toList = []
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the reverse direction of `Units.inv_mul_le_one`. -/
Units.inv_mul_le_one_of_le : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a : M}, a ≤ ↑u → ↑u⁻¹ * a ≤ 1
-- Std.Data.DTreeMap.Raw.Lemmas
/-- Simpler variant of `get!_filter` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Raw.Const.get!_filter' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited β] {f : α → β → Bool} {k : α},
  t.WF →
    Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.filter f t) k =
      (Option.filter (f k) (Std.DTreeMap.Raw.Const.get? t k)).get!
-- Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
EuclideanGeometry.preimage_inversion_sphere_dist_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c y : P} {R : ℝ},
  R ≠ 0 →
    y ≠ c →
      EuclideanGeometry.inversion c R ⁻¹' Metric.sphere y (dist y c) =
        insert c ↑(AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y))
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.compl : ∀ {α : Type u} {β : Type v} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {l : α → β} {u : β → α},
  GaloisConnection l u → GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl)
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithTop.untop.match_1.splitter : {α : Type u_1} →
  (motive : (x : WithTop α) → x ≠ ⊤ → Sort u_2) →
    (x : WithTop α) → (x_1 : x ≠ ⊤) → ((x : α) → (x_2 : ↑x ≠ ⊤) → motive (some x) x_2) → motive x x_1
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` reflects finite limits, then `F : C ⥤ Dᵒᵖ` reflects finite
colimits.  -/
CategoryTheory.Limits.reflectsFiniteColimits_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteLimits F.leftOp],
  CategoryTheory.Limits.ReflectsFiniteColimits F
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.center_eq_top : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_3) [inst_1 : NonUnitalCommSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], NonUnitalSubalgebra.center R A = ⊤
-- Mathlib.Combinatorics.Matroid.Basic
/-- The ground set is finite  -/
Matroid.Finite.ground_finite : ∀ {α : Type u_1} {M : Matroid α} [self : M.Finite], M.E.Finite
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.type₁_dim : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s : h.ι), (h.type₁ s).dim = h.dim s + 1
-- Mathlib.Data.Part
Part.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (o : Part α),
  Part.map g (Part.map f o) = Part.map (g ∘ f) o
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- Map a fractional ideal `I` to a submodule by forgetting that `∃ a, a I ⊆ R`.

This implements the coercion `FractionalIdeal S P → Submodule R P`.
 -/
FractionalIdeal.coeToSubmodule : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → FractionalIdeal S P → Submodule R P
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k fallback : α}, (t.insert k).maxD fallback = t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpParams.mk.inj : ∀ {toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams}
  {toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams} {context? : Option Lean.Lsp.SignatureHelpContext}
  {toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams}
  {toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams} {context?_1 : Option Lean.Lsp.SignatureHelpContext},
  { toTextDocumentPositionParams := toTextDocumentPositionParams, toWorkDoneProgressParams := toWorkDoneProgressParams,
        context? := context? } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1,
        toWorkDoneProgressParams := toWorkDoneProgressParams_1, context? := context?_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1 ∧
      toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧ context? = context?_1
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.updateLet!Impl : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Expr
-- Mathlib.Topology.Neighborhoods
/-- The intersection of an open dense set with a dense set is a dense set.  -/
Dense.inter_of_isOpen_left : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, Dense s → Dense t → IsOpen s → Dense (s ∩ t)
-- Mathlib.MeasureTheory.Measure.Prod
/-- If `s ×ˢ t` is a null measurable set and `μ s ≠ 0`, then `t` is a null measurable set.  -/
MeasureTheory.NullMeasurableSet.right_of_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set α} {t : Set β},
  MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) → μ s ≠ 0 → MeasureTheory.NullMeasurableSet t ν
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (a b n : ℤ) (h : a + b = n) (a' n' : ℤ) (ha' : a' + b = n') (hn' : n' = n + x) {Z : C}
  (h_1 : (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).total (ComplexShape.up ℤ)).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a' b n' ha')
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv
        (CategoryTheory.CategoryStruct.comp ((K.totalShift₁Iso x).inv.f n) h_1)) =
    CategoryTheory.CategoryStruct.comp (K.shiftFunctor₁XXIso a x a' ⋯ b).inv
      (CategoryTheory.CategoryStruct.comp
        (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h) h_1)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_iInf : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] (S : ι → Subsemigroup M), (iInf S).op = ⨅ i, (S i).op
-- Mathlib.Order.JordanHolder
JordanHolderLattice.second_iso : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {x y : X},
  JordanHolderLattice.IsMaximal x (x ⊔ y) → JordanHolderLattice.Iso (x, x ⊔ y) (x ⊓ y, y)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))),
  ⇑X.isoSpec.inv ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isRat_ratCast : ∀ {R : Type u_1} [inst : DivisionRing R] [CharZero R] {q : ℚ} {n : ℤ} {d : ℕ},
  Mathlib.Meta.NormNum.IsRat q n d → Mathlib.Meta.NormNum.IsRat (↑q) n d
-- Plausible.Testable
Plausible.PrintableProp.mk : {p : Prop} → String → Plausible.PrintableProp p
-- Init.Data.Iterators.Basic
Std.IterM.step_eq : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1}
  {IsPlausibleStep : Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop}
  {step : (it : Std.IterM m β) → m (Std.Shrink (Std.PlausibleIterStep (IsPlausibleStep it)))} {it : Std.IterM m β},
  it.step = step it
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts a `Minute.Offset` from a `PlainDateTime`, adjusting the hour and date if the minutes underflow.
 -/
Std.Time.PlainDateTime.subMinutes : Std.Time.PlainDateTime → Std.Time.Minute.Offset → Std.Time.PlainDateTime
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `CommSemigroup` across an `Equiv`  -/
Equiv.commSemigroup : {α : Type u_2} → {β : Type u_3} → α ≃ β → [CommSemigroup β] → CommSemigroup α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.polynomialZ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R),
  W'.polynomialZ = (MvPolynomial.pderiv 2) W'.polynomial
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_bot_right : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M), Submodule.map₂ f p ⊥ = ⊥
-- Mathlib.Topology.Path
Path.continuous_trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X}, Continuous fun ρ => ρ.1.trans ρ.2
-- Init.Data.Zero
/-- The fundamental power operation in a monoid.
`npowRec n a = a*a*...*a` n times.
This function should not be used directly; it is often used to implement a `Pow M Nat` instance,
but end users should use the `a ^ n` notation instead.
 -/
npowRec : {M : Type u_1} → [One M] → [Mul M] → ℕ → M → M
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- An equivalence between `σ` and `τ` induces an equivalence between the subtypes of `Sym σ n` and
`Sym τ n` corresponding to a given partition.  -/
Nat.Partition.ofSymShapeEquiv : {n : ℕ} →
  {σ : Type u_1} →
    {τ : Type u_2} →
      [inst : DecidableEq σ] →
        [inst_1 : DecidableEq τ] →
          (μ : n.Partition) → σ ≃ τ → { x // Nat.Partition.ofSym x = μ } ≃ { x // Nat.Partition.ofSym x = μ }
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nhdsWithin_Iio_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b : α} [ClosedIciTopology α], (nhdsWithin a (Set.Iio b)).IsMeasurablyGenerated
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `r / s : K` is the valuation of `r` divided by the valuation of `s`.  -/
IsDedekindDomain.HeightOneSpectrum.valuation_of_mk' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R}
  {s : ↥(nonZeroDivisors R)},
  (IsDedekindDomain.HeightOneSpectrum.valuation K v) (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation ↑s
-- Mathlib.CategoryTheory.Limits.Cones
/-- `mapCone` commutes with `whisker`  -/
CategoryTheory.Functor.mapConeWhisker : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                (H : CategoryTheory.Functor C D) →
                  {F : CategoryTheory.Functor J C} →
                    {E : CategoryTheory.Functor K J} →
                      {c : CategoryTheory.Limits.Cone F} →
                        H.mapCone (CategoryTheory.Limits.Cone.whisker E c) ≅
                          CategoryTheory.Limits.Cone.whisker E (H.mapCone c)
-- Lean.CoreM
/-- Returns the current log and then resets its messages while adjusting `MessageLog.hadErrors`. Used
for incremental reporting during elaboration of a single command.
 -/
Lean.Core.getAndEmptyMessageLog : Lean.CoreM Lean.MessageLog
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- Action of the stabilizer of a point on the complement.  -/
SubAddAction.ofStabilizer : (G : Type u_1) →
  [inst : AddGroup G] →
    {α : Type u_2} → [inst_1 : AddAction G α] → (a : α) → SubAddAction (↥(AddAction.stabilizer G a)) α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insert! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α} {v : β}
  {h₁ : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insert! k v t) = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.insert! k v t) a h₁ =
    if h₂ : compare k a = Ordering.eq then v else Std.DTreeMap.Internal.Impl.Const.get t a ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.some.injEq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x y : R) (h : W'.Nonsingular x y) (x_1 y_1 : R)
  (h_1 : W'.Nonsingular x_1 y_1),
  (WeierstrassCurve.Affine.Point.some x y h = WeierstrassCurve.Affine.Point.some x_1 y_1 h_1) = (x = x_1 ∧ y = y_1)
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.continuous_choose : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ), Continuous fun x => Ring.choose x k
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.instNontrivialOfNonempty : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [Nonempty Γ] [Nontrivial R],
  Nontrivial (HahnSeries Γ R)
-- Mathlib.Analysis.Asymptotics.Defs
/-- `f = O(g)` if and only if `IsBigOWith c f g` for all sufficiently large `c`.  -/
Asymptotics.isBigO_iff_eventually_isBigOWith : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, f =O[l] g' ↔ ∀ᶠ (c : ℝ) in Filter.atTop, Asymptotics.IsBigOWith c l f g'
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
/-- The derivative of `log ∘ f` is the logarithmic derivative provided `f` is differentiable and
we are on the slitPlane.  -/
Complex.deriv_log_comp_eq_logDeriv : ∀ {f : ℂ → ℂ} {x : ℂ}, DifferentiableAt ℂ f x → f x ∈ Complex.slitPlane → deriv (Complex.log ∘ f) x = logDeriv f x
-- Mathlib.Logic.Equiv.Sum
Equiv.sumCompl_symm_apply_of_pos : ∀ {α : Type u_9} {p : α → Prop} [inst : DecidablePred p] {a : α} (h : p a), (Equiv.sumCompl p).symm a = Sum.inl ⟨a, h⟩
-- Init.Data.Fin.Basic
/-- If you actually have an element of `Fin n`, then the `n` is always positive  -/
Fin.pos : ∀ {n : ℕ} (i : Fin n), 0 < n
-- Std.Http.Transport
/-- Tries to receive data without blocking, joining all immediately available chunks.
Returns `none` if no data is available.
 -/
Std.Http.Internal.Mock.Client.tryRecv? : Std.Http.Internal.Mock.Client → optParam UInt64 0 → BaseIO (Option ByteArray)
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- See also `Module.instFiniteDimensionalOfIsReflexive` for the converse over a field.  -/
Module.IsReflexive.of_finite_of_free : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M] [Module.Free R M], Module.IsReflexive R M
-- Lean.Elab.App
/-- Set the `motive` field in the state.  -/
Lean.Elab.Term.ElabElim.setMotive : Lean.Expr → Lean.Elab.Term.ElabElim.M Unit
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.writtenInCharts : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x),
  Set.EqOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (⇑h.equiv ∘ fun x_1 => (x_1, 0))
    (h.domChart.extend I).target
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables for monotone functions.
If `f` is continuous on `[a, b]` and has a nonnegative derivative `f'` in `(a, b)`,
then we can substitute `u = f x` to get `∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.  -/
intervalIntegral.integral_comp_mul_deriv_of_deriv_nonpos : ∀ {a b : ℝ} {f f' g : ℝ → ℝ},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), f' x ≤ 0) → ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
-- Init.Data.Nat.Basic
Nat.sub_one_eq_self : ∀ {n : ℕ}, n - 1 = n ↔ n = 0
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- The natural isomorphism exhibiting compatibility between pushforward and sheafification.  -/
CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (G : CategoryTheory.Functor C D) →
          (A : Type w) →
            [inst_2 : CategoryTheory.Category.{w', w} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [G.IsCocontinuous J K] →
                    [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] →
                      [inst_5 : G.IsContinuous J K] →
                        [inst_6 : CategoryTheory.HasWeakSheafify J A] →
                          [inst_7 : CategoryTheory.HasWeakSheafify K A] →
                            ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp
                                (CategoryTheory.presheafToSheaf J A) ≅
                              (CategoryTheory.presheafToSheaf K A).comp (G.sheafPushforwardContinuous A J K)
-- Mathlib.Algebra.Group.Equiv.Opposite
MulOpposite.opAddEquiv_toEquiv : ∀ {α : Type u_2} [inst : Add α], ↑MulOpposite.opAddEquiv = MulOpposite.opEquiv
-- Mathlib.Order.Northcott
northcott_iff : ∀ {α : Type u_1} {β : Type u_2} (h : α → β) [inst : LE β], Northcott h ↔ ∀ (b : β), {a | h a ≤ b}.Finite
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAtFilter.isBigO_sub : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {L : Filter F},
  HasGradientAtFilter f f' x L → (fun x' => f x' - f x) =O[L] fun x' => x' - x
-- Init.Data.String.Pattern.Char
String.Slice.Pattern.Char.instBackwardPatternChar : {c : Char} → String.Slice.Pattern.BackwardPattern c
-- Mathlib.Topology.EMetricSpace.Defs
Metric.closedEBall_zero : ∀ {γ : Type w} [inst : EMetricSpace γ] (x : γ), Metric.closedEBall x 0 = {x}
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mod_zero : ∀ (a : Ordinal.{u_4}), a % 0 = a
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getKey : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → (a : α) → (l : List ((a : α) × β a)) → Std.Internal.List.containsKey a l = true → α
-- Mathlib.Topology.Covering.Quotient
/-- If a group `G` acts on a space `E` and `U` is an open subset disjoint from all
other `G`-translates of itself, and `p` is a quotient map by this action, then `p` admits a
`Bundle.Trivialization` over the base set `p(U)`.  -/
Topology.IsQuotientMap.trivializationOfVAddDisjoint : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {G : Type u_3} →
            [inst_2 : AddGroup G] →
              [inst_3 : AddAction G E] →
                Topology.IsQuotientMap f →
                  [ContinuousConstVAdd G E] →
                    (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) →
                      [inst_5 : TopologicalSpace G] →
                        [DiscreteTopology G] →
                          (U : Set E) →
                            IsOpen U →
                              (∀ (g : G), ((fun x => g +ᵥ x) '' U ∩ U).Nonempty → g = 0) → Bundle.Trivialization G f
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Icc_left : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₁ ≤ a₂ → Set.Icc a₂ b ⊆ Set.Icc a₁ b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A binary cofan is just a cocone on a diagram indexing a coproduct.  -/
CategoryTheory.Limits.BinaryCofan : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Type (max (max 0 u) v)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.module_finite : ∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K]
  {E : Type u_2} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace K E] [FiniteDimensional K E] [ProperSpace E]
  (L : Submodule ℤ E) [inst_9 : DiscreteTopology ↥L] [IsZLattice K L], Module.Finite ℤ ↥L
-- Mathlib.Order.Nucleus
Nucleus.map_himp_apply : ∀ {X : Type u_1} [inst : Order.Frame X] (n : Nucleus X) (x y : X), n (x ⇨ n y) = x ⇨ n y
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.mem_darts_iff_infix_support : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} (h : G.Adj u' v'),
  { fst := u', snd := v', adj := h } ∈ p.darts ↔ [u', v'] <:+: p.support
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Pull-out property of the conditional expectation.  -/
MeasureTheory.condExp_mul_of_stronglyMeasurable_right : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ℝ},
  MeasureTheory.StronglyMeasurable g →
    MeasureTheory.Integrable (f * g) μ → MeasureTheory.Integrable f μ → μ[f * g | m] =ᵐ[μ] μ[f | m] * g