mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.GroupWithZero
/-- If `G₀` is a group with zero with topology such that `x ↦ x⁻¹` is continuous at all nonzero
points. Then the coercion `G₀ˣ → G₀` is a topological embedding.  -/
Units.isEmbedding_val₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀],
  Topology.IsEmbedding Units.val
-- Mathlib.MeasureTheory.Measure.Map
MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} (e : α ≃ᵐ β),
  MeasureTheory.Measure.map (⇑e) μ = ν ↔ μ = MeasureTheory.Measure.map (⇑e.symm) ν
-- Mathlib.Combinatorics.Quiver.Cast
/-- Change the endpoints of an arrow using equalities.  -/
Quiver.Hom.cast : {U : Type u_1} → [inst : Quiver U] → {u v u' v' : U} → u = u' → v = v' → (u ⟶ v) → (u' ⟶ v')
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_pow_dvd : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M} {n : ℕ}, UniqueFactorizationMonoid.radical (a ^ n) ∣ UniqueFactorizationMonoid.radical a
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_naturality_left_square_iff : ∀ {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} (adj : F ⊣ G) {X' X : C} {Y Y' : D} (f : X' ⟶ X)
  (g : F.obj X ⟶ Y') (h : F.obj X' ⟶ Y) (k : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y') g) =
      CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y) h) (G.map k) ↔
    CategoryTheory.CategoryStruct.comp (F.map f) g = CategoryTheory.CategoryStruct.comp h k
-- Std.Http.Data.Status
Std.Http.Status.proxyAuthenticationRequired.sizeOf_spec : sizeOf Std.Http.Status.proxyAuthenticationRequired = 1
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- Data witnessing the fact that `f` has local property `P` at `x`  -/
Manifold.LocalPresentationAt : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_4} →
      {H : Type u_6} →
        {G : Type u_8} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 F G →
                            {M : Type u_10} →
                              {N : Type u_12} →
                                [inst : TopologicalSpace M] →
                                  [ChartedSpace H M] →
                                    [inst_8 : TopologicalSpace N] →
                                      [ChartedSpace G N] →
                                        WithTop ℕ∞ →
                                          (M → N) →
                                            M →
                                              ((M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop) →
                                                Type (max (max (max u_10 u_12) u_6) u_8)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.toQuaternion_ι : ∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R} (v : R × R),
  CliffordAlgebraQuaternion.toQuaternion ((CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) v) =
    { re := 0, imI := v.1, imJ := v.2, imK := 0 }
-- Std.Data.HashMap.Lemmas
Std.HashMap.get_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_eq_toIocDiv_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b c : α), toIocDiv hp a (b - c) = toIocDiv hp (a + c) b
-- Std.Tactic.Do.Syntax
/-- `mexact` is like `exact`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (Q : SPred σs) : Q ⊢ₛ Q := by
  mstart
  mintro HQ
  mexact HQ
