mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Basic
Nat.eq_of_mul_eq_mul_right : ∀ {n m k : ℕ}, 0 < m → n * m = k * m → n = k
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.runWith : {α : Type} → String → optParam (Array String) #[] → Lean.Lsp.Ipc.IpcM α → IO α
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- The complete lattice of subcomplexes of a simplicial set.  -/
SSet.Subcomplex : SSet → Type (max 0 u)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.ρ_inv_hom : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X : CategoryTheory.FreeMonoidalCategory C}, CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Std.Internal.UV.TCP
/-- Shuts down an incoming connection on a listening TCP socket.
 -/
Std.Internal.UV.TCP.Socket.shutdown : Std.Internal.UV.TCP.Socket → IO (IO.Promise (Except IO.Error Unit))
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
/-- The Riemannian extended distance between two points, in a manifold where the tangent spaces
have an extended norm, defined as the infimum of the lengths of `C^1` paths between the points.  -/
Manifold.riemannianEDist : {E : Type u_4} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_5} →
        [inst_2 : TopologicalSpace H] →
          (I : ModelWithCorners ℝ E H) →
            {M : Type u_6} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] → [(x : M) → ENorm (TangentSpace I x)] → M → M → ENNReal
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso.inv.app (HomotopicalAlgebra.BifibrantObject.toHoCat.obj X) =
    HomotopicalAlgebra.BifibrantObject.toHoCat.map
      (HomotopicalAlgebra.BifibrantObject.homMk
        (HomotopicalAlgebra.CofibrantObject.mk X.obj).iBifibrantResolutionObj.hom)
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.genMatchCongrEqns : Lean.Name → Lean.MetaM (Array Lean.Name)
-- Init.Data.Float.Model.Float32
/-- Construct a `Float32.Model` from its bit representation. This operation canonicalizes
all `NaN` inputs into the canonical `NaN`.
 -/
Float32.Model.ofBits : UInt32 → Float32.Model
-- Batteries.Data.AssocList
Batteries.AssocList.cons.inj : ∀ {α : Type u} {β : Type v} {key : α} {value : β} {tail : Batteries.AssocList α β} {key_1 : α} {value_1 : β}
  {tail_1 : Batteries.AssocList α β},
  Batteries.AssocList.cons key value tail = Batteries.AssocList.cons key_1 value_1 tail_1 →
    key = key_1 ∧ value = value_1 ∧ tail = tail_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
/-- Construct a parallel-prefix-sum circuit, invoking `blastCpopLayer` for
each layer, until a single addition node is left.
 -/
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget aig w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.NumberTheory.PrimeCounting
Nat.prime_of_mem_primesLE : ∀ {p n : ℕ}, p ∈ n.primesLE → Nat.Prime p
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.supported_eq_map : ∀ (R : Type u_1) (S : Type u_2) {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M),
  AddMonoidAlgebra.supported R S s =
    Submodule.map (↑(AddMonoidAlgebra.coeffLinearEquiv R).symm) (Finsupp.supported S R s)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.right : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → D → CategoryTheory.Join C D
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.mem_localizationLocalizationSubmodule : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {N : Submonoid S} {x : R},
  x ∈ IsLocalization.localizationLocalizationSubmodule M N ↔ ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z
-- Init.System.IO
/-- Converts POSIX-style file permissions to their numeric representation, with three bits each for the
owner's permissions, the group's permissions, and others' permissions.
 -/
