mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.submartingale_of_setIntegral_le : ∀ {Ω : Type u_1} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ},
  MeasureTheory.StronglyAdapted ℱ f →
    (∀ (i : ι), MeasureTheory.Integrable (f i) μ) →
      (∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ) →
        MeasureTheory.Submartingale f ℱ μ
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.StrongHomClass.toEquiv.congr_simp : ∀ {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : EquivLike F M N] [inst_3 : L.StrongHomClass F M N] (a a_1 : F),
  a = a_1 → FirstOrder.Language.StrongHomClass.toEquiv a = FirstOrder.Language.StrongHomClass.toEquiv a_1
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.instToString : (n : ℕ) → ToString (Composition n)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- Contract an element of the Clifford algebra with an element `d : Module.Dual R M` from the
right.

Note that $x ⌊ v$ is spelt `contractRight x (Q.associated v)`.

This includes [grinberg_clifford_2016] Theorem 16.75  -/
CliffordAlgebra.contractRight : {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q : QuadraticForm R M} → CliffordAlgebra Q →ₗ[R] Module.Dual R M →ₗ[R] CliffordAlgebra Q
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- `N.IsFinitelyNormallyGenerated` says that the additive subgroup `N`
is the normal closure of a finite set.  -/
AddSubgroup.IsFinitelyNormallyGenerated : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → Prop
-- Mathlib.Algebra.Category.Grp.Colimits
/-- If `J` is `w`-small, then any functor `J ⥤ AddCommGrpCat.{w}` has a colimit.
 -/
AddCommGrpCat.hasColimitsOfShape : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [Small.{w, u} J],
  CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat
-- Init.Data.SInt.Lemmas
Int16.ofIntClamp_toInt : ∀ (x : Int16), Int16.ofIntClamp x.toInt = x
-- Mathlib.Algebra.Ring.Regular
/-- A ring with no zero divisors is a cancellative `MonoidWithZero`.