```
 -/
Lean.Parser.Tactic.mexactError : Lean.ParserDescr
-- Mathlib.SetTheory.Cardinal.Defs
/-- The representative of the cardinal of a type is equivalent to the original type.  -/
Cardinal.outMkEquiv : {α : Type v} → Quotient.out (Cardinal.mk α) ≃ α
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_rco : ∀ {m n : ℤ} {i : ℕ}, (m...n).toList[i]? = if i < (n - m).toNat then some (m + ↑i) else none
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.map_id : ∀ {α : Type u_1} [inst : Preorder α], Topology.WithUpperSet.map OrderHom.id = ContinuousMap.id (Topology.WithUpperSet α)
-- Mathlib.Data.List.Cycle
Cycle.prev_next : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x ∈ s),
  s.prev hs (s.next hs x hx) ⋯ = x
-- Init.Data.List.Sublist
List.cons_prefix_cons : ∀ {α : Type u_1} {a : α} {l₁ : List α} {b : α} {l₂ : List α}, a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoid.End.instAddCommMonoid : {M : Type uM} → [inst : AddCommMonoid M] → AddCommMonoid (AddMonoid.End M)
-- Mathlib.RingTheory.HahnSeries.Cardinal
/-- The `κ`-bounded submonoid of Hahn series with less than `κ` terms.  -/
HahnSeries.cardSuppLTAddSubmonoid : (Γ : Type u_1) →
  (R : Type u_2) →
    (κ : Cardinal.{u_1}) →
      [inst : PartialOrder Γ] →
        [inst_1 : AddMonoid R] → [hκ : Fact (Cardinal.aleph0 ≤ κ)] → AddSubmonoid (HahnSeries Γ R)
-- Mathlib.Analysis.Asymptotics.Defs
/-- `f = O(g)` if and only if `∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖` for all sufficiently large `c`.  -/
Asymptotics.isBigO_iff_eventually : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, f =O[l] g' ↔ ∀ᶠ (c : ℝ) in Filter.atTop, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g' x‖
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.isZGroup : ∀ {G : Type u_1} {inst : Group G} [self : IsZGroup G] (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.toCycles_comp_homologyπ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] {Z : C} (h : S.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.toCycles (CategoryTheory.CategoryStruct.comp S.homologyπ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.sdiv.match_1.eq_3 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match true, false with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_3 ()
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertMany!_list_le : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {l : List (α × β)}, (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).size ≤ t.size + l.length
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- The typeclass associated with the structure `UniversallyEffectiveEquivalenceRelation`.  -/
CategoryTheory.IsUniversallyEffectiveEquivalenceRelation : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {R A : C} → (R ⟶ A) → (R ⟶ A) → Prop
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftEquiv'_unitIso : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (i j : A) (h : i + j = 0),
  (CategoryTheory.shiftEquiv' C i j h).unitIso = (CategoryTheory.shiftFunctorCompIsoId C i j h).symm
-- Lean.Message
Lean.instInhabitedMessageSeverity.default : Lean.MessageSeverity
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.isAddCommGroup : {R : Type u} → [inst : Ring R] → (self : ModuleCat R) → AddCommGroup ↑self
-- Mathlib.Topology.Constructions
Pi.induced_domRestrict : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] (S : Set ι),
  TopologicalSpace.induced S.domRestrict Pi.topologicalSpace = ⨅ i ∈ S, TopologicalSpace.induced (Function.eval i) (T i)
-- Std.Internal.Do.Order.PreservesSup
/-- Unit, free from the definition of `upperAdjoint`: `f x ⊑ b → x ⊑ upperAdjoint f b`. Needs only
`CompleteLattice`.  -/
Lean.Order.PreservesSup.le_upperAdjoint : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (f : α → α) {b x : α},
  Lean.Order.PartialOrder.rel (f x) b → Lean.Order.PartialOrder.rel x (Lean.Order.PreservesSup.upperAdjoint f b)
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Bornology α] →
      [inst_1 : Bornology β] →
        (toFun : α → β) → Filter.comap toFun (Bornology.cobounded β) ≤ Bornology.cobounded α → LocallyBoundedMap α β
-- Lean.Parser.Types
Lean.Parser.ParserState.mkErrorsAt : Lean.Parser.ParserState → List String → String.Pos.Raw → optParam (Option ℕ) none → Lean.Parser.ParserState
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version on a set.  -/
MDifferentiableOn.mpullbackWithin_vectorField_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} [inst_11 : IsManifold I 2 M]
  [inst_12 : IsManifold I' 2 M'] [CompleteSpace E],
  MDiff[t] (T% V) →
    ContMDiffOn I I' n f s →
      (∀ x ∈ s ∩ f ⁻¹' t, (mfderiv[s] f x).IsInvertible) →
        UniqueMDiff[s] → 2 ≤ n → MDiff[s ∩ f ⁻¹' t] fun x => ⟨x, VectorField.mpullbackWithin I I' f V s x⟩
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- An `n`-Freiman homomorphism preserves products of `n` elements.  -/
IsMulFreimanHom.map_prod_eq_map_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β},
  IsMulFreimanHom n A B f →
    ∀ ⦃s t : Multiset α⦄,
      (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
        (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
          s.card = n → t.card = n → s.prod = t.prod → (Multiset.map f s).prod = (Multiset.map f t).prod
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_pow : ∀ (a : UInt32) (n : ℕ), (a ^ n).toBitVec = a.toBitVec ^ n
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Array.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) (it' : Std.IterM m α)
  (out : α) (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Data.Nat.Bitwise
Nat.bitwise_zero : ∀ {f : Bool → Bool → Bool}, Nat.bitwise f 0 0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.induce_adj : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set V) (u v : V),
  (G'.induce s).Adj u v = (u ∈ s ∧ v ∈ s ∧ G'.Adj u v)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Under a dense continuous linear map, a submodule whose `TopologicalClosure` is `⊤` is sent to
another such submodule.  That is, the image of a dense set under a map with dense range is dense.
 -/
DenseRange.topologicalClosure_map_submodule : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : RingHomSurjective σ₁₂]
  [inst_9 : TopologicalSpace R₁] [inst_10 : TopologicalSpace R₂] [inst_11 : ContinuousSMul R₁ M₁]
  [inst_12 : ContinuousAdd M₁] [inst_13 : ContinuousSMul R₂ M₂] [inst_14 : ContinuousAdd M₂] {f : M₁ →SL[σ₁₂] M₂},
  DenseRange ⇑f → ∀ {s : Submodule R₁ M₁}, s.topologicalClosure = ⊤ → (Submodule.map (↑f) s).topologicalClosure = ⊤
-- Lean.Parser.Basic
/-- Recover from errors in `parser` using `handler` to consume input until a known-good state has appeared.
If `handler` fails itself, then no recovery is performed.

`handler` is run in the state immediately after the failure.

The interactions between <|> and `recover` are subtle, especially for syntactic
categories that admit user extension. Consider avoiding it in these cases.  -/
Lean.Parser.recover : Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser
-- Init.SimpLemmas
instIdempotentOpAnd : Std.IdempotentOp And
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeScientificLitVal?.decodeAfterDot : String → String.Pos.Raw → ℕ → ℕ → Option (ℕ × Bool × ℕ)
-- Init.Data.List.Sublist
List.dropLast_sublist : ∀ {α : Type u_1} (l : List α), l.dropLast.Sublist l
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- The `n`th coefficient of `p` when seen as a power series.  -/
FormalMultilinearSeries.coeff : {𝕜 : Type u} →
  {E : Type v} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → FormalMultilinearSeries 𝕜 𝕜 E → ℕ → E
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.egirth_bot : ∀ {α : Type u_1}, ⊥.egirth = ⊤
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_eq_sum_sdiff_singleton_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι},
  i ∈ s → ∀ (f : ι → M), ∑ x ∈ s, f x = ∑ x ∈ s \ {i}, f x + f i
-- Lean.Parser.Module
Lean.Parser.ModuleParserState.recovering : Lean.Parser.ModuleParserState → Bool
-- Mathlib.Order.Interval.Set.Defs
/-- `Ici a` is the left-closed right-infinite interval $[a, ∞)$.  -/
Set.Ici : {α : Type u_1} → [Preorder α] → α → Set α
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.algebraMap_mk : ∀ {α : Type u_1} {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring α]
  [inst_3 : Algebra R A] [inst_4 : Algebra A α] {S : Subalgebra R A} (a : A) (ha : a ∈ S),
  (algebraMap (↥S) α) ⟨a, ha⟩ = (algebraMap A α) a
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
HomotopicalAlgebra.LeftHomotopyRel.iff_map_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {H : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] (X Y : C) [HomotopicalAlgebra.IsCofibrant X]
  [HomotopicalAlgebra.IsFibrant Y] {f g : X ⟶ Y}, HomotopicalAlgebra.LeftHomotopyRel f g ↔ L.map f = L.map g
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.toRuleFilter : Aesop.Frontend.RuleConfig → Aesop.ElabM (Aesop.RuleSetNameFilter × Aesop.RuleFilter)
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.castNum.match_1.splitter : (motive : Num → Sort u_1) → (x : Num) → (Unit → motive Num.zero) → ((p : PosNum) → motive (Num.pos p)) → motive x
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- 7.6(b) from [axler2024].
See `ContinuousLinearMap.orthogonal_ker` for the infinite-dimensional version.  -/
LinearMap.orthogonal_ker : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  A.kerᗮ = (LinearMap.adjoint A).range
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeSingleton : {α : Type u} → (a : α) → Fintype ↑{a}
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.supermartingale_of_condExp_sub_nonneg_nat : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] [inst_3 : PartialOrder E]
  [IsOrderedAddMonoid E] [ClosedIciTopology E] [IsOrderedModule ℝ E] [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → E},
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (i : ℕ), 0 ≤ᵐ[μ] μ[f i - f (i + 1) | ↑𝒢 i]) → MeasureTheory.Supermartingale f 𝒢 μ
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.SheafedSpace.GlueData.f_open : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : AlgebraicGeometry.SheafedSpace.GlueData C)
  (i j : self.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (self.f i j)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.AddMon C),
  (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).hom = CategoryTheory.CategoryStruct.id F.X
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk_def : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ),
  (ClassGroup.mk K) I =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K (FractionRing R))) I)
-- Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
/-- If `f` is `n` times continuously differentiable at `x` within `s`, then the `n`th iterated Fréchet
derivative within `s` with respect to `𝕜` equals scalar restriction of the `n`th iterated Fréchet
derivative within `s` with respect to `𝕜'`.
 -/
