mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instDecidableLtOffset : {x y : Std.Time.Hour.Offset} → Decidable (x < y)
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.monadToMon_map_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Monad C} (f : X ⟶ Y),
  ((CategoryTheory.Monad.monadToMon C).map f).hom = f.toNatTrans
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.toLinearMap_smul : ∀ {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : Module S V] [inst_5 : AddCommMonoid W]
  [inst_6 : Module R W] [inst_7 : Module S W] [inst_8 : SMulCommClass R S W] [inst_9 : SMul S R]
  [inst_10 : IsScalarTower S R V] [inst_11 : IsScalarTower S R W] (e : V ≃ₗ[R] W) (α : Sˣ), ↑(α • e) = ↑α • ↑e
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    MeasureTheory.IsAddFundamentalDomain G t μ →
      ∀ (f : α → ENNReal), (∀ (g : G) (x : α), f (g +ᵥ x) = f x) → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
-- Aesop.Util.EqualUpToIds
_private.Aesop.Util.EqualUpToIds.0.Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃.compareMVarValues : Aesop.EqualUpToIds.MVarValue → Aesop.EqualUpToIds.MVarValue → Aesop.EqualUpToIds.ExprsEqualUpToIdsM Bool
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- This lemma uses the simp-normal form `⇑(A.adjoint) ∘ ⇑A` instead of `⇑(A.adjoint ∘ₗ A)`
(note the difference between `∘` and `∘ₗ`).
You may need to rewrite with `LinearMap.coe_comp` before applying this lemma.
 -/
LinearMap.adjoint_comp_self_injective_iff : ∀ {𝕜 : 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),
  Function.Injective (⇑(LinearMap.adjoint A) ∘ ⇑A) ↔ Function.Injective ⇑A
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- the diagonal of the (pre)path object  -/
HomotopicalAlgebra.PrepathObject.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {A : C} → (self : HomotopicalAlgebra.PrepathObject A) → A ⟶ self.P
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.zero_add : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.AddMonObj X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.zero X)
      CategoryTheory.AddMonObj.add =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_modify_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ [Inhabited α] {k fallback : α} {f : β k → β k},
      (m.modify k f).getKeyD k fallback = if m.contains k = true then k else fallback
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- A linear map that sends an orthonormal basis to orthonormal vectors is a linear isometry.  -/
LinearMap.isometryOfOrthonormal : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {ι : Type u_4} →
            {E' : Type u_7} →
              [inst_3 : SeminormedAddCommGroup E'] →
                [inst_4 : InnerProductSpace 𝕜 E'] →
                  (f : E →ₗ[𝕜] E') → {v : Module.Basis ι 𝕜 E} → Orthonormal 𝕜 ⇑v → Orthonormal 𝕜 (⇑f ∘ ⇑v) → E →ₗᵢ[𝕜] E'
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.prodLeftIsoPullback_inv_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X)
  [inst_1 : CategoryTheory.Limits.HasPullback Y.hom Z.hom] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  {Z_1 : C} (h : Y.left ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.fst) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst Y.hom Z.hom) h
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.constantsToVars.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (_n : ℕ) (f : (L.withConstants γ).Functions (_n + 1))
  (ts : Fin (_n + 1) → (L.withConstants γ).Term α),
  (FirstOrder.Language.func f ts).constantsToVars =
    Sum.casesOn f (fun f => FirstOrder.Language.func f fun i => (ts i).constantsToVars) fun c => isEmptyElim c
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.objIsoOfEq_rfl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I),
  X.objIsoOfEq ⋯ = CategoryTheory.Iso.refl (X.obj i)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algEquivOfTranscendental_symm_aeval : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : L)
  (h : Transcendental K f) (g : Polynomial K),
  (RatFunc.algEquivOfTranscendental f h).symm ((Polynomial.aeval (IntermediateField.AdjoinSimple.gen K f)) g) =
    (algebraMap (Polynomial K) (RatFunc K)) g
