mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Complex.hasStrictDerivAt_const_cpow : ∀ {x y : ℂ}, x ≠ 0 ∨ y ≠ 0 → HasStrictDerivAt (fun y => x ^ y) (x ^ y * Complex.log x) y
-- Batteries.Recycling.RBTree.Basic
/-- A red node is balanced with black-height `n`
if its children are both black with with black-height `n`.  -/
RBTree.RBNode.Balanced.red : ∀ {α : Type u_1} {x : RBTree.RBNode α} {n : ℕ} {y : RBTree.RBNode α} {v : α},
  x.Balanced RBTree.RBColor.black n →
    y.Balanced RBTree.RBColor.black n → (RBTree.RBNode.node RBTree.RBColor.red x v y).Balanced RBTree.RBColor.red n
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).unmop =
    (CategoryTheory.MonoidalCategoryStruct.associator Z.unmop Y.unmop X.unmop).symm
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.homMk_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} (f : F X ⟶ F Y), (CategoryTheory.InducedCategory.homMk f).hom = f
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.symm_symm : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (e : A ≃⋆+* B), e.symm.symm = e
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α}, (m.insertManyIfNewUnit l).size ≤ m.size + l.length
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, s.Nonempty → (-s).Nonempty
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- For `m ≤ n`, `⦋m⦌ₙ` is the `m`-dimensional simplex in `Truncated n`. The
proof `p : m ≤ n` can also be provided using the syntax `⦋m, p⦌ₙ`.  -/
SimplexCategory.Truncated.mkNotation : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- A homological complex `K` has homology in degree `i` if the associated
short complex `K.sc i` has.  -/
HomologicalComplex.HasHomology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → {c : ComplexShape ι} → HomologicalComplex C c → ι → Prop
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The pullback functor for categories of sheaves of modules over schemes
is left adjoint to the pushforward functor.  -/
AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → AlgebraicGeometry.Scheme.Modules.pullback f ⊣ AlgebraicGeometry.Scheme.Modules.pushforward f
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The action by a subalgebra is the action by the underlying algebra.  -/
Subalgebra.instMulActionWithZeroSubtypeMem : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {α : Type u_1} → [inst_3 : Zero α] → [MulActionWithZero A α] → (S : Subalgebra R A) → MulActionWithZero (↥S) α
-- Mathlib.Tactic.FunProp.Attr
_private.Mathlib.Tactic.FunProp.Attr.0.Mathlib.Meta.FunProp.funPropHelpString : String
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ_zero : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.Ψ 0 = 0
-- Mathlib.Algebra.Order.Floor.Extended
/-- `⌈r⌉ₑ` is the least extended natural `n` such that `r ≤ n`  -/
ENat.ceil : ENNReal → ℕ∞
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.snd_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (v : V × W), (Representation.IntertwiningMap.snd A ρ σ) v = v.2
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {h' : k ∈ Std.ExtDTreeMap.filter f t},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.filter f t) k h' = Std.ExtDTreeMap.Const.get t k ⋯
-- Mathlib.Algebra.Group.Hom.Defs
/-- In principle this could be an instance, but in practice it causes performance issues.  -/
Subsingleton.of_oneHomClass : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N] [Subsingleton M]
  [OneHomClass F M N], Subsingleton F
-- Mathlib.Topology.EMetricSpace.Defs
/-- Auxiliary function to replace the uniformity on an emetric space with
a uniformity which is equal to the original one, but maybe not defeq.
This is useful if one wants to construct an emetric space with a
specified uniformity. See Note [forgetful inheritance] explaining why having definitionally
the right uniformity is often important.
See note [reducible non-instances].
 -/
EMetricSpace.replaceUniformity : {γ : Type u_2} → [U : UniformSpace γ] → (m : EMetricSpace γ) → uniformity γ = uniformity γ → EMetricSpace γ
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a negative constant, `fun x ↦ f x / r` tends to infinity along a filter `l`
if and only if `f` tends to negative infinity along `l`.  -/
Filter.tendsto_div_const_atTop_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → (Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot)
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.ind : ∀ (K : Type u_1) {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {motive : ConjRootClass K L → Prop}, (∀ (x : L), motive (ConjRootClass.mk K x)) → ∀ (c : ConjRootClass K L), motive c
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteLimits_embedding : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor D Cᵒᵖ) [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C],
  CategoryTheory.Limits.PreservesFiniteLimits
    (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding F)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (h : Diffeomorph I I' M M' n), n ≠ 0 → MDiff ⇑h
