mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.ofIsPresentation_toSolution : ∀ {A : Type u} [inst : Ring A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  {relations : Module.Relations A} {solution : relations.Solution M} (h : solution.IsPresentation),
  (Module.Presentation.ofIsPresentation h).toSolution = solution
-- Mathlib.RingTheory.Support
/-- [Stacks Tag 00L3](https://stacks.math.columbia.edu/tag/00L3) ((3)) -/
Module.support_subset_of_surjective : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  Function.Surjective ⇑f → Module.support R N ⊆ Module.support R M
-- Std.Time.Time.PlainTime
/-- Adds milliseconds to a `PlainTime`.
 -/
Std.Time.PlainTime.addMilliseconds : Std.Time.PlainTime → Std.Time.Millisecond.Offset → Std.Time.PlainTime
-- Mathlib.CategoryTheory.Shift.Quotient
HomRel.IsCompatibleWithShift.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {r : HomRel C} {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A],
  (∀ (a : A) ⦃X Y : C⦄ (f g : X ⟶ Y),
      r f g → r ((CategoryTheory.shiftFunctor C a).map f) ((CategoryTheory.shiftFunctor C a).map g)) →
    r.IsCompatibleWithShift A
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], Cardinal.toENat (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.conjStarAlgAut_ext_iff : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] {S : Type u_3} [inst_2 : CommSemiring S]
  [inst_3 : Algebra S R] [Algebra.IsCentral S R] (u v : ↥(unitary R)),
  (Unitary.conjStarAlgAut S R) u = (Unitary.conjStarAlgAut S R) v ↔ ∃ α, ↑u = α • ↑v
-- Mathlib.Data.Finmap
Finmap.disjoint_empty : ∀ {α : Type u} {β : α → Type v} (x : Finmap β), ∅.Disjoint x
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyι_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hj : c.next i = j) (h : K.d i j = 0)
  [inst_2 : K.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.isoHomologyι i j hj h).inv =
    CategoryTheory.CategoryStruct.id (K.homology i)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- If `s` is Borel-measurable in a Polish space and `f` is continuous injective on `s`, then
the restriction of `f` to `s` is a measurable embedding.  -/
ContinuousOn.measurableEmbedding : ∀ {γ : Type u_3} {β : Type u_5} [inst : MeasurableSpace β] [tβ : TopologicalSpace β] [T2Space β] {s : Set γ} {f : γ → β}
  [BorelSpace β] [inst_3 : TopologicalSpace γ] [PolishSpace γ] [inst_5 : MeasurableSpace γ] [BorelSpace γ],
  MeasurableSet s → ContinuousOn f s → Set.InjOn f s → MeasurableEmbedding (s.domRestrict f)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.pairwise_disjoint_gammaSet : ∀ (N r : ℕ), Pairwise (Function.onFun Disjoint (EisensteinSeries.gammaSet N r))
-- Mathlib.Analysis.Normed.Group.Basic
abs_norm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (z : E), |‖z‖| = ‖z‖
-- Mathlib.SetTheory.Lists
Lists'.to_ofList : ∀ {α : Type u_1} (l : List (Lists α)), (Lists'.ofList l).toList = l
-- Mathlib.Algebra.AffineMonoid.Basic
IsAffineAddMonoid.toFG : ∀ {M : Type u_1} {inst : AddCommMonoid M} [self : IsAffineAddMonoid M], AddMonoid.FG M
-- Init.Data.Option.Lemmas
Option.bind_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → Option γ} {x : Option α},
  (Option.map f x).bind g = x.bind (g ∘ f)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.setTR.go.eq_2 : ∀ {α : Type u_1} (l : List α) (a : α) (a_1 : Array α) (head : α) (xs : List α),
  List.setTR.go✝ l a (head :: xs) 0 a_1 = a_1.toListAppend (a :: xs)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω), ↑(ν s) = ↑ν s
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.zero_le : ∀ (p : DyckWord), 0 ≤ p
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.IsIsolated.of_subsingleton : ∀ {V : Type u} [Subsingleton V] (G : SimpleGraph V) (v : V), G.IsIsolated v
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharNeTwoNF_iff : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R), W.IsCharNeTwoNF ↔ W.a₁ = 0 ∧ W.a₃ = 0
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorem.priority : Lean.Meta.SimpTheorem → ℕ
-- Mathlib.RingTheory.Valuation.ValuationRing
/-- The value group of the valuation ring `A`. Note: this is actually a group with zero.  -/
ValuationRing.ValueGroup : (A : Type u) → [inst : CommRing A] → (K : Type v) → [inst_1 : Field K] → [Algebra A K] → Type v
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Kind.bicategory.sizeOf_spec : sizeOf Mathlib.Tactic.Widget.StringDiagram.Kind.bicategory = 1
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.card_mul_eq_mul_card_of_injOn_opSMul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {H : Subgroup G} [inst_2 : Fintype ↥H] {Z : Finset G},
  Set.InjOn (fun x => MulOpposite.op x • ↑H) ↑Z → Fintype.card ↥H * Z.card = ((↑H).toFinset * Z).card
