mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.Liouville
/-- **Cauchy's estimate for the first order derivative**: If `f` is complex differentiable on an
open disc of radius `R > 0`, is continuous on its closure, and its values on the boundary circle
of this disc are bounded from above by `C`, then the norm of its derivative at the center is at
most `C / R`. Note that this theorem does not require the completeness of the codomain of `f`. In
contrast, the completeness is needed for `norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le`.  -/
Complex.norm_deriv_le_of_forall_mem_sphere_norm_le : ∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] {c : ℂ} {R C : ℝ} {f : ℂ → F},
  0 < R → DiffContOnCl ℂ f (Metric.ball c R) → (∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) → ‖deriv f c‖ ≤ C / R
-- Mathlib.Order.Defs.Unbundled
rel_congr : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] [IsTrans α r] {a b c d : α}, r a b → r c d → (r a c ↔ r b d)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The identity homomorphism for an Eilenberg–Moore algebra.  -/
CategoryTheory.Monad.Algebra.Hom.id : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {T : CategoryTheory.Monad C} → (A : T.Algebra) → A.Hom A
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.centralizer_toSubmonoid : ∀ {R : Type u_1} [inst : Semiring R] (s : Set R), (Subsemiring.centralizer s).toSubmonoid = Submonoid.centralizer s
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.refl_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁],
  (ContinuousAffineEquiv.refl k P₁).symm = ContinuousAffineEquiv.refl k P₁
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_inter_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂
-- Mathlib.Analysis.Normed.Module.Dual
NormedSpace.eq_zero_iff_forall_dual_eq_zero : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (x : E),
  x = 0 ↔ ∀ (g : StrongDual 𝕜 E), g x = 0
-- Mathlib.Order.RelClasses
/-- A version of `right_iff_left_not_left` with explicit `r` and `s`.  -/
right_iff_left_not_left_of : ∀ {α : Type u} (r s : α → α → Prop) [IsNonstrictStrictOrder α r s] {a b : α}, s a b ↔ r a b ∧ ¬r b a
-- Mathlib.Tactic.LinearCombination.Lemmas
/-- Given an (in)equality, look up the lemma to move everything to the LHS.  -/
Mathlib.Ineq.rearrangeData : Mathlib.Ineq → Lean.Name
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.ncard_block_eq_relIndex : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] {B : Set X},
  MulAction.IsBlock G B → ∀ {x : X}, x ∈ B → B.ncard = (MulAction.stabilizer G x).relIndex (MulAction.stabilizer G B)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmodMulEquivOfGenerator_symm_apply_generator : ∀ {G : Type u_2} [inst : Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n),
  (zmodMulEquivOfGenerator hg hn).symm g = Multiplicative.ofAdd 1
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_inv_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.op =
    (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).hom
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.exists_revMatchesAt_iff_eq_append : ∀ {pat s : String.Slice},
  (∃ pos, String.Slice.Pattern.Model.RevMatchesAt pat pos) ↔ ∃ t₁ t₂, s.copy = t₁ ++ pat.copy ++ t₂
-- Mathlib.Algebra.Order.Chebyshev
/-- **Chebyshev's Sum Inequality**: When `f` and `g` monovary together (e.g. they are both
monotone/antitone), the scalar product of their sum is less than the size of the set times their
scalar product.  -/
MonovaryOn.sum_smul_sum_le_card_smul_sum : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {s : Finset ι} {f : ι → α} {g : ι → β},
  MonovaryOn f g ↑s → (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ s.card • ∑ i ∈ s, f i • g i
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of the forward direction of `Asymptotics.isBigOTVS_iff_smallSets`. -/
Asymptotics.IsBigOTVS.eventually_smallSets : ∀ {α : 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] {l : Filter α} {f : α → E} {g : α → F},
  f =O[𝕜; l] g →
    ∀ U ∈ nhds 0, ∀ᶠ (V : Set F) in (nhds 0).smallSets, ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)
