mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.CandidateKind.appArg.sizeOf_spec : sizeOf Lean.Server.FileWorker.SignatureHelp.CandidateKind.appArg = 1
-- Mathlib.Algebra.MvPolynomial.Basic
/-- `constantCoeff p` returns the constant term of the polynomial `p`, defined as `coeff 0 p`.
This is a ring homomorphism.
 -/
MvPolynomial.constantCoeff : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → MvPolynomial σ R →+* R
-- Mathlib.MeasureTheory.Integral.CircleIntegral
hasDerivAt_circleMap : ∀ (c : ℂ) (R θ : ℝ), HasDerivAt (circleMap c R) (circleMap 0 R θ * Complex.I) θ
-- Mathlib.Tactic.NormNum.NatFib
Mathlib.Meta.NormNum.proveNatFibAux : (en' : Q(ℕ)) → (ea' : Q(ℕ)) × (eb' : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsFibAux «$en'» «$ea'» «$eb'»)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_inv : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : Inv G] (a : G), ↑a⁻¹ = (↑a)⁻¹
-- Mathlib.Algebra.Order.Group.Abs
mabs_div_pos : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G}, 1 < |a / b|ₘ ↔ a ≠ b
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_subset_Ioo_union_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioo a c ⊆ Set.Ioo a b ∪ Set.Ico b c
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_hom_add_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : CommMonoid N] {f g : α →₀ M}
  (h : α → Multiplicative M →* N),
  ((f + g).prod fun a b => (h a) (Multiplicative.ofAdd b)) =
    (f.prod fun a b => (h a) (Multiplicative.ofAdd b)) * g.prod fun a b => (h a) (Multiplicative.ofAdd b)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k : α},
      m.contains k = false →
        l.contains k = false → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey? k = none
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f : ∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (m n : S)
  (X : CategoryTheory.DifferentialObject S C),
  ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).inv.app X).f =
    (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.unitors_equal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.RingTheory.Finiteness.Basic
/-- The submodule generated by a finite supremum of finite-dimensional submodules is
finite-dimensional.

Note that strictly this only needs `∀ i ∈ s, FiniteDimensional K (S i)`, but that doesn't
work well with typeclass search.  -/
Submodule.finite_finset_sup : ∀ {R : Type u_2} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {ι : Type u_1}
  (s : Finset ι) (S : ι → Submodule R V) [∀ (i : ι), Module.Finite R ↥(S i)], Module.Finite R ↥(s.sup S)
-- Mathlib.Computability.AkraBazzi.SumTransform
_private.Mathlib.Computability.AkraBazzi.SumTransform.0.AkraBazziRecurrence.termε : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_add : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : Semiring S] (f : R →+* S),
  Polynomial.map f (p + q) = Polynomial.map f p + Polynomial.map f q
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- A Hamiltonian path visits every vertex.  -/
SimpleGraph.Walk.IsHamiltonian.mem_support : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b},
  p.IsHamiltonian → ∀ (c : α), c ∈ p.support
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ → ∀ (f : (a : α) → β a → Option (γ a)), (Std.DTreeMap.filterMap f t₁).Equiv (Std.DTreeMap.filterMap f t₂)
-- Mathlib.CategoryTheory.Skeletal
/-- If `C` is thin and skeletal, then any naturally isomorphic functors to `C` are equal.  -/
CategoryTheory.Functor.eq_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F₁ F₂ : CategoryTheory.Functor D C} [Quiver.IsThin C], CategoryTheory.Skeletal C → ∀ (hF : F₁ ≅ F₂), F₁ = F₂
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.instBEqComparisonResult : BEq Mathlib.Linter.TextBased.ComparisonResult✝
-- Lean.Expr
/-- `inferImplicit e numParams considerRange` updates the first `numParams` parameter binder annotations of the `e` forall type.
It marks any parameter with an explicit binder annotation if there is another explicit arguments that depends on it or
the resulting type if `considerRange == true`.

Remark: we use this function to infer the binder annotations of structure projections.
 -/
