mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Apply
/-- Try to close the goal using `Subsingleton.elim`. Returns whether or not it succeeds.

We are careful to apply `Subsingleton.elim` in a way that does not assign any metavariables.
This is to prevent the `Subsingleton Prop` instance from being used as justification to specialize
`Sort _` to `Prop`.
 -/
Lean.MVarId.subsingletonElim : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Algebra.RingQuot
RingQuot.lift_unique : ∀ {R : Type uR} [inst : Semiring R] {T : Type uT} [inst_1 : Semiring T] (f : R →+* T) {r : R → R → Prop}
  (w : ∀ ⦃x y : R⦄, r x y → f x = f y) (g : RingQuot r →+* T),
  g.comp (RingQuot.mkRingHom r) = f → g = RingQuot.lift ⟨f, w⟩
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOp_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) (X : Cᵒᵖ), F.leftOp.obj X = Opposite.unop (F.obj (Opposite.unop X))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.instToString : ToString Std.Tactic.BVDecide.BVUnOp
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (s s_1 : X ⟶ Y) (e_s : s = s_1) (hs : W s),
  CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs =
    CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s_1 ⋯
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- The natural transformation
`F.leftDerivedToHomotopyCategory ⟶ G.leftDerivedToHomotopyCategory` induced by
a natural transformation `F ⟶ G` between additive functors.  -/
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasProjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              {F G : CategoryTheory.Functor C D} →
                [inst_5 : F.Additive] →
                  [inst_6 : G.Additive] → (F ⟶ G) → (F.leftDerivedToHomotopyCategory ⟶ G.leftDerivedToHomotopyCategory)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffs_X_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R) (n : σ),
  (MvPolynomial.X n * p).coeffs = p.coeffs
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
RootPairing.linearIndepOn_root_baseOf : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : Field R] [CharZero R] [inst_4 : Module R M] [inst_5 : Module R N]
  (P : RootPairing ι R M N) [P.IsRootSystem] [P.IsCrystallographic] (f : M →+ ℚ),
  (∀ (i : ι), f (P.root i) ≠ 0) → LinearIndepOn R (⇑P.root) (IsAddIndecomposable.baseOf (⇑P.root) f)
-- Mathlib.RingTheory.WittVector.Defs
WittVector.instSub : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → Sub (WittVector p R)
-- Mathlib.FieldTheory.Laurent
RatFunc.laurent_at_zero : ∀ {R : Type u} [inst : CommRing R] (f : RatFunc R) [inst_1 : IsDomain R], (RatFunc.laurent 0) f = f
-- Mathlib.Computability.EpsilonNFA
εNFA.evalFrom_append_singleton : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) (x : List α) (a : α),
  M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a
-- Mathlib.Logic.Relation
Relation.Join.refl : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r], Std.Refl (Relation.Join r)
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
fderivPiPolarCoordSymm.eq_1 : ∀ {ι : Type u_1} (p : ι → ℝ × ℝ),
  fderivPiPolarCoordSymm p = ContinuousLinearMap.pi fun i => fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj i
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `upperHemicontinuousAt_singleton_iff`. -/
ContinuousAt.upperHemicontinuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α},
  ContinuousAt f x → UpperHemicontinuousAt (fun x => {f x}) x
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.coe_reindexAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] [inst_5 : Semiring A] [inst_6 : Algebra R A]
  (e : m ≃ n), ⇑(Matrix.reindexAlgEquiv R A e) = ⇑(Matrix.reindex e e)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.algebraMap_apply : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]), (algebraMap ℤ_[p] ℚ_[p]) x = ↑x
-- Mathlib.Order.ModularLattice
/-- **Alias** of `inf_covBy_of_covBy_sup_of_covBy_sup_left`. -/
CovBy.inf_of_sup_of_sup_left : ∀ {α : Type u_1} [inst : Lattice α] [IsWeakLowerModularLattice α] {a b : α}, a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.tensorModelOfHasCoeffsInv.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] (P : Algebra.Presentation R S ι σ) (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀],
  P.tensorModelOfHasCoeffsInv R₀ =
    (Ideal.Quotient.liftₐ P.ker
          ((Algebra.TensorProduct.map (AlgHom.id R R)
                (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀))))).comp
            ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
          ⋯).comp
      ↑(AlgEquiv.restrictScalars R P.quotientEquiv).symm
