mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.Trivialization.contMDiffOn_iff : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  {f : M → Bundle.TotalSpace F E} {s : Set M},
  Set.MapsTo f s e.source →
    (ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f s ↔
      ContMDiffOn IM IB n (fun x => (f x).proj) s ∧
        ContMDiffOn IM (modelWithCornersSelf 𝕜 F) n (fun x => (↑e (f x)).2) s)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.concat.congr_simp : ∀ {X : SSet} {n : ℕ} (self self_1 : X.StrictSegalCore n),
  self = self_1 →
    ∀ (x x_1 : X.obj (Opposite.op { len := 1 })) (e_x : x = x_1) (s s_1 : X.obj (Opposite.op { len := n }))
      (e_s : s = s_1)
      (h :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
          (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
      self.concat x s h = self_1.concat x_1 s_1 ⋯
-- Init.Data.Range.Polymorphic.Char
Char.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE Char
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List (α × β)} {k : α}, k ∈ m.insertMany l → (List.map Prod.fst l).contains k = false → k ∈ m
-- Mathlib.GroupTheory.Nilpotent
/-- Any ascending central series for an additive group is bounded above by the upper
central series.  -/
AddSubgroup.ascending_central_series_le_upper : ∀ {G : Type u_1} [inst : AddGroup G] (H : ℕ → AddSubgroup G),
  AddSubgroup.IsAscendingCentralSeries H → ∀ (n : ℕ), H n ≤ AddSubgroup.upperCentralSeries G n
-- Mathlib.Geometry.Manifold.Instances.Real
instZeroEuclideanQuadrant : {n : ℕ} → Zero (EuclideanQuadrant n)
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionHomologyIso_hom_homologyι_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) (hi : c.prev j = i)
  (hk : c.next j = k) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i')
  (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j] {Z : C}
  (h : K.opcycles j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom
      (CategoryTheory.CategoryStruct.comp (K.homologyι j') h) =
    CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyι j)
      (CategoryTheory.CategoryStruct.comp (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom h)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- `Matrix.conjTranspose` as a `StarRingEquiv` to the opposite ring  -/
Matrix.conjTransposeRingEquiv : (m : Type u_2) →
  (α : Type v) →
    [inst : NonUnitalNonAssocSemiring α] →
      [inst_1 : StarRing α] → [inst_2 : Fintype m] → Matrix m m α ≃⋆+* (Matrix m m α)ᵐᵒᵖ
-- Mathlib.Topology.LocallyConstant.Algebra
/-- Characteristic functions are locally constant functions taking `x : X` to `1` if `x ∈ U`,
where `U` is a clopen set, and `0` otherwise.  -/
LocallyConstant.charFn : {X : Type u_1} →
  (Y : Type u_2) → [inst : TopologicalSpace X] → [MulZeroOneClass Y] → {U : Set X} → IsClopen U → LocallyConstant X Y
-- Mathlib.FieldTheory.Relrank
IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_inf : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E),
  Cardinal.lift.{v, w} ((IntermediateField.comap f A).relrank (IntermediateField.comap f B)) =
    Cardinal.lift.{w, v} (A.relrank (B ⊓ f.fieldRange))
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The quotient `G ⧸ N` of a complete first countable uniform group `G` by a normal subgroup
is itself complete. In contrast to `QuotientGroup.completeSpace_left'`, in this version `G` is
already equipped with a uniform structure.
[N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Even though `G` is equipped with a uniform structure, the quotient `G ⧸ N` does not inherit a
uniform structure, so it is still provided manually via `IsTopologicalGroup.leftUniformSpace`.
In the most common use cases, this coincides (definitionally) with the uniform structure on the
quotient obtained via other means.  -/
QuotientGroup.completeSpace_left : ∀ (G : Type u_1) [inst : Group G] [us : UniformSpace G] [inst_1 : IsLeftUniformGroup G] [FirstCountableTopology G]
  (N : Subgroup G) [inst_3 : N.Normal] [hG : CompleteSpace G], CompleteSpace (G ⧸ N)
-- Init.SizeOf
Bool.sizeOf_eq_one : ∀ (b : Bool), sizeOf b = 1
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_sum : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {α : Type u_2} [inst_1 : DecidableEq σ] {s : Finset α}
  {f : α → MvPolynomial σ R}, (∑ x ∈ s, f x).support ⊆ s.biUnion fun x => (f x).support
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.mk.inj : ∀ {G : Type u_6} {inst : AddGroup G} {toNonarchAddGroupSeminorm : NonarchAddGroupSeminorm G}
  {eq_zero_of_map_eq_zero' : ∀ (x : G), toNonarchAddGroupSeminorm.toFun x = 0 → x = 0}
  {toNonarchAddGroupSeminorm_1 : NonarchAddGroupSeminorm G}
  {eq_zero_of_map_eq_zero'_1 : ∀ (x : G), toNonarchAddGroupSeminorm_1.toFun x = 0 → x = 0},
  { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
      { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm_1,
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 } →
    toNonarchAddGroupSeminorm = toNonarchAddGroupSeminorm_1
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_one : ∀ {α : Type u_1} (M : Type u_3) [inst : One M] (s : Set α), (s.mulIndicator fun x => 1) = fun x => 1
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.mem_support_iff : ∀ {α : Type u_1} (p : PMF α) (a : α), a ∈ p.support ↔ p a ≠ 0
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if the maximum number of E-matching rounds has been reached.  -/
Lean.Meta.Grind.checkMaxEmatchExceeded : Lean.Meta.Grind.GoalM Bool
-- Batteries.Data.AssocList
Batteries.AssocList.isEmpty.eq_1 : ∀ {α : Type u_1} {β : Type u_2}, Batteries.AssocList.nil.isEmpty = true
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.constructors : Array Lean.Name → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_div_iff' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c d : α}, a / b < c / d ↔ a * d < c * b
-- Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Module.Basis.empty.congr_simp : ∀ {ι : Type u_1} {R : Type u_3} (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Subsingleton M] [inst_4 : IsEmpty ι], Module.Basis.empty M = Module.Basis.empty M
-- Mathlib.Data.Num.Lemmas
SNum.lt : LT SNum
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_mem_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k a : α}, a ∈ Std.DTreeMap.Internal.Impl.erase! k t → a ∈ t
-- Init.Data.String.Basic
String.Slice.Pos.prevAux.go.eq_def : ∀ {s : String.Slice} (off : ℕ) (h₁ : off < s.utf8ByteSize),
  String.Slice.Pos.prevAux.go off h₁ =
    if hbyte : (s.getUTF8Byte { byteIdx := off } h₁).IsUTF8FirstByte then { byteIdx := off }
    else
      have this := ⋯;
      match off, h₁, hbyte, this with
      | 0, h₁, hbyte, this => ⋯.elim
      | off.succ, h₁, hbyte, this => String.Slice.Pos.prevAux.go off ⋯
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.take_mem : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)} {n : ℕ} (x : ↥T), List.take n ↑x ∈ T
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` preserves limits if it creates limits and `D` has limits.  -/
CategoryTheory.preservesColimits_of_createsColimits_and_hasColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} D],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.starIsoTerminal_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.WithTerminal.starIsoTerminal.inv =
    CategoryTheory.WithTerminal.starTerminal.from (⊤_ CategoryTheory.WithTerminal C)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.IsSymmetric.zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R], MvPolynomial.IsSymmetric 0
-- Mathlib.Data.Multiset.Count
Multiset.countP_attach : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α),
  Multiset.countP (fun a => p ↑a) s.attach = Multiset.countP p s
-- Mathlib.Algebra.Group.Defs
/-- `NSMul` is an implementation detail of `AddMonoid`. It is needed because it is
impossible to extend `SMul ℕ M` and `SMul ℤ M` at the same time.  -/
NSMul : Type u → Type u
-- Mathlib.Topology.EMetricSpace.Defs
/-- Reformulation of the uniform structure in terms of the extended distance  -/
uniformity_pseudoedist : ∀ {α : Type u} [inst : PseudoEMetricSpace α],
  uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε}
-- Std.Data.HashSet.Basic
/-- Transforms the hash set into a list of elements in some order.  -/
Std.HashSet.toList : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → List α
-- Init.NotationExtra
unexpandMkArray3 : Lean.PrettyPrinter.Unexpander
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- A vector equals a rotation of that vector if and only if the vector or the angle is zero.  -/
Orientation.eq_rotation_self_iff : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) (θ : Real.Angle), x = (o.rotation θ) x ↔ x = 0 ∨ θ = 0
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
/-- The jointly surjective topology on `Scheme` is defined by the same condition as the jointly
surjective pretopology.  -/
AlgebraicGeometry.Scheme.jointlySurjectiveTopology : CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme
-- Mathlib.Data.Prod.Basic
Prod.instReflLex_mathlib_1 : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Refl s], Std.Refl (Prod.Lex r s)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.monotone_degree : ∀ {α : Type u_1} [inst : LinearOrder α], Monotone fun x => Finsupp.degree (ofDegLex x)
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.instFullOverForget : ∀ (S : AlgebraicGeometry.Scheme), (AlgebraicGeometry.Scheme.ProEt.forget S).Full
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.StructuralOfExpr_monoidalComp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g h i : C} [inst_1 : CategoryTheory.MonoidalCoherence g h]
  (η : f ⟶ g) (η' : f ≅ g),
  η'.hom = η →
    ∀ (θ : h ⟶ i) (θ' : h ≅ i),
      θ'.hom = θ → (CategoryTheory.monoidalIsoComp η' θ').hom = CategoryTheory.monoidalComp η θ
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.Clause.relabel_relabel' : ∀ {α : Type u_1} {α_1 : Type u_2} {r1 : α → α_1} {α_2 : Type u_3} {r2 : α_2 → α},
  Std.Sat.CNF.Clause.relabel r1 ∘ Std.Sat.CNF.Clause.relabel r2 = Std.Sat.CNF.Clause.relabel (r1 ∘ r2)
-- Std.Net.Addr
Std.Net.instInhabitedSocketAddress.default : Std.Net.SocketAddress
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.differentiable_sinh : Differentiable ℂ Complex.sinh
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fundamentalSequenceProp_inl_some : ∀ (o a : ONote), o.FundamentalSequenceProp (Sum.inl (some a)) ↔ o.repr = Order.succ a.repr ∧ (o.NF → a.NF)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- A submagma of a right cancellative magma inherits right cancellation.  -/
MulMemClass.isRightCancelMul : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] [IsRightCancelMul M]
  (S : A), IsRightCancelMul ↥S
-- Lean.Parser.Basic
Lean.Parser.atomicFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.symm_mapAddEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Add M] (e : R ≃+ S),
  (AddMonoidAlgebra.mapAddEquiv M e).symm = AddMonoidAlgebra.mapAddEquiv M e.symm
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instMul.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Mul Y],
  LocallyConstant.instMul = { mul := fun f g => { toFun := ⇑f * ⇑g, isLocallyConstant := ⋯ } }
-- Lean.Parser.Extension
/-- If the parsing stack is of the form `#[.., openDecl]`, we process the open declaration, and execute `p`  -/
Lean.Parser.withOpenDeclFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_one_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], ValuativeRel.ValueGroupWithZero.mk 1 1 = 1
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.algebraMapCoeffs_apply : ∀ {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (b : Module.Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)) (i : ι),
  (Module.Basis.algebraMapCoeffs A b h) i = b i
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearMap.mfderiv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E →L[𝕜] E') {x : E}, mfderiv% ⇑f x = f
-- Mathlib.Probability.Process.Adapted
/-- For filtrations indexed by a discrete order, `StronglyAdapted` and `IsStronglyProgressive` are
equivalent. This lemma provides `StronglyAdapted f u → IsStronglyProgressive f u`.
See `IsStronglyProgressive.stronglyAdapted` for the reverse direction, which is true more generally.
 -/
MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : TopologicalSpace ι] [DiscreteTopology ι]
  [SecondCountableTopology ι] [inst_5 : MeasurableSpace ι] [OpensMeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.IsStronglyProgressive f u
-- Mathlib.Order.Filter.IsBounded
OrderIso.isBoundedUnder_le_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {l : Filter γ} {u : γ → α},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => e (u x)) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
/-- The topological closure of the non-unital star subalgebra generated by a single element.  -/
NonUnitalStarAlgebra.elemental : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [IsScalarTower R A A] →
                [SMulCommClass R A A] →
                  [StarModule R A] →
                    [inst_8 : TopologicalSpace A] →
                      [IsSemitopologicalSemiring A] →
                        [ContinuousConstSMul R A] → [ContinuousStar A] → A → NonUnitalStarSubalgebra R A
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Left.nsmul_nonpos : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M}, a ≤ 0 → ∀ (n : ℕ), n • a ≤ 0
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_le : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] {M N P : Submodule R A}, M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univUnitBall_apply : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E),
  ↑OpenPartialHomeomorph.univUnitBall x = (√(1 + ‖x‖ ^ 2))⁻¹ • x
