mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.isUniformEmbedding_singleton : ∀ {α : Type u_1} [inst : UniformSpace α], IsUniformEmbedding fun x => {x}
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Step.visit.sizeOf_spec : ∀ (e : Lean.Meta.Simp.Result), sizeOf (Lean.Meta.Simp.Step.visit e) = 1 + sizeOf e
-- Mathlib.Data.List.Flatten
/-- See also `head_head_eq_head_flatten`, which switches around the proof obligations.  -/
List.head_flatten_eq_head_head : ∀ {α : Type u_1} {l : List (List α)} (hl : l.flatten ≠ []) (hl' : l.head ⋯ ≠ []),
  l.flatten.head hl = (l.head ⋯).head hl'
-- Mathlib.Data.List.Cycle
Cycle.instDecidableNodup : {α : Type u_1} → [DecidableEq α] → {s : Cycle α} → Decidable s.Nodup
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_comap_le : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {S : AddSubsemigroup N} {f : M →ₙ+ N},
  AddSubsemigroup.map f (AddSubsemigroup.comap f S) ≤ S
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_inv_hom_id : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)),
  CategoryTheory.CategoryStruct.comp (h.isoMap φ hφ).inv (F.map φ) = CategoryTheory.CategoryStruct.id (F.obj j)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorObj.eq_2 : ∀ (n : AugmentedSimplexCategory), AugmentedSimplexCategory.tensorObj CategoryTheory.WithInitial.star n = n
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.congr : ∀ (A : Type u_2) [inst : Monoid A] [H1 : Finset.HasMulAntidiagonal A] [H2 : Finset.HasMulAntidiagonal A],
  Finset.HasMulAntidiagonal.mulAntidiagonal = Finset.HasMulAntidiagonal.mulAntidiagonal
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
/-- Given a family `X i` of topological space, this is a predicate
on maps `g : Y → Z` between topological spaces saying that for any
continuous map `f : X i → Y`, the composition `g ∘ f` is continuous.
We say that `g` is `X`-continuous.  -/
Topology.ContinuousGeneratedBy : {ι : Type t} →
  (X : ι → Type u) →
    [(i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} → [TopologicalSpace Y] → {Z : Type v'} → [TopologicalSpace Z] → (Y → Z) → Prop
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- Variation of `TensorProduct.exists_finite_submodule_left_of_setFinite` where `M` and `N` are
already submodules.  -/
TensorProduct.exists_finite_submodule_left_of_setFinite' : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N}
  (s : Set (TensorProduct R ↥M₁ ↥N₁)),
  s.Finite → ∃ M', ∃ (hM : M' ≤ M₁), Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.rTensor (↥N₁) (Submodule.inclusion hM)).range
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- **Alias** of `Submodule.isSymmetricProjection_projection_iff`. -/
Submodule.IsCompl.projection_isSymmetricProjection_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} (hUV : IsCompl U V), (U.projection V hUV).IsSymmetricProjection ↔ U ⟂ V
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.ofPermHomFun_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (σ τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)) (x : α),
  a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.nonDegenerateEquiv'_symm_apply_mem : ∀ {n d : ℕ} (S : ↑{S | S.card = d + 1}) (i : Fin (d + 1)), ↑(SSet.stdSimplex.nonDegenerateEquiv'.symm S) i ∈ ↑S
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgEquiv.toCoalgIso_inv : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module R Y] [inst_5 : Coalgebra R X] [inst_6 : Coalgebra R Y] (e : X ≃ₗc[R] Y),
  e.toCoalgIso.inv = CoalgCat.ofHom ↑e.symm
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsRefl.eq_iff : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsRefl → ∀ {x y : M₁}, (B x) y = 0 ↔ (B y) x = 0
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.instStarHomClass : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B], StarHomClass (A →⋆ₙₐ[R] B) A B
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.replaceEntry.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k), Std.Internal.List.replaceEntry k v [] = []
-- Lean.Server.Utils
/-- Converts an UTF-8-based `Lean.Syntax.Range` in `text` to an equivalent LSP UTF-16-based `Lsp.Range`
in `text`.
 -/
Lean.Syntax.Range.toLspRange : Lean.FileMap → Lean.Syntax.Range → Lean.Lsp.Range
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk_pow : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ℕ), ↑(a ^ n) = ↑a ^ n
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.parseLowerHex?.match_1.eq_1 : ∀ (motive : Option ℕ → Sort u_1) (d : ℕ) (h_1 : (d : ℕ) → motive (some d)) (h_2 : Unit → motive none),
  (match some d with
    | some d => h_1 d
    | none => h_2 ()) =
    h_1 d
