mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k},
  (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ k ∉ m then some k else m.getKey? a
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. An integrable function is greater than its mean on a set of positive
measure.  -/
MeasureTheory.measure_average_le_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  μ ≠ 0 → MeasureTheory.Integrable f μ → 0 < μ {x | ⨍ (a : α), f a ∂μ ≤ f x}
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.toHomeomorph_toEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  h.toHomeomorph.toEquiv = h.toEquiv
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_vadd_ball : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ), (fun x => c +ᵥ x) ⁻¹' Metric.ball x r = Metric.ball (-c +ᵥ x) r
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.nnRat_ofNat_smul_2 : ∀ {n d : ℕ} {R : Type u_3} {A : Type u_4} [inst : Semifield R] [inst_1 : Semifield A] [inst_2 : Algebra R A] {a : A}
  [inst_3 : n.AtLeastTwo] [inst_4 : d.AtLeastTwo],
  (OfNat.ofNat n / OfNat.ofNat d) • a = OfNat.ofNat n / OfNat.ofNat d * a
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.pointReflection_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] (x y : P₁), (ContinuousAffineEquiv.pointReflection k x) y = (x -ᵥ y) +ᵥ x
-- Mathlib.Topology.UniformSpace.Closeds
UniformContinuous.sup_closeds : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  {f g : α → TopologicalSpace.Closeds β},
  UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x ⊔ g x
-- Mathlib.CategoryTheory.Filtered.FinallySmall
CategoryTheory.InitiallySmall.exists_of_isCofiltered : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C]
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.InitiallySmall C],
  ∃ D x, ∃ (_ : CategoryTheory.IsCofiltered D), ∃ F, F.Initial
-- Mathlib.Topology.Algebra.Monoid
/-- If a submonoid of an additive topological monoid is commutative, then so is its
topological closure.

See note [reducible non-instances].  -/
AddSubmonoid.addCommMonoidTopologicalClosure : {M : Type u_3} →
  [inst : TopologicalSpace M] →
    [inst_1 : AddMonoid M] →
      [inst_2 : SeparatelyContinuousAdd M] →
        [T2Space M] → (s : AddSubmonoid M) → (∀ (x y : ↥s), x + y = y + x) → AddCommMonoid ↥s.topologicalClosure
-- Lean.Server.References
/-- Whether the `private` flag is set on this import.  -/
Lean.Server.ModuleImport.isPrivate : Lean.Server.ModuleImport → Bool
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_nsmul : ∀ {R : Type u} [inst : Semiring R] (a : ℕ) (b : AddMonoidAlgebra R ℕ), { toFinsupp := a • b } = a • { toFinsupp := b }
-- Mathlib.Data.Nat.Bitwise
Nat.land_bit : ∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ), Nat.bit a m &&& Nat.bit b n = Nat.bit (a && b) (m &&& n)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.verify₃.eq_1 : ∀ (w x y : UInt8),
  ByteArray.utf8DecodeChar?.verify₃ w x y =
    if
        (ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
            ByteArray.utf8DecodeChar?.isInvalidContinuationByte y) =
          true then
      false
    else
      have r := ByteArray.utf8DecodeChar?.assemble₃Unchecked w x y;
      decide (2048 ≤ r ∧ (r < 55296 ∨ 57343 < r))
-- Mathlib.NumberTheory.Divisors
/-- This lemma justifies its existence from its utility in crystallographic root system theory.  -/
Int.mul_mem_zero_one_two_three_four_iff : ∀ {a b : ℤ},
  (a = 0 ↔ b = 0) →
    (a * b ∈ {0, 1, 2, 3, 4} ↔
      (a, b) ∈
        {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1),
          (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)})
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbit_eq_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a b : α},
  AddAction.orbit G a = AddAction.orbit G b ↔ a ∈ AddAction.orbit G b
