mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- Note: the priority is set to 90 to ensure that this instance is only applied after
`PseudoEMetricSpace.pseudoMetrizableSpace`. This prevents unnecessary attempts to infer
completeness.  -/
TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X],
  TopologicalSpace.PseudoMetrizableSpace X
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s t : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → t ⊆ s → HasFPowerSeriesWithinOnBall f p t x r
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.ext : ∀ {x y : Std.Time.Timestamp}, x.val = y.val → x = y
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.traceClsCast : Lean.Name
-- Mathlib.Data.Int.Sqrt
Int.sqrt_ofNat : ∀ (n : ℕ), Int.sqrt (OfNat.ofNat n) = ↑(OfNat.ofNat n).sqrt
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.response.injEq : ∀ (id : Lean.JsonRpc.RequestID) (result : Lean.Json) (id_1 : Lean.JsonRpc.RequestID) (result_1 : Lean.Json),
  (Lean.JsonRpc.Message.response id result = Lean.JsonRpc.Message.response id_1 result_1) =
    (id = id_1 ∧ result = result_1)
-- Mathlib.Algebra.CharP.Frobenius
MonoidHom.map_iterateFrobenius : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (f : R →* S) (p : ℕ)
  [inst_2 : ExpChar R p] [inst_3 : ExpChar S p] (x : R) (n : ℕ),
  f ((iterateFrobenius R p n) x) = (iterateFrobenius S p n) (f x)
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureResult.mk : List Aesop.Script.Step → Lean.Meta.SavedState → Aesop.Script.DynStructureResult
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Except.toBool.match_1.eq_1 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (a : ε) → motive (Except.error a)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error a => h_2 a) =
    h_1 a
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_comp_η_tensorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] {X : C} {Y : D} (f : F.obj X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Functor.OplaxMonoidal.η F) f) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) f))
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.homogeneousLocalizationCommRing : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} → [GradedRing 𝒜] → {x : Submonoid A} → CommRing (HomogeneousLocalization 𝒜 x)
-- Mathlib.Data.Set.MulAntidiagonal
Set.MulAntidiagonal.eq_of_fst_eq_fst : ∀ {α : Type u_1} [inst : CommMonoid α] [IsCancelMul α] {s t : Set α} {a : α} {x y : ↑(s.mulAntidiagonal t a)},
  (↑x).1 = (↑y).1 → x = y
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- Two partial maps from reduced schemes to separated schemes are equivalent if and only if
they are equal on **any** open dense subset.  -/
AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated_of_le : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] [AlgebraicGeometry.IsReduced X]
  [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f g : X.PartialMap Y} [AlgebraicGeometry.Scheme.PartialMap.IsOver S f]
  [AlgebraicGeometry.Scheme.PartialMap.IsOver S g] {W : X.Opens} (hW : Dense ↑W) (hWl : W ≤ f.domain)
  (hWr : W ≤ g.domain), f.equiv g ↔ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
-- Mathlib.Dynamics.Ergodic.Action.Basic
AddAction.aeconst_of_aestabilizer_eq_top : ∀ (G : Type u_1) {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : AddGroup G]
  [inst_1 : AddAction G α] [inst_2 : ErgodicVAdd G α μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → AddAction.aestabilizer G μ s = ⊤ → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.Probability.ProductMeasure
/-- If we push the product measure forward by a reindexing equivalence, we get a product measure
on the reindexed product.  -/
MeasureTheory.Measure.infinitePi_map_piCongrLeft : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {α : Type u_3} (e : α ≃ ι),
  MeasureTheory.Measure.map (⇑(MeasurableEquiv.piCongrLeft X e)) (MeasureTheory.Measure.infinitePi fun i => μ (e i)) =
    MeasureTheory.Measure.infinitePi μ
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- Taking a subset of the rows and columns reduces the rank.  -/
Matrix.rank_submatrix_le : ∀ {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R]
  [StrongRankCondition R] [inst_3 : Fintype n₀] (A : Matrix m n R) (r : m₀ → m) (c : n₀ → n),
  (A.submatrix r c).rank ≤ A.rank
-- Init.Data.List.Lemmas
List.mem_reverseAux : ∀ {α : Type u_1} {x : α} {as bs : List α}, x ∈ as.reverseAux bs ↔ x ∈ as ∨ x ∈ bs
-- Init.Data.Order.Classes
Std.IsPartialOrder.toIsPreorder : ∀ {α : Type u} {inst : LE α} [self : Std.IsPartialOrder α], Std.IsPreorder α
-- Mathlib.Computability.DFA
/-- A DFA is a set of states (`σ`), a transition function from state to state labelled by the
alphabet (`step`), a starting state (`start`) and a set of acceptance states (`accept`).  -/
DFA : Type u → Type v → Type (max u v)
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α},
  (m.insert a).isEmpty = false
