mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.parallelPair.ext.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (zero zero_1 :
    F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
  (e_zero : zero = zero_1)
  (one one_1 :
    F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one)
  (e_one : one = one_1)
  (left :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) one.hom =
      CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
  (right :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) one.hom =
      CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right)),
  CategoryTheory.Limits.parallelPair.ext zero one left right = CategoryTheory.Limits.parallelPair.ext zero_1 one_1 ⋯ ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.addRightStrictMono : ∀ {α : Type u} [inst : LT α] [inst_1 : Add α] [c : AddRightStrictMono α], AddRightStrictMono αᵒᵈ
-- Mathlib.GroupTheory.Congruence.Defs
/-- Additive congruence relations are closed under addition  -/
AddCon.add' : ∀ {M : Type u_1} [inst : Add M] (self : AddCon M) {w x y z : M},
  self.toSetoid w x → self.toSetoid y z → self.toSetoid (w + y) (x + z)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsRefl.smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_8}
  [inst_3 : Semiring α] [IsDomain α] [inst_5 : Module α R] [inst_6 : SMulCommClass R α R] [Module.IsTorsionFree α R]
  (a : α) {B : LinearMap.BilinForm R M}, B.IsRefl → (a • B).IsRefl
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α}, m.WF → (k ∈ Std.DHashMap.Raw.map f m ↔ k ∈ m)
-- Mathlib.Order.WellFoundedSet
IsAntichain.finite_of_partiallyWellOrderedOn : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α}, IsAntichain r s → s.PartiallyWellOrderedOn r → s.Finite
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Reindexing by the inverse of an equivalence and that equivalence yields the original simplex.  -/
Affine.Simplex.reindex_symm_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} (s : Affine.Simplex k P m) (e : Fin (n + 1) ≃ Fin (m + 1)),
  (s.reindex e.symm).reindex e = s
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_trans_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y = Z) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom q) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
-- Lean.Meta.Tactic.Simp.Diagnostics
Lean.Meta.Simp.mkDiagMessages : Lean.Meta.Simp.Diagnostics → Lean.MetaM (Array Lean.MessageData)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `none` if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryLT? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → Option (α × β)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_union : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {A B : Set α},
  MeasurableSet B → Disjoint A B → ∫⁻ (a : α) in A ∪ B, f a ∂μ = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ
-- Mathlib.Order.UpperLower.Prod
IsLowerSet.prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β},
  IsLowerSet s → IsLowerSet t → IsLowerSet (s ×ˢ t)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.ofFn.go.match_1.eq_2 : ∀ {n : ℕ} (motive : (x : ℕ) → x ≤ n → Sort u_1) (x : 0 ≤ n) (h_1 : (i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h)
  (h_2 : (x : 0 ≤ n) → motive 0 x),
  (match 0, x with
    | i.succ, h => h_1 i h
    | 0, x => h_2 x) =
    h_2 x
-- Mathlib.CategoryTheory.ExtremalEpi
CategoryTheory.ExtremalEpi.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [toEpi : CategoryTheory.Epi f],
  (∀ {Z : C} (p : X ⟶ Z) (i : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp p i = f → ∀ [CategoryTheory.Mono i], CategoryTheory.IsIso i) →
    CategoryTheory.ExtremalEpi f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (Std.TreeMap.ofList l cmp)[k]? = none
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_curry : ∀ {ι : Type u_6} {κ : Type u_7} {X : Type u_8} [inst : MeasurableSpace X], Measurable Function.curry
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.not_mem_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → k ∉ t₁ \ t₂
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : SizeOf α] [inst_3 : SizeOf β] (toFun : α → β) (injective : Function.Injective toFun)
  (succ?_toFun : ∀ (a : α), Std.PRange.succ? (toFun a) = Option.map toFun (Std.PRange.succ? a))
  (succMany?_toFun : ∀ (n : ℕ) (a : α), Std.PRange.succMany? n (toFun a) = Option.map toFun (Std.PRange.succMany? n a)),
  sizeOf { toFun := toFun, injective := injective, succ?_toFun := succ?_toFun, succMany?_toFun := succMany?_toFun } = 1
-- Mathlib.CategoryTheory.Generator.Basic
/-- Given a category `C` that has a detector (`HasDetector C`), `detector C` is an arbitrarily
chosen detector of `C`.
 -/
CategoryTheory.detector : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.HasDetector C] → C
-- Mathlib.Data.Finset.Preimage
Finset.coe_preimage : ∀ {α : Type u} {β : Type v} {f : α → β} (s : Finset β) (hf : Set.InjOn f (f ⁻¹' ↑s)), ↑(s.preimage f hf) = f ⁻¹' ↑s
-- Mathlib.Order.CompleteLatticeIntervals
Set.Iic.coe_iInf : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLattice α] {a : α} (f : ι → ↑(Set.Iic a)), ↑(⨅ i, f i) = a ⊓ ⨅ i, ↑(f i)
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The forgetful functor from the category of ring objects in `C` to `C`.  -/
CategoryTheory.CommRingObjCat.forget : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Functor (CategoryTheory.CommRingObjCat C) C
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eval_zero : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.eval 0 (Polynomial.Chebyshev.T R n) = ↑(if Even n then ↑(n / 2).negOnePow else 0)
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.suppPreservation_iff_liftpPreservation : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F], MvQPF.SuppPreservation ↔ MvQPF.LiftPPreservation
-- Mathlib.Algebra.CharP.Two
CharTwo.sq_inj : ∀ {R : Type u_1} [inst : CommRing R] [CharP R 2] [NoZeroDivisors R] {x y : R}, x ^ 2 = y ^ 2 ↔ x = y
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (acc : aig.Ref) (idx : ℕ)
  (s : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f],
  aig.decls.size ≤ (Std.Sat.AIG.RefVec.fold.go aig acc idx len s f).aig.decls.size
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.mono_ac : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν₁ ν₂ : MeasureTheory.Measure α},
  μ₁.MutuallySingular ν₁ → μ₂.AbsolutelyContinuous μ₁ → ν₂.AbsolutelyContinuous ν₁ → μ₂.MutuallySingular ν₂
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instFullMonCatForget₂MonoidHomCarrierCarrier : (CategoryTheory.forget₂ CommMonCat MonCat).Full
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.leftInverse_comap_map : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W), Function.LeftInverse (SimpleGraph.comap ⇑f) (SimpleGraph.map ⇑f)
-- Mathlib.Algebra.Category.Grp.Colimits
/-- The obvious additive map from `Quot F` to `Quot (F ⋙ uliftFunctor.{u'})`.
 -/