Note this is not an instance as it forms a typeclass loop.  -/
NoZeroDivisors.toIsCancelMulZero : ∀ {α : Type u_1} [inst : NonUnitalNonAssocRing α] [NoZeroDivisors α], IsCancelMulZero α
-- Mathlib.Data.Stream.Init
_private.Mathlib.Data.Stream.Init.0.Stream'.cons.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Data.Sym.Basic
Sym.mem_append_iff : ∀ {α : Type u_1} {n m : ℕ} {s : Sym α n} {a : α} {s' : Sym α m}, a ∈ s.append s' ↔ a ∈ s ∨ a ∈ s'
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- A probability measure can be interpreted as a measure.  -/
MeasureTheory.ProbabilityMeasure.instCoeMeasure : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → Coe (MeasureTheory.ProbabilityMeasure Ω) (MeasureTheory.Measure Ω)
-- Mathlib.NumberTheory.MahlerMeasure
/-- The set of polynomials whose coefficients are bounded between `B₁` and `B₂`. This
construction is used as part of our proof of Northcott's theorem.  -/
Polynomial.boxPoly : (n : ℕ) → (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) → Set (Polynomial ℤ)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.isClosed : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (s : ClosedSubmodule R M), IsClosed ↑s
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.prodMap : ∀ {𝕜 : 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'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_14} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_15}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {s : Set M} {f : M → M'} {g : N → N'} {r : Set N},
  MDiff[s] f → MDiff[r] g → MDiff[s ×ˢ r] (Prod.map f g)
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffOn_chart_symm : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {x : M} [IsManifold I n M],
  ContMDiffOn I I n (↑(chartAt H x).symm) (chartAt H x).target
-- Mathlib.Analysis.Analytic.Order
/-- If an analytic function `f` vanishes at `z₀`, then its derivative has finite analytic order `n`
at `z₀` if and only if `f` has analytic order `n + 1` at `z₀`.  -/
analyticOrderAt_deriv_eq_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {z₀ : 𝕜} {f : 𝕜 → E},
  AnalyticAt 𝕜 f z₀ → f z₀ = 0 → ∀ {n : ℕ}, analyticOrderAt f z₀ = ↑n + 1 ↔ analyticOrderAt (deriv f) z₀ = ↑n
-- Aesop.Forward.PremiseIndex
Aesop.PremiseIndex.toNat : Aesop.PremiseIndex → ℕ
-- Mathlib.Tactic.TermCongr
Mathlib.Tactic.TermCongr.CongrType.heq.sizeOf_spec : sizeOf Mathlib.Tactic.TermCongr.CongrType.heq = 1
-- Mathlib.Algebra.Group.Equiv.Basic
Equiv.neg_apply : ∀ (G : Type u_14) [inst : InvolutiveNeg G], ⇑(Equiv.neg G) = Neg.neg
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHAddOffset_6 : HAdd Std.Time.Timestamp Std.Time.Nanosecond.Offset Std.Time.Timestamp
-- Init.Data.Int.DivMod.Bootstrap
Int.dvd_mul_left : ∀ (a b : ℤ), b ∣ a * b
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.functor_map : ∀ (R : CommRingCat) {X Y : ModuleCat ↑R} (f : X ⟶ Y),
  (AlgebraicGeometry.tilde.functor R).map f = AlgebraicGeometry.tilde.map f
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] (x : E), HasFDerivAt id (ContinuousLinearMap.id 𝕜 E) x
-- Init.Data.Int.Order
Int.add_lt_add_of_le_of_lt : ∀ {a b c d : ℤ}, a ≤ b → c < d → a + c < b + d
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertList_distinct : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      (∀ (a : α), Std.Internal.List.containsKey a l = true → Std.Internal.List.containsKey a toInsert = false) →
        (Std.Internal.List.insertList l toInsert).length = l.length + toInsert.length
-- Mathlib.Topology.MetricSpace.Completion
UniformSpace.Completion.dist_triangle : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : UniformSpace.Completion α), dist x z ≤ dist x y + dist y z
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_of_subset_right : ∀ {α : Type u_1} {s t u : Multiset α}, t ⊆ u → Disjoint s u → Disjoint s t
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The `n`-th Fourier coefficient of a function `UnitAddTorus d → E`, for `E` a complete normed
`ℂ`-vector space, defined as the integral over `UnitAddTorus d` of `mFourier (-n) t • f t`.  -/
UnitAddTorus.mFourierCoeff : {d : Type u_1} →
  [Fintype d] → {E : Type u_2} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (UnitAddTorus d → E) → (d → ℤ) → E
-- Mathlib.Algebra.Order.CauSeq.BigOperators
IsCauSeq.of_abv : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β},
  (IsCauSeq abs fun m => ∑ n ∈ Finset.range m, abv (f n)) → IsCauSeq abv fun m => ∑ n ∈ Finset.range m, f n
-- Mathlib.Tactic.ClickSuggestions.FindPremises
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.computeImportDiscrTrees.setIfNone : {α : Type} → IO.Ref (Option α) → α → BaseIO Unit
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_bot : ∀ {α : Type u_1} [inst : LE α], ↑⊥ = Set.univ
-- Mathlib.Topology.Algebra.Algebra
Subsemiring.topologicalClosure.congr_simp : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [inst_2 : IsSemitopologicalSemiring R]
  (s s_1 : Subsemiring R), s = s_1 → s.topologicalClosure = s_1.topologicalClosure
-- Mathlib.Data.Sym.Basic
Sym.map_congr : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f g : α → β} {s : Sym α n}, (∀ x ∈ s, f x = g x) → Sym.map f s = Sym.map g s
-- Mathlib.LinearAlgebra.Dimension.Finite
rank_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  (∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n) → Module.rank R M ≤ ↑n
-- Init.Data.String.Slice
/-- If `pat` matches a suffix of `s`, returns the remainder. Returns `none` otherwise.