-- Mathlib.Data.Finset.NAry
Finset.Nonempty.of_image₂_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
  (Finset.image₂ f s t).Nonempty → t.Nonempty
-- Mathlib.Algebra.GroupWithZero.Units.Basic
CommGroupWithZero.toDivisionCommMonoid : {G₀ : Type u_3} → [CommGroupWithZero G₀] → DivisionCommMonoid G₀
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_ofNat : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {n : ℕ} [inst_3 : n.AtLeastTwo], (OfNat.ofNat n).IsPositive
-- Lean.Elab.InfoTree.Types
/-- Context from the root of the `InfoTree` up to this node.
Note that the term information collected during elaboration may contain metavariables, and their
assignments are stored at `mctx`.
 -/
Lean.Elab.ContextInfo : Type
-- Mathlib.Data.ENNReal.Inv
ENNReal.coe_div : ∀ {r p : NNReal}, r ≠ 0 → ↑(p / r) = ↑p / ↑r
-- Mathlib.Topology.WithTopology
WithTopology.instDecidableLE : {X : Type u_1} → (t : TopologicalSpace X) → [inst : LE X] → [DecidableLE X] → DecidableLE (WithTopology X t)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_comp_measurePreserving : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β}
  {g : β → ε} {ν : MeasureTheory.Measure β},
  MeasureTheory.AEStronglyMeasurable g ν →
    MeasureTheory.MeasurePreserving f μ ν → MeasureTheory.eLpNorm (g ∘ f) p μ = MeasureTheory.eLpNorm g p ν