IO.FileRight.flags : IO.FileRight → UInt32
-- Mathlib.Probability.Kernel.Disintegration.Basic
ProbabilityTheory.Kernel.condKernelCountable.instIsMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : Countable α] (κCond : α → ProbabilityTheory.Kernel β Ω)
  [∀ (a : α), ProbabilityTheory.IsMarkovKernel (κCond a)]
  (h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y),
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.condKernelCountable κCond h_atom)
-- Init.Sym.Lemmas
Lean.Sym.UInt32.eq_eq_false : ∀ (a b : UInt32), decide (a = b) = false → (a = b) = False
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_eq_some_getD_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {a : α} {fallback : β a}, Std.DTreeMap.Internal.Impl.contains a t = true → t.get? a = some (t.getD a fallback)
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_last_castSucc : ∀ {n : ℕ} {i : Fin (n + 1)}, (Fin.last n).predAbove i.castSucc = i
-- Init.Data.Array.Lemmas
Array.filter_eq_push_iff : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α} {a : α},
  Array.filter p xs = ys.push a ↔
    ∃ as bs, xs = as.push a ++ bs ∧ Array.filter p as = ys ∧ p a = true ∧ ∀ x ∈ bs, ¬p x = true
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point
in the source is a neighborhood of the preimage, within a set.  -/
extChartAt_preimage_mem_nhdsWithin' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s t : Set M} [inst_5 : ChartedSpace H M] {x x' : M},
  x' ∈ (extChartAt I x).source →
    t ∈ nhdsWithin x' s →
      ↑(extChartAt I x).symm ⁻¹' t ∈ nhdsWithin (↑(extChartAt I x) x') (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.instFaithfulCatTypeToCat : CategoryTheory.typeToCat.Faithful
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.norm_polarCoord_symm : ∀ (p : ℝ × ℝ), ‖↑Complex.polarCoord.symm p‖ = |p.1|
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey! (t.minKeyD fallback) = t.minKeyD fallback
-- Mathlib.Data.Fin.Tuple.Basic
/-- `tail` and `init` commute. We state this lemma in a non-dependent setting, as otherwise it
would involve a cast to convince Lean that the two types are equal, making it harder to use.  -/
Fin.tail_init_eq_init_tail : ∀ {n : ℕ} {β : Sort u_2} (q : Fin (n + 2) → β), Fin.tail (Fin.init q) = Fin.init (Fin.tail q)
-- Lean.Compiler.ImplementedByAttr
Lean.Compiler.setImplementedBy : Lean.Environment → Lean.Name → Lean.Name → Except String Lean.Environment
-- Mathlib.CategoryTheory.Products.Basic
/-- Any morphism in a product factors as a morphism whose right component is an identity
followed by a morphism whose left component is an identity.  -/
CategoryTheory.Prod.fac'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {x y : C × D} (f : x ⟶ y) {Z : C × D} (h : y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id x.2))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id y.1) f.2) h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_eq_none : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α}, a ∉ t → t.get? a = none
-- Init.PropLemmas
exists_eq_left' : ∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∃ a, a' = a ∧ p a) ↔ p a'
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.shortExact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [CategoryTheory.Mono f],
  { X₁ := K, X₂ := L, X₃ := CategoryTheory.Limits.cokernel f, f := f, g := CategoryTheory.Limits.cokernel.π f,
      zero := ⋯ }.ShortExact
-- Init.Data.SInt.Bitwise
Int8.zero_shiftLeft : ∀ {a : Int8}, 0 <<< a = 0
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.alter.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} (a : α) (motive : Option (β a) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (b : β a) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Tactic.Sat.FromLRAT
/-- A valuation is an assignment of values to all the propositional variables.  -/
Sat.Valuation : Type
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.text.inj : ∀ {α : Type u} {a a_1 : String}, Lean.Widget.TaggedText.text a = Lean.Widget.TaggedText.text a_1 → a = a_1
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] (d : D),
  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxRightLinear.μᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.InfinitePlace.nrComplexPlaces.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.InfinitePlace.nrComplexPlaces K = Fintype.card { w // w.IsComplex }
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The fixator of a finite subset of cardinal d in an n-transitive additive action
acts m transitively on the complement if d + m ≤ n.  -/
SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive' : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {m n : ℕ}
  [AddAction.IsMultiplyPretransitive G α n] (s : Set α) [Finite ↑s],
  s.ncard + m ≤ n →
    ↑n ≤ ENat.card α →
      AddAction.IsMultiplyPretransitive (↥(fixingAddSubgroup G s)) (↥(SubAddAction.ofFixingAddSubgroup G s)) m
-- Init.Data.Array.Basic
/-- Erases repeated elements, keeping the first element of each run.

`O(|as|)`.

Example:
* `#[1, 3, 2, 2, 2, 3, 3, 5].eraseReps = #[1, 3, 2, 3, 5]`
 -/
Array.eraseReps : {α : Type u_1} → [BEq α] → Array α → Array α
-- Mathlib.MeasureTheory.Measure.Restrict
/-- If `μ s ≠ 0`, then `μ.restrict s ≠ 0`, in terms of `NeZero` instances.  -/
MeasureTheory.Measure.restrict.neZero : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NeZero (μ s)],
  NeZero (μ.restrict s)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_of_not_nonneg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A},
  ¬0 ≤ a → CFC.sqrt a = 0
-- Init.Data.BitVec.Bitblast
BitVec.getElem_smod : ∀ {w i : ℕ} {x y : BitVec w} (h : i < w),
  (x.smod y)[i] =
    match x.msb, y.msb with
    | false, false => (x % y)[i]
    | false, true => (if x % -y = 0#w then x % -y else x % -y + y)[i]
    | true, false => (if -x % y = 0#w then -x % y else y - -x % y)[i]
    | true, true => (-(-x % -y))[i]
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.HomotopyCategory.homToNerveMk_comp : ∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C] {D : Type u}
  [inst_1 : CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor X.HomotopyCategory C)
  (G : CategoryTheory.Functor C D),
  SSet.Truncated.HomotopyCategory.homToNerveMk (F.comp G) =
    CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homToNerveMk F)
      ((SSet.truncation 2).map (CategoryTheory.nerveMap G))
