mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The norm of the image after the embedding associated to `v` is equal to the `v`-adic absolute
value.  -/
NumberField.FinitePlace.norm_embedding : ∀ {K : Type u_1} [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x : K),
  ‖(NumberField.FinitePlace.embedding v) x‖ = (NumberField.HeightOneSpectrum.adicAbv K v) x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_inter_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.Analysis.Normed.Module.FiniteDimension
exists_seq_norm_le_one_le_norm_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜],
  ¬FiniteDimensional 𝕜 E → ∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst.sizeOf_spec : ∀ (x : Lean.Grind.Linarith.Var) (c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr)
  (c₂ : Lean.Meta.Grind.Arith.Linear.IneqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst x c₁ c₂) = 1 + sizeOf x + sizeOf c₁ + sizeOf c₂
-- Mathlib.Control.Monad.Cont
ContT.run_seq : ∀ {r : Type u} {m : Type u → Type v} {α β : Type w} (f : ContT r m (α → β)) (x : ContT r m α) (k : β → m r),
  (f <*> x).run k = f.run fun f => x.run (k ∘ f)
-- Mathlib.Probability.Martingale.Basic
/-- Given a discrete submartingale `f` and a predictable process `ξ` (i.e. `ξ (n + 1)` is strongly
adapted) the process defined by `fun n => ∑ k ∈ Finset.range n, ξ (k + 1) * (f (k + 1) - f k)` is
also a submartingale.  -/
MeasureTheory.Submartingale.sum_smul_sub' : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] [inst_3 : PartialOrder E]
  [IsOrderedModule ℝ E] [ClosedIciTopology E] [IsOrderedAddMonoid E] [MeasureTheory.IsFiniteMeasure μ] {R : ℝ}
  {ξ : ℕ → Ω → ℝ} {f : ℕ → Ω → E},
  MeasureTheory.Submartingale f 𝒢 μ →
    (MeasureTheory.StronglyAdapted 𝒢 fun n => ξ (n + 1)) →
      (∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R) →
        (∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω) →
          MeasureTheory.Submartingale (fun n => ∑ k ∈ Finset.range n, ξ (k + 1) • (f (k + 1) - f k)) 𝒢 μ
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- A cone postcomposed with a natural isomorphism is a weak limit cone
if and only if the original cone is.
 -/