AddCommGrpCat.Colimits.quotToQuotUlift : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : DecidableEq J] →
        AddCommGrpCat.Colimits.Quot F →+ AddCommGrpCat.Colimits.Quot (F.comp AddCommGrpCat.uliftFunctor)
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLawfulOrderMinOpposite : ∀ {α : Type u_1} {il : LE α} {im : Min α} [Std.LawfulOrderMin α], Std.LawfulOrderMax α
-- Mathlib.FieldTheory.SeparableDegree
/-- A constant polynomial has zero separable degree.  -/
Polynomial.natSepDegree_eq_zero : ∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natDegree = 0 → f.natSepDegree = 0
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X)
  (P : CategoryTheory.Functor Dᵒᵖ A) {Z : A} (h : (Φ.map F K).presheafFiber.obj P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.map (F.map f).op)
      (CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) h) =
    CategoryTheory.CategoryStruct.comp
      (Φ.toPresheafFiberMap F K P Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x)) h
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- `negAt` preserves the volume .  -/
NumberField.mixedEmbedding.volume_preserving_negAt : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} [inst_1 : NumberField K],
  MeasureTheory.MeasurePreserving (⇑(NumberField.mixedEmbedding.negAt s)) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.codisjoint_supported_supported : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s t : Set α}, Codisjoint s t → Codisjoint (Finsupp.supported M R s) (Finsupp.supported M R t)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashSet α), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.get? a = m_1.get? a_1
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.toFun_eq_coe : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {f : CuspForm Γ k}, f.toFun = ⇑f
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
ContDiff.continuous_iteratedDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {n : WithTop ℕ∞} (m : ℕ),
  ContDiff 𝕜 n f → ↑m ≤ n → Continuous (iteratedDeriv m f)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length'_nil : ∀ {α : Type u}, Stream'.Seq.nil.length' = 0
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Mon.mul.go.match_1.eq_3 : ∀ (motive : Nat.Internal.SOM.Mon → Nat.Internal.SOM.Mon → Sort u_1) (v₁ : Nat.Internal.Linear.Var)
  (m₁ : List Nat.Internal.Linear.Var) (v₂ : Nat.Internal.Linear.Var) (m₂ : List Nat.Internal.Linear.Var)
  (h_1 : (m₁ : Nat.Internal.SOM.Mon) → motive m₁ []) (h_2 : (m₂ : Nat.Internal.SOM.Mon) → motive [] m₂)
  (h_3 :
    (v₁ : Nat.Internal.Linear.Var) →
      (m₁ : List Nat.Internal.Linear.Var) →
        (v₂ : Nat.Internal.Linear.Var) → (m₂ : List Nat.Internal.Linear.Var) → motive (v₁ :: m₁) (v₂ :: m₂)),
  (match v₁ :: m₁, v₂ :: m₂ with
    | m₁, [] => h_1 m₁
    | [], m₂ => h_2 m₂
    | v₁ :: m₁, v₂ :: m₂ => h_3 v₁ m₁ v₂ m₂) =
    h_3 v₁ m₁ v₂ m₂
-- Lean.Environment
_private.Lean.Environment.0.Lean.PersistentEnvExtension.getModuleEntries.unsafe_impl_2 : {α β σ : Type} →
  [Inhabited σ] → Lean.PersistentEnvExtension α β σ → Lean.ModuleIdx → Array Lean.EnvExtensionState → Array α
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.instIsIsoFunctorTypeToRangeOfMono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (p : F' ⟶ F)
  [CategoryTheory.Mono p], CategoryTheory.IsIso (CategoryTheory.Subfunctor.toRange p)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.instIsIntegralOfIsMinimal : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K}
  [WeierstrassCurve.IsMinimal R W], WeierstrassCurve.IsIntegral R W
-- Mathlib.RingTheory.LaurentSeries
/-- The integral valuation of the power series `X : K⟦X⟧` equals `(ofAdd -1) : ℤᵐ⁰`.  -/
PowerSeries.intValuation_X : ∀ {K : Type u_2} [inst : Field K], (PowerSeries.idealX K).intValuation PowerSeries.X = WithZero.exp (-1)
-- Mathlib.Order.Atoms
IsCoatom.sInf_le : ∀ {α : Type u_2} [inst : Order.Coframe α] {s : Set α} {a : α}, IsCoatom a → (sInf s ≤ a ↔ ∃ b ∈ s, b ≤ a)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.isHomo : Lean.Expr → Lean.Expr → Lean.Expr → Bool
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_inj : ∀ {R : Type u_2} [inst : NonAssocRing R] {S T : Subring Rᵐᵒᵖ}, S.unop = T.unop ↔ S = T
-- Mathlib.CategoryTheory.Limits.Cones
/-- Functoriality is functorial.  -/
CategoryTheory.Limits.Cone.functorialityCompFunctoriality : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {E : Type u₅} →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} E] →
                (F : CategoryTheory.Functor J C) →
                  (G : CategoryTheory.Functor C D) →
                    (H : CategoryTheory.Functor D E) →
                      (CategoryTheory.Limits.Cone.functoriality F G).comp
                          (CategoryTheory.Limits.Cone.functoriality (F.comp G) H) ≅
                        CategoryTheory.Limits.Cone.functoriality F (G.comp H)
