mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.MeasuredSets
MeasureTheory.instPseudoEMetricSpaceMeasuredSets : {α : Type u_1} →
  [mα : MeasurableSpace α] → {μ : MeasureTheory.Measure α} → PseudoEMetricSpace (MeasureTheory.MeasuredSets μ)
-- Init.Data.Rat.Lemmas
Rat.lt_floor_add_one : ∀ (a : ℚ), a < ↑(a.floor + 1)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.comapStructureSheafFun.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B] [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B]
  {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜] [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (U : TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)) (V : TopologicalSpace.Opens (ProjectiveSpectrum ℬ))
  (hUV : V.carrier ⊆ ⇑(AlgebraicGeometry.ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier)
  (s : (x : ↥U) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toSubmodule) (y : ↥V),
  AlgebraicGeometry.Proj.comapStructureSheafFun f hf U V hUV s y =
    (HomogeneousLocalization.localRingHom f (Ideal.comap f (↑y).asHomogeneousIdeal.toSubmodule)
        (↑y).asHomogeneousIdeal.toSubmodule ⋯)
      (s ⟨(AlgebraicGeometry.ProjectiveSpectrum.comap f hf) ↑y, ⋯⟩)
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The map of quotients by powers of an integer induced by a group homomorphism.  -/
QuotientGroup.homQuotientZPowOfHom : {A B : Type u} →
  [inst : CommGroup A] →
    [inst_1 : CommGroup B] → (A →* B) → (n : ℤ) → A ⧸ (zpowGroupHom n).range →* B ⧸ (zpowGroupHom n).range
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `le_div_iff₀` for a version with multiplication on the other side.  -/
le_div_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (a ≤ b / c ↔ c * a ≤ b)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.Tendsto.uniformity_add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f g : ι → α × α}
  {l : Filter ι},
  Filter.Tendsto f l (uniformity α) → Filter.Tendsto g l (uniformity α) → Filter.Tendsto (f + g) l (uniformity α)
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The extension of functors functor `(C ⥤ D) ⥤ (Karoubi C ⥤ D)`
when `D` is idempotent complete.  -/
CategoryTheory.Idempotents.functorExtension : (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.IsIdempotentComplete D] →
          CategoryTheory.Functor (CategoryTheory.Functor C D)
            (CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D)
-- Mathlib.Algebra.Module.Equiv.Basic
/-- An additive equivalence whose underlying function preserves `smul` is a linear equivalence.  -/
AddEquiv.toLinearEquiv : {R : Type u_1} →
  {M : Type u_5} →
    {M₂ : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M] →
              [inst_4 : Module R M₂] → (e : M ≃+ M₂) → (∀ (c : R) (x : M), e (c • x) = c • e x) → M ≃ₗ[R] M₂
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.star_eq_zero : ∀ {z : Complex.UnitClosedDisc}, star z = 0 ↔ z = 0
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.sdiff_ae_eq_right : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → t \ s =ᵐ[μ] t
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `allOnes`  -/
BitVec.reduceAllOnes : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_nonneg : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K},
  0 ≤ x → 0 ≤ ArchimedeanClass.stdPart x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The bijection `h.ι ≃ h.II` when `h : A.PairingCore`.  -/
SSet.Subcomplex.PairingCore.equivII : {X : SSet} → {A : X.Subcomplex} → (h : A.PairingCore) → h.ι ≃ ↑h.II
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.frequently_ae_ne_zero_of_setIntegral_ne_zero : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  ∫ᵛ (x : X) in t, f x ∂[B; μ] ≠ 0 → ∃ᵐ (x : X) ∂μ.variation.restrict t, f x ≠ 0
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.listProd : ∀ {α : Type u_1} {ι : Type u_2} {β : Type u_3} [inst : NormedField β] {l : Filter α} {L : List ι} {f g : ι → α → β},
  (∀ i ∈ L, Asymptotics.IsEquivalent l (f i) (g i)) →
    Asymptotics.IsEquivalent l (fun x => (List.map (fun x_1 => f x_1 x) L).prod) fun x =>
      (List.map (fun x_1 => g x_1 x) L).prod
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.T_apply : ∀ {R : Type u_1} [inst : Semiring R] (m n : ℤ), (LaurentPolynomial.T n).coeff m = if n = m then 1 else 0
-- Mathlib.Topology.Instances.CantorSet
cantorSet_eq_zero_two_ofDigits : cantorSet = {x | ∃ a, (∀ (i : ℕ), a i ≠ 1) ∧ Real.ofDigits a = x}
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
BoundedContinuousFunction.toLp_injective : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_3}
  [inst_5 : Fact (1 ≤ p)] [inst_6 : NormedRing 𝕜] [inst_7 : Module 𝕜 E] [inst_8 : IsBoundedSMul 𝕜 E]
  [μ.IsOpenPosMeasure], Function.Injective ⇑(BoundedContinuousFunction.toLp p μ 𝕜)
