mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.DeclarationNames
/-- If `stx` is a syntax node for an `export` statement, then `getAliasSyntax stx` returns the array of
identifiers with the "exported" names.
 -/
Mathlib.Linter.getAliasSyntax : {m : Type → Type} → [Monad m] → [Lean.MonadResolveName m] → Lean.Syntax → m (Array Lean.Syntax)
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A function which can be locally uniformly approximated by functions which are continuous
within a set at a point is continuous within this set at this point.  -/
continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α} {x : α},
  x ∈ s →
    (∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) →
      ContinuousWithinAt f s x
-- Lean.Server.GoTo
Lean.Server.locationLinksFromTermInfo : Lean.Elab.TermInfo → Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_mem_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k a : α} {v : β k}, a ∈ Std.DTreeMap.Internal.Impl.insert! k v t → compare k a ≠ Ordering.eq → a ∈ t
-- Lean.Parser.Command
Lean.Parser.Command.declBody.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.Height.MvPolynomial
Height.mulHeight_sym2_ge : ∀ (K : Type u_4) [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K],
  ∃ C > 0,
    ∀ {a b c d : K},
      ![a, b] ≠ 0 →
        ![c, d] ≠ 0 →
          C * Height.mulHeight ![a, b] * Height.mulHeight ![c, d] ≤ Height.mulHeight ![a * c, a * d + b * c, b * d]
-- Mathlib.Combinatorics.Additive.Dissociation
Finset.mem_addSpan : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s : Finset α} {a : α},
  a ∈ s.addSpan ↔ ∃ ε, (∀ (a : α), ε a = -1 ∨ ε a = 0 ∨ ε a = 1) ∧ ∑ a ∈ s, ε a • a = a
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.reportMVarInternalization : Lean.Meta.Grind.GrindM Bool
-- Init.Data.Int.DivMod.Lemmas
Int.neg_fmod_self : ∀ (a : ℤ), (-a).fmod a = 0
-- Mathlib.Data.ENNReal.Basic
ENNReal.one_lt_top : 1 < ⊤
-- Mathlib.Data.Prod.Lex
Prod.Lex.instLT : (α : Type u_3) → (β : Type u_4) → [LT α] → [LT β] → LT (Lex (α × β))
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The center of a (not necessarily unital or associative) ring
is isomorphic to the center of its opposite.  -/
NonUnitalSubring.centerToMulOpposite : {R : Type u} → [inst : NonUnitalNonAssocRing R] → ↥(NonUnitalSubring.center R) ≃+* ↥(NonUnitalSubring.center Rᵐᵒᵖ)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.instFunLike : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → FunLike (P →ᵃⁱ[𝕜] P₂) P P₂
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquivAlg_mk : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Ring B] [inst_4 : Algebra R₁ B] {I : Ideal A} (J : Ideal B) [inst_5 : I.IsTwoSided] [inst_6 : J.IsTwoSided]
  (f : A ≃ₐ[R₁] B) (hIJ : J = Ideal.map (↑f) I) (x : A),
  (I.quotientEquivAlg J f hIJ) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) (f x)
-- Mathlib.Data.Nat.Bitwise
Nat.binaryRec_of_ne_zero : ∀ {C : ℕ → Sort u_1} (z : C 0) (f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)) {n : ℕ},
  n ≠ 0 → Nat.binaryRec z f n = ⋯ ▸ f n.bodd n.div2 (Nat.binaryRec z f n.div2)