-- Init.Data.SInt.Lemmas
Int32.toISize_le : ∀ {a b : Int32}, a.toISize ≤ b.toISize ↔ a ≤ b
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
ModuleCat.MonoidalCategory.instBraidedSemimoduleCatFunctorEquivalenceSemimoduleCat : {R : Type u} → [inst : CommRing R] → ModuleCat.equivalenceSemimoduleCat.functor.Braided
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the constant sequence `1` and of the Möbius function are inverses.  -/
LSeries_one_mul_Lseries_moebius : ∀ {s : ℂ}, 1 < s.re → LSeries 1 s * LSeries (fun n => ↑(ArithmeticFunction.moebius n)) s = 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toListModel_alter! : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {t : Std.DTreeMap.Internal.Impl α fun x => β} {a : α} {f : Option β → Option β},
  t.Balanced →
    t.Ordered →
      (Std.DTreeMap.Internal.Impl.Const.alter! a f t).toListModel.Perm
        (Std.Internal.List.Const.alterKey a f t.toListModel)
-- Mathlib.Data.PFun
/-- Graph of a partial function as a relation. `x` and `y` are related iff `f x` is defined and
"equals" `y`.  -/
PFun.graph' : {α : Type u_1} → {β : Type u_2} → (α →. β) → SetRel α β
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.isoOfEq_inv_ι_assoc : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U = V) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.isoOfEq e).inv (CategoryTheory.CategoryStruct.comp U.ι h) =
    CategoryTheory.CategoryStruct.comp V.ι h
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_inv_left_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj B] (f g h : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv)
          g)
        CategoryTheory.MonObj.mul =
      h ↔
    g = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f h) CategoryTheory.MonObj.mul
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.HasColimit.reflectsColimit : ∀ {R : Type w} [inst : Ring R] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))],
  CategoryTheory.Limits.ReflectsColimit F (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_eq_some_getElem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α} (h : a ∈ t),
  t[a]? = some t[a]