-- Init.Data.Slice.Array.Lemmas
Array.start_mkSlice_ric : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ}, (Std.Ric.Sliceable.mkSlice xs *...=hi).start = 0
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
QuasispectrumRestricts.apply_mem : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] {a : A} {f : S → R} [IsScalarTower S A A]
  [SMulCommClass S A A] [IsScalarTower R S A],
  QuasispectrumRestricts a f → ∀ {s : S}, s ∈ quasispectrum S a → f s ∈ quasispectrum R a
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_finsetSum : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  {ι : Type u_8} {s : Finset ι} {f : ι → ℝ → E},
  (∀ i ∈ s, IntervalIntegrable (f i) μ a b) →
    ∫ (x : ℝ) in a..b, ∑ i ∈ s, f i x ∂μ = ∑ i ∈ s, ∫ (x : ℝ) in a..b, f i x ∂μ
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.embedding : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R},
  OrthogonalIdempotents e → ∀ {J : Type u_4} (i : J ↪ I), OrthogonalIdempotents (e ∘ ⇑i)
-- Mathlib.Algebra.Ring.Regular
isRegular_iff_ne_zero' : ∀ {α : Type u_1} [Nontrivial α] [inst : NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α}, IsRegular k ↔ k ≠ 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
/-- The sheafification of presheaves of modules commutes with the functor which
forgets the module structures.  -/
PresheafOfModules.sheafificationCompToSheaf : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α] →
                [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] →
                  [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
                    (PresheafOfModules.sheafification α).comp (SheafOfModules.toSheaf R) ≅
                      (PresheafOfModules.toPresheaf R₀).comp (CategoryTheory.presheafToSheaf J AddCommGrpCat)
-- Init.Data.List.Nat.Erase
List.eraseIdx_set_gt : ∀ {α : Type u_1} {l : List α} {i j : ℕ} {a : α}, i < j → (l.set i a).eraseIdx j = (l.eraseIdx j).set i a
-- Mathlib.Tactic.Translate.Core
/-- If `src` was declared with `alias`, then record `tgt` as an alias,
and give it an alias-style docstring if it doesn't have a doc-string already  -/
Mathlib.Tactic.Translate.copyAliasAttribute : Mathlib.Tactic.Translate.TranslateData → Lean.Name → Lean.Name → Lean.CoreM Unit
-- Mathlib.LinearAlgebra.SesquilinearForm.Star
star_dotProduct_toMatrix₂_mulVec : ∀ {R : Type u_1} {M : Type u_2} {n : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Fintype n] [inst_5 : DecidableEq n] {B : M →ₗ⋆[R] M →ₗ[R] R} (b : Module.Basis n R M)
  (x y : n → R), star x ⬝ᵥ ((LinearMap.toMatrix₂ b b) B).mulVec y = (B (b.equivFun.symm x)) (b.equivFun.symm y)
-- Mathlib.NumberTheory.FLT.Three
/-- If `a b c : ℤ` are such that `¬ 3 ∣ a * b * c`, then `a ^ 3 + b ^ 3 ≠ c ^ 3`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.fermatLastTheoremThree_case_1 : ∀ {a b c : ℤ}, ¬3 ∣ a * b * c → a ^ 3 + b ^ 3 ≠ c ^ 3
-- Mathlib.Order.Hom.WithTopBot
/-- Any `OrderBot` is equivalent to `WithBot` of the subtype excluding `⊥`.

See also `Equiv.optionSubtypeNe`.  -/
WithBot.subtypeOrderIso : {α : Type u_1} →
  [inst : PartialOrder α] → [inst_1 : OrderBot α] → [DecidablePred fun x => x = ⊥] → WithBot { a // a ≠ ⊥ } ≃o α
-- Std.Async.Select
_private.Std.Async.Select.0.Std.Async.shuffleIt.go.match_1.eq_1 : ∀ (motive : ℕ × StdGen → Sort u_1) (j : ℕ) (gen : StdGen) (h_1 : (j : ℕ) → (gen : StdGen) → motive (j, gen)),
  (match (j, gen) with
    | (j, gen) => h_1 j gen) =
    h_1 j gen
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l →
          ∀ {h : k' ∈ Std.ExtDHashMap.Const.ofList l},
            Std.ExtDHashMap.Const.get (Std.ExtDHashMap.Const.ofList l) k' h = v
-- Mathlib.Data.Fin.Tuple.Basic
/-- A finite sequence of properties `P` holds for `{0, ..., m + n - 1}` iff
it holds separately for both `{0, ..., m - 1}` and `{m, ..., m + n - 1}`.  -/
Fin.forall_fin_add : ∀ {m n : ℕ} (P : Fin (m + n) → Prop),
  (∀ (i : Fin (m + n)), P i) ↔ (∀ (i : Fin m), P (Fin.castAdd n i)) ∧ ∀ (j : Fin n), P (Fin.natAdd m j)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get? k = m₁.get? k
-- Mathlib.CategoryTheory.Opposites
/-- The opposite isomorphism.
 -/
CategoryTheory.Iso.op : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ≅ Y) → (Opposite.op Y ≅ Opposite.op X)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
/-- The indexed infimum of two functions are comparable if the functions are pointwise
comparable  -/
Directed.ciInf_mono : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] {f g : ι → α},
  Directed (fun x1 x2 => x2 ≤ x1) f →
    Directed (fun x1 x2 => x2 ≤ x1) g → BddBelow (Set.range g) → (∀ (x : ι), g x ≤ f x) → iInf g ≤ iInf f
-- Mathlib.Algebra.Order.Module.Defs
posSMulStrictMono_iff_PosSMulReflectLE : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β] [inst_3 : Zero α],
  PosSMulStrictMono α β ↔ PosSMulReflectLE α β
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddGroup.toNorm : {E : Type u_8} → [self : NormedAddGroup E] → Norm E
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.of_isMaximal_nilradical : ∀ (R : Type u_1) [inst : CommSemiring R] [(nilradical R).IsMaximal], Ring.KrullDimLE 0 R
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_zero : Real.cosh 0 = 1
-- Mathlib.Topology.FiberBundle.Basic
/-- The projection from a fiber bundle to its base is an open map.  -/
FiberBundle.isOpenMap_proj : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E],
  IsOpenMap Bundle.TotalSpace.proj
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.pullback_apply : ∀ {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : TopologicalSpace F] [inst_3 : TopologicalSpace B]
  [inst_4 : ∀ (_b : B), Nonempty (E _b)] {K : Type U} [inst_5 : FunLike K B' B] [inst_6 : ContinuousMapClass K B' B]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (f : K) (z : Bundle.TotalSpace F (⇑f *ᵖ E)),
  ↑(e.pullback f) z = (z.proj, (↑e (Bundle.Pullback.lift (⇑f) z)).2)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_neg : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (f : α → F'),
  MeasureTheory.condExpL1 hm μ (-f) = -MeasureTheory.condExpL1 hm μ f
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
withSeminorms_pi : ∀ {𝕜 : Type u_2} {ι : Type u_9} [inst : NormedField 𝕜] {κ : ι → Type u_11} {E : ι → Type u_12}
  [inst_1 : (i : ι) → AddCommGroup (E i)] [inst_2 : (i : ι) → Module 𝕜 (E i)]
  [inst_3 : (i : ι) → TopologicalSpace (E i)] {p : (i : ι) → SeminormFamily 𝕜 (E i) (κ i)},
  (∀ (i : ι), WithSeminorms (p i)) → WithSeminorms (SeminormFamily.sigma fun i => (p i).comp (LinearMap.proj i))
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.quotToQuotUlift_ι : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] (j : J) (x : ↑(F.obj j)),
  (AddCommGrpCat.Colimits.quotToQuotUlift F) ((AddCommGrpCat.Colimits.Quot.ι F j) x) =
    (AddCommGrpCat.Colimits.Quot.ι (F.comp AddCommGrpCat.uliftFunctor) j) { down := x }
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentPositionParams.position : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.Position
-- Batteries.Data.String.Lemmas
/-- The stop position of a substring is at least the start.  -/
Substring.Raw.Valid.le : ∀ {s : Substring.Raw}, s.Valid → s.startPos ≤ s.stopPos
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instIsZeroApply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N], IsZeroApply (QuadraticMap R M N) M N
-- Mathlib.Algebra.Order.Group.Basic
zsmul_mono_right : ∀ (α : Type u_1) [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ},
  0 ≤ n → Monotone fun x => n • x
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_inverse_map_hom_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)}
  {t₁ t₂ : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)} {f : t₁ ⟶ t₂},
  (CategoryTheory.WithInitial.coconeEquiv.inverse.map f).hom.right = f.hom
