mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.MongePoint
/-- Two simplices with the same points have the same Monge point.  -/
Affine.Simplex.mongePoint_eq_of_range_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} {s₁ s₂ : Affine.Simplex ℝ P n},
  Set.range s₁.points = Set.range s₂.points → s₁.mongePoint = s₂.mongePoint
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.order_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R} [inst_2 : Zero Γ],
  r ≠ 0 → ((HahnSeries.single a) r).order = a
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.zeroX.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (F : FormalGroup R),
  F.zeroX = MvPowerSeries.subst ![0, PowerSeries.X] F.toPowerSeries
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Complex.hasStrictFDerivAt_exp_real : ∀ (x : ℂ), HasStrictFDerivAt Complex.exp (Complex.exp x • 1) x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow.eq_2 : ∀ (n : ℕ) (r : ℝ) (basis_hd : ℝ → ℝ) (basis_tl : List (ℝ → ℝ)),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow (basis_hd :: basis_tl) n r =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow basis_hd basis_tl n r)
      ((basis_hd :: basis_tl)[n]! ^ r)
-- Lean.AuxRecursor
Lean.isRecOnRecursor : Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.Algebra.Hom
AlgHom.ofLinearMap_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1)
  (map_mul : ∀ (x y : A), f (x * y) = f x * f y) (a : A), (AlgHom.ofLinearMap f map_one map_mul) a = f a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
/-- The cocone for `R ⋙ forget _ ⊗ M.presheaf ⋙ forget _` with point
`ModuleColimit hcR hcM` which allows to define the scalar multiplication
by `cR.pt` on `ModuleColimit hcR hcM`.  -/
PresheafOfModules.ModuleColimit.coconeSMul : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {cR : CategoryTheory.Limits.Cocone R} →
        CategoryTheory.Limits.IsColimit cR →
          {M : PresheafOfModules R} →
            {cM : CategoryTheory.Limits.Cocone M.presheaf} →
              CategoryTheory.Limits.IsColimit cM →
                CategoryTheory.Limits.Cocone
                  (CategoryTheory.MonoidalCategoryStruct.tensorObj (R.comp (CategoryTheory.forget RingCat))
                    (M.presheaf.comp (CategoryTheory.forget Ab)))
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidate.mk.inj : ∀ {group : Lean.Elab.Structural.IndGroupInst} {comb : Array Lean.Elab.Structural.RecArgInfo}
  {group_1 : Lean.Elab.Structural.IndGroupInst} {comb_1 : Array Lean.Elab.Structural.RecArgInfo},
  { group := group, comb := comb } = { group := group_1, comb := comb_1 } → group = group_1 ∧ comb = comb_1
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.right' : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f g : a ⟶ b) →
        [CategoryTheory.BicategoricalCoherence f g] →
          CategoryTheory.BicategoricalCoherence f
            (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b))
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- For a ring hom `f : R →+* S` and a prime ideal `J` in `S`, the induced ring hom from the
localization of `R` at `J.comap f` to the localization of `S` at `J`.

To make this definition more flexible, we allow any ideal `I` of `R` as input, together with a proof
that `I = J.comap f`. This can be useful when `I` is not definitionally equal to `J.comap f`.
 -/
Localization.localRingHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    {P : Type u_3} →
      [inst_1 : CommSemiring P] →
        (I : Ideal R) →
          [hI : I.IsPrime] →
            (J : Ideal P) →
              [inst_2 : J.IsPrime] →
                (f : R →+* P) → I = Ideal.comap f J → Localization.AtPrime I →+* Localization.AtPrime J
-- Init.Data.UInt.Lemmas
USize.ofNatTruncate_finVal : ∀ (n : Fin USize.size), USize.ofNatClamp ↑n = USize.ofFin n
-- Mathlib.Data.Int.Cast.Lemmas
Commute.self_intCast_mul : ∀ {α : Type u_3} [inst : Ring α] (a : α) (n : ℤ), Commute a (↑n * a)
-- Init.Data.String.Basic
String.Internal.toArray : String → Array Char
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : LinearMap.GeneralLinearGroup R M), ⇑((LinearMap.GeneralLinearGroup.generalLinearEquiv R M) f) = ⇑↑f
-- Init.Data.Nat.Lemmas
Nat.one_le_pow : ∀ (n m : ℕ), 0 < m → 1 ≤ m ^ n
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_map_iff : ∀ {α : Type u_1} {β : Type u_2} {n : Type u_3} {A : Matrix n n α} {f : α → β},
  Function.Injective f → ((A.map f).IsSymm ↔ A.IsSymm)
