mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangle : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b),
  CategoryTheory.Bicategory.leftZigzag η ε =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
        (CategoryTheory.Bicategory.rightUnitor f).inv →
    CategoryTheory.bicategoricalComp (CategoryTheory.Bicategory.rightZigzag η ε)
        (CategoryTheory.Bicategory.rightZigzag η ε) =
      CategoryTheory.Bicategory.rightZigzag η ε
-- Mathlib.Data.Set.Finite.Basic
Set.finite_range_const : ∀ {α : Type u} {β : Type v} {c : β}, (Set.range fun x => c).Finite
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Clz
Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {curr w : ℕ} (aig : Std.Sat.AIG α) (acc xc : aig.RefVec w)
  (x : BitVec w) (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := xc.get idx hidx }⟧ = x.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w),
        if curr = 0 then ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (BitVec.ofNat w w).getLsbD idx
        else ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (x.clzAuxRec (curr - 1)).getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go aig xc curr acc).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go aig xc curr acc).vec.get idx hidx }⟧ =
          (x.clzAuxRec (w - 1)).getLsbD idx
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.mem_map_equiv : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G ≃* N} {K : Subgroup G} {x : N},
  x ∈ Subgroup.map f.toMonoidHom K ↔ f.symm x ∈ K
-- Mathlib.Data.Set.Enumerate
/-- Given a choice function `sel`, enumerates the elements of a set in the order
`a 0 = sel s`, `a 1 = sel (s \ {a 0})`, `a 2 = sel (s \ {a 0, a 1})`, ... and stops when
`sel (s \ {a 0, ..., a n}) = none`. Note that we don't require `sel` to be a choice function.  -/
Set.enumerate : {α : Type u_1} → (Set α → Option α) → Set α → ℕ → Option α
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.getSimpExtension? : Lean.Name → Lean.CoreM (Option Lean.Meta.SimpExtension)
-- Mathlib.Order.Heyting.Basic
/-- `p → p`  -/
himp_self : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a : α}, a ⇨ a = ⊤
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_centralizer_centralizer : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (s : Set A),
  ↑(StarSubalgebra.centralizer R ↑(StarSubalgebra.centralizer R s)) = (s ∪ star s).centralizer.centralizer
-- Plausible.Testable
Plausible.TestResult.gaveUp.inj : ∀ {p : Prop} {a a_1 : ℕ}, Plausible.TestResult.gaveUp a = Plausible.TestResult.gaveUp a_1 → a = a_1
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.mem_polar_singleton : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {a : E} (y : StrongDual 𝕜 E),
  y ∈ StrongDual.polar 𝕜 {a} ↔ ‖y a‖ ≤ 1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_neg_add_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α],
  a - b ≤ -a + b ↔ a ≤ b
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.mk_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X),
  (CategoryTheory.Pretriangulated.Triangle.mk f g h).obj₁ = X
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- The essential (i.e. finite codimensional) part of a Fredholm decomposition.  -/
FredholmDecomposition.X₁ : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] → [inst_3 : TopologicalSpace E] → FredholmDecomposition 𝕜 E → Submodule 𝕜 E
-- Mathlib.Data.Multiset.Filter
Multiset.Nodup.erase_eq_filter : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) {s : Multiset α},
  s.Nodup → s.erase a = Multiset.filter (fun x => x ≠ a) s
-- Init.System.IOError
IO.Error.mkInvalidArgumentFile : String → UInt32 → String → IO.Error
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsCofibrantResolutionObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C),
  HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj X)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- A submodule containing `1` and closed under multiplication is a subalgebra.  -/
Submodule.toSubalgebra : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] → (p : Submodule R A) → 1 ∈ p → (∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) → Subalgebra R A
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_eq_starClosure_adjoin : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (s : Set A),
  StarAlgebra.adjoin R s = (Algebra.adjoin R s).starClosure
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.mk.sizeOf_spec : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} [inst_3 : SizeOf N] [inst_4 : SizeOf E] [inst_5 : SizeOf G] (toMonoidHom : G →* E)
  (rightInverse_rightHom : Function.RightInverse (↑toMonoidHom).toFun ⇑S.rightHom),
  sizeOf { toMonoidHom := toMonoidHom, rightInverse_rightHom := rightInverse_rightHom } = 1 + sizeOf toMonoidHom
