mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.IsDedekindDomain.ramificationIdx'_eq_one_iff`. -/
Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  {p : Ideal R} {P : Ideal S} [inst_4 : P.IsPrime],
  P ≠ ⊥ →
    Ideal.map (algebraMap R S) p ≤ P →
      (p.ramificationIdx' P = 1 ↔
        Ideal.map (algebraMap R (Localization.AtPrime P)) p = IsLocalRing.maximalIdeal (Localization.AtPrime P))
-- Mathlib.Algebra.Polynomial.Basic
_private.Mathlib.Algebra.Polynomial.Basic.0.Polynomial.support.match_1.splitter : {R : Type u_1} →
  [inst : Semiring R] →
    (motive : Polynomial R → Sort u_2) →
      (x : Polynomial R) → ((p : AddMonoidAlgebra R ℕ) → motive { toFinsupp := p }) → motive x
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- The adjunction between `Spec` and `Γ` as functors between commutative `R`-algebras and
schemes over `Spec R`.  -/
AlgebraicGeometry.algΓAlgSpecAdjunction : (R : CommRingCat) → AlgebraicGeometry.algΓ R ⊣ AlgebraicGeometry.algSpec R
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_eq_sum_compProd_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ)
  [inst : ProbabilityTheory.IsSFiniteKernel η],
  κ.compProd η = ProbabilityTheory.Kernel.sum fun n => κ.compProd (η.seq n)