-- Lean.Elab.Command
Lean.Elab.Command.ModuleLinter.name : Lean.Elab.Command.ModuleLinter → Lean.Name
-- Mathlib.Algebra.Star.StarRingHom
/-- A *⋆-ring* equivalence is an equivalence preserving addition, multiplication, and the star
operation, which allows for considering both unital and non-unital equivalences with a single
structure.  -/
StarRingEquiv : (A : Type u_1) → (B : Type u_2) → [Add A] → [Add B] → [Mul A] → [Mul B] → [Star A] → [Star B] → Type (max u_1 u_2)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_smul_of_tower : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {α : Type u_3}
  [inst_3 : Monoid α] [inst_4 : MulAction α R] [IsScalarTower α R R] [SMulCommClass α R R] (c : α) (A : Matrix n n R),
  (c • A).det = c ^ Fintype.card n • A.det
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Push forward a `GroupWithZero` along a surjective function.
See note [reducible non-instances].  -/
Function.Surjective.groupWithZero : {G₀ : Type u_2} →
  {G₀' : Type u_4} →
    [inst : GroupWithZero G₀] →
      [inst_1 : Zero G₀'] →
        [inst_2 : Mul G₀'] →
          [inst_3 : One G₀'] →
            [inst_4 : Inv G₀'] →
              [inst_5 : Div G₀'] →
                [inst_6 : Pow G₀' ℕ] →
                  [inst_7 : Pow G₀' ℤ] →
                    0 ≠ 1 →
                      (f : G₀ → G₀') →
                        Function.Surjective f →
                          f 0 = 0 →
                            f 1 = 1 →
                              (∀ (x y : G₀), f (x * y) = f x * f y) →
                                (∀ (x : G₀), f x⁻¹ = (f x)⁻¹) →
                                  (∀ (x y : G₀), f (x / y) = f x / f y) →
                                    (∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n) →
                                      (∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n) → GroupWithZero G₀'
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHom₂RightUnitorInv : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f : a ⟶ b) →
        [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.rightUnitor f).inv
-- Mathlib.Algebra.Homology.Double
/-- If a complex shape `c : ComplexShape ι` has no loop,
then for any `X : C` and `j : ι`, the functor which sends `K : HomologicalComplex C c`
to `X ⟶ K.X j` is corepresentable.  -/
HomologicalComplex.evalCompCoyonedaCorepresentable : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {ι : Type u_2} →
          (c : ComplexShape ι) →
            [c.HasNoLoop] →
              (X : C) →
                (j : ι) →
                  ((HomologicalComplex.eval C c j).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).CorepresentableBy
                    (HomologicalComplex.evalCompCoyonedaCorepresentative c X j)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.orderTop_mul_of_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R},
  x.leadingCoeff * y.leadingCoeff ≠ 0 → (x * y).orderTop = x.orderTop + y.orderTop
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mrange_inr' : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mrange (AddMonoidHom.inr M N) = AddSubmonoid.comap (AddMonoidHom.fst M N) ⊥
-- Mathlib.NumberTheory.Divisors
Int.map_prodComm_divisorsAntidiag : ∀ {z : ℤ}, Finset.map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag = z.divisorsAntidiag
-- Mathlib.Data.Finsupp.Defs
Finsupp.nontrivial_of_nontrivial : ∀ (α : Type u_1) {M : Type u_4} [inst : Zero M] [h : Nontrivial (α →₀ M)], Nontrivial M
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addLeftCancelMonoid : {α : Type u} → [LeftCancelMonoid α] → AddLeftCancelMonoid (Additive α)
-- Mathlib.Data.Set.Operations
Set.rangeFactorization.eq_1 : ∀ {α : Type u} {ι : Sort u_1} (f : ι → α) (i : ι), Set.rangeFactorization f i = ⟨f i, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit G f g =
    CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit G f g
-- Mathlib.Data.PNat.Basic
PNat.natPred_monotone : Monotone PNat.natPred
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_ne_center : ∀ {c : ℂ} {R : ℝ}, R ≠ 0 → ∀ {θ : ℝ}, circleMap c R θ ≠ c
-- Mathlib.Data.Finset.Erase
Finset.erase_idem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, (s.erase a).erase a = s.erase a
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.instFunLike : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → FunLike (MeasureTheory.ProbabilityMeasure Ω) (Set Ω) NNReal
-- Mathlib.Algebra.Order.Field.Basic
one_div_le_one_div_of_neg_of_le : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b < 0 → a ≤ b → 1 / b ≤ 1 / a
-- Mathlib.Algebra.Lie.BaseChange
LieSubmodule.tmul_mem_baseChange_of_mem : ∀ {R : Type u_1} {A : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : CommRing A] [inst_8 : Algebra R A] {N : LieSubmodule R L M} (a : A) {m : M},
  m ∈ N → a ⊗ₜ[R] m ∈ LieSubmodule.baseChange A N
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_mul : ∀ {R : Type u} {a b : R} [inst : Semiring R], Polynomial.C (a * b) = Polynomial.C a * Polynomial.C b
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_eq_union : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
  Finset.uIcc a b = Finset.Icc a b ∪ Finset.Icc b a
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- There is a primitive additive character on `ZMod n` if the characteristic of the target
does not divide `n`  -/
AddChar.primitiveZModChar : (n : ℕ+) → (F' : Type v) → [inst : Field F'] → ↑↑n ≠ 0 → AddChar.PrimitiveAddChar (ZMod ↑n) F'
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.μ_natural_right_assoc : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) {Z : CategoryTheory.LocalizedMonoidal L W ε}
  (h :
    (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y₂) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X Y₂).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X Y₁).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))
        h)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
    CategoryTheory.SemiCartesianMonoidalCategory.toUnit X
-- Init.Data.Array.MinMax
Array.max?_replicate : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] {n : ℕ} {a : α},
  (Array.replicate n a).max? = if n = 0 then none else some a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] {W : C} {g h : CategoryTheory.Limits.image f ⟶ W}
  [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) g =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) h →
    g = h
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.homEquiv_symm_apply : ∀ {X Y : Type u} (f : X → Y), TypeCat.homEquiv.symm f = TypeCat.ofHom f
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.instInhabitedState : Inhabited Lean.Meta.Grind.AC.State
-- Mathlib.Topology.MetricSpace.Algebra
IsBoundedSMul.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β],
  (∀ (x : α) (y₁ y₂ : β), dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂) →
    (∀ (x₁ x₂ : α) (y : β), dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0) → IsBoundedSMul α β
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ι_leftInverse : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Function.LeftInverse ⇑ExteriorAlgebra.ιInv ⇑(ExteriorAlgebra.ι R)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.sup_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {f g : E →ₛₗ.[σ] F}
  (H : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) (x : ↥f.domain) (y : ↥g.domain)
  (z : ↥(f.domain ⊔ g.domain)), ↑x + ↑y = ↑z → ↑(f.sup g H) z = ↑f x + ↑g y
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.zero_apply : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (a : L),
  0 a = 0