-- Mathlib.Order.BoundedOrder.Basic
Ne.bot_lt : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≠ ⊥ → ⊥ < a
-- Init.Data.Bool
Bool.coe_false_iff_true : ∀ {a b : Bool}, (a = false ↔ b = true) ↔ (!a) = b
-- Mathlib.Probability.Kernel.Posterior
/-- The main property of the posterior.  -/
ProbabilityTheory.compProd_posterior_eq_map_swap : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω],
  (μ.bind ⇑κ).compProd (ProbabilityTheory.posterior κ μ) = MeasureTheory.Measure.map Prod.swap (μ.compProd κ)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_X_pow : ∀ {R : Type u} [inst : Semiring R] {x : R} (n : ℕ), Polynomial.eval x (Polynomial.X ^ n) = x ^ n
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.dom_le_dom : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N}, f ≤ g → f.dom ≤ g.dom
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.IntegrableOn.smul_continuousOn : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {K : Set X} {𝕜 : Type u_9} [inst_4 : NormedRing 𝕜]
  [inst_5 : Module 𝕜 E] [IsBoundedSMul 𝕜 E] [T2Space X] [SecondCountableTopologyEither X E] {f : X → 𝕜},
  MeasureTheory.IntegrableOn f K μ →
    ∀ {g : X → E}, ContinuousOn g K → IsCompact K → MeasureTheory.IntegrableOn (fun x => f x • g x) K μ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.cartesianMonoidalCategory : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [CategoryTheory.CartesianMonoidalCategory C] →
          CategoryTheory.CartesianMonoidalCategory (CategoryTheory.Functor J C)