CategoryTheory.Limits.IsWeakLimit.postcompose_hom_iff_of_iso : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F G : CategoryTheory.Functor J C} (α : F ≅ G)
  (c : CategoryTheory.Limits.Cone F),
  Nonempty (CategoryTheory.Limits.IsWeakLimit ((CategoryTheory.Limits.Cone.postcompose α.hom).obj c)) ↔
    Nonempty (CategoryTheory.Limits.IsWeakLimit c)
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  {M N : ↑(F.obj { as := Opposite.op S })} (f : M ⟶ N),
  F.presheafHomObjHomEquiv f =
    CategoryTheory.CategoryStruct.comp ((F.mapId { as := Opposite.op S }).hom.toNatTrans.app M)
      (CategoryTheory.CategoryStruct.comp f ((F.mapId { as := Opposite.op S }).inv.toNatTrans.app N))
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.deriv_mulExpNegMulSq : ∀ {ε : ℝ} (y : ℝ), deriv ε.mulExpNegMulSq y = Real.exp (-(ε * y * y)) + y * (Real.exp (-(ε * y * y)) * (-2 * ε * y))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.link.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr_2 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) (hr_4 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.link k v (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') Std.DTreeMap.Internal.Impl.leaf
      hr_2 hr_4 =
    { impl := (Std.DTreeMap.Internal.Impl.insertMax k v (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') ⋯).impl,
      balanced_impl := ⋯, size_impl := ⋯ }
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.revAll_char_eq_revAll_beq : ∀ {c : Char} {s : String.Slice}, s.revAll c = s.revAll fun x => x == c
-- Mathlib.GroupTheory.Index
AddSubgroup.index_comap : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) (f : G' →+ G),
  (AddSubgroup.comap f H).index = H.relIndex f.range
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.commutator_lt : ∀ (G : Type u_1) [inst : Group G] [Finite G] [IsZGroup G] [Nontrivial G], commutator G < ⊤
-- Mathlib.Analysis.InnerProductSpace.Subspace
OrthogonalFamily.inner_right_fintype : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V →
    ∀ [inst_5 : Fintype ι] (l : (i : ι) → G i) (i : ι) (v : G i), inner 𝕜 ((V i) v) (∑ j, (V j) (l j)) = inner 𝕜 v (l i)
-- Mathlib.Algebra.CharP.Algebra
/-- If a ring homomorphism `R →+* A` is injective then `A` has the same characteristic as `R`.  -/
charP_of_injective_ringHom : ∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring A] {f : R →+* A},
  Function.Injective ⇑f → ∀ (p : ℕ) [CharP R p], CharP A p
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.inner_fourier_toL2_eq : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] {H : Type u_4} [inst_5 : NormedAddCommGroup H]
  [inst_6 : InnerProductSpace ℂ H] [CompleteSpace H] (f g : SchwartzMap V H),
  inner ℂ ((FourierTransform.fourier f).toLp 2 MeasureTheory.volume)
      ((FourierTransform.fourier g).toLp 2 MeasureTheory.volume) =
    inner ℂ (f.toLp 2 MeasureTheory.volume) (g.toLp 2 MeasureTheory.volume)
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk_d : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0)
  (n : ℕ),
  (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 3) (n + 2) =
    CategoryTheory.CategoryStruct.comp (ChainComplex.mkXIso X₀ X₁ X₂ d₀ d₁ s succ n).hom
      (succ
            { X₁ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2),
              X₂ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
              X₃ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X n,
              f := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
              g := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst
-- Mathlib.Order.CompleteLattice.Basic
binary_relation_sInf_iff : ∀ {α : Type u_8} {β : Type u_9} (s : Set (α → β → Prop)) {a : α} {b : β}, sInf s a b ↔ ∀ r ∈ s, r a b
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_inf : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  (K L : Ideal S) [inst_3 : RingHomClass F R S], Ideal.comap f (K ⊓ L) = Ideal.comap f K ⊓ Ideal.comap f L
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.mk : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} →
    autoParam (⦃n : ℕ⦄ → L.Functions n → L'.Functions n) FirstOrder.Language.LHom.onFunction._autoParam →
      autoParam (⦃n : ℕ⦄ → L.Relations n → L'.Relations n) FirstOrder.Language.LHom.onRelation._autoParam → (L →ᴸ L')
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.empty_right : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (s : Set X), Metric.AreSeparated s ∅
-- Mathlib.FieldTheory.Galois.Basic
/-- Equivalent characterizations of a Galois extension of finite degree.  -/
IsGalois.tfae : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E],
  [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Nat.card Gal(E/F) = Module.finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
-- Mathlib.Order.Lex
instCoeFunColex : {α : Type u_2} → {γ : α → Sort u_3} → [H : CoeFun α γ] → CoeFun (Colex α) γ
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a left invariant measure under a left additive action is left
invariant, assuming that the action preserves addition.  -/
MeasureTheory.isAddLeftInvariant_map_vadd : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G}
  {α : Type u_3} [inst_3 : VAdd α G] [VAddCommClass α G G] [MeasurableConstVAdd α G] [μ.IsAddLeftInvariant] (a : α),
  (MeasureTheory.Measure.map (fun x => a +ᵥ x) μ).IsAddLeftInvariant
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
Commute.pow_dvd_add_pow_of_pow_eq_zero_left : ∀ {R : Type u_1} {x y : R} {n m p : ℕ} [inst : Semiring R],
  n + m ≤ p + 1 → Commute x y → x ^ n = 0 → y ^ m ∣ (x + y) ^ p
-- Mathlib.Order.Heyting.Basic
/-- `p ∧ (p → q) ↔ p ∧ q`  -/
inf_himp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⊓ (a ⇨ b) = a ⊓ b
-- Mathlib.Data.List.TakeWhile
List.mem_takeWhile_imp : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {x : α}, x ∈ List.takeWhile p l → p x = true
-- Lean.Util.Profile
Lean.profiler.threshold.getSecs : Lean.Options → Float
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.kerCotangentToTensor_toCotangent : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] (x : ↥(RingHom.ker (algebraMap A B))),
  (KaehlerDifferential.kerCotangentToTensor R A B) ((RingHom.ker (algebraMap A B)).toCotangent x) =
    1 ⊗ₜ[A] (KaehlerDifferential.D R A) ↑x
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.invalidStatusLine.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.invalidStatusLine = 1
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.TableEntry.answers : Lean.Meta.SynthInstance.TableEntry → Array Lean.Meta.SynthInstance.Answer
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_iUnion_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : Fintype ι] (f : α → ENNReal) (t : ι → Set α),
  ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑ i, ∑' (x : ↑(t i)), f ↑x
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instT2Space : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [T2Space R] [T2Space M],
  T2Space (TrivSqZeroExt R M)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_le_size_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β}, t.size - 1 ≤ (Std.ExtDTreeMap.Const.alter t k f).size
