mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_rcc : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : LE α]
  [inst_5 : DecidableLE α] [inst_6 : Std.PRange.UpwardEnumerable α] [inst_7 : Std.Rxc.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLE α] {xs : Std.Rcc α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Data.ENNReal.Action
/-- An `Algebra` over `ℝ≥0∞` restricts to an `Algebra` over `ℝ≥0`.  -/
ENNReal.instAlgebraNNReal : {A : Type u_1} → [inst : Semiring A] → [Algebra ENNReal A] → Algebra NNReal A
-- Mathlib.RingTheory.Perfection
ModP.instNontrivialOfPrimeOfFactNotIsUnitCast : ∀ (O : Type u₂) [inst : CommRing O] (p : ℕ) [hp : Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p], Nontrivial (ModP O p)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instSMulCommClass : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) [SMulCommClass R A A], SMulCommClass R ↥S ↥S
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instInhabitedMatcherInfo : Inhabited Lean.Meta.MatcherInfo
-- Mathlib.Data.Finset.Sups
Finset.infs_left_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t u : Finset α), s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)
-- Mathlib.Analysis.Normed.Group.Bounded
HasCompactSupport.exists_bound_of_continuous : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
  HasCompactSupport f → Continuous f → ∃ C, ∀ (x : α), ‖f x‖ ≤ C
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.instIsRegularCardinalOrder : IsRegularCardinalOrder Cardinal.{u_1}
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Pos.find?_prop_eq_find?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String} {pos : s.Pos}, pos.find? p = pos.find? fun x => decide (p x)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.mono : ∀ {G : Type u_1} {β : Type u_5} [inst : AddMonoid G] {x : G} [inst_1 : AddMonoid β] {y : β},
  IsOfFinAddOrder x → addOrderOf y ∣ addOrderOf x → IsOfFinAddOrder y
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.ev_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ GrpCat) {I : Type w'}
  (U : I → C) (γ : CategoryTheory.PresheafOfGroups.OneCocycle G U) (i : I) ⦃T : C⦄ (a : T ⟶ U i), γ.ev i i a a = 1
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.coe_trans_orderIso : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Add α] [inst_4 : Add β] [inst_5 : Add γ] (f : α ≃+o β) (g : β ≃+o γ), ↑(f.trans g) = (↑f).trans ↑g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.modify_equiv_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α} (f : β k → β k), (↑(m₁.modify k f)).Equiv ↑(m₂.modify k f)
-- Init.Data.BitVec.Lemmas
BitVec.not_eq_neg_add : ∀ {w : ℕ} (x : BitVec w), ~~~x = -x - 1#w
-- Mathlib.Order.Interval.Finset.Nat
Nat.Ioc_succ_singleton : ∀ (b : ℕ), Finset.Ioc b (b + 1) = {b + 1}
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.widthInfty.eq_1 : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)), 𝒢.widthInfty = 𝒢.adjoinNegOne.strictWidthInfty
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.congr : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f g : α → E} {s : Set α},
  Set.EqOn f g s → eVariationOn f s = eVariationOn g s
-- Mathlib.Algebra.Order.Module.Defs
SMulPosReflectLT.toSMulPosReflectLE : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β]
  [inst_3 : PartialOrder α] [inst_4 : PartialOrder β] [IsDomain α] [Module.IsTorsionFree α β] [SMulPosReflectLT α β],
  SMulPosReflectLE α β
