mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.comp_symm_cancel_right : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₂₃ : R₂ →+* R₃} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃]
  (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₂ →ₛₗ[σ₂₃] M₃), (f ∘ₛₗ ↑e) ∘ₛₗ ↑e.symm = f
-- Init.Data.Array.Nat
Array.sum_pos_iff_exists_pos_nat : ∀ {xs : Array ℕ}, 0 < xs.sum ↔ ∃ x ∈ xs, 0 < x
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_toAddMonoidHomEquiv : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M),
  ⇑(AddChar.toAddMonoidHomEquiv ψ) = ⇑Additive.ofMul ∘ ⇑ψ
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.single.congr_simp : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R]
  (x x_1 : M), x = x_1 → Convexity.StdSimplex.single x = Convexity.StdSimplex.single x_1
-- Mathlib.Geometry.Manifold.Notation
/-- `UniqueMDiff[s]` elaborates to `UniqueMDiffOn I s`,
trying to determine `I` from the local context.  -/
Manifold.«termUniqueMDiff[_]» : Lean.ParserDescr
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.add_assoc : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a b c : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.add (Lean.Grind.IntModule.OfNatModule.add a b) c =
    Lean.Grind.IntModule.OfNatModule.add a (Lean.Grind.IntModule.OfNatModule.add b c)
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordMonoidWithZeroHom_eq_ordMonoidHom : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : Ring.KrullDimLE 1 R]
  [inst_3 : Nontrivial R] (x : ↥(nonZeroDivisors R)),
  ↑(Multiplicative.ofAdd ↑(Multiplicative.toAdd (Ring.ordMonoidHom x))) = (Ring.ordMonoidWithZeroHom R) ↑x
-- Mathlib.RingTheory.Congruence.Hom
RingCon.quotientQuotientEquivQuotientₐ_coe_coe : ∀ {M : Type u_1} (R : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M] {c d : RingCon M}
  (h : c ≤ d) (x : M), (RingCon.quotientQuotientEquivQuotientₐ R h) ↑↑x = ↑x
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendHomologyIso_inv_homologyι_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'] {Z : C}
  (h : (K.extend e).opcycles j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').inv
      (CategoryTheory.CategoryStruct.comp ((K.extend e).homologyι j') h) =
    CategoryTheory.CategoryStruct.comp (K.homologyι j)
      (CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hj').inv h)
-- Mathlib.Tactic.Linter.FindDeprecations
/-- The `<` partial order on modules: `importLT env mod₁ mod₂` means that `mod₂` imports `mod₁`.  -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.importLT : Lean.Environment → Lean.Name → Lean.Name → Bool
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadIso.mk_hom_toNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Monad C}
  (f : M.toFunctor ≅ N.toFunctor)
  (f_η :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (M.η.app X) (f.hom.app X) = N.η.app X)
      CategoryTheory.MonadIso.mk._auto_1)
  (f_μ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (M.μ.app X) (f.hom.app X) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) (N.μ.app X))
      CategoryTheory.MonadIso.mk._auto_3),
  (CategoryTheory.MonadIso.mk f f_η f_μ).hom.toNatTrans = f.hom
-- Mathlib.Order.Birkhoff
/-- **Birkhoff Representation for partial orders.** Any partial order is isomorphic
to the partial order of sup-irreducible elements in its lattice of lower sets.  -/
OrderIso.supIrredLowerSet : {α : Type u_1} → [inst : PartialOrder α] → [Finite α] → α ≃o { s // SupIrred s }
-- Init.Data.UInt.Basic
/-- Bitwise right shift for 64-bit unsigned integers. Usually accessed via the `>>>` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.shiftRight : UInt64 → UInt64 → UInt64
-- Mathlib.Data.Nat.Pairing
iInf_unpair : ∀ {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → ℕ → α), ⨅ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⨅ i, ⨅ j, f i j
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
/-- See `lt_tsub_iff_left` for a stronger statement in a linear order.  -/
lt_tsub_iff_left_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], c ≤ b → (a < b - c ↔ c + a < b)
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicInterior_nonempty : ∀ {V : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {s : Set V},
  Convex ℝ s → ((intrinsicInterior ℝ s).Nonempty ↔ s.Nonempty)
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.vadd_const : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : VAdd M X] {m : MeasurableSpace α}
  {f : α → M} [inst_2 : MeasurableSpace M] [MeasurableVAdd M X], Measurable f → ∀ (y : X), Measurable fun x => f x +ᵥ y
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {k a : α} {fallback : β a} {v : β k},
      (m.insert k v).getD a fallback = if h : (k == a) = true then cast ⋯ v else m.getD a fallback
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
Matrix.IsReducedRowEchelon.isRowEchelon : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} [inst : Zero R] [inst_1 : LT m] [inst_2 : LT n] [inst_3 : One R]
  {A : Matrix m n R}, A.IsReducedRowEchelon → A.IsRowEchelon
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instIsGEObjιOfIsGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory.Plus C) (n : ℤ) [X.IsGE n], (DerivedCategory.Plus.ι.obj X).IsGE n
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- The pseudoelement induced by an arrow is zero precisely when that arrow is zero.  -/
CategoryTheory.Abelian.Pseudoelement.pseudoZero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P : C}
  (a : CategoryTheory.Over P), Quot.mk (CategoryTheory.Abelian.PseudoEqual P) a = 0 ↔ a.hom = 0