-- Mathlib.Topology.MetricSpace.Holder
/-- **Alias** of the reverse direction of `holderOnWith_one`. -/
LipschitzOnWith.holderOnWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C : NNReal} {f : X → Y}
  {s : Set X}, LipschitzOnWith C f s → HolderOnWith C 1 f s
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.pi_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {ι : Type u_4} {φ : ι → Type u_5} [inst_4 : (i : ι) → TopologicalSpace (φ i)]
  [inst_5 : (i : ι) → AddCommMonoid (φ i)] [inst_6 : (i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i),
  ContinuousLinearMap.pi f = 0 ↔ ∀ (i : ι), f i = 0
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_iInf : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {ι : Sort u_7} (f : G →* N) (s : ι → Subgroup N),
  Subgroup.comap f (iInf s) = ⨅ i, Subgroup.comap f (s i)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_apply_mono_right : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] (u : ι → Ω → β) (s : Set β)
  (n : ι) (ω : Ω), Monotone fun x => MeasureTheory.hittingBtwn u s n x ω
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The terminal factorisation is a terminal object  -/
CategoryTheory.Factorisation.IsTerminal_terminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Limits.IsTerminal CategoryTheory.Factorisation.terminal
-- Mathlib.MeasureTheory.Measure.Restrict
ae_eq_restrict_iff_indicator_ae_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
  [inst_1 : Zero β] {g : α → β}, MeasurableSet s → (f =ᵐ[μ.restrict s] g ↔ s.indicator f =ᵐ[μ] s.indicator g)
-- Mathlib.AlgebraicGeometry.Properties
/-- [Stacks Tag 02IZ](https://stacks.math.columbia.edu/tag/02IZ) -/
AlgebraicGeometry.ringKrullDim_stalk_eq_coheight : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X), ringKrullDim ↑(X.presheaf.stalk x) = ↑(Order.coheight x)
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜), UniqueDiffWithinAt 𝕜 s x → derivWithin id s x = 1
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.next_toList_eq_apply : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : Equiv.Perm α) (x y : α) (hy : y ∈ p.toList x),
  (p.toList x).next y hy = p y
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.mul : {α : Type u} → [Add α] → Mul (Multiplicative α)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.eq_dual_comm : ∀ {α : Type u_1} {M₁ M₂ : Matroid α}, M₁ = M₂✶ ↔ M₂ = M₁✶
-- Mathlib.Order.Cover
Pi.exists_forall_antisymmRel_of_wcovBy : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] {a b : (i : ι) → α i} [Nonempty ι],
  a ⩿ b → ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 => x1 ≤ x2) (a j) (b j)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
/-- `abs a`, denoted `|a|`, is the absolute value of `a`  -/
«term|___|» : Lean.ParserDescr
-- Mathlib.Order.UpperLower.Fibration
Relation.fibration_iff_image_Iic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  Monotone f →
    (Relation.Fibration (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) f ↔ ∀ (x : α), f '' Set.Iic x = Set.Iic (f x))
-- Mathlib.Topology.ContinuousMap.Compact
/-- If the product of continuous functions on a compact space is zero, then the norm of their sum
is the maximum of their norms.  -/
ContinuousMap.nnnorm_add_eq_max : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] {R : Type u_4}
  [inst_2 : NonUnitalSeminormedRing R] [IsCancelMulZero R] {f g : C(α, R)}, f * g = 0 → ‖f + g‖₊ = max ‖f‖₊ ‖g‖₊
