mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.addMonObj_add : ∀ {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] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.AddMonObj (F.obj X)],
  CategoryTheory.AddMonObj.add =
    hF.preimage
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.AddMonObj.add)
-- Mathlib.Order.SuccPred.Basic
Order.le_and_le_succ_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α},
  a ≤ b ∧ b ≤ Order.succ a ↔ b = a ∨ b = Order.succ a
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.left.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : SizeOf C] [inst_3 : SizeOf D] (a : C), sizeOf (CategoryTheory.Join.left a) = 1 + sizeOf a
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.restrict_compl_nullSet : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (h : μ.MutuallySingular ν),
  ν.restrict h.nullSetᶜ = 0
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instSemigroup : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : Semigroup M] → [ContinuousMul M] → Semigroup (SeparationQuotient M)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- The space of continuous affine maps from `P` to `Q` is an affine space over the space of
continuous affine maps from `P` to `W`.  -/
ContinuousAffineMap.instAddTorsor : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        {Q : Type u_5} →
          [inst : Ring R] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : Module R V] →
                [inst_3 : TopologicalSpace P] →
                  [inst_4 : AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [inst_6 : Module R W] →
                        [inst_7 : TopologicalSpace Q] →
                          [inst_8 : AddTorsor W Q] →
                            [inst_9 : TopologicalSpace W] →
                              [inst_10 : IsTopologicalAddGroup W] →
                                [IsTopologicalAddTorsor Q] → AddTorsor (P →ᴬ[R] W) (P →ᴬ[R] Q)
-- Std.Net.Addr
/-- The subnet mask associated with the interface.
 -/
Std.Net.InterfaceAddress.netMask : Std.Net.InterfaceAddress → Std.Net.IPAddr
-- Init.Data.String.PosRaw
String.Pos.Raw.ext_iff : ∀ {x y : String.Pos.Raw}, x = y ↔ x.byteIdx = y.byteIdx
-- Mathlib.Order.RelSeries
RelSeries.snoc_castSucc : ∀ {α : Type u_1} {r : SetRel α α} (s : RelSeries r) (a : α) (connect : (s.last, a) ∈ r) (i : Fin (s.length + 1)),
  (s.snoc a connect).toFun i.castSucc = s.toFun i
-- Mathlib.Algebra.ContinuedFractions.Translations
_private.Mathlib.Algebra.ContinuedFractions.Translations.0.GenContFract.contsAux.match_1.splitter : {K : Type u_1} →
  (motive : Option (GenContFract.Pair K) → Sort u_2) →
    (x : Option (GenContFract.Pair K)) →
      (Unit → motive none) → ((gp : GenContFract.Pair K) → motive (some gp)) → motive x
-- Mathlib.Data.List.MinMax
List.minimum_of_length_pos.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} (h : 0 < l.length),
  List.minimum_of_length_pos h = l.minimum.untop ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits, then `F : C ⥤ D` preserves limits.  -/
CategoryTheory.Limits.preservesLimitsOfSize_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Logic.Equiv.Defs
Equiv.existsUnique_subtype_congr : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : { a // p a } ≃ { b // q b }), (∃! a, p a) ↔ ∃! b, q b
-- Init.Sym.Lemmas
Lean.Sym.dite_true_congr : ∀ {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬c → α) (c' : Prop) (h : c = c') {ht : c'},
  dite c a b = a ⋯
-- Mathlib.Data.Sym.Sym2
Sym2.Rel.is_equivalence : ∀ {α : Type u_1}, Equivalence (Sym2.Rel α)
-- Lean.Environment
Lean.Kernel.Exception.unknownConstant : Lean.Kernel.Environment → Lean.Name → Lean.Kernel.Exception
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Config.mk.sizeOf_spec : ∀ (maxSuggestions : ℕ) (caller : Option String) (filter : Lean.Name → Lean.MetaM Bool) (hint : Option String),
  sizeOf { maxSuggestions := maxSuggestions, caller := caller, filter := filter, hint := hint } =
    1 + sizeOf maxSuggestions + sizeOf caller + sizeOf hint
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.mk₀_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y : C} [inst_3 : CategoryTheory.Preadditive C] (m₀ : M) (hm₀ : m₀ = 0)
  (f : X ⟶ Y), CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (-f) = -CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- The map `R ⧸ I →ₗ[R] R ⧸ (a • I)` defined by multiplication by `a` is injective if `a` is
a nonzero divisor.
 -/
Ideal.mulQuot_injective : ∀ {R : Type u_1} [inst : CommRing R] {a : R} (I : Ideal R),
  a ∈ nonZeroDivisors R → Function.Injective ⇑(Ideal.mulQuot a I)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) (X : C),
  CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG ⊤ = ⊤