Lean.Expr.inferImplicit : Lean.Expr → ℕ → Bool → Lean.Expr
-- Init.Data.BitVec.Lemmas
BitVec.ushiftRight_or_distrib : ∀ {w : ℕ} (x y : BitVec w) (n : ℕ), (x ||| y) >>> n = x >>> n ||| y >>> n
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.isoOfHom_inv_hom_id_assoc : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W f) {Z : D}
  (h : L.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W f hf).inv
      (CategoryTheory.CategoryStruct.comp (L.map f) h) =
    h
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_containsKey_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValueCastD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback =
        fallback
-- Mathlib.Algebra.Group.Basic
mul_div : ∀ {G : Type u_3} [inst : DivInvMonoid G] (a b c : G), a * (b / c) = a * b / c
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfList.eq_def : ∀ {ι : Type u_1} (a s : ι → ℕ) (x : List ι) (x_1 : List.Pairwise (Function.onFun Nat.Coprime s) x),
  Nat.chineseRemainderOfList a s x x_1 =
    match x, x_1 with
    | [], x => ⟨0, ⋯⟩
    | i :: l, co =>
      have this := ⋯;
      have ih := Nat.chineseRemainderOfList a s l ⋯;
      have k := Nat.chineseRemainder this (a i) ↑ih;
      ⟨↑k, ⋯⟩
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.mem_inf : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (t₁ t₂ : CategoryTheory.Pretopology C) {X : C} (S : CategoryTheory.Presieve X),
  S ∈ (t₁ ⊓ t₂).coverings X ↔ S ∈ t₁.coverings X ∧ S ∈ t₂.coverings X
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α], FreeAddGroup.toWord = Quot.lift FreeAddGroup.reduce ⋯
-- Mathlib.RingTheory.LocalRing.ResidueField.Instances
instIsSeparableQuotientIdealOfResidueField : ∀ {A : Type u_2} {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  (q : Ideal B) [inst_3 : q.LiesOver p] [inst_4 : p.IsMaximal] [inst_5 : q.IsMaximal]
  [inst_6 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_7 : Localization.AtPrime.IsLiesOverAlgebra p q] [Algebra.IsSeparable p.ResidueField q.ResidueField],
  Algebra.IsSeparable (A ⧸ p) (B ⧸ q)
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.adjoin_rootSet' : ∀ {K : Type v} {L : Type w} {inst : Field K} {inst_1 : Field L} {inst_2 : Algebra K L} {f : Polynomial K}
  [self : Polynomial.IsSplittingField K L f], Algebra.adjoin K (f.rootSet L) = ⊤
-- Batteries.CodeAction.Deprecated
/-- A code action which applies replacements for `@[deprecated]` definitions.  -/
Batteries.CodeAction.deprecatedCodeActionProvider : Lean.Server.CodeActionProvider
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.ofFullyFaithful.eq_1 : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] [inst_5 : F.Full]
  [inst_6 : F.Faithful] [inst_7 : CategoryTheory.BraidedCategory D],
  CategoryTheory.BraidedCategory.ofFullyFaithful F =
    CategoryTheory.BraidedCategory.ofFaithful F
      (fun X Y =>
        F.preimageIso
          ((CategoryTheory.Functor.Monoidal.μIso F X Y).symm ≪≫
            β_ (F.obj X) (F.obj Y) ≪≫ CategoryTheory.Functor.Monoidal.μIso F Y X))
      ⋯
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.mk.sizeOf_spec : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J} [inst_3 : SizeOf J]
  (val : F.obj (Opposite.op j))
  (map_zero : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val = val₀)
  (map_succ :
    ∀ (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val =
        d.succ i ⋯ ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val))
  (map_limit :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) val =
        d.lift i hi
          ⟨fun x =>
            match x with
            | Opposite.op ⟨k, hk⟩ => (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val,
            ⋯⟩),
  sizeOf { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit } =
    1 + sizeOf val + sizeOf map_zero
-- Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η]
  [MeasurableSpace.CountableOrCountablyGenerated α β] [MeasureTheory.SFinite μ],
  (μ.compProd κ).AbsolutelyContinuous (ν.compProd η) → ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)
