mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Tactic.Alias
/-- The command `alias name := target` creates a synonym of `target` with the given name.

The command `alias ⟨fwd, rev⟩ := target` creates synonyms for the forward and reverse directions
of an iff theorem. Use `_` if only one direction is required.

These commands accept all modifiers and attributes that `def` and `theorem` do.
 -/
Batteries.Tactic.Alias.aliasLR : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
/-- Any surjective, quasi-compact and flat morphism is an effective epimorphism.  -/
AlgebraicGeometry.Scheme.instEffectiveEpiOfQuasiCompactOfSurjectiveOfFlat : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.Surjective f]
  [AlgebraicGeometry.Flat f], CategoryTheory.EffectiveEpi f
-- Mathlib.Order.Interval.Multiset
Multiset.left_notMem_Ioo : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, a ∉ Multiset.Ioo a b
-- Lean.Meta.IndPredBelow
/-- Generate `belowNames[motiveIdx]`  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowInductive : ℕ → ℕ → Lean.Meta.IndPredBelow.Context✝ → Lean.MetaM (ℕ × Lean.InductiveType)
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.mker_ordFrac_eq_isUnitSubmonoid : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K],
  MonoidHom.mker (Ring.ordFrac R) = Submonoid.map (algebraMap R K) (IsUnit.submonoid R)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.inv_base_hom_base : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y),
  CategoryTheory.CategoryStruct.comp e.inv.base e.hom.base = CategoryTheory.CategoryStruct.id ↑Y.toPresheafedSpace
-- Mathlib.MeasureTheory.Group.Measure
/-- A nonzero left-invariant regular measure gives positive mass to any open set.  -/
MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_regular : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular] [NeZero μ], μ.IsOpenPosMeasure
-- Init.Data.Nat.Basic
Nat.sub_le_succ_sub : ∀ (a i : ℕ), a - i ≤ a.succ - i
-- Mathlib.Order.Filter.Partial
Filter.rmap_compose : ∀ {α : Type u} {β : Type v} {γ : Type w} (r : SetRel α β) (s : SetRel β γ),
  Filter.rmap s ∘ Filter.rmap r = Filter.rmap (r.comp s)
-- Mathlib.Topology.Constructions.SumProd
/-- `X × Y` is homeomorphic to `Y × X`.  -/
Homeomorph.prodComm : (X : Type u) → (Y : Type v) → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X × Y ≃ₜ Y × X
-- Mathlib.Analysis.Complex.BranchLogRoot
/-- If `g : X → ℂ` defined on a locally path connected space
is continuous on an open simply connected set `U` and `0 ∉ g '' U`,
then there exists a continuous branch of `log ∘ g` on `U`.
More precisely, there exists a function `f : X → ℂ` continuous on `U`
such that `exp (f x) = g x` for all `x ∈ U`.  -/
Complex.exists_continuousOn_eqOn_exp_comp : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {U : Set X},
  IsSimplyConnected U →
    IsOpen U → ∀ {g : X → ℂ}, ContinuousOn g U → 0 ∉ g '' U → ∃ f, ContinuousOn f U ∧ Set.EqOn (Complex.exp ∘ f) g U
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
SSet.Subcomplex.Pairing.instIsProperOp : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper], P.op.IsProper
-- Mathlib.Algebra.Polynomial.Basic
/-- A more convenient spelling of `Polynomial.ofFinsupp.injEq` in terms of `Iff`.  -/
Polynomial.ofFinsupp_inj : ∀ {R : Type u} [inst : Semiring R] {a b : AddMonoidAlgebra R ℕ}, { toFinsupp := a } = { toFinsupp := b } ↔ a = b
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
/-- A section `ℂ → ℍ` of the natural inclusion map, bundled as an `OpenPartialHomeomorph`.  -/
UpperHalfPlane.ofComplex : OpenPartialHomeomorph ℂ UpperHalfPlane
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.clift.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {ι : Type u_5} [inst_3 : TopologicalSpace ι] (T : Bundle.Trivialization F proj)
  [inst_4 : LocallyCompactPair ι ↑T.baseSet],
  T.clift = (T.liftCM.comp { toFun := fun eγt => (eγt.1.1, eγt.1.2 eγt.2), continuous_toFun := ⋯ }).curry
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Add a complete match.  -/
Aesop.ForwardRuleMatches.insert : Aesop.ForwardRuleMatch → Aesop.ForwardRuleMatches → Aesop.ForwardRuleMatches
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.copy_sliceFrom_eq : ∀ {t₁ t₂ s : String} {p : s.Pos}, p.Splits t₁ t₂ → (s.sliceFrom p).copy = t₂
-- Mathlib.CategoryTheory.Endomorphism
/-- The multiplicative bijection `End X ≃* End (F X)` when `X : InducedCategory C F`.  -/
CategoryTheory.InducedCategory.endEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      {F : D → C} → {X : CategoryTheory.InducedCategory C F} → CategoryTheory.End X ≃* CategoryTheory.End (F X)
-- Mathlib.Data.Finset.Sups
Finset.instCommutativeDisjSups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint], Std.Commutative fun x1 x2 => x1.disjSups x2
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_finsetInf : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {ι : Type u_9} (f : M →ₛₗ[σ₁₂] M₂) (s : Finset ι) (p : ι → Submodule R₂ M₂),
  Submodule.comap f (s.inf p) = s.inf fun i => Submodule.comap f (p i)