-- Mathlib.Analysis.Normed.Operator.Completeness
/-- Let `f : E → F` be a map, let `g : α → E →SL[σ₁₂] F` be a family of continuous (semi)linear maps
that takes values in a bounded set and converges to `f` pointwise along a nontrivial filter. Then
`f` is a continuous (semi)linear map.  -/
ContinuousLinearMap.ofTendstoOfBoundedRange : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {F : Type u_4} →
      [inst : NormedAddCommGroup F] →
        [inst_1 : NontriviallyNormedField 𝕜] →
          [inst_2 : NontriviallyNormedField 𝕜₂] →
            [inst_3 : NormedSpace 𝕜₂ F] →
              {σ₁₂ : 𝕜 →+* 𝕜₂} →
                {E' : Type u_6} →
                  [inst_4 : SeminormedAddCommGroup E'] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      [inst_6 : RingHomIsometric σ₁₂] →
                        {α : Type u_7} →
                          {l : Filter α} →
                            [l.NeBot] →
                              (f : E' → F) →
                                (g : α → E' →SL[σ₁₂] F) →
                                  Filter.Tendsto (fun a x => (g a) x) l (nhds f) →
                                    Bornology.IsBounded (Set.range g) → E' →SL[σ₁₂] F
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.AbsoluteLspSemanticToken.mk.sizeOf_spec : ∀ (pos tailPos : Lean.Lsp.Position) (type : Lean.Lsp.SemanticTokenType) (priority : ℕ),
  sizeOf { pos := pos, tailPos := tailPos, type := type, priority := priority } =
    1 + sizeOf pos + sizeOf tailPos + sizeOf type + sizeOf priority
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.instContinuousFourier : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E],
  ContinuousFourier ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.closure_sub : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {t : Set G},
  IsOpen t → ∀ (s : Set G), closure s - t = s - t
-- Init.Control.Except
/-- Handles exceptions thrown by an action that can have no effects _other_ than throwing exceptions.
 -/
ExceptT.bindCont : {ε : Type u} → {m : Type u → Type v} → [Monad m] → {α β : Type u} → (α → ExceptT ε m β) → Except ε α → m (Except ε β)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Multiplicativity of a continuous multilinear map along all coordinates at the same time,
writing `f (fun i ↦ c i • m i)` as `(∏ i, c i) • f m`.  -/
ContinuousMultilinearMap.map_smul_univ : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : Fintype ι] (c : ι → R) (m : (i : ι) → M₁ i),
  (f fun i => c i • m i) = (∏ i, c i) • f m
-- Mathlib.Algebra.Group.Basic
/-- If a binary function from a type equipped with a total
relation `r` to an additive monoid is anti-symmetric (i.e. satisfies `f a b + f b a = 0`), in
order to show it is additive (i.e. satisfies `f a c = f a b + f b c`), we may assume `r a b` and
`r b c` are satisfied. We allow restricting to a subset specified by a predicate `p`.  -/
additive_of_total : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid β] (r : α → α → Prop) [Std.Total r] (f : α → α → β) (p : α → Prop),
  (∀ {a b : α}, p a → p b → f a b + f b a = 0) →
    (∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b + f b c) →
      ∀ {a b c : α}, p a → p b → p c → f a c = f a b + f b c
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.map_f₃₄_op_glue : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] {S : J.MayerVietorisSquare}
  {P : CategoryTheory.Functor Cᵒᵖ (Type v')} (h : S.SheafCondition P) (u : P.obj (Opposite.op S.X₂))
  (v : P.obj (Opposite.op S.X₃))
  (huv :
    (CategoryTheory.ConcreteCategory.hom (P.map S.f₁₂.op)) u =
      (CategoryTheory.ConcreteCategory.hom (P.map S.f₁₃.op)) v),
  (CategoryTheory.ConcreteCategory.hom (P.map S.f₃₄.op)) (h.glue u v huv) = v
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- Isomorphism of cones preserves whether or not they are weak limit cones.  -/
CategoryTheory.Limits.IsWeakLimit.equivIsoWeakLimit : {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 : CategoryTheory.Functor J C} →
          {r t : CategoryTheory.Limits.Cone F} →
            (r ≅ t) → CategoryTheory.Limits.IsWeakLimit r ≃ CategoryTheory.Limits.IsWeakLimit t
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.bound_ne_top : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsFiniteKernel κ], κ.bound ≠ ⊤
-- Mathlib.Order.Directed
directedOn_iff_isCodirectedOrder : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, DirectedOn (fun x1 x2 => x2 ≤ x1) s ↔ IsCodirectedOrder ↑s
-- Mathlib.Data.ENNReal.Inv
_private.Mathlib.Data.ENNReal.Inv.0.ENNReal.exists_lt_mul_left : ∀ {a b c : ENNReal}, c < a * b → ∃ a' < a, c < a' * b
-- Mathlib.ModelTheory.Syntax
/-- The `Finset` of variables from the left side of a sum used in a given term.  -/
FirstOrder.Language.Term.varFinsetLeft : {L : FirstOrder.Language} → {α : Type u'} → {β : Type v'} → [DecidableEq α] → L.Term (α ⊕ β) → Finset α
-- Mathlib.Order.RelSeries
LTSeries.comap_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (p : LTSeries β) (f : α → β)
  (comap : ∀ ⦃x y : α⦄, f x < f y → x < y) (surjective : Function.Surjective f) (i : Fin (p.length + 1)),
  (p.comap f comap surjective).toFun i = ⋯.choose
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
IntervalIntegrable.log : ∀ {a b : ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ],
  ContinuousOn f (Set.uIcc a b) → (∀ x ∈ Set.uIcc a b, f x ≠ 0) → IntervalIntegrable (fun x => Real.log (f x)) μ a b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.equiv_iff_toArray_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.toArray = t₂.toArray)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.jordanDecomposition_add_withDensity_mutuallySingular : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : MeasureTheory.SignedMeasure α} {f : α → ℝ},
  Measurable f →
    MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure →
      (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)).MutuallySingular
        (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x))
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.le_min_of_le_of_lt : ∀ {R : Type u_2} [inst : LinearOrder R] {a b c : R}, a ≤ b → a < c → a ≤ min b c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, t.contains k = true → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Init.Data.Int.Order
Int.natCast_pos : ∀ {n : ℕ}, 0 < ↑n ↔ 0 < n
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.comul_comp_finsuppLcoeFun : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M : Type u_4}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : CoalgebraStruct R M],
  CoalgebraStruct.comul ∘ₗ Finsupp.lcoeFun = TensorProduct.map Finsupp.lcoeFun Finsupp.lcoeFun ∘ₗ CoalgebraStruct.comul
