mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Algebra.TensorProduct.includeLeft.eq_1 : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CommSemiring S] [inst_6 : Algebra S A]
  [inst_7 : SMulCommClass R S A],
  Algebra.TensorProduct.includeLeft = { toRingHom := Algebra.TensorProduct.includeLeftRingHom, commutes' := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Affine
inner_vsub_right_eq_zero_symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {v : V} {a b : P},
  inner 𝕜 v (a -ᵥ b) = 0 ↔ inner 𝕜 v (b -ᵥ a) = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.self_le_maxKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {v : β}, (cmp k (t.insert k v).maxKey!).isLE = true
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.projr_mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K ⋊⁅ψ⁆ L),
  (LieAlgebra.SemiDirectSum.projr ψ) x = x.right
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
/-- If `-m < c`, then `(fun t : ℝ ↦ (t + m) ^ a)` is integrable on `(c, ∞)` for all `a < -1`.  -/
integrableOn_add_rpow_Ioi_of_lt : ∀ {a c m : ℝ}, a < -1 → -m < c → MeasureTheory.IntegrableOn (fun x => (x + m) ^ a) (Set.Ioi c) MeasureTheory.volume
-- Mathlib.Algebra.Module.Equiv.Basic
/-- `LinearEquiv.applyDistribMulAction` is faithful.  -/
LinearEquiv.apply_faithfulSMul : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  FaithfulSMul (M ≃ₗ[R] M) M
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 ≠ W'.negY Q * P 2 → P 1 ≠ W'.negY P
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.fdecl.injEq : ∀ (f : Lean.IR.FunId) (xs : Array Lean.IR.Param) (type : Lean.IR.IRType) (body : Lean.IR.FnBody)
  (info : Lean.IR.DeclInfo) (f_1 : Lean.IR.FunId) (xs_1 : Array Lean.IR.Param) (type_1 : Lean.IR.IRType)
  (body_1 : Lean.IR.FnBody) (info_1 : Lean.IR.DeclInfo),
  (Lean.IR.Decl.fdecl f xs type body info = Lean.IR.Decl.fdecl f_1 xs_1 type_1 body_1 info_1) =
    (f = f_1 ∧ xs = xs_1 ∧ type = type_1 ∧ body = body_1 ∧ info = info_1)
-- Mathlib.Data.Fintype.Inv
/-- Given a fintype `α` and a predicate `p`, associate to a proof that there is a unique element of
`α` satisfying `p` this unique element, as an element of `α`.  -/
Fintype.choose : {α : Type u_1} → [Fintype α] → (p : α → Prop) → [DecidablePred p] → (∃! a, p a) → α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_eq_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : LawfulBEq α] {a : α}
  {fallback : β}, Std.DHashMap.Const.getD m a fallback = m.getD a fallback
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_eq_head?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.minKey? = t.keys.head?
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.instDecidableEqDart : {V : Type u_2} → {G : SimpleGraph V} → [DecidableEq V] → DecidableEq G.Dart
-- Mathlib.Dynamics.FixedPoints.Basic
Function.IsFixedPt.apply : ∀ {α : Type u_1} {f : α → α} {x : α}, Function.IsFixedPt f x → Function.IsFixedPt f (f x)
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_bijective : ∀ {α : Type u_1}, Function.Bijective ⇑SymAlg.unsym
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.size_toArray : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.HasSize α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α], r.toArray.size = r.size
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.lift_le : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F : IntermediateField K L}
  (E : IntermediateField K ↥F), IntermediateField.lift E ≤ F
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_ext_iff : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} {f g : A ⟶ B},
  f = g ↔ Rep.Hom.hom f = Rep.Hom.hom g
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_minView : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced}
  {hr : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size},
  ⟨(Std.DTreeMap.Internal.Impl.minView k v l r hl hr hlr).k,
        (Std.DTreeMap.Internal.Impl.minView k v l r hl hr hlr).v⟩ ::
      (Std.DTreeMap.Internal.Impl.minView k v l r hl hr hlr).tree.impl.toListModel =
    l.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app : ∀ (X : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)),
  CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.unitIso.hom.app X = CategoryTheory.eqToHom ⋯
-- Init.Data.UInt.Lemmas
UInt16.ofNatClamp_eq_ofNat : ∀ n < UInt16.size, UInt16.ofNatClamp n = UInt16.ofNat n
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_notMem_ball : ∀ (c : ℂ) (R θ : ℝ), circleMap c R θ ∉ Metric.ball c R
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.mul_one : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : NonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : NonAssocSemiring B] [inst_6 : Module R B]
  [inst_7 : SMulCommClass R B B] [inst_8 : IsScalarTower R B B] (x : TensorProduct R A B),
  (Algebra.TensorProduct.mul x) (1 ⊗ₜ[R] 1) = x