-- Mathlib.Data.Set.Image
Set.image_preimage_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f '' f ⁻¹' s = s ↔ s ⊆ Set.range f
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeInv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} [inst_3 : H.IsEquivalence] (c : CategoryTheory.Limits.Cocone (F.comp H)),
  H.mapCoconeInv c = (CategoryTheory.Limits.Cocone.functorialityEquivalence F H.asEquivalence).inverse.obj c
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Pattern found so far.  -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.State.patterns : Lean.Meta.Grind.Collector.State✝ → Array Lean.Expr
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.congr_of_eventuallyEq : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E} {g : E → F},
  ContDiffPointwiseHolderAt k α f a → f =ᶠ[nhds a] g → ContDiffPointwiseHolderAt k α g a
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.upperBound?_least_ub : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} {ub : Option α} {x y : α}
  [Std.TransCmp cmp] [RBTree.RBNode.IsCut cmp cut],
  RBTree.RBNode.Ordered cmp t →
    (∀ {x : α}, ub = some x → RBTree.RBNode.All (fun x_1 => RBTree.RBNode.cmpLT cmp x_1 x) t) →
      RBTree.RBNode.upperBound? cut t ub = some x →
        y ∈ t → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
-- Mathlib.RingTheory.Localization.FractionRing
/-- The action of `G` on the fraction field `L` of `B` given by `IsFractionRing.mulSemiringAction`
is compatible with the embedding `B ⊆ L`.  -/
IsFractionRing.smulDistribClass : ∀ (G : Type u_10) (B : Type u_12) (L : Type u_14) [inst : Group G] [inst_1 : CommRing B]
  [inst_2 : MulSemiringAction G B] [inst_3 : Field L] [inst_4 : Algebra B L] [inst_5 : IsFractionRing B L],
  SMulDistribClass G B L
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Cycle.isCycle_formPerm : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (h : s.Nodup), s.Nontrivial → (s.formPerm h).IsCycle
-- Std.Time.Format.Modifier
/-- `OffsetZ` represents different offset formats based on the number of pattern letters (capital 'Z').
 -/
