mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_eq_getD : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {a : α} {fallback : β} {h : Std.DTreeMap.Internal.Impl.contains a t = true},
      Std.DTreeMap.Internal.Impl.Const.get t a h = Std.DTreeMap.Internal.Impl.Const.getD t a fallback
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_compl_eq_interior_compl : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U : TopologicalSpace.Opens α}, ↑Uᶜ = interior (↑U)ᶜ
-- Mathlib.Data.Multiset.Basic
/-- Given a proof `hp` that there exists a unique `a ∈ l` such that `p a`, `choose p l hp` returns
that `a`.  -/
Multiset.choose : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → (l : Multiset α) → (∃! a, a ∈ l ∧ p a) → α
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k : α}, k ∉ m → l.contains k = false → (m.insertMany l).get? k = none
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.toSubring.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T),
  p.toSubring T hp = ∑ i ∈ p.support, (Polynomial.monomial i) ⟨p.coeff i, ⋯⟩
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Precomposing `f` with `Prod.fst` is `C^n`  -/
ContDiff.fst' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → G},
  ContDiff 𝕜 n f → ContDiff 𝕜 n fun x => f x.1
-- Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
LinearMap.pi.eq_1 : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  {φ : ι → Type i} [inst_3 : (i : ι) → AddCommMonoid (φ i)] [inst_4 : (i : ι) → Module R (φ i)]
  (f : (i : ι) → M₂ →ₗ[R] φ i), LinearMap.pi f = { toFun := fun c i => (f i) c, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
/-- The discrete uniformity makes an additive group a `IsUniformAddGroup`.  -/
instIsUniformAddGroupOfDiscreteUniformity : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : UniformSpace G] [DiscreteUniformity G], IsUniformAddGroup G
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The canonical isomorphism relating `(Span f g).op` and `Cospan f.op g.op`  -/
CategoryTheory.Limits.opSpan : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          (CategoryTheory.Limits.span f g).op ≅
            CategoryTheory.Limits.walkingSpanOpEquiv.functor.comp (CategoryTheory.Limits.cospan f.op g.op)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α], Lex.instCommMonoid = { toMonoid := Lex.instMonoid, mul_comm := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a fallback : α} {v : β},
  (m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.mono : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s.Infinite → t.Infinite
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.add_modEq_right : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] {a b p : M}, a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]
-- Mathlib.Algebra.Order.Pi
Function.one_le_const_of_one_le : ∀ {α : Type u_2} (β : Type u_3) [inst : One α] [inst_1 : Preorder α] {a : α}, 1 ≤ a → 1 ≤ Function.const β a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂)[k]? = none
-- Init.Data.FloatArray.Basic
instToStringFloatArray : ToString FloatArray
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [self : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S}
  {g : Y ⟶ S} [inst : CategoryTheory.Limits.HasPullback f g],
  P g → ∀ (x : ↥X) (y : ↥Y), f x = g y → ∃ a, (CategoryTheory.Limits.pullback.fst f g) a = x
-- Mathlib.ModelTheory.Algebra.Field.Basic
_private.Mathlib.ModelTheory.Algebra.Field.Basic.0.FirstOrder.Field.FieldAxiom.toSentence.match_1.splitter : (motive : FirstOrder.Field.FieldAxiom → Sort u_1) →
  (x : FirstOrder.Field.FieldAxiom) →
    (Unit → motive FirstOrder.Field.FieldAxiom.addAssoc) →
      (Unit → motive FirstOrder.Field.FieldAxiom.zeroAdd) →
        (Unit → motive FirstOrder.Field.FieldAxiom.negAddCancel) →
          (Unit → motive FirstOrder.Field.FieldAxiom.mulAssoc) →
            (Unit → motive FirstOrder.Field.FieldAxiom.mulComm) →
              (Unit → motive FirstOrder.Field.FieldAxiom.oneMul) →
                (Unit → motive FirstOrder.Field.FieldAxiom.existsInv) →
                  (Unit → motive FirstOrder.Field.FieldAxiom.leftDistrib) →
                    (Unit → motive FirstOrder.Field.FieldAxiom.existsPairNE) → motive x
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.coe_valA : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (p : Subalgebra R A), ↑p.valA = p.subtype
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.some_maxEntry_eq_maxEntry? : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β} {he : l.isEmpty = false},
  some (l.maxEntry he) = l.maxEntry?