-- Lean.Meta.Sym.InstantiateS
/-- Apply the given arguments to `f`, beta-reducing if `f` is a lambda expression,
ensuring maximally shared terms. See `betaRevS` for details.
 -/
Lean.Meta.Sym.betaS : Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ContinuousFunctionalCalculus.isCompact_spectrum : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A),
  IsCompact (spectrum R a)
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- The indexing category of the filtered colimit presentation  -/
CategoryTheory.Limits.IndObjectPresentation.ℐ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (self : CategoryTheory.Limits.IndObjectPresentation A) → CategoryTheory.SmallCategory self.I
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_pi_sub : ∀ (x : ℝ), Real.cos (Real.pi - x) = -Real.cos x
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.instSigmaFiniteElemRealIoiOfNatVolumeIoiPow : ∀ (n : ℕ), MeasureTheory.SigmaFinite (MeasureTheory.Measure.volumeIoiPow n)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.contains t.min! = true
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The algebra isomorphism between multivariable polynomials in a sum of two types,
and multivariable polynomials in one of the types,
with coefficients in multivariable polynomials in the other type.
 -/
MvPolynomial.sumAlgEquiv : (R : Type u) →
  (S₁ : Type v) →
    (S₂ : Type w) → [inst : CommSemiring R] → MvPolynomial (S₁ ⊕ S₂) R ≃ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.isOpen : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (U : OpenSubgroup G), IsOpen ↑U
-- Std.Time.Internal.Bounded
/-- Creates a new `Bounded` integer.
 -/
Std.Time.Internal.Bounded.LE.ofInt : {lo hi : ℤ} → ℤ → Option (Std.Time.Internal.Bounded.LE lo hi)
-- Init.Grind.Interactive
/-- `cbv` performs simplification that closely mimics call-by-value evaluation.
It reduces terms by unfolding definitions using their defining equations and
applying matcher equations. The unfolding is propositional, so `cbv` also works
with functions defined via well-founded recursion or partial fixpoints.

`cbv` reduces the goal target using call-by-value evaluation. For equation goals
(`lhs = rhs`), `cbv` automatically attempts `refl` after reduction to close the goal.

Unlike the standalone `cbv` tactic, this variant does not support the `at` location
syntax: in `sym =>` mode it only reduces the goal target.

`cbv` is not a finishing tactic in general: it may leave a new (simpler) goal.

The proofs produced by `cbv` only use the three standard axioms.
In particular, they do not require trust in the correctness of the code
generator.

This is a variant of `cbv` that only works in `sym =>` mode.
 -/
Lean.Parser.Tactic.Grind.symCbv : Lean.ParserDescr
-- Mathlib.Algebra.Regular.Prod
IsAddRegular.sumMk : ∀ {R : Type u_2} {S : Type u_3} [inst : Add R] [inst_1 : Add S] {a : R} {b : S},
  IsAddRegular a → IsAddRegular b → IsAddRegular (a, b)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.comp_fin3 : ∀ {R : Type r} {S : Type s} (f : R → S) (a b c : R), f ∘ ![a, b, c] = ![f a, f b, f c]
-- Mathlib.Order.Filter.Defs
/-- A filter is `NeBot` if it is not equal to `⊥`, or equivalently the empty set does not belong to
the filter. Bourbaki include this assumption in the definition of a filter but we prefer to have a
`CompleteLattice` structure on `Filter _`, so we use a typeclass argument in lemmas instead.  -/
Filter.NeBot : {α : Type u_1} → Filter α → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldrM_eq_foldrM_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ},
  Std.DTreeMap.Raw.foldrM f init t = List.foldrM (fun a b => f a.fst a.snd b) init t.toList
-- Lean.SubExpr
Lean.SubExpr.mk.injEq : ∀ (expr : Lean.Expr) (pos : Lean.SubExpr.Pos) (expr_1 : Lean.Expr) (pos_1 : Lean.SubExpr.Pos),
  ({ expr := expr, pos := pos } = { expr := expr_1, pos := pos_1 }) = (expr = expr_1 ∧ pos = pos_1)