Std.Time.OffsetZ : Type
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stepAux.eq_4 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (x : σ) (x_1 : Turing.Tape Γ) (p : Γ → σ → Bool)
  (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.stepAux (Turing.TM1.Stmt.branch p q₁ q₂) x x_1 =
    bif p x_1.head x then Turing.TM1.stepAux q₁ x x_1 else Turing.TM1.stepAux q₂ x x_1
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.map_range : ∀ {R : Type u} {S : Type v} {T : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : NonUnitalNonAssocRing T] (g : S →ₙ+* T) (f : R →ₙ+* S), NonUnitalSubring.map g f.range = (g.comp f).range
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_cons_of_lt : ∀ {w n acc : ℕ} {x : BitVec w} {b : Bool}, w < n → (BitVec.cons b x).cpopNatRec n acc = b.toNat + x.cpopNatRec n acc
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.toSeminorm : {R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} → [inst_1 : Ring S] → [inst_2 : Algebra R S] → MulAlgebraNorm R S → Seminorm R S
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {ι : Type w}
  [Small.{v, w} ι] (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (AlgebraicGeometry.SheafedSpace C))
  [inst_3 : CategoryTheory.Limits.HasColimit F] (i : CategoryTheory.Discrete ι)
  [CategoryTheory.Limits.HasStrictTerminalObjects C],
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion (CategoryTheory.Limits.colimit.ι F i)
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.isVerdierLeftLocalizing_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty 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] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms],
  A.IsVerdierLeftLocalizing B ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y),
      A Y → B.trW s → ∃ Z s' a, A Z ∧ (A ⊓ B).trW s' ∧ CategoryTheory.CategoryStruct.comp a s = s'
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- **Alias** of `SimpleGraph.Walk.edges_takeUntil_subset_edges`. -/
SimpleGraph.Walk.edges_takeUntil_subset : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).edges ⊆ p.edges
-- Init.Data.String.Basic
String.Slice.Pos.le_cast_iff : ∀ {s t : String.Slice} {pos : t.Pos} {pos' : s.Pos} {h : s.copy = t.copy}, pos ≤ pos'.cast h ↔ pos.cast ⋯ ≤ pos'
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤),
  (∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) →
    ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N ⋯ ∘ₗ f n = f m
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : OpensMeasurableSpace E] (L₁ L₂ : StrongDual ℝ E),
  ‖((ProbabilityTheory.uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ
-- Mathlib.Tactic.Continuity
/-- `continuity` solves goals of the form `Continuous f` by applying lemmas tagged with the attribute
`@[continuity]`. If the goal is not solved after attempting all rules, `continuity` fails.

`fun_prop` is a (usually more powerful) alternative to `continuity`.

This tactic is extensible. Tagging lemmas with the `@[continuity]` attribute can allow `continuity`
to solve more goals.

* `continuity?` reports the proof script found by `continuity`.
 -/
tacticContinuity : Lean.ParserDescr
-- Mathlib.Util.Notation3
/-- A normal variable, delaborate its expression.  -/
Mathlib.Notation3.BoundValueType.normal : Mathlib.Notation3.BoundValueType
-- Mathlib.Algebra.Order.Group.Abs
min_abs_abs_le_abs_max : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] {a b : G}, min |a| |b| ≤ |max a b|
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Composition on the left by a (continuous) homomorphism of topological monoids, as a
`MonoidHom`. Similar to `MonoidHom.compLeft`.  -/
MonoidHom.compLeftContinuous : (α : Type u_1) →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {γ : Type u_3} →
          [inst_2 : Monoid β] →
            [inst_3 : ContinuousMul β] →
              [inst_4 : TopologicalSpace γ] →
                [inst_5 : Monoid γ] → [inst_6 : ContinuousMul γ] → (g : β →* γ) → Continuous ⇑g → C(α, β) →* C(α, γ)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.comp_add'_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] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y Z : C} (f : L.obj X ⟶ L.obj Y) (g₁ g₂ : L.obj Y ⟶ L.obj Z) {Z_1 : D}
  (h : L.obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add' W g₁ g₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.CategoryStruct.comp f g₁)
        (CategoryTheory.CategoryStruct.comp f g₂))
      h
-- Mathlib.Tactic.CrossRefAttribute
/-- The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or
uppercase letters.  -/
Mathlib.CrossRef.stacksTagParser : Lean.Parser.Parser
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
_private.Mathlib.Algebra.SkewMonoidAlgebra.Basic.0.SkewMonoidAlgebra.add.match_1.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (motive : SkewMonoidAlgebra k G → SkewMonoidAlgebra k G → Sort u_3)
  (a b : G →₀ k) (h_1 : (a b : G →₀ k) → motive { coeff := a } { coeff := b }),
  (match { coeff := a }, { coeff := b } with
    | { coeff := a }, { coeff := b } => h_1 a b) =
    h_1 a b
-- Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
ContinuousLinearMap.restrict.congr_simp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] (f f_1 : M₁ →SL[σ₁₂] M₂)
  (e_f : f = f_1) {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (h : ∀ x ∈ p, f x ∈ q), f.restrict h = f_1.restrict ⋯
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve : ∀ {X : AlgebraicGeometry.Scheme} {U : X.AffineZariskiSite} {S : CategoryTheory.Sieve U},
  S ∈ (AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology X) U ↔
    Ideal.span (AlgebraicGeometry.Scheme.AffineZariskiSite.sectionsOfPresieve S.arrows) = ⊤
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.instIsIsoMapAppUnitOfFaithfulOfFull : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Faithful] [R.Full] {X : C},
  CategoryTheory.IsIso (L.map (h.unit.app X))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.mk.injEq : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] (carrier : Set M)
  (vadd_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c +ᵥ x ∈ carrier) (carrier_1 : Set M)
  (vadd_mem'_1 : ∀ (c : R) {x : M}, x ∈ carrier_1 → c +ᵥ x ∈ carrier_1),
  ({ carrier := carrier, vadd_mem' := vadd_mem' } = { carrier := carrier_1, vadd_mem' := vadd_mem'_1 }) =
    (carrier = carrier_1)
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.one_le_extended_of_one_le : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  (I : FractionalIdeal M K), 1 ≤ I → 1 ≤ FractionalIdeal.extended L hf I
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.inhabited : (R : Type u) → Inhabited (Rack.PreEnvelGroup R)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- Auxiliary construction for `CliffordAlgebra.changeForm`  -/
CliffordAlgebra.changeFormAux : {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) → LinearMap.BilinForm R M → M →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.measurableSet_countableFiltration_countablePartitionSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (n : ℕ) (t : α),
  MeasurableSet (MeasurableSpace.countablePartitionSet n t)
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.nnnorm_toSpanSingleton : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (x : E), ‖ContinuousLinearMap.toSpanSingleton 𝕜 x‖₊ = ‖x‖₊
-- Mathlib.Analysis.Convex.Extreme
/-- **Alias** of `Convex.mem_extremePoints_iff_mem_sdiff_convexHull_sdiff`. -/
Convex.mem_extremePoints_iff_mem_diff_convexHull_diff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [DenselyOrdered 𝕜] [Module.IsTorsionFree 𝕜 E] {A : Set E} {x : E},
  Convex 𝕜 A → (x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜) (A \ {x}))
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.last.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x : ι) (x_3 : M x) (a : x_3 ≠ 1),
  (Monoid.CoprodI.NeWord.singleton x_3 a).last = x_3
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The additive homomorphism from `R` to `AddOreLocalization R S`,
mapping `r : R` to the difference `r -ₒ 0`.  -/
AddOreLocalization.numeratorHom : {R : Type u_1} →
  [inst : AddMonoid R] → {S : AddSubmonoid R} → [inst_1 : AddOreLocalization.AddOreSet S] → R →+ AddOreLocalization S R
