mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Cont.eval.match_1.eq_4 : ∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont)
  (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (fs : Turing.ToPartrec.Code) →
      (as : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ fs as k))
  (h_3 : (ns : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ ns k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp f k))
  (h_5 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix f k)),
  (match Turing.ToPartrec.Cont.comp f k with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ fs as k => h_2 fs as k
    | Turing.ToPartrec.Cont.cons₂ ns k => h_3 ns k
    | Turing.ToPartrec.Cont.comp f k => h_4 f k
    | Turing.ToPartrec.Cont.fix f k => h_5 f k) =
    h_4 f k
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModule.mk : String → Lean.Lsp.DocumentUri → Option Lean.Json → Lean.Lsp.LeanModule
-- Mathlib.Data.Analysis.Topology
Ctop.ofEquiv_val : ∀ {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ ≃ τ) (F : Ctop α σ) (a : τ),
  (Ctop.ofEquiv E F).f a = F.f (E.symm a)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.TheoremGuard.mk.inj : ∀ {e : Lean.Expr} {check : Bool} {e_1 : Lean.Expr} {check_1 : Bool},
  { e := e, check := check } = { e := e_1, check := check_1 } → e = e_1 ∧ check = check_1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.smul_integral_comp_mul_left : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c : ℝ),
  c • ∫ (x : ℝ) in a..b, f (c * x) = ∫ (x : ℝ) in c * a..c * b, f x
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite : ∀ (σ : Type u) (R : Type v) [inst : CommSemiring R] [Finite σ] (N : ℕ),
  Module.Finite R ↥(MvPolynomial.restrictTotalDegree σ R N)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, (t.insertManyIfNewUnit l).contains k = (t.contains k || l.contains k)