-- Mathlib.CategoryTheory.Adjunction.Restrict
CategoryTheory.Adjunction.restrictFullyFaithful_homEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'}
  {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful)
  (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
  (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) {X : C} {Y : D} (f : L.obj X ⟶ Y),
  ((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y) f =
    hiC.preimage
      (CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X))
        (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X))
          (CategoryTheory.CategoryStruct.comp (R'.map (iD.map f)) (comm2.hom.app Y))))
-- Mathlib.Tactic.Lift
PiSubtype.canLift : ∀ (ι : Sort u_1) (α : ι → Sort u_2) [∀ (i : ι), Nonempty (α i)] (p : ι → Prop),
  CanLift ((i : Subtype p) → α ↑i) ((i : ι) → α i) (fun f i => f ↑i) fun x => True
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toArray_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → β → γ},
  (Std.TreeMap.Raw.map f t).toArray = Array.map (fun p => (p.1, f p.1 p.2)) t.toArray
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y : C} →
      {P : HomotopicalAlgebra.PrepathObject Y} →
        {X : C} →
          {f g : X ⟶ Y} →
            (h : X ⟶ P.P) →
              autoParam (CategoryTheory.CategoryStruct.comp h P.p₀ = f)
                  HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀._autoParam →
                autoParam (CategoryTheory.CategoryStruct.comp h P.p₁ = g)
                    HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁._autoParam →
                  P.RightHomotopy f g
-- Mathlib.Control.Monad.Cont
ContT.run_pure : ∀ {r : Type u} {m : Type u → Type v} {α : Type w} (a : α) (k : α → m r), (pure a).run k = k a
-- Std.Http.Server.Handler
/-- Called when an I/O or transport error occurs while processing a request (e.g. broken socket,
handler exception). This is a **notification only**: the connection will close regardless of
the handler's response. Use this for logging and metrics. The default implementation does nothing.
 -/
Std.Http.Server.Handler.onFailure : {σ : Type} → [self : Std.Http.Server.Handler σ] → σ → IO.Error → Std.Async.Async Unit
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The forgetful functor from `Mon C` to `C` is monoidal when `C` is monoidal.  -/
CategoryTheory.Mon.instMonoidalForget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.Mon.forget C).Monoidal
-- Mathlib.Data.List.Sort
List.sortedGE_mergeSort : ∀ {α : Type u_1} {l : List α} [inst : LinearOrder α], (l.mergeSort fun x1 x2 => decide (x1 ≥ x2)).SortedGE
-- Init.Data.Vector.Basic
Vector.forM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {n : ℕ} → [Monad m] → Vector α n → (α → m PUnit.{u_1 + 1}) → m PUnit.{u_1 + 1}
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- Substitution of power series into a power series.  -/
PowerSeries.subst : {R : Type u_2} →
  [inst : CommRing R] →
    {τ : Type u_3} →
      {S : Type u_4} → [inst_1 : CommRing S] → [Algebra R S] → MvPowerSeries τ S → PowerSeries R → MvPowerSeries τ S
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
/-- The map which sends a non degenerate simplex of a simplicial set to
the subcomplex it generates is an order embedding.  -/
SSet.orderEmbeddingN : (X : SSet) → X.N ↪o X.Subcomplex
-- Init.Omega.IntList
Lean.Omega.IntList.gcd.eq_1 : ∀ (xs : Lean.Omega.IntList), xs.gcd = List.foldr (fun x g => x.natAbs.gcd g) 0 xs
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsProperLinearSet.isLinearSet : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, IsProperLinearSet s → IsLinearSet s
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.val_preimage_orbit : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : ↥p),
  Subtype.val ⁻¹' MulAction.orbit R ↑m = MulAction.orbit R m
-- Init.Data.Fin.Basic
/-- The type `Fin 0` is uninhabited, so it can be used to derive any result whatsoever.

This is similar to `Empty.elim`. It can be thought of as a compiler-checked assertion that a code
path is unreachable, or a logical contradiction from which `False` and thus anything else could be
derived.
 -/