-- Lean.Meta.Tactic.Assert
Lean.Meta.AssertAfterResult.mk.injEq : ∀ (fvarId : Lean.FVarId) (mvarId : Lean.MVarId) (subst : Lean.Meta.FVarSubst) (fvarId_1 : Lean.FVarId)
  (mvarId_1 : Lean.MVarId) (subst_1 : Lean.Meta.FVarSubst),
  ({ fvarId := fvarId, mvarId := mvarId, subst := subst } =
      { fvarId := fvarId_1, mvarId := mvarId_1, subst := subst_1 }) =
    (fvarId = fvarId_1 ∧ mvarId = mvarId_1 ∧ subst = subst_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ_three : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.Ψ 3 = Polynomial.C W.Ψ₃
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The **Wedderburn–Artin Theorem**: an Artinian simple ring is isomorphic to a matrix
ring over the opposite of the endomorphism ring of its simple module.  -/
IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite : ∀ (R : Type u) [inst : Ring R] [IsSimpleRing R] [IsArtinianRing R],
  ∃ n, ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalPi'_μ : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : (i : I) → CategoryTheory.Functor D (C i)) [inst_4 : (i : I) → (F i).Monoidal] (X Y : D) (i : I),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Functor.pi' F) X Y i =
    CategoryTheory.Functor.LaxMonoidal.μ (F i) X Y
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LVal.fieldIdx.injEq : ∀ (ref : Lean.Syntax) (i : ℕ) (levels : List Lean.Level) (ref_1 : Lean.Syntax) (i_1 : ℕ) (levels_1 : List Lean.Level),
  (Lean.Elab.Term.LVal.fieldIdx ref i levels = Lean.Elab.Term.LVal.fieldIdx ref_1 i_1 levels_1) =
    (ref = ref_1 ∧ i = i_1 ∧ levels = levels_1)
-- Mathlib.RingTheory.Derivation.DifferentialRing
DifferentialAlgebra.deriv_algebraMap : ∀ {A : Type u_1} {B : Type u_2} {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : Algebra A B}
  {inst_3 : Differential A} {inst_4 : Differential B} [self : DifferentialAlgebra A B] (a : A),
  ((algebraMap A B) a)′ = (algebraMap A B) a′
-- Mathlib.Order.Irreducible
SupIrred.eq_1 : ∀ {α : Type u_2} [inst : SemilatticeSup α] (a : α), SupIrred a = (¬IsMin a ∧ ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a)
-- Mathlib.Algebra.Group.End
AddAut.zero_def : ∀ (M : Type u_2) [inst : Add M], 0 = AddEquiv.refl M
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.nonDegenerate : ∀ {X : SSet} (self : X.N), self.simplex ∈ X.nonDegenerate self.dim
-- Mathlib.Algebra.Module.Lattice
/-- Any `R`-lattice in `ι → K` has `#ι` as `R`-rank.  -/
Submodule.IsLattice.rank_of_pi : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] [IsDomain R]
  [IsPrincipalIdealRing R] {ι : Type u_4} [inst_5 : Fintype ι] [IsFractionRing R K] (M : Submodule R (ι → K))
  [Submodule.IsLattice K M], Module.rank R ↥M = ↑(Fintype.card ι)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.continuous_postcomp : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : Zero X] [inst_1 : Zero Y] [inst_2 : Zero R]
  [inst_3 : TopologicalSpace X] [inst_4 : TopologicalSpace Y] [inst_5 : TopologicalSpace R] (g : ContinuousMapZero Y R),
  Continuous g.comp
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_inv_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G] {l : Filter α}
  {m : α → G} {a : G}, Filter.Tendsto (fun x => (m x)⁻¹) l (nhds a⁻¹) ↔ Filter.Tendsto m l (nhds a)
-- Lean.CoreM
Lean.Core.checkSystem : String → Lean.CoreM Unit
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedClosed₃OfIsTriangulated : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated], P.IsTriangulatedClosed₃
-- Mathlib.Topology.Compactness.Compact
/-- A set `s` is compact if for every family of closed sets whose intersection avoids `s`,
there exists a finite subfamily whose intersection avoids `s`.  -/
isCompact_of_finite_subfamily_closed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  (∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅) →
    IsCompact s
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- If `M` is nondegenerate and `v ≠ 0`, then there is some `w` such that `w * M * v ≠ 0`.  -/
Matrix.Nondegenerate.exists_not_ortho_of_ne_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Fintype n], M.Nondegenerate → ∀ {v : m → R}, v ≠ 0 → ∃ w, v ⬝ᵥ M.mulVec w ≠ 0
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_ceil_right_pure_add_one : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto Int.ceil (nhdsWithin (↑n) (Set.Ioi ↑n)) (pure (n + 1))
-- Init.Conv
/-- Expands let-declarations and let-variables.  -/
Lean.Parser.Tactic.Conv.zeta : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableWithinAt_fst : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set (M × M')} {x : M × M'},
  MDiffAt[s] Prod.fst x
