mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- Given a Borel-measurable function from a Polish space to a second-countable space, there exists
a finer Polish topology on the source space for which the function is continuous.  -/
Measurable.exists_continuous : ∀ {α : Type u_3} {β : Type u_4} [t : TopologicalSpace α] [PolishSpace α] [inst : MeasurableSpace α] [BorelSpace α]
  [tβ : TopologicalSpace β] [inst_2 : MeasurableSpace β] [OpensMeasurableSpace β] {f : α → β}
  [SecondCountableTopology ↑(Set.range f)], Measurable f → ∃ t' ≤ t, Continuous f ∧ PolishSpace α
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_symm_eq_iff_map_eq : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {N : Type u_5} [inst_1 : AddGroup N] {H : AddSubgroup N}
  {e : G ≃+ N}, AddSubgroup.map (↑e.symm) H = K ↔ AddSubgroup.map (↑e) K = H
-- Init.Data.SInt.Lemmas
Int8.toInt64_ofNat : ∀ {n : ℕ}, n ≤ 127 → (OfNat.ofNat n).toInt64 = OfNat.ofNat n
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesAt.eventually_differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} [CompleteSpace F],
  HasFPowerSeriesAt f p x → ∀ᶠ (z : E) in nhds x, DifferentiableAt 𝕜 f z
-- Mathlib.Topology.JacobsonSpace
preimage_closedPoints_subset : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Function.Injective f → Continuous f → f ⁻¹' closedPoints Y ⊆ closedPoints X
-- Mathlib.NumberTheory.Divisors
/-- `divisors z` is the `Finset` of divisors of `z`. By convention, we set `divisors 0 = ∅`.  -/
Int.divisors : ℤ → Finset ℤ
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.norm_surjective : ∀ {α : Type u_1} [inst : DecidableEq α] [Nonempty α], Function.Surjective FreeGroup.norm
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.equivQuotMaximalIdealPow_apply_mk : ∀ {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] (Rₚ : Type u_8) [inst_2 : CommRing Rₚ]
  [inst_3 : Algebra R Rₚ] [inst_4 : IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ] (n : ℕ) (x : R),
  (IsLocalization.AtPrime.equivQuotMaximalIdealPow p Rₚ n) ((Ideal.Quotient.mk (p ^ n)) x) =
    (Ideal.Quotient.mk (IsLocalRing.maximalIdeal Rₚ ^ n)) ((algebraMap R Rₚ) x)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.tprod_mul_tprod_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [T2Space α]
  [ContinuousMul α] {s : Set β},
  Multipliable (f ∘ Subtype.val) →
    Multipliable (f ∘ Subtype.val) → (∏' (x : ↑s), f ↑x) * ∏' (x : ↑sᶜ), f ↑x = ∏' (x : β), f x
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_singleton : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M) {a : α}, v.restrict {a} = MeasureTheory.VectorMeasure.dirac a (v {a})
-- Batteries.Data.AssocList
Batteries.AssocList.toList.eq_def : ∀ {α : Type u_1} {β : Type u_2} (x : Batteries.AssocList α β),
  x.toList =
    match x with
    | Batteries.AssocList.nil => []
    | Batteries.AssocList.cons a b es => (a, b) :: es.toList
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- The last element of a nonempty Dyck word is `D`.  -/
DyckWord.getLast_eq_D : ∀ (p : DyckWord) (h : ↑p ≠ []), (↑p).getLast h = DyckStep.D
-- Mathlib.MeasureTheory.Measure.Regular
/-- **Alias** of `MeasurableSet.exists_isCompact_sdiff_lt`.

---

If `μ` is inner regular for finite measure sets with respect to compact sets,
then any measurable set of finite measure can be approximated by a
compact subset. See also `MeasurableSet.exists_isCompact_lt_add` and
`MeasurableSet.exists_lt_isCompact_of_ne_top`.  -/
MeasurableSet.exists_isCompact_diff_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [OpensMeasurableSpace α] [T2Space α] [μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
  MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ K ⊆ A, IsCompact K ∧ μ (A \ K) < ε
-- Mathlib.Data.Set.Prod
Set.univ_pi_singleton : ∀ {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → α i), (Set.univ.pi fun i => {f i}) = {f}
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.fromExpr? : Lean.Expr → Lean.Meta.SimpM (Option Fin.Value✝)
-- Mathlib.Data.Sum.Basic
Sum.elim_injective' : ∀ {α : Type u} {β : Type v} {γ : Sort u_3} {f : α → γ}, Function.Injective (Sum.elim f)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.equiv_iff_keys_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.keys = t₂.keys)
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.int_rawCast_neg : ∀ {n : ℕ} {R : Type u_3} [inst : Ring R], (Int.negOfNat n).rawCast = -n.rawCast
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.ext : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f g : SchwartzMap E F}, (∀ (x : E), f x = g x) → f = g
-- Mathlib.Order.Minimal
maximal_subset_iff' : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α}, Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → s ⊆ t → t ⊆ s
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_rightUnitor_hom_eq_rightUnitor_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V] (D : Type u₃)
  [inst_4 : CategoryTheory.Category.{v₃, u₃} D] [inst_5 : CategoryTheory.MonoidalCategoryStruct D]
  [inst_6 : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] (d : D)
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)],
  (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor d).hom =
    (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d)).hom