-- Mathlib.Algebra.Module.Defs
/-- A module over a semiring automatically inherits a `MulActionWithZero` structure.  -/
Module.toMulActionWithZero : {R : Type u_5} → {M : Type u_6} → {x : Semiring R} → {x_1 : AddCommMonoid M} → [Module R M] → MulActionWithZero R M
-- Mathlib.Algebra.Group.Action.Units
Units.instMulAction.eq_1 : ∀ {M : Type u_3} {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α],
  Units.instMulAction = { toSMul := Units.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Init.Data.String.Defs
String.toByteArray_inj : ∀ {s t : String}, s.toByteArray = t.toByteArray ↔ s = t
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.instInhabited : (R : Type u_1) →
  [inst : NonAssocRing R] → [DecidableEq R] → [NoZeroDivisors R] → [Nontrivial R] → Inhabited (MulRingNorm R)
-- Mathlib.Algebra.Star.StarProjection
/-- `q - p` is a star projection iff `p * q = p`.  -/
IsStarProjection.sub_iff_mul_eq_left : ∀ {R : Type u_1} [inst : NonUnitalRing R] [inst_1 : StarRing R] [IsAddTorsionFree R] {p q : R},
  IsStarProjection p → IsStarProjection q → (IsStarProjection (q - p) ↔ p * q = p)
-- Mathlib.Data.Sym.Sym2
Sym2.diag_injective : ∀ {α : Type u_1}, Function.Injective Sym2.diag
-- Lean.Parser.Command
/-- `#show_deprecated_modules` displays all modules in the current environment that have been
marked with `deprecated_module`.
 -/
Lean.Parser.Command.showDeprecatedModules : Lean.Parser.Parser
-- Mathlib.Probability.Martingale.OptionalSampling
/-- The value of a martingale `f` at a stopping time `τ` bounded by `n` is the conditional
expectation of `f n` with respect to the σ-algebra generated by `τ`.  -/
MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range : ∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : TopologicalSpace ι]
  [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m}
  [MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι} [inst_8 : Nonempty ι],
  MeasureTheory.Martingale f ℱ μ →
    ∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n),
      (Set.range τ).Countable →
        ∀ [MeasureTheory.SigmaFinite (μ.trim ⋯)], MeasureTheory.stoppedValue f τ =ᵐ[μ] μ[f n | hτ.measurableSpace]
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instWeakEquivalenceMapFullSubcategoryι : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) [HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.WeakEquivalence (P.ι.map f)
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.linearOrder : LinearOrder ℚ
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.whiskerLeft_app : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {L' : CategoryTheory.Functor C₁ C₃}
  (w : CategoryTheory.TwoSquare T L R B) (α : L ⟶ L') (X : C₁),
  (w.whiskerLeft α).app X = CategoryTheory.CategoryStruct.comp (w.natTrans.app X) (B.map (α.app X))
-- Mathlib.Data.Finset.Sum
Finset.toLeft_disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, (s.disjSum t).toLeft = s
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- **Alias** of `SimpleGraph.IsTree.isAcyclic`.

---

A tree is acyclic.  -/
SimpleGraph.IsTree.IsAcyclic : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree → G.IsAcyclic
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- If a group satisfies the universal property of a free group with respect to a given type, then
it admits a free group basis based on this type. Here
the universal property is expressed as in `IsFreeGroup.unique_lift`.  -/
FreeGroupBasis.ofUniqueLift : {G : Type u} →
  [inst : Group G] →
    (X : Type u) →
      (of : X → G) →
        (∀ {H : Type u} [inst_1 : Group H] (f : X → H), ∃! F, ∀ (a : X), F (of a) = f a) → FreeGroupBasis X G
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instHasColimitOfModuleCatCompForget₂ContinuousLinearMapIdCarrierLinearMap : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {J : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_2} J] {F : CategoryTheory.Functor J (TopModuleCat R)}
  [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))],
  CategoryTheory.Limits.HasColimit F