-- Mathlib.Analysis.Convex.Between
AffineEquiv.sbtw_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {x y z : P} (f : P ≃ᵃ[R] P'),
  Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.coe_compl : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
  (P : { P // IsLprojection X P }), ↑Pᶜ = 1 - ↑P
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.mem_skeleton : ∀ (X : SSet) {i : ℕ} (x : X.obj (Opposite.op { len := i })) {n : ℕ},
  autoParam (i < n) SSet.mem_skeleton._auto_1 → x ∈ (X.skeleton n).obj (Opposite.op { len := i })
-- Mathlib.Data.List.Perm.Basic
List.Perm.flatMap : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f g : α → List β},
  l₁.Perm l₂ → (∀ a ∈ l₁, (f a).Perm (g a)) → (List.flatMap f l₁).Perm (List.flatMap g l₂)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_comp_toLinearMap : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B C : Rep.{w, u, v} k G} (f : A ⟶ B) (g : B ⟶ C),
  (Rep.Hom.hom (CategoryTheory.CategoryStruct.comp f g)).toLinearMap =
    (Rep.Hom.hom g).toLinearMap ∘ₗ (Rep.Hom.hom f).toLinearMap
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- `LinearMap.restrictScalars` as a `LinearMap`.  -/
LinearMap.restrictScalarsₗ : (R : Type u_14) →
  (S : Type u_15) →
    (M : Type u_16) →
      (N : Type u_17) →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module S M] →
                      [inst_7 : Module S N] →
                        [LinearMap.CompatibleSMul M N R S] →
                          (R₁ : Type u_19) →
                            [inst_9 : Semiring R₁] →
                              [inst_10 : Module R₁ N] →
                                [inst_11 : SMulCommClass S R₁ N] →
                                  [inst_12 : SMulCommClass R R₁ N] → (M →ₗ[S] N) →ₗ[R₁] M →ₗ[R] N
-- Mathlib.Topology.Irreducible
/-- **Alias** of the reverse direction of `isIrreducible_iff_closure`.

---

[Stacks Tag 004W](https://stacks.math.columbia.edu/tag/004W) ((1)) -/
IsIrreducible.closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsIrreducible s → IsIrreducible (closure s)
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
/-- A Finset of all trees with `n` nodes. See `mem_treesOfNodesEq`  -/
BinaryTree.treesOfNumNodesEq : ℕ → Finset (BinaryTree Unit)
-- Mathlib.Computability.MyhillNerode
Language.accepts_toDFA : ∀ {α : Type u} (L : Language α), L.toDFA.accepts = L
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.contains_eq_isSome_getKey?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β}, t.Ordered → Std.DTreeMap.Internal.Impl.contains k t = (t.getKey?ₘ k).isSome
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- If `p` is prime, the `p`-th roots of unity in an integral domain are exactly the primitive
`p`-th roots of unity together with `1`.  -/
nthRootsFinset_eq_of_prime : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ} [inst_2 : DecidableEq R],
  Nat.Prime p → Polynomial.nthRootsFinset p 1 = primitiveRoots p R ∪ {1}
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_add : ∀ {M : Type u_5} [inst : CommMonoid M] (s t : Multiset M), (s + t).prod = s.prod * t.prod
-- Mathlib.Topology.Instances.EReal.Lemmas
/-- The set of finite `EReal` numbers is homeomorphic to `ℝ`.  -/
EReal.neBotTopHomeomorphReal : ↑{⊥, ⊤}ᶜ ≃ₜ ℝ
-- Lean.Parser.Term.Basic
Lean.Parser.convParser : optParam ℕ 0 → Lean.Parser.Parser
-- Mathlib.Topology.Homotopy.Basic
/-- Given a continuous function `f`, we can define a `ContinuousMap.Homotopy f f` by
`F (t, x) = f x`
 -/
ContinuousMap.Homotopy.refl : {X : Type u} → {Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (f : C(X, Y)) → f.Homotopy f
-- Mathlib.Data.Vector.MapLemmas
List.Vector.map₂_eq_mapAccumr₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {xs : List.Vector α n} {ys : List.Vector β n} {f : α → β → γ},
  List.Vector.map₂ f xs ys = (List.Vector.mapAccumr₂ (fun x y x_1 => ((), f x y)) xs ys ()).2
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Position.mk : ℕ → ℕ → Lean.Lsp.Position
-- Mathlib.MeasureTheory.Measure.OpenPos
Continuous.isOpenPosMeasure_map : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure]
  [OpensMeasurableSpace X] {Z : Type u_3} [inst_3 : TopologicalSpace Z] [inst_4 : MeasurableSpace Z] [BorelSpace Z]
  {f : X → Z}, Continuous f → Function.Surjective f → (MeasureTheory.Measure.map f μ).IsOpenPosMeasure