-- Mathlib.Analysis.Convex.Between
right_mem_affineSegment : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] (x y : P), y ∈ affineSegment R x y
-- Init.Data.Vector.Monadic
Vector.foldlM_attachWith : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] {xs : Vector α n} {q : α → Prop}
  (H : ∀ a ∈ xs, q a) {f : β → { x // q x } → m β} {b : β},
  Vector.foldlM f b (xs.attachWith q H) =
    Vector.foldlM
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b xs.attach
-- Mathlib.Computability.Encoding
/-- Deprecated: `Γ` is now an explicit parameter of `Encoding`.  -/
Computability.Encoding.Γ : {α : Type u} → {Γ : Type v} → Computability.Encoding α Γ → Type v
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_ext_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {X Y : C} {f : J → C}
  {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j)) =
        CategoryTheory.CategoryStruct.comp h
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j))) →
    g = h
-- Mathlib.Algebra.Group.Ext
CommGroup.toGroup_injective : ∀ {G : Type u_1}, Function.Injective (@CommGroup.toGroup G)
-- Mathlib.Analysis.Convex.Between
Wbtw.map : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {x y z : P},
  Wbtw R x y z → ∀ (f : P →ᵃ[R] P'), Wbtw R (f x) (f y) (f z)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Neg β] (f : MeasureTheory.SimpleFunc α β),
  ⇑(-f) = -⇑f
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.associator_hom_apply_1 : ∀ {X Y Z : TopCat}
  {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) x).1 = x.1.1
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
/-- [Stacks Tag 0AH8](https://stacks.math.columbia.edu/tag/0AH8) -/
AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ S) (s : ↥S),
  (⇑f '' ⇑(CategoryTheory.CategoryStruct.comp f g) ⁻¹' {s}).Finite →
    ∀ [AlgebraicGeometry.IsProper (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsSeparated g]
      [AlgebraicGeometry.LocallyOfFiniteType g],
      ∃ U,
        s ∈ U ∧
          AlgebraicGeometry.IsFinite (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.imageι f) g ∣_ U)
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_min : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a b : ℤ}, ↑(min a b) = min ↑a ↑b
-- Mathlib.Topology.EMetricSpace.Defs
instEMetricSpaceMultiplicative : {X : Type u_1} → [EMetricSpace X] → EMetricSpace (Multiplicative X)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_prod_range_succ : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β}
  [inst : CommMonoid β] [MeasurableMul₂ β] {f : ℕ → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ℕ), Measurable (f i)) → ∀ (n : ℕ), ProbabilityTheory.IndepFun (∏ j ∈ Finset.range n, f j) (f n) μ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.isIntegral_of_exists_lift : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] {W : WeierstrassCurve K},
  (∃ r₁, (algebraMap R K) r₁ = W.a₁) →
    (∃ r₂, (algebraMap R K) r₂ = W.a₂) →
      (∃ r₃, (algebraMap R K) r₃ = W.a₃) →
        (∃ r₄, (algebraMap R K) r₄ = W.a₄) → (∃ r₆, (algebraMap R K) r₆ = W.a₆) → WeierstrassCurve.IsIntegral R W
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.of_carrier : ∀ (R : Type u) [inst : CommRing R] (X : Type v) [inst_1 : Ring X] [inst_2 : Bialgebra R X],
  (BialgCat.of R X).carrier = X
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  a ∉ t → t.getKeyD a fallback = fallback
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.BinaryCoproductsDisjoint.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (X Y : C), CategoryTheory.Limits.BinaryCoproductDisjoint X Y) → CategoryTheory.Limits.BinaryCoproductsDisjoint C
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.trivial_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Mon.trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k : α}, (List.map Sigma.fst l).contains k = false → (Std.DHashMap.Raw.ofList l).get? k = none
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instSub : {R : Type u_1} → {a b : R} → [Sub R] → Sub (QuadraticAlgebra R a b)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.Candidate.π_desc_assoc : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts V] {u v : CategoryTheory.Arrow V} (f : u ⟶ v)
  {w : CategoryTheory.Arrow V} (g : v ⟶ w)
  (h : CategoryTheory.Arrow.RightHomotopy (CategoryTheory.CategoryStruct.comp f g) 0) {Z : CategoryTheory.Arrow V}
  (h_1 : w ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Preadditive.RightFreyd.Candidate.π f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Preadditive.RightFreyd.Candidate.desc f g h) h_1) =
    CategoryTheory.CategoryStruct.comp g h_1