-- Lean.Meta.Sym.InstantiateS
/-- Similar to `Lean.Expr.instantiate`.
It assumes the input is maximally shared, and ensures the output is too.
 -/
Lean.Meta.Sym.instantiateS : Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.source_preimage_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.source ⊆ ↑e ⁻¹' e.target
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent_eq_zero_of_notMem : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : DecidableEq M] (φ : MvPolynomial σ R),
  ∀ i ∉ Finset.image (⇑(Finsupp.weight w)) φ.support, (MvPolynomial.weightedHomogeneousComponent w i) φ = 0
-- Mathlib.LinearAlgebra.AffineSpace.Slope
AffineMap.slope_comp : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] {F : Type u_4} {PF : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module k F]
  [inst_6 : AddTorsor F PF] (f : PE →ᵃ[k] PF) (g : k → PE) (a b : k), slope (⇑f ∘ g) a b = f.linear (slope g a b)
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.equivInverse_map : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] (D : Type u'')
  [inst_2 : CategoryTheory.Category.{v'', u''} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D] {X Y : D}
  (f : X ⟶ Y),
  (CategoryTheory.ForgetEnrichment.equivInverse V D).map f =
    CategoryTheory.ForgetEnrichment.homOf V ((CategoryTheory.eHomEquiv V) f)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.toMonoidWithZeroHom_injective : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀],
  Function.Injective Valuation.toMonoidWithZeroHom
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g : M → M'} {s t : Set M} {x : M},
  G.LocalInvariantProp G' P →
    t ∈ nhds x → (ChartedSpace.LiftPropWithinAt P g (s ∩ t) x ↔ ChartedSpace.LiftPropWithinAt P g s x)
-- Mathlib.Analysis.Convex.Basic
Convex.is_linear_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {s : Set E},
  Convex 𝕜 s → ∀ {f : E → F}, IsLinearMap 𝕜 f → Convex 𝕜 (f '' s)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.centroid_eq_centralizer_mulLeftRight : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α],
  (CentroidHom.toEndRingHom α).rangeS =
    Subsemiring.centralizer (Set.range ⇑AddMonoid.End.mulLeft ∪ Set.range ⇑AddMonoid.End.mulRight)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_X_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : σ) (p : MvPolynomial σ R),
  (MvPolynomial.X s * p).support = Finset.map (addLeftEmbedding fun₀ | s => 1) p.support