-- Mathlib.Topology.Continuous
closure_image_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  Continuous f → closure (f '' closure s) = closure (f '' s)
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- The trivial group-with-zero hom is absorbing for composition.  -/
MonoidWithZeroHom.apply_one_apply_eq : ∀ {M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [inst : MulZeroOneClass M₀] [inst_1 : Nontrivial M₀]
  [inst_2 : NoZeroDivisors M₀] [inst_3 : MulZeroOneClass N₀] [inst_4 : MulZeroOneClass G₀]
  [inst_5 : DecidablePred fun x => x = 0] (f : N₀ →*₀ G₀) (x : M₀), f (1 x) = 1 x
-- Init.Data.Array.MinMax
Array.min_replicate : ∀ {α : Type u_1} [inst : Min α] [Std.MinEqOr α] {n : ℕ} {a : α} (h : Array.replicate n a ≠ #[]),
  (Array.replicate n a).min h = a
-- Mathlib.Data.EReal.Basic
EReal.natCast_lt_iff : ∀ {m n : ℕ}, ↑m < ↑n ↔ m < n
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- `IsEffective R S` is true for any faithfully flat `R`-algebra `S`.  -/
Algebra.IsEffective.of_faithfullyFlat : ∀ (R : Type u_3) [inst : CommRing R] (S : Type u_4) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Module.FaithfullyFlat R S], Algebra.IsEffective R S
-- Mathlib.Logic.Function.Basic
Function.RightInverse.leftInverse_of_surjective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α},
  Function.RightInverse f g → Function.Surjective f → Function.LeftInverse f g
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_roots_sub_C' : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R} {a : R},
  0 < p.degree → (p - Polynomial.C a).roots.card ≤ p.natDegree
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
/-- Pentagonal numbers $k(3k-1)/2$ for integer $k$.  -/
pentagonal : ℤ → ℕ
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.piEquivL_apply : ∀ (𝕜 : Type u_6) [inst : NormedField 𝕜] {E : Type u_7} {ι : Type u_8} (F : ι → Type u_9) [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : (i : ι) → AddCommGroup (F i)]
  [inst_5 : (i : ι) → Module 𝕜 (F i)] [inst_6 : (i : ι) → TopologicalSpace (F i)]
  [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] (𝔖 : Set (Set E))
  (T : (i : ι) → UniformConvergenceCLM (RingHom.id 𝕜) (F i) 𝔖) (e : E) (i : ι),
  ((UniformConvergenceCLM.piEquivL 𝕜 F 𝔖) T) e i = (T i) e
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).getKey! k = if t₂.contains k = true then default else t₁.getKey! k
-- Mathlib.Analysis.Convex.Function
ConvexOn.le_left_of_right_le'' : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {x y z : 𝕜} {s : Set 𝕜} {f : 𝕜 → β},
  ConvexOn 𝕜 s f → x ∈ s → z ∈ s → x ≤ y → y < z → f z ≤ f y → f y ≤ f x
-- Init.Data.SInt.Bitwise
ISize.ofBitVec_xor : ∀ (a b : BitVec System.Platform.numBits), ISize.ofBitVec (a ^^^ b) = ISize.ofBitVec a ^^^ ISize.ofBitVec b
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singletonAddHom_apply : ∀ {α : Type u_2} [inst : Add α] (a : α), Set.singletonAddHom a = {a}
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.mk_eq_mk_iff_crossProduct_eq_zero : ∀ {F : Type u_1} [inst : Field F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0),
  Projectivization.mk F v hv = Projectivization.mk F w hw ↔ (crossProduct v) w = 0
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The angle between three points is zero if and only if one of the first and third points is
weakly between the other two, and not equal to the second.  -/
EuclideanGeometry.angle_eq_zero_iff_ne_and_wbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = 0 ↔ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
-- Mathlib.Analysis.PSeries
/-- Harmonic series is not unconditionally summable.  -/
Real.not_summable_natCast_inv : ¬Summable fun n => (↑n)⁻¹
-- Init.Data.Int.Lemmas
Int.neg_mul_eq_neg_mul : ∀ (a b : ℤ), -(a * b) = -a * b
-- Mathlib.Data.Fintype.Basic
seqOfForallFinsetExistsAux.eq_def : ∀ {α : Type u_4} [inst : DecidableEq α] (P : α → Prop) (r : α → α → Prop)
  (h : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y) (x : ℕ),
  seqOfForallFinsetExistsAux P r h x =
    let n := x;
    Classical.choose ⋯
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Real.continuous_rpow_const : ∀ {q : ℝ}, 0 ≤ q → Continuous fun x => x ^ q