mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  [inst_9 : Module.Finite R L] [inst_10 : Module.Free R L] [Nontrivial R] (b : Module.Basis ι R L),
  φ.nilRank = (φ.polyCharpoly b).natTrailingDegree
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.comap_apply : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph W) (v : V), (SimpleGraph.Embedding.comap f G) v = f v
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_sub_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a - x) '' Set.Ioc b c = Set.Ico (a - c) (a - b)
-- Mathlib.Computability.EpsilonNFA
/-- `M.accepts` is the language of `x` such that there is an accept state in `M.eval x`.  -/
εNFA.accepts : {α : Type u} → {σ : Type v} → εNFA α σ → Language α
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.congr_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M ≃ₗ[R] N) (x : AdicCompletion I M),
  (AdicCompletion.congr I f) x = (AdicCompletion.map I ↑f) x
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isRightKanExtension_iff_postcomp₁ : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') [G.IsEquivalence] (e : L.comp G ≅ L') {F : CategoryTheory.Functor C H}
  {F' : CategoryTheory.Functor D' H} (α : L'.comp F' ⟶ F),
  F'.IsRightKanExtension α ↔
    (G.comp F').IsRightKanExtension
      (CategoryTheory.CategoryStruct.comp (L.associator G F').inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e.hom F') α))
-- Lean.Elab.Tactic.Simp
/-- Runs the given action.
If it throws a maxRecDepth exception (nested or not), run the loop checking.
If it does not throw, run the loop checking only if explicitly enabled.
 -/
Lean.Elab.Tactic.withLoopChecking : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadExcept Lean.Exception m] →
        [Lean.MonadRuntimeException m] → [MonadLiftT Lean.MetaM m] → Lean.Elab.Tactic.MkSimpContextResult → m α → m α