-- Mathlib.Algebra.Star.TransferInstance
/-- Transfer `StarModule` across an `Equiv`  -/
Equiv.starModule : ∀ {R : Type u_1} {S : Type u_2} (e : R ≃ S) (𝕜 : Type u_3) [inst : Star 𝕜] [inst_1 : Star S] [inst_2 : SMul 𝕜 S]
  [StarModule 𝕜 S], StarModule 𝕜 R
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_inv_le_iff_of_neg : ∀ {x y z : ℝ}, 0 < x → 0 < y → z < 0 → (x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x)
-- Mathlib.Topology.UniformSpace.CompactConvergence
CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {V : ℕ → Set (β × β)}
  (K : CompactExhaustion α),
  (uniformity β).HasAntitoneBasis V →
    (uniformity C(α, β)).HasAntitoneBasis fun n => {fg | ∀ x ∈ K n, (fg.1 x, fg.2 x) ∈ V n}
-- Mathlib.Topology.Homotopy.Product
/-- The product of path classes q₁ and q₂. This is `Path.prod` descended to the quotient.  -/
Path.Homotopic.prod : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {a₁ a₂ : α} →
          {b₁ b₂ : β} →
            Path.Homotopic.Quotient a₁ a₂ → Path.Homotopic.Quotient b₁ b₂ → Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂)
-- Mathlib.Computability.PartrecCode
/-- Code for partial recursive functions from ℕ to ℕ.
See `Nat.Partrec.Code.eval` for the interpretation of these constructors.
 -/