-- Mathlib.Algebra.Free
/-- Semigroup quotient of a magma.  -/
Magma.AssocQuotient : (α : Type u) → [Mul α] → Type u
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_eq_back!_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.maxKey! = t.keysArray.back!
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termI₁ : Lean.ParserDescr
-- Std.Time.Format.Modifier
Std.Time.Modifier.B.injEq : ∀ (presentation presentation_1 : Std.Time.Text),
  (Std.Time.Modifier.B presentation = Std.Time.Modifier.B presentation_1) = (presentation = presentation_1)
-- Init.Data.Option.Monadic
Option.forIn'_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [inst : Monad m] [LawfulMonad m]
  (o : Option α) (g : α → β) (f : (b : β) → b ∈ Option.map g o → γ → m (ForInStep γ)),
  forIn' (Option.map g o) init f = forIn' o init fun a h y => f (g a) ⋯ y
-- Std.Http.Data.Status
/-- HTTP Status codes. Status codes are three-digit integer codes that describe the result of an
HTTP request. This implementation includes common named statuses and supports custom codes through
`Status.other`.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes
 -/
Std.Http.Status : Type
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.toConjAct_mul : ∀ {G : Type u_3} [inst : DivInvMonoid G] (x y : G),
  ConjAct.toConjAct (x * y) = ConjAct.toConjAct x * ConjAct.toConjAct y
-- Mathlib.ModelTheory.DirectLimit
/-- The `L.Structure` on a direct limit of `L.Structure`s.  -/
FirstOrder.Language.DirectLimit.instStructureDirectLimit : {L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      (G : ι → Type w) →
        [inst_1 : (i : ι) → L.Structure (G i)] →
          (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) →
            [inst_2 : IsDirectedOrder ι] →
              [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] →
                [Nonempty ι] → L.Structure (FirstOrder.Language.DirectLimit G f)
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
OrderDual.instDistribSMul_1 : {G₀ : Type u_1} → {M₀ : Type u_2} → [inst : AddZeroClass M₀] → [DistribSMul G₀ M₀] → DistribSMul G₀ M₀ᵒᵈ
-- Mathlib.Order.Interval.Set.Fin
Fin.range_natAdd_eq_Ici : ∀ (m n : ℕ) [inst : NeZero n], Set.range (Fin.natAdd m) = Set.Ici (Fin.natAdd m 0)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.getEntry?.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)),
  (match [] with
    | [] => h_1 ()
    | ⟨k, v⟩ :: l => h_2 k v l) =
    h_1 ()
