mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Algebra.finite_adjoin_of_finite_of_isIntegral : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {s : Set A},
  s.Finite → (∀ x ∈ s, IsIntegral R x) → Module.Finite R ↥(Algebra.adjoin R s)
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalateGo_append : ∀ {s t u : String} {l : List String}, String.intercalate.go✝ (s ++ t) u l = s ++ String.intercalate.go✝ t u l
-- Lean.Parser.Basic
Lean.Parser.sepBy1NoAntiquot : Lean.Parser.Parser → Lean.Parser.Parser → optParam Bool false → Lean.Parser.Parser
-- Mathlib.GroupTheory.OrderOfElement
orderOf_abs_ne_one : ∀ {G : Type u_1} [inst : Ring G] [inst_1 : LinearOrder G] [IsStrictOrderedRing G] {x : G}, |x| ≠ 1 → orderOf x = 0
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_subtypeDomain_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {v : Π₀ (i : ι), β i} {p : ι → Prop}
  [inst_4 : DecidablePred p] {h : (i : ι) → β i → γ},
  (∀ x ∈ v.support, p x) → ((DFinsupp.subtypeDomain p v).prod fun i b => h (↑i) b) = v.prod h
-- Mathlib.NumberTheory.NumberField.House
/-- `c₂` is the product of the maximum of `1` and `c`, and `supOfBasis`.  -/
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c₂ : (K : Type u_1) → [inst : Field K] → [NumberField K] → [DecidableEq (K →+* ℂ)] → ℝ
-- Mathlib.Order.Heyting.Hom
BiheytingHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β]
  [inst_2 : BiheytingAlgebra γ] {f₁ f₂ : BiheytingHom α β} {g : BiheytingHom β γ},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Topology.Irreducible
nonempty_preirreducible_inter : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [PreirreducibleSpace X],
  IsOpen s → IsOpen t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty
-- Batteries.Control.ForInStep.Lemmas
ForInStep.bind_yield : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (a : α) (f : α → m (ForInStep α)),
  (ForInStep.yield a).bind f = f a
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertList_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      ∀ (contains : Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true)
        (not_contains : Std.Internal.List.containsKey k l = false),
        Std.Internal.List.getKey k (Std.Internal.List.insertList l toInsert) contains =
          Std.Internal.List.getKey k toInsert ⋯
-- Mathlib.Topology.Algebra.Ring.Basic
Subsemiring.topologicalSemiring : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [IsTopologicalSemiring R] (S : Subsemiring R),
  IsTopologicalSemiring ↥S
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar : ∀ (n : ℕ) [inst : NeZero n], Function.Surjective (⇑(rootsOfUnityCircleEquiv n) ∘ ⇑(ZMod.rootsOfUnityAddChar n))
-- Init.Core
/-- Stores an already-computed value in a thunk.

Because the value has already been computed, there is no laziness.
 -/
Thunk.pure : {α : Type u_1} → α → Thunk α
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_le_card_height : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : CommSemiring R]
  [StrongRankCondition R] (A : Matrix m n R), A.rank ≤ Fintype.card m