ContDiffWithinAt.restrictScalars_iteratedFDerivWithin_eventuallyEq : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {x : E} {f : E → F} {n : ℕ}
  {s : Set E},
  ContDiffWithinAt 𝕜' (↑n) f s x →
    UniqueDiffOn 𝕜 s →
      x ∈ s →
        ContinuousMultilinearMap.restrictScalars 𝕜 ∘ iteratedFDerivWithin 𝕜' n f s =ᶠ[nhdsWithin x s]
          iteratedFDerivWithin 𝕜 n f s
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.le_orthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → as ≤ s.orthRadius p
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueue.entriesToMessageData : Aesop.UnsafeQueue → Array Lean.MessageData
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
/-- the map `limᵢ (Gᵢ ⊗ M) → (limᵢ Gᵢ) ⊗ M` induced by the family of maps `Gᵢ ⊗ M → (limᵢ Gᵢ) ⊗ M`
given by `gᵢ ⊗ m ↦ [gᵢ] ⊗ m`.
 -/
TensorProduct.fromDirectLimit : {R : Type u_1} →
  [inst : CommSemiring R] →
    {ι : Type u_2} →
      [inst_1 : DecidableEq ι] →
        [inst_2 : Preorder ι] →
          {G : ι → Type u_3} →
            [inst_3 : (i : ι) → AddCommMonoid (G i)] →
              [inst_4 : (i : ι) → Module R (G i)] →
                (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                  (M : Type u_4) →
                    [inst_5 : AddCommMonoid M] →
                      [inst_6 : Module R M] →
                        (Module.DirectLimit (fun x => TensorProduct R (G x) M) fun i j h =>
                            LinearMap.rTensor M (f i j h)) →ₗ[R]
                          TensorProduct R (Module.DirectLimit G f) M
-- Mathlib.Data.Set.Lattice.Image
Set.iUnion_iUnion_eq' : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → Set β},
  ⋃ x, ⋃ y, ⋃ (_ : f y = x), g x = ⋃ y, g (f y)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side.  -/
EuclideanGeometry.dist_div_tan_oangle_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → dist p₃ p₂ / (EuclideanGeometry.oangle p₃ p₁ p₂).tan = dist p₁ p₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.one_eq_zero_unsat_cert : Lean.Grind.CommRing.Poly → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Construct an isomorphism between categorical coproducts (indexed by the same type)
from a family of isomorphisms between the factors.
 -/
CategoryTheory.Limits.Sigma.mapIso : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : β → C} → [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape β C] → ((b : β) → f b ≅ g b) → (∐ f ≅ ∐ g)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.mk : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : Zero β] →
        [inst_2 : TopologicalSpace β] →
          (toContinuousMap : C(α, β)) →
            Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (nhds 0) → ZeroAtInftyContinuousMap α β
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- If a sequence of functions is uniformly Cauchy on a set, then the values at each point form
a Cauchy sequence.  -/
UniformCauchySeqOn.cauchy_map : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {x : α}
  {p : Filter ι} [hp : p.NeBot], UniformCauchySeqOn F p s → x ∈ s → Cauchy (Filter.map (fun i => F i x) p)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