-- Mathlib.RingTheory.DedekindDomain.Different
traceForm_dualSubmodule_adjoin : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra A K] [inst_4 : Algebra K L] [inst_5 : Algebra A L] [inst_6 : IsScalarTower A K L] [IsDomain A]
  [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegrallyClosed A] {x : L},
  K[x] = ⊤ →
    IsIntegral A x →
      (Algebra.traceForm K L).dualSubmodule (Subalgebra.toSubmodule A[x]) =
        ((Polynomial.aeval x) (Polynomial.derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule A[x]
-- Mathlib.Data.Finset.Image
Function.Commute.finset_map : ∀ {α : Type u_1} {f g : α ↪ α}, Function.Commute ⇑f ⇑g → Function.Commute (Finset.map f) (Finset.map g)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.ComonadicLeftAdjoint L],
  (CategoryTheory.Comonad.comparison (CategoryTheory.comonadicAdjunction L)).IsEquivalence
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentations.mk.sizeOf_spec : ∀ (presentations : Array ProofWidgets.ExprPresentationData),
  sizeOf { presentations := presentations } = 1 + sizeOf presentations
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Structure for sparse matrices over ℚ, implemented as an array of hashmaps, containing only nonzero
values.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix : ℕ → ℕ → Type
-- Init.Data.UInt.Lemmas
UInt8.mod_self : ∀ {a : UInt8}, a % a = 0
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isLoop_iff_forall_notMem_isBase : ∀ {α : Type u_1} {M : Matroid α} {e : α},
  autoParam (e ∈ M.E) Matroid.isLoop_iff_forall_notMem_isBase._auto_1 → (M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B)
-- Mathlib.Tactic.DefEqTransformations
/-- `reduce at loc` completely reduces the given location.
This also exists as a `conv`-mode tactic.

This does the same transformation as the `#reduce` command.
 -/
Mathlib.Tactic.tacticReduce__ : Lean.ParserDescr
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `X + y`
has Gaussian law with mean `μ + y` and variance `v`.  -/
ProbabilityTheory.gaussianReal_add_const : ∀ {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasLaw X (ProbabilityTheory.gaussianReal μ v) P →
    ∀ (y : ℝ), ProbabilityTheory.HasLaw (fun ω => X ω + y) (ProbabilityTheory.gaussianReal (μ + y) v) P
-- Mathlib.Data.Int.CardIntervalMod
Int.Ioc_filter_dvd_eq : ∀ (a b : ℤ) {r : ℤ} (hr : 0 < r),
  {x ∈ Finset.Ioc a b | r ∣ x} = Finset.map { toFun := fun x => x * r, inj' := ⋯ } (Finset.Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)
-- Mathlib.Logic.Equiv.Set
Equiv.ofLeftInverse'_eq_ofInjective : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (f_inv : β → α) (hf : Function.LeftInverse f_inv f),
  Equiv.ofLeftInverse' f f_inv hf = Equiv.ofInjective f ⋯
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.mk.inj : ∀ {α : Type u_8} {β : Type u_9} {inst : CompleteLattice α} {inst_1 : CompleteLattice β} {tosInfHom : sInfHom α β}
  {map_sSup' : ∀ (s : Set α), tosInfHom.toFun (sSup s) = sSup (tosInfHom.toFun '' s)} {tosInfHom_1 : sInfHom α β}
  {map_sSup'_1 : ∀ (s : Set α), tosInfHom_1.toFun (sSup s) = sSup (tosInfHom_1.toFun '' s)},
  { tosInfHom := tosInfHom, map_sSup' := map_sSup' } = { tosInfHom := tosInfHom_1, map_sSup' := map_sSup'_1 } →
    tosInfHom = tosInfHom_1
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.HasTrivialRadical.radical_eq_bot : ∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  [self : LieAlgebra.HasTrivialRadical R L], LieAlgebra.radical R L = ⊥
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_nonneg_of_forall : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ}, a ≤ b → (∀ (u : ℝ), 0 ≤ f u) → 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr_one : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N), ((CliffordAlgebra.foldr Q f hf) n) 1 = n
-- Mathlib.Order.Category.BoolAlg
typeToBoolAlgOp_map : ∀ {X Y : Type u} (f : X ⟶ Y),
  typeToBoolAlgOp.map f =
    (BoolAlg.ofHom
        (have __src :=
          { toFun := ⇑(CompleteLatticeHom.setPreimage ⇑(CategoryTheory.ConcreteCategory.hom f)), map_sup' := ⋯,
            map_inf' := ⋯ };
        { toFun := ⇑(CompleteLatticeHom.setPreimage ⇑(CategoryTheory.ConcreteCategory.hom f)), map_sup' := ⋯,
          map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })).op
-- Mathlib.CategoryTheory.Category.Basic
/-- Notation for composition of morphisms in a category.  -/
CategoryTheory.«term_≫_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.TaggedPrepartition.unionComplToSubordinate_boxes : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I)
  (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)),
  (π₁.unionComplToSubordinate π₂ hU r).boxes = π₁.boxes ∪ (π₂.toSubordinate r).boxes
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.of_compactSpace : ∀ {α : Type u_2} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : Zero γ] [CompactSpace α] (f : α → γ),
  HasCompactSupport f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Finset.stronglyMeasurable_fun_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M]
  {m : MeasurableSpace α} {ι : Type u_6} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)) → MeasureTheory.StronglyMeasurable fun a => ∏ i ∈ s, f i a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_reverse : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β}, l.reverse.toListModel = l.toListModel.reverse