-- Lean.Environment
Lean.ConstantInfo.instantiateTypeLevelParams : Lean.ConstantInfo → List Lean.Level → Lean.Expr
-- Init.Data.List.Lemmas
List.replicate_one : ∀ {α : Type u_1} {a : α}, List.replicate 1 a = [a]
-- Mathlib.Algebra.Order.Kleene
KleeneAlgebra.mul_kstar_le_kstar : ∀ {α : Type u_5} [self : KleeneAlgebra α] (a : α), a * KStar.kstar a ≤ KStar.kstar a
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.commute_mulLeft_right : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] (a b : A),
  Commute (LinearMap.mulLeft R a) (LinearMap.mulRight R b)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  {inst_1 : CategoryTheory.Category.{v', u'} J} {X : C}
  {toColimitPresentation : CategoryTheory.Limits.ColimitPresentation J X}
  {prop_diag_obj : ∀ (j : J), P (toColimitPresentation.diag.obj j)}
  {toColimitPresentation_1 : CategoryTheory.Limits.ColimitPresentation J X}
  {prop_diag_obj_1 : ∀ (j : J), P (toColimitPresentation_1.diag.obj j)},
  { toColimitPresentation := toColimitPresentation, prop_diag_obj := prop_diag_obj } =
      { toColimitPresentation := toColimitPresentation_1, prop_diag_obj := prop_diag_obj_1 } →
    toColimitPresentation = toColimitPresentation_1
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Slot.mk.injEq : ∀ {α : Type} (value : Option α) (pos remaining : ℕ) (value_1 : Option α) (pos_1 remaining_1 : ℕ),
  ({ value := value, pos := pos, remaining := remaining } =
      { value := value_1, pos := pos_1, remaining := remaining_1 }) =
    (value = value_1 ∧ pos = pos_1 ∧ remaining = remaining_1)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] (f : MeasureTheory.SimpleFunc α β)
  {s : Set α}, MeasurableSet s → ∀ {t : Set β}, 0 ∉ t → ⇑(f.restrict s) ⁻¹' t = s ∩ ⇑f ⁻¹' t
-- Mathlib.Analysis.Normed.Module.Completion
UniformSpace.Completion.instNormedSpace : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [NormedSpace 𝕜 E] → NormedSpace 𝕜 (UniformSpace.Completion E)
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.locallyLipschitzOn_iff_continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ},
  IsOpen C → ConcaveOn ℝ C f → (LocallyLipschitzOn C f ↔ ContinuousOn f C)
-- Lean.Parser.Basic
Lean.Parser.PrattParsingTables : Type
-- Mathlib.Data.Fintype.EquivFin
Finset.card_eq_of_equiv : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : ↥s ≃ ↥t), s.card = t.card
-- Mathlib.Data.Finmap
Finmap.keys_val : ∀ {α : Type u} {β : α → Type v} (s : AList β), s.toFinmap.keys.val = ↑s.keys
-- Mathlib.Data.Num.Basic
/-- Auxiliary definition for a `sqrt` function which is not currently implemented.  -/
_private.Mathlib.Data.Num.Basic.0.PosNum.sqrtAux : PosNum → Num → Num → Num
-- Mathlib.ModelTheory.Definability
Set.definableFun_iff_empty_definableFun_with_params : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M},
  Set.DefinableFun L A f ↔ Set.DefinableFun (L.withConstants ↑A) ∅ f
-- Init.Data.Order.Lemmas
Std.min_eq_or : ∀ {α : Type u} [inst : Min α] [Std.MinEqOr α] {a b : α}, a ⊓ b = a ∨ a ⊓ b = b
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_mul : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [ContinuousConstSMul α α] {s t : Set α},
  interior s * interior t ⊆ interior (s * t)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoid : {M : Type u_1} → [inst : AddCommMonoid M] → AddCommGroup ↥(IsAddUnit.addSubmonoid M)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- A series of non-negative real numbers converges to `r` in the sense of `HasSum` if and only if
the sequence of partial sum converges to `r`.  -/
NNReal.hasSum_iff_tendsto_nat : ∀ {f : ℕ → NNReal} {r : NNReal}, HasSum f r ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds r)
-- Mathlib.Algebra.Category.Grp.AB
instHasFilteredColimitsAddCommGrpCat : CategoryTheory.Limits.HasFilteredColimits AddCommGrpCat
-- Mathlib.CategoryTheory.EpiMono
/-- `f` composed with `retraction` is the identity  -/
CategoryTheory.SplitMono.id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.SplitMono f),
  CategoryTheory.CategoryStruct.comp f self.retraction = CategoryTheory.CategoryStruct.id X
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (Std.DHashMap.Raw.ofList l).getKey? k' = some k
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.power_add : ∀ (a b c : Cardinal.{u_1}), a ^ (b + c) = a ^ b * a ^ c
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.go.eq_def : ∀ {α : Type u_1} (sep : Array α) (a : List α) (a_1 : List (List α)) (a_2 : Array α),
  List.intercalateTR.go✝ sep a a_1 a_2 =
    match a, a_1, a_2 with
    | x, [], acc => acc.toListAppend x
    | x, y :: xs, acc => List.intercalateTR.go✝ sep y xs (acc ++ x ++ sep)
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.eq_1 : ∀ {G : Type u_1} [inst : Group G] (S T : Set G), Subgroup.IsComplement S T = Function.Bijective fun x => ↑x.1 * ↑x.2
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.apply_one : ∀ {E : Type u_3} [inst : Group E] [inst_1 : DecidableEq E] (x : E), 1 x = if x = 1 then 0 else 1
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- An unbounded operator is closable iff the closure of its graph is a graph.  -/
LinearPMap.IsClosable : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] →
                    [ContinuousAdd E] →
                      [ContinuousAdd F] →
                        [inst_9 : TopologicalSpace R] →
                          [ContinuousSMul R E] → [ContinuousSMul R F] → (E →ₗ.[R] F) → Prop