-- Mathlib.Data.Multiset.UnionInter
Multiset.count_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α),
  Multiset.count a (s ∩ t) = min (Multiset.count a s) (Multiset.count a t)
-- Mathlib.Analysis.CStarAlgebra.Basic
/-- This instance exists to short circuit type class resolution because of problems with
inference involving Π-types.  -/
Pi.starRing' : {ι : Type u_4} →
  {R : ι → Type u_7} →
    [inst : (i : ι) → NonUnitalNormedRing (R i)] → [(i : ι) → StarRing (R i)] → StarRing ((i : ι) → R i)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact : ∀ {a : ℝ}, 0 < a → ∀ (s : ℝ), Filter.Tendsto (fun x => |x| ^ s * Real.exp (-a * x ^ 2)) (Filter.cocompact ℝ) (nhds 0)
-- Mathlib.Data.Matrix.Mul
IsStablyFiniteRing.of_injective : ∀ {R : Type u_10} {S : Type u_11} {F : Type u_12} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : FunLike F R S] [RingHomClass F R S] (f : F),
  Function.Injective ⇑f → ∀ [IsStablyFiniteRing S], IsStablyFiniteRing R
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.mk.sizeOf_spec : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] [inst_5 : SizeOf F] [inst_6 : SizeOf E] [inst_7 : SizeOf K]
  (carrier : IntermediateField F E) (emb : ↥carrier →ₐ[F] K),
  sizeOf { carrier := carrier, emb := emb } = 1 + sizeOf carrier + sizeOf emb
-- Lean.Parser.Extra
/-- No-op parser combinator that advises the pretty printer to dedent the given syntax.
Dedenting can in particular be used to counteract automatic indentation.  -/
Lean.Parser.ppDedent : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.differentiableOn : ∀ {𝕜 : 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] {s : Set E}
  (iso : E ≃ₗᵢ[𝕜] F), DifferentiableOn 𝕜 (⇑iso) s