Use `String.Slice.dropSuffix` to return the slice
unchanged when `pat` does not match a suffix.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".toSlice.dropSuffix? " blue" == some "red green".toSlice`

* `"red green blue".toSlice.dropSuffix? "bluu " == none`

* `"red green blue".toSlice.dropSuffix? 'e' == some "red green blu".toSlice`

* `"red green blue".toSlice.dropSuffix? Char.isLower == some "red green blu".toSlice`
 -/
String.Slice.dropSuffix? : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Option String.Slice
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.map_g₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S T : J.Cover X} {I₁ I₂ : S.Arrow} (r : I₁.Relation I₂) (f : S ⟶ T), (r.map f).g₂ = r.g₂
-- Init.Prelude
/-- Get the current namespace in the file.  -/
Lean.Macro.Methods.getCurrNamespace : Lean.Macro.Methods → Lean.MacroM Lean.Name
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftMonoidWithZeroHom.congr_simp : ∀ {G₀ : Type u_1} {R : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : CommRing R] (φ φ_1 : Polynomial R →*₀ G₀)
  (e_φ : φ = φ_1) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)),
  RatFunc.liftMonoidWithZeroHom φ hφ = RatFunc.liftMonoidWithZeroHom φ_1 ⋯
-- Mathlib.Analysis.Convex.Function
ConcaveOn.left_le_of_le_right' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f →
    ∀ {x y : E},
      x ∈ s → y ∈ s → ∀ {a b : 𝕜}, 0 < a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ f y → f x ≤ f (a • x + b • y)