-- Mathlib.Order.LatticeIntervals
Set.Iio.coe_inf : ∀ {α : Type u_1} [inst : SemilatticeInf α] {a : α} {x y : ↑(Set.Iio a)}, ↑(x ⊓ y) = ↑x ⊓ ↑y
-- Mathlib.LinearAlgebra.Complex.Module
Complex.lift_apply : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] (I' : { I' // I' * I' = -1 }),
  Complex.lift I' = Complex.liftAux ↑I' ⋯
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_bmod : ∀ {x : ℤ} {m : ℕ}, (x.bmod m).bmod m = x.bmod m
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- Right-whiskering the pushout-product of `X₁` and `X₂` with `W : C` is isomorphic to the
pushout-product of `X₁` and `X₂ ▷ W`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        (X₁ X₂ : CategoryTheory.Arrow C) →
          {W : C} →
            [CategoryTheory.Limits.PreservesColimit
                  (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
                  (CategoryTheory.MonoidalCategory.tensorRight W)] →
              CategoryTheory.Arrow.mk (CategoryTheory.MonoidalCategoryStruct.whiskerRight (X₁ □ X₂).hom W) ≅
                X₁ □ CategoryTheory.Arrow.mk (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom W)
-- Init.Data.Vector.Lemmas
Vector.sum_toList : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] [inst_1 : Zero α] {xs : Vector α n}, xs.toList.sum = xs.sum
-- Init.Classical
Classical.typeDecidableEq : (α : Sort u) → DecidableEq α
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.instOrderHomClassNatSet : ∀ {X : Type u_1} [inst : TopologicalSpace X], OrderHomClass (CompactExhaustion X) ℕ (Set X)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.prodCongr_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂]
  [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : TopologicalSpace P₃] [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄]
  [inst_15 : AddTorsor V₄ P₄] [inst_16 : TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₃ ≃ᴬ[k] P₄),
  (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- A function `f : G × G → M` satisfies the 2-coboundary condition if there's `x : G → M` such
that `g • x(h) / x(gh) * x(g) = f(g, h)` for all `g, h : G`.  -/
groupCohomology.IsMulCoboundary₂ : {G : Type u_1} → {M : Type u_2} → [Mul G] → [CommGroup M] → [SMul G M] → (G × G → M) → Prop
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_singleton_of_fintype : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [inst : Fintype ι]
  [∀ (i : ι), MeasurableSingletonClass (X i)] (f : (i : ι) → X i),
  (MeasureTheory.Measure.infinitePi μ) {f} = ∏ i, (μ i) {f i}
-- Mathlib.FieldTheory.Finite.Basic
Subfield.mem_bot_iff_pow_eq_self : ∀ (F : Type u_3) [inst : Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] {x : F}, x ∈ ⊥ ↔ x ^ p = x
-- Mathlib.Data.Fin.SuccPred
Fin.pred_castSucc_lt_iff : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a.castSucc ≠ 0), a.castSucc.pred ha < b ↔ a ≤ b
-- Mathlib.Order.GaloisConnection.Basic
isLUB_image2_of_isLUB_isGLB : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {s : Set α}
  {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β},
  (∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) →
    (∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) →
      IsLUB s a₀ → IsGLB t b₀ → IsLUB (Set.image2 l s t) (l a₀ b₀)
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_self_sub_left : ∀ {m n : ℕ}, m ≤ n → ((n - m).Coprime n ↔ m.Coprime n)
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.unoneD_eq_unoneD_iff : ∀ {α : Type u} {d : α} {x y : WithOne α},
  WithOne.unoneD d x = WithOne.unoneD d y ↔ x = y ∨ x = ↑d ∧ y = 1 ∨ x = 1 ∧ y = ↑d
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι],
  Submodule.map (↑P.toPerfPair.symm) (P.corootSpan R).dualAnnihilator ≤ LinearMap.ker P.RootForm