-- Mathlib.Topology.Sequences
/-- If `x : ℕ → X` has no convergent subsequence in a T₁ sequential space, then its range is
closed.  -/
isClosed_range_of_not_tendsto : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : ℕ → X} [SequentialSpace X] [T1Space X],
  (∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Filter.Tendsto (x ∘ φ) Filter.atTop (nhds l)) → IsClosed (Set.range x)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.logEmbedding_ker : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  (NumberField.Units.logEmbedding K).ker = Subgroup.toAddSubgroup (NumberField.Units.torsion K)
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.Intermediate.step_appendSnd : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] {it₂ : Std.Iter β},
  (Std.Iter.Intermediate.appendSnd α₁ it₂).step =
    match it₂.step with
    | ⟨Std.IterStep.yield it₂' out, h⟩ => Std.PlausibleIterStep.yield (Std.Iter.Intermediate.appendSnd α₁ it₂') out ⋯
    | ⟨Std.IterStep.skip it₂', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.Intermediate.appendSnd α₁ it₂') ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Lean.Level
/-- Auxiliary function used at `normalize`  -/
_private.Lean.Level.0.Lean.Level.mkIMaxAux : Lean.Level → Lean.Level → Lean.Level
-- Mathlib.Order.Hom.Basic
Pi.evalOrderHom_coe : ∀ {ι : Type u_6} {π : ι → Type u_7} [inst : (i : ι) → Preorder (π i)] (i : ι), ⇑(Pi.evalOrderHom i) = Function.eval i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α} {k : α}, Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l) k = ()
-- Mathlib.Topology.Maps.Basic
Topology.IsCoinducing.isOpenMap_of_injective : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsCoinducing f → Function.Injective f → IsOpenMap f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.equiv_iff_toList_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.toList = t₂.toList)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
/-- **Alias** of the forward direction of `HomogeneousIdeal.map_le_iff_le_comap`. -/
HomogeneousIdeal.le_comap_of_map_le : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : AddSubmonoidClass σ A] [inst_5 : AddSubmonoidClass τ B]
  [inst_6 : DecidableEq ι] [inst_7 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {I : HomogeneousIdeal 𝒜} {J : HomogeneousIdeal ℬ},
  HomogeneousIdeal.map f I ≤ J → I ≤ HomogeneousIdeal.comap f J
-- Aesop.Rule.Basic
Aesop.instInhabitedRule : {a : Type} → [Inhabited a] → Inhabited (Aesop.Rule a)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- The **Cauchy criterion** for infinite products, also known as the **Cauchy convergence test**  -/
multipliable_iff_cauchySeq_finset : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommMonoid α] [CompleteSpace α] {f : β → α},
  Multipliable f ↔ CauchySeq fun s => ∏ b ∈ s, f b