-- Mathlib.Topology.Order.OrderClosed
Continuous.min : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f g : β → α}
  [inst_3 : TopologicalSpace β], Continuous f → Continuous g → Continuous fun b => min (f b) (g b)
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
HasStrictFDerivAt.eventually_apply_implicitFunctionOfProdDomain : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂]
  [inst_5 : NormedSpace 𝕜 E₂] [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {f'u : E₁ × E₂ →L[𝕜] F}
  (dfu : HasStrictFDerivAt f f'u u) (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  ∀ᶠ (x : E₁) in nhds u.1, f (x, dfu.implicitFunctionOfProdDomain if₂u x) = f u
-- Aesop.Util.EqualUpToIds
/-- Allow metavariables to be unassigned on one side of the comparison and
assigned on the other. So when we compare two expressions and we encounter
a metavariable `?x` in one of them and a subexpression `e` in the other (at
the same position), we consider `?x` equal to `e`.  -/
Aesop.EqualUpToIdsM.Context.allowAssignmentDiff : Aesop.EqualUpToIdsM.Context → Bool
-- Mathlib.ModelTheory.Syntax
/-- Applies a relation to terms as a formula.  -/
FirstOrder.Language.Relations.formula : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.Relations n → (Fin n → L.Term α) → L.Formula α
-- Init.Data.BitVec.Bootstrap
BitVec.getElem_setWidth : ∀ {n : ℕ} (m : ℕ) (x : BitVec n) (i : ℕ) (h : i < m), (BitVec.setWidth m x)[i] = x.getLsbD i
-- Lean.Environment
Lean.EnvExtension.mkInitial : {σ : Type} → Lean.EnvExtension σ → IO σ
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.biprodIsoProd_inv_comp_desc : ∀ {G H K : AddCommGrpCat} (f : G ⟶ K) (g : H ⟶ K),
  CategoryTheory.CategoryStruct.comp (G.biprodIsoProd H).inv (CategoryTheory.Limits.biprod.desc f g) =
    CategoryTheory.CategoryStruct.comp (AddCommGrpCat.ofHom (AddMonoidHom.fst ↑G ↑H)) f +
      CategoryTheory.CategoryStruct.comp (AddCommGrpCat.ofHom (AddMonoidHom.snd ↑G ↑H)) g
-- Std.Data.TreeSet.Basic
Std.TreeSet.instForInOfMonad : {α : Type u} → {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForIn m (Std.TreeSet α cmp) α
-- Mathlib.Geometry.Manifold.Immersion
_private.Mathlib.Geometry.Manifold.Immersion.0.Manifold.IsImmersion.eq_1 : ∀ {𝕜 : 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),
  Manifold.IsImmersion I J n f = ∃ F x x_1, Manifold.IsImmersionOfComplement F I J n f
-- Mathlib.Topology.Constructions
Homeomorph.ofEqSubtypes_toEquiv : ∀ {X : Type u} [inst : TopologicalSpace X] {p q : X → Prop} (hpq : p = q),
  (Homeomorph.ofEqSubtypes hpq).toEquiv = Equiv.subtypeEquivProp hpq
-- Lean.Elab.Term.TermElabM
/-- Heed `elab_as_elim` attribute.  -/
Lean.Elab.Term.Context.heedElabAsElim : Lean.Elab.Term.Context → Bool
-- Init.Data.Option.Lemmas
Option.any_eq_false : ∀ {α : Type u_1} (p : α → Bool) (x : Option α), Option.any p x = false ↔ ∀ (y : α), x = some y → p y = false
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.addLeftReflectLE : ∀ {α : Type u} [inst : LE α] [inst_1 : Add α] [AddLeftReflectLE α], AddLeftReflectLE αᵒᵈ
-- 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 => β} [Std.TransOrd α] (h : t.WF)
  {a k : α} {v : β},
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl a =
    if compare k a = Ordering.eq then some v else Std.DTreeMap.Internal.Impl.Const.get? t a
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Evaluate a recursive call at a given `MutualMeasure`  -/
Lean.Elab.WF.GuessLex.inspectCall : Lean.Elab.WF.GuessLex.RecCallCache → Lean.Elab.WF.GuessLex.MutualMeasure → Lean.MetaM Lean.Elab.WF.GuessLex.GuessLexRel
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.apply_continuousLinearMap : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} {H : Type u_9}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup H] {𝕜 : Type u_10} {𝕜' : Type u_11}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜' E]
  [inst_5 : NormedSpace 𝕜 H] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] {φ : α → H →SL[σ] E},
  MeasureTheory.Integrable φ μ → ∀ (v : H), MeasureTheory.Integrable (fun a => (φ a) v) μ
-- Mathlib.Tactic.Linter.Whitespace
/-- Given an array `a` of `SyntaxNodeKind`s, we accumulate the ranges of the syntax nodes of the
input syntax whose kind is in `a`.

The linter uses this information to avoid emitting a warning for nodes with kind contained in
`unlintedNodes`.
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.getUnlintedRanges : Array Lean.SyntaxNodeKind → Std.HashSet Lean.Syntax.Range → Lean.Syntax → Std.HashSet Lean.Syntax.Range
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin : ∀ {𝕜 : 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 : WithTop ℕ∞} {m : ℕ},
  ContDiffWithinAt 𝕜 n f s x →
    ↑m < n → UniqueDiffOn 𝕜 (insert x s) → DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x
-- Mathlib.Algebra.Group.Basic
sub_eq_sub_add_sub : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), a - b = c - b + (a - c)
-- Mathlib.Analysis.Polynomial.CauchyBound
Polynomial.cauchyBound_one : ∀ {K : Type u_1} [inst : NormedDivisionRing K], Polynomial.cauchyBound 1 = 1
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- Variation of `TensorProduct.exists_finite_submodule_right_of_setFinite` where `M` and `N` are
already submodules.  -/
TensorProduct.exists_finite_submodule_right_of_setFinite' : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N}
  (s : Set (TensorProduct R ↥M₁ ↥N₁)),
  s.Finite → ∃ N', ∃ (hN : N' ≤ N₁), Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.lTensor (↥M₁) (Submodule.inclusion hN)).range
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vaddCommClass_set'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α γ] [inst_1 : VAdd β γ] [VAddCommClass α β γ],
  VAddCommClass (Set α) β (Set γ)