-- Mathlib.Algebra.Star.Unitary
Unitary.commute_star_self : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (u : ↥(unitary R)), Commute (star u) u
-- Mathlib.Topology.Instances.Rat
NNRat.instContinuousSMulOfIsScalarTowerOfRat : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : MulAction ℚ R] [inst_2 : MulAction ℚ≥0 R] [IsScalarTower ℚ≥0 ℚ R]
  [ContinuousSMul ℚ R], ContinuousSMul ℚ≥0 R
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.StrongTrans F G) {a b : B} {f g : a ⟶ b}
  (η : f ⟶ g) {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (self.app a) (G.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b))
      (CategoryTheory.CategoryStruct.comp (self.naturality g).hom h) =
    CategoryTheory.CategoryStruct.comp (self.naturality f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η)) h)
-- Mathlib.Topology.Sheaves.Functors
/-- The pushforward of a sheaf (by a continuous map) is a sheaf.
 -/
TopCat.Sheaf.pushforward_sheaf_of_sheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) {F : TopCat.Presheaf C X},
  F.IsSheaf → ((TopCat.Presheaf.pushforward C f).obj F).IsSheaf
-- Mathlib.Control.LawfulFix
Part.Fix.approx_le_fix : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (i : ℕ),
  Part.Fix.approx (⇑f) i ≤ Part.fix ⇑f
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
_private.Mathlib.Tactic.CategoryTheory.Coherence.Normalize.0.Mathlib.Tactic.BicategoryLike.evalComp.match_1.eq_1 : ∀ (motive : Mathlib.Tactic.BicategoryLike.Eval.Result → Sort u_1) (ι : Mathlib.Tactic.BicategoryLike.NormalExpr)
  (e_ι : Lean.Expr)
  (h_1 : (ι : Mathlib.Tactic.BicategoryLike.NormalExpr) → (e_ι : Lean.Expr) → motive { expr := ι, proof := e_ι }),
  (match { expr := ι, proof := e_ι } with
    | { expr := ι, proof := e_ι } => h_1 ι e_ι) =
    h_1 ι e_ι
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.support_subset_support_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk v w) (hadj : G.Adj u v),
  p.support ⊆ (SimpleGraph.Walk.cons hadj p).support
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.exists_nnnorm_lt_one : ∀ (K : Type u_1) [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K], ∃ x, 0 < ‖x‖₊ ∧ ‖x‖₊ < 1
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.isQuotientMap_mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] (N : AddSubgroup G),
  Topology.IsQuotientMap QuotientAddGroup.mk
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.instReprWeekday.repr.match_1.eq_1 : ∀ (motive : Std.Time.Weekday → Sort u_1) (h_1 : Unit → motive Std.Time.Weekday.monday)
  (h_2 : Unit → motive Std.Time.Weekday.tuesday) (h_3 : Unit → motive Std.Time.Weekday.wednesday)
  (h_4 : Unit → motive Std.Time.Weekday.thursday) (h_5 : Unit → motive Std.Time.Weekday.friday)
  (h_6 : Unit → motive Std.Time.Weekday.saturday) (h_7 : Unit → motive Std.Time.Weekday.sunday),
  (match Std.Time.Weekday.monday with
    | Std.Time.Weekday.monday => h_1 ()
    | Std.Time.Weekday.tuesday => h_2 ()
    | Std.Time.Weekday.wednesday => h_3 ()
    | Std.Time.Weekday.thursday => h_4 ()
    | Std.Time.Weekday.friday => h_5 ()
    | Std.Time.Weekday.saturday => h_6 ()
    | Std.Time.Weekday.sunday => h_7 ()) =
    h_1 ()
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- The measure of a segment is the distance between its endpoints.  -/
MeasureTheory.hausdorffMeasure_segment : ∀ {E : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] (x y : E), (MeasureTheory.Measure.hausdorffMeasure 1) (segment ℝ x y) = edist x y
-- Lean.Parser.Types
Lean.Parser.instInhabitedInputContext : Inhabited Lean.Parser.InputContext
-- Mathlib.GroupTheory.Torsion
/-- A torsion monoid is isomorphic to its torsion submonoid.  -/
IsMulTorsion.torsionMulEquiv : {G : Type u_1} → [inst : CommMonoid G] → IsMulTorsion G → ↥(CommMonoid.torsion G) ≃* G
-- Init.Data.Repr
/-- Converts a natural number less than `10` to the corresponding Unicode superscript digit character.
Returns `'*'` for other numbers.