-- Mathlib.Algebra.GroupWithZero.TransferInstance
/-- Transfer `MonoidWithZero` across an `Equiv`  -/
Equiv.monoidWithZero : {α : Type u} → {β : Type v} → α ≃ β → [MonoidWithZero β] → MonoidWithZero α
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Specification for matrix types over ℚ which can be used in the Gauss Elimination and the Simplex
Algorithm. It was introduced to unify dense matrices and sparse matrices.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm : (ℕ → ℕ → Type) → Type
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.neg_smul_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) {u : R},
  IsUnit u → W'.neg (u • P) ≈ W'.neg P
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_congr_nhds : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M},
  nhdsWithin x s = nhdsWithin x t → (MDiffAt[s] f x ↔ MDiffAt[t] f x)
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.succeeded.sizeOf_spec : ∀ (newRapps : Array Aesop.RappRef), sizeOf (Aesop.SafeRulesResult.succeeded newRapps) = 1 + sizeOf newRapps
-- Mathlib.Computability.Primrec.List
/-- If `R a b` is decidable, then given `L : List α` and `b : β`, `g L b ↔ ∃ a L, R a b`
is a primitive recursive relation.  -/
PrimrecRel.exists_mem_list : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [inst : Primcodable α] [inst_1 : Primcodable β],
  PrimrecRel R → PrimrecRel fun L b => ∃ a ∈ L, R a b
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueSet_bot : ∀ {α : Type u_1} {n : ℕ}, 1 < n → ⊥.cliqueSet n = ∅
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeParams.mk.injEq : ∀ (textDocument textDocument_1 : Lean.Lsp.TextDocumentIdentifier),
  ({ textDocument := textDocument } = { textDocument := textDocument_1 }) = (textDocument = textDocument_1)