-- Mathlib.RingTheory.HahnSeries.Multiplication
/-- The casting function to the type synonym.  -/
HahnModule.of : {Γ : Type u_1} →
  {V : Type u_5} →
    [inst : PartialOrder Γ] →
      [inst_1 : Zero V] → (R : Type u_6) → [inst_2 : SMul R V] → HahnSeries Γ V ≃ HahnModule Γ R V
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.splits_rotateRight : ∀ {s : String} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits t₁ (t₂ ++ t₃)), h.rotateRight.Splits (t₁ ++ t₂) t₃
-- Mathlib.Order.Preorder.Chain
Flag.coe_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (s : Flag α),
  ↑((Flag.map e) s) = ⇑e '' ↑s
-- Aesop.Script.ScriptM
Aesop.withScriptStep : {α : Type} →
  Lean.MVarId → (α → Array Lean.MVarId) → (α → Bool) → (α → Aesop.Script.TacticBuilder) → Lean.MetaM α → Aesop.ScriptM α
-- Std.Sync.Semaphore
/-- Counting semaphore.

`Semaphore.acquire` returns a promise that is resolved once a permit is available.
If a permit is currently available, the returned promise is already resolved.
`Semaphore.release` either resolves one waiting promise or increments the available permits.
 -/
Std.Semaphore : Type
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The centroid commutes with translation by a constant point.
Subtracting a fixed point `p₀` from the centroid is the same as taking the centroid of
the family translated by `-ᵥ p₀`  -/
Finset.centroid_vsub_const : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [CharZero k] {p : ι → P} {p₀ : P},
  s.Nonempty → Finset.centroid k s p -ᵥ p₀ = Finset.centroid k s fun i => p i -ᵥ p₀
-- Mathlib.Tactic.Ring.Common
/-- The data used to represent coefficients in exponents. This is the same data that `ring` uses.  -/
Mathlib.Tactic.Ring.Common.btℕ : Q(ℕ) → Type
-- Mathlib.Data.Fintype.EquivFin
Infinite.instSigmaOfNonempty : ∀ {α : Type u_1} {β : α → Type u_4} [Infinite α] [∀ (a : α), Nonempty (β a)], Infinite ((a : α) × β a)
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.trivializationAt_symmL : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) {b₀ b : B},
  b ∈ (trivializationAt F Z.Fiber b₀).baseSet →
    Bundle.Trivialization.symmL R (trivializationAt F Z.Fiber b₀) b = Z.coordChange (Z.indexAt b₀) (Z.indexAt b) b