-- Mathlib.Topology.Category.Compactum
Compactum.instHasLimits : CategoryTheory.Limits.HasLimits Compactum
-- Init.Data.Float.Model.Format.Basic
Float.Model.Format.hm : ∀ (self : Float.Model.Format), 0 < self.mantissaBitsWithoutImplicit
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.range_coe : ∀ {α : Type u_1} [inst : Preorder α], Set.range WithTop.some = Set.Iio ⊤
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.sheafedSpace_toSheafedSpace : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [inst_1 : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace Y f.hom = X
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtype_symm_apply_apply_some : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β) (e : α ≃ { y // y ≠ x }) (a : α),
  ↑((Equiv.optionSubtype x).symm e) (some a) = ↑(e a)
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instNeg : {α : Type u} → [Neg α] → Neg (WithZero α)
-- Mathlib.MeasureTheory.Category.MeasCat
MeasCat.of.injEq : ∀ (carrier : Type u) [str : MeasurableSpace carrier] (carrier_1 : Type u) (str_1 : MeasurableSpace carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_nonempty : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support.Nonempty ↔ p ≠ 0
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the month to the given `month` value, with any
out-of-range days clipped to the nearest valid date.
 -/
Std.Time.PlainDateTime.withMonthClip : Std.Time.PlainDateTime → Std.Time.Month.Ordinal → Std.Time.PlainDateTime
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_add : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst_1 : Add β] [inst_2 : FunLike F α β]
  [AddHomClass F α β] (m : F) {s t : Set α}, ⇑m '' (s + t) = ⇑m '' s + ⇑m '' t
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The presubmersive presentation on `P.ModelOfHasCoeffs R₀` provided `P.HasCoeffs R₀`.  -/
Algebra.PreSubmersivePresentation.ofHasCoeffs : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              (P : Algebra.PreSubmersivePresentation R S ι σ) →
                (R₀ : Type u_5) →
                  [inst_3 : CommRing R₀] →
                    [inst_4 : Algebra R₀ R] →
                      [inst_5 : Algebra R₀ S] →
                        [inst_6 : IsScalarTower R₀ R S] →
                          [inst_7 : P.HasCoeffs R₀] →
                            Algebra.PreSubmersivePresentation R₀ (Algebra.Presentation.ModelOfHasCoeffs R₀) ι σ
-- Mathlib.RingTheory.Jacobson.Ring
Polynomial.isMaximal_comap_C_of_isMaximal : ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal] [IsJacobsonRing R] [Nontrivial R],
  (∀ (x : R), Polynomial.C x ∈ P → x = 0) → (Ideal.comap Polynomial.C P).IsMaximal
-- Mathlib.Order.Heyting.Hom
/-- Copy of a `BiheytingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
BiheytingHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : BiheytingAlgebra α] →
      [inst_1 : BiheytingAlgebra β] → (f : BiheytingHom α β) → (f' : α → β) → f' = ⇑f → BiheytingHom α β
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.instInhabitedId : {X : TopPair} → Inhabited (TopPair.Homotopy (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toArray_ensureTermination_eq_match_step : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toArray =
    match ↑it.step with
    | Std.IterStep.yield it' out => #[out] ++ it'.toArray
    | Std.IterStep.skip it' => it'.toArray
    | Std.IterStep.done => #[]
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_neg_left : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x y : M),
  QuadraticMap.polar (⇑Q) (-x) y = -QuadraticMap.polar (⇑Q) x y
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.monotone_rpow_of_nonneg : ∀ {z : ℝ}, 0 ≤ z → Monotone fun x => x ^ z
-- Init.Data.UInt.Lemmas
UInt16.lt_ofNat_iff : ∀ {n : UInt16} {m : ℕ}, m < UInt16.size → (n < UInt16.ofNat m ↔ n.toNat < m)
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.Config.mk.inj : ∀ {trace : Bool} {target : Lean.Name} {doc : Option (Lean.TSyntax `Lean.Parser.Command.docComment)}
  {allowAutoName : Bool} {reorder? : Option Mathlib.Tactic.Translate.ArgReorder}
  {relevantArg? : Option Mathlib.Tactic.Translate.RelevantArg} {attrs : Array Lean.Syntax} {dontTranslate : List ℕ}
  {ref : Lean.Syntax} {existing self none : Bool} {rename : Lean.NameMap Lean.Name} {trace_1 : Bool}
  {target_1 : Lean.Name} {doc_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)} {allowAutoName_1 : Bool}
  {reorder?_1 : Option Mathlib.Tactic.Translate.ArgReorder}
  {relevantArg?_1 : Option Mathlib.Tactic.Translate.RelevantArg} {attrs_1 : Array Lean.Syntax}
  {dontTranslate_1 : List ℕ} {ref_1 : Lean.Syntax} {existing_1 self_1 none_1 : Bool}
  {rename_1 : Lean.NameMap Lean.Name},
  { trace := trace, target := target, doc := doc, allowAutoName := allowAutoName, reorder? := reorder?,
        relevantArg? := relevantArg?, attrs := attrs, dontTranslate := dontTranslate, ref := ref, existing := existing,
        self := self, none := none, rename := rename } =
      { trace := trace_1, target := target_1, doc := doc_1, allowAutoName := allowAutoName_1, reorder? := reorder?_1,
        relevantArg? := relevantArg?_1, attrs := attrs_1, dontTranslate := dontTranslate_1, ref := ref_1,
        existing := existing_1, self := self_1, none := none_1, rename := rename_1 } →
    trace = trace_1 ∧
      target = target_1 ∧
        doc = doc_1 ∧
          allowAutoName = allowAutoName_1 ∧
            reorder? = reorder?_1 ∧
              relevantArg? = relevantArg?_1 ∧
                attrs = attrs_1 ∧
                  dontTranslate = dontTranslate_1 ∧
                    ref = ref_1 ∧ existing = existing_1 ∧ self = self_1 ∧ none = none_1 ∧ rename = rename_1