-- Mathlib.Order.BoundedOrder.Basic
not_isMin_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] [Nontrivial α], ¬IsMin ⊤
-- Mathlib.Algebra.GroupWithZero.Torsion
IsMulTorsionFree.mk' : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsReduced M],
  (∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y) → IsMulTorsionFree M
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instInhabited : Inhabited CommMonCat
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_maxKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {fallback : α},
        Std.Internal.List.getKey? (Std.Internal.List.maxKeyD l fallback) l = some (Std.Internal.List.maxKeyD l fallback)
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorKerInv.eq_1 : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f : N →ₗ[R] P) [inst_11 : Module.Flat R M],
  LinearMap.tensorKerInv S M f =
    ((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker.subtype.codRestrictOfInjective
      ((TensorProduct.AlgebraTensorModule.lTensor S M) f.ker.subtype) ⋯ ⋯
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.nonempty_of_doubling : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G}, ↑(A * A).card < 3 / 2 * ↑A.card → A.Nonempty
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The (not necessarily limiting) `PushoutCocone f g` implicit in the statement
that we have `CommSq f g h i`.
 -/
CategoryTheory.CommSq.cocone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z : C} →
      {f : W ⟶ X} →
        {g : W ⟶ Y} →
          {h : X ⟶ Z} → {i : Y ⟶ Z} → CategoryTheory.CommSq f g h i → CategoryTheory.Limits.PushoutCocone f g
-- Init.Data.Fin.Lemmas
Fin.natAdd_subNat_cast : ∀ {n m : ℕ} {i : Fin (n + m)} (h : n ≤ ↑i), Fin.natAdd n (Fin.subNat n (Fin.cast ⋯ i) h) = i
-- Mathlib.RingTheory.LocalProperties.Exactness
surjective_of_isLocalization_of_span_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] {s : Set R},
  Ideal.span s = ⊤ →
    ∀ (Rᵣ : ↑s → Type u_3) [inst_2 : (r : ↑s) → CommSemiring (Rᵣ r)] [inst_3 : (r : ↑s) → Algebra R (Rᵣ r)]
      (Sᵣ : ↑s → Type u_4) [inst_4 : (r : ↑s) → CommSemiring (Sᵣ r)] [inst_5 : (r : ↑s) → Algebra S (Sᵣ r)]
      (f : R →+* S) [inst_6 : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)]
      [inst_7 : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)],
      (∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)) → Function.Surjective ⇑f
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneLeftOpOfCocone_π_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F) (X : Jᵒᵖ),
  (CategoryTheory.Limits.coneLeftOpOfCocone c).π.app X = (c.ι.app (Opposite.unop X)).unop
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanIdentifier : Lean.FromJson Lean.Lsp.LeanIdentifier
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.mem_singleton : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {a b : α}, a ∈ {b} ↔ a = b
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.compSL_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜 →+* 𝕜₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomIsometric σ₂₃]
  [inst_11 : RingHomIsometric σ₁₃] [inst_12 : RingHomIsometric σ₁₂] (f : F →SL[σ₂₃] G) (g : E →SL[σ₁₂] F),
  ((ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃) f) g = f ∘SL g
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (carrier : TopCat) → TopCat.Presheaf C carrier → AlgebraicGeometry.PresheafedSpace C
-- Mathlib.NumberTheory.Padics.PadicIntegers
nonunits.eq_1 : ∀ (α : Type u_4) [inst : Monoid α], nonunits α = {a | ¬IsUnit a}
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_univ₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  [inst_3 : Fintype β] {s : Finset α}, ¬s ⊆ 0 → s • Finset.univ = Finset.univ
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_eq_bot_of_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂}, Function.Injective ⇑f → f.ker = ⊥
-- Mathlib.Data.NNRat.Lemmas
/-- A version of `NNRat.mul_num` without division.  -/
NNRat.num_mul_num_eq_num_mul_gcd : ∀ (q₁ q₂ : ℚ≥0), q₁.num * q₂.num = (q₁ * q₂).num * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.emptyWithCapacity_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {c : ℕ},
  Std.Sat.AIG.RefVec.emptyWithCapacity c = Std.Sat.AIG.RefVec.empty
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instInhabited : {E : Type u_3} → [inst : AddGroup E] → [DecidableEq E] → Inhabited (AddGroupNorm E)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : (NumberField.RingOfIntegers K)ˣ},
  (NumberField.Units.logEmbedding K) (Additive.ofMul x) = 0 ↔ x ∈ NumberField.Units.torsion K