-- Lean.Class
Lean.ClassEntry.mk.sizeOf_spec : ∀ (name : Lean.Name) (outParams outLevelParams : Array ℕ),
  sizeOf { name := name, outParams := outParams, outLevelParams := outLevelParams } =
    1 + sizeOf name + sizeOf outParams + sizeOf outLevelParams
-- Mathlib.Condensed.Limits
instHasLimitsCondensedSet : CategoryTheory.Limits.HasLimits CondensedSet
-- Mathlib.CategoryTheory.Category.Quiv
/-- An isomorphism of quivers defines an equivalence on hom types.  -/
CategoryTheory.Quiv.homEquivOfIso : {V W : CategoryTheory.Quiv} → (e : V ≅ W) → {X Y : ↑V} → (X ⟶ Y) ≃ (e.hom.obj X ⟶ e.hom.obj Y)
-- Mathlib.Analysis.Convex.Topology
Convex.openSegment_interior_self_subset_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E}, x ∈ interior s → y ∈ s → openSegment 𝕜 x y ⊆ interior s
-- Mathlib.Dynamics.Flow
Flow.image_eq_preimage_symm : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddGroup τ]
  (ϕ : Flow τ α) (t : τ) (s : Set α), ϕ.toFun t '' s = ϕ.toFun (-t) ⁻¹' s
-- Mathlib.MeasureTheory.Group.FoelnerFilter
/-- The maximal Følner filter with respect to some additive group `G` acting
on a measure space `X` is the pullback of `𝓝 0` along the map `s ↦ μ (g +ᵥ s) / μ s`
on measurable sets of finite non-zero measure.  -/
maxAddFoelner : (G : Type u_1) →
  {X : Type u_2} →
    [inst : MeasurableSpace X] → MeasureTheory.Measure X → [inst : AddGroup G] → [AddAction G X] → Filter (Set X)
-- Mathlib.Algebra.Opposites
AddOpposite.unop_surjective : ∀ {α : Type u_1}, Function.Surjective AddOpposite.unop
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- An open cover of a scheme `X` is a cover where all component maps are open immersions.  -/
AlgebraicGeometry.Scheme.OpenCover : AlgebraicGeometry.Scheme → Type (max (v + 1) (u + 1))
-- Mathlib.NumberTheory.Dioph
IsPoly.mul : ∀ {α : Type u_1} {f g : (α → ℕ) → ℤ}, IsPoly f → IsPoly g → IsPoly fun x => f x * g x
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- Adjoining S and then T is the same as adjoining `S ∪ T`.  -/
IntermediateField.adjoin_adjoin_left : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S T : Set E),
  IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F S)) T) =
    IntermediateField.adjoin F (S ∪ T)
-- Mathlib.Data.Fin.Tuple.Basic
/-- A weak version of `Fin.find_mono_of_le`, requiring `q` implies `p` everywhere.
 -/
Fin.find_mono : ∀ {n : ℕ} {p q : Fin n → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q],
  (∀ (i : Fin n), q i → p i) → ∀ {hp : ∃ i, p i} {hq : ∃ i, q i}, Fin.find p hp ≤ Fin.find q hq
-- Mathlib.Data.Nat.ModEq
Nat.modEq_add_modulus_mul_iff : ∀ {n a b c : ℕ}, a ≡ b + n * c [MOD n] ↔ a ≡ b [MOD n]
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Definable₁.mk_out : ∀ {f : ZFSet.{u} → ZFSet.{u}} [inst : ZFSet.Definable₁ f] {x : PSet.{u}},
  ZFSet.mk (ZFSet.Definable₁.out f x) = f (ZFSet.mk x)
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G)
  [CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G] (A : adj.toMonad.Algebra),
  CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G
-- Mathlib.Data.EReal.Basic
EReal.image_coe_Ioo : ∀ (x y : ℝ), Real.toEReal '' Set.Ioo x y = Set.Ioo ↑x ↑y
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.instBEqRelevantArg : BEq Mathlib.Tactic.Translate.RelevantArg
-- Mathlib.Algebra.Order.Hom.Basic
abs_sub_map_le_sub : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommGroup β]
  [inst_3 : LinearOrder β] [IsOrderedAddMonoid β] [AddGroupSeminormClass F α β] (f : F) (x y : α),
  |f x - f y| ≤ f (x - y)
