mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.Convolution
Finset.vadd_addConvolution_eq_addConvolution_neg_add : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (s x : G),
  (s +ᵥ A).addConvolution B x = A.addConvolution B (-s + x)
-- Mathlib.Order.Atoms
isCoatom_bot : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], IsCoatom ⊥
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'_mul : ∀ {α : Type u_1} (P Q : RegularExpression α), (P * Q).matches' = P.matches' * Q.matches'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], k ∉ m₁ → (m₁ \ m₂).get! k = default
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.toNormedSpace : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_4} →
      {F : Type u_5} →
        [inst : SeminormedAddCommGroup E] →
          [inst_1 : SeminormedAddCommGroup F] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NontriviallyNormedField 𝕜₂] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : NormedSpace 𝕜₂ F] →
                    {σ₁₂ : 𝕜 →+* 𝕜₂} →
                      [inst_6 : RingHomIsometric σ₁₂] →
                        {𝕜' : Type u_9} →
                          [inst_7 : NormedField 𝕜'] →
                            [inst_8 : NormedSpace 𝕜' F] → [SMulCommClass 𝕜₂ 𝕜' F] → NormedSpace 𝕜' (E →SL[σ₁₂] F)
-- Mathlib.Topology.Order.LowerUpperTopology
/-- `toLower` is the identity function to the `WithLower` of a type.  -/
Topology.WithLower.toLower : {α : Type u_1} → α ≃ Topology.WithLower α
-- Mathlib.Computability.Language
Language.one_add_kstar_mul_self_eq_kstar : ∀ {α : Type u_1} (l : Language α), 1 + KStar.kstar l * l = KStar.kstar l
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanCompIso_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospanCompIso F f g).app CategoryTheory.Limits.WalkingCospan.one =
    CategoryTheory.Iso.refl (((CategoryTheory.Limits.cospan f g).comp F).obj CategoryTheory.Limits.WalkingCospan.one)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.evalₗ_apply : ∀ {𝕜 : Type u_1} {α : Type u_3} (E : α → Type u_4) [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] (p : ENNReal) (i : α) (f : ↥(lp E p)),
  (lp.evalₗ E p i) f = ↑f i
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.rightHomologyIso_hom_comp_homologyι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  CategoryTheory.CategoryStruct.comp S.rightHomologyIso.hom S.homologyι = S.rightHomologyι
-- Mathlib.Algebra.Module.Rat
map_nnratCast_smul : ∀ {M : Type u_1} {M₂ : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] {F : Type u_3}
  [inst_2 : FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_4) (S : Type u_5)
  [inst_4 : DivisionSemiring R] [inst_5 : DivisionSemiring S] [inst_6 : Module R M] [inst_7 : Module S M₂] (c : ℚ≥0)
  (x : M), f (↑c • x) = ↑c • f x
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_le_of_injective : ∀ {α β : Type u} {f : α → β}, Function.Injective f → Cardinal.mk α ≤ Cardinal.mk β
-- Init.Data.SInt.Bitwise
Int64.and_zero : ∀ {a : Int64}, a &&& 0 = 0
-- Mathlib.Order.Basic
PartialOrder.toPreorder_injective_iff : ∀ {α : Type u_2} {a₁ a₂ : PartialOrder α}, a₁ = a₂ ↔ a₁.toPreorder = a₂.toPreorder
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
closedBall_add_closedBall : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ} [ProperSpace E],
  0 ≤ ε → 0 ≤ δ → ∀ (a b : E), Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α}, (a == b) = true → (a ∈ m ↔ b ∈ m)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_id_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (X : B × C),
  (CategoryTheory.CategoryStruct.id X).1 = CategoryTheory.CategoryStruct.id X.1