-- Init.Data.SInt.Bitwise
Int16.ofBitVec_not : ∀ (a : BitVec 16), Int16.ofBitVec (~~~a) = ~~~Int16.ofBitVec a
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.quotientCompQhIso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (f : K ⟶ L) {Z : DerivedCategory C}
  (h : DerivedCategory.Q.obj L ⟶ Z),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f))
      (CategoryTheory.CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C).hom.app L) h) =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C).hom.app K)
      (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map f) h)
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- For a unary operation (e.g. `x ↦ -x`) defined at each stalk, if a prelocal predicate is closed
under the operation on each open set, then the sheafified predicate is also closed under the
operation. See `sheafify_inductionOn` for the version with refinement.  -/
TopCat.PrelocalPredicate.sheafify_inductionOn' : ∀ {X : TopCat} {T : ↑X → Type u_2} (P : TopCat.PrelocalPredicate T) (op : {x : ↑X} → T x → T x),
  (∀ {U : TopologicalSpace.Opens ↑X} {a : (x : ↥U) → T ↑x}, P.pred a → P.pred fun x => op (a x)) →
    ∀ {U : TopologicalSpace.Opens ↑X} {a : (x : ↥U) → T ↑x}, P.sheafify.pred a → P.sheafify.pred fun x => op (a x)
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R],
  CanLift (Set R) (StarSubsemiring R) SetLike.coe fun s =>
    0 ∈ s ∧
      (∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s) ∧
        1 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x : R}, x ∈ s → star x ∈ s
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The angle between three points is zero if and only if one of the first and third points is
strictly between the other two, or those two points are equal but not equal to the second.  -/
EuclideanGeometry.angle_eq_zero_iff_eq_and_ne_or_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₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
-- Mathlib.Combinatorics.SimpleGraph.Tutte
/-- This lemma constructs a perfect matching on `G` from two near-matchings.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Tutte.0.SimpleGraph.tutte_exists_isPerfectMatching_of_near_matchings : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V] {x a b c : V} {M1 : (G ⊔ SimpleGraph.edge x b).Subgraph}
  {M2 : (G ⊔ SimpleGraph.edge a c).Subgraph},
  G.Adj x a →
    G.Adj a b →
      ¬G.Adj x b →
        ¬G.Adj a c →
          x ≠ b → x ≠ c → a ≠ c → b ≠ c → M1.IsPerfectMatching → M2.IsPerfectMatching → ∃ M, M.IsPerfectMatching
-- Mathlib.Tactic.FieldSimp
/-- Given `l` of type `qNF M`, i.e. a list of `(ℤ × Q($M)) × ℕ`s (two `Expr`s and a natural
number), apply an expression representing a function with domain `ℤ` to each of the `ℤ`
components.  -/
Mathlib.Tactic.FieldSimp.qNF.onExponent : {v : Lean.Level} → {M : Q(Type v)} → Mathlib.Tactic.FieldSimp.qNF M → (ℤ → ℤ) → Mathlib.Tactic.FieldSimp.qNF M
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.IterM.step_append.match_1.eq_1 : ∀ {α₁ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β) (out : β)
  (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out))
  (h_1 :
    (it₁' : Std.IterM m β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it₁' out, h⟩ with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => h_1 it₁' out h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₁' out h
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The morphism that is part of an object in `Over X`.  -/
CategoryTheory.Over.hom : {T : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} T] → {X : T} → (f : CategoryTheory.Over X) → f.left ⟶ X
-- Batteries.Data.PairingHeap
/-- Auxiliary for `Heap.deleteMin`: merge the forest in pairs.  -/
Batteries.PairingHeapImp.Heap.combine : {α : Type u_1} → (α → α → Bool) → Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α
-- Mathlib.LinearAlgebra.Matrix.Ideal
RingCon.matrix_apply : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocSemiring R] [inst_1 : Fintype n] {c : RingCon R}
  {M N : Matrix n n R}, (RingCon.matrix n c) M N ↔ ∀ (i j : n), c (M i j) (N i j)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx?.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.gt) → motive x