-- Init.Data.Nat.ToString
Nat.nine_eq_digitChar : ∀ {n : ℕ}, '9' = n.digitChar ↔ n = 9
-- Mathlib.Topology.Connected.Basic
/-- The image of a connected set is connected as well.  -/
IsConnected.image : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α},
  IsConnected s → ∀ (f : α → β), ContinuousOn f s → IsConnected (f '' s)
-- Mathlib.Order.Category.PartOrd
PartOrd.Iso.mk_hom : ∀ {α β : PartOrd} (e : ↑α ≃o ↑β), (PartOrd.Iso.mk e).hom = PartOrd.ofHom ↑e
-- Mathlib.Topology.MetricSpace.Bounded
/-- If a function is continuous within a set `s` at every point of a compact set `k`, then it is
bounded on some open neighborhood of `k` in `s`.  -/
Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {k s : Set β} {f : β → α},
  IsCompact k → (∀ x ∈ k, ContinuousWithinAt f s x) → ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.iterate_derivative_succ_at_0_eq_zero : ∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ),
  Polynomial.eval 0 ((⇑Polynomial.derivative)^[ν] (bernsteinPolynomial R n (ν + 1))) = 0
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.subspaceInhabited : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Inhabited (Projectivization.Subspace K V)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
RingCon.liftₐEquiv.eq_1 : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] (c : RingCon M),
  c.liftₐEquiv =
    { toFun := fun f => c.liftₐ ↑f ⋯, invFun := fun F => ⟨F.comp (RingCon.mkₐ R c), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.FG.biSup_finset : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_3} (s : Finset ι) (P : ι → AddSubmonoid M),
  (∀ i ∈ s, (P i).FG) → (⨆ i ∈ s, P i).FG
-- Init.Core
/-- `x ≈ y` is the distinguished equivalence relation of a setoid.  -/
Setoid.r : {α : Sort u} → [self : Setoid α] → α → α → Prop
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {X Y :
    CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory)
      (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))}
  (φ : X ⟶ Y) (x : CategoryTheory.WithInitial SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.inverse.map φ).app x =
    match x with
    | CategoryTheory.WithInitial.of x => φ.right.app x
    | CategoryTheory.WithInitial.star => φ.left
-- Mathlib.Algebra.Polynomial.Basic
/-- Expressing the product of two polynomials as a double sum.  -/
Polynomial.mul_eq_sum_sum : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p * q = ∑ i ∈ p.support, q.sum fun j a => (Polynomial.monomial (i + j)) (p.coeff i * a)
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
Commute.pow_dvd_pow_of_add_pow_eq_zero : ∀ {R : Type u_1} {x y : R} {n m p : ℕ} [inst : Ring R], n + m ≤ p + 1 → Commute x y → (x + y) ^ n = 0 → x ^ m ∣ y ^ p
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.cosPartialHomeomorph.eq_1 : Real.cosPartialHomeomorph =
  { toFun := Real.cos, invFun := Real.arccos, source := Set.Ioo 0 Real.pi, target := Set.Ioo (-1) 1,
    map_source' := Real.cosPartialHomeomorph._proof_2, map_target' := Real.cosPartialHomeomorph._proof_3,
    left_inv' := Real.cosPartialHomeomorph._proof_4, right_inv' := Real.cosPartialHomeomorph._proof_5,
    continuousOn_toFun := Real.cosPartialHomeomorph._proof_6, continuousOn_invFun := Real.cosPartialHomeomorph._proof_7,
    open_source := Real.cosPartialHomeomorph._proof_8, open_target := Real.sinPartialHomeomorph._proof_9 }
-- Mathlib.Order.UpperLower.Closure
UpperSet.sdiff_inf_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {t : Set α},
  t ⊆ ↑s → (∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) → s.sdiff t ⊓ upperClosure t = s
-- Mathlib.Order.PrimeIdeal
Order.Ideal.IsPrime.of_mem_or_mem : ∀ {P : Type u_1} [inst : SemilatticeInf P] {I : Order.Ideal P} [I.IsProper],
  (∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I) → I.IsPrime
-- Mathlib.Data.Nat.ModEq
Nat.modEq_modulus_add_iff : ∀ {n a b : ℕ}, a ≡ n + b [MOD n] ↔ a ≡ b [MOD n]
-- Init.Data.SInt.Lemmas
Int8.zero_div : ∀ {a : Int8}, 0 / a = 0
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.onBoundedFormula.eq_3 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (g : L →ᴸ L') (x l : ℕ) (_R : L.Relations l)
  (ts : Fin l → L.Term (α ⊕ Fin x)),
  g.onBoundedFormula (FirstOrder.Language.BoundedFormula.rel _R ts) = (g.onRelation _R).boundedFormula (g.onTerm ∘ ts)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.mk_eq_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1}, Metric.Snowflaking.mk = ⇑Metric.Snowflaking.toSnowflaking