-- Std.Do.WP.Sound
/-- Soundness lemma for `Except` without the equality hypothesis (deprecated).  -/
Std.Do.Except.of_wp : ∀ {ε α : Type} {prog : Except ε α} (P : Except ε α → Prop),
  (⊢ₛ (Std.Do.wp prog).apply (fun a => ⌜P (Except.ok a)⌝, fun e => ⌜P (Except.error e)⌝, PUnit.unit)) → P prog
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- A sheaf of modules is quasi-coherent if it is locally the cokernel of a
morphism between coproducts of copies of the sheaf of rings.  -/
SheafOfModules.IsQuasicoherent : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] → SheafOfModules R → Prop
-- Mathlib.Analysis.Normed.Group.Basic
norm_div_rev : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖a / b‖ = ‖b / a‖
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.height_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)),
  (s.map f.toAffineMap ⋯).height i = s.height i
-- Mathlib.Data.EReal.Operations
EReal.bot_lt_add_iff : ∀ {x y : EReal}, ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.instMulActionProjectiveSpecialLinearGroupForall : {K : Type u_1} →
  [inst : Field K] →
    {ι : Type u_3} →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] → MulAction (Matrix.ProjectiveSpecialLinearGroup ι K) (Projectivization K (ι → K))
-- Mathlib.Topology.Algebra.Group.Basic
AddSubgroup.connectedComponentOfZero.eq_1 : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G],
  AddSubgroup.connectedComponentOfZero G =
    { carrier := connectedComponent 0, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintOptions.mk : Lean.Lsp.WorkDoneProgressOptions → Option Bool → Lean.Lsp.InlayHintOptions
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_zero : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Zero α], (NonemptyInterval.toProd 0).2 = 0
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.dualPairing_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {W : Submodule R M}
  (φ : Module.Dual R M) (x : ↥W), (W.dualPairing (Submodule.Quotient.mk φ)) x = φ ↑x
-- Mathlib.Order.InitialSeg
PrincipalSeg.codRestrict_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : PrincipalSeg r s)
  (H : ∀ (a : α), f.toRelEmbedding a ∈ p) (H₂ : f.top ∈ p) (a : α),
  (PrincipalSeg.codRestrict p f H H₂).toRelEmbedding a = ⟨f.toRelEmbedding a, ⋯⟩
-- Mathlib.Data.Set.Function
Equiv.invOn : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α} {t : Set β}, Set.InvOn (⇑e) (⇑e.symm) t s
-- Init.Data.SInt.Lemmas
Int8.neg_ofInt : ∀ {n : ℤ}, -Int8.ofInt n = Int8.ofInt (-n)
-- Mathlib.Order.WithBot
/-- The image of a binary function `f : α → β → γ` as a function
`WithTop α → WithTop β → WithTop γ`.

Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.  -/
WithTop.map₂ : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → WithTop α → WithTop β → WithTop γ
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Equality of the composition of the unit and counit with the identity `F ⟶ FGF ⟶ F = 𝟙`  -/
CategoryTheory.Adjunction.left_triangle_components : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : F ⊣ G) (X : C),
  CategoryTheory.CategoryStruct.comp (F.map (self.unit.app X)) (self.counit.app (F.obj X)) =
    CategoryTheory.CategoryStruct.id (F.obj X)
-- Aesop.Tree.Check
Aesop.MVarClusterRef.checkInvariantsIfEnabled : Aesop.MVarClusterRef → Lean.Meta.SavedState → Lean.MetaM Unit
-- Mathlib.Logic.Equiv.Fin.Basic
finSumFinEquiv_symm_apply_natAdd : ∀ {m n : ℕ} (x : Fin n), finSumFinEquiv.symm (Fin.natAdd m x) = Sum.inr x
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.neg.injEq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (a a_1 : CommRingCat.Colimits.Prequotient F), (a.neg = a_1.neg) = (a = a_1)
-- Lean.Expr
/-- If the given expression is a sequence of
function applications `f a₁ .. aₙ`, return `f`.
Otherwise return the input expression.
 -/