-- Mathlib.Data.Stream.Init
Stream'.take_prefix_take_left : ∀ {α : Type u} (m n : ℕ) (a : Stream' α), m ≤ n → Stream'.take m a <+: Stream'.take n a
-- Init.Data.SInt.Lemmas
ISize.toInt8_sub : ∀ (a b : ISize), (a - b).toInt8 = a.toInt8 - b.toInt8
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜}, DifferentiableOn 𝕜 (⇑f) s
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.liminf_const_sub : ∀ {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) {c : ENNReal},
  c ≠ ⊤ → Filter.liminf (fun i => c - f i) F = c - Filter.limsup f F
-- Mathlib.Data.Sigma.Order
Sigma.mk_lt_mk_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LT (α i)] {i : ι} {a b : α i}, ⟨i, a⟩ < ⟨i, b⟩ ↔ a < b
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_add_atTop : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.mkOfSucc_subinterval_eq : ∀ {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin l),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.mkOfSucc i) (SimplexCategory.subinterval j l hjl) =
    SimplexCategory.mkOfSucc ⟨j + ↑i, ⋯⟩
-- Mathlib.Geometry.Manifold.Immersion
_private.Mathlib.Geometry.Manifold.Immersion.0.Manifold.IsImmersionAt.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] (I : ModelWithCorners 𝕜 E H)
  (J : ModelWithCorners 𝕜 E'' G) {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) (x : M),
  Manifold.IsImmersionAt I J n f x = ∃ F x_1 x_2, Manifold.IsImmersionAtOfComplement F I J n f x
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.algebraMap_toCompletion : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (R : Type u_2) [inst_1 : CommSemiring R]
  [inst_2 : Algebra R (WithAbs ↑v)] [inst_3 : UniformContinuousConstSMul R (WithAbs ↑v)] (r : R),
  ((algebraMap R v.Completion) r).toCompletion = (algebraMap R (↑v).Completion) r
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.fg_unit : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : (FractionalIdeal S P)ˣ), (↑↑I).FG
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_inter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.inter! m₂) = true},
  Std.DTreeMap.Internal.Impl.Const.get (m₁.inter! m₂) k h_contains = Std.DTreeMap.Internal.Impl.Const.get m₁ k ⋯
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMulActionOfMulActionHomClass.eq_1 : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Monoid R]
  [inst_5 : (i : ι) → MulAction R (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)],
  DirectLimit.instMulActionOfMulActionHomClass = { toSMul := DirectLimit.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.maxD fallback ∈ t
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
LinearIsometryEquiv.toMeasurableEquiv_symm : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : MeasurableSpace F] [inst_7 : BorelSpace F] (f : E ≃ₗᵢ[ℝ] F),
  f.symm.toMeasurableEquiv = f.toMeasurableEquiv.symm
-- Mathlib.Data.Set.Insert
Set.singleton_iff_unique_mem : ∀ {α : Type u_1} {s : Set α}, (∃ a, s = {a}) ↔ ∃! a, a ∈ s
-- Mathlib.Data.Prod.Lex
Prod.Lex.toLex_lt_toLex : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {x y : α × β},
  toLex x < toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic_source : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1),
  (stereographic hv).source = {⟨v, ⋯⟩}ᶜ
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
/-- Precompose a simplicial homotopy with a morphism of simplicial objects.  -/
CategoryTheory.SimplicialObject.Homotopy.precomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : CategoryTheory.SimplicialObject C} →
      {f g : X ⟶ Y} →
        CategoryTheory.SimplicialObject.Homotopy f g →
          {X' : CategoryTheory.SimplicialObject C} →
            (p : X' ⟶ X) →
              CategoryTheory.SimplicialObject.Homotopy (CategoryTheory.CategoryStruct.comp p f)
                (CategoryTheory.CategoryStruct.comp p g)
-- Mathlib.Algebra.FiniteSupport.Defs
Function.HasFiniteMulSupport.eq_1 : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (f : α → M),
  Function.HasFiniteMulSupport f = (Function.mulSupport f).Finite
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_inj : ∀ {a b : Ordinal.{u}}, ZFSet.vonNeumann a = ZFSet.vonNeumann b ↔ a = b