-- Mathlib.RingTheory.TensorProduct.Finite
/-- Every `x : I ⊗ M` is the image of some `y : J ⊗ M`, where `J ≤ I` is finitely generated,
under the tensor product of `J.inclusion ‹J ≤ I› : J → I` and the identity `M → M`.  -/
Submodule.exists_fg_le_eq_rTensor_inclusion : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {I : Submodule R N}
  (x : TensorProduct R (↥I) M),
  ∃ J, ∃ (_ : J.FG) (hle : J ≤ I), ∃ y, x = (LinearMap.rTensor M (Submodule.inclusion hle)) y
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.symm_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (x : X),
  h.symm (h x) = x
-- Lean.Parser.Term
Lean.Parser.Term.privateDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The underlying morphism  -/
CategoryTheory.RingObjCat.Hom.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → {R₁ R₂ : CategoryTheory.RingObjCat C} → R₁.Hom R₂ → (R₁.X ⟶ R₂.X)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- `RatFunc.X` is the polynomial variable (aka indeterminate).  -/
RatFunc.X : {K : Type u} → [inst : CommRing K] → [IsDomain K] → RatFunc K
-- Init.Data.List.BasicAux
List.le_antisymm : ∀ {α : Type u_1} [inst : LT α] [i : Std.Trichotomous fun x1 x2 => x1 < x2] {as bs : List α}, as ≤ bs → bs ≤ as → as = bs
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.disjoint_vadd_set : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s t : Set β} {a : α},
  Disjoint (a +ᵥ s) (a +ᵥ t) ↔ Disjoint s t
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.preBeth_ord : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → Cardinal.preBeth c.ord = c
-- Init.Data.List.MinMaxIdx
List.minIdxOn?_replicate_of_pos : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.Refl fun x1 x2 => x1 ≤ x2] {n : ℕ} {a : α}
  {f : α → β}, 0 < n → List.minIdxOn? f (List.replicate n a) = some 0
-- Mathlib.Analysis.Convex.PathConnected
/-- Every topological vector space over ℝ is path connected.

Not an instance, because it creates enormous TC subproblems (turn on `pp.all`).
 -/
IsTopologicalAddGroup.pathConnectedSpace : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E], PathConnectedSpace E
-- Lean.Util.PtrSet
Lean.instBEqPtr : {α : Type u_1} → BEq (Lean.Ptr α)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
/-- The subgraph consisting of the vertices and edges of the walk.  -/
SimpleGraph.Walk.toSubgraph : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → G.Subgraph
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Shorthand for the 2nd group cohomology of a `k`-linear `G`-representation `A`, `H²(G, A)`,
defined as the 2nd cohomology of the complex of inhomogeneous cochains of `A`.  -/
groupCohomology.H2 : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ModuleCat k
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The completed L-function of a function `ZMod N → ℂ`, modified by adding multiples of `N ^ (-s) / s`
and `N ^ (-s) / (1 - s)` to make it entire.
 -/
