mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.eval₂_hom : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : R),
  Polynomial.eval₂ f (f x) p = f (Polynomial.eval x p)
-- Batteries.Data.List.Basic
List.zipWithLeft'TR.go.eq_3 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : Array γ) (a_1 : α) (as : List α) (b : β)
  (bs : List β),
  List.zipWithLeft'TR.go f (a_1 :: as) (b :: bs) a = List.zipWithLeft'TR.go f as bs (a.push (f a_1 (some b)))
-- Aesop.RuleTac.Basic
Aesop.RuleApplication.mk.sizeOf_spec : ∀ (goals : Array Aesop.Subgoal) (postState : Lean.Meta.SavedState) (scriptSteps? : Option (Array Aesop.Script.LazyStep))
  (successProbability? : Option Aesop.Percent),
  sizeOf
      { goals := goals, postState := postState, scriptSteps? := scriptSteps?,
        successProbability? := successProbability? } =
    1 + sizeOf goals + sizeOf postState + sizeOf scriptSteps? + sizeOf successProbability?
-- Mathlib.Topology.Bases
TopologicalSpace.isSeparable_univ_iff : ∀ {α : Type u} [t : TopologicalSpace α], TopologicalSpace.IsSeparable Set.univ ↔ TopologicalSpace.SeparableSpace α
-- Std.Http.Data.Method
/-- Retrieve a resource.
Source: https://httpwg.org/specs/rfc9110.html#section-9.3.1
 -/
Std.Http.Method.get : Std.Http.Method
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_le_minKey_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {he : (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false},
  (compare (t.minKey ⋯) ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKey he)).isLE = true