-- Std.Data.TreeSet.Lemmas
/-- This is a restatement of `mem_of_mem_insert` that is written to exactly match the
proof obligation in the statement of `get_insert`.  -/
Std.TreeSet.mem_of_mem_insert' : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a : α},
  a ∈ t.insert k → ¬(cmp k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `L` with the spectral norm is a `NormedField`.  -/
spectralNorm.normedField : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    (L : Type v) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Algebra.IsAlgebraic K L] → [hu : IsUltrametricDist K] → [CompleteSpace K] → NormedField L
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_lt_iff_lt_right : ∀ {a b c : ENNReal}, b ≠ ⊤ → b ≤ a → (a - b < c ↔ a < c + b)
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- A `GuessLexRel` described how a recursive call affects a measure; whether it
decreases strictly, non-strictly, is equal, or else.   -/
Lean.Elab.WF.GuessLex.GuessLexRel : Type
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
ClassGroup.extendedHom_quotientMk : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Module.IsTorsionFree A B] [inst_4 : IsDomain A] [inst_5 : IsDomain B]
  (α : (FractionalIdeal (nonZeroDivisors A) (FractionRing A))ˣ),
  (ClassGroup.extendedHom A B) ↑α = ↑((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) α)
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The underlying predicate of a prelocal predicate  -/
TopCat.PrelocalPredicate.pred : {X : TopCat} →
  {T : ↑X → Type u_1} → TopCat.PrelocalPredicate T → {U : TopologicalSpace.Opens ↑X} → ((x : ↥U) → T ↑x) → Prop
-- Aesop.Rule
Aesop.instLTSafeRuleInfo : LT Aesop.SafeRuleInfo
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- If the expression is a candidate for app unexpanders,
try applying an app unexpander using some prefix of the arguments, longest prefix first.
This function makes sure that the unexpanded syntax is annotated and given TermInfo so that it is hoverable in the InfoView.

Ref logic:
1. The unexpanders are run with the head constant's syntax as the ref.
2. If `pp.tagAppFns` is false, then this does nothing, since `delabConst` won't register any terminfo for the constant.
3. If `pp.tagAppFns` is true, then this causes all tokens in app unexpanders to refer to the head constant.
   The effect is that in docgen, every token will be linkified (supposing the app unexpander uses syntax quotations).
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.tryAppUnexpanders : Lean.Term → Array Lean.PrettyPrinter.Delaborator.AppImplicitArg → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Data.List.Induction
/-- Like `bidirectionalRec`, but with the list parameter placed first.  -/
List.bidirectionalRecOn : {α : Type u_1} →
  {C : List α → Sort u_2} →
    (l : List α) → C [] → ((a : α) → C [a]) → ((a : α) → (l : List α) → (b : α) → C l → C (a :: (l ++ [b]))) → C l
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map_add : ∀ {α β : Type u} (f : α → β) (x y : FreeAddGroup α), f <$> (x + y) = f <$> x + f <$> y
-- Lean.Parser.Types
Lean.Parser.instInhabitedParser.default : Lean.Parser.Parser
-- Mathlib.Order.Comparable
incompRel_compl : ∀ {α : Type u_1} (r : α → α → Prop), IncompRel rᶜ = AntisymmRel r
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `G` be a complete nonarchimedean multiplicative abelian group, and let `f : α → G` be a
function that tends to one on the filter of cofinite sets. Then `f` is unconditionally
multipliable.  -/
NonarchimedeanGroup.multipliable_of_tendsto_cofinite_one : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : UniformSpace G] [IsUniformGroup G]
  [NonarchimedeanGroup G] [CompleteSpace G] {f : α → G}, Filter.Tendsto f Filter.cofinite (nhds 1) → Multipliable f
-- Mathlib.Analysis.Normed.Ring.Basic
Pi.normOneClass : ∀ {ι : Type u_5} {α : ι → Type u_6} [Nonempty ι] [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (α i)]
  [inst_2 : (i : ι) → One (α i)] [∀ (i : ι), NormOneClass (α i)], NormOneClass ((i : ι) → α i)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.ext_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {F G : f₀.Homotopy f₁}, F = G ↔ ∀ (x : ↑unitInterval × X), F x = G x
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.exs.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (x_1 : L.BoundedFormula α x),
  x_1.exs =
    match x, x_1 with
    | 0, φ => φ
    | _n.succ, φ => φ.ex.exs
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      k ∈ Std.DTreeMap.Raw.Const.insertMany t l ↔ k ∈ t ∨ (List.map Prod.fst l).contains k = true
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.mul_lt_sin : ∀ {x : ℝ}, 0 < x → x < Real.pi / 2 → 2 / Real.pi * x < Real.sin x
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.Eqv.of_smul : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (x : DecidableEq ι) (r : R) (f : (i : ι) → s i) (i : ι) (r' : R),
  PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, Function.update f i (r' • f i))) (FreeAddMonoid.of (r' * r, f))