-- Mathlib.Order.Heyting.Basic
himp_triangle : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b c : α), (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c
-- Mathlib.Condensed.Light.Monoidal
LightCondensed.instMonoidalLightCondSetLightCondModFree : (R : Type u) → [inst : CommRing R] → (LightCondensed.free R).Monoidal
-- Mathlib.Combinatorics.Graph.Basic
Graph.Adj.right_mem : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β}, G.Adj x y → y ∈ G.vertexSet
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.IsNaturalSMul.naturality : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {F : CategoryTheory.Functor C FintypeCat} {G : Type u_1}
  {inst_1 : Group G} {inst_2 : (X : C) → MulAction G (F.obj X).obj}
  [self : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] (g : G) {X Y : C} (f : X ⟶ Y) (x : (F.obj X).obj),
  (CategoryTheory.ConcreteCategory.hom (F.map f)) (g • x) = g • (CategoryTheory.ConcreteCategory.hom (F.map f)) x
-- Init.Data.List.TakeDrop
List.dropWhile_cons : ∀ {α : Type u_1} {x : α} {xs : List α} {p : α → Bool},
  List.dropWhile p (x :: xs) = if p x = true then List.dropWhile p xs else x :: xs
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.limitCommMonoid : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommMonCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] →
        CommMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommMonCat))).pt
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.equivQuotientZSMulOfEquiv_refl : ∀ {A : Type u} [inst : AddCommGroup A] (n : ℤ),
  AddEquiv.refl (A ⧸ (zsmulAddGroupHom n).range) = QuotientAddGroup.equivQuotientZSMulOfEquiv (AddEquiv.refl A) n
-- Init.Data.Range.Polymorphic.Fin
Fin.instLawfulUpwardEnumerableLT : ∀ {n : ℕ}, Std.PRange.LawfulUpwardEnumerableLT (Fin n)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_filter_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {f : α → β → Bool} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.filter f t) k =
        (Option.filter (fun x => f k' x) (Std.DTreeMap.Raw.Const.get? t k)).get!
-- Mathlib.LinearAlgebra.TensorProduct.Free
Algebra.TensorProduct.equivPiOfFiniteBasis_symm_apply : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommSemiring A] [inst_1 : CommSemiring R] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] {ι : Type u_4} (b : Module.Basis ι R V) [inst_5 : Finite ι]
  (a : ι → A),
  (Algebra.TensorProduct.equivPiOfFiniteBasis A b).symm a =
    (LinearEquiv.baseChange R A V (ι → R) b.equivFun).symm ((TensorProduct.piScalarRight R A A ι).symm a)
-- Mathlib.Data.Set.Lattice
Set.iUnion_range_eq_sUnion : ∀ {α : Type u_12} {β : Type u_13} (C : Set (Set α)) {f : (s : ↑C) → β → ↑↑s},
  (∀ (s : ↑C), Function.Surjective (f s)) → (⋃ y, Set.range fun s => ↑(f s y)) = ⋃₀ C
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.min?_mem : ∀ {α : Type u_1} {a : α} {t : RBTree.RBNode α}, t.min? = some a → a ∈ t
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.instIsIntegralToSchemeOfNonemptyCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {U : X.Opens} [Nonempty ↥↑U],
  AlgebraicGeometry.IsIntegral ↑U
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_sq_le_normSq : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.im z * RCLike.im z ≤ RCLike.normSq z
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.liftQ_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ f.ker), p.liftQ f h ∘ₛₗ p.mkQ = f
-- Mathlib.RingTheory.Ideal.Quotient.Operations
RingHom.quotientKerEquivOfRightInverse.Symm.apply : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} {g : S → R}
  (hf : Function.RightInverse g ⇑f) (x : S),
  (RingHom.quotientKerEquivOfRightInverse hf).symm x = (Ideal.Quotient.mk (RingHom.ker f)) (g x)
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Regular C] {A B : C} (f : A ⟶ B)
  (A' : CategoryTheory.Subobject A) (B' : CategoryTheory.Subobject B),
  (CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation f A' B').e =
    CategoryTheory.Regular.frobeniusMorphism f A' B'
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.injective : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [Nontrivial R], Function.Injective ⇑b
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_join : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) {S : Stream'.WSeq (Stream'.WSeq α)} {T : Stream'.WSeq (Stream'.WSeq β)},
  Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T → Stream'.WSeq.LiftRel R S.join T.join
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.false_of_from_star' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C}
  (f : CategoryTheory.WithTerminal.star.Hom (CategoryTheory.WithTerminal.of X)), False