Examples:
* `Nat.superDigitChar 3 = '³'`
* `Nat.superDigitChar 7 = '⁷'`
* `Nat.superDigitChar 10 = '*'`
 -/
Nat.superDigitChar : ℕ → Char
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.CostructuredArrow.Hom.ext : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] {P : CategoryTheory.MorphismProperty D}
  {Q : CategoryTheory.MorphismProperty C} [inst_2 : Q.IsMultiplicative] {F : CategoryTheory.Functor C D} {X : D}
  {A B : P.CostructuredArrow Q F X} {f g : A ⟶ B}, f.left = g.left → f = g
-- Mathlib.Data.Setoid.Basic
/-- Given an equivalence relation `r` on `α`, the order-preserving bijection between the set of
equivalence relations containing `r` and the equivalence relations on the quotient of `α` by `r`.  -/
Setoid.correspondence : {α : Type u_1} → (r : Setoid α) → { s // r ≤ s } ≃o Setoid (Quotient r)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.isClosed_ker : ∀ {V₁ : Type u_3} [inst : SeminormedAddCommGroup V₁] {V₂ : Type u_6} [inst_1 : NormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), IsClosed ↑f.ker
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.nodup_keys : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keys.Nodup
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `add_apply`. -/
QuadraticMap.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- If `M ⟶ N` is an epimorphism and that `M` is generated by some sections,
then `N` is generated by the images of these sections.  -/
SheafOfModules.GeneratingSections.ofEpi : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M N : SheafOfModules R} →
              M.GeneratingSections → (p : M ⟶ N) → [CategoryTheory.Epi p] → N.GeneratingSections
-- Batteries.Data.AssocList
Batteries.AssocList.toList_eq_toListTR : @Batteries.AssocList.toList = @Batteries.AssocList.toListTR
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.Products.max_eq_o_cons_tail : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2) [inst_2 : Inhabited I] (l : Profinite.NobelingProof.Products I),
  ↑l ≠ [] → (↑l).head! = Profinite.NobelingProof.term I ho → ↑l = Profinite.NobelingProof.term I ho :: ↑l.Tail
-- Mathlib.Order.Concept
Concept.mk.injEq : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (extent : Set α) (intent : Set β)
  (upperPolar_extent : upperPolar r extent = intent) (lowerPolar_intent : lowerPolar r intent = extent)
  (extent_1 : Set α) (intent_1 : Set β) (upperPolar_extent_1 : upperPolar r extent_1 = intent_1)
  (lowerPolar_intent_1 : lowerPolar r intent_1 = extent_1),
  ({ extent := extent, intent := intent, upperPolar_extent := upperPolar_extent,
        lowerPolar_intent := lowerPolar_intent } =
      { extent := extent_1, intent := intent_1, upperPolar_extent := upperPolar_extent_1,
        lowerPolar_intent := lowerPolar_intent_1 }) =
    (extent = extent_1 ∧ intent = intent_1)