-- Init.Data.String.Basic
String.Slice.Pos.cast_inj : ∀ {s t : String.Slice} {hst : s.copy = t.copy} {p q : s.Pos}, p.cast hst = q.cast hst ↔ p = q
-- Init.Data.SInt.Lemmas
Int64.toInt_div_of_ne_right : ∀ (a b : Int64), b ≠ -1 → (a / b).toInt = a.toInt.tdiv b.toInt
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSMul'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [inst : SMul M β],
  Filter.Germ.instSMul' = { smul := Filter.Germ.map₂ fun x1 x2 => x1 • x2 }
-- Mathlib.RingTheory.Localization.Defs
Localization.instUniqueLocalization : {R : Type u_1} → [inst : CommSemiring R] → {M : Submonoid R} → [Subsingleton R] → Unique (Localization M)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- Convert an unbundled `IsAbsoluteValue` to a bundled `AbsoluteValue`.  -/
IsAbsoluteValue.toAbsoluteValue : {S : Type u_5} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_6} → [inst_2 : Semiring R] → (abv : R → S) → [IsAbsoluteValue abv] → AbsoluteValue R S
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodCartanEquiv_aux : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {R : Type u_5} [inst_4 : CommRing R] [inst_5 : LieAlgebra R L₁]
  {H₁ : LieSubalgebra R L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_6 : LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂}
  (b₂ : LieAlgebra.Basis ι₂ H₂),
  Set.InjOn ⇑(LinearMap.fst R L₁ L₂) ↑(Submodule.span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
-- Mathlib.Analysis.Normed.MulAction
NormSMulClass.mk : ∀ {α : Type u_3} {β : Type u_4} [inst : Norm α] [inst_1 : Norm β] [inst_2 : SMul α β],
  (∀ (r : α) (x : β), ‖r • x‖ = ‖r‖ * ‖x‖) → NormSMulClass α β
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.dotProduct_toMatrix_mulVec : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (x y : n → R₁),
  x ⬝ᵥ ((LinearMap.BilinForm.toMatrix b) B).mulVec y = (B (b.equivFun.symm x)) (b.equivFun.symm y)
-- Mathlib.Algebra.Category.MonCat.Adjunctions
/-- The free-forgetful adjunction for monoids.  -/
MonCat.adj : MonCat.free ⊣ CategoryTheory.forget MonCat
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instLinearOrderedCommGroupWithZero : {α : Type u_1} →
  [inst : CommGroup α] → [inst_1 : LinearOrder α] → [IsOrderedMonoid α] → LinearOrderedCommGroupWithZero (WithZero α)
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- **Alias** of `AddHomClass.isAddFreimanHom`. -/
AddMonoidHomClass.isAddFreimanHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α}
  {B : Set β} {n : ℕ} [inst_2 : FunLike F α β] [AddHomClass F α β] (f : F),
  Set.MapsTo (⇑f) A B → IsAddFreimanHom n A B ⇑f
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.iIndepFun.integrable_exp_mul_sum : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ}
  [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ},
  ProbabilityTheory.iIndepFun X μ →
    (∀ (i : ι), Measurable (X i)) →
      ∀ {s : Finset ι},
        (∀ i ∈ s, MeasureTheory.Integrable (fun ω => Real.exp (t * X i ω)) μ) →
          MeasureTheory.Integrable (fun ω => Real.exp (t * (∑ i ∈ s, X i) ω)) μ