ZMod.completedLFunction₀ : {N : ℕ} → [NeZero N] → (ZMod N → ℂ) → ℂ → ℂ
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mk.injEq : ∀ (cells : Finset (ℕ × ℕ)) (isLowerSet : IsLowerSet ↑cells) (cells_1 : Finset (ℕ × ℕ))
  (isLowerSet_1 : IsLowerSet ↑cells_1),
  ({ cells := cells, isLowerSet := isLowerSet } = { cells := cells_1, isLowerSet := isLowerSet_1 }) = (cells = cells_1)
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Build a `MulEquiv` from an isomorphism in the category `MagmaCat`.  -/
CategoryTheory.Iso.magmaCatIsoToMulEquiv : {X Y : MagmaCat} → (X ≅ Y) → ↑X ≃* ↑Y
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsCompleteBetween.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) (s t : Set V),
  G.IsCompleteBetween s t = ∀ ⦃v₁ : V⦄, v₁ ∈ s → ∀ ⦃v₂ : V⦄, v₂ ∈ t → G.Adj v₁ v₂
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.one_def : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α], 1 = Dilation.id α
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair.compRightIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A B : C} (f g : A ⟶ B) (s : B ⟶ A) (sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B)
  (sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B) (F : CategoryTheory.Functor C D)
  (x : CategoryTheory.Limits.WalkingReflexivePair),
  (CategoryTheory.Limits.reflexivePair.compRightIso f g s sl sr F).inv.app x =
    match x with
    | CategoryTheory.Limits.WalkingReflexivePair.zero => CategoryTheory.CategoryStruct.id (F.obj B)
    | CategoryTheory.Limits.WalkingReflexivePair.one => CategoryTheory.CategoryStruct.id (F.obj A)
-- Mathlib.Data.Set.Basic
/-- **Alias** of the reverse direction of `Set.ssubset_univ_iff_nonempty_compl`. -/
Set.Nonempty.ssubset_univ : ∀ {α : Type u} {s : Set α}, sᶜ.Nonempty → s ⊂ Set.univ
-- Init.Data.List.Nat.InsertIdx
List.getElem?_insertIdx : ∀ {α : Type u} {l : List α} {x : α} {i j : ℕ},
  (l.insertIdx i x)[j]? = if j < i then l[j]? else if j = i then if j ≤ l.length then some x else none else l[j - 1]?
-- Mathlib.RingTheory.Polynomial.IsIntegral
Polynomial.isIntegral_iff_isIntegral_coeff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {f : Polynomial S},
  IsIntegral (Polynomial R) f ↔ ∀ (n : ℕ), IsIntegral R (f.coeff n)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict_of_not_measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] {f : MeasureTheory.SimpleFunc α β}
  {s : Set α}, ¬MeasurableSet s → f.restrict s = 0
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compAlongComposition.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] [inst_6 : Module 𝕜 G]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : IsTopologicalAddGroup F]
  [inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G] {n : ℕ}
  (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n),
  q.compAlongComposition p c = ContinuousMultilinearMap.compAlongComposition p c (q c.length)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The angle between three points is π if and only if the second point is strictly between the
other two.  -/
EuclideanGeometry.angle_eq_pi_iff_sbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi ↔ Sbtw ℝ p₁ p₂ p₃
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_bot : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] (S : AddSubmonoid R), S * ⊥ = ⊥
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂Aux_apply : ∀ (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7}
  {N₂ : Type u_10} {n : Type u_11} {m : Type u_12} [inst : CommSemiring R] [inst_1 : Semiring R₁] [inst_2 : Semiring S₁]
  [inst_3 : Semiring R₂] [inst_4 : Semiring S₂] [inst_5 : AddCommMonoid M₁] [inst_6 : Module R₁ M₁]
  [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] [inst_9 : AddCommMonoid N₂] [inst_10 : Module R N₂]
  [inst_11 : Module S₁ N₂] [inst_12 : Module S₂ N₂] [inst_13 : SMulCommClass S₁ R N₂] [inst_14 : SMulCommClass S₂ R N₂]
  [inst_15 : SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂} (f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) (b₁ : n → M₁)
  (b₂ : m → M₂) (i : n) (j : m), (LinearMap.toMatrix₂Aux R b₁ b₂) f i j = (f (b₁ i)) (b₂ j)
-- Mathlib.Algebra.Lie.Basic
LieAlgebra.toModule : {R : Type u} → {L : Type v} → {inst : CommRing R} → {inst_1 : LieRing L} → [self : LieAlgebra R L] → Module R L
-- Mathlib.Data.Holor
Holor.instAddGroup : {α : Type} → {ds : List ℕ} → [AddGroup α] → AddGroup (Holor α ds)
-- Lean.Attributes
Lean.EnumAttributes.ext : {α : Type} → Lean.EnumAttributes α → Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)
-- Mathlib.Order.Filter.Prod
Filter.Frequently.of_curry : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {p : α × β → Prop},
  (∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p (x, y)) → ∃ᶠ (xy : α × β) in la ×ˢ lb, p xy