-- Mathlib.Geometry.Manifold.Notation
/-- `MDiff f` elaborates to `MDifferentiable I J f`,
trying to determine `I` and `J` from the local context.  -/
Manifold.termMDiff__ : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Hom
Algebra.instMulDistribMulActionAlgHomUnits : {R : Type u} →
  (A : Type v) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → MulDistribMulAction (A →ₐ[R] A) Aˣ
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.map_map : ∀ {ι : 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 ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] {C : Type u_6} {ψ : Type u_7}
  [inst_10 : CommRing C] [inst_11 : SetLike ψ C] [inst_12 : AddSubgroupClass ψ C] {𝒞 : ι → ψ} [inst_13 : GradedRing 𝒞]
  {f : 𝒜 →+*ᵍ ℬ} {g : ℬ →+*ᵍ 𝒞} {P : Submonoid A} {Q : Submonoid B} {R : Submonoid C} (hpq : P ≤ Submonoid.comap f Q)
  (hqr : Q ≤ Submonoid.comap g R) (x : HomogeneousLocalization 𝒜 P),
  (HomogeneousLocalization.map g hqr) ((HomogeneousLocalization.map f hpq) x) =
    (HomogeneousLocalization.map (g.comp f) ⋯) x
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.isCompact_preimage : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β} [inst_2 : TopologicalSpace β]
  {K : Set β}, HasCompactMulSupport f → Continuous f → IsClosed K → 1 ∉ K → IsCompact (f ⁻¹' K)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_smul_le : ∀ {R : Type u} [inst : Semiring R] {S : Type u_2} [inst_1 : SMulZeroClass S R] (a : S) (p : Polynomial R),
  (a • p).natDegree ≤ p.natDegree
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.zariskiPrecoverage_le_qcPrecoverage : AlgebraicGeometry.Scheme.zariskiPrecoverage ≤ AlgebraicGeometry.Scheme.qcPrecoverage
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.completion_obj_str : ∀ (V : SemiNormedGrp), (SemiNormedGrp.completion.obj V).str = NormedAddCommGroup.toSeminormedAddCommGroup
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffineAddEquiv_symm_apply : ∀ {F : Type u} [inst : Field F] (W : WeierstrassCurve.Projective F) [inst_1 : DecidableEq F] (a : W.toAffine.Point),
  (WeierstrassCurve.Projective.Point.toAffineAddEquiv W).symm a = WeierstrassCurve.Projective.Point.fromAffine a
-- Mathlib.Algebra.Homology.Bifunctor
/-- The inclusion of a summand of `(mapBifunctor K₁ K₂ F c).X j`.  -/
HomologicalComplex.ιMapBifunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            (K₁ : HomologicalComplex C₁ c₁) →
                              (K₂ : HomologicalComplex C₂ c₂) →
                                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  [inst_6 : F.PreservesZeroMorphisms] →
                                    [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                      (c : ComplexShape J) →
                                        [inst_8 : TotalComplexShape c₁ c₂ c] →
                                          [inst_9 : K₁.HasMapBifunctor K₂ F c] →
                                            [inst_10 : DecidableEq J] →
                                              (i₁ : I₁) →
                                                (i₂ : I₂) →
                                                  (j : J) →
                                                    c₁.π c₂ c (i₁, i₂) = j →
                                                      ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X j)
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.standard.inj : ∀ {backend : Lean.Name} {fn : String} {backend_1 : Lean.Name} {fn_1 : String},
  Lean.ExternEntry.standard backend fn = Lean.ExternEntry.standard backend_1 fn_1 → backend = backend_1 ∧ fn = fn_1
-- Mathlib.Topology.UniformSpace.Compact
lebesgue_number_lemma_nhds : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {U : α → Set α},
  IsCompact K → (∀ x ∈ K, U x ∈ nhds x) → ∃ V ∈ uniformity α, ∀ x ∈ K, ∃ y, UniformSpace.ball x V ⊆ U y
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.ins.eq_3 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : α) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α),
  RBTree.RBNode.ins cmp x (RBTree.RBNode.node RBTree.RBColor.black a y b) =
    match cmp x y with
    | Ordering.lt => (RBTree.RBNode.ins cmp x a).balance1 y b
    | Ordering.gt => a.balance2 y (RBTree.RBNode.ins cmp x b)
    | Ordering.eq => RBTree.RBNode.node RBTree.RBColor.black a x b
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.not_cliqueFree_iff_top_isContained : ∀ {α : Type u_1} {G : SimpleGraph α} (n : ℕ), ¬G.CliqueFree n ↔ (SimpleGraph.completeGraph (Fin n)).IsContained G
-- Mathlib.Data.Matrix.Mul
Matrix.mul_apply : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Fintype m] [inst_1 : Mul α]
  [inst_2 : AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i : l} {k : n}, (M * N) i k = ∑ j, M i j * N j k
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- If `f` preserves multiplication, then so does `lift f`.  -/
FreeAbelianGroup.liftMonoid : {α : Type u} → {R : Type u_2} → [inst : Monoid α] → [inst_1 : Ring R] → (α →* R) ≃ (FreeAbelianGroup α →+* R)
-- Mathlib.GroupTheory.Coset.Basic
eq_addCosets_of_normal : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), s.Normal → ∀ (g : α), g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s
-- Mathlib.Algebra.Lie.UniversalEnveloping
/-- See note [partially-applied ext lemmas].  -/
UniversalEnvelopingAlgebra.hom_ext : ∀ (R : Type u₁) {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u₃}
  [inst_3 : Ring A] [inst_4 : Algebra R A] {g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A},
  g₁.toLieHom.comp (UniversalEnvelopingAlgebra.ι R) = g₂.toLieHom.comp (UniversalEnvelopingAlgebra.ι R) → g₁ = g₂
-- Batteries.Data.List.Lemmas
List.replaceF_cons_of_none : ∀ {α : Type u_1} {a : α} {l : List α} (p : α → Option α), p a = none → List.replaceF p (a :: l) = a :: List.replaceF p l
-- Mathlib.Analysis.Seminorm
/-- A seminorm is continuous if `p.ball 0 r ∈ 𝓝 0` for *all* `r > 0`.
Over a `NontriviallyNormedField` it is actually enough to check that this is true
for *some* `r`, see `Seminorm.continuous`.  -/
Seminorm.continuous_of_forall : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] {p : Seminorm 𝕝 E},
  (∀ r > 0, p.ball 0 r ∈ nhds 0) → Continuous ⇑p