Nat.Partrec.Code : Type
-- Mathlib.Order.WithBot
WithBot.unbot.eq_1 : ∀ {α : Type u_1} (x_2 : α) (x_3 : ↑x_2 ≠ ⊥), WithBot.unbot (some x_2) x_3 = x_2
-- Mathlib.Analysis.Calculus.Deriv.Inv
HasDerivWithinAt.div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} {c' d' : 𝕜'},
  HasDerivWithinAt c c' s x →
    HasDerivWithinAt d d' s x → d x ≠ 0 → HasDerivWithinAt (c / d) ((c' * d x - c x * d') / d x ^ 2) s x
-- Aesop.Util.UnionFind
Aesop.instInhabitedUnionFind.default : {α : Type u_1} → {inst : BEq α} → {inst_1 : Hashable α} → Aesop.UnionFind α
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_subset : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), G'.edgeSet ⊆ G.edgeSet
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.lift_of : ∀ {α : Type u_3} {M : Type u_4} [inst : Monoid M] (f : α → M) {rels : FreeMonoid α → FreeMonoid α → Prop}
  (h : ∀ (a b : FreeMonoid α), rels a b → (FreeMonoid.lift f) a = (FreeMonoid.lift f) b) {x : α},
  (PresentedMonoid.lift f h) (PresentedMonoid.of rels x) = f x
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationData.mk : Lean.Name → String → ProofWidgets.Html → ProofWidgets.ExprPresentationData
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_add_tsub_comm : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c d : α},
  AddLECancellable b → AddLECancellable d → b ≤ a → d ≤ c → a - b + (c - d) = a + c - (b + d)
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.copy.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] (f : sInfHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_sInf' := ⋯ }
-- Mathlib.CategoryTheory.Opposites
/-- The opposite of a fully faithful functor is fully faithful.  -/
CategoryTheory.Functor.FullyFaithful.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ᵒᵖ} → F.FullyFaithful → F.leftOp.FullyFaithful
-- Init.Data.Rat.Lemmas
Rat.intCast_natCast : ∀ (n : ℕ), ↑↑n = ↑n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_insert!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k}, t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insert! k v t).minKey ⋯ = k
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.coeff_eq_zero_of_totalDegree_lt : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ},
  f.totalDegree < ∑ i ∈ d.support, d i → MvPolynomial.coeff d f = 0
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.struct.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Preregular C}
  {inst_2 : CategoryTheory.FinitaryExtensive C}
  {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} {X : ℕ → C}
  {x : (n : ℕ) → (F.obj (Opposite.op n)).obj.obj (Opposite.op (X n))} {map : (n : ℕ) → X (n + 1) ⟶ X n}
  {effectiveEpi : ∀ (n : ℕ), CategoryTheory.EffectiveEpi (map n)}
  {w :
    ∀ (n : ℕ),
      (CategoryTheory.ConcreteCategory.hom ((F.map (CategoryTheory.homOfLE ⋯).op).hom.app (Opposite.op (X (n + 1)))))
          (x (n + 1)) =
        (CategoryTheory.ConcreteCategory.hom ((F.obj (Opposite.op n)).obj.map (map n).op)) (x n)}
  {X_1 : ℕ → C} {x_1 : (n : ℕ) → (F.obj (Opposite.op n)).obj.obj (Opposite.op (X_1 n))}
  {map_1 : (n : ℕ) → X_1 (n + 1) ⟶ X_1 n} {effectiveEpi_1 : ∀ (n : ℕ), CategoryTheory.EffectiveEpi (map_1 n)}
  {w_1 :
    ∀ (n : ℕ),
      (CategoryTheory.ConcreteCategory.hom ((F.map (CategoryTheory.homOfLE ⋯).op).hom.app (Opposite.op (X_1 (n + 1)))))
          (x_1 (n + 1)) =
        (CategoryTheory.ConcreteCategory.hom ((F.obj (Opposite.op n)).obj.map (map_1 n).op)) (x_1 n)},
  { X := X, x := x, map := map, effectiveEpi := effectiveEpi, w := w } =
      { X := X_1, x := x_1, map := map_1, effectiveEpi := effectiveEpi_1, w := w_1 } →
    X = X_1 ∧ x ≍ x_1 ∧ map ≍ map_1
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.declNameNonRec : Lean.Elab.PartialFixpoint.EqnInfo → Lean.Name
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
_private.Init.Data.Float.Model.Unpacked.Pack.Lemmas.0.Float.Model.UnpackedFloat.pack.match_1.eq_1 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)),
  (match Float.Model.UnpackedFloat.notANumber with
    | Float.Model.UnpackedFloat.notANumber => h_1 ()
    | Float.Model.UnpackedFloat.infinity s => h_2 s
    | Float.Model.UnpackedFloat.zero s => h_3 s
    | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) =
    h_1 ()
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance between a set and its closure vanishes.  -/
Metric.hausdorffDist_self_closure : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Metric.hausdorffDist s (closure s) = 0
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- If a measurable space is countably generated and equipped with an s-finite measure, then the
measure is separable.  -/
MeasureTheory.instIsSeparableOfCountablyGeneratedOfSFinite : ∀ {X : Type u_1} [m : MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasurableSpace.CountablyGenerated X]
  [MeasureTheory.SFinite μ], MeasureTheory.IsSeparable μ
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.ι_colimitConstInitial_hom : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasInitial C] {j : J},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j)
      CategoryTheory.Limits.colimitConstInitial.hom =
    CategoryTheory.Limits.initial.to (⊥_ C)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mapPreimage.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  (K K_1 : CategoryTheory.GrothendieckTopology D) (e_K : K = K_1) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) {X Y : C} (f f_1 : G.obj X ⟶ G.obj Y),
  f = f_1 →
    CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F f =
      CategoryTheory.Functor.IsDenseSubsite.mapPreimage K_1 G F f_1
-- Init.Data.UInt.Lemmas
UInt64.left_eq_add : ∀ {a b : UInt64}, a = a + b ↔ b = 0
-- Mathlib.Data.Multiset.Sections
Multiset.mem_sections : ∀ {α : Type u_1} {s : Multiset (Multiset α)} {a : Multiset α}, a ∈ s.Sections ↔ Multiset.Rel (fun s a => a ∈ s) s a