-- Mathlib.Order.Interval.Multiset
/-- **Alias** of the reverse direction of `Multiset.Ioc_eq_zero_iff`. -/
Multiset.Ioc_eq_zero : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a < b → Multiset.Ioc a b = 0
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- Transformation of `seqTendstoAeSeqAux` to makes sure it is strictly monotone.  -/
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        [inst : PseudoEMetricSpace E] →
          {f : ℕ → α → E} → {g : α → E} → MeasureTheory.TendstoInMeasure μ f Filter.atTop g → ℕ → ℕ
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.of_smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T : Set α → β}
  [inst : AddMonoid β] {c : ENNReal},
  c ≠ ⊤ → MeasureTheory.FinMeasAdditive (c • μ) T → MeasureTheory.FinMeasAdditive μ T
-- Init.Data.List.Impl
/-- Auxiliary for `insertIdxTR`: `insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l`.  -/
_private.Init.Data.List.Impl.0.List.insertIdxTR.go : {α : Type u_1} → α → ℕ → List α → Array α → List α
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- Main theorem on differentiation of measures: given a Vitali family `v` for a locally finite
measure `μ`, and another locally finite measure `ρ`, then for `μ`-almost every `x` the
ratio `ρ a / μ a` converges, when `a` shrinks to `x` along the Vitali family, towards the
Radon-Nikodym derivative of `ρ` with respect to `μ`.  -/
VitaliFamily.ae_tendsto_rnDeriv : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  (ρ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure ρ],
  ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (nhds (ρ.rnDeriv μ x))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `inv_lt_iff_one_lt_mul₀'` for a version with multiplication on the other side.  -/
inv_lt_iff_one_lt_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀},
  0 < a → (a⁻¹ < b ↔ 1 < b * a)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂'_obj_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' C).obj X₁).obj X₂).obj X₃ =
    CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₃ X₂)
-- Mathlib.Data.Nat.Bitwise
/-- The xor of the numbers from 0 to n can be easily calculated using `n mod 4`.  -/
Nat.xor_range : ∀ (n : ℕ),
  List.foldl (fun x1 x2 => x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.coe.inj : ∀ {header? : Option String} {expectedType e : Lean.Expr} {f? : Option Lean.Expr}
  {mkErrorMsg? : Option (Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData)} {header?_1 : Option String}
  {expectedType_1 e_1 : Lean.Expr} {f?_1 : Option Lean.Expr}
  {mkErrorMsg?_1 : Option (Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData)},
  Lean.Elab.Term.SyntheticMVarKind.coe header? expectedType e f? mkErrorMsg? =
      Lean.Elab.Term.SyntheticMVarKind.coe header?_1 expectedType_1 e_1 f?_1 mkErrorMsg?_1 →
    header? = header?_1 ∧ expectedType = expectedType_1 ∧ e = e_1 ∧ f? = f?_1 ∧ mkErrorMsg? = mkErrorMsg?_1
-- Mathlib.Analysis.Calculus.Deriv.Mul
DifferentiableWithinAt.fun_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} {𝔸' : Type u_3}
  [inst_1 : NormedCommRing 𝔸'] [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) → DifferentiableWithinAt 𝕜 (fun x => ∏ i ∈ u, f i x) s x
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.measurable_gaussianPDFReal : ∀ (μ : ℝ) (v : NNReal), Measurable (ProbabilityTheory.gaussianPDFReal μ v)
-- Mathlib.Logic.ExistsUnique
ExistsUnique.unique₂ : ∀ {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop},
  (∃! x, ∃! hx, q x hx) → ∀ {y₁ y₂ : α} (hpy₁ : p y₁), q y₁ hpy₁ → ∀ (hpy₂ : p y₂), q y₂ hpy₂ → y₁ = y₂
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.basisOfIsMaxRank.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u u_1 : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (e_u : u = u_1)
  (hu : NumberField.Units.IsMaxRank u), NumberField.Units.basisOfIsMaxRank hu = NumberField.Units.basisOfIsMaxRank ⋯
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
Real.rank_rat_real : Module.rank ℚ ℝ = Cardinal.continuum
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.comp_symm : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  ↑e ∘ₛₗ ↑e.symm = LinearMap.id
-- Mathlib.Dynamics.Flow
IsInvariant.isForwardInvariant : ∀ {τ : Type u_1} {α : Type u_2} [inst : Preorder τ] [inst_1 : Zero τ] {ϕ : τ → α → α} {s : Set α},
  IsInvariant ϕ s → IsForwardInvariant ϕ s
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd_eq : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b : ℤ),
  CategoryTheory.shiftFunctorAdd (CategoryTheory.Pretriangulated.Triangle C) a b =
    CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b (a + b) ⋯
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_tensorUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  Opposite.unop (CategoryTheory.MonoidalCategoryStruct.tensorUnit Cᵒᵖ) =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.RingTheory.Unramified.LocalRing
Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S] (p : Ideal R) [inst_4 : p.IsPrime] (q : Ideal S) [inst_5 : q.IsPrime]
  [inst_6 : q.LiesOver p] [inst_7 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q] [Algebra.IsUnramifiedAt R q],
  Algebra.IsSeparable p.ResidueField q.ResidueField
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.eq_symm_comp : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {α : Type u_9} (e : M ≃+ N) (f : α → M) (g : α → N),
  f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