-- Mathlib.Order.Filter.Pointwise
Filter.one_le_div_iff : ∀ {α : Type u_2} [inst : Group α] {f g : Filter α}, 1 ≤ f / g ↔ ¬Disjoint f g
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
AnalyticOn.sigmoid : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  AnalyticOn ℝ f s → AnalyticOn ℝ (Real.sigmoid ∘ f) s
-- Batteries.Data.MLList.Basic
/-- Convert any value in the monad to the singleton monadic lazy list.  -/
MLList.monadLift : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → m α → MLList m α
-- Mathlib.Order.InitialSeg
PrincipalSeg.toRelEmbedding : {α : Type u_4} → {β : Type u_5} → {r : α → α → Prop} → {s : β → β → Prop} → PrincipalSeg r s → r ↪r s
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- `MeromorphicNFOn` is invariant under translation, special case where the set is a sphere.  -/
meromorphicNFOn_sphere_comp_sub_const_iff_meromorphicNFOn_sphere : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicNFOn (f ∘ fun x => x - c) (Metric.sphere c R) ↔ MeromorphicNFOn f (Metric.sphere 0 R)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.memLp_one_iff_integrable : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε}, MeasureTheory.MemLp f 1 μ ↔ MeasureTheory.Integrable f μ
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_eq_fdiv : ∀ {a b : ℤ},
  a.tdiv b =
    a.fdiv b + if b ∣ a then 0 else if 0 ≤ a then if 0 ≤ b then 0 else 1 else if 0 ≤ b then b.sign else 1 + b.sign
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainNonUnitalRingHom_comp : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [inst : Semiring R] [inst_1 : Add M] [inst_2 : Add N]
  [inst_3 : Add O] (f : N →ₙ+ O) (g : M →ₙ+ N),
  AddMonoidAlgebra.mapDomainNonUnitalRingHom R (f.comp g) =
    (AddMonoidAlgebra.mapDomainNonUnitalRingHom R f).comp (AddMonoidAlgebra.mapDomainNonUnitalRingHom R g)
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.ParseResult.success.sizeOf_spec : ∀ {α ι : Type} [inst : SizeOf α] [inst_1 : SizeOf ι] (pos : ι) (res : α),
  sizeOf (Std.Internal.Parsec.ParseResult.success pos res) = 1 + sizeOf pos + sizeOf res
-- Batteries.Data.ByteArray
ByteArray.get.congr_simp : ∀ (a a_1 : ByteArray) (e_a : a = a_1) (i i_1 : ℕ) (e_i : i = i_1) (h : i < a.size), a.get i h = a_1.get i_1 ⋯
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox.eq_def : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x : α) (a : Ordinal.{u}),
  OrdinalApprox.gfpApprox f x a = x ⊓ ⨅ b, ⨅ (_ : b < a), f (OrdinalApprox.gfpApprox f x b)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.closure_le_normalClosure : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, Subgroup.closure s ≤ Subgroup.normalClosure s
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.not_step_nil : ∀ {α : Type u} {L : List (α × Bool)}, ¬FreeGroup.Red.Step [] L
-- Mathlib.Algebra.Group.Prod
Prod.instMulOneClass.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Prod.instMulOneClass = { toOne := Prod.instOne, toMul := Prod.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.addBottom_head_fst : ∀ {K : Type u_1} {Γ : K → Type u_2} (L : Turing.ListBlank ((k : K) → Option (Γ k))),
  (Turing.TM2to1.addBottom L).head.1 = true
-- Batteries.Data.List.Perm
List.perm_insertP : ∀ {α : Type u_1} (p : α → Bool) (a : α) (l : List α), (List.insertP p a l).Perm (a :: l)
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.flip_surjective_iff₁ : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁],
  Function.Surjective ⇑B.flip ↔ Function.Injective ⇑B
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.hasDimensionLT_iSup_iff : ∀ {X : SSet} {ι : Type u_1} (A : ι → X.Subcomplex) (d : ℕ),
  (⨆ i, A i).toSSet.HasDimensionLT d ↔ ∀ (i : ι), (A i).toSSet.HasDimensionLT d