-- Init.Data.String.Lemmas.FindPos
String.Slice.pos_eq_posGE : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : String.Pos.Raw.IsValidForSlice s p}, s.pos p h = s.posGE p ⋯
-- Mathlib.Data.Nat.Squarefree
Nat.prod_primeFactors_dvd_iff : ∀ {n k : ℕ}, k ≠ 0 → (∏ p ∈ n.primeFactors, p ∣ k ↔ n.primeFactors ⊆ k.primeFactors)
-- Mathlib.Algebra.Notation.Support
Function.range_eq_image_or_of_support_subset : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M} {k : Set ι},
  Function.support f ⊆ k → Set.range f = f '' k ∨ Set.range f = insert 0 (f '' k)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainAddEquiv.eq_1 : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Add M] [inst_2 : Add N] (e : M ≃ N),
  AddMonoidAlgebra.mapDomainAddEquiv R e =
    { toFun := fun x => AddMonoidAlgebra.mapDomain (⇑e) x, invFun := fun x => AddMonoidAlgebra.mapDomain (⇑e.symm) x,
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Lean.Expr
Lean.mkSortEx : Lean.Level → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.IsLimit.hasWeightedLimit : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.WeightedCone W F}
  (hc : c.IsLimit), CategoryTheory.Limits.HasWeightedLimit W F
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulCommClass_closedBall_closedBall_ball : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [SMulCommClass 𝕜 𝕜' E], SMulCommClass ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Given bifunctors `F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂`, `G : C₁₂ ⥤ C₃ ⥤ C₄`, graded objects
`X₁ : GradedObject I₁ C₁`, `X₂ : GradedObject I₂ C₂`, `X₃ : GradedObject I₃ C₃` and
`ρ₁₂ : BifunctorComp₁₂IndexData r`, this asserts that for all `i₁₂ : ρ₁₂.I₁₂` and `i₃ : I₃`,
the functor `G(-, X₃ i₃)` commutes with the coproducts of the `F₁₂(X₁ i₁, X₂ i₂)`
such that `ρ₁₂.p ⟨i₁, i₂⟩ = i₁₂`.  -/
CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₁₂ : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] →
                    CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂) →
                      CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄) →
                        {I₁ : Type u_7} →
                          {I₂ : Type u_8} →
                            {I₃ : Type u_9} →
                              {J : Type u_10} →
                                {r : I₁ × I₂ × I₃ → J} →
                                  CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r →
                                    CategoryTheory.GradedObject I₁ C₁ →
                                      CategoryTheory.GradedObject I₂ C₂ → CategoryTheory.GradedObject I₃ C₃ → Prop
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.injOn_edgeSet : ∀ {V : Type u_1} {G : SimpleGraph V},
  Set.InjOn SimpleGraph.Subgraph.edgeSet (Set.ofPred SimpleGraph.Subgraph.IsMatching)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_isIso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C) (x : B), CategoryTheory.IsIso (F.mapId x)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_eq_nil_iff : ∀ {n : ℕ}, (*...n).toArray = #[] ↔ n = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.π_colimMap_desc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] {X' Y' Z : C} (f' g' : X' ⟶ Y')
  [inst_2 : CategoryTheory.Limits.HasCoequalizer f' g'] (p : X ⟶ X') (q : Y ⟶ Y')
  (wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
  (wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g') (h : Y' ⟶ Z)
  (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom f g f' g' p q wf wg))
        (CategoryTheory.Limits.coequalizer.desc h wh)) =
    CategoryTheory.CategoryStruct.comp q h
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.mul_certC.eq_1 : ∀ (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Stepwise.mul_certC p₁ k p c = (Lean.Grind.CommRing.Poly.mulConstC k p₁ c).beq' p
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.State.toDerive : Lean.Elab.ConfigEval.State✝ → Lean.NameMap Lean.ExprSet
-- Lean.Data.Json.Basic
Lean.Json.mkObj : List (String × Lean.Json) → Lean.Json
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β}, (m.insert k v).contains a = (k == a || m.contains a)
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.mk.injEq : ∀ {R : Type u_1} [inst : Ring R] (toSubsemiring : Subsemiring R)
  (eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0)
  (toSubsemiring_1 : Subsemiring R)
  (eq_zero_of_mem_of_neg_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring_1.carrier → -a ∈ toSubsemiring_1.carrier → a = 0),
  ({ toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem' } =
      { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'_1 }) =
    (toSubsemiring = toSubsemiring_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {v : β k}, a ∈ t.insert k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Lean.Parser.Do
Lean.Parser.Term.doLetArrow : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.opIso_inv_inr_op_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr.op h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h
-- Lean.Elab.Do.Basic
Lean.Elab.Do.MonadInfo.mk.injEq : ∀ (m : Lean.Expr) (u v : Lean.Level) (cachedPUnit cachedPUnitUnit m_1 : Lean.Expr) (u_1 v_1 : Lean.Level)
  (cachedPUnit_1 cachedPUnitUnit_1 : Lean.Expr),
  ({ m := m, u := u, v := v, cachedPUnit := cachedPUnit, cachedPUnitUnit := cachedPUnitUnit } =
      { m := m_1, u := u_1, v := v_1, cachedPUnit := cachedPUnit_1, cachedPUnitUnit := cachedPUnitUnit_1 }) =
    (m = m_1 ∧ u = u_1 ∧ v = v_1 ∧ cachedPUnit = cachedPUnit_1 ∧ cachedPUnitUnit = cachedPUnitUnit_1)
-- Mathlib.Algebra.Order.Group.Defs
/-- **Alias** of `le_of_mul_le_mul_left'`. -/
OrderedCommGroup.le_of_mul_le_mul_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] [MulLeftReflectLE α] {a b c : α}, a * b ≤ a * c → b ≤ c
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.smul_C : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] (s : S) (r : R),
  s • Polynomial.C r = Polynomial.C (s • r)
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.algebraMap₀_one : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorPower.algebraMap₀ 1 = GradedMonoid.GOne.one
-- Mathlib.Order.RelIso.Set
RelHomClass.map_inf : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : SemilatticeInf α] [inst_1 : LinearOrder β]
  [inst_2 : FunLike F β α] [RelHomClass F (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2] (a : F) (m n : β),
  a (min m n) = a m ⊓ a n
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.recv' : Std.Http.Body.Stream → BaseIO (Std.Async.AsyncTask (Option Std.Http.Chunk))
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
CategoryTheory.Functor.ShiftSequence.induced_isoShiftZero_hom_app_obj_assoc : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D A} {G : CategoryTheory.Functor C A} (e : L.comp F ≅ G)
  (M : Type u_4) [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : G.ShiftSequence M]
  (F' : M → CategoryTheory.Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m)
  [inst_6 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full]
  [inst_7 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] [inst_8 : CategoryTheory.HasShift D M]
  [inst_9 : L.CommShift M] (X : C) {Z : A} (h : F.obj (L.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.isoShiftZero M).hom.app (L.obj X)) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((e' 0).hom.app X)
        (CategoryTheory.CategoryStruct.comp ((G.isoShiftZero M).hom.app X) (e.inv.app X)))
      h
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicator_one_of_mem_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α},
  x ∈ closure E → (thickenedIndicator δ_pos E) x = 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
_private.Mathlib.LinearAlgebra.CliffordAlgebra.Even.0.CliffordAlgebra.even.lift.fFold_fFold : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : CliffordAlgebra.EvenHom Q A)
  (m : M) (x : A × ↥(CliffordAlgebra.even.lift.S✝ f)),
  ((CliffordAlgebra.even.lift.fFold✝ f) m) (((CliffordAlgebra.even.lift.fFold✝ f) m) x) = Q m • x
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.L₀'.f S.φ₁ = S.v₁₂.τ₁
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.IsMarkovKernel.piecewise : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  {s : Set α} {hs : MeasurableSet s} [inst : DecidablePred fun x => x ∈ s] [ProbabilityTheory.IsMarkovKernel κ]
  [ProbabilityTheory.IsMarkovKernel η], ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.piecewise hs κ η)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.distinct_keys_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → List.Pairwise (fun a b => (a.1 == b.1) = false) (Std.DHashMap.Raw.Const.toList m)
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotationAux₂.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)), o.rightAngleRotationAux₂ = { toLinearMap := o.rightAngleRotationAux₁, norm_map' := ⋯ }
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemHandler : Type
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyComplex.complexEmbedding_not_isReal : ∀ {K : Type u_2} [inst : Field K] [NumberField.IsTotallyComplex K] (φ : K →+* ℂ), ¬NumberField.ComplexEmbedding.IsReal φ
-- Mathlib.Algebra.QuadraticAlgebra.Defs
/-- `QuadraticAlgebra.re` as a `LinearMap`  -/
QuadraticAlgebra.reₗ : {R : Type u_1} → (a b : R) → [inst : Semiring R] → QuadraticAlgebra R a b →ₗ[R] R
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_abs_abs : ∀ {α : Type u_1} {l : Filter α} {u v : α → ℝ}, ((fun x => |u x|) =O[l] fun x => |v x|) ↔ u =O[l] v
-- Mathlib.Data.Fin.Tuple.Finset
Fin.cons_mem_piFinset_cons : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {x_zero : α 0} {x_tail : (i : Fin n) → α i.succ} {s_zero : Finset (α 0)}
  {s_tail : (i : Fin n) → Finset (α i.succ)},
  Fin.cons x_zero x_tail ∈ Fintype.piFinset (Fin.cons s_zero s_tail) ↔
    x_zero ∈ s_zero ∧ x_tail ∈ Fintype.piFinset s_tail
-- Mathlib.Algebra.Category.Grp.Basic
/-- Turn a morphism in `AddCommGrpCat` back into an `AddMonoidHom`.  -/
AddCommGrpCat.Hom.hom : {X Y : AddCommGrpCat} → X.Hom Y → ↑X →+ ↑Y
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- If `n` is finite and `B`,`C` are `R`-modules with the module topology,
then any bilinear map `Rⁿ × B → C` is automatically continuous.

Note that whilst this result works for semirings, for rings this result is superseded
by `IsModuleTopology.continuous_bilinear_of_finite_left`.
 -/
IsModuleTopology.continuous_bilinear_of_pi_fintype : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {B : Type u_2} [inst_2 : AddCommMonoid B]
  [inst_3 : Module R B] [inst_4 : TopologicalSpace B] [IsModuleTopology R B] {C : Type u_3} [inst_6 : AddCommMonoid C]
  [inst_7 : Module R C] [inst_8 : TopologicalSpace C] [IsModuleTopology R C] (ι : Type u_4) [Finite ι]
  (bil : (ι → R) →ₗ[R] B →ₗ[R] C), Continuous fun ab => (bil ab.1) ab.2
-- Mathlib.Algebra.Order.Star.Basic
IsSelfAdjoint.conjugate_nonneg : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a : R}, 0 ≤ a → ∀ {c : R}, IsSelfAdjoint c → 0 ≤ c * a * c
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
tangentMap_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M], tangentMap I I id = id