-- Init.Data.Fin.Lemmas
Fin.cast_castAdd_right : ∀ {n m m' : ℕ} (i : Fin n) (h : n + m' = n + m), Fin.cast h (Fin.castAdd m' i) = Fin.castAdd m i
-- Mathlib.Data.Sym.Basic
Sym.uniqueZero : {α : Type u_1} → Unique (Sym α 0)
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.Script.TacticBuilder.simpAllOrSimpAtStarStx : {m : Type → Type} → [Monad m] → [Lean.MonadQuotation m] → Bool → Option Lean.Term → m Lean.Syntax.Tactic
-- Lean.LibrarySuggestions.SineQuaNon
/-- Return the relevant constants (i.e. ignoring instances and proofs)
which appear in the type of `ci` and which are approximately least frequent in the library
(relative to other constants appearing in the type of `ci`).
 -/
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.triggerSymbols : Lean.ConstantInfo → optParam Float 3.0 → Lean.MetaM (Array (Lean.Name × Float))
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- This lemma uses the simp-normal form `⇑A ∘ ⇑(A.adjoint)` instead of `⇑(A ∘ₗ A.adjoint)`
(note the difference between `∘` and `∘ₗ`).
You may need to rewrite with `LinearMap.coe_comp` before applying this lemma.
 -/
LinearMap.self_comp_adjoint_injective_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  Function.Injective (⇑A ∘ ⇑(LinearMap.adjoint A)) ↔ Function.Injective ⇑(LinearMap.adjoint A)
-- Mathlib.Analysis.Distribution.TestFunction
/-- Given a continuous `𝕜`-bilinear map `B : F₁ →L[𝕜] F₂ →L[𝕜] F₃`, a measure `μ` on `E`,
and a function `φ : E → F₂` which is locally `μ`-integrable, this is the *continuous* `𝕜`-linear map
`f ↦ ∫ x, B (f x) (φ x) ∂μ` from `𝓓^{n}(E, F₁)` to `F₃`. Otherwise, this is the zero map.  -/
TestFunction.integralAgainstBilinCLM : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {Ω : TopologicalSpace.Opens E} →
            {n : ℕ∞} →
              {m : MeasurableSpace E} →
                [OpensMeasurableSpace E] →
                  {F₁ : Type u_6} →
                    {F₂ : Type u_7} →
                      {F₃ : Type u_8} →
                        [inst_4 : NormedAddCommGroup F₁] →
                          [inst_5 : NormedSpace 𝕜 F₁] →
                            [inst_6 : NormedSpace ℝ F₁] →
                              [inst_7 : NormedAddCommGroup F₂] →
                                [inst_8 : NormedSpace 𝕜 F₂] →
                                  [inst_9 : NormedAddCommGroup F₃] →
                                    [inst_10 : NormedSpace 𝕜 F₃] →
                                      [inst_11 : Algebra ℝ 𝕜] →
                                        [inst_12 : IsScalarTower ℝ 𝕜 F₁] →
                                          [inst_13 : NormedSpace ℝ F₃] →
                                            [IsScalarTower ℝ 𝕜 F₃] →
                                              (F₁ →L[𝕜] F₂ →L[𝕜] F₃) →
                                                MeasureTheory.Measure E → (E → F₂) → TestFunction Ω F₁ n →L[𝕜] F₃
-- Mathlib.Topology.Maps.Basic
Topology.isCoinducing_iff : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsCoinducing f ↔ ∀ (s : Set Y), IsOpen (f ⁻¹' s) ↔ IsOpen s
-- Mathlib.Tactic.CongrExclamation
/-- The transparency level to use when trying to close goals before applying congruence lemmas.
This includes trying to prove the goal by `rfl` and using the `assumption` tactic.
By default this is `.reducible`, which prevents unfolding of most definitions.  -/
Congr!.Config.preTransparency : Congr!.Config → Lean.Meta.TransparencyMode
-- Std.Time.Date.Unit.Week
Std.Time.Week.instDecidableLeOffset : {x y : Std.Time.Week.Offset} → Decidable (x ≤ y)
-- Mathlib.Order.Notation
_private.Mathlib.Order.Notation.0.Mathlib.Meta.linearOrderExpr : (u : Lean.Level) → Q(Type u → Type u)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is `π / 2`, the first and third points are not equal.  -/
EuclideanGeometry.left_ne_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → p₁ ≠ p₃
-- Std.Do.SPred.SPred
Std.Do.SPred.entails_nil : ∀ {P Q : Std.Do.SPred []}, (P ⊢ₛ Q) = (P.down → Q.down)
-- Mathlib.Analysis.Normed.Group.Submodule
/-- A submodule of a normed group is also a normed group, with the restriction of the norm.  -/
Submodule.normedAddCommGroup : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Ring 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : Module 𝕜 E] → (s : Submodule 𝕜 E) → NormedAddCommGroup ↥s
-- Mathlib.CategoryTheory.Sites.Monoidal
CategoryTheory.GrothendieckTopology.W.transport_isMonoidal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₃)
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.MonoidalCategory A] {D : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D)
  (G : CategoryTheory.Functor D C) [G.IsCoverDense J] [G.Full] [inst_6 : G.IsContinuous K J]
  [(G.sheafPushforwardContinuous A K J).EssSurj] [K.W.IsMonoidal], J.W.IsMonoidal
-- Mathlib.Topology.Algebra.Group.Basic
/-- A monoid homomorphism (a bundled morphism of a type that implements `MonoidHomClass`)
from a topological group to a topological monoid is continuous
provided that it is continuous at one.

This version assumes that `f x → 1` as `x → 1`,
saving a rewrite of `f 1 = 1` compared to `continuous_of_continuousAt_one` in some cases.
See also `uniformContinuous_of_continuousAt_one`.  -/
continuous_of_tendsto_nhds_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {M : Type u_1} {hom : Type u_2}
  [inst_3 : MulOneClass M] [inst_4 : TopologicalSpace M] [ContinuousMul M] [inst_6 : FunLike hom G M]
  [MonoidHomClass hom G M] (f : hom), Filter.Tendsto (⇑f) (nhds 1) (nhds 1) → Continuous ⇑f
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.ExactFunctor.whiskeringRight_map_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : D ⥤ₑ E} (η : F ⟶ G) (H : C ⥤ₑ D),
  ((CategoryTheory.ExactFunctor.whiskeringRight C D E).map η).app H =
    CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app H.obj)