-- Lean.Data.Position
Lean.instReprPosition.repr : Lean.Position → ℕ → Std.Format
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integrableOn_comp_log_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) {a : ℝ},
  0 < a →
    (MeasureTheory.IntegrableOn (fun x => x⁻¹ • g (Real.log x)) (Set.Ioi a) MeasureTheory.volume ↔
      MeasureTheory.IntegrableOn g (Set.Ioi (Real.log a)) MeasureTheory.volume)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_rev_Iio : ∀ {n : ℕ} (i : Fin n), Fin.rev ⁻¹' Set.Iio i = Set.Ioi i.rev
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomAddAct.instVAddCommClassAEEqFun_2 : ∀ {M : Type u_3} {N : Type u_1} {α : Type u_2} {β : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : VAdd M α] [inst_3 : MeasurableConstVAdd M α]
  [inst_4 : MeasureTheory.VAddInvariantMeasure M α μ] [inst_5 : VAdd N α] [inst_6 : MeasurableConstVAdd N α]
  [inst_7 : MeasureTheory.VAddInvariantMeasure N α μ] [VAddCommClass M N α], VAddCommClass Mᵈᵃᵃ Nᵈᵃᵃ (α →ₘ[μ] β)
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.mk.sizeOf_spec : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L] [inst_3 : SizeOf A]
  [inst_4 : SizeOf L] (toSubmodule : Submodule A L)
  (lie_mem' : ∀ {a b : L}, a ∈ toSubmodule.carrier → b ∈ toSubmodule.carrier → ⁅a, b⁆ ∈ toSubmodule.carrier),
  sizeOf { toSubmodule := toSubmodule, lie_mem' := lie_mem' } = 1 + sizeOf toSubmodule
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.mk.inj : ∀ {R : Type u_7} {S : Type u_8} {inst : Mul R} {inst_1 : Mul S} {inst_2 : Add R} {inst_3 : Add S} {toEquiv : R ≃ S}
  {map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y}
  {map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y} {toEquiv_1 : R ≃ S}
  {map_mul'_1 : ∀ (x y : R), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y}
  {map_add'_1 : ∀ (x y : R), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y},
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' } =
      { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 } →
    toEquiv = toEquiv_1
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.Hom.comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (self : D₁.Hom D₂) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄
  (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
  (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
  CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (self.hom i₁)) (D₂.hom q f₁ f₂ ⋯ ⋯) =
    CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (self.hom i₂))
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_above_dvd`. -/
Ideal.ramificationIdx'_above_dvd : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q] [Module.Flat S T], r.ramificationIdx S ∣ r.ramificationIdx R
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `G` be a nonarchimedean multiplicative abelian group, and let `f : α → G` be a function that
tends to one on the filter of cofinite sets. For each finite subset of `α`, consider the partial
product of `f` on that subset. These partial products form a Cauchy filter.  -/
NonarchimedeanGroup.cauchySeq_prod_of_tendsto_cofinite_one : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : UniformSpace G] [IsUniformGroup G]
  [NonarchimedeanGroup G] {f : α → G}, Filter.Tendsto f Filter.cofinite (nhds 1) → CauchySeq fun s => ∏ i ∈ s, f i
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.instTopOfCompactSpaceOfNonempty : {α : Type u_1} →
  [inst : TopologicalSpace α] → [CompactSpace α] → [Nonempty α] → Top (TopologicalSpace.PositiveCompacts α)
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `S ∪ T`, then `B`
is a cyclotomic extension of `adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1 }` given by
roots of unity of order in `T`.  -/
IsCyclotomicExtension.union_right : ∀ (S T : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [h : IsCyclotomicExtension (S ∪ T) A B],
  IsCyclotomicExtension T (↥(Algebra.adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B
-- Mathlib.Data.List.Basic
Function.Injective.list_map : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective f → Function.Injective (List.map f)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- The Bochner integral in L1 space as a continuous linear map.  -/
MeasureTheory.L1.integralCLM' : {α : Type u_1} →
  {E : Type u_2} →
    (𝕜 : Type u_4) →
      [inst : NormedAddCommGroup E] →
        {m : MeasurableSpace α} →
          {μ : MeasureTheory.Measure α} →
            [inst_1 : NormedSpace ℝ E] →
              [inst_2 : NormedRing 𝕜] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : IsBoundedSMul 𝕜 E] →
                    [SMulCommClass ℝ 𝕜 E] → [CompleteSpace E] → ↥(MeasureTheory.Lp E 1 μ) →L[𝕜] E
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.FunPropDecl.mk : Lean.Name → Array Lean.Meta.DiscrTree.Key → ℕ → Mathlib.Meta.FunProp.FunPropDecl
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : Inhabited α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∪ m₂).getKey! k = m₁.getKey! k
-- Std.Data.Internal.List.Associative
Std.Internal.List.distinctKeys_interSmallerFn : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] (l sofar : List ((a : α) × β a)) (k : α),
  Std.Internal.List.DistinctKeys sofar → Std.Internal.List.DistinctKeys (Std.Internal.List.interSmallerFn l sofar k)
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
/-- When considering functions between manifolds, this statement shows up often. It entails
the unique differential of the pullback in extended charts of the set where the function can
be read in the charts.  -/
UniqueMDiffOn.uniqueDiffOn_inter_preimage : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M'' : Type u_8} [inst_9 : TopologicalSpace M''] [inst_10 : ChartedSpace H' M''] {s : Set M} [IsManifold I 1 M],
  UniqueMDiff[s] →
    ∀ (x : M) (y : M'') {f : M → M''},
      ContinuousOn f s →
        UniqueDiffOn 𝕜 ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableAt.sub_iff_right` -/
DifferentiableAt.fun_sub_iff_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → (DifferentiableAt 𝕜 (fun i => f i - g i) x ↔ DifferentiableAt 𝕜 g x)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.restrictVarLeft.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] {γ : Type u_2} (a : α)
  (f : ↥(FirstOrder.Language.var (Sum.inl a)).varFinsetLeft → β),
  (FirstOrder.Language.var (Sum.inl a)).restrictVarLeft f = FirstOrder.Language.var (Sum.inl (f ⟨a, ⋯⟩))
-- Mathlib.Geometry.Euclidean.SignedDist
AffineSubspace.signedInfDist_apply_of_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
  [inst_5 : s.direction.HasOrthogonalProjection] (p : P) {x : P}, x ∈ s → (s.signedInfDist p) x = 0
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.mk.sizeOf_spec : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C)
  (unit_eq : CategoryTheory.Functor.id C = functor.comp inverse)
  (counit_eq : inverse.comp functor = CategoryTheory.Functor.id D),
  sizeOf { functor := functor, inverse := inverse, unit_eq := unit_eq, counit_eq := counit_eq } =
    1 + sizeOf functor + sizeOf inverse + sizeOf unit_eq + sizeOf counit_eq
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.dual_rank_eq : ∀ {K : Type uK} {V : Type uV} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V] [Module.Free K V]
  [Module.Finite K V], Module.rank K (Module.Dual K V) = Cardinal.lift.{uK, uV} (Module.rank K V)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_eq_false_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = true → t.isEmpty = false
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instSMulCommClass_1 : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α], SMulCommClass (CentroidHom α) α α
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Relations.boundedFormula₂.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (r : L.Relations 2) (t₁ t₂ : L.Term (α ⊕ Fin n)),
  r.boundedFormula₂ t₁ t₂ = r.boundedFormula ![t₁, t₂]
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.op_map : ∀ (X : SSet) {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) (x : X.op.obj n),
  (CategoryTheory.ConcreteCategory.hom (X.op.map f)) x =
    SSet.opObjEquiv.symm
      ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.rev.map f.unop).op)) (SSet.opObjEquiv x))
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.zero_iff_nonpos : ∀ {x : ℝ}, x.smoothTransition = 0 ↔ x ≤ 0
-- Mathlib.Algebra.Ring.Int.Parity
Int.odd_coe_nat : ∀ (n : ℕ), Odd ↑n ↔ Odd n
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.mk.inj : ∀ {J : CategoryTheory.Limits.MulticospanShape} {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {left : J.L → C}
  {right : J.R → C} {fst : (b : J.R) → left (J.fst b) ⟶ right b} {snd : (b : J.R) → left (J.snd b) ⟶ right b}
  {left_1 : J.L → C} {right_1 : J.R → C} {fst_1 : (b : J.R) → left_1 (J.fst b) ⟶ right_1 b}
  {snd_1 : (b : J.R) → left_1 (J.snd b) ⟶ right_1 b},
  { left := left, right := right, fst := fst, snd := snd } =
      { left := left_1, right := right_1, fst := fst_1, snd := snd_1 } →
    left = left_1 ∧ right = right_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendHom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cocone F) {X : C} (f : s.pt ⟶ X), (s.extendHom f).hom = f
-- Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
/-- The standard short complex `0 → N → P → M → 0` with `P= R^{⊕M}` free.  -/
ModuleCat.projectiveShortComplex : {R : Type u} → [inst : Ring R] → [Small.{v, u} R] → ModuleCat R → CategoryTheory.ShortComplex (ModuleCat R)
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
/-- The bijection `Subtype P.op ≃ Subtype P` for `P : ObjectProperty C`.  -/
CategoryTheory.ObjectProperty.subtypeOpEquiv : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] → (P : CategoryTheory.ObjectProperty C) → Subtype P.op ≃ Subtype P
-- Init.Data.Int.Order
Int.instCommutativeMin : Std.Commutative min
-- Mathlib.Data.Set.Lattice
Set.inter_empty_of_inter_sUnion_empty : ∀ {α : Type u_1} {s t : Set α} {S : Set (Set α)}, t ∈ S → s ∩ ⋃₀ S = ∅ → s ∩ t = ∅
-- Init.Data.SInt.Basic
instDivInt16 : Div Int16
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isAddRegular_unop`. -/
IsAddRegular.unop : ∀ {R : Type u_1} [inst : Add R] {a : Rᵃᵒᵖ}, IsAddRegular a → IsAddRegular (AddOpposite.unop a)
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.verschiebungFun.eq_1 : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R),
  x.verschiebungFun = { coeff := fun n => if n = 0 then 0 else x.coeff (n - 1) }
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- Together `Matrix.invertibleTranspose` and `Matrix.invertibleOfInvertibleTranspose` form an
equivalence, although both sides of the equiv are subsingleton anyway.  -/
Matrix.transposeInvertibleEquivInvertible : {n : Type u_2} →
  {α : Type u_3} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommSemiring α] → (A : Matrix n n α) → Invertible A.transpose ≃ Invertible A
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.card_map_of_injective : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_3} [inst_1 : AddGroup H] {K : AddSubgroup G} {f : G →+ H},
  Function.Injective ⇑f → Nat.card ↥(AddSubgroup.map f K) = Nat.card ↥K
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.Embedding.submatrix_adjMatrix : ∀ (α : Type u_1) {V : Type u_2} {W : Type u_3} {G : SimpleGraph V} [inst : DecidableRel G.Adj] [inst_1 : Zero α]
  [inst_2 : One α] {H : SimpleGraph W} [inst_3 : DecidableRel H.Adj] (f : G ↪g H),
  (SimpleGraph.adjMatrix α H).submatrix ⇑f ⇑f = SimpleGraph.adjMatrix α G
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.centralizer_univ : ∀ (M : Type u_1) [inst : Monoid M], Submonoid.centralizer Set.univ = Submonoid.center M
-- Mathlib.Order.Lattice
Pi.instMaxForall_mathlib : {ι : Type u_1} → {α' : ι → Type u_2} → [(i : ι) → Max (α' i)] → Max ((i : ι) → α' i)
-- Std.Data.TreeMap.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
proof obligation in the statement of `get_insertIfNew`.  -/
Std.TreeMap.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α} {v : β},
  a ∈ t.insertIfNew k v → ¬(cmp k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Mathlib.Algebra.Order.Module.Pointwise
bddBelow_smul_iff_of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : GroupWithZero α] [inst_3 : Zero β]
  [inst_4 : MulActionWithZero α β] [PosSMulMono α β] [PosSMulReflectLE α β] {s : Set β} {a : α},
  0 < a → (BddBelow (a • s) ↔ BddBelow s)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.instEpiSimplexCategoryE : ∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ), CategoryTheory.Epi A.e
-- Init.Data.List.Sublist
List.isInfixOf_internal.eq_def : ∀ {α : Type u} [inst : BEq α] (l₁ l₂ : List α),
  l₁.isInfixOf_internal l₂ =
    (l₁.isPrefixOf l₂ ||
      match l₂ with
      | [] => false
      | head :: l₂ => l₁.isInfixOf_internal l₂)
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
/-- A 2-square is Guitart exact iff it is so after replacing the left and right functors by
isomorphic functors.  -/
CategoryTheory.TwoSquare.GuitartExact.whiskerVertical_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] {T : CategoryTheory.Functor C₁ D₁} {L : CategoryTheory.Functor C₁ C₂}
  {R : CategoryTheory.Functor D₁ D₂} {B : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T L R B)
  {L' : CategoryTheory.Functor C₁ C₂} {R' : CategoryTheory.Functor D₁ D₂} (α : L ≅ L') (β : R ≅ R'),
  (w.whiskerVertical α.hom β.inv).GuitartExact ↔ w.GuitartExact
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.eq_1 : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] (l : Filter α) (f : α → E) (g : α → F),
  f =Θ[l] g = (f =O[l] g ∧ g =O[l] f)
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
AffineSubspace.nonempty_map : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {E : AffineSubspace k P₁} [Ene : Nonempty ↥E] {φ : P₁ →ᵃ[k] P₂},
  Nonempty ↥(AffineSubspace.map φ E)
-- Mathlib.Data.Finset.NAry
Finset.card_le_card_image₂_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} (t : Finset β) {a : α}
  {s : Finset α}, a ∈ s → Function.Injective (f a) → t.card ≤ (Finset.image₂ f s t).card
-- Std.Http.Server.Handler
/-- A type class for handling HTTP server requests. Implement this class to define how the server
responds to incoming requests, failures, and `Expect: 100-continue` headers.
 -/
Std.Http.Server.Handler : Type → Type 1
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.of_ofLinearEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsAdicComplete I M] (x : AdicCompletion I M),
  (AdicCompletion.of I M) ((AdicCompletion.ofLinearEquiv I M).symm x) = x
-- Mathlib.Topology.Separation.Basic
/-- A point `x` in a discrete subset `s` of a topological space admits a neighbourhood
that only meets `s` at `x`.  -/
nhds_inter_eq_singleton_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s → ∀ {x : X}, x ∈ s → ∃ U ∈ nhds x, U ∩ s = {x}
-- Batteries.Data.AssocList
Batteries.AssocList.beq.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst_1 : BEq β],
  Batteries.AssocList.nil.beq Batteries.AssocList.nil = true
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstLTNat : Lean.Expr → Lean.MetaM Bool
-- Std.Time.Date.Unit.Day
/-- Convert `Day.Offset` into `Nanosecond.Offset`.
 -/
Std.Time.Day.Offset.toNanoseconds : Std.Time.Day.Offset → Std.Time.Nanosecond.Offset
-- Std.Data.String.ToNat
String.Slice.isSome_toNat? : ∀ {s : String.Slice}, s.toNat?.isSome = s.isNat
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.toFractionRingAlgEquiv_apply : ∀ (K : Type u) [inst : CommRing K] [inst_1 : IsDomain K] (R : Type u_1) [inst_2 : CommSemiring R]
  [inst_3 : Algebra R (Polynomial K)] (self : RatFunc K),
  (RatFunc.toFractionRingAlgEquiv K R) self = self.toFractionRing
-- Mathlib.CategoryTheory.Category.PartialFun
Equiv.optionSubtypeNe.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α),
  Equiv.optionSubtypeNe a = ↑((Equiv.optionSubtype a).symm (Equiv.refl { y // y ≠ a }))
-- Mathlib.Lean.Expr.Basic
/-- Update `ConstantVal` (the data common to all constructors of `ConstantInfo`)
in a `ConstantInfo`.  -/
Lean.ConstantInfo.updateConstantVal : Lean.ConstantInfo → Lean.ConstantVal → Lean.ConstantInfo
-- Mathlib.Data.Nat.WithBot
Nat.WithBot.one_le_iff_zero_lt : ∀ {x : WithBot ℕ}, 1 ≤ x ↔ 0 < x
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.StructuredArrow.functor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (T : CategoryTheory.Functor C D) (d : Dᵒᵖ),
  (CategoryTheory.StructuredArrow.functor T).obj d =
    CategoryTheory.Cat.of (CategoryTheory.StructuredArrow (Opposite.unop d) T)
-- Init.Data.Array.Basic
Array.instFunctor : Functor Array
-- Std.Async.TCP
_private.Std.Async.TCP.0.Std.Async.TCP.Socket.Client.ofNative : Std.Internal.UV.TCP.Socket → Std.Async.TCP.Socket.Client
-- Mathlib.RingTheory.Jacobson.Ring
/-- The constant coefficient as an R-linear morphism  -/
_private.Mathlib.RingTheory.Jacobson.Ring.0.MvPolynomial.Cₐ : (R : Type u) →
  (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → S →ₐ[R] Polynomial S
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyRel.symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {f g : X ⟶ Y},
  HomotopicalAlgebra.LeftHomotopyRel f g → HomotopicalAlgebra.LeftHomotopyRel g f
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.instSubsingletonHomToSSetBot : ∀ {X Y : SSet}, Subsingleton (⊥.toSSet ⟶ Y)
-- Mathlib.Order.Filter.CardinalInter
Filter.cardinal_bInter_mem : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι},
  Cardinal.mk ↑S < c →
    ∀ {s : (i : ι) → i ∈ S → Set α}, ⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_transpose_iff : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, A.transpose.IsHermitian ↔ A.IsHermitian