-- Mathlib.Algebra.Order.Ring.Abs
sq_lt_sq' : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  -b < a → a < b → a ^ 2 < b ^ 2
-- Mathlib.GroupTheory.Finiteness
Monoid.powers_fg : ∀ {M : Type u_1} [inst : Monoid M] (r : M), Monoid.FG ↥(Submonoid.powers r)
-- Mathlib.Order.CompleteLattice.Finset
Finset.iSup_finset_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice β] [inst_1 : DecidableEq α] {f : γ → α}
  {g : α → β} {s : Finset γ}, ⨆ x ∈ Finset.image f s, g x = ⨆ y ∈ s, g (f y)
-- Mathlib.Probability.Martingale.Basic
/-- A predictable supermartingale is a.e. less than or equal to its initial state.  -/
MeasureTheory.Supermartingale.le_zero_of_predictable' : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : Preorder E]
  [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
  MeasureTheory.Supermartingale f 𝒢 μ → MeasureTheory.IsStronglyPredictable 𝒢 f → ∀ (n : ℕ), f n ≤ᵐ[μ] f 0
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.Shatters.nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α}, 𝒜.Shatters s → 𝒜.Nonempty
-- Mathlib.MeasureTheory.Function.UnifTight
MeasureTheory.UnifTight.sub : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f g : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifTight f p μ →
    MeasureTheory.UnifTight g p μ →
      (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
        (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ) → MeasureTheory.UnifTight (f - g) p μ
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Occurrence sets are open.  -/
SymbolicDynamics.FullShift.isOpen_occursInAt : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Inhabited A] {G : Type u_2} [inst_2 : AddMonoid G]
  [IsLeftCancelAdd G] [DiscreteTopology A] (p : SymbolicDynamics.FullShift.Pattern A G) (g : G),
  IsOpen {x | p.occursInAt x g}
-- Mathlib.Order.SupClosed
isSublattice_preimage_toDual : ∀ {α : Type u_3} [inst : Lattice α] {s : Set αᵒᵈ}, IsSublattice (⇑OrderDual.toDual ⁻¹' s) ↔ IsSublattice s
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.pushoutCongr_hom_app_left_fst : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [inst_2 : P.HasPushoutsAlong f] {g : X ⟶ Y}
  [inst_3 : P.IsStableUnderCobaseChangeAlong f] [inst_4 : Q.IsStableUnderCobaseChange] (h : f = g) (A : P.Under Q X),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom f)
      ((CategoryTheory.MorphismProperty.Under.pushoutCongr h).hom.app A).right =
    CategoryTheory.Limits.pushout.inl A.hom g
-- Mathlib.Analysis.SpecialFunctions.Arsinh
ContDiffWithinAt.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a : E} {n : ℕ∞},
  ContDiffWithinAt ℝ (↑n) f s a → ContDiffWithinAt ℝ (↑n) (fun x => Real.arsinh (f x)) s a