mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Hom.Units
/-- An isomorphism of ordered monoids descends to their units.  -/
OrderMonoidIso.unitsCongr : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] → [inst_1 : Monoid α] → [inst_2 : Preorder β] → [inst_3 : Monoid β] → (α ≃*o β) → αˣ ≃*o βˣ
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicatorAux.eq_1 : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α) (x : α),
  thickenedIndicatorAux δ E x = 1 - Metric.infEDist x E / ENNReal.ofReal δ
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.primeSpectrumEquiv_apply : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (P : PrimeSpectrum ↥A),
  A.primeSpectrumEquiv P = ⟨A.ofPrime P.asIdeal, ⋯⟩
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.snd_surjective : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W), Function.Surjective ⇑(Representation.IntertwiningMap.snd A ρ σ)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.ordered_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => cmp a b = Ordering.lt) t.keys
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.sphere_subset_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.sphere x ε ⊆ Metric.closedBall x ε
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeIso_comp : ∀ {B : Type u} [inst : Quiver B] {a : B} {b c d : CategoryTheory.FreeBicategory B} (p : Quiver.Path a b) (f : b ⟶ c)
  (g : c ⟶ d),
  CategoryTheory.FreeBicategory.normalizeIso p (CategoryTheory.CategoryStruct.comp f g) =
    (CategoryTheory.Bicategory.associator ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) f g).symm ≪≫
      CategoryTheory.Bicategory.whiskerRightIso (CategoryTheory.FreeBicategory.normalizeIso p f) g ≪≫
        CategoryTheory.FreeBicategory.normalizeIso (CategoryTheory.FreeBicategory.normalizeAux p f) g
-- Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
/-- Jacobi's theta-function transformation formula for the sum of `exp -Q(x)`, where `Q` is a
negative definite quadratic form.  -/
Complex.tsum_exp_neg_quadratic : ∀ {a : ℂ},
  0 < a.re →
    ∀ (b : ℂ),
      ∑' (n : ℤ), Complex.exp (-↑Real.pi * a * ↑n ^ 2 + 2 * ↑Real.pi * b * ↑n) =
        1 / a ^ (1 / 2) * ∑' (n : ℤ), Complex.exp (-↑Real.pi / a * (↑n + Complex.I * b) ^ 2)
-- Mathlib.Algebra.Order.CauSeq.Completion
/-- Every Cauchy sequence has a limit.  -/
CauSeq.IsComplete.isComplete : ∀ {α : Type u_1} {inst : Field α} {inst_1 : LinearOrder α} {inst_2 : IsStrictOrderedRing α} {β : Type u_2}
  {inst_3 : Ring β} {abv : β → α} {inst_4 : IsAbsoluteValue abv} [self : CauSeq.IsComplete β abv] (s : CauSeq β abv),
  ∃ b, s ≈ CauSeq.const abv b
-- Mathlib.Topology.Order.Priestley
exists_isClopen_upper_or_lower_of_ne : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] [PriestleySpace α] {x y : α},
  x ≠ y → ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
/-- There exists a continuous `K`-linear map from `SeparationQuotient E` to `E`
such that `mk (outCLM x) = x` for all `x`.

Note that continuity of this map comes for free, because `mk` is a topology inducing map.
 -/
SeparationQuotient.exists_out_continuousLinearMap : ∀ (K : Type u_1) (E : Type u_2) [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul K E],
  ∃ f, SeparationQuotient.mkCLM K E ∘SL f = ContinuousLinearMap.id K (SeparationQuotient E)
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- Given `h : CoreSmallCategoryOfSet Ω C`, this is the
obvious functor `h.smallCategoryOfSet.obj ⥤ C`.  -/
CategoryTheory.CoreSmallCategoryOfSet.functor : {Ω : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (h : CategoryTheory.CoreSmallCategoryOfSet Ω C) → CategoryTheory.Functor (↑h.smallCategoryOfSet.obj) C
-- Mathlib.Data.DFinsupp.Order
DFinsupp.coe_sup : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → SemilatticeSup (α i)]
  (f g : Π₀ (i : ι), α i), ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.op_add : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (f g : X ⟶ Y), (f + g).op = f.op + g.op
-- Mathlib.CategoryTheory.Monad.Algebra
/-- An Eilenberg-Moore coalgebra for a comonad `T`.  -/
CategoryTheory.Comonad.Coalgebra : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Comonad C → Type (max u₁ v₁)
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySheafFor.map_amalgamate : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} (h : E.IsStronglySheafFor F)
  (x : (i : E.I₀) → F.obj (Opposite.op (E.X i)))
  (hc :
    ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
      (CategoryTheory.ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) =
        (CategoryTheory.ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j))
  (i : E.I₀), (CategoryTheory.ConcreteCategory.hom (F.map (E.f i).op)) (h.amalgamate x hc) = x i