-- Mathlib.Algebra.Category.CommAlgCat.Basic
commAlgCatEquivUnder_functor_map : ∀ (R : CommRingCat) {A B : CommAlgCat ↑R} (f : A ⟶ B),
  (commAlgCatEquivUnder R).functor.map f = (CommAlgCat.Hom.hom f).toUnder
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceR!.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (r : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  motive
                    (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf
                      Std.DTreeMap.Internal.Impl.leaf)) →
            ((size : ℕ) →
                (rk : α) →
                  (rv : β rk) →
                    (size_1 : ℕ) →
                      (k : α) →
                        (v : β k) →
                          (l r : Std.DTreeMap.Internal.Impl α β) →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                                (Std.DTreeMap.Internal.Impl.inner size_1 k v l r))) →
              ((size : ℕ) →
                  (rk : α) →
                    (rv : β rk) →
                      (size_1 : ℕ) →
                        (rlk : α) →
                          (rlv : β rlk) →
                            (l r : Std.DTreeMap.Internal.Impl α β) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size rk rv
                                  (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                                  Std.DTreeMap.Internal.Impl.leaf)) →
                ((rs : ℕ) →
                    (rk : α) →
                      (rv : β rk) →
                        (rls : ℕ) →
                          (k : α) →
                            (v : β k) →
                              (l r : Std.DTreeMap.Internal.Impl α β) →
                                (size : ℕ) →
                                  (k_1 : α) →
                                    (v_1 : β k_1) →
                                      (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                                        motive
                                          (Std.DTreeMap.Internal.Impl.inner rs rk rv
                                            (Std.DTreeMap.Internal.Impl.inner rls k v l r)
                                            (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l_1 r_1))) →
                  motive r
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instZSMul : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → SubNegMonoid (R i)] →
              [∀ (i : ι), AddSubgroupClass (S i) (R i)] → SMul ℤ (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq' : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 2 = Q 2 → Q 2 ∈ nonZeroDivisors R → (P ≈ Q ↔ P = Q)
-- Mathlib.Data.Sum.Order
OrderIso.sumLexDualAntidistrib_symm_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (b : β),
  (OrderIso.sumLexDualAntidistrib α β).symm (Sum.inl (OrderDual.toDual b)) = OrderDual.toDual (Sum.inr b)
-- Aesop.Index.RulePattern
/-- Get all substitutions of the rule patterns that match a subexpression of
a hypothesis or the target. Subexpressions containing bound variables are not
considered.  -/
Aesop.RulePatternIndex.getInGoal : Lean.MVarId → Aesop.RulePatternIndex → Aesop.BaseM Aesop.RulePatternSubstMap
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ofMultiset_parts : ∀ (l : Multiset ℕ), (Nat.Partition.ofMultiset l).parts = Multiset.filter (fun x => ¬x = 0) l
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_spec' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
  (algebraMap R S) ↑y * IsLocalization.mk' S x y = (algebraMap R S) x
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- Converts a `LinearEquiv` to an isomorphism in the category `FGModuleCat R`.  -/
LinearEquiv.toFGModuleCatIso : {R : Type u} →
  [inst : Ring R] →
    {V W : Type v} →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          [inst_3 : Module.Finite R V] →
            [inst_4 : AddCommGroup W] →
              [inst_5 : Module R W] →
                [inst_6 : Module.Finite R W] → (V ≃ₗ[R] W) → (FGModuleCat.of R V ≅ FGModuleCat.of R W)
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticOnNhd.aeval_mvPolynomial : ∀ {𝕜 : Type u_1} {E : Type u_2} {A : Type u_3} {B : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : CommSemiring A] {s : Set E}
  [inst_4 : NormedCommRing B] [inst_5 : NormedAlgebra 𝕜 B] [inst_6 : Algebra A B] {σ : Type u_5} {f : E → σ → B},
  (∀ (i : σ), AnalyticOnNhd 𝕜 (fun x => f x i) s) →
    ∀ (p : MvPolynomial σ A), AnalyticOnNhd 𝕜 (fun x => (MvPolynomial.aeval (f x)) p) s
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.map_comp : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'}
  [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N]
  [inst_9 : AddCommMonoid P] [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P]
  [inst_13 : AddCommMonoid Q] [inst_14 : Module R Q] [inst_15 : AddCommMonoid P'] [inst_16 : Module R P']
  [inst_17 : Module A P'] [inst_18 : IsScalarTower R A P'] [inst_19 : AddCommMonoid Q'] [inst_20 : Module R Q']
  (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q),
  TensorProduct.AlgebraTensorModule.map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) =
    TensorProduct.AlgebraTensorModule.map f₂ g₂ ∘ₗ TensorProduct.AlgebraTensorModule.map f₁ g₁
-- Mathlib.Algebra.Algebra.Defs
Algebra.toModule : {R : Type u_2} → {A : Type u_3} → {x : CommSemiring R} → {x_1 : Semiring A} → [Algebra R A] → Module R A