-- Mathlib.Order.CompleteLattice.Defs
/-- In a linearly ordered type, we assume the order relations are all decidable.  -/
CompleteLinearOrder.toDecidableEq : {α : Type u_8} → [self : CompleteLinearOrder α] → DecidableEq α
-- Init.Data.List.Nat.Range
List.pairwise_lt_range : ∀ {n : ℕ}, List.Pairwise (fun x1 x2 => x1 < x2) (List.range n)
-- Mathlib.CategoryTheory.Adjunction.Parametrized
/-- The notation `F ⊣₂ G` stands for `ParametrizedAdjunction F G`
representing that the bifunctor `F` is the left adjoint to `G`
in an adjunction with a parameter.  -/
CategoryTheory.«term_⊣₂_» : Lean.TrailingParserDescr
-- Mathlib.Topology.EMetricSpace.Defs
/-- The topology on `α` is at most as fine as the topology generated by the `edist`.  -/
WeakPseudoEMetricSpace.topology_le : ∀ {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α],
  (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace ≤ τ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
/-- If `X` represents a presheaf of commutative groups, then `X` is a commutative group object.  -/
CategoryTheory.CommGrpObj.ofRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (X : C) →
          (F : CategoryTheory.Functor Cᵒᵖ CommGrpCat) →
            (F.comp (CategoryTheory.forget CommGrpCat)).RepresentableBy X → CategoryTheory.CommGrpObj X
-- Mathlib.Algebra.Star.StarRingHom
/-- See Note [custom simps projection]  -/
NonUnitalStarRingHom.Simps.apply : {A : Type u_1} →
  {B : Type u_2} →
    [inst : NonUnitalNonAssocSemiring A] →
      [inst_1 : Star A] → [inst_2 : NonUnitalNonAssocSemiring B] → [inst_3 : Star B] → (A →⋆ₙ+* B) → A → B
-- Init.Data.Int.LemmasAux
Int.ble'_eq_false : ∀ (a b : ℤ), (a.ble' b = false) = ¬a ≤ b
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
exists_eq_ciInf_of_finite : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [Nonempty ι] [Finite ι] {f : ι → α},
  ∃ i, f i = ⨅ i, f i
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSub.measurable_const_sub : ∀ {G : Type u_2} {inst : MeasurableSpace G} {inst_1 : Sub G} [self : MeasurableSub G] (c : G), Measurable fun x => c - x
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.linearEquiv_apply : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) (x : relations.Quotient),
  h.linearEquiv x = solution.fromQuotient x
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.eq_1 : ∀ (a a_1 b b_1 : ℤ),
  Lean.Grind.instBEqIntInterval.beq (Lean.Grind.IntInterval.co a a_1) (Lean.Grind.IntInterval.co b b_1) =
    (a == b && a_1 == b_1)
-- Mathlib.RingTheory.AdicCompletion.Basic
Hausdorffification.lift_comp_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [h : IsHausdorff I N] (f : M →ₗ[R] N),
  Hausdorffification.lift I f ∘ₗ Hausdorffification.of I M = f
-- Mathlib.Algebra.Order.Field.Power
zpow_eq_one_iff_of_ne_zero₀ : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  n ≠ 0 → (a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.borel_eq_generateFrom_Iio_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ a, {Set.Iio ↑a})
-- Init.Data.UInt.Bitwise
UInt64.shiftLeft_eq_shiftLeft_mod : ∀ (a b : UInt64), a <<< b = a <<< (b % 64)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.iSup_comap_le : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {ι : Sort u_7} (f : G →* N) (s : ι → Subgroup N),
  ⨆ i, Subgroup.comap f (s i) ≤ Subgroup.comap f (iSup s)
-- Mathlib.Algebra.Order.Star.Basic
/-- **Alias** of `IsSelfAdjoint.map'`.

---