-- Mathlib.Algebra.Ring.ULift
ULift.down_intCast : ∀ {R : Type u} [inst : IntCast R] (n : ℤ), (↑n).down = ↑n
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.quot_add : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (x y : RingCat.Colimits.Prequotient F),
  Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) (x.add y) =
    (have this := Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x;
      this) +
      have this := Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) y;
      this
-- Mathlib.RingTheory.KrullDimension.Regular
ringKrullDim_le_ringKrullDim_add_card : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] {S : Finset R},
  ↑S ⊆ ↑(IsLocalRing.maximalIdeal R) → ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span ↑S) + ↑S.card
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContinuousLinearEquiv_toContinuousLinearMap : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ),
  ↑φ.toContinuousLinearEquiv = (↑φ).toContinuousLinearMap
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instSemiring : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Semiring β] → Semiring (MeasureTheory.SimpleFunc α β)
-- Mathlib.Order.BoundedOrder.Basic
OrderBot.toBot : {α : Type u} → {inst : LE α} → [self : OrderBot α] → Bot α
-- Mathlib.Algebra.Group.Basic
pow_sub : ∀ {G : Type u_3} [inst : Group G] (a : G) {m n : ℕ}, n ≤ m → a ^ (m - n) = a ^ m * (a ^ n)⁻¹
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.ofIso_p : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {Y : SSet} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B)
  (x : ↑P.II),
  (P.ofIso e hA).p ⟨(SSet.Subcomplex.N.orderIsoOfIso e hA).symm ↑x, ⋯⟩ =
    ⟨(SSet.Subcomplex.N.orderIsoOfIso e hA).symm ↑(P.p x), ⋯⟩