-- Init.Data.Nat.Compare
Nat.compare_eq_ite_lt : ∀ (a b : ℕ), compare a b = if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq
-- Mathlib.Data.Real.Embedding
/-- For `u v : ℚ` and `x y : M`, one can informally write
`u < x → v < y → u + v < x + y`. We formalize this using smul.  -/
num_smul_one_lt_den_smul_add : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M] {u v : ℚ}
  {x y : M}, u.num • 1 < u.den • x → v.num • 1 < v.den • y → (u + v).num • 1 < (u + v).den • (x + y)
-- Init.Data.Int.Order
Int.natAbs_one : Int.natAbs 1 = 1
-- Aesop.Forward.Match.Types
Aesop.ForwardRuleMatch.mk.inj : ∀ {rule : Aesop.ForwardRule} {«match» : Aesop.CompleteMatch} {rule_1 : Aesop.ForwardRule}
  {match_1 : Aesop.CompleteMatch},
  { rule := rule, «match» := «match» } = { rule := rule_1, «match» := match_1 } → rule = rule_1 ∧ «match» = match_1
-- Mathlib.Data.List.Permutation
List.nodup_permutations_iff : ∀ {α : Type u_1} {s : List α}, s.permutations.Nodup ↔ s.Nodup
-- Mathlib.Testing.Plausible.Functions
Plausible.TotalFunction.zeroDefault.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Zero β] (A : List ((_ : α) × β)) (a : β),
  (Plausible.TotalFunction.withDefault A a).zeroDefault = Plausible.TotalFunction.withDefault A 0
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.one_or_eq_of_le_of_prime : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p m : Associates M}, Prime p → m ≤ p → m = 1 ∨ m = p
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.inhabited : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → Inhabited (NormedAddGroupHom V₁ V₂)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.liftOrderHom.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f : M → α)
  (h : ∀ (a b : M), MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b → f a ≤ f b),
  MulArchimedeanClass.liftOrderHom f h = { toFun := MulArchimedeanClass.lift f ⋯, monotone' := ⋯ }
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- A dense open set `U : Opens X` of a `S`-rational scheme `X` is `S`-rational.  -/
AlgebraicGeometry.Scheme.Opens.isRationalOver_of_dense : ∀ {X S : AlgebraicGeometry.Scheme} (U : X.Opens) (sX : X ⟶ S),
  Dense ↑U →
    ∀ [AlgebraicGeometry.Scheme.IsRationalOver sX],
      AlgebraicGeometry.Scheme.IsRationalOver (CategoryTheory.CategoryStruct.comp U.ι sX)
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.extend_unique : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  {f : α → β} [CompleteSpace β] [T0Space β],
  UniformContinuous f → ∀ {g : pkg.space → β}, UniformContinuous g → (∀ (a : α), f a = g (pkg.coe a)) → pkg.extend f = g
-- Mathlib.Order.Circular
Set.mem_cIcc : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b x : α}, x ∈ Set.cIcc a b ↔ btw a x b
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.add : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {f₁ f₂ : α → E} {g : α → F}
  {l : Filter α}, f₁ =O[𝕜; l] g → f₂ =O[𝕜; l] g → (f₁ + f₂) =O[𝕜; l] g
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.inter_of_left : ∀ {α : Type u} {s : Set α}, s.Finite → ∀ (t : Set α), (s ∩ t).Finite
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
RingOfIntegers.exponent_eq_one_iff : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K}, RingOfIntegers.exponent θ = 1 ↔ ℤ[θ] = ⊤