-- Lean.AuxRecursor
Lean.NoConfusionInfo.perCtor.inj : ∀ {arity fields arity_1 fields_1 : ℕ},
  Lean.NoConfusionInfo.perCtor arity fields = Lean.NoConfusionInfo.perCtor arity_1 fields_1 →
    arity = arity_1 ∧ fields = fields_1
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp_of_injective : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_1} [inst : L.Structure M] {N : Type u_2}
  [inst_1 : L.Structure N] {F : Type u_3} [inst_2 : FunLike F M N] {φ : L.BoundedFormula α n},
  φ.IsAtomic →
    ∀ [L.HomClass F M N] {f : F},
      Function.Injective ⇑f → ∀ {v : α → M} {xs : Fin n → M}, φ.Realize v xs → φ.Realize (⇑f ∘ v) (⇑f ∘ xs)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            h)
  (size : ℕ) (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β)
  (x_2 : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false),
  x = Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r →
    x_1 ≍ x_2 →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
        | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
          h_3 => h_2 size k v l size_1 k_1 v_1 l_1 r h r_1 h_3) ≍
        h_1 size k v r x_2
-- Mathlib.Data.Finset.Prod
Finset.product_inter_product : ∀ {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t t' : Finset β} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiffOn.div` -/
ContDiffOn.fun_div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {f g : E → 𝕜} {n : WithTop ℕ∞},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g s → (∀ x ∈ s, g x ≠ 0) → ContDiffOn 𝕜 n (fun i => f i / g i) s
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanIleanInfoParams : Lean.ToJson Lean.Lsp.LeanIleanInfoParams
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer.0.CategoryTheory.Limits.WalkingMultispan.instFinCategoryOfLOfDecidableEqR.match_4.eq_2 : ∀ {J : CategoryTheory.Limits.MultispanShape}
  (motive :
    (b : J.R) →
      (a : J.L) →
        (CategoryTheory.Limits.WalkingMultispan.left a ⟶ CategoryTheory.Limits.WalkingMultispan.right b) →
          J.fst a = b → J.snd a = b → Sort u_3)
  (a : J.L) (h₁ : J.fst a = J.snd a) (h₂ : J.snd a = J.snd a)
  (h_1 :
    (a : J.L) →
      (h₁ : J.fst a = J.fst a) →
        (h₂ : J.snd a = J.fst a) → motive (J.fst a) a (CategoryTheory.Limits.WalkingMultispan.Hom.fst a) h₁ h₂)
  (h_2 :
    (a : J.L) →
      (h₁ : J.fst a = J.snd a) →
        (h₂ : J.snd a = J.snd a) → motive (J.snd a) a (CategoryTheory.Limits.WalkingMultispan.Hom.snd a) h₁ h₂),
  (match J.snd a, a, CategoryTheory.Limits.WalkingMultispan.Hom.snd a, h₁, h₂ with
    | .(J.fst a), a, CategoryTheory.Limits.WalkingMultispan.Hom.fst .(a), h₁, h₂ => h_1 a h₁ h₂
    | .(J.snd a), a, CategoryTheory.Limits.WalkingMultispan.Hom.snd .(a), h₁, h₂ => h_2 a h₁ h₂) =
    h_2 a h₁ h₂
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_mul : ∀ (a b c : Ordinal.{u_1}), a ^ (b * c) = (a ^ b) ^ c
-- Mathlib.Logic.Function.Basic
Function.ne_iff : ∀ {α : Sort u_1} {β : α → Sort u_4} {f₁ f₂ : (a : α) → β a}, f₁ ≠ f₂ ↔ ∃ a, f₁ a ≠ f₂ a
-- Mathlib.Tactic.Polynomial.Core
_private.Mathlib.Tactic.Polynomial.Core.0.Mathlib.Tactic.Polynomial.mkPolynomialExt.unsafe_1 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Tactic.Polynomial.PolynomialExt
-- Mathlib.NumberTheory.Padics.PadicIntegers
/-- `unitCoeff hx` is the unit `u` in the unique representation `x = u * p ^ n`.
See `unitCoeff_spec`.  -/
PadicInt.unitCoeff : {p : ℕ} → [hp : Fact (Nat.Prime p)] → {x : ℤ_[p]} → x ≠ 0 → ℤ_[p]ˣ
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns true if the given key `a` is in the RBMap.  -/
RBTree.RBMap.contains : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → α → Bool
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_subset_closedBall' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ},
  ε₁ + dist x y ≤ ε₂ → Metric.closedBall x ε₁ ⊆ Metric.closedBall y ε₂
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- At an invertible element `x` of a normed division algebra `R`, the inversion is strictly
differentiable, with derivative the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. For a nicer formula in
the commutative case, see `hasStrictFDerivAt_inv`.  -/
hasStrictFDerivAt_inv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedDivisionRing R]
  [inst_2 : NormedAlgebra 𝕜 R] {x : R},
  x ≠ 0 → HasStrictFDerivAt Inv.inv (-((ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹) x
-- Init.Data.Subtype.Basic
Subtype.forall : ∀ {α : Sort u} {p : α → Prop} {q : { a // p a } → Prop}, (∀ (x : { a // p a }), q x) ↔ ∀ (a : α) (b : p a), q ⟨a, b⟩
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.OrderedListType.all_complete : ∀ (x : Lean.Doc.Parser.OrderedListType), x ∈ Lean.Doc.Parser.OrderedListType.all✝
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.indep_limsup_atBot_self : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω}
  {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [inst : SemilatticeInf ι]
  [NoMinOrder ι] [Nonempty ι],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.Kernel.iIndep s κ μα →
      ProbabilityTheory.Kernel.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) κ μα
-- Mathlib.LinearAlgebra.TensorPower.Basic
/-- Two dependent pairs of tensor products are equal if their index is equal and the contents
are equal after a canonical reindexing.  -/
PiTensorProduct.gradedMonoid_eq_of_reindex_cast : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ιι : Type u_3}
  {ι : ιι → Type u_4} {a b : GradedMonoid fun ii => PiTensorProduct R fun x => M} (h : a.fst = b.fst),
  (PiTensorProduct.reindex R (fun x => M) (Equiv.cast ⋯)) a.snd = b.snd → a = b
-- Mathlib.Data.Setoid.Basic
/-- Given two equivalence relations with `r ≤ s`, a bijection between the sum of the quotients by
`r` on each equivalence class by `s` and the quotient by `r`.  -/
Setoid.sigmaQuotientEquivOfLe : {α : Type u_1} → {r s : Setoid α} → r ≤ s → (q : Quotient s) × Quotient (Setoid.comap Subtype.val r) ≃ Quotient r
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar_smul_map : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure]
  [μ.Regular] (φ : G ≃ₜ+ G), MeasureTheory.addEquivAddHaarChar φ • MeasureTheory.Measure.map (⇑φ) μ = μ
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacGen.inj : ∀ {decl decl_1 : Lean.Name}, Aesop.RuleTacDescr.tacGen decl = Aesop.RuleTacDescr.tacGen decl_1 → decl = decl_1
-- Std.Data.ExtTreeSet.Basic
/-- Inserts the given element into the set. If the tree set already contains an element that is
equal (with regard to `cmp`) to the given element, then the tree set is returned unchanged.

Note: this non-replacement behavior is true for `ExtTreeSet` and `ExtTreeSet.Raw`.
The `insert` function on `ExtTreeMap`, `ExtDTreeMap`, `ExtTreeMap.Raw` and `ExtDTreeMap.Raw` behaves
differently: it will overwrite an existing mapping.
 -/
Std.ExtTreeSet.insert : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → Std.ExtTreeSet α cmp
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.smul_tprodCoeff' : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {R₁ : Type u_5} {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
  [inst_4 : DistribMulAction R₁ R] [inst_5 : SMulCommClass R₁ R R] (r : R₁) (z : R) (f : (i : ι) → s i),
  r • PiTensorProduct.tprodCoeff R z f = PiTensorProduct.tprodCoeff R (r • z) f
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mrange_fst : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mrange (MonoidHom.fst M N) = ⊤
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- `primitiveRoots k R` is the finset of primitive `k`-th roots of unity
in the integral domain `R`.  -/
primitiveRoots : ℕ → (R : Type u_7) → [inst : CommRing R] → [IsDomain R] → Finset R
-- Mathlib.Topology.MetricSpace.Isometry
/-- The identity is an isometry  -/
isometry_id : ∀ {α : Type u} [inst : PseudoEMetricSpace α], Isometry id
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.mul_integral_comp_mul_add : ∀ {a b : ℝ} {f : ℝ → ℝ} (c d : ℝ), c * ∫ (x : ℝ) in a..b, f (c * x + d) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
-- Mathlib.MeasureTheory.Group.Measure
/-- A measure on a group is a Haar measure if it is left-invariant, and gives finite mass to
compact sets and positive mass to open sets.

Textbooks generally require an additional regularity assumption to ensure nice behavior on
arbitrary locally compact groups. Use `[IsHaarMeasure μ] [Regular μ]` or
`[IsHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
sense is automatically regular and inner regular on second countable locally compact groups, as
checked just below this definition.  -/
MeasureTheory.Measure.IsHaarMeasure : {G : Type u_3} → [Group G] → [TopologicalSpace G] → [inst : MeasurableSpace G] → MeasureTheory.Measure G → Prop
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- Values of an absolute value coincide on the image of `ℕ` in `R`
if and only if they coincide on the image of `ℤ` in `R`.  -/
AbsoluteValue.eq_on_nat_iff_eq_on_int : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [inst_3 : Ring R]
  [NoZeroDivisors S] {f g : AbsoluteValue R S}, (∀ (n : ℕ), f ↑n = g ↑n) ↔ ∀ (n : ℤ), f ↑n = g ↑n
-- Std.Time.DateTime.WallTime
/-- Creates a `WallTime` from a `Duration`. The epoch is 1970-01-01 00:00:00 in local
(civil) time, not UTC.
 -/
Std.Time.WallTime.ofDuration : Std.Time.Duration → Std.Time.WallTime
-- Mathlib.Analysis.Complex.ReImTopology
Complex.isQuotientMap_im : Topology.IsQuotientMap Complex.im
-- Init.Data.List.Pairwise
List.Pairwise.forall_sublist : ∀ {α : Type u_1} {l : List α} {R : α → α → Prop}, List.Pairwise R l → ∀ {a b : α}, [a, b].Sublist l → R a b
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_of_contains_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  (m.erase k).contains a = true → m.contains a = true
-- Mathlib.Data.Set.Sups
Set.sups_subset_right : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_insert_le_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {v : β} {km kmi : α}, t.minKey? = some km → (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.instInitialProdProd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C' D')
  [F.Initial] [G.Initial], (F.prod G).Initial
-- Batteries.Data.Array.Basic
/-- Returns the first minimal element among `d` and elements of the array.
If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered (in addition to `d`).
 -/
Array.minWith : {α : Type u_1} → [ord : Ord α] → (xs : Array α) → α → optParam ℕ 0 → optParam ℕ xs.size → α
-- Mathlib.Order.Interval.Finset.Defs
Fintype.card_Icc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α) [inst_2 : Fintype ↑(Set.Icc a b)],
  Fintype.card ↑(Set.Icc a b) = (Finset.Icc a b).card
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.uniqueAddUnits.eq_1 : ∀ {α : Type u_1}, FreeAddMonoid.uniqueAddUnits = { toInhabited := AddUnits.instInhabited, uniq := ⋯ }
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.stepAsHetT_filterMapWithPostcondition : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α β γ : Type u_1} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Std.Iterator α m β] [inst_5 : MonadLiftT m n] [LawfulMonadLiftT m n]
  {f : β → Std.Iterators.PostconditionT n (Option γ)} {it : Std.IterM m β},
  (Std.IterM.filterMapWithPostcondition f it).stepAsHetT =
    (Std.Iterators.HetT.liftInner n it.stepAsHetT).bind fun x =>
      match x with
      | Std.IterStep.yield it' out => do
        let __do_lift ← Std.Iterators.HetT.ofPostconditionT (f out)
        match __do_lift with
          | some out' => pure (Std.IterStep.yield (Std.IterM.filterMapWithPostcondition f it') out')
          | none => pure (Std.IterStep.skip (Std.IterM.filterMapWithPostcondition f it'))
      | Std.IterStep.skip it' => pure (Std.IterStep.skip (Std.IterM.filterMapWithPostcondition f it'))
      | Std.IterStep.done => pure Std.IterStep.done
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.restr_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)),
  ↑(h.restr hs).symm = ↑e.symm
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.equivDirectSum_symm_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a : DirectSum ℕ fun n => TensorPower R n M), TensorAlgebra.equivDirectSum.symm a = TensorAlgebra.ofDirectSum a
-- Std.Sat.CNF.Basic
Std.Sat.CNF.instDecidableVarMemOfDecidableEq : {α : Type u_1} → {v : α} → {f : Std.Sat.CNF α} → [DecidableEq α] → Decidable (Std.Sat.CNF.VarMem v f)
-- Mathlib.MeasureTheory.Measure.Decomposition.Hahn
MeasureTheory.IsHahnDecomposition.ge_on_compl : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.IsHahnDecomposition μ ν s → ν.restrict sᶜ ≤ μ.restrict sᶜ
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.Shrink.instLocallySmallShrink : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Small.{w', u} C]
  [CategoryTheory.LocallySmall.{w, v, u} C], CategoryTheory.LocallySmall.{w, v, w'} (Shrink.{w', u} C)
-- Lean.Parser.Term
Lean.Parser.Term.trueVal : Lean.Parser.Parser
-- Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic
/-- Algebraic cycle on a scheme `X` with coefficients in a type `Z` is just a function from `X` to `Z`
with locally finite support (see the module docstring for more details).

Note: currently this is an abbrev to save some effort in duplicating API. This seems fine for now,
but be aware of this if there is ever an instance clash involving algebraic cycles.
 -/
AlgebraicGeometry.AlgebraicCycle : AlgebraicGeometry.Scheme → (R : Type u_2) → [Zero R] → Type (max u u_2)
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- The `ramificationIdxIn` is equal to any ramification index over the same ideal.  -/
Ideal.ramificationIdxIn_eq_ramificationIdx : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] (G : Type u_3) [inst_3 : Group G] [Finite G]
  [inst_5 : MulSemiringAction G B] [IsGaloisGroup G A B], p.ramificationIdxIn B = P.ramificationIdx A
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.isoMk_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x y : F.Elements)
  (e : x.fst ≅ y.fst) (he : (CategoryTheory.ConcreteCategory.hom (F.map e.hom)) x.snd = y.snd),
  (CategoryTheory.CategoryOfElements.isoMk x y e he).inv = CategoryTheory.CategoryOfElements.homMk y x e.inv ⋯
-- Mathlib.Algebra.Order.CompleteField
/-- The induced order-preserving function from a linear ordered field to a conditionally complete
linear ordered field, defined by taking the Sup in the codomain of all the rationals less than the
input.  -/
ConditionallyCompleteLinearOrderedField.inducedMap : (α : Type u_2) → (β : Type u_3) → [Field α] → [LinearOrder α] → [Field β] → [ConditionallyCompleteLinearOrder β] → α → β
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isPath_of_isSubwalk : ∀ {V : Type u} {G : SimpleGraph V} {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'},
  p₁.IsSubwalk p₂ → p₂.IsPath → p₁.IsPath
-- Mathlib.Data.Seq.Computation
Computation.empty_orElse : ∀ {α : Type u} (c : Computation α), (Computation.empty α <|> c) = c
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.le_skipWhile_of_isLongestMatchAtChain : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain pat startPos endPos → endPos ≤ startPos.skipWhile pat