-- Init.Grind.Attr
/-- The `cases eager` modifier marks inductively-defined predicates as suitable for case splitting,
and instructs `grind` to perform it eagerly while preprocessing hypotheses.
 -/
Lean.Parser.Attr.grindCasesEager : Lean.ParserDescr
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_congr : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {X' : α → β} {Y' : α → Ω},
  Y =ᵐ[μ] Y' → X =ᵐ[μ] X' → ProbabilityTheory.condDistrib Y X μ = ProbabilityTheory.condDistrib Y' X' μ
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.finiteHeight_of_isNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (I : Ideal R), I.FiniteHeight
-- Lean.Elab.Calc
Lean.Elab.Term.throwCalcFailure : {α : Type} → Array Lean.Elab.Term.CalcStepView → Lean.Expr → Lean.Expr → Lean.MetaM α
-- Mathlib.Algebra.Star.Basic
star_star : ∀ {R : Type u} [inst : InvolutiveStar R] (r : R), star (star r) = r
-- Mathlib.Data.Nat.MaxPowDiv
/-- **Alias** of `padicValNat_base_pow_mul`. -/
Nat.maxPowDiv.base_pow_mul : ∀ {p n : ℕ}, 1 < p → n ≠ 0 → ∀ (k : ℕ), padicValNat p (p ^ k * n) = padicValNat p n + k
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size_tail : ∀ {α : Type u_1} (le : α → α → Bool) {s : Batteries.PairingHeapImp.Heap α},
  s.NoSibling → (Batteries.PairingHeapImp.Heap.tail le s).size = s.size - 1
-- Mathlib.Data.Seq.Defs
/-- Convert a sequence which is known to terminate into a list  -/
Stream'.Seq.toList : {α : Type u} → (s : Stream'.Seq α) → s.Terminates → List α
-- Init.Data.List.Count
List.countP.go.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : ℕ) (a_1 : α) (l : List α),
  List.countP.go p (a_1 :: l) a = bif p a_1 then List.countP.go p l (a + 1) else List.countP.go p l a
-- Mathlib.Geometry.Diffeology.Basic
/-- A function between diffeological spaces is smooth iff composition with it preserves
smoothness of plots.  -/
Diffeology.DSmooth : {X : Type u_1} → {Y : Type u_2} → [DiffeologicalSpace X] → [DiffeologicalSpace Y] → (X → Y) → Prop
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.charZero : ∀ {α : Type u} [inst : AddMonoidWithOne α] [CharZero α], CharZero (WithTop α)
-- Mathlib.Data.Int.Bitwise
Int.bit_decomp : ∀ (n : ℤ), Int.bit n.bodd n.div2 = n
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.inv_mem_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : Rˣ} {a : Aˣ},
  ↑r ∈ spectrum R ↑a ↔ ↑r⁻¹ ∈ spectrum R ↑a⁻¹