While `IsSelfAdjoint.map` assumes the map is star-preserving, this lemma instead assumes the
map is an order-preserving additive map from a space where self-adjoint elements can be expressed as
differences of nonnegative elements, and whose codomain is a star-ordered ring. When such maps are
linear over `ℂ`, they are also star-preserving, and this lemma is used to establish that one by
splitting into real and imaginary parts.  -/
map_isSelfAdjoint : ∀ {F : Type u_6} {E : Type u_7} {R : Type u_8} [inst : AddCommGroup E] [inst_1 : PartialOrder E]
  [inst_2 : StarAddMonoid E] [inst_3 : NonUnitalRing R] [inst_4 : PartialOrder R] [inst_5 : StarRing R]
  [StarOrderedRing R] [SelfAdjointDecompose E] [inst_8 : FunLike F E R] [OrderHomClass F E R] [AddMonoidHomClass F E R]
  {a : E}, IsSelfAdjoint a → ∀ (f : F), IsSelfAdjoint (f a)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.prod.of : ∀ {α : Type u} [inst : Group α] {x : α}, FreeGroup.prod (FreeGroup.of x) = x
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.encodeSum.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : α ⊕ β → Sort u_3) →
      (x : α ⊕ β) → ((a : α) → motive (Sum.inl a)) → ((b : β) → motive (Sum.inr b)) → motive x
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- If `s` is a measurable set in a standard Borel space, there is a compatible Polish topology
making `s` clopen.  -/
MeasurableSet.isClopenable' : ∀ {α : Type u_4} [inst : MeasurableSpace α] [StandardBorelSpace α] {s : Set α},
  MeasurableSet s → ∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.dualSubmoduleParing_spec : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_2} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) {N : Submodule R M} (x : ↥(B.dualSubmodule N)) (y : ↥N),
  (algebraMap R S) (B.dualSubmoduleParing x y) = (B ↑x) ↑y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_not_contains_map_fst_of_containsKey_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getKey? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = none
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsImmersion f], IsLocallyClosed (Set.range ⇑f)
-- Mathlib.NumberTheory.Dioph
IsPoly.proj : ∀ {α : Type u_1} (i : α), IsPoly fun x => ↑(x i)
-- Mathlib.RingTheory.Ideal.Prod
Ideal.isPrime_ideal_prod_top : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} [h : I.IsPrime], (I.prod ⊤).IsPrime
-- Init.Data.List.Lemmas
/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`.  -/
List.map_id_fun' : ∀ {α : Type u_1}, (List.map fun a => a) = id
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.instAddActionOfVAddCommClass.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : VAdd M X]
  [inst_1 : VAdd N Y] [inst_2 : AddMonoid R] [inst_3 : AddAction R Y] [inst_4 : VAddCommClass N R Y],
  AddActionHom.instAddActionOfVAddCommClass =
    { toVAdd := AddActionHom.instVAddOfVAddCommClass, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.piLinearEquiv_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : Semiring R] [inst_1 : Semiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : Module A M] {ι' : Type u_6} {M' : ι' → Type u_7}
  [inst_5 : (i : ι') → AddCommMonoid (M' i)] [inst_6 : (i : ι') → TopologicalSpace (M' i)]
  [inst_7 : ∀ (i : ι'), ContinuousAdd (M' i)] [inst_8 : (i : ι') → Module R (M' i)]
  [inst_9 : (i : ι') → Module A (M' i)] [inst_10 : ∀ (i : ι'), SMulCommClass A R (M' i)]
  [inst_11 : ∀ (i : ι'), ContinuousConstSMul R (M' i)] (a : (i : ι') → M [⋀^ι]→L[A] M' i),
  ContinuousAlternatingMap.piLinearEquiv a = ContinuousAlternatingMap.pi a
-- Mathlib.Algebra.Algebra.Equiv
MulSemiringAction.toAlgAut_apply : ∀ (G : Type u_2) (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G R A] (g : G),
  (MulSemiringAction.toAlgAut G R A) g = MulSemiringAction.toAlgEquiv R A g
-- Mathlib.RingTheory.RingHom.Flat
/-- Composition of flat ring homomorphisms is flat.  -/
RingHom.Flat.comp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T}, f.Flat → g.Flat → (g.comp f).Flat
-- Init.Data.UInt.Lemmas
USize.toNat_ofNat' : ∀ {n : ℕ}, (USize.ofNat n).toNat = n % 2 ^ System.Platform.numBits
-- Mathlib.Data.Sym.Basic
Sym.val_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, ↑(Sym.replicate n a) = Multiset.replicate n a
-- Mathlib.RingTheory.LaurentSeries
/-- The ring equivalence between `RatFuncAdicCompl K` and `K⸨X⸩`.  -/
LaurentSeries.ratfuncAdicComplRingEquiv : (K : Type u_2) → [inst : Field K] → LaurentSeries.RatFuncAdicCompl K ≃+* LaurentSeries K
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opUnopEquiv_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Functor.opUnopEquiv C D).counitIso = CategoryTheory.NatIso.ofComponents (fun F => F.unopOpIso) ⋯
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instSemilatticeSup : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] → [(i : ι) → SemilatticeSup (α i)] → SemilatticeSup (Π₀ (i : ι), α i)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.NormalizedHom.cons.injEq : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₁) (a : Mathlib.Tactic.BicategoryLike.NormalizedHom)
  (a_1 : Mathlib.Tactic.BicategoryLike.Atom₁) (e_1 : Mathlib.Tactic.BicategoryLike.Mor₁)
  (a_2 : Mathlib.Tactic.BicategoryLike.NormalizedHom) (a_3 : Mathlib.Tactic.BicategoryLike.Atom₁),
  (Mathlib.Tactic.BicategoryLike.NormalizedHom.cons e a a_1 =
      Mathlib.Tactic.BicategoryLike.NormalizedHom.cons e_1 a_2 a_3) =
    (e = e_1 ∧ a = a_2 ∧ a_1 = a_3)
-- Mathlib.Probability.Independence.Process.Basic
/-- If stochastic processes `X : (i : S) → (j : T i) → Ω → 𝓧 i j` are independent and
for all `i j`, `X' i j` is almost everywhere equal to `X i j`,
then `X'` are also independent. This implies that independence results about
measurable processes should generally also hold
for processes whose marginals are only a.e.-measurable.  -/
ProbabilityTheory.iIndepFun.process_congr : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : S → Type u_4}
  {𝓧 : (i : S) → T i → Type u_5} [inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)]
  {X X' : (i : S) → (j : T i) → Ω → 𝓧 i j},
  ProbabilityTheory.iIndepFun (fun i ω j => X i j ω) P →
    (∀ (i : S) (j : T i), X i j =ᵐ[P] X' i j) → ProbabilityTheory.iIndepFun (fun i ω j => X' i j ω) P
-- Mathlib.Topology.Sheaves.CommRingCat
/-- The submonoid structure for each component  -/
TopCat.Presheaf.SubmonoidPresheaf.obj : {X : TopCat} →
  {F : TopCat.Presheaf CommRingCat X} → F.SubmonoidPresheaf → (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Submonoid ↑(F.obj U)
-- Init.Data.Order.Ord
Bool.instLawfulEqOrd : Std.LawfulEqOrd Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.mk.inj : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} {inv : SSet.Edge x₁ x₀}
  {homInvId : hom.CompStruct inv (SSet.Edge.id x₀)} {invHomId : inv.CompStruct hom (SSet.Edge.id x₁)}
  {inv_1 : SSet.Edge x₁ x₀} {homInvId_1 : hom.CompStruct inv_1 (SSet.Edge.id x₀)}
  {invHomId_1 : inv_1.CompStruct hom (SSet.Edge.id x₁)},
  { inv := inv, homInvId := homInvId, invHomId := invHomId } =
      { inv := inv_1, homInvId := homInvId_1, invHomId := invHomId_1 } →
    inv = inv_1 ∧ homInvId ≍ homInvId_1 ∧ invHomId ≍ invHomId_1
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ ≤ a₁ → b₁ ≤ b₂ → Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂
-- Batteries.Data.List.Lemmas
List.getElem_findIdxs_eq_findIdxNth_add : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {s : ℕ} {xs : List α} {h : n < (List.findIdxs p xs s).length},
  (List.findIdxs p xs s)[n] = List.findIdxNth p xs n + s
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.secondCountableTopology_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  SecondCountableTopology (TopologicalSpace.NonemptyCompacts α) ↔ SecondCountableTopology α
-- Mathlib.Algebra.Group.Prod
/-- Multiplying by the trivial monoid doesn't change the structure.

This is the `MulEquiv` version of `Equiv.uniqueProd`.  -/
MulEquiv.uniqueProd : {M : Type u_3} → {N : Type u_4} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [Unique N] → N × M ≃* M
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.expRecOn_exp : ∀ {M : Type u_4} {motive : WithZero (Multiplicative M) → Sort u_6} (x : M) (zero : motive 0)
  (exp : (a : M) → motive (WithZero.exp a)), WithZero.expRecOn (WithZero.exp x) zero exp = exp x
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
/-- The type of `n`-simplices of `X.op` identify to type of `n`-simplices of `X`.  -/
SSet.opObjEquiv : {X : SSet} → {n : SimplexCategoryᵒᵖ} → X.op.obj n ≃ X.obj n
-- Lean.Declaration
Lean.mkDefinitionValEx : Lean.Name →
  List Lean.Name →
    Lean.Expr → Lean.Expr → Lean.ReducibilityHints → Lean.DefinitionSafety → List Lean.Name → Lean.DefinitionVal
-- Mathlib.Tactic.MoveAdd
/-- Recursively compute the Array of `getAddends` Arrays by recursing into the expression `sum`
looking for instances of the operation `op`.

Possibly returns duplicates!
 -/
Mathlib.MoveAdd.getOps : Lean.Name → Lean.Expr → Lean.MetaM (Array (Array Lean.Expr × Lean.Expr))
-- Mathlib.Algebra.Divisibility.Units
/-- Units of a monoid divide any element of the monoid.  -/
IsUnit.dvd : ∀ {α : Type u_1} [inst : Monoid α] {a u : α}, IsUnit u → u ∣ a
-- Mathlib.Order.DirSupClosed
DirSupInacc.of_inter_subset : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  (∀ ⦃d : Set α⦄,
      d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s) →
    DirSupInacc s
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- A left rigid monoidal category is one in which every object has a right dual.  -/
CategoryTheory.LeftRigidCategory : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)