-- Mathlib.Topology.Connected.PathConnected
AddSubmonoid.pathComponentZero.eq_1 : ∀ (M : Type u_4) [inst : AddMonoid M] [inst_1 : TopologicalSpace M] [inst_2 : ContinuousAdd M],
  AddSubmonoid.pathComponentZero M = { carrier := pathComponent 0, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Order.Nucleus
/-- A nucleus is idempotent.  -/
NucleusClass.idempotent : ∀ {F : Type u_2} {X : Type u_3} {inst : SemilatticeInf X} {inst_1 : FunLike F X X} [self : NucleusClass F X] (x : X)
  (f : F), f (f x) ≤ f x
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.ModEq.sub_iff_left`. -/
AddCommGroup.ModEq.sub_left_cancel : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a₁ a₂ b₁ b₂ : G},
  a₁ ≡ b₁ [PMOD p] → a₁ - a₂ ≡ b₁ - b₂ [PMOD p] → a₂ ≡ b₂ [PMOD p]
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.tendsto_nhdsWithin_nhdsWithin : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {s : Set α} [inst_1 : PseudoEMetricSpace β] {f : α → β}
  {t : Set β} {a : α} {b : β},
  Filter.Tendsto f (nhdsWithin a s) (nhdsWithin b t) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
-- Mathlib.Probability.Process.Adapted
MeasureTheory.isStronglyProgressive_of_tendsto' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} {γ : Type u_4} [inst_2 : MeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β] (fltr : Filter γ) [fltr.NeBot] [fltr.IsCountablyGenerated]
  {U : γ → ι → Ω → β},
  (∀ (l : γ), MeasureTheory.IsStronglyProgressive f (U l)) →
    Filter.Tendsto U fltr (nhds u) → MeasureTheory.IsStronglyProgressive f u
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.val_neg : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : SubMulAction R M)
  (x : ↥p), ↑(-x) = -↑x
-- Mathlib.FieldTheory.PrimitiveElement
/-- Primitive element theorem for finite-dimensional extension of a finite field.  -/
Field.exists_primitive_element_of_finite_bot : ∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [Finite F]
  [FiniteDimensional F E], ∃ α, F⟮α⟯ = ⊤
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.lift_mapId : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (F : B ⥤q C)
  (x : CategoryTheory.FreeBicategory B),
  (CategoryTheory.FreeBicategory.lift F).mapId x =
    CategoryTheory.Iso.refl (CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.id x))
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instContinuousMapClass : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ContinuousMapClass (A →ₜ+ B) A B
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getD_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α fun x => β} {a : α} {fallback : β},
  Std.DHashMap.Internal.AssocList.getD a fallback l = Std.Internal.List.getValueD a l.toList fallback
-- Mathlib.Probability.Process.Adapted
MeasureTheory.StronglyAdapted.add : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u v : (i : ι) → Ω → β i}
  [inst_2 : (i : ι) → Add (β i)] [∀ (i : ι), ContinuousAdd (β i)],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.StronglyAdapted f v → MeasureTheory.StronglyAdapted f (u + v)
-- Lean.Meta.Tactic.Grind.EqResolution
Lean.Meta.Grind.TopSort.State.mk.injEq : ∀ (tempMark permMark : Std.HashSet Lean.Expr) (result : Array Lean.Expr) (tempMark_1 permMark_1 : Std.HashSet Lean.Expr)
  (result_1 : Array Lean.Expr),
  ({ tempMark := tempMark, permMark := permMark, result := result } =
      { tempMark := tempMark_1, permMark := permMark_1, result := result_1 }) =
    (tempMark = tempMark_1 ∧ permMark = permMark_1 ∧ result = result_1)
-- Mathlib.Algebra.BigOperators.Fin
finPiFinEquiv_apply : ∀ {m : ℕ} {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ↑(finPiFinEquiv f) = ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j)
-- Mathlib.RingTheory.Smooth.IntegralClosure
/-- [Stacks Tag 03GE](https://stacks.math.columbia.edu/tag/03GE) (without the generalization to arbitrary etale algebra) -/
mem_adjoin_map_integralClosure_of_isStandardEtale : ∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.IsStandardEtale R S] (a : TensorProduct R S B),
  IsIntegral S a → a ∈ Algebra.adjoin S ↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B))
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.functorialityCompFunctoriality`.

---

Functoriality is functorial.  -/
CategoryTheory.Limits.Cones.functorialityCompFunctoriality : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {E : Type u₅} →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} E] →
                (F : CategoryTheory.Functor J C) →
                  (G : CategoryTheory.Functor C D) →
                    (H : CategoryTheory.Functor D E) →
                      (CategoryTheory.Limits.Cone.functoriality F G).comp
                          (CategoryTheory.Limits.Cone.functoriality (F.comp G) H) ≅
                        CategoryTheory.Limits.Cone.functoriality F (G.comp H)