-- Mathlib.Data.Set.Operations
Set.mem_diagonal_iff : ∀ {α : Type u} {x : α × α}, x ∈ Set.diagonal α ↔ x.1 = x.2
-- Init.Data.List.ToArray
List.append_toArray : ∀ {α : Type u_1} (l₁ l₂ : List α), l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.stalkClosedPointTo.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X),
  AlgebraicGeometry.Scheme.stalkClosedPointTo f =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f (IsLocalRing.closedPoint ↑R))
      (AlgebraicGeometry.stalkClosedPointIso R).hom
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.exists_or : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (x : A.N), ∃ y, x = ↑y ∨ x = ↑(P.p y)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.instNeg : {ι : Type u_1} →
  {I₀ : WithTop (BoxIntegral.Box ι)} →
    {M : Type u_4} → [inst : AddCommGroup M] → Neg (BoxIntegral.BoxAdditiveMap ι M I₀)
-- Mathlib.Analysis.Normed.Affine.MazurUlam
IsometryEquiv.coeFn_toRealAffineIsometryEquiv : ∀ {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : MetricSpace PE] [inst_3 : NormedAddTorsor E PE] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F]
  [inst_6 : MetricSpace PF] [inst_7 : NormedAddTorsor F PF] (f : PE ≃ᵢ PF), ⇑f.toRealAffineIsometryEquiv = ⇑f
-- Mathlib.Topology.LocallyClosed
IsLocallyClosed.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), IsLocallyClosed s = ∃ U Z, IsOpen U ∧ IsClosed Z ∧ s = U ∩ Z
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W₁ W₂ : CategoryTheory.MorphismProperty C}
  {inst_1 : W₁.IsMultiplicative} {inst_2 : W₂.IsMultiplicative} {α : Type u_2} {inst_3 : LinearOrder α}
  {inst_4 : OrderBot α} {inst_5 : SuccOrder α} {inst_6 : WellFoundedLT α} {deg : C → α}
  {lt₁ : ∀ {X Y : C} (f : X ⟶ Y), W₁ f → ¬CategoryTheory.MorphismProperty.identities C f → deg Y < deg X}
  {lt₂ : ∀ {X Y : C} (f : X ⟶ Y), W₂ f → ¬CategoryTheory.MorphismProperty.identities C f → deg X < deg Y}
  {nonempty_unique : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (Unique (W₁.MapFactorizationData W₂ f))} {deg_1 : C → α}
  {lt₁_1 : ∀ {X Y : C} (f : X ⟶ Y), W₁ f → ¬CategoryTheory.MorphismProperty.identities C f → deg_1 Y < deg_1 X}
  {lt₂_1 : ∀ {X Y : C} (f : X ⟶ Y), W₂ f → ¬CategoryTheory.MorphismProperty.identities C f → deg_1 X < deg_1 Y}
  {nonempty_unique_1 : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (Unique (W₁.MapFactorizationData W₂ f))},
  { deg := deg, lt₁ := lt₁, lt₂ := lt₂, nonempty_unique := nonempty_unique } =
      { deg := deg_1, lt₁ := lt₁_1, lt₂ := lt₂_1, nonempty_unique := nonempty_unique_1 } →
    deg = deg_1
-- Mathlib.Analysis.Convex.Gauge
gauge_unit_ball : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E), gauge (Metric.ball 0 1) x = ‖x‖
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.semilinearEquivOfRingEquiv_algebraMap : ∀ {A : Type u_8} {B : Type u_9} (K : Type u_10) (L : Type u_11) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (f : A ≃+* B) (a : A),
  (IsFractionRing.semilinearEquivOfRingEquiv K L f) ((algebraMap A K) a) = (algebraMap B L) (f a)