-- Mathlib.CategoryTheory.Shift.Twist
/-- Given `t : TwistShiftData C A`, the shift on the category `TwistShift t` has
the same shift functors as `C`, the same isomorphism `shiftFunctorZero` isomorphism,
but the `shiftFunctorAdd` isomorphisms are modified using `t`.  -/
CategoryTheory.TwistShiftData.shiftMkCore : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (t : CategoryTheory.TwistShiftData C A) → CategoryTheory.ShiftMkCore t.Category A
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.rightAdjointOfEquiv_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
  (he :
    ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
      (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g))
  (a : D), (CategoryTheory.Adjunction.rightAdjointOfEquiv e he).obj a = G_obj a
-- Mathlib.Order.RelClasses
/-- An unbundled relation class stating that `r` is the nonstrict relation corresponding to the
strict relation `s`. Compare `lt_iff_le_not_ge`. This is mostly meant to provide dot
notation on `(⊆)` and `(⊂)`.  -/
IsNonstrictStrictOrder : (α : Type u_1) → semiOutParam (α → α → Prop) → (α → α → Prop) → Prop
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_zero_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.covariance X 0 μ = 0
-- Mathlib.Algebra.Group.Action.Basic
vadd_left_cancel_iff : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] (g : α) {x y : β}, g +ᵥ x = g +ᵥ y ↔ x = y
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mulRight_zero_eq_zero : ∀ (R : Type u_14) (A : Type u_15) [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A], LinearMap.mulRight R 0 = 0
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.mul_tprod_tprod : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] [inst_2 : (i : ι) → Module R (A i)]
  [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)] [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)]
  (x y : (i : ι) → A i),
  (PiTensorProduct.mul ((PiTensorProduct.tprod R) x)) ((PiTensorProduct.tprod R) y) = (PiTensorProduct.tprod R) (x * y)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.coe_sup : ∀ {N : Type u_7} [inst : CommMonoid N] (H K : Submonoid N), ↑(H ⊔ K) = ↑H * ↑K
-- Init.Data.Vector.Lex
Vector.lt_trans : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [i₁ : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2]
  {xs ys zs : Vector α n}, xs < ys → ys < zs → xs < zs
-- Init.Data.UInt.Basic
/-- Unsigned division for word-sized unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.

This operation is sometimes called “floor division.” Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.
 -/
USize.div : USize → USize → USize
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- The q-ary entropy function is continuous everywhere.
This is due to definition of `Real.log` for negative numbers.  -/
Real.qaryEntropy_continuous : ∀ {q : ℕ}, Continuous (Real.qaryEntropy q)
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain_injective : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} [inst : Zero M] (f : α ↪ β), Function.Injective (Finsupp.embDomain f)
-- Mathlib.Data.Nat.Bits
/-- `bodd n` returns `true` if `n` is odd  -/
Nat.bodd : ℕ → Bool
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.comp₃_contDiffOn : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_6}
  {E₂ : Type u_7} {E₃ : Type u_8} [inst_5 : NormedAddCommGroup E₁] [inst_6 : NormedAddCommGroup E₂]
  [inst_7 : NormedAddCommGroup E₃] [inst_8 : NormedSpace 𝕜 E₁] [inst_9 : NormedSpace 𝕜 E₂] [inst_10 : NormedSpace 𝕜 E₃]
  {g : E₁ × E₂ × E₃ → G} {f₁ : F → E₁} {f₂ : F → E₂} {f₃ : F → E₃} {s : Set F},
  ContDiff 𝕜 n g →
    ContDiffOn 𝕜 n f₁ s → ContDiffOn 𝕜 n f₂ s → ContDiffOn 𝕜 n f₃ s → ContDiffOn 𝕜 n (fun x => g (f₁ x, f₂ x, f₃ x)) s
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_eq_of_ne' : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] {i j : ι}
  (r : G i), i ≠ j → (RestrictedProduct.single A i r) j = 0
-- Init.Data.Range.Polymorphic.SInt
ISize.instRxiHasSize : Std.Rxi.HasSize ISize
-- Mathlib.Analysis.Normed.Module.RCLike.Real
interior_sphere' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ),
  interior (Metric.sphere x r) = ∅
