mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] {α : LieModule.Weight K (↥H) L} {e f : L},
  e ∈ LieAlgebra.rootSpace H ⇑α →
    f ∈ LieAlgebra.rootSpace H (-⇑α) →
      (∀ (h : ↥H), ⁅h, e⁆ = α h • e) →
        ⁅e, f⁆ =
          ((killingForm K L) e) f •
            ↑((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α))
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.instInhabitedId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a c : B} → {g : a ⟶ c} → Inhabited (CategoryTheory.Bicategory.LeftExtension (CategoryTheory.CategoryStruct.id a) g)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- A constant `BitVec` value.
 -/
Std.Tactic.BVDecide.BVExpr.const : {w : ℕ} → BitVec w → Std.Tactic.BVDecide.BVExpr w
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.IsTerminal.hasTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : CategoryTheory.Limits.IsTerminal X),
  CategoryTheory.Limits.HasTerminal C
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_copy : ∀ {α : Type u} [inst : AddMonoid α] (u : AddUnits α) (val : α) (hv : val = ↑u) (neg : α) (hi : neg = ↑(-u)),
  ↑(u.copy val hv neg hi) = val
-- Init.Data.Ord.UInt
UInt16.instLawfulOrderOrd : Std.LawfulOrderOrd UInt16
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.ofNatCode.eq_3 : Nat.Partrec.Code.ofNatCode 2 = Nat.Partrec.Code.left
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
ContinuousAt.compMeasurePreservingLp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] [R1Space X]
  [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3}
  [inst_10 : NormedAddCommGroup E] {p : ENNReal} [inst_11 : Fact (1 ≤ p)] {Z : Type u_4} [inst_12 : TopologicalSpace Z]
  {f : Z → ↥(MeasureTheory.Lp E p ν)} {g : Z → C(X, Y)} {z : Z},
  ContinuousAt f z →
    ContinuousAt g z →
      ∀ (hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν),
        p ≠ ⊤ → ContinuousAt (fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) z