-- Mathlib.Order.Hom.WithTopBot
WithBot.subtypeOrderIso.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : DecidablePred fun x => x = ⊥],
  WithBot.subtypeOrderIso =
    {
      toEquiv :=
        { toFun := fun a => WithBot.unbotD ⊥ (WithBot.map Subtype.val a),
            invFun := fun a => if h : a = ⊥ then ⊥ else ↑⟨a, h⟩, left_inv := ⋯, right_inv := ⋯,
            map_rel_iff' := ⋯ }.toEquiv,
      map_rel_iff' := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Map
/-- A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map,
use `Subgroup.equivMapOfInjective`.  -/
MulEquiv.subgroupMap : {G : Type u_1} →
  {G' : Type u_2} →
    [inst : Group G] → [inst_1 : Group G'] → (e : G ≃* G') → (H : Subgroup G) → ↥H ≃* ↥(Subgroup.map (↑e) H)
-- Mathlib.Order.ULift
ULift.instBEq_mathlib : {α : Type u} → [BEq α] → BEq (ULift.{v, u} α)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The circumradius is non-negative.  -/
Affine.Simplex.circumradius_nonneg : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n), 0 ≤ s.circumradius
-- Mathlib.Order.Heyting.Basic
IsCompl.eq_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, IsCompl a b → a = bᶜ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_inter!_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₂.isEmpty = true → (m₁.inter! m₂).isEmpty = true
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A group is commutative if the quotient by the center is cyclic.
Also see `addCommGroupOfCyclicCenterQuotient` for the `AddCommGroup` instance.  -/
AddMonoidHom.isAddCommutative_of_isAddCyclic_of_ker_le_center : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] [IsAddCyclic G'] (f : G →+ G'),
  f.ker ≤ AddSubgroup.center G → IsAddCommutative G
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.domChart.congr_simp : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G]
  {I I_1 : ModelWithCorners 𝕜 E H} (e_I : I = I_1) {J J_1 : ModelWithCorners 𝕜 E'' G} (e_J : J = J_1) {M : Type u_11}
  {N : Type u_13} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N]
  [inst_12 : ChartedSpace G N] {n n_1 : WithTop ℕ∞} (e_n : n = n_1) {f f_1 : M → N} (e_f : f = f_1) {x x_1 : M}
  (e_x : x = x_1) (h : Manifold.IsSubmersionAtOfComplement F I J n f x), h.domChart = ⋯.domChart
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- **Alias** of the forward direction of `SimpleGraph.degree_eq_zero`. -/
SimpleGraph.IsIsolated.of_degree_eq_zero : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], G.degree v = 0 → G.IsIsolated v
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearEquiv.coeFn_ofBijective : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] (f : E →SL[σ] F) (hinj : (↑f).ker = ⊥) (hsurj : (↑f).range = ⊤),
  ⇑(ContinuousLinearEquiv.ofBijective f hinj hsurj) = ⇑f
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
/-- For a norm-continuous group homomorphism `f`, its lift to the separation quotient
is bounded by the norm of `f`.  -/
SeparationQuotient.norm_liftNormedAddGroupHom_le : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (f : NormedAddGroupHom M N) (hf : ∀ (s : M), ‖s‖ = 0 → f s = 0), ‖SeparationQuotient.liftNormedAddGroupHom f hf‖ ≤ ‖f‖
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the reverse direction of `Order.pred_ne_pred_iff`. -/
Order.pred_ne_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  a ≠ b → Order.pred a ≠ Order.pred b
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
CategoryTheory.Enriched.HasConicalLimit.toHasLimit : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {V : outParam (Type u')}
  {inst_1 : CategoryTheory.Category.{v', u'} V} {inst_2 : CategoryTheory.MonoidalCategory V} {C : Type u}
  {inst_3 : CategoryTheory.Category.{v, u} C} {inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C}
  {F : CategoryTheory.Functor J C} [self : CategoryTheory.Enriched.HasConicalLimit V F],
  CategoryTheory.Limits.HasLimit F
-- Lean.Parser.Term.Doc
/-- The notation in question.  -/
Lean.Parser.Term.Doc.RecommendedSpelling.notation : Lean.Parser.Term.Doc.RecommendedSpelling → String
-- Mathlib.Order.SymmDiff
le_bihimp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, b ⊓ c ≤ a → a ⊓ c ≤ b → c ≤ bihimp a b
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_left_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P) (c : ℝ),
  ((signedDist v) p) ((AffineMap.lineMap p q) c) = c * ((signedDist v) p) q
-- Std.Data.DHashMap.AdditionalOperations
Std.DHashMap.Raw.WF.map : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β},
  m.WF → ∀ {f : (a : α) → β a → δ a}, (Std.DHashMap.Raw.map f m).WF