-- ProofWidgets.Data.Html
/-- Characters not allowed inside JSX plain text.  -/
ProofWidgets.Jsx.jsxTextForbidden : String
-- Mathlib.Algebra.Ring.NonZeroDivisors
le_nonZeroDivisorsLeft_iff_isLeftRegular : ∀ {R : Type u_1} [inst : Ring R] {S : Submonoid R}, S ≤ nonZeroDivisorsLeft R ↔ ∀ (s : ↥S), IsLeftRegular ↑s
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.below.ind : ∀ {F : Type u → Type v} [q : QPF F] {motive : (a a_1 : (QPF.P F).W) → QPF.Wequiv a a_1 → Prop} (a : (QPF.P F).A)
  (f f' : (QPF.P F).B a → (QPF.P F).W) (a_1 : ∀ (x : (QPF.P F).B a), QPF.Wequiv (f x) (f' x)),
  (∀ (x : (QPF.P F).B a), QPF.Wequiv.below ⋯) → (∀ (x : (QPF.P F).B a), motive (f x) (f' x) ⋯) → QPF.Wequiv.below ⋯
-- Mathlib.Tactic.Ring.Common
/-- The data associated to the normalization.  -/
Mathlib.Tactic.Ring.Common.Result.val : {u : Lean.Level} →
  {α : Q(Type u)} →
    {E : Q(«$α») → Type u_1} → {e : Q(«$α»)} → (self : Mathlib.Tactic.Ring.Common.Result E e) → E self.expr
-- Mathlib.Data.Finset.Sort
/-- Given a finset `s` of cardinality `k` in a linear order `α`, the map `orderEmbOfFin s h` is
the increasing bijection between `Fin k` and `s` as an order embedding into `α`. Here, `h` is a
proof that the cardinality of `s` is `k`. We use this instead of an embedding `Fin s.card ↪o α` to
avoid casting issues in further uses of this function.  -/
Finset.orderEmbOfFin : {α : Type u_1} → [inst : LinearOrder α] → (s : Finset α) → {k : ℕ} → s.card = k → Fin k ↪o α
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.expandNonAtomicDiscrs? : Lean.Syntax → Lean.Elab.TermElabM (Option Lean.Syntax)
-- Mathlib.Data.NNRat.Encodable
NNRat.instEncodable : Encodable ℚ≥0
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.comapEq.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {β γ : Type w} {f g : β → γ} (h : f = g),
  CategoryTheory.GradedObject.comapEq C h = CategoryTheory.GradedObject.comapEq C h
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- `sr i` has order 2.
 -/
DihedralGroup.orderOf_sr : ∀ {n : ℕ} (i : ZMod n), orderOf (DihedralGroup.sr i) = 2
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool} {k : α} {h : k ∈ Std.ExtHashSet.filter f m}, (Std.ExtHashSet.filter f m).get k h = m.get k ⋯
-- Mathlib.Algebra.Group.PUnit
PUnit.instInv_mathlib.eq_1 : PUnit.instInv_mathlib = { inv := fun x => PUnit.unit }
-- Mathlib.Data.Complex.Basic
Complex.ofRealHom_eq_coe : ∀ (r : ℝ), Complex.ofRealHom r = ↑r
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- Order equivalence between blocks in `X` containing a point `a`
and subgroups of `G` containing the stabilizer of `a` (Wielandt, th. 7.5)  -/
MulAction.block_stabilizerOrderIso : (G : Type u_1) →
  [inst : Group G] →
    {X : Type u_2} →
      [inst_1 : MulAction G X] →
        [htGX : MulAction.IsPretransitive G X] →
          (a : X) → { B // a ∈ B ∧ MulAction.IsBlock G B } ≃o ↑(Set.Ici (MulAction.stabilizer G a))
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.mk.injEq : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
  (toReducedWord : HNNExtension.NormalWord.ReducedWord G A B)
  (mem_set : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord.toList → g ∈ d.set u)
  (toReducedWord_1 : HNNExtension.NormalWord.ReducedWord G A B)
  (mem_set_1 : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord_1.toList → g ∈ d.set u),
  ({ toReducedWord := toReducedWord, mem_set := mem_set } =
      { toReducedWord := toReducedWord_1, mem_set := mem_set_1 }) =
    (toReducedWord = toReducedWord_1)
-- Mathlib.Data.Countable.Basic
instUncountableSigmaOfNonempty : ∀ {α : Type u} {π : α → Type w} [Nonempty α] [∀ (a : α), Uncountable (π a)], Uncountable (Sigma π)
-- Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} [T2Space M]
  [BoundarylessManifold I M],
  (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) → IsMIntegralCurve γ v → IsMIntegralCurve γ' v → γ t₀ = γ' t₀ → γ = γ'
-- Mathlib.Algebra.Group.Defs
zsmul_neg_coe_of_pos : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a : G) {n : ℕ}, 0 < n → -↑n • a = -(n • a)
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.whiskerOfCompIdIsoSelf_inv_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  (t : CategoryTheory.Bicategory.LeftExtension f g),
  t.whiskerOfCompIdIsoSelf.inv.right = (CategoryTheory.Bicategory.rightUnitor t.extension).inv