-- Mathlib.Order.Interval.Set.Infinite
Set.Ico_infinite : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] {a b : α}, a < b → (Set.Ico a b).Infinite
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.univ_div_univ : ∀ {α : Type u_2} [inst : DivisionMonoid α], Set.univ / Set.univ = Set.univ
-- Mathlib.RingTheory.Norm.Transitivity
LinearMap.det_restrictScalars : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Module.Free R S] [inst_4 : AddCommGroup A] [inst_5 : Module R A] [inst_6 : Module S A] [inst_7 : IsScalarTower R S A]
  [Module.Free S A] {f : A →ₗ[S] A}, LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`, where one side is a multiple
of a rotation of another by `π / 2`.  -/
Orientation.oangle_add_left_smul_rotation_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V},
  x ≠ 0 →
    ∀ (r : ℝ), o.oangle (x + r • (o.rotation ↑(Real.pi / 2)) x) (r • (o.rotation ↑(Real.pi / 2)) x) = ↑(Real.arctan r⁻¹)
-- Init.Data.Option.Attach
Option.map_attachWith : ∀ {α : Type u_1} {β : Type u_2} {l : Option α} {P : α → Prop} {H : ∀ (a : α), l = some a → P a} (f : { x // P x } → β),
  Option.map f (l.attachWith P H) =
    Option.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      l.attach
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.toOpen_map_app : ∀ {R : CommRingCat} {M N : ModuleCat ↑R} (f : M ⟶ N) (U : TopologicalSpace.Opens (PrimeSpectrum ↑R)),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.toOpen M U)
      ((AlgebraicGeometry.modulesSpecToSheaf.map (AlgebraicGeometry.tilde.map f)).hom.app (Opposite.op U)) =
    CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.tilde.toOpen N U)
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {l' : List β} {l : List α} {f : (i : ℕ) → α → i < l.length → β},
  l.mapFinIdx f = l' ↔ ∃ (h : l'.length = l.length), ∀ (i : ℕ) (h_1 : i < l.length), l'[i] = f i l[i] h_1
-- Init.Data.List.Monadic
List.filterMapM_subtype : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {p : α → Prop}
  {l : List { x // p x }} {f : { x // p x } → m (Option β)} {g : α → m (Option β)},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → List.filterMapM f l = List.filterMapM g l.unattach
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_eq_tsum_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β)
  [inst : ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ)
  [inst_1 : ProbabilityTheory.IsSFiniteKernel η] (a : α),
  MeasurableSet s → ((κ.compProd η) a) s = ∑' (n : ℕ) (m : ℕ), (((κ.seq n).compProd (η.seq m)) a) s
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The coefficients `b i` are positive.  -/
AkraBazziRecurrence.b_pos : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r) (i : α), 0 < b i
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.containsThenInsertIfNew : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {a : α} {b : β},
  m.WF → (m.containsThenInsertIfNew a b).2.WF
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaEquiv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : C}
  {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} (α : CategoryTheory.shrinkYoneda.{w, v, u}.obj X ⟶ P) (β : P ⟶ Q),
  CategoryTheory.shrinkYonedaEquiv (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.ConcreteCategory.hom (β.app (Opposite.op X))) (CategoryTheory.shrinkYonedaEquiv α)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.hasPullback_of_right_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso g],
  CategoryTheory.Limits.HasPullback f g
-- Init.Data.Array.Lemmas
Array.anyM_congr : ∀ {m : Type → Type u_1} {α : Type u_2} {start₁ start₂ stop₁ stop₂ : ℕ} [inst : Monad m] {xs ys : Array α},
  xs = ys →
    ∀ {p q : α → m Bool},
      (∀ (a : α), p a = q a) →
        start₁ = start₂ → stop₁ = stop₂ → Array.anyM p xs start₁ stop₁ = Array.anyM q ys start₂ stop₂
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_source_mem_nhds' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x x' : M},
  x' ∈ (extChartAt I x).source → (extChartAt I x).source ∈ nhds x'
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_insertMany_list_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, k ∈ m → (m.insertMany l).get? k = m.get? k
-- Lean.Parser.Command
Lean.Parser.Command.optDeclSig.formatter : Lean.PrettyPrinter.Formatter
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.orelse.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.IsAscendingCentralSeries.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : ℕ → AddSubgroup G),
  AddSubgroup.IsAscendingCentralSeries H = (H 0 = ⊥ ∧ ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n)
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.LiftPPreservation.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F],
  MvQPF.LiftPPreservation =
    ∀ ⦃α : TypeVec.{u} n⦄ (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : ↑(MvQPF.P F) α),
      MvFunctor.LiftP p (MvQPF.abs x) ↔ MvFunctor.LiftP p x
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffWithinAt.neg : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieAddGroup I n G] {f : M → G} {s : Set M} {x₀ : M},
  ContMDiffWithinAt I' I n f s x₀ → ContMDiffWithinAt I' I n (fun x => -f x) s x₀
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_right_le_size_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₂.size ≤ (m₁ ∪ m₂).size
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.moduleCat_of_toModuleCat : ∀ {R : Type u} [inst : CommRing R] (X : QuadraticModuleCat R), ModuleCat.of R ↑X.toModuleCat = X.toModuleCat
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- The identity `StrictlyUnitaryPseudofunctor`.  -/
CategoryTheory.StrictlyUnitaryPseudofunctor.id : (B : Type u₁) → [inst : CategoryTheory.Bicategory B] → CategoryTheory.StrictlyUnitaryPseudofunctor B B
-- Mathlib.Data.List.Forall2
List.SublistForall₂.below.nil : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}
  {motive : (a : List α) → (a_1 : List β) → List.SublistForall₂ R a a_1 → Prop} {l : List β},
  List.SublistForall₂.below ⋯
-- Mathlib.GroupTheory.Index
Subgroup.index_ker : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G'), f.ker.index = Nat.card ↥f.range
-- Mathlib.Analysis.Convex.Between
wbtw_const_add_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Wbtw R (v + x) (v + y) (v + z) ↔ Wbtw R x y z
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If two unoriented angles are equal, and the signs of the corresponding oriented angles are
negations of each other, then the oriented angles are negations of each other (even in degenerate
cases).  -/
EuclideanGeometry.oangle_eq_neg_of_angle_eq_of_sign_eq_neg : ∀ {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₄ p₅ p₆ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆ →
    (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -(EuclideanGeometry.oangle p₄ p₅ p₆).sign →
      EuclideanGeometry.oangle p₁ p₂ p₃ = -EuclideanGeometry.oangle p₄ p₅ p₆
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_def : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A}
  {y : NNReal}, a ^ y = cfcₙ (fun x => x.nnrpow y) a
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.mem_fixedPoints_iff_card_orbit_eq_one : ∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] {a : α}
  [inst_2 : Fintype ↑(MulAction.orbit M a)], a ∈ MulAction.fixedPoints M α ↔ Fintype.card ↑(MulAction.orbit M a) = 1
-- Mathlib.Analysis.LocallyConvex.AbsConvex
nhds_hasBasis_absConvex_open : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [LocallyConvexSpace 𝕜 E] [ContinuousSMul 𝕜 E]
  [IsTopologicalAddGroup E] [ZeroLEOneClass 𝕜], (nhds 0).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s) id
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.brecOn_1.go : {motive_1 : Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Sort u} →
    {motive_3 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
      {motive_4 : Task Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
        (t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
          ((t : Lean.Language.Lean.CommandParsedSnapshot) → t.below → motive_1 t) →
            ((t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
                Lean.Language.Lean.CommandParsedSnapshot.below_1 t → motive_2 t) →
              ((t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
                  Lean.Language.Lean.CommandParsedSnapshot.below_2 t → motive_3 t) →
                ((t : Task Lean.Language.Lean.CommandParsedSnapshot) →
                    Lean.Language.Lean.CommandParsedSnapshot.below_3 t → motive_4 t) →
                  motive_2 t ×' Lean.Language.Lean.CommandParsedSnapshot.below_1 t
-- Mathlib.Topology.Basic
Classical.strongIndefiniteDescription.congr_simp : ∀ {α : Sort u} (p : α → Prop) (h : Nonempty α),
  Classical.strongIndefiniteDescription p h = Classical.strongIndefiniteDescription p h
-- Mathlib.Topology.Order
le_iff_nhds : ∀ {α : Type u_1} (t t' : TopologicalSpace α), t ≤ t' ↔ ∀ (x : α), nhds x ≤ nhds x
-- Mathlib.Analysis.Normed.Group.Bounded
Bornology.IsBounded.exists_pos_norm_le : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] {s : Set E}, Bornology.IsBounded s → ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piUnique_apply : ∀ {α : Type u_7} [inst : Unique α] (f : α → Type u_8) [inst_1 : (x : α) → TopologicalSpace (f x)],
  ⇑(Homeomorph.piUnique f) = fun f => f default
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.logTaylor.eq_1 : ∀ (n : ℕ) (z : ℂ), Complex.logTaylor n z = ∑ j ∈ Finset.range n, (-1) ^ (j + 1) * z ^ j / ↑j
-- Lean.Data.Json.Parser
Lean.Json.Parser.natNumDigits : Std.Internal.Parsec.String.Parser (ℕ × ℕ)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inl_v_snd_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + -1 = q)
  {Z : C} (h : L.X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.snd φ).v p q hpq) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_neg : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Ring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : DirectSum ι fun x => M), (-f).toAddMonoidAlgebra = -f.toAddMonoidAlgebra
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentPositionParams.textDocument : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.TextDocumentIdentifier
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of the reverse direction of `SimpleGraph.edgeSet_subset_edgeSet`. -/
SimpleGraph.edgeSet_mono : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V}, G₁ ≤ G₂ → G₁.edgeSet ⊆ G₂.edgeSet
-- Std.Net.Addr
/-- Obtain the `AddressFamily` associated with an `IPAddr`.
 -/
Std.Net.IPAddr.family : Std.Net.IPAddr → Std.Net.AddressFamily
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular], μ ≠ 0 → IsOpen U → U.Nonempty → 0 < μ U
-- Mathlib.GroupTheory.Subsemigroup.Center
Subsemigroup.center_eq_top : ∀ (M : Type u_1) [inst : CommSemigroup M], Subsemigroup.center M = ⊤
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The (exact) sequence `0 ⟶ E^n(f₁, f₂, f₃) ⟶ H^n(f₂ ≫ f₃) ⟶ H^n(f₃) ⊞ H^{n+1}(f₁)`.  -/
CategoryTheory.Abelian.SpectralObject.kernelSequenceE : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k l : ι} →
              (i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (f₂₃ : j ⟶ l) →
                      CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
                        (n₀ n₁ n₂ : ℤ) →
                          autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_1 →
                            autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_3 →
                              CategoryTheory.ShortComplex C
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piFinTwo_symm_apply : ∀ (α : Fin 2 → Type u_8) [inst : (i : Fin 2) → MeasurableSpace (α i)],
  ⇑(MeasurableEquiv.piFinTwo α).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- Build an algebra equivalence from a linear equivalence out of a triple tensor product,
and evidence of multiplicativity on pure tensors.
 -/
Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      {C : Type uC} →
        {D : Type uD} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A] →
              [inst_2 : Algebra R A] →
                [inst_3 : Semiring B] →
                  [inst_4 : Algebra R B] →
                    [inst_5 : Semiring C] →
                      [inst_6 : Semiring D] →
                        [inst_7 : Algebra R D] →
                          [inst_8 : Algebra R C] →
                            (f : TensorProduct R (TensorProduct R A B) C ≃ₗ[R] D) →
                              (∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
                                  f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) =
                                    f (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * f (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂)) →
                                f (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) = 1 → TensorProduct R (TensorProduct R A B) C ≃ₐ[R] D
-- Mathlib.Data.Num.ZNum
ZNum.succ.eq_1 : ZNum.zero.succ = 1
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} (f : (i : ι) → X i ⟶ S) {ι' : Type t'} {X' : ι' → C} (f' : (i' : ι') → X' i' ⟶ S),
  CategoryTheory.Sieve.ofArrows X f = CategoryTheory.Sieve.ofArrows X' f' →
    ((F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence)
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `lowerSemicontinuous_iff_frequently`. -/
LowerSemicontinuous.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β},
  LowerSemicontinuous f → ∀ (x : α) (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≤ y) → f x ≤ y
-- Mathlib.Data.List.Prime
Prime.not_dvd_prod : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M} {L : List M}, Prime p → (∀ a ∈ L, ¬p ∣ a) → ¬p ∣ L.prod
-- Mathlib.LinearAlgebra.Matrix.ToLin
instIsStablyFiniteRingEndForallOfFinite : ∀ {A : Type u_3} [inst : Semiring A] (ι : Type u_5) [Finite ι] [IsStablyFiniteRing A],
  IsStablyFiniteRing (Module.End A (ι → A))
-- Mathlib.Order.Partition.Finpartition
Finpartition.instFintypeFinset : {α : Type u_1} → [inst : DecidableEq α] → {s : Finset α} → Fintype (Finpartition s)
-- Mathlib.Data.Fintype.Quotient
_private.Mathlib.Data.Fintype.Quotient.0.Quotient.listChoice.match_3.splitter : {ι : Type u_1} →
  {α : ι → Sort u_2} →
    {S : (i : ι) → Setoid (α i)} →
      (motive : (l : List ι) → ((i : ι) → i ∈ l → Quotient (S i)) → Sort u_3) →
        (l : List ι) →
          (q : (i : ι) → i ∈ l → Quotient (S i)) →
            ((q : (i : ι) → i ∈ [] → Quotient (S i)) → motive [] q) →
              ((i : ι) →
                  (tail : List ι) → (q : (i_1 : ι) → i_1 ∈ i :: tail → Quotient (S i_1)) → motive (i :: tail) q) →
                motive l q
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
/-- The distribution of the increment of the real Brownian motion from time `s` to time `t`
is the centered Gaussian with variance `t - s`.  -/
ProbabilityTheory.BrownianReal.measurePreserving_eval_sub_eval_projectiveFamily : ∀ (I : Finset NNReal) (s t : ↥I),
  MeasureTheory.MeasurePreserving (fun x => x s - x t) (ProbabilityTheory.BrownianReal.projectiveFamily I)
    (ProbabilityTheory.gaussianReal 0 (nndist ↑s ↑t))
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.Std.Slice.Internal.ByteSliceData.mk.congr_simp : ∀ (byteArray byteArray_1 : ByteArray) (e_byteArray : byteArray = byteArray_1) (start start_1 : ℕ)
  (e_start : start = start_1) (stop stop_1 : ℕ) (e_stop : stop = stop_1) (start_le_stop : start ≤ stop)
  (stop_le_size_byteArray : stop ≤ byteArray.size),
  { byteArray := byteArray, start := start, stop := stop, start_le_stop := start_le_stop,
      stop_le_size_byteArray := stop_le_size_byteArray } =
    { byteArray := byteArray_1, start := start_1, stop := stop_1, start_le_stop := ⋯, stop_le_size_byteArray := ⋯ }
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.id_apply : ∀ (X : NonemptyFinLinOrd) (x : ↑X.toLinOrd),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Given a local frame `s i ` on `u`, if a section `t` has `C^k` coefficients on `u` w.r.t. `s i`,
then `t` is `C^n` on `u`.  -/
IsLocalFrameOn.contMDiffOn_of_coeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {t : (x : M) → V x} (hs : IsLocalFrameOn I F n s u) [VectorBundle 𝕜 F V]
  [FiniteDimensional 𝕜 F],
  (∀ (i : ι), ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) n ((LinearMap.piApply (hs.coeff i)) t) u) →
    ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t x⟩) u
-- Mathlib.Data.List.Lattice
List.mem_of_mem_inter_left : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α} [inst : DecidableEq α], a ∈ l₁ ∩ l₂ → a ∈ l₁
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyReal.of_algebra : ∀ (F : Type u_1) [inst : Field F] (K : Type u_2) [inst_1 : Field K] [NumberField.IsTotallyReal K] [inst_3 : Algebra F K]
  [Algebra.IsAlgebraic F K], NumberField.IsTotallyReal F