-- Lean.Server.Requests
Lean.Server.RequestContext.mk.injEq : ∀ (rpcSessions : Std.TreeMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare)
  (doc : Lean.Server.FileWorker.EditableDocument) (hLog : IO.FS.Stream) (initParams : Lean.Lsp.InitializeParams)
  (cancelTk : Lean.Server.RequestCancellationToken) (serverRequestEmitter : Lean.Server.ServerRequestEmitter)
  (rpcSessions_1 : Std.TreeMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare)
  (doc_1 : Lean.Server.FileWorker.EditableDocument) (hLog_1 : IO.FS.Stream) (initParams_1 : Lean.Lsp.InitializeParams)
  (cancelTk_1 : Lean.Server.RequestCancellationToken) (serverRequestEmitter_1 : Lean.Server.ServerRequestEmitter),
  ({ rpcSessions := rpcSessions, doc := doc, hLog := hLog, initParams := initParams, cancelTk := cancelTk,
        serverRequestEmitter := serverRequestEmitter } =
      { rpcSessions := rpcSessions_1, doc := doc_1, hLog := hLog_1, initParams := initParams_1, cancelTk := cancelTk_1,
        serverRequestEmitter := serverRequestEmitter_1 }) =
    (rpcSessions = rpcSessions_1 ∧
      doc = doc_1 ∧
        hLog = hLog_1 ∧
          initParams = initParams_1 ∧ cancelTk = cancelTk_1 ∧ serverRequestEmitter = serverRequestEmitter_1)
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.exists_iff_exists_existsUnique : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G},
  (∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0) ↔ ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 + ab.2 = g