-- Mathlib.LinearAlgebra.SymplecticGroup
Matrix.map_J : ∀ (l : Type u_1) {R : Type u_2} [inst : DecidableEq l] [inst_1 : CommRing R] {F : Type u_3} {S : Type u_4}
  [inst_2 : CommRing S] [inst_3 : FunLike F R S] [AddMonoidHomClass F R S] [OneHomClass F R S] (f : F),
  (Matrix.J l R).map ⇑f = Matrix.J l S
-- Mathlib.Data.PNat.Factors
PNat.mem_factorMultiset : ∀ {p n : ℕ+}, p ∈ n.factorMultiset.toPNatMultiset ↔ p.Prime ∧ p ∣ n
-- Mathlib.Topology.Baire.CompleteMetrizable
/-- **First Baire theorem**: a completely pseudometrizable topological space has Baire property.  -/
BaireSpace.of_completelyPseudoMetrizable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X], BaireSpace X
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_of_nonpos : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  autoParam (a ≤ 0) CFC.abs_of_nonpos._auto_1 → CFC.abs a = -a
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Substructure.models_of_isUniversal : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S : L.Substructure M) (T : L.Theory) [T.IsUniversal]
  [M ⊨ T], ↥S ⊨ T
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.iInter : ∀ {ι : Sort u_1} {α : Type u_2} [inst : LE α] {f : ι → Set α},
  (∀ (i : ι), CountableSupClosed (f i)) → CountableSupClosed (⋂ i, f i)
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {w : σ → ℕ} {f : MvPowerSeries σ R} {p : ℕ},
  ↑p < MvPowerSeries.weightedOrder w f → (MvPowerSeries.weightedHomogeneousComponent w p) f = 0
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.isUniformInducing_comp : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {δ : Type u_2}
  [inst_2 : UniformSpace δ] (g : C(β, δ)), IsUniformInducing ⇑g → IsUniformInducing g.comp
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientMapOfLE_apply_mk : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (h : s ≤ t) (g : α), AddSubgroup.quotientMapOfLE h ↑g = ↑g
-- Mathlib.Data.Set.Basic
Set.univ_nonempty : ∀ {α : Type u} [Nonempty α], Set.univ.Nonempty
-- Mathlib.Topology.Order.HullKernel
PrimitiveSpectrum.hull_kernel_of_isClosed : ∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α} [inst_1 : TopologicalSpace α] [Topology.IsLower α],
  (∀ p ∈ T, InfPrime p) →
    PrimitiveSpectrum.OrderGenerates T →
      ∀ {C : Set ↑T}, IsClosed C → PrimitiveSpectrum.hull T (PrimitiveSpectrum.kernel C) = C
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.add_nonpos : ∀ {α : Type u} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {a b : α}, a ≤ 0 → b ≤ 0 → a + b ≤ 0
-- Init.Data.UInt.Bitwise
UInt64.shiftLeft_zero : ∀ {a : UInt64}, a <<< 0 = a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {f : (a : α) → β a → Bool} {k : α},
  (Std.ExtDTreeMap.filter f t).getKey! k = ((t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)).get!
-- Mathlib.Topology.Algebra.MulAction
Units.continuousSMul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : Monoid M]
  [inst_3 : MulAction M X] [ContinuousSMul M X], ContinuousSMul Mˣ X
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instAddCommGroup : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] →
          [inst_3 : AddCommGroup R] → [IsTopologicalAddGroup R] → AddCommGroup (ContinuousMapZero X R)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.im_star : ∀ (z : Complex.UnitDisc), (star z).im = -z.im
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.closure_eq_of_le : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {t : NonUnitalSubring R},
  s ⊆ ↑t → t ≤ NonUnitalSubring.closure s → NonUnitalSubring.closure s = t
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.reindex_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [inst : AddGroup G] (b : FreeAddGroupBasis ι G) (e : ι ≃ ι') (x : ι'),
  (b.reindex e) x = b (e.symm x)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcycles_opcyclesIsoSc'_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (K.opcyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).pOpcycles
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulEquiv.subsemigroupMap_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : ↥S),
  ↑((e.subsemigroupMap S) x) = e ↑x