Fin.elim0 : {α : Sort u} → Fin 0 → α
-- Batteries.Recycling.RBTree.Basic
/-- A stream over the iterator.  -/
RBTree.RBMap.Values.toStream : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap.Values α β cmp → RBTree.RBMap.Values.Stream α β
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f)
  (X : ↑(F.obj b₀)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
      ((F.mapComp' f₀₁ f₁₃ f hf).inv.toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X))
      ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_neg : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M), ⇑(-D) = -⇑D
-- Lean.Declaration
Lean.ConstantInfo.recInfo.injEq : ∀ (val val_1 : Lean.RecursorVal), (Lean.ConstantInfo.recInfo val = Lean.ConstantInfo.recInfo val_1) = (val = val_1)
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.equivalenceLeftToRight_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : F.augmentedCechConerve ⟶ X),
  (CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G).right =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι (fun x => F.hom) 0)
      (G.right.app { len := 0 })
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddCommGroupContinuousMap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddCommGroup β]
  [inst_3 : IsTopologicalAddGroup β],
  ContinuousMap.instAddCommGroupContinuousMap =
    { toAddGroup := ContinuousMap.instAddGroupOfIsTopologicalAddGroup, add_comm := ⋯ }
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instT2Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], T2Space (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_ker : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R}, PointedCone.dual p ↑p.ker = ⊤
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- **Alias** of `CategoryTheory.Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamation`. -/
CategoryTheory.Presieve.extension_iff_amalgamation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w))
  (f : (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F)
  (g : CategoryTheory.shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).ι g = f ↔
    (↑(CategoryTheory.Presieve.shrinkFunctorHomEquiv f)).IsAmalgamation (CategoryTheory.shrinkYonedaEquiv g)
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.Semiconj.mapsTo_ptsOfPeriod : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {g : α → β},
  Function.Semiconj g fa fb → ∀ (n : ℕ), Set.MapsTo g (Function.ptsOfPeriod fa n) (Function.ptsOfPeriod fb n)
-- Mathlib.RingTheory.Support
/-- Given an exact sequence `0 → M → N → P → 0` of `R`-modules, `Supp N = Supp M ∪ Supp P`.  -/
Module.support_of_exact : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  {P : Type u_4} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup P] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    Function.Injective ⇑f → Function.Surjective ⇑g → Module.support R N = Module.support R M ∪ Module.support R P
-- Mathlib.Topology.Order
/-- If the codomain of a continuous injective function has discrete topology,
then so does the domain.

See also `Embedding.discreteTopology` for an important special case.  -/
DiscreteTopology.of_continuous_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [DiscreteTopology β]
  {f : α → β}, Continuous f → Function.Injective f → DiscreteTopology α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.simp : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (k₁ : ℤ)
  (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.simp_cert k₁ p₁ k₂ m₂ p₂ p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Batteries.Data.Vector.Basic
Vector.scanlM.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} [inst : Monad m] (f : β → α → m β) (as : Vector α n)
  (cur : β) (i : ℕ) (hi : i ≤ n) (acc : Vector β i),
  Vector.scanlM.loop f as cur i hi acc =
    if h_lt : i < n then do
      let next ← f cur as[i]
      Vector.scanlM.loop f as next (i + 1) ⋯ (acc.push cur)
    else pure (Vector.cast ⋯ (acc.push cur))
-- Init.Data.Range.Basic
Std.Legacy.Range.mk.inj : ∀ {start stop step : ℕ} {step_pos : 0 < step} {start_1 stop_1 step_1 : ℕ} {step_pos_1 : 0 < step_1},
  [start:stop:step] = [start_1:stop_1:step_1] → start = start_1 ∧ stop = stop_1 ∧ step = step_1
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.inseparable_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : OnePoint X},
  Inseparable x y ↔ x = OnePoint.infty ∧ y = OnePoint.infty ∨ ∃ x', x = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'
-- Init.Data.Array.Erase
Array.erase_append : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {xs ys : Array α},
  (xs ++ ys).erase a = if a ∈ xs then xs.erase a ++ ys else xs ++ ys.erase a
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `UniqueMul` is preserved by inverse images under injective, multiplicative maps.  -/
UniqueMul.mulHom_preimage : ∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] (f : G →ₙ* H) (hf : Function.Injective ⇑f) (a0 b0 : G)
  {A B : Finset H}, UniqueMul A B (f a0) (f b0) → UniqueMul (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the left, excluding the subtraction of that point from itself.  -/
vectorSpan_range_eq_span_range_vsub_left_ne : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i₀ : ι),
  vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p i₀ -ᵥ p ↑i)
-- Mathlib.Algebra.GroupWithZero.Opposite
AddOpposite.instNoZeroDivisors : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [NoZeroDivisors α], NoZeroDivisors αᵃᵒᵖ
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeQcPrecoverage : AlgebraicGeometry.Scheme.qcPrecoverage.IsStableUnderBaseChange
-- Mathlib.Data.Set.Semiring
Set.up_union : ∀ {α : Type u_1} (s t : Set α), Set.up (s ∪ t) = Set.up s + Set.up t