-- Mathlib.Analysis.RCLike.Basic
RCLike.continuous_im : ∀ {K : Type u_1} [inst : RCLike K], Continuous ⇑RCLike.im
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerDone_flatMap : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β},
  it₁.IsPlausibleStep Std.IterStep.done → (Std.IterM.flatMapAfter f it₁ none).IsPlausibleStep Std.IterStep.done
-- Std.Data.HashMap.Lemmas
Std.HashMap.erase_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ},
  (Std.HashMap.emptyWithCapacity c).erase a = Std.HashMap.emptyWithCapacity c
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.IsUltra.sup : ∀ {X : Type u_1} {R : Type u_2} [inst : AddZeroClass R] [inst_1 : SemilatticeSup R] [inst_2 : AddLeftMono R]
  [inst_3 : AddRightMono R] {d d' : PseudoMetric X R} [d.IsUltra] [d'.IsUltra], (d ⊔ d').IsUltra
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Submodule.mem_span_image_finset_iff_exists_fun : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} {x : M} {s : Finset α}, x ∈ Submodule.span R (v '' ↑s) ↔ ∃ c, ∑ i, c i • v ↑i = x
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoComp : ∀ {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] (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D)
  {E : Type u_4} [inst_5 : CategoryTheory.Category.{v_3, u_4} E] [inst_6 : CategoryTheory.HasShift E A]
  (G : CategoryTheory.Functor D E) [inst_7 : F.CommShift A] [inst_8 : G.CommShift A],
  CategoryTheory.NatTrans.CommShift (CategoryTheory.NatTrans.OppositeShift.natIsoComp A F G).hom A
-- Init.Data.Order.Classes
Std.MaxEqOr.max_eq_or : ∀ {α : Type u} {inst : Max α} [self : Std.MaxEqOr α] (a b : α), a ⊔ b = a ∨ a ⊔ b = b
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.coe_algebraMap_over_bot : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  ⇑(algebraMap (↥⊥) F) = ⇑(IntermediateField.botEquiv F E)
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.ChainComplex.augment.match_3.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) →
    (Unit → motive 1 0) →
      ((i j : ℕ) → motive i.succ j.succ) →
        ((x x_2 : ℕ) → (x = 1 → x_2 = 0 → False) → (∀ (i j : ℕ), x = i.succ → x_2 = j.succ → False) → motive x x_2) →
          motive x x_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.symmetry' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : C) [inst_1 : CategoryTheory.Limits.HasBinaryProduct P Q]
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct Q P],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
      (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) =
    CategoryTheory.CategoryStruct.id (P ⨯ Q)
-- Mathlib.Data.Fin.VecNotation
Matrix.empty_vecAlt1 : ∀ (α : Type u_1) {h : 0 = 0 + 0}, Matrix.vecAlt1 h ![] = ![]
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.isUnit_iff_mulLeft_bijective : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit a ↔ Function.Bijective fun x => a * x
-- Mathlib.Control.Functor
Functor.map_comp_map : ∀ {F : Type u → Type v} {α β γ : Type u} [inst : Functor F] [LawfulFunctor F] (f : α → β) (g : β → γ),
  ((fun x => g <$> x) ∘ fun x => f <$> x) = fun x => (g ∘ f) <$> x