-- Init.Data.Slice.Notation
Std.Roi.Sliceable.mk : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → (α → Std.Roi β → γ) → Std.Roi.Sliceable α β γ
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.edist_toL1_toL1 : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f g : α → β) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ),
  edist (MeasureTheory.Integrable.toL1 f hf) (MeasureTheory.Integrable.toL1 g hg) = ∫⁻ (a : α), edist (f a) (g a) ∂μ
-- Mathlib.Algebra.Star.Prod
Prod.instInvolutiveStar : {R : Type u} → {S : Type v} → [InvolutiveStar R] → [InvolutiveStar S] → InvolutiveStar (R × S)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_union_add_mk_inter : ∀ {α : Type u} {S T : Set α}, Cardinal.mk ↑(S ∪ T) + Cardinal.mk ↑(S ∩ T) = Cardinal.mk ↑S + Cardinal.mk ↑T
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
map_finsuppSum : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Zero M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] {H : Type u_16} [inst_3 : FunLike H N P] [AddMonoidHomClass H N P] (h : H) (f : α →₀ M)
  (g : α → M → N), h (f.sum g) = f.sum fun a b => h (g a b)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_zero : ∀ {α : Type u_2} [inst : Zero α], {0} = 0
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- If `s` is a non-empty open subset of `M`, every chart of `s` is the restriction
of some chart on `M`.  -/
TopologicalSpace.Opens.chart_eq : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {s : TopologicalSpace.Opens M} (hs : Nonempty ↥s) {e : OpenPartialHomeomorph (↥s) H},
  e ∈ atlas H ↥s → ∃ x, e = (chartAt H ↑x).subtypeRestr hs
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.IsSupClosedCompact.wellFoundedGT : ∀ (α : Type u_2) [inst : CompleteLattice α], CompleteLattice.IsSupClosedCompact α → WellFoundedGT α
-- Mathlib.Topology.EMetricSpace.Defs
PseudoEMetricSpace.edist_triangle : ∀ {α : Type u} [self : PseudoEMetricSpace α] (x y z : α), edist x z ≤ edist x y + edist y z
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of an additive Haar measure under a continuous surjective proper additive group
homomorphism is again an additive Haar measure. See also `AddEquiv.isAddHaarMeasure_map`,
`ContinuousAddEquiv.isAddHaarMeasure_map` and `ContinuousLinearEquiv.isAddHaarMeasure_map`.  -/
MeasureTheory.Measure.isAddHaarMeasure_map : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [ContinuousAdd G] {H : Type u_3}
  [inst_6 : AddGroup H] [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H] [BorelSpace H]
  [IsTopologicalAddGroup H] (f : G →+ H),
  Continuous ⇑f →
    Function.Surjective ⇑f →
      Filter.Tendsto (⇑f) (Filter.cocompact G) (Filter.cocompact H) →
        (MeasureTheory.Measure.map (⇑f) μ).IsAddHaarMeasure
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.find?_toList_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {v : β k},
  List.find? (fun x => cmp x.fst k == Ordering.eq) t.toList = some ⟨k, v⟩ ↔ t.get? k = some v