-- Lean.Parser.Command
Lean.Parser.Command.printTacTags.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.mk.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {userData : Array Std.Http.Chunk}
  {outputData : Std.Http.Internal.ChunkedBuffer} {state : Std.Http.Protocol.H1.Writer.State}
  {knownSize : Option Std.Http.Body.Length} {messageHead : Std.Http.Protocol.H1.Message.Head dir.swap}
  {sentMessage userClosedBody omitBody : Bool} {userDataBytes : ℕ} {userData_1 : Array Std.Http.Chunk}
  {outputData_1 : Std.Http.Internal.ChunkedBuffer} {state_1 : Std.Http.Protocol.H1.Writer.State}
  {knownSize_1 : Option Std.Http.Body.Length} {messageHead_1 : Std.Http.Protocol.H1.Message.Head dir.swap}
  {sentMessage_1 userClosedBody_1 omitBody_1 : Bool} {userDataBytes_1 : ℕ},
  { userData := userData, outputData := outputData, state := state, knownSize := knownSize, messageHead := messageHead,
        sentMessage := sentMessage, userClosedBody := userClosedBody, omitBody := omitBody,
        userDataBytes := userDataBytes } =
      { userData := userData_1, outputData := outputData_1, state := state_1, knownSize := knownSize_1,
        messageHead := messageHead_1, sentMessage := sentMessage_1, userClosedBody := userClosedBody_1,
        omitBody := omitBody_1, userDataBytes := userDataBytes_1 } →
    userData = userData_1 ∧
      outputData = outputData_1 ∧
        state = state_1 ∧
          knownSize = knownSize_1 ∧
            messageHead = messageHead_1 ∧
              sentMessage = sentMessage_1 ∧
                userClosedBody = userClosedBody_1 ∧ omitBody = omitBody_1 ∧ userDataBytes = userDataBytes_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.go_Inv_of_Inv : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {w : ℕ}
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig cache →
    ∀ (expr : Std.Tactic.BVDecide.BVExpr w),
      Std.Tactic.BVDecide.BVExpr.Cache.Inv assign (↑(Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr cache).result).aig
        (Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr cache).cache
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- Coercion from `α` to `WithTop α` as an `AddMonoidHom`.  -/
WithTop.addHom : {α : Type u} → [inst : AddMonoid α] → α →+ WithTop α
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.re_inner_starProjection_eq_normSq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (v : E),
  RCLike.re (inner 𝕜 (K.starProjection v) v) = ‖K.orthogonalProjectionOnto v‖ ^ 2
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
/-- The number of times an irreducible factor `p` appears in `normalizedFactors x` is defined by
the number of times it divides `x`.

See also `multiplicity_eq_count_normalizedFactors` if `n` is given by `multiplicity p x`.
 -/
UniqueFactorizationMonoid.count_normalizedFactors_eq : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] [inst_2 : NormalizationMonoid R]
  [inst_3 : DecidableEq R] {p x : R},
  Irreducible p →
    normalize p = p →
      ∀ {n : ℕ}, p ^ n ∣ x → ¬p ^ (n + 1) ∣ x → Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- `exteriorAlgebra.ιMulti` is the alternating map from `Fin n → M` to `⋀[r]^n M`