-- Lean.Elab.BuiltinTerm
_private.Lean.Elab.BuiltinTerm.0.Lean.Elab.Term.evalFilePathUnsafe : Lean.Syntax → Lean.Elab.TermElabM System.FilePath
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.image_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β),
  ⇑e.symm '' s = ⇑e ⁻¹' s
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.instFullSheafTypeYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical], J.yoneda.Full
-- Mathlib.Data.Set.Finite.Powerset
Set.Finite.powerset : ∀ {α : Type u} {s : Set α}, s.Finite → (𝒫 s).Finite
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.toPartialEquivOfImageEq_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β) (h : ⇑e '' s = t),
  ↑(e.toPartialEquivOfImageEq s t h) = ⇑e
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Collector.visitApp : Lean.Expr → Lean.Meta.FunIndInfo → Array Lean.Expr → Lean.Meta.FunInd.Collector.M Unit
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a `NormedCommGroup` from a `SeminormedCommGroup` satisfying
`∀ x, ‖x‖ = 0 → x = 1`. This avoids having to go back to the `(Pseudo)MetricSpace` level when
declaring a `NormedCommGroup` instance as a special case of a more general `SeminormedCommGroup`
instance.  -/
NormedCommGroup.ofSeparation : {E : Type u_5} → [inst : SeminormedCommGroup E] → (∀ (x : E), ‖x‖ = 0 → x = 1) → NormedCommGroup E
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipPrefix?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.LawfulForwardPattern pat]
  {s : String.Slice}, s.skipPrefix? pat = none ↔ s.startsWith pat = false
-- Qq.Typ
/-- Creates a quoted expression.  Requires that `e` has type `α`.

You should usually write this using the notation `q($e)`.
 -/
Qq.Quoted.unsafeMk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.negMulLog_lt_one_sub_self : ∀ {x : ℝ}, 0 ≤ x → x ≠ 1 → x.negMulLog < 1 - x
-- Mathlib.Logic.Basic
/-- We intentionally restrict the type of `α` in this lemma so that this is a safer to use in simp
than `forall_comm`.  -/
imp_forall_iff : ∀ {α : Type u_3} {p : Prop} {q : α → Prop}, (p → ∀ (x : α), q x) ↔ ∀ (x : α), p → q x
-- Mathlib.Topology.Algebra.Monoid
/-- Eta-expanded form of `ContinuousOn.pow` -/
ContinuousOn.fun_pow : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Monoid M]
  [ContinuousMul M] {f : X → M} {s : Set X}, ContinuousOn f s → ∀ (n : ℕ), ContinuousOn (fun i => f i ^ n) s
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.map_fst : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
  (T : Turing.Tape Γ), (Turing.Tape.map f T).head = f.f T.head
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_mul_closedBall : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E),
  {x} * Metric.closedBall y δ = Metric.closedBall (x * y) δ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_filter_eq_size_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool},
  (Std.ExtDTreeMap.filter f t).size = t.size ↔
    ∀ (a : α) (h : a ∈ t), f (t.getKey a h) (Std.ExtDTreeMap.Const.get t a h) = true
-- Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
MeasureTheory.IsZeroOneMeasure.exists_measure_eq_one_iff_measure_univ_eq_one : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOneMeasure μ],
  (∃ s, μ s = 1) ↔ μ Set.univ = 1
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_2} {c : ComplexShape ι} {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁)
  (h : i₀ ≠ i₁) (X : C) {K : HomologicalComplex C c}
  (φ₀ : ((HomologicalComplex.eval C c i₀).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).obj K),
  (HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId hi₀₁ h X).homEquiv.symm φ₀ =
    HomologicalComplex.mkHomFromDouble hi₀₁ h φ₀ (CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁)) ⋯ ⋯
-- Lean.Expr
Lean.Expr.instToString : ToString Lean.Expr
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_three_gt_d9 : 1.0986122885 < Real.log 3