-- Mathlib.LinearAlgebra.Dimension.Free
/-- The `finrank` of a free module `M` over `R` is the cardinality of `ChooseBasisIndex R M`.  -/
Module.finrank_eq_card_chooseBasisIndex : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [StrongRankCondition R] [inst_5 : Module.Finite R M],
  Module.finrank R M = Fintype.card (Module.Free.ChooseBasisIndex R M)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The fork associated to a pre-`0`-hypercover induced by taking the coproduct of the
components.  -/
CategoryTheory.PreOneHypercover.forkOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
        {S : C} →
          (E : CategoryTheory.PreOneHypercover S) →
            {c : CategoryTheory.Limits.Cofan E.X} →
              CategoryTheory.Limits.IsColimit c →
                {d : CategoryTheory.Limits.Cofan E.Y'} →
                  (hd : CategoryTheory.Limits.IsColimit d) →
                    (F : CategoryTheory.Functor Cᵒᵖ A) →
                      CategoryTheory.Limits.Fork
                        (F.map
                          (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x =>
                              CategoryTheory.CategoryStruct.comp (E.p₁ x.snd) (c.inj x.fst.1)).op)
                        (F.map
                          (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x =>
                              CategoryTheory.CategoryStruct.comp (E.p₂ x.snd) (c.inj x.fst.2)).op)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_sum_right : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ι' : Type u_4} [Countable ι']
  (m : MeasureTheory.Measure α) (m' : ι' → MeasureTheory.Measure β) [∀ (n : ι'), MeasureTheory.SFinite (m' n)],
  m.prod (MeasureTheory.Measure.sum m') = MeasureTheory.Measure.sum fun p => m.prod (m' p)
-- Mathlib.Data.Set.Card
Set.ncard_le_card : ∀ {α : Type u_1} [Finite α] (s : Set α), s.ncard ≤ Nat.card α
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_op_apply : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A)
  (p : Polynomial R), (Polynomial.aeval (MulOpposite.op x)) p = MulOpposite.op ((Polynomial.aeval x) p)
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryGED : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → α × β → α × β
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.eval_getLsbD : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {a : ℕ} {expr : Std.Tactic.BVDecide.BVExpr a} {idx : ℕ},
  Std.Tactic.BVDecide.BVPred.eval assign (Std.Tactic.BVDecide.BVPred.getLsbD expr idx) =
    (Std.Tactic.BVDecide.BVExpr.eval assign expr).getLsbD idx
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_symmDiff_eq : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    MeasurableSet t →
      autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_symmDiff_eq._auto_1 →
        autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_symmDiff_eq._auto_3 →
          μ.real (symmDiff s t) = μ.real (s \ t) + μ.real (t \ s)
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Ioc_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] {p : α},
  0 < p → ⋃ n, Set.Ioc (n • p) ((n + 1) • p) = Set.univ
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.coeFn_toFiniteMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω), ⇑μ.toFiniteMeasure = ⇑μ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_diff_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₁ \ m₂ ↔ k ∈ m₁ ∧ k ∉ m₂
-- Mathlib.Tactic.Linarith.Preprocessing
Mathlib.Tactic.Linarith.without_one_mul : ∀ {M : Type u_1} [inst : MulOneClass M] {a b : M}, 1 * a = b → a = b
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.diffₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] →
      [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Tactic.LinearCombination.Lemmas
/-- Given an (in)equality, look up the lemma to divide it by a constant.  If relevant, also take
into account the degree of positivity which can be proved of the constant: strict or non-strict.  -/
Mathlib.Ineq.divRelConstData : Mathlib.Ineq.WithStrictness → Lean.Name
-- Std.Time.DateTime.PlainDateTime
/-- Converts a `PlainDateTime` to a `WallTime`.
 -/
Std.Time.PlainDateTime.toWallTime : Std.Time.PlainDateTime → Std.Time.WallTime
-- Mathlib.Algebra.Lie.Solvable
/-- A Lie algebra is solvable if its derived series reaches 0 (in a finite number of steps).  -/
LieAlgebra.IsSolvable : (L : Type v) → [LieRing L] → Prop
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
UniqueMDiffOn.prod : ∀ {𝕜 : 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} {t : Set M'},
  UniqueMDiff[s] → UniqueMDiff[t] → UniqueMDiff[s ×ˢ t]
-- Init.Data.Range.Polymorphic.Char
Char.instIsAlwaysFinite_2 : Std.Rxi.IsAlwaysFinite Char
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp (t.minKey ⋯) k).isLE = true
-- Init.Data.UInt.Lemmas
UInt64.ofNatTruncate_uSizeToNat : ∀ (n : USize), UInt64.ofNatClamp n.toNat = n.toUInt64
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A version of `CostructuredArrow.ofDiagEquivalence` with the roles of the first and second
projection swapped.  -/
CategoryTheory.CostructuredArrow.ofDiagEquivalence' : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T × T) →
      CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X ≌
        CategoryTheory.CostructuredArrow (CategoryTheory.Over.forget X.2) X.1
-- Mathlib.Analysis.Convolution
BddAbove.continuous_convolution_left_of_integrable : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [inst_12 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] [FirstCountableTopology G] [SecondCountableTopologyEither G E],
  BddAbove (Set.range fun x => ‖f x‖) →
    Continuous f → MeasureTheory.Integrable g μ → Continuous (MeasureTheory.convolution f g L μ)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.Context.macroStack : Lean.Elab.Term.Context → Lean.Elab.MacroStack
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedPreElabHeaderResult.default : Lean.Elab.Command.PreElabHeaderResult
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.pushIdent : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instSemiring : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] → [IsOrderedCancelAddMonoid Γ] → [inst : Semiring R] → Semiring (HahnSeries Γ R)
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
_private.Mathlib.Combinatorics.Extremal.RuzsaSzemeredi.0.instExplicitDisjointTriangleIndices : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : CommRing α] {s : Finset α} [Fact (IsUnit 2)],
  SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint (triangleIndices✝ s)