-- Mathlib.GroupTheory.EckmannHilton
/-- If a type carries a unital magma structure that distributes over a unital binary
operation, then the magma structure is a commutative monoid.  -/
EckmannHilton.commMonoid : {X : Type u} →
  {m₁ : X → X → X} →
    {e₁ : X} →
      EckmannHilton.IsUnital m₁ e₁ →
        [h : MulOneClass X] → (∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d) → CommMonoid X
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
isZGroup_iff : ∀ (G : Type u_1) [inst : Group G], IsZGroup G ↔ ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
-- Init.Data.Nat.Lemmas
/-- If `m` and `n` are equal mod `k`, `m - n` is zero mod `k`.  -/
Nat.sub_mod_eq_zero_of_mod_eq : ∀ {m k n : ℕ}, m % k = n % k → (m - n) % k = 0
-- Mathlib.Topology.Separation.Hausdorff
separated_by_isOpenEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space X] {f : X → Y},
  Topology.IsOpenEmbedding f → ∀ {x y : X}, x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ f x ∈ u ∧ f y ∈ v ∧ Disjoint u v
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
BoundarylessManifold.isInteriorPoint : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} [BoundarylessManifold I M], I.IsInteriorPoint x
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_Ioc_val : ∀ {n : ℕ} (i j : Fin n), Fin.val ⁻¹' Set.Ioc ↑i ↑j = Set.Ioc i j
-- Mathlib.Algebra.Group.Defs
mul_inv_cancel_comm_assoc : ∀ {G : Type u_1} [inst : CommGroup G] (a b : G), a * (b * a⁻¹) = b
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.mk.inj : ∀ {X : Type u_5} {Y : Type u_6} {inst : TopologicalSpace X} {toFun : X → Y}
  {isLocallyConstant : IsLocallyConstant toFun} {toFun_1 : X → Y} {isLocallyConstant_1 : IsLocallyConstant toFun_1},
  { toFun := toFun, isLocallyConstant := isLocallyConstant } =
      { toFun := toFun_1, isLocallyConstant := isLocallyConstant_1 } →
    toFun = toFun_1
-- Lean.Util.ParamMinimizer
/-- **Initialization (growing phase).**
Starting from `initialMask`, this procedure sequentially activates parameters
(i.e., flips `false` bits to `true`) until `test` first returns `true`.

For each inactive parameter index `i`, it:
1. sets `cur[i] := true` and records `i` in `added`;
2. calls `tryCur` to evaluate the updated mask;
3. stops immediately once `test` succeeds.

This phase exploits the assumption that `test` is *monotonic* and that the
minimal true configuration is *close* to `initialMask`.  It guarantees that
at completion, the current mask `cur` satisfies `test` if there is a configuration
that satisfies it. `(← get).added.back!` is the element whose inclusion first made `test` true.
 -/
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.init : {m : Type → Type} → [Monad m] → Lean.Util.ParamMinimizer.M✝ m Unit
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.infClosed : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L : BooleanSubalgebra α), InfClosed ↑L
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.hg_int : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (self : WeakFEPair E),
  MeasureTheory.LocallyIntegrableOn self.g (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.Topology.Separation.Basic
isClosedMap_prodMk_left : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space X] (x : X),
  IsClosedMap fun y => (x, y)