Lean.Expr.getAppFn : Lean.Expr → Lean.Expr
-- Mathlib.Topology.Category.TopPair
/-- The first space of the pair  -/
TopPair.fst : {X : TopPair} → TopCat
-- Init.Data.Iterators.Consumers.Total
Std.Iter.Total.mk.sizeOf_spec : ∀ {α β : Type w} [inst : SizeOf α] [inst_1 : SizeOf β] (it : Std.Iter β), sizeOf { it := it } = 1 + sizeOf it
-- Mathlib.Order.BourbakiWitt
/-- The type of nonempty chains of an order  -/
NonemptyChain : (α : Type u_4) → [LE α] → Type u_4
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- Use the extended GCD algorithm to generate the `a` and `b` values
satisfying `gcd x y = x * a + y * b`.  -/
EuclideanDomain.xgcd : {R : Type u} → [EuclideanDomain R] → [DecidableEq R] → R → R → R × R
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- `IndepMatroid.ofBdd` constructs a `RankFinite` matroid.  -/
IndepMatroid.instRankFiniteMatroidOfBdd : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) (h_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n),
  (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.RankFinite
-- Init.Sym.Lemmas
Lean.Sym.Int8.eq_eq_true : ∀ (a b : Int8), decide (a = b) = true → (a = b) = True
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.instIsSplitEpiComp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z}
  [hf : CategoryTheory.IsSplitEpi f] [hg : CategoryTheory.IsSplitEpi g],
  CategoryTheory.IsSplitEpi (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.GradedMonoid
/-- A graded version of `CommMonoid`.  -/
GradedMonoid.GCommMonoid : {ι : Type u_1} → (ι → Type u_2) → [AddCommMonoid ι] → Type (max u_1 u_2)
-- Mathlib.Algebra.Quaternion
/-- Coercion `R → ℍ[R]`.  -/
Quaternion.coe : {R : Type u_3} → [inst : CommRing R] → R → Quaternion R
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_lt_iff_lt : ∀ {a b : ℤ} (ha₁ : Int64.minValue.toInt ≤ a) (ha₂ : a ≤ Int64.maxValue.toInt) (hb₁ : Int64.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int64.maxValue.toInt), Int64.ofIntLE a ha₁ ha₂ < Int64.ofIntLE b hb₁ hb₂ ↔ a < b
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Regular monomorphisms are preserved by isomorphisms in the arrow category.  -/
CategoryTheory.RegularMono.ofArrowIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y X' Y' : C} →
      {f : X ⟶ Y} →
        {g : X' ⟶ Y'} →
          (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) →
            CategoryTheory.RegularMono f → CategoryTheory.RegularMono g
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_target : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.symm.target = e.source
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.instCoeFunForallForallHomProp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → CoeFun (J.Cover X) fun x => ⦃Y : C⦄ → (Y ⟶ X) → Prop
-- Mathlib.FieldTheory.Finite.Extension
/-- Given a finite field `k` of characteristic `p`, we have a non-canonically chosen extension
of any given degree `n > 0`.  -/
FiniteField.Extension : (k : Type u_1) → [inst : Field k] → (p : ℕ) → [Fact (Nat.Prime p)] → [CharP k p] → ℕ → Type
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.derivWithin_lt_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f S y → derivWithin f S y < slope f x y
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_ΨSq_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [NoZeroDivisors R] {n : ℤ},
  ↑n ≠ 0 → (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) ≠ 0
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
Metric.finite_approx_of_totallyBounded : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  TotallyBounded s → ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.ball y ε
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsUniformGroup.cauchy_iff_tendsto : ∀ {G : Type u_4} [inst : Group G] [inst_1 : UniformSpace G] [IsUniformGroup G] (𝓕 : Filter G),
  Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun p => p.1 / p.2) (𝓕 ×ˢ 𝓕) (nhds 1)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G) (j : J) {Z : C}
  (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (s.ι.app j)
      (CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).hom h) =
    CategoryTheory.CategoryStruct.comp (w.hom.app j) (CategoryTheory.CategoryStruct.comp (t.ι.app j) h)