-- Mathlib.Algebra.Order.Module.Defs
OrderedSemiring.toPosSMulMonoNat : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α], PosSMulMono ℕ α
-- Mathlib.RingTheory.Ideal.GoingUp
/-- **Alias** of `Ideal.IsIntegral.comap_lt_comap`. -/
Ideal.IsIntegralClosure.comap_le_comap : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] {I J : Ideal A} [I.IsPrime],
  I < J → Ideal.comap (algebraMap R A) I < Ideal.comap (algebraMap R A) J
-- Mathlib.SetTheory.ZFC.Class
instLEClass : LE Class.{u_1}
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mem_div_iff_of_ne_zero : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K},
  J ≠ 0 → ∀ {x : K}, x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I
-- Init.Prelude
/-- Create array `#[a₁, a₂]`  -/
Array.mkArray2 : {α : Type u} → α → α → Array α
-- Std.Http.Data.Method
/-- Retrieve a report on a resource.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-3.6
 -/
Std.Http.Method.report : Std.Http.Method
-- Mathlib.Data.Set.Basic
Set.eq_univ_of_subset : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s = Set.univ → t = Set.univ
-- Mathlib.Topology.UniformSpace.Defs
IsUniformEmbedding.isUniformInducing : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformEmbedding f → IsUniformInducing f
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : α → β)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.respectsIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), F.relativelyRepresentable.RespectsIso
-- Mathlib.Topology.Baire.BaireMeasurable
tendsto_residual_of_isOpenMap : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → IsOpenMap f → Filter.Tendsto f (residual α) (residual β)
-- Init.Data.Array.Lemmas
Array.reverse_ne_empty_iff : ∀ {α : Type u_1} {xs : Array α}, xs.reverse ≠ #[] ↔ xs ≠ #[]
-- Mathlib.Logic.Equiv.Sum
/-- A subtype of a sum is equivalent to a sum of subtypes.  -/
Equiv.subtypeSum : {α : Type u_9} → {β : Type u_10} → {p : α ⊕ β → Prop} → { c // p c } ≃ { a // p (Sum.inl a) } ⊕ { b // p (Sum.inr b) }
-- Mathlib.Algebra.DirectSum.Basic
/-- If two additive homomorphisms from `⨁ i, β i` are equal on each `of β i y`,
then they are equal.  -/
DirectSum.addHom_ext : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u_1}
  [inst_2 : AddZeroClass γ] ⦃f g : (DirectSum ι fun i => β i) →+ γ⦄,
  (∀ (i : ι) (y : β i), f ((DirectSum.of β i) y) = g ((DirectSum.of β i) y)) → f = g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.compare_getKey?_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  Option.all (fun x => decide (cmp x k = Ordering.eq)) (t.getKey? k) = true
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.cokernelBiproductιIso_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)],
  (CategoryTheory.Limits.cokernelBiproductιIso f i).hom =
    CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.ι f i) 0)
      (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f fun j => ¬j = i) ⋯)
-- Mathlib.Topology.UniformSpace.Closeds
IsUniformInducing.nonemptyCompacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β}
  (hf : IsUniformInducing f), IsUniformInducing (TopologicalSpace.NonemptyCompacts.map f ⋯)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The interior of `u : Opens M` is the preimage of the interior of `M` under the inclusion.  -/
ModelWithCorners.interior_open : ∀ {𝕜 : 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] {u : TopologicalSpace.Opens M},
  ModelWithCorners.interior ↥u = Subtype.val ⁻¹' ModelWithCorners.interior M
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.activateTheoremPatterns : Lean.Name → ℕ → Lean.Meta.Grind.GoalM Unit