-- Mathlib.Order.Filter.Cofinite
/-- The coproduct of the cofinite filters on two types is the cofinite filter on their product.  -/
Filter.coprod_cofinite : ∀ {α : Type u_2} {β : Type u_3}, Filter.cofinite.coprod Filter.cofinite = Filter.cofinite
-- Mathlib.Data.QPF.Multivariate.Constructions.Prj
/-- Representation function of the `QPF` instance  -/
MvQPF.Prj.repr : {n : ℕ} → (i : Fin2 n) → ⦃α : TypeVec.{u_1} n⦄ → MvQPF.Prj i α → ↑(MvQPF.Prj.P i) α
-- Lean.Util.Trace
Lean.getTraces : {m : Type → Type} → [Monad m] → [Lean.MonadTrace m] → m (Lean.PersistentArray Lean.TraceElem)
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.take.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (n : ℕ) → motive n.succ []) (h_3 : (n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, [] => h_2 n
    | n.succ, a :: as => h_3 n a as) =
    h_1 x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  m.getKey? k = some k' →
    Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.filterMap f m) k = ((Std.ExtDHashMap.Const.get? m k).bind (f k')).get!
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.MemLp.indicator : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {s : Set α} {f : α → ε},
  MeasurableSet s → MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (s.indicator f) p μ
-- Mathlib.Algebra.Order.IsBotOne
one_lt_of_gt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α] [inst_1 : One α] [IsBotOneClass α], a < b → 1 < b
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.FullSubcategory.comp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : C} (h : Z.obj ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
-- Mathlib.Order.BooleanAlgebra.Basic
/-- Pullback a `BooleanAlgebra` along an injection.  -/
Function.Injective.booleanAlgebra : {α : Type u} →
  {β : Type u_1} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : Top α] →
              [inst_5 : Bot α] →
                [inst_6 : Compl α] →
                  [inst_7 : SDiff α] →
                    [inst_8 : HImp α] →
                      [inst_9 : BooleanAlgebra β] →
                        (f : α → β) →
                          Function.Injective f →
                            (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                              (∀ {x y : α}, f x < f y ↔ x < y) →
                                (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                  (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                    f ⊤ = ⊤ →
                                      f ⊥ = ⊥ →
                                        (∀ (a : α), f aᶜ = (f a)ᶜ) →
                                          (∀ (a b : α), f (a \ b) = f a \ f b) →
                                            (∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) → BooleanAlgebra α
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.combine'.match_1.eq_4 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var)
  (p₁ : Int.Internal.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Internal.Linear.Var) (p₂ : Int.Internal.Linear.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.num k₂))
  (h_2 :
    (k₁ a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.add a x p))
  (h_3 :
    (a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k₂ : ℤ) → motive (Int.Internal.Linear.Poly.add a x p) (Int.Internal.Linear.Poly.num k₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)),
  (match Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ with
    | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.num k₂ => h_1 k₁ k₂
    | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.add a x p => h_2 k₁ a x p
    | Int.Internal.Linear.Poly.add a x p, Int.Internal.Linear.Poly.num k₂ => h_3 a x p k₂
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) =
    h_4 a₁ x₁ p₁ a₂ x₂ p₂
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.ext_iff : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.Embedding M N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.norm_Integral_le_one : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E], ‖MeasureTheory.L1.integralCLM‖ ≤ 1
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.mk : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  (∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0) → μ.AbsolutelyContinuous ν
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f₁` and `f₂` have unequal order at `x`, then the trailing coefficient of `f₁ - f₂` at `x` is the
trailing coefficient of the function with the lowest order.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E},
  MeromorphicAt f₂ x →
    meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x →
      meromorphicTrailingCoeffAt (fun z => f₁ z - f₂ z) x = meromorphicTrailingCoeffAt f₁ x
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndunion_le : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s.ndunion t ≤ u ↔ s ⊆ u ∧ t ≤ u
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- After we process a set of patterns, we obtain the set of de Bruijn indices in these patterns.
We say they are pattern variables. This function checks whether the set of pattern variables is sufficient for
instantiating the theorem with proof `thmProof`. The theorem has `numParams` parameters.
The missing parameters:
1- we may be able to infer them using type inference or type class synthesis, or
2- they are propositions, and may become hypotheses of the instantiated theorem.

For type class instance parameters, we must check whether the free variables in class input parameters are available.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.checkCoverage : Lean.Expr → ℕ → Std.HashSet ℕ → Lean.MetaM Lean.Meta.Grind.CheckCoverageResult
-- Init.Core
/-- Lifts a binary function from the underlying types to a binary function on quotients. The function
must respect both quotients' equivalence relations.

`Quotient.lift` is a version of this operation for unary functions. `Quotient.liftOn₂` is a version
that take the quotient parameters first.
 -/
Quotient.lift₂ : {α : Sort uA} →
  {β : Sort uB} →
    {φ : Sort uC} →
      {s₁ : Setoid α} →
        {s₂ : Setoid β} →
          (f : α → β → φ) →
            (∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) →
              Quotient s₁ → Quotient s₂ → φ
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- If the infinite place `v` is complex, then `v.Completion` is isometric to `ℂ`.  -/
NumberField.InfinitePlace.Completion.isometryEquivComplexOfIsComplex : {K : Type u_1} → [inst : Field K] → {v : NumberField.InfinitePlace K} → v.IsComplex → v.Completion ≃ᵢ ℂ
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.isBounded_iff_eventually : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  Bornology.IsBounded s ↔ ∀ᶠ (C : ℝ) in Filter.atTop, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtSource.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  (P Q : CategoryTheory.MorphismProperty C) [P.IsLocalAtSource K] [Q.IsLocalAtSource K], (P ⊓ Q).IsLocalAtSource K
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_4 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (distance : ℕ) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_4 distance
-- Mathlib.Order.KrullDimension
Order.exists_series_of_coheight_eq_coe : ∀ {α : Type u_1} [inst : Preorder α] (a : α) {n : ℕ}, Order.coheight a = ↑n → ∃ p, RelSeries.head p = a ∧ p.length = n
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'XIso.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryLE i),
  K.truncLE'XIso e hi' hi = (K.op.truncGE'XIso e.op hi' ⋯).symm.unop
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_comm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.WSameSide x y ↔ s.WSameSide y x
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.IsVertexCover.preimage : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {F : Type u_3} [inst : FunLike F V W]
  [SimpleGraph.HomClass F G H] (f : F) {c : Set W}, H.IsVertexCover c → G.IsVertexCover (⇑f ⁻¹' c)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.instIsAddMonHomId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  [inst_2 : CategoryTheory.AddMonObj X], CategoryTheory.IsAddMonHom (CategoryTheory.CategoryStruct.id X)
-- Lean.Parser.Basic
Lean.Parser.octalNumberFn : String.Pos.Raw → optParam Bool true → Lean.Parser.ParserFn
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_fiberwise_of_maps_to' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ}
  [inst_1 : DecidableEq κ] {g : ι → κ},
  (∀ i ∈ s, g i ∈ t) → ∀ (f : κ → M), ∑ j ∈ t, ∑ i ∈ s with g i = j, f j = ∑ i ∈ s, f (g i)