-- Mathlib.Algebra.Order.BigOperators.Group.List
/-- See also `List.le_sum_of_mem`.  -/
List.single_le_sum : ∀ {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : List M},
  (∀ x ∈ l, 0 ≤ x) → ∀ x ∈ l, x ≤ l.sum
-- Init.Control.Do
/-- Exit a computation by returning a value `r : ρ` early.  -/
EarlyReturnT.return : {ρ : Type u_1} → {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → ρ → EarlyReturnT ρ m α
-- Mathlib.LinearAlgebra.LinearPMap
Submodule.valFromGraph_mem : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) {a : E}
  (ha : a ∈ Submodule.map (LinearMap.fst R E F) g), (a, Submodule.valFromGraph hg ha) ∈ g
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualRestrict_def : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (W : Submodule R M), W.dualRestrict = W.subtype.dualMap
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Transform a word representing a free group element into a word representing its inverse.  -/
FreeGroup.invRev : {α : Type u} → List (α × Bool) → List (α × Bool)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.isSubordinate_single : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {x : ι → ℝ} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [inst : Fintype ι] (hJ : J ≤ I)
  (h : x ∈ BoxIntegral.Box.Icc I),
  (BoxIntegral.TaggedPrepartition.single I J hJ x h).IsSubordinate r ↔
    BoxIntegral.Box.Icc J ⊆ Metric.closedBall x ↑(r x)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.trunc_C_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n : σ →₀ ℕ) (a : R)
  (p : MvPowerSeries σ R),
  (MvPowerSeries.trunc R n) (MvPowerSeries.C a * p) = MvPolynomial.C a * (MvPowerSeries.trunc R n) p
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase!_eq_eraseₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} {t : Std.DTreeMap.Internal.Impl α β} (h : t.Balanced),
  Std.DTreeMap.Internal.Impl.erase! k t = Std.DTreeMap.Internal.Impl.eraseₘ k t h
-- Mathlib.Algebra.Group.AddChar
AddChar.toMonoidHomEquiv_symm_mul : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ φ : Multiplicative A →* M),
  AddChar.toMonoidHomEquiv.symm (ψ * φ) = AddChar.toMonoidHomEquiv.symm ψ + AddChar.toMonoidHomEquiv.symm φ
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_uSizeToBitVec : ∀ (n : USize), { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mem_top : ∀ {M : Type u_1} [inst : Mul M] (x : M), x ∈ ⊤
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
/-- If `B` is a faithfully-flat `A`-algebra, the lifting an ideal in `A` to `B` is injective.  -/
Ideal.map_injective_of_faithfullyFlat : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Module.FaithfullyFlat A B], Function.Injective (Ideal.map (algebraMap A B))
-- Init.Prelude
/-- Proves that `p` is decidable by supplying a proof of `¬p`  -/
Decidable.isFalse : {p : Prop} → ¬p → Decidable p
-- Mathlib.Data.Set.Pairwise.Basic
Set.Pairwise.mono : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, t ⊆ s → s.Pairwise r → t.Pairwise r
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- The composition of two localizers morphisms.  -/
CategoryTheory.LocalizerMorphism.comp : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {W₁ : CategoryTheory.MorphismProperty C₁} →
              {W₂ : CategoryTheory.MorphismProperty C₂} →
                {W₃ : CategoryTheory.MorphismProperty C₃} →
                  CategoryTheory.LocalizerMorphism W₁ W₂ →
                    CategoryTheory.LocalizerMorphism W₂ W₃ → CategoryTheory.LocalizerMorphism W₁ W₃