-- Mathlib.Topology.Category.Born
/-- The underlying bornology.  -/
Born.carrier : Born → Type u_1
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- Pulling back through `extChartAt` the scalar multiplication of a vector field by
the derivative of a scalar function equals the scalar multiplication by the manifold derivative.  -/
VectorField.mpullback_mfderivWithin_apply_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x}
  [IsManifold I 2 M] {f : M → 𝕜},
  MDiffAt[s] f x →
    have V' := VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I);
    have W' := VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) W (Set.range ↑I);
    VectorField.mpullback I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x))
        (fun x₀ =>
          (fderivWithin 𝕜 (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) x₀) (V' x₀) •
            W' x₀)
        x =
      (mfderiv[s] f x) (V x) • W x
-- Aesop.Tree.Free
_private.Aesop.Tree.Free.0.Aesop.freeMVarClusterRef : Aesop.GoalRef → Aesop.MVarClusterRef → Aesop.MVarClusterRef → BaseIO Unit
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_addMonoidHom_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β] (f : α → β)
  (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0)
  (h₃ :
    ∀ (x y : α),
      { toFun := f, map_mul' := h₁ }.toFun (x + y) =
        { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y),
  ↑{ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_zero' := h₂, map_add' := h₃ }
-- Mathlib.Order.Atoms
OrderIso.isAtom_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] (f : α ≃o β) (a : α), IsAtom (f a) ↔ IsAtom a
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.comap_mono : ∀ {α : Type u_1} {β : Type u_3} (f : α → β), Monotone ⇑(MeasureTheory.OuterMeasure.comap f)
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
/-- For a field `K`, the group `GL(2, K)` acts on `OnePoint K`, via the canonical identification
with the `ℙ¹(K)` (which is given explicitly by Möbius transformations).  -/
OnePoint.instGLAction : {K : Type u_1} → [inst : Field K] → [DecidableEq K] → MulAction (GL (Fin 2) K) (OnePoint K)
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- The adjugate map of the sylvester map. It takes `P` to `(p, q)` such that
`f * q + g * p = Res(f, g) * P`.  -/
Polynomial.adjSylvester : {m n : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] →
      Polynomial R →
        Polynomial R → ↥(Polynomial.degreeLT R (m + n)) →ₗ[R] ↥(Polynomial.degreeLT R m) × ↥(Polynomial.degreeLT R n)
-- Mathlib.Topology.MetricSpace.CauSeqFilter
CauchySeq.isCauSeq : ∀ {β : Type v} [inst : NormedField β] {f : ℕ → β}, CauchySeq f → IsCauSeq norm f
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux_inv : ∀ {n : ℕ} (f : Equiv.Perm (Fin n)), f⁻¹.signAux = f.signAux
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.one_nonempty : ∀ {α : Type u_2} [inst : One α], Set.Nonempty 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ},
  t.WF →
    ((Std.DTreeMap.Raw.filterMap f t).isEmpty = false ↔
      ∃ k, ∃ (h : k ∈ t), (f (t.getKey k h) (Std.DTreeMap.Raw.Const.get t k h)).isSome = true)