-- Mathlib.Order.Bounds.Image
StrictAnti.mem_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {a : α} {s : Set α},
  StrictAnti f → (f a ∈ lowerBounds (f '' s) ↔ a ∈ upperBounds s)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_zsmul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] {𝒜 : ι → σ} (x : Submonoid A) (n : ℤ) (y : HomogeneousLocalization 𝒜 x),
  (n • y).val = n • y.val
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyPrepareParams : Lean.FromJson Lean.Lsp.CallHierarchyPrepareParams
-- Mathlib.Algebra.Group.Prod
Prod.instCommMonoid : {M : Type u_3} → {N : Type u_4} → [CommMonoid M] → [CommMonoid N] → CommMonoid (M × N)
-- Mathlib.RingTheory.Radical.NatInt
Nat.two_le_radical_iff : ∀ {n : ℕ}, 2 ≤ UniqueFactorizationMonoid.radical n ↔ 2 ≤ n
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- A walk between two vertices separated by a set of edges must go through one of those edges.  -/
SimpleGraph.Walk.exists_mem_edges_of_not_reachable_deleteEdges : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {s : Set (Sym2 V)},
  ¬(G.deleteEdges s).Reachable u v → ∃ e ∈ s, e ∈ w.edges
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.natCoe : {R : Type u_1} → [inst : AddMonoidWithOne R] → Coe (ArithmeticFunction ℕ) (ArithmeticFunction R)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageAddHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Add α] [inst_2 : Add β]
  [inst_3 : FunLike F α β] [inst_4 : AddHomClass F α β] (f : F) [inst_5 : DecidableEq β],
  Finset.imageAddHom f = { toFun := Finset.image ⇑f, map_add' := ⋯ }
-- Init.Data.UInt.Bitwise
UInt16.shiftRight_xor : ∀ {a b c : UInt16}, (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubring.unitization_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S)
  (x : Unitization ℤ ↥s), (NonUnitalSubring.unitization s) x = ↑x.toProd.1 + ↑x.toProd.2
-- Mathlib.CategoryTheory.Abelian.Images
/-- The kernel of the cokernel of `f` is called the (abelian) image of `f`.  -/
CategoryTheory.Abelian.image : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (f : P ⟶ Q) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] → C
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_obj_left_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.left = sq.X₁
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instBEqRingMode.beq : Mathlib.Tactic.RingNF.RingMode → Mathlib.Tactic.RingNF.RingMode → Bool
-- Init.Data.Array.Lemmas
Array.mem_ite_empty_left : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {xs : Array α}, (x ∈ if p then #[] else xs) ↔ ¬p ∧ x ∈ xs
-- Mathlib.CategoryTheory.Opposites
/-- An equivalence between opposite categories gives an equivalence between the original categories.
 -/
CategoryTheory.Equivalence.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (Cᵒᵖ ≌ Dᵒᵖ) → (C ≌ D)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.inclusion_injective : ∀ {R : Type u} [inst : NonAssocSemiring R] {S T : Subsemiring R} (h : S ≤ T),
  Function.Injective ⇑(Subsemiring.inclusion h)
-- Std.Sync.Broadcast
/-- Enqueues an element to the back of the circular buffer.
If the buffer is full, the oldest element (at front) is overwritten.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.enqueue : {α : Type} → α → Std.Bounded.State✝ α → BaseIO (Std.Bounded.State✝ α)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
cfcₙHom_integral : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [inst_8 : CompleteSpace A] [inst_9 : NormedSpace ℝ A] (a : A) (f : X → ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜),
  MeasureTheory.Integrable f μ →
    ∀ (ha : autoParam (p a) cfcₙHom_integral._auto_1),
      ∫ (x : X), (cfcₙHom ha) (f x) ∂μ = (cfcₙHom ha) (∫ (x : X), f x ∂μ)
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
_private.Lean.Meta.Tactic.Simp.SimpCongrTheorems.0.Lean.Meta.addSimpCongrTheoremEntry.insert : Lean.Meta.SimpCongrTheorem → List Lean.Meta.SimpCongrTheorem → List Lean.Meta.SimpCongrTheorem
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_pow : ∀ (x : ℕ∞) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.RingTheory.Valuation.RankOne
/-- If `v` is a rank one valuation, then `x : Γ₀` has image `0` under `RankOne.hom v` if and
only if `x = 0`.  -/
Valuation.RankOne.hom_eq_zero_iff : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  [hv : v.RankOne] {x : (MonoidWithZeroHom.ofClass v).ValueGroup₀}, (Valuation.RankOne.hom v) x = 0 ↔ x = 0
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_zero_of_not_uniqueDiffWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, ¬UniqueDiffWithinAt 𝕜 s x → derivWithin f s x = 0
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.associator_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] (X Y Z : P.FullSubcategory),
  CategoryTheory.MonoidalCategoryStruct.associator X Y Z =
    P.isoMk (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj)
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.instOrderHomClassNat : ∀ {α : Type u_1} {s : Set α}, OrderHomClass s.FiniteExhaustion ℕ (Set α)
-- Lean.Parser.Types
Lean.Parser.FirstTokens : Type
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.hom_ofHom : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), CommRingCat.Hom.hom (CommRingCat.ofHom f) = f
-- Mathlib.Data.Finset.Functor
Finset.instAlternativeMonad : [(P : Prop) → Decidable P] → AlternativeMonad Finset
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.coe_sSup_of_directedOn : ∀ {M : Type u_1} [inst : AddZeroClass M] {S : Set (AddSubmonoid M)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ↑(sSup S) = ⋃ s ∈ S, ↑s
-- Mathlib.Algebra.Homology.ImageToKernel
imageSubobjectIso_imageToKernel' : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasImages V]
  (w : CategoryTheory.CategoryStruct.comp f g = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom (imageToKernel' f g w) =
    CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobjectIso g).hom
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_two : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.T R 2 = 2 * Polynomial.X ^ 2 - 1
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y)
  (U :
    TopologicalSpace.Opens
      ↑↑(CategoryTheory.Limits.coequalizer (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
              (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).toPresheafedSpace)
  (s :
    ↑((CategoryTheory.Limits.coequalizer (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
              (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).presheaf.obj
        (Opposite.op U))),
  ⇑(CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.coequalizer.π (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
                (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).hom.base) ⁻¹'
      ⇑(CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.coequalizer.π (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
                  (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).hom.base) ''
        (AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen f g U s).carrier =
    (AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen f g U s).carrier
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {d d' : D} (f : d ⟶ d'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d').inv
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.stdBasis_apply_isReal : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K)
  (w : { w // w.IsReal }), ((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inl w) = x.1 w
-- Aesop.Forward.Match
/-- Construct the proof of the new hypothesis represented by `m`.  -/
Aesop.ForwardRuleMatch.getProof : Lean.MVarId → Aesop.ForwardRuleMatch → Lean.MetaM (Option Lean.Expr)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.addMap_of_Z_eq_zero_right : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : WeierstrassCurve.Projective.PointClass F}
  {Q : Fin 3 → F}, W.NonsingularLift P → W.Nonsingular Q → Q 2 = 0 → W.addMap P ⟦Q⟧ = P
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.HasCountableLimits.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  autoParam
      (∀ (J : Type) [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J],
        CategoryTheory.Limits.HasLimitsOfShape J C)
      CategoryTheory.Limits.HasCountableLimits.out._autoParam →
    CategoryTheory.Limits.HasCountableLimits C
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_mod : ∀ (a n : ℕ), ↑(a % n) = ↑a
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.CorePlotsOn.isPlotOn_univ : ∀ {X : Type u_1} (self : DiffeologicalSpace.CorePlotsOn X) {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  self.isPlotOn ⋯ p ↔ self.isPlot p
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.Subcomplex.mem_degenerate_iff : ∀ {X : SSet} (A : X.Subcomplex) {n : ℕ} (x : ↑(A.obj (Opposite.op { len := n }))),
  x ∈ A.toSSet.degenerate n ↔ ↑x ∈ X.degenerate n
-- Mathlib.CategoryTheory.Enriched.Opposite
CategoryTheory.forgetEnrichmentOppositeEquivalence_unitIso : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  [inst_2 : CategoryTheory.BraidedCategory V] (C : Type u) [inst_3 : CategoryTheory.EnrichedCategory V C],
  (CategoryTheory.forgetEnrichmentOppositeEquivalence V C).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.ForgetEnrichment V Cᵒᵖ)).obj x)) ⋯
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.registerLevelMVarErrorExprInfo : Lean.Expr → Lean.Syntax → optParam (Option Lean.MessageData) none → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.eq_of_eqOn_stop : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f g : R →+* S},
  Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Context.mk.sizeOf_spec : ∀ (optionsPerPos : Lean.PrettyPrinter.Delaborator.OptionsPerPos) (currNamespace : Lean.Name)
  (openDecls : List Lean.OpenDecl) (inPattern : Bool) (subExpr : Lean.SubExpr) (depth lctxInitIndices : ℕ),
  sizeOf
      { optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls, inPattern := inPattern,
        subExpr := subExpr, depth := depth, lctxInitIndices := lctxInitIndices } =
    1 + sizeOf optionsPerPos + sizeOf currNamespace + sizeOf openDecls + sizeOf inPattern + sizeOf subExpr +
        sizeOf depth +
      sizeOf lctxInitIndices
-- Mathlib.Data.NNRat.Defs
NNRat.num_zero : NNRat.num 0 = 0
-- Mathlib.Order.Disjoint
isCompl_ofDual_iff : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {a b : αᵒᵈ},
  IsCompl (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ IsCompl a b
-- Mathlib.Logic.Equiv.Functor
Functor.mapEquiv.congr_simp : ∀ {α β : Type u} (f : Type u → Type v) [inst : Functor f] [inst_1 : LawfulFunctor f] (h h_1 : α ≃ β),
  h = h_1 → Functor.mapEquiv f h = Functor.mapEquiv f h_1
-- Mathlib.Data.Seq.Defs
_private.Mathlib.Data.Seq.Defs.0.Stream'.Seq.omap.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option (α × β) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (a : α) → (b : β) → motive (some (a, b))),
  (match none with
    | none => h_1 ()
    | some (a, b) => h_2 a b) =
    h_1 ()
-- Mathlib.Algebra.MvPolynomial.Variables
/-- `vars p` is the set of variables appearing in the polynomial `p`  -/
MvPolynomial.vars : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → MvPolynomial σ R → Finset σ
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.weakEquivalence_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {A : C} (self : HomotopicalAlgebra.Cylinder A), HomotopicalAlgebra.WeakEquivalence self.π
-- Mathlib.Data.List.Nodup
List.nodup_attach : ∀ {α : Type u} {l : List α}, l.attach.Nodup ↔ l.Nodup
-- Lean.Util.Heartbeats
/-- Counts the number of heartbeats used during a monadic function.

Remember that user facing heartbeats (e.g. as used in `set_option maxHeartbeats`)
differ from the internally tracked heartbeats by a factor of 1000,
so you need to divide the results here by 1000 before comparing with user facing numbers.
 -/
Lean.withHeartbeats : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadLiftT BaseIO m] → m α → m (α × ℕ)
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_X_pow : ∀ {R : Type u} {n : ℕ} [inst : Semiring R], (Polynomial.X ^ n).divX = if n = 0 then 0 else Polynomial.X ^ (n - 1)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_biUnion_closure_eq_closure_sUnion : ∀ {α : Type u_2} (M : Matroid α) (Xs : Set (Set α)), M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.adhoc.injEq : ∀ (backend backend_1 : Lean.Name),
  (Lean.ExternEntry.adhoc backend = Lean.ExternEntry.adhoc backend_1) = (backend = backend_1)
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_add_right_ball : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ℝ),
  (fun x => x + a) ⁻¹' Metric.ball b r = Metric.ball (b - a) r
-- Mathlib.Algebra.Group.Defs
IsAddCommutative.instAddCommSemigroup.eq_1 : ∀ {M : Type u_2} [inst : AddSemigroup M] [inst_1 : IsAddCommutative M],
  IsAddCommutative.instAddCommSemigroup = { toAddSemigroup := inst, add_comm := ⋯ }
-- Mathlib.Analysis.Convex.Gauge
interior_subset_gauge_lt_one : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousSMul ℝ E]
  (s : Set E), interior s ⊆ {x | gauge s x < 1}
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivaryOn_inv_left₀`. -/
MonovaryOn.inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → MonovaryOn f g s → AntivaryOn f⁻¹ g s
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN : {α : Type u_1} → [Lean.Grind.NatModule α] → Lean.Grind.Linarith.Context α → Lean.Grind.Linarith.Poly → α
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.Order.Frame.MinimalAxioms.inf_iSup_eq : ∀ {α : Type u} {ι : Sort w} [inst : CompleteLattice α],
  Order.Frame.MinimalAxioms α → ∀ (a : α) (f : ι → α), a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
-- Mathlib.Topology.Constructions
MapClusterPt.curry_prodMap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {α : Type u_5} {β : Type u_6}
  {f : α → X} {g : β → Y} {la : Filter α} {lb : Filter β} {x : X} {y : Y},
  MapClusterPt x la f → MapClusterPt y lb g → MapClusterPt (x, y) (la.curry lb) (Prod.map f g)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Pushing a free group basis through a group isomorphism.  -/
FreeGroupBasis.map : {ι : Type u_1} →
  {G : Type u_3} →
    {H : Type u_4} → [inst : Group G] → [inst_1 : Group H] → FreeGroupBasis ι G → G ≃* H → FreeGroupBasis ι H
-- Mathlib.Order.Notation
/-- Delaborate `max x y` into `x ⊔ y` if the type is not a linear order.  -/
Mathlib.Meta.delabSup : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.of_insert : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E} {y : E},
  DifferentiableWithinAt 𝕜 f (insert y s) x → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Algebra.Prime.Defs
Prime.ne_one : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → p ≠ 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β},
  Std.ExtDHashMap.Const.get? (m.insert k v) a = if (k == a) = true then some v else Std.ExtDHashMap.Const.get? m a
-- Mathlib.GroupTheory.SemidirectProduct
/-- The canonical projection map `N ⋊[φ] G →* G`, as a group hom.  -/
SemidirectProduct.rightHom : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → N ⋊[φ] G →* G
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- There exists a vertex of minimal degree. Note the assumption of being nonempty is necessary, as
the lemma implies there exists a vertex.  -/
SimpleGraph.exists_minimal_degree_vertex : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Nonempty V],
  ∃ v, G.minDegree = G.degree v
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_naturality : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
  (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y')
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y).HasMap
      p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y').HasMap
      p],
  CategoryTheory.CategoryStruct.comp φ (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv
      (CategoryTheory.GradedObject.mapBifunctorMapMap F p
        (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
-- Mathlib.Data.Quot
/-- A version of `Trunc.rec` taking `q : Trunc α` as the first argument.  -/
Trunc.recOn : {α : Sort u_1} →
  {C : Trunc α → Sort u_3} → (q : Trunc α) → (f : (a : α) → C (Trunc.mk a)) → (∀ (a b : α), ⋯ ▸ f a = f b) → C q
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.coe_of : ∀ (α : Type u_1) [inst : Nonempty α] [inst_1 : Fintype α] [inst_2 : LinearOrder α],
  ↑(NonemptyFinLinOrd.of α).toLinOrd = α
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBase.closure_eq : ∀ {α : Type u_2} {M : Matroid α} {B : Set α}, M.IsBase B → M.closure B = M.E
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_sub_theta_ge_psi_add_psi_add_psi : ∀ {x : ℝ},
  0 ≤ x →
    Chebyshev.psi (x ^ 2⁻¹) + Chebyshev.psi (x ^ 3⁻¹) + Chebyshev.psi (x ^ 7⁻¹) ≤ Chebyshev.psi x - Chebyshev.theta x
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.mulMon_nc_NonnegCoeffs : ∀ {p : Lean.Grind.CommRing.Poly} {k : ℤ} (m : Lean.Grind.CommRing.Mon),
  k ≥ 0 → p.NonnegCoeffs → (Lean.Grind.CommRing.Poly.mulMon_nc k m p).NonnegCoeffs
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.exponent_two : ∀ {G : Type u_1} {inst : Group G} [self : IsKleinFour G], Monoid.exponent G = 2
-- Init.Data.Fin.Lemmas
Fin.cast_addNat_right : ∀ {n m m' : ℕ} (i : Fin n) (h : n + m' = n + m), Fin.cast h (i.addNat m') = i.addNat m
-- Init.Data.Vector.OfFn
Vector.ofFnM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α},
  (Vector.ofFnM fun i => pure (f i)) = pure (Vector.ofFn f)
-- Mathlib.Order.RelClasses
/-- **Alias** of `eq_of_subset_of_not_ssubset'`.

---

Set notation form of `eq_of_le_of_not_lt'` -/
eq_of_superset_of_not_ssuperset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, b ⊆ a → ¬b ⊂ a → a = b