-- Mathlib.FieldTheory.PrimeField
instSubsingletonSubfieldRat : Subsingleton (Subfield ℚ)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.compare_getKey_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} (h' : k ∈ t), compare (t.getKey k h') k = Ordering.eq
-- Mathlib.Data.Int.WithZero
WithZeroMulInt.toNNReal.congr_simp : ∀ {e e_1 : NNReal} (e_e : e = e_1) (he : e ≠ 0), WithZeroMulInt.toNNReal he = WithZeroMulInt.toNNReal ⋯
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Construct a bundled `AddMagmaCat` from the underlying type and typeclass.  -/
AddMagmaCat.of : (M : Type u) → [Add M] → AddMagmaCat
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.of_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α → β} {g : β → γ}, UniformContinuous f → UniformContinuous g → IsUniformInducing (g ∘ f) → IsUniformInducing f
-- Mathlib.Algebra.Ring.Divisibility.Basic
dvd_mul_sub_mul : ∀ {α : Type u_1} [inst : NonUnitalCommRing α] {k a b x y : α}, k ∣ a - b → k ∣ x - y → k ∣ a * x - b * y
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformly.add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l → TendstoLocallyUniformly G g l → TendstoLocallyUniformly (F + G) (f + g) l
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- Turn an unbundled `R`-Hopf algebra into the corresponding object in the category of
`R`-Hopf algebras.  -/
CommHopfAlgCat.of : (R : Type u) →
  [inst : CommRing R] → (X : Type v) → [commRing : CommRing X] → [hopfAlgebra : HopfAlgebra R X] → CommHopfAlgCat R
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.baseEmbedding_pos : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R) {x : ↥seed.baseEmbedding.domain},
  0 < x → 0 < ↑seed.baseEmbedding x
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_zpow_const : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] (n : ℤ), UniformContinuous fun x => x ^ n
-- Mathlib.Order.SuccPred.Relation
/-- `(n, m)` is in the reflexive-transitive closure of `~` if `i ~ pred i` and `pred i ~ i`
for all `i` between `n` and `m`.  -/
reflTransGen_of_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → (∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → Relation.ReflTransGen r n m
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.toNat.match_1.eq_2 : ∀ (motive : WType WType.Natβ → Sort u_1) (f : WType.Natβ WType.Natα.succ → WType WType.Natβ)
  (h_1 : (f : WType.Natβ WType.Natα.zero → WType WType.Natβ) → motive (WType.mk WType.Natα.zero f))
  (h_2 : (f : WType.Natβ WType.Natα.succ → WType WType.Natβ) → motive (WType.mk WType.Natα.succ f)),
  (match WType.mk WType.Natα.succ f with
    | WType.mk WType.Natα.zero f => h_1 f
    | WType.mk WType.Natα.succ f => h_2 f) =
    h_2 f
-- Mathlib.Analysis.Normed.Group.Defs
/-- Auxiliary class, endowing a type `E` with a function `norm : E → ℝ` with notation `‖x‖`. This
class is designed to be extended in more interesting classes specifying the properties of the norm.
 -/
Norm : Type u_8 → Type u_8
-- Mathlib.Data.List.AList
AList.mem_lookup_iff : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s : AList β},
  b ∈ AList.lookup a s ↔ ⟨a, b⟩ ∈ s.entries
-- Mathlib.Algebra.Homology.Homotopy
/-- The morphism property on `HomologicalComplex V c` given by homotopy equivalences.  -/
HomologicalComplex.homotopyEquivalences : {ι : Type u_1} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        (c : ComplexShape ι) → CategoryTheory.MorphismProperty (HomologicalComplex V c)
-- Mathlib.MeasureTheory.Function.Jacobian
/-- If a differentiable function `f` is approximated by a linear map `A` on a set `s`, up to `δ`,
then at almost every `x` in `s` one has `‖f' x - A‖ ≤ δ`.  -/
ApproximatesLinearOn.norm_fderiv_sub_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
  {A : E →L[ℝ] E} {δ : NNReal},
  ApproximatesLinearOn f A s δ →
    MeasurableSet s →
      ∀ (f' : E → E →L[ℝ] E), (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → ∀ᵐ (x : E) ∂μ.restrict s, ‖f' x - A‖₊ ≤ δ
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift_inr_inl : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f₁ : α₁ → β₁ → Finset γ₁) (f₂ : α₂ → β₂ → Finset γ₂) (g₁ : α₁ → β₂ → Finset γ₁) (g₂ : α₁ → β₂ → Finset γ₂) (a : α₂)
  (b : β₁), Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inl b) = ∅