-- Mathlib.Algebra.Group.Action.Sum
Sum.instIsCentralVAdd : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β] [inst_2 : VAdd Mᵃᵒᵖ α]
  [inst_3 : VAdd Mᵃᵒᵖ β] [IsCentralVAdd M α] [IsCentralVAdd M β], IsCentralVAdd M (α ⊕ β)
-- Mathlib.Combinatorics.Graph.Lattice
Graph.disjoint_iff : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, Disjoint G H ↔ Disjoint G.vertexSet H.vertexSet
-- Mathlib.Topology.Clopen
isClopen_discrete : ∀ {X : Type u} [inst : TopologicalSpace X] [DiscreteTopology X] (s : Set X), IsClopen s
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_ofNat_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ)
  [inst_4 : n.AtLeastTwo] (a : R), Int.fract (OfNat.ofNat n + a) = Int.fract a
-- Mathlib.Order.BoundedOrder.Basic
subsingleton_of_bot_eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊥ = ⊤ → Subsingleton α
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Composing a multilinear map with a linear equiv on each argument gives the zero map
if and only if the multilinear map is the zero map.  -/
MultilinearMap.comp_linearEquiv_eq_zero_iff : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] [inst_6 : (i : ι) → Module R (M₁' i)]
  (g : MultilinearMap R M₁' M₂) (f : (i : ι) → M₁ i ≃ₗ[R] M₁' i), (g.compLinearMap fun i => ↑(f i)) = 0 ↔ g = 0
-- Mathlib.Logic.ExistsUnique
existsUnique_prop_of_true : ∀ {p : Prop} {q : p → Prop} (h : p), (∃! h', q h') ↔ q h
-- Mathlib.Algebra.Order.Group.Synonym
isAddLeftRegular_ofDual : ∀ {α : Type u_1} [inst : AddMonoid α] {a : αᵒᵈ}, IsAddLeftRegular (OrderDual.ofDual a) ↔ IsAddLeftRegular a
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Given an open set `s` containing a closed set `t` in a finite-dimensional real manifold, there
exists a smooth function with support equal to `s`, taking values in `[0,1]`, and equal to `1`
exactly on `t`.  -/
exists_contMDiff_support_eq_eq_one_iff : ∀ {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]
  [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] [T2Space M] {n : ℕ∞} {s t : Set M},
  IsOpen s →
    IsClosed t →
      t ⊆ s →
        ∃ f,
          ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) f ∧
            Set.range f ⊆ Set.Icc 0 1 ∧ Function.support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_empty : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], ∅ᶜ = Finset.univ
-- Mathlib.GroupTheory.Focal
Subgroup.transferFocal.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.FiniteIndex],
  H.transferFocal = (QuotientGroup.mk' H.focalSubgroupOf).transfer
-- Mathlib.Data.Set.Lattice
Set.Ici_iSup₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} [inst : CompleteLattice α] (f : (i : ι) → κ i → α),
  Set.Ici (⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, Set.Ici (f i j)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_ball_mul_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ},
  0 < r → ∀ (s : ℝ), μ (Metric.ball x (r * s)) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.ball 0 s)
-- Init.Data.Array.Lemmas
Array.any_eq_not_all_not : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, xs.any p = !xs.all fun x => !p x
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isLoop_iff_closure_eq_loops : ∀ {α : Type u_1} {M : Matroid α} {e : α},
  autoParam (e ∈ M.E) Matroid.isLoop_iff_closure_eq_loops._auto_1 → (M.IsLoop e ↔ M.closure {e} = M.loops)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ComputedFieldView.ref : Lean.Elab.Command.ComputedFieldView → Lean.Syntax
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry.step.injEq : ∀ (cls : Lean.Name) (decls : Array Lean.IR.Decl) (cls_1 : Lean.Name) (decls_1 : Array Lean.IR.Decl),
  (Lean.IR.LogEntry.step cls decls = Lean.IR.LogEntry.step cls_1 decls_1) = (cls = cls_1 ∧ decls = decls_1)
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.instTopologicalSpaceAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M],
  AddOpposite.instTopologicalSpaceAddOpposite = TopologicalSpace.induced AddOpposite.unop inst