-- Init.Data.Vector.Lemmas
Vector.setIfInBounds_replicate_self : ∀ {n : ℕ} {α : Type u_1} {a : α} {i : ℕ}, (Vector.replicate n a).setIfInBounds i a = Vector.replicate n a
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.isEmbedding_restrictScalars : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [ContinuousSMul 𝕜 E] {F : Type u_3} [inst_5 : AddCommGroup F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [inst_8 : Module 𝕜 F] (𝕜' : Type u_4)
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : Module 𝕜' E]
  [inst_12 : IsScalarTower 𝕜' 𝕜 E] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F],
  Topology.IsEmbedding (ContinuousLinearMap.restrictScalars 𝕜')
-- Mathlib.Order.OmegaCompletePartialOrder
/-- When proving that a chain of applications is below a bound `z`, it suffices to consider the
functions and values being selected from the same index in the chains.

This lemma is more specific than necessary, i.e. `c₀` only needs to be a
chain of monotone functions, but it is only used with continuous functions.  -/
OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α) (z : β),
  (∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
-- Mathlib.Data.Matrix.Mul
Matrix.instNonUnitalRing : {n : Type u_3} → {α : Type v} → [Fintype n] → [NonUnitalRing α] → NonUnitalRing (Matrix n n α)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_le_add_iff_of_lt_aleph0 : ∀ {α β γ : Cardinal.{u_1}}, γ < Cardinal.aleph0 → (α + γ ≤ β + γ ↔ α ≤ β)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.isOrthogonal_short_and_long : ∀ {ι : 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 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] {i : ι},
  P.root i ∉ RootPairing.EmbeddedG2.allRoots P →
    P.IsOrthogonal i (RootPairing.EmbeddedG2.short P) ∧ P.IsOrthogonal i (RootPairing.EmbeddedG2.long P)
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_dvd_sub_iff_zsmul_eq_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} {a b : ℤ}, ↑(addOrderOf x) ∣ a - b ↔ a • x = b • x
-- Mathlib.Analysis.Calculus.FDeriv.Congr
DifferentiableWithinAt.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → (∀ x ∈ s, f₁ x = f x) → f₁ x = f x → DifferentiableWithinAt 𝕜 f₁ s x
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.fun_smul : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] (c : ℝ),
  ProbabilityTheory.HasGaussianLaw X P → ProbabilityTheory.HasGaussianLaw (fun ω => c • X ω) P
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.instCoeSortType : {R : Type u} → [inst : CommRing R] → CoeSort (HopfAlgCat R) (Type v)
-- Mathlib.NumberTheory.Padics.PadicNumbers
instAddCommGroupPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → AddCommGroup ℚ_[p]
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.decompLinearIsometryEquiv.eq_1 : ∀ (𝕜 : Type u_1) (R : Type u_2) (V : Type u_3) (W : Type u_4) [inst : SeminormedAddCommGroup V]
  [inst_1 : SeminormedAddCommGroup W] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : Ring R] [inst_6 : Module R W] [inst_7 : ContinuousConstSMul R W]
  [inst_8 : SMulCommClass 𝕜 R W],
  ContinuousAffineMap.decompLinearIsometryEquiv 𝕜 R V W =
    { toLinearEquiv := ContinuousAffineMap.decompLinearEquiv 𝕜 R V W, norm_map' := ⋯ }
-- Mathlib.NumberTheory.NumberField.Basic
/-- The canonical map from `𝓞 K` to `K` is injective.

This is a convenient abbreviation for `FaithfulSMul.algebraMap_injective`.
 -/
NumberField.RingOfIntegers.coe_injective : ∀ {K : Type u_1} [inst : Field K], Function.Injective ⇑(algebraMap (NumberField.RingOfIntegers K) K)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.mem_op : ∀ {M : Type u_2} [inst : MulOneClass M] {x : Mᵐᵒᵖ} {S : Submonoid M}, x ∈ S.op ↔ MulOpposite.unop x ∈ S
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.closure_iUnion : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} (s : ι → Set M),
  AddSubmonoid.closure (⋃ i, s i) = ⨆ i, AddSubmonoid.closure (s i)
-- Lean.Elab.Level
Lean.Elab.Level.Context : Type
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.mem_coe : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {x : X} {p : DiscreteTiling.Prototile G X},
  x ∈ ↑p ↔ x ∈ p
-- Init.Omega.Coeffs
/-- Shim for `IntList.get`.  -/
Lean.Omega.Coeffs.get : Lean.Omega.Coeffs → ℕ → ℤ
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncate.eq_1 : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)],
  WittVector.truncate n =
    { toFun := WittVector.truncateFun n, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.snd.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  OrderMonoidHom.snd α β = { toMonoidHom := MonoidHom.snd α β, monotone' := ⋯ }
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.instIsScalarTowerInteger : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {ΓR : Type u_6}
  {ΓA : Type u_7} [inst_3 : LinearOrderedCommGroupWithZero ΓR] [inst_4 : LinearOrderedCommGroupWithZero ΓA]
  {vR : Valuation R ΓR} {vA : Valuation A ΓA} [inst_5 : vR.HasExtension vA], IsScalarTower (↥vR.integer) (↥vA.integer) A
-- Lean.Level
_private.Lean.Level.0.Lean.Level.normLtAux.match_1.eq_1 : ∀ (motive : Lean.Level → ℕ → Lean.Level → ℕ → Sort u_1) (l₁ : Lean.Level) (k₁ : ℕ) (l₂ : Lean.Level) (k₂ : ℕ)
  (h_1 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁.succ k₁ l₂ k₂)
  (h_2 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂.succ k₂)
  (h_3 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.max l₁₂ →
        (k₁ : ℕ) → (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.max l₂₂ → (k₂ : ℕ) → motive (l₁₁.max l₁₂) k₁ (l₂₁.max l₂₂) k₂)
  (h_4 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.imax l₁₂ →
        (k₁ : ℕ) →
          (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.imax l₂₂ → (k₂ : ℕ) → motive (l₁₁.imax l₁₂) k₁ (l₂₁.imax l₂₂) k₂)
  (h_5 :
    (n₁ : Lean.Name) →
      (k₁ : ℕ) → (n₂ : Lean.Name) → (k₂ : ℕ) → motive (Lean.Level.param n₁) k₁ (Lean.Level.param n₂) k₂)
  (h_6 :
    (n₁ : Lean.LMVarId) →
      (k₁ : ℕ) → (n₂ : Lean.LMVarId) → (k₂ : ℕ) → motive (Lean.Level.mvar n₁) k₁ (Lean.Level.mvar n₂) k₂)
  (h_7 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂ k₂),
  (match l₁.succ, k₁, l₂, k₂ with
    | l₁.succ, k₁, l₂, k₂ => h_1 l₁ k₁ l₂ k₂
    | l₁, k₁, l₂.succ, k₂ => h_2 l₁ k₁ l₂ k₂
    | l₁@h:(l₁₁.max l₁₂), k₁, l₂@h_8:(l₂₁.max l₂₂), k₂ => h_3 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | l₁@h:(l₁₁.imax l₁₂), k₁, l₂@h_8:(l₂₁.imax l₂₂), k₂ => h_4 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ => h_5 n₁ k₁ n₂ k₂
    | Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ => h_6 n₁ k₁ n₂ k₂
    | l₁, k₁, l₂, k₂ => h_7 l₁ k₁ l₂ k₂) =
    h_1 l₁ k₁ l₂ k₂
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.small_fullSubcategory_filteredClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  (f : α → C), Small.{max v w, u} (CategoryTheory.IsFiltered.filteredClosure f).FullSubcategory
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_eq_comap_of_inverse : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {g : N →* G},
  Function.LeftInverse ⇑g ⇑f → Function.RightInverse ⇑g ⇑f → ∀ (H : Subgroup G), Subgroup.map f H = Subgroup.comap g H
-- Init.Data.String.Lemmas.StringOrder
String.not_lt : ∀ {a b : String}, ¬a < b ↔ b ≤ a
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Any regular Haar measure is invariant under inversion in an abelian group.  -/
MeasureTheory.Measure.IsHaarMeasure.isInvInvariant_of_regular : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [LocallyCompactSpace G] [μ.Regular], μ.IsInvInvariant
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.coe_sSup_apply : ∀ {E : Type u_3} [inst : AddGroup E] {s : Set (NonarchAddGroupSeminorm E)},
  BddAbove s → ∀ {x : E}, (sSup s) x = ⨆ p, ↑p x
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- If `F ⊣ G` is an adjunction, the `G` is lax monoidal iff `F` is oplax monoidal.
It is advisable to use `Adjunction.leftAdjointOplaxMonoidal` and
`Adjunction.rightAdjointLaxMonoidal`, because compatibilities between
the oplax monoidal left adjoint and the lax monoidal right adjoint
(`Adjunction.IsMonoidal`) have been stated for these definitions.  -/
CategoryTheory.Adjunction.laxMonoidalEquivOplaxMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} → (F ⊣ G) → G.LaxMonoidal ≃ F.OplaxMonoidal
-- Mathlib.ModelTheory.Topology.Types
CompleteType.isOpen_typesWith : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1} (φ : (L.withConstants α).Sentence), IsOpen (T.typesWith φ)
-- Mathlib.Logic.Embedding.Basic
/-- Given an equivalence to a subtype, produce an embedding to the elements of the corresponding
set.  -/
Equiv.asEmbedding : {β : Sort u_1} → {α : Sort u_2} → {p : β → Prop} → α ≃ Subtype p → α ↪ β
-- Init.Data.SInt.Lemmas
UInt16.toInt16_mul : ∀ (a b : UInt16), (a * b).toInt16 = a.toInt16 * b.toInt16
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_le_iff_le_mul : ∀ {k x y : ℤ}, 0 < k → (x / k ≤ y ↔ x < y * k + k)
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.monday.sizeOf_spec : sizeOf Std.Time.Weekday.monday = 1
-- Mathlib.Order.KrullDimension
/-- **Alias** of the reverse direction of `Order.coheight_eq_zero`.

---

The elements of coheight zero are the maximal elements.  -/
Order.IsMax.coheight_eq_zero : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, IsMax x → Order.coheight x = 0
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- `ZeroMemClass S M` says `S` is a type of subsets `s ≤ M`, such that `0 ∈ s` for all `s`.  -/
ZeroMemClass : (S : Type u_3) → (M : outParam (Type u_4)) → [Zero M] → [SetLike S M] → Prop
-- Mathlib.GroupTheory.Index
/-- If `J` has finite index in `K`, then `J ⊓ L` has finite index in `K ⊓ L` for any
`L`.  -/
AddSubgroup.relIndex_inter_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {J K : AddSubgroup G},
  J.relIndex K ≠ 0 → ∀ (L : AddSubgroup G), (J ⊓ L).relIndex (K ⊓ L) ≠ 0
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.ι_mul_ι_comm_of_isOrtho : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {a b : M},
  QuadraticMap.IsOrtho Q a b →
    (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b = -((CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.not_measurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M) {i : Set α}, ¬MeasurableSet i → v i = 0
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.posixParseSign : Std.Internal.Parsec.String.Parser ℤ
-- Mathlib.Algebra.Group.Defs
/-- A commutative monoid is a monoid with commutative `(*)`.  -/
CommMonoid : Type u → Type u
-- Mathlib.Algebra.Lie.Abelian
LieModule.maxTrivEquiv_of_equiv_symm_eq_symm : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (e : M ≃ₗ⁅R,L⁆ N), (LieModule.maxTrivEquiv e).symm = LieModule.maxTrivEquiv e.symm
-- Mathlib.Data.Matrix.Mul
Matrix.mul_sub : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype n]
  (M : Matrix m n α) (N N' : Matrix n o α), M * (N - N') = M * N - M * N'
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_iInter : ∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Sort u_5} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {f : ι → Set E},
  (∀ (i : ι), Balanced 𝕜 (f i)) → Balanced 𝕜 (⋂ i, f i)