-- Mathlib.CategoryTheory.Action.Basic
Action.forget_map : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G] {X Y : Action V G}
  (f : X ⟶ Y), (Action.forget V G).map f = f.hom
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.iff_lintegral_lt_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal},
  (∀ᵐ (a : α) ∂μ, f a ≠ ⊤) → (f.FinMeasSupp μ ↔ f.lintegral μ < ⊤)
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.toLinearPMap : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] → {i : M →ₗ[R] N} → {f : M →ₗ[R] Q} → Module.Baer.ExtensionOf i f → N →ₗ.[R] Q
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.cast.congr_simp : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i j : ℕ}
  (h : i = j), TensorPower.cast R M h = TensorPower.cast R M h
-- Mathlib.CategoryTheory.ComposableArrows.One
/-- The natural transformation `functorArrows C i j n ⟶ functorArrows C i' j' n`
when `i ≤ i'` and `j ≤ j'`.  -/
CategoryTheory.ComposableArrows.mapFunctorArrows : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (i j i' j' n : ℕ) →
      (x : autoParam (i ≤ j) CategoryTheory.ComposableArrows.mapFunctorArrows._auto_1) →
        (x_1 : autoParam (i' ≤ j') CategoryTheory.ComposableArrows.mapFunctorArrows._auto_3) →
          autoParam (i ≤ i') CategoryTheory.ComposableArrows.mapFunctorArrows._auto_5 →
            (x_3 : autoParam (j ≤ j') CategoryTheory.ComposableArrows.mapFunctorArrows._auto_7) →
              (x_4 : autoParam (j' ≤ n) CategoryTheory.ComposableArrows.mapFunctorArrows._auto_9) →
                CategoryTheory.ComposableArrows.functorArrows C i j n ⋯ ⋯ ⟶
                  CategoryTheory.ComposableArrows.functorArrows C i' j' n ⋯ ⋯
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The natural projection from a representation to its quotient by a subrepresentation.  -/
Rep.mkQ : {k : Type u} →
  {G : Type v} →
    [inst : Ring k] →
      [inst_1 : Monoid G] →
        (A : Rep.{u_1, u, v} k G) →
          (W : Submodule k ↑A) → (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) → A ⟶ A.quotient W le_comap
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.equiv_of_beq : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  (m₁ == m₂) = true → m₁.Equiv m₂
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t u : Finset β},
  s • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.arrowCongrAddEquiv.congr_simp : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₂ : Type u_14}
  {M₁' : Type u_15} {M₂' : Type u_16} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₁']
  [inst_3 : Semiring R₂'] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid M₁']
  [inst_7 : AddCommMonoid M₂'] [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] [inst_10 : Module R₁' M₁']
  [inst_11 : Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'}
  {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' σ₂₁'_1 : R₂ →+* R₁'} (e_σ₂₁' : σ₂₁' = σ₂₁'_1) {σ₁₂' σ₁₂'_1 : R₁ →+* R₂'}
  (e_σ₁₂' : σ₁₂' = σ₁₂'_1) [inst_12 : RingHomInvPair σ₁₂ σ₂₁] [inst_13 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂']
  [inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ e₁_1 : M₁ ≃ₛₗ[σ₁₂] M₂),
  e₁ = e₁_1 → ∀ (e₂ e₂_1 : M₁' ≃ₛₗ[σ₁'₂'] M₂'), e₂ = e₂_1 → e₁.arrowCongrAddEquiv e₂ = e₁_1.arrowCongrAddEquiv e₂_1
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The Fourier transform of the delta distribution is equal to the volume.

Informally, this is usually represented as `𝓕 δ = 1`.  -/
TemperedDistribution.fourier_delta_zero : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E],
  FourierTransform.fourier (TemperedDistribution.delta 0) = MeasureTheory.volume.toTemperedDistribution
-- Mathlib.Data.DFinsupp.Lex
/-- The linear order on `DFinsupp`s obtained by the lexicographic ordering.  -/
DFinsupp.Lex.linearOrder : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [LinearOrder ι] → [(i : ι) → LinearOrder (α i)] → LinearOrder (Lex (Π₀ (i : ι), α i))
-- Mathlib.Order.Circular
btw_rfl : ∀ {α : Type u_1} [inst : CircularPreorder α] {a : α}, btw a a a
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrderTop.mk.congr_simp : ∀ {α : Type u_1} [inst : Preorder α] (finsetIoi finsetIoi_1 : α → Finset α) (e_finsetIoi : finsetIoi = finsetIoi_1)
  (finsetIci finsetIci_1 : α → Finset α) (e_finsetIci : finsetIci = finsetIci_1)
  (finset_mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x) (finset_mem_Ioi : ∀ (a x : α), x ∈ finsetIoi a ↔ a < x),
  { finsetIoi := finsetIoi, finsetIci := finsetIci, finset_mem_Ici := finset_mem_Ici,
      finset_mem_Ioi := finset_mem_Ioi } =
    { finsetIoi := finsetIoi_1, finsetIci := finsetIci_1, finset_mem_Ici := ⋯, finset_mem_Ioi := ⋯ }
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.outBlock : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- A finsupp `∑ aᵢ·gᵢ : G →₀ A` satisfies the 1-cycle condition if `∑ gᵢ⁻¹ • aᵢ = ∑ aᵢ`.  -/
groupHomology.IsCycle₁ : {G : Type u_1} → {A : Type u_2} → [Inv G] → [inst : AddCommGroup A] → [SMul G A] → (G →₀ A) → Prop
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.disjoint_genEigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] (f : Module.End R M) {μ₁ μ₂ : R},
  μ₁ ≠ μ₂ → ∀ (k l : ℕ∞), Disjoint ((f.genEigenspace μ₁) k) ((f.genEigenspace μ₂) l)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- The difference `f m₁ - f m₂` is controlled in terms of `‖f‖` and `‖m₁ - m₂‖`, precise version.
For a less precise but more usable version, see `norm_image_sub_le`. The bound reads
`‖f m - f m'‖ ≤
  ‖f‖ * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ...`,
where the other terms in the sum are the same products where `1` is replaced by any `i`.  -/
ContinuousMultilinearMap.norm_image_sub_le' : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (f : ContinuousMultilinearMap 𝕜 E G) (m₁ m₂ : (i : ι) → E i),
  ‖f m₁ - f m₂‖ ≤ ‖f‖ * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
-- Mathlib.NumberTheory.ModularForms.Discriminant
_private.Mathlib.NumberTheory.ModularForms.Discriminant.0.ModularForm.term𝕢 : Lean.ParserDescr
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Option.isSome.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : (val : α) → motive (some val))
  (h_2 : Unit → motive none),
  (match some val with
    | some val => h_1 val
    | none => h_2 ()) =
    h_1 val
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N P : C} [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N] [inst_5 : CategoryTheory.AddMonObj P],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P
          (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
            (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add))
          CategoryTheory.AddMonObj.add))
      (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom
        (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P) M
          (CategoryTheory.MonoidalCategoryStruct.tensorObj N P))
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ N P N P)
            (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add
              CategoryTheory.AddMonObj.add))))
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.ΓObjEquivSections_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type w)] [inst_2 : CategoryTheory.HasGlobalSectionsFunctor J (Type w)]
  {F G : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ G) (x : (CategoryTheory.Sheaf.Γ J (Type w)).obj F),
  (CategoryTheory.Sheaf.ΓObjEquivSections J G)
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Sheaf.Γ J (Type w)).map f)) x) =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.sectionsFunctor Cᵒᵖ).map f.hom))
      ((CategoryTheory.Sheaf.ΓObjEquivSections J F) x)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsUnramified.of_restrictScalars : ∀ {k : Type u_1} [inst : Field k] (K : Type u_2) [inst_1 : Field K] {F : Type u_3} [inst_2 : Field F]
  [inst_3 : Algebra k K] [inst_4 : Algebra k F] [inst_5 : Algebra K F] [IsScalarTower k K F]
  {w : NumberField.InfinitePlace F},
  NumberField.InfinitePlace.IsUnramified k w → NumberField.InfinitePlace.IsUnramified K w