/-- The subalgebra of `Matrix ι ι R` that consists of matrices that actually represent
endomorphisms on `M`.  -/
Matrix.isRepresentation : {ι : Type u_1} →
  [inst : Fintype ι] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        (R : Type u_3) →
          [inst_2 : CommRing R] → [Module R M] → (ι → M) → [inst_4 : DecidableEq ι] → Subalgebra R (Matrix ι ι R)
-- Lean.Language.Basic
Lean.Language.SnapshotLeaf.mk.injEq : ∀ (toSnapshot toSnapshot_1 : Lean.Language.Snapshot),
  ({ toSnapshot := toSnapshot } = { toSnapshot := toSnapshot_1 }) = (toSnapshot = toSnapshot_1)
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_23 : HAdd Std.Time.Minute.Offset Std.Time.Week.Offset Std.Time.Minute.Offset
-- Init.Data.Int.DivMod.Lemmas
Int.mul_bmod_right : ∀ (a : ℕ) (b : ℤ), (↑a * b).bmod a = 0
-- Lean.Elab.MatchAltView
Lean.Elab.Term.MatchAltView.lhs : {k : Lean.SyntaxNodeKinds} → Lean.Elab.Term.MatchAltView k → Lean.Syntax
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.enumOrd_isNormal_iff_isClosed : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → (Order.IsNormal (Ordinal.enumOrd s) ↔ IsClosed s)