-- Std.Http.Protocol.H1.Config
/-- Maximum allowed total body size per message in bytes (default: 64 MiB).
This limit applies across all body framing modes. For chunked transfer encoding,
chunk-size lines (including extensions) and the trailer section also count toward
this limit, so the total wire bytes consumed by the body cannot exceed this value.
 -/
Std.Http.Protocol.H1.Config.maxBodySize : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
CompactConvergenceCLM.hasBasis_nhds_zero_of_basis : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F] {ι : Type u_7}
  {p : ι → Prop} {b : ι → Set F},
  (nhds 0).HasBasis p b → (nhds 0).HasBasis (fun Si => IsCompact Si.1 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
-- Init.Data.SInt.Lemmas
Int64.ofNat_int16ToNatClampNeg : ∀ (x : Int16), 0 ≤ x → Int64.ofNat x.toNatClampNeg = x.toInt64
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.sinZeta_neg : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.sinZeta (-a) s = -HurwitzZeta.sinZeta a s
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.valuation_isEquiv_inftyValuation_of_one_lt_valuation_X : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [inst_2 : DecidableEq (RatFunc K)] [Valuation.IsTrivialOn K v],
  1 < v RatFunc.X → v.IsEquiv (RatFunc.inftyValuation K)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_throw_OptionT_apply : ∀ {Pred : Type u} {EPred : Type u_1} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ Pred EPred} (err : PUnit.{u_2 + 1}),
  Lean.Order.PartialOrder.rel epost.head (Std.Internal.Do.wp (MonadExceptOf.throw err) post epost)
-- Mathlib.CategoryTheory.IsoCat
/-- The inverse functor of an isomorphism of categories.  -/
CategoryTheory.IsoCat.inverse : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.IsoCat C D → CategoryTheory.Functor D C
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- The identity morphism in `SingleFunctors C D A`.  -/
CategoryTheory.SingleFunctors.Hom.id : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] → (F : CategoryTheory.SingleFunctors C D A) → F.Hom F
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.sumElimCategory : {I : Type w₀} →
  (C : I → Type u₁) →
    [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type w₀} →
        {D : J → Type u₁} →
          [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] →
            (s : I ⊕ J) → CategoryTheory.Category.{v₁, u₁} (Sum.elim C D s)
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element that is greater than or equal to the
given element, returning `fallback` if no such element exists.
 -/
Std.TreeSet.Raw.getGED : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → α → α
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.map_subtype_range_inclusion : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M} (h : p ≤ p'), Submodule.map p'.subtype (Submodule.inclusion h).range = p
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.minEntry!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minEntry! = t₂.minEntry!
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.absolutelyContinuous_restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  (μ.restrict s).AbsolutelyContinuous μ
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `FunLike.coe_zero`. -/
NonarchAddGroupSeminorm.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Init.Data.List.Nat.Range
List.mem_range : ∀ {m n : ℕ}, m ∈ List.range n ↔ m < n
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α]
  [CompleteSpace α] {f : β × γ → α}, Multipliable f → Multipliable fun b => ∏' (c : γ), f (b, c)
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_le_coe : ∀ {a : ℝ} {b : NNReal}, ENNReal.ofReal a ≤ ↑b ↔ a ≤ ↑b
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- Given a limit cone over the underlying modules, equipping the cone point with
the induced topology gives a limit cone in `TopModuleCat R`.  -/
TopModuleCat.isLimit : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {J : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_1, u_2} J] →
          {F : CategoryTheory.Functor J (TopModuleCat R)} →
            {c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))} →
              CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsLimit (TopModuleCat.ofCone c)
-- Mathlib.Topology.Sheaves.Sheafify
/-- The natural morphism from the stalk of the sheafification to the original stalk.
In `sheafifyStalkIso` we show this is an isomorphism.
 -/