-- Mathlib.LinearAlgebra.TensorProduct.Pi
_private.Mathlib.LinearAlgebra.TensorProduct.Pi.0.TensorProduct.piScalarRightInv_single : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] (ι : Type u_4)
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι] (x : N) (i : ι),
  (TensorProduct.piScalarRightInv R S N ι) (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1
-- Aesop.Forward.State
/-- Add a hypothesis and to the forward state, along with any rule pattern
substitutions obtained from it.  -/
Aesop.ForwardState.enqueueHypWithPatSubsts : Lean.FVarId →
  Array (Aesop.ForwardRule × Aesop.PremiseIndex) →
    Array (Aesop.ForwardRule × Aesop.Substitution) → Aesop.ForwardState → Aesop.ForwardState
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.sInf : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {ℐ : Set (Ideal A)},
  (∀ I ∈ ℐ, Ideal.IsHomogeneous 𝒜 I) → Ideal.IsHomogeneous 𝒜 (sInf ℐ)
-- Init.Data.SInt.Basic
/-- Bitwise complement, also known as bitwise negation, for 32-bit signed integers. Usually accessed via
the `~~~` prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
Integers use the two's complement representation, so `Int32.complement a = -(a + 1)`.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.complement : Int32 → Int32
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.singularPart_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α), MeasureTheory.SignedMeasure.singularPart 0 μ = 0
-- Mathlib.LinearAlgebra.Dimension.Finite
Submodule.bot_eq_top_of_rank_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M], Module.rank R M = 0 → ⊥ = ⊤
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.all_eq_all_toListModel : ∀ {α : Type u} {β : α → Type v} {p : (a : α) → β a → Bool} {m : Std.DTreeMap.Internal.Impl α β},
  m.all p = m.toListModel.all fun x => p x.fst x.snd
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- Two Lie derivations equal on a set are equal on its Lie span.  -/
LieDerivation.eqOn_lieSpan : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {D1 D2 : LieDerivation R L M} {s : Set L}, Set.EqOn (⇑D1) (⇑D2) s → Set.EqOn ⇑D1 ⇑D2 ↑(LieSubalgebra.lieSpan R L s)
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_preimage_of_notMem : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (s : Set α) (f : α → M) {t : Set M},
  1 ∉ t → s.mulIndicator f ⁻¹' t = f ⁻¹' t ∩ s
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the forward direction of `SimpleGraph.Walk.isCycle_rotate`. -/
SimpleGraph.Walk.IsCycle.of_rotate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {c : G.Walk v v} (hu : u ∈ c.support),
  (c.rotate u hu).IsCycle → c.IsCycle
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.invertibleEquivDetInvertible_apply : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [inst_3 : Invertible A], A.invertibleEquivDetInvertible inst_3 = A.detInvertibleOfInvertible
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.le.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (val : β)
  (h_1 : (val : β) → motive none (some val)) (h_2 : Unit → motive none none) (h_3 : (val : α) → motive (some val) none)
  (h_4 : (x : α) → (y : β) → motive (some x) (some y)),
  (match none, some val with
    | none, some val => h_1 val
    | none, none => h_2 ()
    | some val, none => h_3 val
    | some x, some y => h_4 x y) =
    h_1 val
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_union_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} (mem : k ∈ t₂), (t₁ ∪ t₂).getKey k ⋯ = t₂.getKey k mem
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.isOpenQuotientMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_3)
  [inst_2 : AddGroup G] [inst_3 : AddAction G E], IsAddQuotientCoveringMap f G → IsOpenQuotientMap f
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.mk'_x : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↥X) (y : ↥Y) (h : f x = g y),
  (AlgebraicGeometry.Scheme.Pullback.Triplet.mk' x y h).x = x
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Quotient.instDiscreteMeasurableSpace : ∀ {α : Type u_6} {s : Setoid α} [inst : MeasurableSpace α] [DiscreteMeasurableSpace α],
  DiscreteMeasurableSpace (Quotient s)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instVAdd : {β : Type u_2} → {α : Type u_1} → [VAdd β α] → VAdd β (Colex α)
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
/-- An atlas member is `C^n` for any `n`.  -/
contMDiffOn_of_mem_maximalAtlas : ∀ {𝕜 : 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 ℕ∞} {e : OpenPartialHomeomorph M H},
  e ∈ IsManifold.maximalAtlas I n M → ContMDiffOn I I n (↑e) e.source
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_ball_comm : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, x ∈ Metric.ball y ε ↔ y ∈ Metric.ball x ε
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_of_coprime : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [Finite G],
  Nat.card ↥H * Nat.card ↥K = Nat.card G → (Nat.card ↥H).Coprime (Nat.card ↥K) → H.IsComplement' K
-- Init.Data.Array.Extract
Array.extract_eq_extract_right : ∀ {α : Type u_1} {as : Array α} {i j j' : ℕ},
  as.extract i j = as.extract i j' ↔ min (j - i) (as.size - i) = min (j' - i) (as.size - i)
-- Mathlib.SetTheory.ZFC.Class
/-- An induction principle for sets. If every subset of a class is a member, then the class is
universal.  -/
Class.eq_univ_of_powerset_subset : ∀ {A : Class.{u_1}}, A.powerset ⊆ A → A = Class.univ
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.minKey : {α : Type u} → {β : α → Type v} → (t : Std.DTreeMap.Internal.Impl α β) → t.isEmpty = false → α
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- Given a sequence of functions `f` which converges in measure to `g`,
`seqTendstoAeSeqAux` is a sequence such that
`∀ m ≥ seqTendstoAeSeqAux n, μ {x | 2⁻¹ ^ n ≤ dist (f m x) (g x)} ≤ 2⁻¹ ^ n`.  -/
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        [inst : PseudoEMetricSpace E] →
          {f : ℕ → α → E} → {g : α → E} → MeasureTheory.TendstoInMeasure μ f Filter.atTop g → ℕ → ℕ
-- Mathlib.Algebra.Ring.GeomSum
pow_one_sub_dvd_pow_mul_sub_one : ∀ {R : Type u_1} [inst : Ring R] (x : R) (m n : ℕ), x ^ m - 1 ∣ x ^ (m * n) - 1
-- Mathlib.Data.Fin.Tuple.Basic
Fin.range_insertNth : ∀ {n : ℕ} {α : Type u_3} (p : Fin (n + 1)) (x : α) (f : Fin n → α),
  Set.range (p.insertNth x f) = Set.insert x (Set.range f)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.ker_lsmul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.IsTorsionFree R M] {a : R}, a ≠ 0 → ((LinearMap.lsmul R M) a).ker = ⊥