-- Mathlib.Order.InitialSeg
InitialSeg.coe_coe_fn : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : InitialSeg r s), ⇑f.toRelEmbedding = ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.mk_π_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X)
  (snd : W ⟶ Y) (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g),
  (CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app CategoryTheory.Limits.WalkingCospan.one =
    CategoryTheory.CategoryStruct.comp fst f
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.ne_zero_iff : ∀ {R : Type u_1} [inst : NonUnitalRing R] {p : RingSeminorm R}, p ≠ 0 ↔ ∃ x, p x ≠ 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.toArray.size = t.size
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_bot : ∀ {α : Type u_1} [Nontrivial α], ⊥.ediam = ⊤
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_mul : ∀ {a b : ℤ} {hab₁ : Int32.minValue.toInt ≤ a * b} {hab₂ : a * b ≤ Int32.maxValue.toInt},
  Int32.ofIntLE (a * b) hab₁ hab₂ = Int32.ofInt a * Int32.ofInt b
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- The canonical map from `P` to its sheafification.  -/
CategoryTheory.toSheafify : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            (P : CategoryTheory.Functor Cᵒᵖ D) → P ⟶ CategoryTheory.sheafify J P
-- Mathlib.Algebra.Order.Positive.Field
Positive.instCommGroupSubtypeLtOfNat : {K : Type u_1} → [inst : Field K] → [inst_1 : LinearOrder K] → [IsStrictOrderedRing K] → CommGroup { x // 0 < x }
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Circle integrability is invariant when functions change along discrete sets.  -/
CircleIntegrable.congr_codiscreteWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E},
  f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂ → CircleIntegrable f₁ c R → CircleIntegrable f₂ c R
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.Rel'.refl : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (x : X₁ ⊕ X₂), CategoryTheory.Limits.Types.Pushout.Rel' f g x x
-- Mathlib.FieldTheory.CardinalEmb
/-- Each embedding of `E⟮<i⟯` into `Ē` extend to `#(X i)` embeddings of `E⟮<i⁺⟯`.  -/
Field.Emb.Cardinal.succEquiv : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            [inst_3 : Algebra.IsAlgebraic F E] →
              (i : (Module.rank F E).ord.ToType) →
                (↥(IntermediateField.adjoin F
                        (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
                          Set.Iio (Order.succ i))) →ₐ[F]
                    AlgebraicClosure E) ≃
                  (↥(IntermediateField.adjoin F
                          (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
                            Set.Iio i)) →ₐ[F]
                      AlgebraicClosure E) ×
                    Field.Emb
                      ↥(IntermediateField.adjoin F
                          (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio i))
                      ↥(↥(IntermediateField.adjoin F
                              (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
                                Set.Iio
                                  i)))⟮(Field.Emb.Cardinal.wellOrderedBasis F E) (Field.Emb.Cardinal.leastExt F E i)⟯
-- Mathlib.Topology.Order.NhdsSet
Ioi_mem_nhdsSet_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  a ≤ b → Set.Ioi a ∈ nhdsSet (Set.Ioc b c)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk_neg : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddGroup (β i)] {s : Finset ι}
  {x : (i : ↑↑s) → β ↑i}, DFinsupp.mk s (-x) = -DFinsupp.mk s x
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isSymm_iff_flip : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsSymm ↔ LinearMap.BilinForm.flipHom B = B
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.isCompact_range : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β} [inst_2 : TopologicalSpace β],
  HasCompactMulSupport f → Continuous f → IsCompact (Set.range f)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.eq_of_eqOn_set_top : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {f g : R →ₙ+* S},
  Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
/-- If `‖f x‖ₑ ≤ c * ‖g x‖ₑ`, then `eLpNorm f p μ ≤ c * eLpNorm g p μ`.

This version allows `c = ∞`, but requires `g` to be a.e. strongly measurable.  -/
MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul'' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_6} [inst : TopologicalSpace ε']
  [inst_1 : ContinuousENorm ε'] {ε : Type u_7} [inst_2 : TopologicalSpace ε] [inst_3 : ESeminormedAddMonoid ε]
  {f : α → ε} {c : ENNReal} {g : α → ε'} (p : ENNReal),
  MeasureTheory.AEStronglyMeasurable g μ →
    (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ) → MeasureTheory.eLpNorm f p μ ≤ c * MeasureTheory.eLpNorm g p μ
-- Mathlib.Topology.Sheaves.PresheafOfFunctions
TopCat.presheafToTypes_map : ∀ (X : TopCat) {T : ↑X → Type u_1} {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} {i : U ⟶ V}
  {f : (fun X => X) ((X.presheafToTypes T).obj U)},
  (CategoryTheory.ConcreteCategory.hom ((X.presheafToTypes T).map i)) f = fun x => f (i.unop x)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzOnWith.eq_1 : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (K : NNReal) (f : α → β)
  (s : Set α), LipschitzOnWith K f s = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → edist (f x) (f y) ≤ ↑K * edist x y
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.simpTheorems : Lean.Elab.Tactic.ElabSimpArgResult → Array Lean.Meta.SimpTheorem