mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.ext_iff : ∀ {α : Type w} {x y : Std.Iterators.Types.ArrayIterator α}, x = y ↔ x.array = y.array ∧ x.pos = y.pos
-- Mathlib.FieldTheory.Separable
Algebra.isSeparable_self : ∀ (F : Type u_1) [inst : Field F], Algebra.IsSeparable F F
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 16-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^16 - 1` for natural numbers greater than or equal to `2^16`.
 -/
UInt16.ofNatTruncate : ℕ → UInt16
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.commShiftIso_add' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] {a b c : A}
  (h : a + b = c),
  CategoryTheory.Functor.commShiftIso F c =
    CategoryTheory.Functor.CommShift.isoAdd' h (CategoryTheory.Functor.commShiftIso F a)
      (CategoryTheory.Functor.commShiftIso F b)
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.bind.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → (α → Option β) → Sort u_3) (x : α → Option β)
  (h_1 : (x : α → Option β) → motive none x) (h_2 : (a : α) → (f : α → Option β) → motive (some a) f),
  (match none, x with
    | none, x => h_1 x
    | some a, f => h_2 a f) =
    h_1 x
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.instField : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] → [inst_1 : PartialOrder S] → [inst_2 : Field R] → (v : AbsoluteValue R S) → Field (WithAbs v)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.map_map_equiv : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} {δ : α → Type w'}
  {f : (a : α) → β a → γ a} {g : (a : α) → γ a → δ a},
  (Std.DTreeMap.map g (Std.DTreeMap.map f t)).Equiv (Std.DTreeMap.map (fun k v => g k (f k v)) t)
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.Scheme.Hom.coborderRange.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst : AlgebraicGeometry.IsImmersion f],
  AlgebraicGeometry.Scheme.Hom.coborderRange f = AlgebraicGeometry.Scheme.Hom.coborderRange f_1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q),
  (CochainComplex.HomComplex.Cochain.fromSingleEquiv h) (CochainComplex.HomComplex.Cochain.fromSingleMk f h) = f
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.instCoeConnectedConnectedElemVertsCoe : {V : Type u} → {G : SimpleGraph V} → {H : G.Subgraph} → Coe H.Connected H.coe.Connected
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk.sizeOf_spec : ∀ {Γ : Type u_1} [inst : Inhabited Γ] [inst_1 : SizeOf Γ] (head : Γ) (left right : Turing.ListBlank Γ),
  sizeOf { head := head, left := left, right := right } = 1 + sizeOf head + sizeOf left + sizeOf right
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited γ] {f : α → β → γ} {k k' : α},
  t.getKey? k = some k' → (Std.TreeMap.map f t)[k]! = (Option.map (f k') t[k]?).get!
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.FGEquiv.symm_coe : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.FGEquiv M N), ↑f.symm = (↑f).symm
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- When `C` has enough injective,
`Injective.d f : Y ⟶ syzygies f` is the composition
`cokernel.π f ≫ ι (cokernel f)`.

(When `C` is abelian, we have `exact f (injective.d f)`.)
 -/
CategoryTheory.Injective.d : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.EnoughInjectives C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {X Y : C} →
          (f : X ⟶ Y) → [inst_3 : CategoryTheory.Limits.HasCokernel f] → Y ⟶ CategoryTheory.Injective.syzygies f
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Filter.IsIncreasingApproximateUnit.mk : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {l : Filter A},
  l.IsApproximateUnit → (∀ᶠ (x : A) in l, 0 ≤ x) → (∀ᶠ (x : A) in l, ‖x‖ ≤ 1) → l.IsIncreasingApproximateUnit
-- Mathlib.Analysis.Convex.StdSimplex
/-- `stdSimplex 𝕜 ι` is a subset of the unit cube  -/
stdSimplex_subset_Icc : ∀ (𝕜 : Type u_2) {ι : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι]
  [IsOrderedAddMonoid 𝕜], stdSimplex 𝕜 ι ⊆ Set.Icc 0 1
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.toEquiv_symm : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  e.symm.toEquiv = e.toEquiv.symm
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.coeff_supportedEquivFinsupp_symm_apply_coe_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M) (a : ↑s →₀ S) (a_1 : M),
  (↑((MonoidAlgebra.supportedEquivFinsupp s).symm a)).coeff a_1 = if h : a_1 ∈ s then a ⟨a_1, h⟩ else 0
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_mul : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f g : Module.End R M),
  LinearMap.baseChange A (f * g) = LinearMap.baseChange A f * LinearMap.baseChange A g
-- Mathlib.Data.QPF.Univariate.Basic
/-- does recursion on `q.P.M` using `g : α → F α` rather than `g : α → P α`  -/
QPF.corecF : {F : Type u → Type u} → [q : QPF F] → {α : Type u} → (α → F α) → α → (QPF.P F).M
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addGroup : {α : Type u} → [Group α] → AddGroup (Additive α)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_le_iff_le_one_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [PosMulMono α]
  [PosMulReflectLE α], 0 < a → (a * b ≤ a ↔ b ≤ 1)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mapEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (g : P ≃ₐ[R] P'),
  (FractionalIdeal.mapEquiv g).symm = FractionalIdeal.mapEquiv g.symm
-- Lean.Setup
Lean.instInhabitedModuleArtifacts : Inhabited Lean.ModuleArtifacts
-- Mathlib.Data.Fintype.Perm
/-- The collection of permutations of a fintype is a fintype.  -/
fintypePerm : {α : Type u_1} → [DecidableEq α] → [Fintype α] → Fintype (Equiv.Perm α)
-- Mathlib.Topology.Homotopy.Basic
/-- Casting a `HomotopyWith f₀ f₁ P` to a `HomotopyWith g₀ g₁ P` where `f₀ = g₀` and `f₁ = g₁`.
 -/
ContinuousMap.HomotopyWith.cast : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {P : C(X, Y) → Prop} → {f₀ f₁ g₀ g₁ : C(X, Y)} → f₀.HomotopyWith f₁ P → f₀ = g₀ → f₁ = g₁ → g₀.HomotopyWith g₁ P
-- Mathlib.Order.Heyting.Basic
PUnit.compl_eq : ∀ (a : PUnit.{u + 1}), aᶜ = PUnit.unit
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f)
  (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)}
  (h : (F.map f₂₃).toFunctor.obj ((F.map f₁₂).toFunctor.obj ((F.map f₀₁).toFunctor.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
        h) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp
        ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) h)
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.integral_condCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ),
  ∫ (a : α), ↑(ProbabilityTheory.condCDF ρ a) x ∂ρ.fst = ρ.real (Set.univ ×ˢ Set.Iic x)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.bijOn_sumElim_conjugate : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  Set.BijOn
    (Sum.elim NumberField.InfinitePlace.embedding
      (NumberField.ComplexEmbedding.conjugate ∘ NumberField.InfinitePlace.embedding))
    (Set.sumEquiv.symm
      (NumberField.InfinitePlace.ramifiedPlacesOver L v, NumberField.InfinitePlace.ramifiedPlacesOver L v))
    (NumberField.ComplexEmbedding.mixedEmbeddingsOver L v.embedding)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.add_antiperiod_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [inst : AddMonoid α] [inst_1 : Neg β],
  Function.Periodic f c₁ → Function.Antiperiodic f c₂ → f (c₁ + c₂) = -f 0
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mkHom_id_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e : C ≌ D},
  CategoryTheory.Equivalence.mkHom (CategoryTheory.CategoryStruct.id e.functor) = CategoryTheory.CategoryStruct.id e
-- Mathlib.Topology.Order.Real
EReal.instOrderTopology : OrderTopology EReal
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An invariant block of a group action is a fixed block.  -/
AddAction.IsInvariantBlock.isFixedBlock : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsInvariantBlock G B → AddAction.IsFixedBlock G B
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffOn.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {ι : Type u_3} {f : ι → E → F} {s : Finset ι} {t : Set E},
  (∀ i ∈ s, ContDiffOn 𝕜 n (fun x => f i x) t) → ContDiffOn 𝕜 n (fun x => ∑ i ∈ s, f i x) t
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0)
  (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0)
  (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f),
  (CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).right =
    CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionParams.toWorkDoneProgressParams : Lean.Lsp.CodeActionParams → Lean.Lsp.WorkDoneProgressParams
-- Mathlib.Analysis.RCLike.Basic
RCLike.realRingEquiv.congr_simp : ∀ {K : Type u_1} [inst : RCLike K] (h : RCLike.I = 0), RCLike.realRingEquiv h = RCLike.realRingEquiv h
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is equicontinuous at some `x₀` within a set `S`, the same is true for its
closure in *any* topology for which evaluation at any `x ∈ S ∪ {x₀}` is continuous. Since
this will be applied to `DFunLike` types, we state it for any topological space with a map
to `X → α` satisfying the right continuity conditions. See also `Set.EquicontinuousWithinAt.closure`
for a more familiar (but weaker) statement.

Note: This could *technically* be called `EquicontinuousWithinAt.closure` without name clashes
with `Set.EquicontinuousWithinAt.closure`, but we don't do it because, even with a `protected`
marker, it would introduce ambiguities while working in namespace `Set` (e.g, in the proof of
any theorem called `Set.something`).  -/
EquicontinuousWithinAt.closure' : ∀ {X : Type u_3} {Y : Type u_5} {α : Type u_6} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [uα : UniformSpace α]
  {A : Set Y} {u : Y → X → α} {S : Set X} {x₀ : X},
  EquicontinuousWithinAt (u ∘ Subtype.val) S x₀ →
    Continuous (S.domRestrict ∘ u) → Continuous (Function.eval x₀ ∘ u) → EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- Two linear maps `S` and `T` are equal, if and only if the identity `⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ` holds
for all `x`.
 -/
ext_inner_map : ∀ {V : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (S T : V →ₗ[ℂ] V),
  (∀ (x : V), inner ℂ (S x) x = inner ℂ (T x) x) ↔ S = T
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.instInfiniteColoringOfNonempty : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} [Nonempty (G.Coloring α)] [Infinite α] [Nonempty V],
  Infinite (G.Coloring α)
-- Mathlib.Data.EReal.Operations
EReal.neg_lt_neg_iff : ∀ {a b : EReal}, -a < -b ↔ b < a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, k ∉ t → l.contains k = false → (t.insertMany l).get? k = none
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.exists_nonzero_eq_adjoin_mul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {s : S},
  IsAlgebraic R s → s ∈ nonZeroDivisors S → ∃ t ∈ R[s], ∃ r, r ≠ 0 ∧ s * t = (algebraMap R S) r
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.autMap_apply_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {A B : C}
  [inst_2 : CategoryTheory.PreGaloisCategory.IsConnected A] [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois B]
  (f : A ⟶ B) (σ τ : CategoryTheory.Aut A),
  CategoryTheory.PreGaloisCategory.autMap f (σ * τ) =
    CategoryTheory.PreGaloisCategory.autMap f σ * CategoryTheory.PreGaloisCategory.autMap f τ
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.cauchy_complete_eLpNorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] [CompleteSpace E],
  1 ≤ p →
    ∀ {f : ℕ → α → E},
      (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
        ∀ {B : ℕ → ENNReal},
          ∑' (i : ℕ), B i ≠ ⊤ →
            (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → MeasureTheory.eLpNorm (f n - f m_1) p μ < B N) →
              ∃ f_lim,
                MeasureTheory.MemLp f_lim p μ ∧
                  Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω}
  {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω},
  MeasurableSet E → Filter.limsup (fun i => (μs i) Eᶜ) L ≤ μ Eᶜ → μ E ≤ Filter.liminf (fun i => (μs i) E) L
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.memberSubfamily_nonMemberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {a : α},
  Finset.memberSubfamily a (Finset.nonMemberSubfamily a 𝒜) = ∅
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainAddEquiv_trans : ∀ {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] (e₁ : M ≃ N) (e₂ : N ≃ O),
  AddMonoidAlgebra.mapDomainAddEquiv R (e₁.trans e₂) =
    (AddMonoidAlgebra.mapDomainAddEquiv R e₁).trans (AddMonoidAlgebra.mapDomainAddEquiv R e₂)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E → F} {g : F → G},
  IsBoundedLinearMap 𝕜 g → IsBoundedLinearMap 𝕜 f → IsBoundedLinearMap 𝕜 (g ∘ f)
-- Mathlib.Topology.Algebra.Order.Group
/-- In a nontrivial densely linearly ordered additive group,
the integer multiples of an element can't be dense.  -/
not_denseRange_zsmul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G] [Nontrivial G] [DenselyOrdered G] {a : G}, ¬DenseRange fun x => x • a
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.pow_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [Nontrivial α] {a : Associates α}
  {k : ℕ}, (a ^ k).factors = k • a.factors
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
RingHom.FiniteType.exists_smallRepr : ∀ (R : Type u) [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] {f : R →+* S},
  f.FiniteType → ∃ T e, f = e.toRingHom.comp (algebraMap R ↑(FGAlgCatSkeleton.eval R T).obj)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.node3R.eq_1 : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α),
  l.node3R x m y r = l.node' x (m.node' y r)
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.instInhabitedExtensionState : {a : Type} → Inhabited (Lean.KeyedDeclsAttribute.ExtensionState a)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.QuasiSeparated.of_quasiSeparatedSpace : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [QuasiSeparatedSpace ↥X], AlgebraicGeometry.QuasiSeparated f
-- Lean.Elab.DocString
Lean.Doc.CodeBlockSuggestion.mk.injEq : ∀ (name : Lean.Name) (args moreInfo : Option String) (name_1 : Lean.Name) (args_1 moreInfo_1 : Option String),
  ({ name := name, args := args, moreInfo := moreInfo } = { name := name_1, args := args_1, moreInfo := moreInfo_1 }) =
    (name = name_1 ∧ args = args_1 ∧ moreInfo = moreInfo_1)
-- Mathlib.CategoryTheory.Localization.Prod
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_uniq : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {E : Type u₅} [inst_2 : CategoryTheory.Category.{v₅, u₅} E]
  (F₁ F₂ : CategoryTheory.Functor (W₁.Localization × W₂.Localization) E),
  (W₁.Q.prod W₂.Q).comp F₁ = (W₁.Q.prod W₂.Q).comp F₂ → F₁ = F₂
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.totallyBounded_principal_iff : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, (Filter.principal s).TotallyBounded ↔ TotallyBounded s
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParams.Info.mk.injEq : ∀ (graph : Array (Array (Option (Array (Option ℕ))))) (revDeps : Array (Array (Array ℕ)))
  (graph_1 : Array (Array (Option (Array (Option ℕ))))) (revDeps_1 : Array (Array (Array ℕ))),
  ({ graph := graph, revDeps := revDeps } = { graph := graph_1, revDeps := revDeps_1 }) =
    (graph = graph_1 ∧ revDeps = revDeps_1)
-- Init.Prelude
HAnd.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HAnd α β γ
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M]
  [Module.Finite R M] {rs : List R},
  (∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson) →
    (RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M rs)
-- Mathlib.Data.Set.NAry
Set.image2_inter_subset_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β},
  Set.image2 f s (t ∩ t') ⊆ Set.image2 f s t ∩ Set.image2 f s t'
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_mul : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (f g : M₁ →L[R₁] M₁), ↑(f * g) = ↑f * ↑g
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
MvQPF.Comp.inst : {n m : ℕ} →
  {F : TypeVec.{u} n → Type u_1} →
    {G : Fin2 n → TypeVec.{u} m → Type u} → [MvQPF F] → [(i : Fin2 n) → MvQPF (G i)] → MvQPF (MvQPF.Comp F G)
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyIrreducible : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.GeometricallyIrreducible
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.mkDerivation_X : ∀ {σ : Type u_1} (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] [inst_4 : IsScalarTower R (MvPolynomial σ R) A] (f : σ → A) (i : σ),
  (MvPolynomial.mkDerivation R f) (MvPolynomial.X i) = f i
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.eq_sub_iff : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b c : α}, IsAddUnit c → (a = b - c ↔ a + c = b)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The action by a subalgebra is the action by the underlying algebra.  -/
Subalgebra.instDistribMulActionSubtypeMem : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {α : Type u_1} →
            [inst_3 : AddMonoid α] → [DistribMulAction A α] → (S : Subalgebra R A) → DistribMulAction (↥S) α
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_trans : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (g : P ≃ₗ[R] Q)
  (f : N ≃ₗ[R] P), LinearEquiv.lTensor M (f ≪≫ₗ g) = LinearEquiv.lTensor M f ≪≫ₗ LinearEquiv.lTensor M g
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.domCongr_support : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N) (x : MonoidAlgebra A M),
  ((MonoidAlgebra.domCongr R A e) x).coeff.support = Finset.map (↑e).toEmbedding x.coeff.support
-- Mathlib.InformationTheory.Coding.UniquelyDecodable
/-- A set of lists is uniquely decodable if distinct concatenations yield distinct strings.  -/
InformationTheory.UniquelyDecodable : {α : Type u_1} → Set (List α) → Prop
-- Mathlib.Order.WellQuasiOrder
Finite.to_wellQuasiOrderedLE : ∀ {α : Type u_1} [inst : Preorder α] [Finite α], WellQuasiOrderedLE α
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.M : Type → Type