-- Mathlib.Tactic.NormNum.Eq
Mathlib.Meta.NormNum.Rat.invOf_denom_swap : ∀ {α : Type u_1} [inst : Ring α] (n₁ n₂ : ℤ) (a₁ a₂ : α) [inst_1 : Invertible a₁] [inst_2 : Invertible a₂],
  ↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁
-- Mathlib.Order.Disjoint
Complementeds.coe_lt_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {a b : Complementeds α}, ↑a < ↑b ↔ a < b
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.instIsScalarTower : ∀ {R : Type u_1} [inst : CommRing R] (R₁ : Type u_6) (R₂ : Type u_7) [inst_1 : SMul R₁ R₂] [inst_2 : DistribSMul R₁ R]
  [inst_3 : DistribSMul R₂ R] [inst_4 : IsScalarTower R₁ R R] [inst_5 : IsScalarTower R₂ R R] [IsScalarTower R₁ R₂ R]
  (f : Polynomial R), IsScalarTower R₁ R₂ (AdjoinRoot f)
-- Lean.DocString.Markdown
/-- Runs an element renderer with a fresh `mdRendererHeartbeats` budget.

The budget applies to each renderer separately.
 -/
Lean.Doc.withMdRendererBudget : {α : Type} → Lean.Doc.MarkdownM α → Lean.Doc.MarkdownM α
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The natural isomorphism arising from `mapForget_eq`.  -/
CategoryTheory.Under.mapForget : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X Y : T} →
      (f : X ⟶ Y) → (CategoryTheory.Under.map f).comp (CategoryTheory.Under.forget X) ≅ CategoryTheory.Under.forget Y
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
tangentMapWithin_prodFst : ∀ {𝕜 : 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_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set (M × M')}
  {p : TangentBundle (I.prod I') (M × M')},
  UniqueMDiffAt[s] p.proj → tangentMapWithin (I.prod I') I Prod.fst s p = ⟨p.proj.1, p.snd.1⟩
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleIndirectSuccessorOf.trans : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it'' it' it : Std.Iter β},
  it''.IsPlausibleIndirectSuccessorOf it' →
    it'.IsPlausibleIndirectSuccessorOf it → it''.IsPlausibleIndirectSuccessorOf it
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] {f g : α →+o β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.Order.Fin.Basic
/-- The inclusion map `Fin n → ℕ` is an order embedding.  -/
Fin.valOrderEmb : (n : ℕ) → Fin n ↪o ℕ
-- Init.Internal.Order.MonadTail
/-- A *tail monad* is a monad whose bind operation preserves a chosen ordering of the continuation.
Specifically, `MonadTail m` asserts that every `m β` carries a chain-complete partial order (CCPO)
and that `>>=` is monotone in its second (continuation) argument with respect to that order.

This is a weaker requirement than `MonoBind`, which requires monotonicity in both arguments.
`MonadTail` is sufficient for `partial_fixpoint`-like recursive definitions where the
recursive call only appears in the continuation (second argument) of `>>=`.
 -/
Lean.Order.MonadTail : (m : Type u → Type v) → [Bind m] → Type (max (u + 1) v)
-- Lean.DocString.DeferredCheck
/-- The options in effect at the reference site.  -/
Lean.Doc.DeferredCheck.options : Lean.Doc.DeferredCheck → Lean.Options
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
FundamentalGroup.one_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, 1 = Path.Homotopic.Quotient.refl x
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_sup_of_normal_right : ∀ {G : Type u_1} [inst : AddGroup G] {s t : AddSubgroup G} [ht : t.Normal] {x : G},
  x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_inter_support : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (s : Set α),
  ∑ᶠ (i : α) (_ : i ∈ s ∩ Function.support f), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- Delta-generated spaces are locally path-connected.  -/
DeltaGeneratedSpace.instLocallyPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [DeltaGeneratedSpace X], LocallyPathConnectedSpace X
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Interpreting the legs of a cocone as a costructured arrow and then forgetting the arrow again
does nothing.  -/
CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) →
            c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.proj F c.pt) ≅ CategoryTheory.Functor.id J
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.instIsClosedUnderIsomorphismsFunctorLeftExactFunctor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.leftExactFunctor C D).IsClosedUnderIsomorphisms
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isZero₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.Limits.IsZero T.obj₁ → CategoryTheory.Limits.IsZero T.obj₂ → CategoryTheory.Limits.IsZero T.obj₃