-- Init.Data.Rat.Lemmas
Rat.neg_le_neg : ∀ {a b : ℚ}, a ≤ b → -b ≤ -a
-- Lean.Meta.Tactic.Grind.Types
/-- Return `true` if `a` and `b` have the same type.  -/
Lean.Meta.Grind.hasSameType : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.Normed.Group.Continuity
Continuous.nnnorm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
  Continuous f → Continuous fun x => ‖f x‖₊
-- Mathlib.Data.Sum.Order
OrderIso.sumComm_symm : ∀ (α : Type u_10) (β : Type u_11) [inst : LE α] [inst_1 : LE β], (OrderIso.sumComm α β).symm = OrderIso.sumComm β α
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.mk.inj : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} {inst : Ring k}
  {inst_1 : AddCommGroup V₁} {inst_2 : Module k V₁} {inst_3 : AddTorsor V₁ P₁} {inst_4 : TopologicalSpace P₁}
  {inst_5 : AddCommGroup V₂} {inst_6 : Module k V₂} {inst_7 : AddTorsor V₂ P₂} {inst_8 : TopologicalSpace P₂}
  {toAffineEquiv : P₁ ≃ᵃ[k] P₂}
  {continuous_toFun : autoParam (Continuous toAffineEquiv.toFun) ContinuousAffineEquiv.continuous_toFun._autoParam}
  {continuous_invFun : autoParam (Continuous toAffineEquiv.invFun) ContinuousAffineEquiv.continuous_invFun._autoParam}
  {toAffineEquiv_1 : P₁ ≃ᵃ[k] P₂}
  {continuous_toFun_1 : autoParam (Continuous toAffineEquiv_1.toFun) ContinuousAffineEquiv.continuous_toFun._autoParam}
  {continuous_invFun_1 :
    autoParam (Continuous toAffineEquiv_1.invFun) ContinuousAffineEquiv.continuous_invFun._autoParam},
  { toAffineEquiv := toAffineEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toAffineEquiv := toAffineEquiv_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 } →
    toAffineEquiv = toAffineEquiv_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_alter_of_compare_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β},
  cmp k k' = Ordering.eq → (k' ∈ Std.DTreeMap.Const.alter t k f ↔ (f (Std.DTreeMap.Const.get? t k)).isSome = true)
-- Mathlib.CategoryTheory.Action.Monoidal
/-- Upgrading the functor `(SingleObj G ⥤ V) ⥤ Action V G` to a monoidal functor.  -/
Action.FunctorCategoryEquivalence.inverseMonoidal : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        [inst_2 : CategoryTheory.MonoidalCategory V] → Action.FunctorCategoryEquivalence.inverse.Monoidal