TopCat.Presheaf.stalkToFiber : {X : TopCat} → (F : TopCat.Presheaf (Type v) X) → (x : ↑X) → F.sheafify.presheaf.stalk x ⟶ F.stalk x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass.0.CategoryTheory.ShortComplex.ShortExact.termHqis : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_add : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {g g' : M → F} {x : M}, MDiffAt g x → MDiffAt g' x → d% (g + g') x = d% g x + d% g' x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_union!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
  (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₁ = false) {h' : k ∈ m₁.union! m₂},
  (m₁.union! m₂).get k h' = m₂.get k ⋯
-- Mathlib.Algebra.Order.Monovary
Antivary.pow_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g : ι → β}, Antivary f g → ∀ (n : ℕ), Antivary f (g ^ n)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.ε_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {X Y : C}
  (f : X ⟶ Y) [inst_3 : F.LaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.ε F).app X)
      ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).map f) =
    CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Functor.LaxMonoidal.ε F).app Y)
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The functor `fun X ↦ 𝟙_ C ⊗ X`.  -/
CategoryTheory.MonoidalCategory.tensorUnitLeft : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor C C
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldr_eq_foldr_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {f : α → β → δ → δ}
  {init : δ}, Std.TreeMap.foldr f init t = Array.foldr (fun a b => f a.1 a.2 b) init t.toArray
-- Mathlib.Order.Minimal
exists_minimal_le_of_wellFoundedLT : ∀ {α : Type u_2} [inst : Preorder α] [WellFoundedLT α] (P : α → Prop) (a : α), P a → ∃ b ≤ a, Minimal P b
-- Mathlib.Algebra.Colimit.Module
/-- Consider direct limits `lim G` and `lim G'` with direct system `f` and `f'` respectively, any
family of equivalences `eᵢ : Gᵢ ≅ G'ᵢ` such that `e ∘ f = f' ∘ e` induces an equivalence
`lim G ⟶ lim G'`.
 -/
AddCommGroup.DirectLimit.congr : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      [inst_1 : (i : ι) → AddCommMonoid (G i)] →
        {f : (i j : ι) → i ≤ j → G i →+ G j} →
          [inst_2 : DecidableEq ι] →
            {G' : ι → Type u_5} →
              [inst_3 : (i : ι) → AddCommMonoid (G' i)] →
                {f' : (i j : ι) → i ≤ j → G' i →+ G' j} →
                  (e : (i : ι) → G i ≃+ G' i) →
                    (∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)) →
                      AddCommGroup.DirectLimit G f ≃+ AddCommGroup.DirectLimit G' f'
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_getElem_utf8EncodeChar_two_of_utf8Size_eq_four : ∀ {c : Char} (hc : c.utf8Size = 4),
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte (String.utf8EncodeChar c)[2] = false
-- Mathlib.Topology.Sets.VietorisTopology
IsCompact.powerset_vietoris : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : Set α}, IsCompact K → IsCompact (𝒫 K)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.swap_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (i : A × B), (ContinuousAddMonoidHom.swap A B) i = (i.2, i.1)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_ofAdd_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0),
  a < ↑(Multiplicative.ofAdd b) ↔ Multiplicative.toAdd (WithZero.unzero ha) < b
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- Right multiplication by `g`. It is meant to mimic the usual notation in Lie groups.
Used mostly through the notation `𝑹`.
Lemmas involving `smoothRightMul` with the notation `𝑹` usually use `R` instead of `𝑹` in the
names.  -/
LieGroup.«term𝑹» : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion at `x`, its domain chart's target `(h.domChart.extend I).target`
is mapped to it codomain chart's target `(h.domChart.extend J).target`:
see `image_target_subset_target` for a version stated using images.  -/
Manifold.IsSubmersionAt.target_subset_preimage_target : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x),
  (h.domChart.extend I).target ⊆ Prod.fst ∘ ⇑h.equiv ⁻¹' (h.codChart.extend J).target
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- Construct an isomorphism of spans from components.  -/
CategoryTheory.Limits.spanExt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z X' Y' Z' : C} →
      (iX : X ≅ X') →
        (iY : Y ≅ Y') →
          (iZ : Z ≅ Z') →
            {f : X ⟶ Y} →
              {g : X ⟶ Z} →
                {f' : X' ⟶ Y'} →
                  {g' : X' ⟶ Z'} →
                    CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom →
                      CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom →
                        (CategoryTheory.Limits.span f g ≅ CategoryTheory.Limits.span f' g')