-- Mathlib.Analysis.Matrix.Normed
/-- Normed space instance (using sup norm of sup norm) for matrices over a normed space.  Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.normedSpace : {R : Type u_1} →
  {m : Type u_3} →
    {n : Type u_4} →
      {α : Type u_5} →
        [inst : Fintype m] →
          [inst_1 : Fintype n] →
            [inst_2 : NormedField R] →
              [inst_3 : SeminormedAddCommGroup α] → [NormedSpace R α] → NormedSpace R (Matrix m n α)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.diff.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t₁ t₁_1 : Std.ExtTreeMap α β cmp),
  t₁ = t₁_1 → ∀ (t₂ t₂_1 : Std.ExtTreeMap α β cmp), t₂ = t₂_1 → t₁.diff t₂ = t₁_1.diff t₂_1
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instFunLike : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] → [inst_1 : PseudoMetricSpace β] → FunLike (BoundedContinuousFunction α β) α β
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Sheaf.isLocallySurjective_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) (ψ : F₂ ⟶ F₃) [CategoryTheory.Sheaf.IsLocallySurjective φ]
  [CategoryTheory.Sheaf.IsLocallySurjective ψ],
  CategoryTheory.Sheaf.IsLocallySurjective (CategoryTheory.CategoryStruct.comp φ ψ)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.whisker_right : {B : Type u} →
  [inst : Quiver B] →
    {a b c : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (h : b ⟶ c) →
          CategoryTheory.FreeBicategory.Hom₂ f g →
            CategoryTheory.FreeBicategory.Hom₂ (CategoryTheory.FreeBicategory.Hom.comp f h)
              (CategoryTheory.FreeBicategory.Hom.comp g h)
-- Lean.CoreM
Lean.Core.instMonadLogCoreM : Lean.MonadLog Lean.CoreM
-- Mathlib.CategoryTheory.ComposableArrows.Three
CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
  (f₁₂ : i ⟶ k) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂),
  (CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 0 = f₁
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.StrongTrans.Modification η θ},
  x = y ↔ x.app = y.app
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_mul_induction : ∀ {R : Type u_1} [inst : Semiring R] (cf cg N O : ℕ) (f g : Polynomial R),
  f.support.card ≤ cf.succ →
    g.support.card ≤ cg.succ →
      f.natDegree ≤ N →
        g.natDegree ≤ O → Polynomial.reflect (N + O) (f * g) = Polynomial.reflect N f * Polynomial.reflect O g
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
/-- The transcendence degree of a commutative algebra `A` over a commutative ring `R` is
defined to be the maximal cardinality of an `R`-algebraically independent set in `A`.  -/
Algebra.trdeg : (R : Type u_2) → (A : Type v) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Cardinal.{v}
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functoriality_obj_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Limits.Cone.functoriality F G).obj A).pt = G.obj A.pt
-- Mathlib.Logic.Function.Basic
Function.Involutive.rightInverse : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → Function.RightInverse f f
-- Init.Data.Int.Gcd
Int.gcd_comm : ∀ (a b : ℤ), a.gcd b = b.gcd a
-- Mathlib.CategoryTheory.GradedObject.Single
CategoryTheory.GradedObject.single_map_singleObjApplyIsoOfEq_hom : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) (i : J)
  (h : i = j),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f i)
      (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j Y i h).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h).hom f