-- Init.Data.BitVec.Decidable
BitVec.instDecidableForallBitVecZero : (P : BitVec 0 → Prop) → [Decidable (P 0#0)] → Decidable (∀ (v : BitVec 0), P v)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_zpow : ∀ {x : ℝ} (m : ℤ), Irrational (x ^ m) → Irrational x
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.levelParams : Lean.Elab.Command.AddAndFinalizeContext✝ → List Lean.Name
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
/-- A version of Newton's identities which may be more useful in the case that we know the values of
the elementary symmetric polynomials and would like to calculate the values of the power sums.  -/
MvPolynomial.psum_eq_mul_esymm_sub_sum : ∀ (σ : Type u_1) [inst : Fintype σ] (R : Type u_2) [inst_1 : CommRing R] (k : ℕ),
  0 < k →
    MvPolynomial.psum σ R k =
      (-1) ^ (k + 1) * ↑k * MvPolynomial.esymm σ R k -
        ∑ a ∈ Finset.HasAntidiagonal.antidiagonal k with a.1 ∈ Set.Ioo 0 k,
          (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sUnion_pair : ∀ (x y : ZFSet.{u}), {x, y}.sUnion = x ∪ y
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_map : ∀ {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂}
  [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.enrichedFunctorTypeEquivFunctor F).map f = (CategoryTheory.ConcreteCategory.hom (F.map X Y)) f
-- Mathlib.Algebra.Tropical.Basic
/-- Reinterpret `x : Tropical R` as an element of `R`.
See `Tropical.tropEquiv` for the equivalence.  -/
Tropical.untrop : {R : Type u} → Tropical R → R
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instMonoid.eq_1 : ∀ {α : Type u_1} [inst : Monoid α],
  MulOpposite.instMonoid =
    { toSemigroup := MulOpposite.instSemigroup, toOne := MulOpposite.instMulOneClass.toOne, one_mul := ⋯, mul_one := ⋯,
      npow := fun n a => MulOpposite.op (MulOpposite.unop a ^ n), npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0),
  CochainComplex.HomComplex.Cochain.ofHom z.homOf = ↑z
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_zmod_eq_zero_iff_dvd : ∀ (a : ℤ) (b : ℕ), ↑a = 0 ↔ ↑b ∣ a
-- Mathlib.Topology.NhdsWithin
mem_nhdsWithin_iff_eventually : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {x : α},
  t ∈ nhdsWithin x s ↔ ∀ᶠ (y : α) in nhds x, y ∈ s → y ∈ t
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
/-- If `l` is a filter on `α`, then a function `f: α → β` is `BoundedAtFilter l`
if `f =O[l] 1`.  -/
Filter.BoundedAtFilter : {α : Type u_2} → {β : Type u_3} → [Norm β] → Filter α → (α → β) → Prop
-- Mathlib.Topology.Constructions
isQuotientMap_quot_mk : ∀ {X : Type u} [inst : TopologicalSpace X] {r : X → X → Prop}, Topology.IsQuotientMap (Quot.mk r)
-- Init.System.ST
EST.throw : {ε σ α : Type} → ε → EST ε σ α
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_retract : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  [self : P.IsStableUnderRetracts] {X Y : C} (x : CategoryTheory.Retract X Y), P Y → P X
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_lt : ∀ {m n : ℕ}, m.sqrt < n ↔ m < n * n
-- Init.System.IO
IO.FS.Stream.mk.inj : ∀ {flush : IO Unit} {read : USize → IO ByteArray} {write : ByteArray → IO Unit} {getLine : IO String}
  {putStr : String → IO Unit} {isTty : BaseIO Bool} {flush_1 : IO Unit} {read_1 : USize → IO ByteArray}
  {write_1 : ByteArray → IO Unit} {getLine_1 : IO String} {putStr_1 : String → IO Unit} {isTty_1 : BaseIO Bool},
  { flush := flush, read := read, write := write, getLine := getLine, putStr := putStr, isTty := isTty } =
      { flush := flush_1, read := read_1, write := write_1, getLine := getLine_1, putStr := putStr_1,
        isTty := isTty_1 } →
    flush = flush_1 ∧ read = read_1 ∧ write = write_1 ∧ getLine = getLine_1 ∧ putStr = putStr_1 ∧ isTty = isTty_1
-- Mathlib.Order.Heyting.Hom
HeytingHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] (f : HeytingHom α β) (f' : α → β)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.LinearAlgebra.Reflection
Module.preReflection_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M)
  (f : Module.Dual R M) (y : M), (Module.preReflection x f) y = y - f y • x
-- Mathlib.Topology.Constructions.SumProd
/-- Continuous functions on products are continuous in their second argument  -/
Continuous.curry_right : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X × Y → Z}, Continuous f → ∀ {x : X}, Continuous fun y => f (x, y)
-- Mathlib.Order.Partition.Finpartition
/-- The elements of the finite partition of `a`  -/
Finpartition.parts : {α : Type u_1} → [inst : Lattice α] → [inst_1 : OrderBot α] → {a : α} → Finpartition a → Finset α