-- Mathlib.Algebra.Lie.Nilpotent
LieAlgebra.center_le_maxNilpotentIdeal : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.center R L ≤ LieAlgebra.maxNilpotentIdeal R L
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.pos : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → 0 < c
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.borel_le_measurable : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R]
  [SecondCountableTopology R], borel R ≤ f.outer.caratheodory
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_right_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] (d : D) {c c' : C}
  (f : c ⟶ c') {Z : D'} (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f) h)
-- Mathlib.Topology.Order.DenselyOrdered
Icc_mem_nhds_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] [NoMaxOrder α] {a b x : α}, Set.Icc a b ∈ nhds x ↔ x ∈ Set.Ioo a b
-- Lean.CoreM
Lean.Core.instMonadWithOptionsCoreM : Lean.MonadWithOptions Lean.CoreM
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α} {v : β},
  (t.insertIfNew k v).getKey? a = if cmp k a = Ordering.eq ∧ k ∉ t then some k else t.getKey? a
-- Init.While
_private.Init.While.0.repeatM_eq : ∀ {α : Type u} {m : Type u → Type v} [inst : Monad m] {β : Type u} [inst_1 : Nonempty β] {f : α → m (α ⊕ β)} (a : α),
  (∃ g, repeatM.body f g = g) → repeatM f a = repeatM.body f (repeatM f) a
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.instIsLocalHomResidueFieldRingHomResidue : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R], IsLocalHom (IsLocalRing.residue R)
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.of_add_mul_left_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsRelPrime x (y + x * z) → IsRelPrime x y
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.op_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G), (CategoryTheory.NatIso.op α).inv = CategoryTheory.NatTrans.op α.inv
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.insertIdxTR.eq_1 : ∀ {α : Type u_1} (l : List α) (n : ℕ) (a : α), l.insertIdxTR n a = List.insertIdxTR.go✝ a n l #[]
-- Mathlib.Algebra.Algebra.Basic
Algebra.algebraMapSubmonoid.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_4) [inst_1 : Semiring S] [inst_2 : Algebra R S] (M : Submonoid R),
  Algebra.algebraMapSubmonoid S M = Submonoid.map (algebraMap R S) M
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_sPolynomial_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
  m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.iSup_lt_ord_lift_of_isRegular : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {c : Cardinal.{max u v}},
  c.IsRegular → Cardinal.lift.{v, u} (Cardinal.mk ι) < c → (∀ (i : ι), f i < c.ord) → iSup f < c.ord
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.CorePlotsOn.isPlotOn_congr : ∀ {X : Type u_1} (self : DiffeologicalSpace.CorePlotsOn X) {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u)
  {p q : EuclideanSpace ℝ (Fin n) → X}, Set.EqOn p q u → (self.isPlotOn hu p ↔ self.isPlotOn hu q)
-- Mathlib.Data.Nat.Fib.Basic
/-- **Alias** of `Nat.isDvdSequence_fib`. -/
Nat.fib_dvd : IsDvdSequence Nat.fib
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.isSymm_ball : ∀ {X : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : Zero R] [inst_2 : Preorder R] (d : PseudoMetric X R) {ε : R},
  SetRel.IsSymm {xy | d xy.1 xy.2 < ε}