induced by `exteriorAlgebra.ιMulti`, i.e. sending a family of vectors `m : Fin n → M` to the
product of its entries.  -/
exteriorPower.ιMulti : (R : Type u) →
  [inst : CommRing R] →
    (n : ℕ) → {M : Type u_1} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.uliftFunctor.eq_1 : CommGrpCat.uliftFunctor =
  { obj := fun X => CommGrpCat.of (ULift.{u, v} ↑X),
    map := fun {x x_1} f =>
      CommGrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((CommGrpCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom)),
    map_id := ⋯, map_comp := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoAux_inv_app : ∀ (C : Type u) (X : CategoryTheory.FreeMonoidalCategory C)
  (X_1 : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  (CategoryTheory.FreeMonoidalCategory.normalizeIsoAux C X).inv.app X_1 =
    (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X X_1).inv
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.meas_preimage_singleton_ne_zero : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : Zero β] {μ : MeasureTheory.Measure α}
  {f : MeasureTheory.SimpleFunc α β}, f.FinMeasSupp μ → ∀ {y : β}, y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.forall_congr : ∀ {σs : List (Type u)} {α : Sort u_1} {Φ Ψ : α → Std.Do.SPred σs}, (∀ (a : α), Φ a ⊣⊢ₛ Ψ a) → (∀ a, Φ a) ⊣⊢ₛ ∀ a, Ψ a
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.homotopyEquivalences_inv : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D),
  HomologicalComplex.homotopyEquivalences V c f.inv
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.dualAnnihilator_ker_eq_range_flip : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [Module.IsReflexive K V₂],
  B.ker.dualAnnihilator = B.flip.range
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseIPv6 : Std.Internal.Parsec.ByteArray.Parser Std.Net.IPv6Addr
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l : ∀ {X Y : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X ⟶ Y),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).l =
    (AlgebraicGeometry.Scheme.Modules.pullback f.as.unop).toCatHom
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, k ∈ t₂ → (t₁ \ t₂).get? k = none
-- Mathlib.AlgebraicTopology.DoldKan.Faces
AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Y : C} {n q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  AlgebraicTopology.DoldKan.HigherFacesVanish q φ →
    n < q → CategoryTheory.CategoryStruct.comp φ ((AlgebraicTopology.DoldKan.Hσ q).f (n + 1)) = 0
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapTrifunctorMapMap : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J) {X₁ Y₁ : CategoryTheory.GradedObject I₁ C₁}
  (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : CategoryTheory.GradedObject I₂ C₂} (f₂ : X₂ ⟶ Y₂) {X₃ Y₃ : CategoryTheory.GradedObject I₃ C₃}
  (f₃ : X₃ ⟶ Y₃) [inst_4 : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  [inst_5 : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p] (i₁ : I₁)
  (i₂ : I₂) (i₃ : I₃) (j : J) (h : p (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.GradedObject.mapTrifunctorMapMap F p f₁ f₂ f₃ j) =
    CategoryTheory.CategoryStruct.comp (((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
      (CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃))
        (CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃))
          (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)))
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.diam_range : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), Metric.diam (Set.range ⇑f) = Metric.diam Set.univ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {km fallback : α}, t.maxD fallback = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isEquivalent_atTop_div : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Asymptotics.IsEquivalent Filter.atTop (fun x => Polynomial.eval x P / Polynomial.eval x Q) fun x =>
    P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)
-- Batteries.Lean.PersistentHashMap
/-- Builds a `PersistentHashMap` from an array of key-value pairs. Values of
duplicated keys are replaced by their respective last occurrences.
 -/
Lean.PersistentHashMap.ofArray : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → {β : Type u_2} → Array (α × β) → Lean.PersistentHashMap α β
-- Mathlib.Topology.NoetherianSpace
/-- In a Noetherian space, every closed set is a finite union of irreducible closed sets.  -/
TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] {s : Set α},
  IsClosed s → ∃ S, S.Finite ∧ (∀ t ∈ S, IsClosed t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = ⋃₀ S
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instAlgebra : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [inst_2 : IsOrderedCancelAddMonoid Γ] →
          [inst_3 : CommSemiring R] →
            {A : Type u_6} → [inst_4 : Semiring A] → [Algebra R A] → Algebra R (HahnSeries Γ A)
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.instMonadSimpSimpM : Lean.Meta.MonadSimp Lean.Meta.SimpM
-- Mathlib.FieldTheory.Relrank
Subfield.finrank_comap : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A : Subfield E) (f : L →+* E),
  Module.finrank (↥(Subfield.comap f A)) L = A.relfinrank f.fieldRange
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann.eq_def : ∀ (o : Ordinal.{u}), ZFSet.vonNeumann o = ZFSet.iUnion fun a => (ZFSet.vonNeumann ↑a).powerset
-- Mathlib.Data.Finsupp.Indicator
Finsupp.indicator_eq_set_indicator : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (s : Finset ι) (g : ι → α),
  ⇑(Finsupp.indicator s fun i x => g i) = (↑s).indicator g
-- Init.Data.String.Slice
/-- If `pat` matches a suffix at `pos`, returns the position at the beginning of the match.
Returns `none` otherwise.

This function is generic over all currently supported patterns.
 -/
String.Slice.Pos.revSkip? : {ρ : Type} → {s : String.Slice} → s.Pos → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Option s.Pos
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_sup : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (s t : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂),
  AffineSubspace.map f (s ⊔ t) = AffineSubspace.map f s ⊔ AffineSubspace.map f t