-- Init.Grind.Module.Basic
Lean.Grind.NatModule.one_nsmul : ∀ {M : Type u} [inst : Lean.Grind.NatModule M] (a : M), 1 • a = a
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.constr_def : ∀ {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M'] (S : Type u_13)
  [inst_5 : Semiring S] [inst_6 : Module S M'] [inst_7 : SMulCommClass R S M'] (f : ι → M'),
  (b.constr S) f = Finsupp.linearCombination R id ∘ₗ Finsupp.lmapDomain R R f ∘ₗ ↑b.repr
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The equivalence between continuous representations.  -/
ContRepresentation.Equiv : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            ContRepresentation R G V → ContRepresentation R G W → Type (max u_3 u_4)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (G : CategoryTheory.ComposableArrows C n),
  (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows G).F = G
-- Std.Sat.AIG.Basic
/-- Flip the inverter bit according to `val`.
 -/
Std.Sat.AIG.Fanin.flip : Std.Sat.AIG.Fanin → Bool → Std.Sat.AIG.Fanin
-- Mathlib.MeasureTheory.MeasurableSpace.Card
/-- `generateMeasurableRec s ω₁` generates precisely the smallest sigma-algebra containing `s`.  -/
MeasurableSpace.generateMeasurable_eq_rec : ∀ {α : Type u} (s : Set (Set α)),
  {t | MeasurableSpace.GenerateMeasurable s t} = MeasurableSpace.generateMeasurableRec s (Ordinal.omega 1)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Split.instInhabitedState : Inhabited Lean.Meta.Grind.Split.State
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.forIn'_congr : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_6 : Monad m] {γ : Type u} {init init' : γ}
  {r r' : Std.Roo α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)}
  (hr : r = r'),
  init = init' → (∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) → forIn' r init f = forIn' r' init' f'
-- Mathlib.Analysis.Normed.Group.ControlledClosure
/-- Given `f : NormedAddGroupHom G H` for some complete `G`, if every element `x` of the image of
an isometric immersion `j : NormedAddGroupHom K H` has a preimage under `f` whose norm is at most
`C*‖x‖` then the same holds for elements of the (topological) closure of this image with constant
`C+ε` instead of `C`, for any positive `ε`.
This is useful in particular if `j` is the inclusion of a normed group into its completion
(in this case the closure is the full target group).
 -/
controlled_closure_range_of_complete : ∀ {G : Type u_1} [inst : NormedAddCommGroup G] [CompleteSpace G] {H : Type u_2} [inst_2 : NormedAddCommGroup H]
  {f : NormedAddGroupHom G H} {K : Type u_3} [inst_3 : SeminormedAddCommGroup K] {j : NormedAddGroupHom K H},
  (∀ (x : K), ‖j x‖ = ‖x‖) →
    ∀ {C ε : ℝ},
      0 < C →
        0 < ε → (∀ (k : K), ∃ g, f g = j k ∧ ‖g‖ ≤ C * ‖k‖) → f.SurjectiveOnWith j.range.topologicalClosure (C + ε)
-- Mathlib.Topology.Instances.Int
Int.closedBall_eq_Icc : ∀ (x : ℤ) (r : ℝ), Metric.closedBall x r = Set.Icc ⌈↑x - r⌉ ⌊↑x + r⌋
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_ofNatLT : ∀ {n : ℕ} (x : ℕ) (lt : x < 2 ^ n) (i : ℕ), (x#'lt).getLsbD i = x.testBit i
-- Mathlib.Data.Fin.Tuple.Take
/-- `Fin.take` intertwines with `List.take` via `List.get`.  -/
Fin.get_take_eq_take_get_comp_cast : ∀ {α : Type u_2} {m : ℕ} (l : List α) (h : m ≤ l.length), (List.take m l).get = Fin.take m h l.get ∘ Fin.cast ⋯
-- Mathlib.Topology.Algebra.Order.Field
IsStrictOrderedRing.toContinuousInv₀ : ∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] [ContinuousMul 𝕜], ContinuousInv₀ 𝕜
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.mk.sizeOf_spec : ∀ {J : Type u_1} [inst : LinearOrder J] [inst_1 : SizeOf J] (as : J), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.Topology.Semicontinuity.Basic
IsClosed.upperSemicontinuousAt_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {x : α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsClosed s → 0 ≤ y → UpperSemicontinuousAt (s.indicator fun _x => y) x
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.unit.eq_1 : ∀ {M : Type u_6} [inst : Monoid M] {x : M} (hx : IsOfFinOrder x),
  hx.unit = { val := x, inv := x ^ (orderOf x - 1), val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The right unitor: `X ⊗ 𝟙_ C ≃ X`  -/
CategoryTheory.MonoidalCategoryStruct.rightUnitor : {C : Type u} →
  {𝒞 : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.MonoidalCategoryStruct C] →
      (X : C) →
        CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ X
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.forget_δ : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.AddMon C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.AddMon.forget C) X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a fallback : α}, m.contains a = false → m.getD a fallback = fallback
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- **Alias** of `sum_apply`. -/
ContinuousMultilinearMap.sum_apply : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α),
  (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x
-- Init.System.IO
/-- The number of hard links to the file.  -/
IO.FS.Metadata.numLinks : IO.FS.Metadata → UInt64
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.equivEquivIso_symm_apply_apply : ∀ {A B : FintypeCat} (i : A ≅ B) (a : A.obj),
  (FintypeCat.equivEquivIso.symm i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.homCategory.ext_iff : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {Γ Δ : η ⟶ θ}, Γ = Δ ↔ ∀ (a : B), Γ.as.app a = Δ.as.app a
-- Init.SizeOf
Lean.SourceInfo.none.sizeOf_spec : sizeOf Lean.SourceInfo.none = 1
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mk.inj : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {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 : ι) → TopologicalSpace (M₁ i)} {inst_6 : TopologicalSpace M₂}
  {toMultilinearMap : MultilinearMap R M₁ M₂} {cont : Continuous toMultilinearMap.toFun}
  {toMultilinearMap_1 : MultilinearMap R M₁ M₂} {cont_1 : Continuous toMultilinearMap_1.toFun},
  { toMultilinearMap := toMultilinearMap, cont := cont } = { toMultilinearMap := toMultilinearMap_1, cont := cont_1 } →
    toMultilinearMap = toMultilinearMap_1
-- Mathlib.CategoryTheory.ConcreteCategory.Elementwise
CategoryTheory.Limits.cokernel.condition_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F]
  (x : carrier X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f))
      ((CategoryTheory.ConcreteCategory.hom f) x) =
    (CategoryTheory.ConcreteCategory.hom 0) x
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
UniformContinuous.nndist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : UniformSpace β] {f g : β → α},
  UniformContinuous f → UniformContinuous g → UniformContinuous fun b => nndist (f b) (g b)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.σ_def : ∀ (p q : ℤ),
  TotalComplexShapeSymmetry.σ (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ) p q = (p * q).negOnePow
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.notConvergentSeq_antitone : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : PseudoEMetricSpace β] {n : ℕ} {f : ι → α → β} {g : α → β}
  [inst_1 : Preorder ι], Antitone (MeasureTheory.Egorov.notConvergentSeq f g n)
-- Mathlib.Algebra.Group.Fin.Basic
Fin.lt_sub_iff : ∀ {n : ℕ} {a b : Fin n}, a < a - b ↔ a < b
-- Init.Data.Function
/-- A function `f : α → β` is called injective if `f x = f y` implies `x = y`.  -/
Function.Injective : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Prop
-- Mathlib.Data.Set.Pairwise.Lattice
Set.pairwise_iUnion₂ : ∀ {α : Type u_1} {s : Set (Set α)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) s → ∀ (r : α → α → Prop), (∀ a ∈ s, a.Pairwise r) → (⋃ a ∈ s, a).Pairwise r