mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (y + x, - x)` is measure-preserving.  -/
MeasureTheory.measurePreserving_add_prod_neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] [ν.IsAddLeftInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.2 + z.1, -z.1)) (μ.prod ν) (μ.prod ν)
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.image_coe_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithBot.some '' Set.Icc b a = Set.Icc ↑b ↑a
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_add : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v), (x + y).toCompletion = x.toCompletion + y.toCompletion
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.differentiableOn_one_sub_smoothingFn : DifferentiableOn ℝ (fun z => 1 - AkraBazziRecurrence.smoothingFn z) (Set.Ioi 1)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.map_mono : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {S₁ S₂ : Subalgebra R A} {f : A →ₐ[R] B},
  S₁ ≤ S₂ → Subalgebra.map f S₁ ≤ Subalgebra.map f S₂
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.charPoly.congr_simp : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e e_1 : AddChar ℝ Circle}
  (e_e : e = e_1) {L L_1 : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (e_L : L = L_1) (he : Continuous ⇑e)
  (hL : Continuous fun p => (L p.1) p.2),
  BoundedContinuousFunction.charPoly he hL = BoundedContinuousFunction.charPoly ⋯ ⋯
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.refl : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → {a b : B} → (f : a ⟶ b) → CategoryTheory.BicategoricalCoherence f f
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- The rank of a matrix is at most the size of any finset containing all its nonzero rows.  -/
Matrix.rank_le_card_of_support_subset : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R] [StrongRankCondition R]
  (A : Matrix m n R) (s : Finset m), Function.support A.row ⊆ ↑s → A.rank ≤ s.card
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.mem_fintsupport_iff : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) (i : ι),
  i ∈ ρ.fintsupport x₀ ↔ x₀ ∈ tsupport ⇑(ρ i)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The coercion from `SubDPIdeal` to `Ideal`.  -/
DividedPowers.SubDPIdeal.toIdeal : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → hI.SubDPIdeal → Ideal A
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Ring.hom_ext_iff : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonAssocSemiring (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)]
  [inst_6 : Nonempty ι] {P : Type u_7} [inst_7 : NonAssocSemiring P] {g₁ g₂ : DirectLimit G f →+* P},
  g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (DirectLimit.Ring.of G f i) = g₂.comp (DirectLimit.Ring.of G f i)
-- Std.Data.HashMap.Basic
/-- Creates a hash map from an array of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.HashMap.unitOfArray : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Std.HashMap α Unit
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.isEmptyEquiv_apply_tprod : ∀ (ι : Type u_1) {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] [inst_3 : IsEmpty ι] (f : (i : ι) → s i),
  (PiTensorProduct.isEmptyEquiv ι) ((PiTensorProduct.tprod R) f) = 1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.alwaysInlineAttr : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Bool
-- Mathlib.Algebra.Category.Ring.Basic
/-- The underlying ring hom.  -/
SemiRingCat.Hom.hom' : {R S : SemiRingCat} → R.Hom S → ↑R →+* ↑S
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_iff_isIso_homologyMap : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  QuasiIsoAt f i ↔ CategoryTheory.IsIso (HomologicalComplex.homologyMap f i)
-- Mathlib.Analysis.Seminorm
Seminorm.comp_comp : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {𝕜₃ : Type u_5} {E : Type u_7} {E₂ : Type u_8} {E₃ : Type u_9}
  [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂] [inst_2 : SeminormedRing 𝕜₃] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [inst_3 : RingHomIsometric σ₁₂] {σ₂₃ : 𝕜₂ →+* 𝕜₃} [inst_4 : RingHomIsometric σ₂₃] {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_5 : RingHomIsometric σ₁₃] [inst_6 : AddCommGroup E] [inst_7 : AddCommGroup E₂] [inst_8 : AddCommGroup E₃]
  [inst_9 : Module 𝕜 E] [inst_10 : Module 𝕜₂ E₂] [inst_11 : Module 𝕜₃ E₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  (p : Seminorm 𝕜₃ E₃) (g : E₂ →ₛₗ[σ₂₃] E₃) (f : E →ₛₗ[σ₁₂] E₂), p.comp (g ∘ₛₗ f) = (p.comp g).comp f
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_lineMap_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P)
  (c₁ c₂ : 𝕜), dist ((AffineMap.lineMap p₁ p₂) c₁) ((AffineMap.lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₁ p₂
-- Mathlib.Order.Hom.Bounded
TopHom.dual.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : OrderTop α] [inst_2 : LE β] [inst_3 : OrderTop β],
  TopHom.dual =
    { toFun := fun f => { toFun := ⇑f, map_bot' := ⋯ }, invFun := fun f => { toFun := ⇑f, map_top' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.SetNotation
Set.sInf_eq_sInter : ∀ {α : Type u} (S : Set (Set α)), sInf S = ⋂₀ S
-- Init.Control.Lawful.MonadAttach.Lemmas
LawfulMonadAttach.canReturn_liftM_imp' : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m]
  [LawfulMonad m] [LawfulMonadAttach m] [inst_4 : Monad n] [inst_5 : MonadAttach n] [LawfulMonad n]
  [LawfulMonadAttach n] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n] {x : m α} {a : α},
  MonadAttach.CanReturn (liftM x) a → MonadAttach.CanReturn x a
-- Mathlib.MeasureTheory.Measure.TightNormed
/-- For a sequence of measures indexed by `ℕ`, if the function
`r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop` tends to 0 at infinity, then the set of measures
in the sequence is tight.
Compared to `isTightMeasureSet_of_tendsto_measure_norm_gt`, this lemma replaces a supremum over
all measures by a limsup. This is possible because the sequence is indexed by `ℕ`.  -/
MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt : ∀ {E : Type u_1} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [ProperSpace E]
  {μ : ℕ → MeasureTheory.Measure E} [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)],
  Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖x‖}) Filter.atTop) Filter.atTop (nhds 0) →
    MeasureTheory.IsTightMeasureSet (Set.range μ)
-- Std.Http.Data.URI.Encoding
/-- Converts a byte to its percent-encoded hexadecimal representation (%XX). For example, a space character
(0x20) becomes "%20".
 -/
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedQueryString.byteToHex : {r : UInt8 → Bool} → UInt8 → Std.Http.URI.EncodedQueryString r → Std.Http.URI.EncodedQueryString r
-- Lean.Data.Options
Lean.OptionDeprecation.mk.sizeOf_spec : ∀ (since : String) (text? : Option String), sizeOf { since := since, text? := text? } = 1 + sizeOf since + sizeOf text?
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- A version of `delete_contract_delete` without the disjointness hypothesis,
and hence a less simple RHS.  -/
Matroid.delete_contract_delete' : ∀ {α : Type u_1} (M : Matroid α) (D C D' : Set α),
  ((M.delete D).contract C).delete D' = (M.contract (C \ D)).delete (D ∪ D')
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instInhabited : {α : Type u} → {β : α → Type v} → Inhabited (Std.DHashMap.Raw α β)
-- Mathlib.Data.Finset.Sups
Finset.card_infs_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t : Finset α), (s ⊼ t).card ≤ s.card * t.card
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.le_rank_root : ∀ {self : Batteries.UnionFind} {x : ℕ}, self.rank x ≤ self.rank (self.rootD x)
-- Lean.Message
Lean.SerialMessage.instToString : ToString Lean.SerialMessage
-- Mathlib.Algebra.Quotient
/-- `HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.  -/
HasQuotient.Quotient : (A : outParam (Type u)) → {B : Type v} → [self : HasQuotient A B] → B → Type (max u v)
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.cokernel_G : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤),
  (pres₂.cokernel data hg₁).G = pres₂.G
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : Jᵒᵖ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).inv
      (CategoryTheory.Limits.limit.π F.op j) =
    (CategoryTheory.Limits.colimit.ι F (Opposite.unop j)).op
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.range_projection`. -/
Submodule.IsCompl.projection_range : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), (p.projection q hpq).range = p
-- Mathlib.Order.CompletePartialOrder
CompletePartialOrder.toOrderBot : {α : Type u_4} → [self : CompletePartialOrder α] → OrderBot α
-- Mathlib.Algebra.GroupWithZero.Regular
/-- In a non-trivial `MulZeroClass`, the `0` element is not right-regular.  -/
not_isRightRegular_zero_iff : ∀ {R : Type u_1} [inst : MulZeroClass R], ¬IsRightRegular 0 ↔ Nontrivial R
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
/-- Reinterpret a closed submodule as a closed set.  -/
ClosedSubmodule.toCloseds : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → ClosedSubmodule R M → TopologicalSpace.Closeds M
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticAt.deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} [CompleteSpace F], AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (deriv f) x
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentChangeRegistrationOptions.mk.injEq : ∀ (documentSelector? : Option Lean.Lsp.DocumentSelector) (syncKind : Lean.Lsp.TextDocumentSyncKind)
  (documentSelector?_1 : Option Lean.Lsp.DocumentSelector) (syncKind_1 : Lean.Lsp.TextDocumentSyncKind),
  ({ documentSelector? := documentSelector?, syncKind := syncKind } =
      { documentSelector? := documentSelector?_1, syncKind := syncKind_1 }) =
    (documentSelector? = documentSelector?_1 ∧ syncKind = syncKind_1)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.measurable_log : Measurable Complex.log
-- Init.Data.Int.Lemmas
Int.ofNat_inj : ∀ {m n : ℕ}, ↑m = ↑n ↔ m = n
-- Mathlib.Data.Nat.Nth
Nat.le_nth_of_count_le : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n k : ℕ}, n ≤ Nat.nth p k → Nat.count p n ≤ k
-- Mathlib.Algebra.CharP.Defs
CharP.char_is_prime_of_pos : ∀ (R : Type u_1) [inst : NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] (p : ℕ) [NeZero p] [CharP R p],
  Fact (Nat.Prime p)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.transitivity₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.TransitiveRelation p₁ p₂) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.t (CategoryTheory.CategoryStruct.comp p₂ h) =
    CategoryTheory.CategoryStruct.comp self.c.snd (CategoryTheory.CategoryStruct.comp p₂ h)
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The underlying `Profinite` of a `LightDiagram`.  -/
LightDiagram.toProfinite : LightDiagram → Profinite
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.constantCoeff_X : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.constantCoeff PowerSeries.X = 0
-- Mathlib.NumberTheory.SmoothNumbers
Nat.smoothNumbers_mono : ∀ {N M : ℕ}, N ≤ M → N.smoothNumbers ⊆ M.smoothNumbers
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_insert_le_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} {he : t ≠ ∅},
  (cmp ((t.insert k).min ⋯) (t.min he)).isLE = true
-- Mathlib.Logic.Function.Iterate
Function.iterate_one : ∀ {α : Type u} (f : α → α), f^[1] = f
-- Mathlib.CategoryTheory.PUnit
CategoryTheory.Functor.equiv_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Functor.equiv.unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Discrete.natIso fun x_1 =>
          CategoryTheory.Iso.refl
            (((CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C)).obj x).obj
              x_1))
      ⋯
-- Lean.Util.Heartbeats
/-- Log a message if it looks like we ran out of time.  -/
Lean.reportOutOfHeartbeats : Lean.Name → Lean.Syntax → optParam ℕ 90 → Lean.CoreM Unit
-- Mathlib.CategoryTheory.Idempotents.SimplicialObject
CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsIdempotentComplete C],
  CategoryTheory.IsIdempotentComplete (CategoryTheory.SimplicialObject C)
-- Mathlib.RingTheory.PowerSeries.Basic
/-- Given a formal power series `p` and a subring `T` that contains the
coefficients of `p`, return the corresponding formal power series
whose coefficients are in `T`.  -/
PowerSeries.toSubring : {R : Type u_1} →
  [inst : Ring R] → (p : PowerSeries R) → (T : Subring R) → (∀ (n : ℕ), (PowerSeries.coeff n) p ∈ T) → PowerSeries ↥T
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The categorical product in `Type u` indexed in `Type v`
is the type-theoretic product `Π j, F j`, after shrinking back to `Type u`.  -/
CategoryTheory.Limits.Types.Small.productIso : {J : Type v} → (F : J → Type u) → [inst : Small.{u, v} J] → ∏ᶜ F ≅ Shrink.{u, max u v} ((j : J) → F j)
-- Aesop.RuleTac.GoalDiff
Aesop.isGoalDiffDefeqTarget : Lean.MVarId → Lean.MVarId → Lean.MetaM Bool
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentFilter.language? : Lean.Lsp.DocumentFilter → Option String
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).size = if t.contains k = true then t.size - 1 else t.size
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- `prod F G` is the explicit binary product of type-valued functors `F` and `G`.  -/
CategoryTheory.FunctorToTypes.prod : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor C (Type w) → CategoryTheory.Functor C (Type w) → CategoryTheory.Functor C (Type w)
-- Mathlib.Data.List.NatAntidiagonal
/-- A pair (i, j) is contained in the antidiagonal of `n` if and only if `i + j = n`.  -/
List.Nat.mem_antidiagonal : ∀ {n : ℕ} {x : ℕ × ℕ}, x ∈ List.Nat.antidiagonal n ↔ x.1 + x.2 = n
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
IsDedekindDomain.differentIdeal_dvd_map_differentIdeal : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [FiniteDimensional K L] [inst_10 : IsScalarTower A K L] (R₁ : Type u_5)
  (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [inst_13 : IsDomain R₁] [inst_14 : Algebra A R₁]
  [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B] [inst_18 : Algebra R₁ L]
  [inst_19 : Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂]
  {F₁ F₂ : IntermediateField K L} [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂] [Module.IsTorsionFree R₁ ↥F₁]
  [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L]
  [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [inst_33 : IsDomain A] [inst_34 : IsDedekindDomain B]
  [IsDedekindDomain R₁] [inst_36 : IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁]
  [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [inst_42 : Module.IsTorsionFree R₁ B]
  [Module.IsTorsionFree R₂ B], ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k' (Std.Internal.List.modifyKey k f l) =
      if (k == k') = true then if Std.Internal.List.containsKey k l = true then some k else none
      else Std.Internal.List.getKey? k' l
-- Batteries.Data.List.Lemmas
List.Pairwise.isChain : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l → List.IsChain R l
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord.orderEmbedding_coe : ⇑Cardinal.ord.orderEmbedding = Cardinal.ord
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.modifyGet_StateT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ α : Type u}
  {epost : EPred} (f : σ → α × σ) (post : α → σ → Pred),
  ⦃ fun s => post (f s).1 (f s).2 ⦄ MonadStateOf.modifyGet f ⦃ post; epost ⦄
-- Mathlib.Computability.Reduce
OneOneReducible.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → β} (q : β → Prop),
  Computable f → Function.Injective f → (fun a => q (f a)) ≤₁ q
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_add : ∀ (a b : UInt32), (a + b).toUInt8 = a.toUInt8 + b.toUInt8
-- Mathlib.NumberTheory.NumberField.Ideal.Basic
Ideal.torsionMapQuot_injective : ∀ {K : Type u_1} [inst : Field K] {I : Ideal (NumberField.RingOfIntegers K)} [inst_1 : NumberField K],
  Ideal.absNorm I ≠ 1 →
    (Ideal.absNorm I).Coprime (NumberField.Units.torsionOrder K) → Function.Injective ⇑I.torsionMapQuot
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.instSubsingletonEdgeLabeling : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Subsingleton K], Subsingleton (G.EdgeLabeling K)
-- Mathlib.Topology.Compactness.Paracompact
/-- In a paracompact space, every open covering of a closed set admits a locally finite refinement
indexed by the same type.  -/
precise_refinement_set : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] [ParacompactSpace X] {s : Set X},
  IsClosed s →
    ∀ (u : ι → Set X),
      (∀ (i : ι), IsOpen (u i)) →
        s ⊆ ⋃ i, u i → ∃ v, (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ i, v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
-- Mathlib.Topology.Constructions
exists_finset_piecewise_mem_of_mem_nhds : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] [inst : DecidableEq ι]
  {s : Set ((a : ι) → A a)} {x : (a : ι) → A a}, s ∈ nhds x → ∀ (y : (a : ι) → A a), ∃ I, I.piecewise x y ∈ s
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.instNontrivialNonZeroDivisors : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K],
  Nontrivial (FractionalIdeal (nonZeroDivisors R₁) K)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isSome_get?_eq_contains : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α}, (m.get? a).isSome = m.contains a
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
/-- When `C` is any category, and `D` is a symmetric monoidal category,
the natural pointwise monoidal structure on the functor category `C ⥤ D`
is also symmetric.
 -/
CategoryTheory.Monoidal.functorCategorySymmetric : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [CategoryTheory.SymmetricCategory D] → CategoryTheory.SymmetricCategory (CategoryTheory.Functor C D)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A functor `WithTerminal C ⥤ D` can be seen as an element of the comma category
`Comma (𝟭 (C ⥤ D)) (const C)`.  -/
CategoryTheory.WithTerminal.mkCommaObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor (CategoryTheory.WithTerminal C) D →
          CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C)
-- Std.Sat.AIG.RelabelNat
/-- The map returned by `ofAIG` fulfills the `Inv2` property.
 -/
Std.Sat.AIG.RelabelNat.State.ofAIG.Inv2 : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (aig : Std.Sat.AIG α),
  Std.Sat.AIG.RelabelNat.State.Inv2 aig.decls aig.decls.size (Std.Sat.AIG.RelabelNat.State.ofAIG aig)
-- Mathlib.Algebra.Order.Group.Equiv
/-- `ofLex` as a `MulEquiv`.  -/
ofLexMulEquiv : (α : Type u_1) → [inst : Mul α] → Lex α ≃* α
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.isSymm_adjMatrix : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Zero α] [inst_2 : One α],
  (SimpleGraph.adjMatrix α G).IsSymm
-- Mathlib.GroupTheory.Index
AddSubgroup.IsFiniteRelIndex.relIndex_ne_zero : ∀ {G : Type u_3} {inst : AddGroup G} {H K : AddSubgroup G} [self : H.IsFiniteRelIndex K], H.relIndex K ≠ 0
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- A ball package is a family of balls in a metric space with positive bounded radii.  -/
Besicovitch.BallPackage : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Init.Data.Nat.Basic
Nat.mul_assoc : ∀ (n m k : ℕ), n * m * k = n * (m * k)