-- Lean.Data.PersistentArray
Lean.PersistentArray.forMAux : {α : Type u} → {m : Type v → Type w} → [Monad m] → (α → m PUnit.{v + 1}) → Lean.PersistentArrayNode α → m PUnit.{v + 1}
-- Mathlib.Data.List.Basic
List.length_erase_add_one : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∈ l → (l.erase a).length + 1 = l.length
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instIsGoodTrans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  [inst_2 : HomotopicalAlgebra.IsFibrant A] (P P' : HomotopicalAlgebra.PathObject A) [P.IsGood] [inst_4 : P'.IsGood],
  (P.trans P').IsGood
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instMulActionOfIsScalarTower : {M : Type u_3} →
  {X : Type u_4} →
    [inst : Monoid M] →
      {S : Submonoid M} →
        [inst_1 : OreLocalization.OreSet S] →
          [inst_2 : MulAction M X] →
            {R : Type u_5} →
              [inst_3 : Monoid R] →
                [inst_4 : MulAction R M] →
                  [IsScalarTower R M M] →
                    [inst_6 : MulAction R X] → [IsScalarTower R M X] → MulAction R (OreLocalization S X)
-- Mathlib.ModelTheory.PartialEquiv
/-- A partial equivalence as an embedding from its domain.  -/
FirstOrder.Language.PartialEquiv.toEmbedding : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → (f : L.PartialEquiv M N) → L.Embedding (↥f.dom) N
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Morphisms between direct sums are matrices.  -/
CategoryTheory.Limits.biproduct.matrixEquiv : {J : Type} →
  [inst : Finite J] →
    {K : Type} →
      [inst_1 : Finite K] →
        {C : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} C] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] →
                {f : J → C} → {g : K → C} → (⨁ f ⟶ ⨁ g) ≃ ((j : J) → (k : K) → f j ⟶ g k)
-- Mathlib.Analysis.Normed.Module.Span
ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {x : E} (h : x ≠ 0), ⇑(ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h).symm = ⇑(ContinuousLinearEquiv.coord 𝕜 x h)
-- Mathlib.Order.Comparable
IncompRel.ne : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {a b : α}, IncompRel r a b → a ≠ b
-- Std.Http.Data.URI.Basic
Std.Http.URI.instBEqPath : BEq Std.Http.URI.Path
-- Init.Data.Array.Lemmas
Array.back_append_right : ∀ {α : Type u_1} {xs ys : Array α} (h : 0 < ys.size), (xs ++ ys).back ⋯ = ys.back h
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.of_card_le_one : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G},
  A.Nonempty → B.Nonempty → A.card ≤ 1 → B.card ≤ 1 → ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
-- Mathlib.Combinatorics.Configuration
Configuration.lineCount.eq_1 : ∀ {P : Type u_1} (L : Type u_2) [inst : Membership P L] (p : P), Configuration.lineCount L p = Nat.card { l // p ∈ l }
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_comp : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} {E : Type uE} {F : Type uF}
  [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A]
  [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B]
  [inst_9 : Semiring C] [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C]
  [inst_13 : Semiring D] [inst_14 : Algebra R D] [inst_15 : Semiring E] [inst_16 : Algebra R E] [inst_17 : Algebra S E]
  [inst_18 : IsScalarTower R S E] [inst_19 : Semiring F] [inst_20 : Algebra R F] (f₂ : C →ₐ[S] E) (f₁ : A →ₐ[S] C)
  (g₂ : D →ₐ[R] F) (g₁ : B →ₐ[R] D),
  Algebra.TensorProduct.map (f₂.comp f₁) (g₂.comp g₁) =
    (Algebra.TensorProduct.map f₂ g₂).comp (Algebra.TensorProduct.map f₁ g₁)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.pointwiseCentralScalar : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] [inst_6 : DistribMulAction αᵐᵒᵖ M]
  [inst_7 : SMulCommClass αᵐᵒᵖ R M] [IsCentralScalar α M], IsCentralScalar α (Submodule R M)
-- Mathlib.Topology.Order.LiminfLimsup
/-- Every cluster point `x` of a function `u` along a filter `f` is greater than or equal to
`liminf u f`.  -/
MapClusterPt.liminf_le : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] {u : β → α} {f : Filter β} {x : α},
  MapClusterPt x f u →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) MapClusterPt.liminf_le._auto_1 → Filter.liminf u f ≤ x
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.isCDotBinderKind : Lean.SyntaxNodeKind → Bool
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
/-- The dynamical entourage associated to a transformation `T`, entourage `U` and time `n`
is the entourage where `x` and `y` are close iff `T^[k] x` and `T^[k] y` are `U`-close
for all `k < n`, i.e. iff they are `U`-close up to time `n`.  -/
Dynamics.dynEntourage : {X : Type u_1} → (X → X) → SetRel X X → ℕ → SetRel X X
-- Mathlib.Order.Concept
/-- **Alias** of the forward direction of `Order.isExtent_iff`. -/
Order.IsExtent.eq : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α}, Order.IsExtent r s → lowerPolar r (upperPolar r s) = s
-- Lean.ScopedEnvExtension
Lean.popScope : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [MonadLiftT (ST IO.RealWorld) m] → m Unit