mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Environment
/-- Like `findAsync` but blocks on everything but the constant's body (if any), which is not accessible
through the result.
 -/
Lean.Environment.findConstVal? : Lean.Environment → Lean.Name → optParam Bool false → Option Lean.ConstantVal
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map_monotone : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} {f : G →g G'},
  Monotone (SimpleGraph.Subgraph.map f)
-- Mathlib.RingTheory.Ideal.Span
Ideal.mem_span_pair : ∀ {α : Type u} [inst : Semiring α] {x y z : α}, z ∈ Ideal.span {x, y} ↔ ∃ a b, a * x + b * y = z
-- Mathlib.Algebra.Polynomial.Div
Polynomial.sub_dvd_eval_sub : ∀ {R : Type u} [inst : CommRing R] (a b : R) (p : Polynomial R), a - b ∣ Polynomial.eval a p - Polynomial.eval b p
-- Mathlib.Analysis.Calculus.LHopital
HasDerivAt.lhopital_zero_left_on_Ioc : ∀ {a b : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  a < b →
    (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) →
        ContinuousOn f (Set.Ioc a b) →
          ContinuousOn g (Set.Ioc a b) →
            (∀ x ∈ Set.Ioo a b, g' x ≠ 0) →
              f b = 0 →
                g b = 0 →
                  Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin b (Set.Iio b)) l →
                    Filter.Tendsto (fun x => f x / g x) (nhdsWithin b (Set.Iio b)) l
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.baseChange_add : ∀ {R : Type r} {S : Type s} {F : Type u} {K : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field F]
  [inst_3 : Field K] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R F]
  [inst_6 : Algebra S F] [IsScalarTower R S F] [inst_8 : Algebra R K] [inst_9 : Algebra S K] [IsScalarTower R S K]
  (f : F →ₐ[S] K) {P Q : Fin 3 → F},
  (W'.baseChange F).Nonsingular P →
    (W'.baseChange F).Nonsingular Q → (W'.baseChange K).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (W'.baseChange F).add P Q
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.colimitAdjunction.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR),
  PresheafOfModules.colimitAdjunction hcR =
    CategoryTheory.Adjunction.mkOfHomEquiv
      {
        homEquiv := fun x x_1 =>
          (PresheafOfModules.ModuleColimit.homEquiv hcR (CategoryTheory.Limits.colimit.isColimit x.presheaf)).toEquiv,
        homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_apply_ne : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (i j : n), i ≠ j → M.charmatrix i j = -Polynomial.C (M i j)
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The universal lift from a morphism `R →* T`, which maps elements of `S` to units of `T`,
to a morphism `R[S⁻¹] →* T`.  -/
OreLocalization.universalMulHom : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {T : Type u_2} →
          [inst_2 : Monoid T] → (f : R →* T) → (fS : ↥S →* Tˣ) → (∀ (s : ↥S), f ↑s = ↑(fS s)) → OreLocalization S R →* T
-- Mathlib.Algebra.Group.Defs
AddGroup.toAddCancelMonoid.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  AddGroup.toAddCancelMonoid = { toAddMonoid := inst.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
-- Lean.Elab.PreDefinition.Structural.Basic
/-- Groups the `xs` by their `f` value, and puts these groups into the order given by `ys`.
 -/
Lean.Elab.Structural.Positions.groupAndSort : {α : Type u_1} →
  {β : Type u_2} → [Inhabited α] → [DecidableEq β] → (α → β) → Array α → Array β → Lean.Elab.Structural.Positions
-- Mathlib.Topology.UniformSpace.Equicontinuity
UniformEquicontinuous.eq_1 : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] (F : ι → β → α),
  UniformEquicontinuous F = ∀ U ∈ uniformity α, ∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U
-- Mathlib.Data.Finsupp.SMul
Finsupp.comapSMul_def : ∀ {α : Type u_1} {M : Type u_3} {G : Type u_5} [inst : Monoid G] [inst_1 : MulAction G α] [inst_2 : AddCommMonoid M]
  (g : G) (f : α →₀ M), g • f = Finsupp.mapDomain (fun x => g • x) f
-- Init.Data.String.Basic
String.Slice.Pos.next_le_of_lt : ∀ {s : String.Slice} {p q : s.Pos} {h : p ≠ s.endPos}, p < q → p.next h ≤ q
-- Std.Async.Basic
Std.Async.EAsync.instMonadAsyncETask : {ε : Type} → Std.Async.MonadAsync (Std.Async.ETask ε) (Std.Async.EAsync ε)
-- Mathlib.Algebra.Order.Field.Power
zpow_eq_zpow_iff_cases₀ : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {n : ℤ},
  a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
/-- The isomorphism between `Gal(ℚ(ζₙ)/ℚ)` and `(ℤ/nℤ)ˣ` that sends `σ` to the class `a` such that
`σ (ζₙ) = ζₙ ^ a`.
 -/
IsCyclotomicExtension.Rat.galEquivZMod : (n : ℕ) →
  [NeZero n] →
    (K : Type u_1) →
      [inst : Field K] → [inst_1 : NumberField K] → [hK : IsCyclotomicExtension {n} ℚ K] → Gal(K/ℚ) ≃* (ZMod n)ˣ
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {f : α → β} {g : β → γ},
  MeasurableSpace.map g (MeasurableSpace.map f m) = MeasurableSpace.map (g ∘ f) m
-- Init.Data.Nat.Gcd
Nat.gcd_ne_zero_left : ∀ {m n : ℕ}, m ≠ 0 → m.gcd n ≠ 0
-- Mathlib.CategoryTheory.Monad.Coequalizer
/-- The bottom map in the coequalizer diagram we will construct.  -/
CategoryTheory.Monad.FreeCoequalizer.bottomMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} → (X : T.Algebra) → T.free.obj (T.obj X.A) ⟶ T.free.obj X.A
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.map_val_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N) {n : ℕ} (x : AdicCompletion I M),
  ↑((AdicCompletion.map I f) x) n = (LinearMap.reduceModIdeal (I ^ n) f) (↑x n)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_union : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t₁ t₂ : Set β}, s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.comp_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D)
  {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (F.comp G).mapComp f g = G.map₂Iso (F.mapComp f g) ≪≫ G.mapComp (F.map f) (F.map g)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.coe_zpow : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : SpecialLinearGroup R V) (m : ℤ), ↑(A ^ m) = ↑A ^ m
-- Mathlib.GroupTheory.GroupAction.CardCommute
/-- **Class formula** for a finite group acting on a finite type.  -/
AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer : ∀ (α : Type u_1) (β : Type u_2) [inst : AddGroup α] [inst_1 : AddAction α β] [inst_2 : Fintype α] [inst_3 : Fintype β]
  [inst_4 : Fintype (Quotient (AddAction.orbitRel α β))] [inst_5 : (b : β) → Fintype ↥(AddAction.stabilizer α b)],
  Fintype.card β = ∑ ω, Fintype.card α / Fintype.card ↥(AddAction.stabilizer α ω.out)
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.eq_1 : ∀ (n : ℕ) (i : Fin (n + 1)),
  SSet.horn n i = { obj := fun x => {s | Set.range ⇑(SSet.stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}, map := ⋯ }
-- Mathlib.Algebra.Category.Grp.Limits
/-- The projection from `Functor.sections` to a factor as a `MonoidHom`.  -/
GrpCat.sectionsπMonoidHom : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J GrpCat) → (j : J) → ↑(F.comp (CategoryTheory.forget GrpCat)).sections →* ↑(F.obj j)
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_eqOn_iff : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] [IsRCLikeNormedField 𝕜] {f g : 𝕜 → 𝕜'} {s : Set 𝕜},
  DifferentiableOn 𝕜 f s →
    DifferentiableOn 𝕜 g s →
      IsOpen s →
        IsPreconnected s →
          (∀ x ∈ s, g x ≠ 0) →
            (∀ x ∈ s, f x ≠ 0) → (Set.EqOn (logDeriv f) (logDeriv g) s ↔ ∃ z, z ≠ 0 ∧ Set.EqOn f (z • g) s)
-- Mathlib.Topology.Order.LeftRightNhds
nhds_basis_Icc_pos : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α] [IsOrderedAddMonoid α]
  [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] (a : α),
  (nhds a).HasBasis (fun x => 0 < x) fun ε => Set.Icc (a - ε) (a + ε)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup_coe_apply : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {g : M} (hg : g +ᵥ t = s)
  (x : ↥(fixingAddSubgroup M t)), ↑((SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup hg) x) = (AddAut.addConj g) ↑x
-- Mathlib.Data.ULift
PLift.instDecidableEq_mathlib : {α : Sort u} → [DecidableEq α] → DecidableEq (PLift α)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
/-- The symmetric difference of two Hahn decompositions has measure zero.  -/
MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i j : Set α},
  MeasurableSet i →
    MeasurableSet j →
      MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧
          MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ →
        MeasureTheory.VectorMeasure.restrict 0 j ≤ MeasureTheory.VectorMeasure.restrict s j ∧
            MeasureTheory.VectorMeasure.restrict s jᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 jᶜ →
          s (symmDiff i j) = 0 ∧ s (symmDiff iᶜ jᶜ) = 0
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.uniqueHomFromTrivial_default_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C), default.hom = CategoryTheory.AddMonObj.zero
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.isPullback_SpecMap_pushout : ∀ {A B C : CommRingCat} (f : A ⟶ B) (g : A ⟶ C),
  CategoryTheory.IsPullback (AlgebraicGeometry.Spec.map (CategoryTheory.Limits.pushout.inl f g))
    (AlgebraicGeometry.Spec.map (CategoryTheory.Limits.pushout.inr f g)) (AlgebraicGeometry.Spec.map f)
    (AlgebraicGeometry.Spec.map g)
-- Mathlib.MeasureTheory.Function.UnifTight
/-- A single function is tight.  -/
MeasureTheory.unifTight_of_subsingleton : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} [Subsingleton ι],
  p ≠ ⊤ → ∀ {f : ι → α → β}, (∀ (i : ι), MeasureTheory.MemLp (f i) p μ) → MeasureTheory.UnifTight f p μ
-- Init.Core
/-- Modus ponens for if and only if. If `a ↔ b` and `a`, then `b`.  -/
Iff.mp : ∀ {a b : Prop}, (a ↔ b) → a → b
-- Mathlib.Algebra.Algebra.Unitization
/-- Non-unital star algebra homomorphisms from `A` into a unital star `R`-algebra `C` lift uniquely
to `Unitization R A →⋆ₐ[R] C`. This is the universal property of the unitization.  -/
Unitization.starLift : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : NonUnitalSemiring A] →
            [inst_3 : StarRing A] →
              [inst_4 : Module R A] →
                [inst_5 : SMulCommClass R A A] →
                  [inst_6 : IsScalarTower R A A] →
                    [inst_7 : Semiring C] →
                      [inst_8 : Algebra R C] →
                        [inst_9 : StarRing C] → [StarModule R C] → (A →⋆ₙₐ[R] C) ≃ (Unitization R A →⋆ₐ[R] C)
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.realUnits.eq_1 : ∀ (K : Type u_1) [inst : Field K],
  NumberField.IsCMField.realUnits K =
    (Units.map
        ↑(algebraMap (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K))
            (NumberField.RingOfIntegers K))).range
-- Mathlib.ModelTheory.Order
/-- The theory of dense linear orders is `ℵ₀`-categorical.  -/
FirstOrder.Language.aleph0_categorical_dlo : Cardinal.aleph0.Categorical FirstOrder.Language.order.dlo
-- Mathlib.Order.Sublattice
Sublattice.apply_coe_mem_map : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} (f : LatticeHom α β)
  (a : ↥L), f ↑a ∈ Sublattice.map f L
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_one_left_eq_zero : Real.logb 1 = 0
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousOn.sup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {s : Set α} {r' : α → β → Prop},
  SemicontinuousOn r s → SemicontinuousOn r' s → SemicontinuousOn (r ⊔ r') s
-- Lean.Parser.Command
Lean.Parser.Command.import.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Notation.Prod
Prod.snd_star : ∀ {R : Type u_6} {S : Type u_7} [inst : Star R] [inst_1 : Star S] (x : R × S), (star x).2 = star x.2
-- Mathlib.RingTheory.WittVector.StructurePolynomial
/-- Write `wittStructureRat p φ n` in terms of `wittStructureRat p φ i` for `i < n`.  -/
wittStructureRat_rec : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) (n : ℕ),
  wittStructureRat p Φ n =
    MvPolynomial.C (1 / ↑p ^ n) *
      ((MvPolynomial.bind₁ fun b => (MvPolynomial.rename fun i => (b, i)) (wittPolynomial p ℚ n)) Φ -
        ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))
-- Mathlib.RingTheory.FiniteType
/-- An additive group `G` is finitely generated if and only if `R[G]` is of
finite type.  -/
AddMonoidAlgebra.finiteType_iff_group_fg : ∀ {R : Type u_1} {G : Type u_3} [inst : AddGroup G] [inst_1 : CommRing R] [Nontrivial R],
  Algebra.FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.FG G
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.comp_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G)
  (adj₂ : H ⊣ I),
  (adj₁.comp adj₂).homEquiv = fun x x_1 => (adj₂.homEquiv (F.obj x) x_1).trans (adj₁.homEquiv x (I.obj x_1))
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.isClosed : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Clopens α), IsClosed ↑s
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote.eq_2 : ∀ (ctx : Int.Internal.Linear.Context) (k : ℤ) (v : Int.Internal.Linear.Var) (p_2 : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote ctx (Int.Internal.Linear.Poly.add k v p_2) =
    k * Int.Internal.Linear.Var.denote ctx v + Int.Internal.Linear.Poly.denote ctx p_2
-- Init.Data.UInt.Lemmas
UInt32.toNat_toUSize : ∀ (x : UInt32), x.toUSize.toNat = x.toNat
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.normal : ∀ (R : Type u_1) (K : Type u_2) [inst : Field R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsAlgClosure R K],
  Normal R K
-- Init.Data.Vector.Lemmas
Vector.take_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) {i : ℕ}, (Vector.mk xs h).take i = Vector.mk (xs.take i) ⋯
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.instCountableSubtypeMulOppositeMemOp : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G) [Countable ↥H], Countable ↥H.op
-- Mathlib.Topology.Separation.Basic
r1Space_iff_specializes_or_disjoint_nhds : ∀ (X : Type u_3) [inst : TopologicalSpace X], R1Space X ↔ ∀ (x y : X), x ⤳ y ∨ Disjoint (nhds x) (nhds y)
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `one_lt_of_gt`. -/
LT.lt.one_lt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α] [inst_1 : One α] [IsBotOneClass α], a < b → 1 < b
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.isDenseInducing : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → DenseRange f → IsDenseInducing f
-- Mathlib.Data.Nat.Choose.Central
/-- A crucial lemma to ensure that Catalan numbers can be defined via their explicit formula
`catalan n = n.centralBinom / (n + 1)`.  -/
Nat.succ_dvd_centralBinom : ∀ (n : ℕ), n + 1 ∣ n.centralBinom
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.trunc_map : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : DecidableEq σ] [inst_1 : CommSemiring R]
  [inst_2 : CommSemiring S] (n : σ →₀ ℕ) (f : R →+* S) (p : MvPowerSeries σ R),
  (MvPowerSeries.trunc S n) ((MvPowerSeries.map f) p) = (MvPolynomial.map f) ((MvPowerSeries.trunc R n) p)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets.indepSets : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set (Set Ω)},
  ProbabilityTheory.iIndepSets s μ → ∀ {i j : ι}, i ≠ j → ProbabilityTheory.IndepSets (s i) (s j) μ
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.continuous_coe : ∀ {α : Type u} [inst : TopologicalSpace α], Continuous ConnectedComponents.mk
-- Mathlib.Order.Disjoint
Complementeds.hasCoeT : {α : Type u_1} → [inst : Lattice α] → [inst_1 : BoundedOrder α] → CoeTC (Complementeds α) α
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.d_of : ∀ {k G : Type u} [inst : CommRing k] {n : ℕ} (c : Fin (n + 1) → G),
  (Rep.standardComplex.d k G n) (MonoidAlgebra.single c 1) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) ((-1) ^ ↑p)
-- Mathlib.Data.Set.Image
Subtype.coe_image_of_subset : ∀ {α : Type u_1} {s t : Set α}, t ⊆ s → Subtype.val '' {x | ↑x ∈ t} = t
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.sum_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) {ι : Type u_6} (s : Finset ι) (f : ι → ρ.IntertwiningMap σ)
  (v : V), (∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.rightHomologyMap'_smul : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (a : R),
  CategoryTheory.ShortComplex.rightHomologyMap' (a • φ) h₁ h₂ =
    a • CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
CategoryTheory.hom_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f))
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_conjTranspose : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_14} [inst : Star α] (M : Matrix (m × o) (n × o) α) (k : o),
  M.conjTranspose.blockDiag k = (M.blockDiag k).conjTranspose
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- The **universal property** of the topology on the restricted product: a map from
`Πʳ i, [R i, A i]_[𝓕]` is continuous *iff* its restriction to each `Πʳ i, [R i, A i]_[𝓟 s]`
(with `𝓕 ≤ 𝓟 s`) is continuous.

See also `RestrictedProduct.continuous_dom_prod_left`.  -/
RestrictedProduct.continuous_dom : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)]
  {X : Type u_3} [inst_1 : TopologicalSpace X] {f : RestrictedProduct (fun i => R i) (fun i => A i) 𝓕 → X},
  Continuous f ↔ ∀ (S : Set ι) (hS : 𝓕 ≤ Filter.principal S), Continuous (f ∘ RestrictedProduct.inclusion R A hS)
-- Mathlib.Algebra.Group.Invertible.Basic
/-- This is the `Invertible` version of `Units.isUnit_mul_units`  -/
invertibleOfMulInvertible : {α : Type u} → [inst : Monoid α] → (a b : α) → [Invertible (a * b)] → [Invertible b] → Invertible a
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The weighted homogeneous components of a weighted homogeneous polynomial.  -/
MvPolynomial.weightedHomogeneousComponent_of_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M}
  [inst_2 : DecidableEq M] {m n : M} {p : MvPolynomial σ R},
  p ∈ MvPolynomial.weightedHomogeneousSubmodule R w n →
    (MvPolynomial.weightedHomogeneousComponent w m) p = if m = n then p else 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.hasAdditiveReduction_iff : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W : WeierstrassCurve K),
  WeierstrassCurve.HasAdditiveReduction R W ↔
    WeierstrassCurve.IsMinimal R W ∧
      (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ < 1 ∧
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.c₄ < 1
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsIntegral.isAlgebraic : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R]
  [Algebra.IsIntegral R A], Algebra.IsAlgebraic R A
-- Lean.Data.PersistentArray
Lean.PersistentArray.forMFrom0 : {α : Type u} → {m : Type v → Type w} → [Monad m] → Lean.PersistentArray α → (α → m PUnit.{v + 1}) → m PUnit.{v + 1}
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.arrowCongrLeft_apply : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} [inst : Inhabited γ] (e : α ↪ β) (f : α → γ),
  e.arrowCongrLeft f = Function.extend (⇑e) f default
-- Mathlib.Probability.CondVar
ProbabilityTheory.integrable_condVar : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  MeasureTheory.Integrable (ProbabilityTheory.condVar m X μ) μ
-- Lean.Elab.MutualInductive
/-- Returns true if all elements of the `mutual` block (`Lean.Parser.Command.mutual`) are inductive declarations.
 -/
Lean.Elab.Command.isMutualInductive : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Syntax → m Bool
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.mkPiRing_coeff_eq : ∀ {𝕜 : Type u} {E : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ),
  ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n) = p n
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.Functor C V} (h h' : CategoryTheory.MonoidalCategory.DayConvolution F G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.unit F G)
      ((CategoryTheory.MonoidalCategory.tensor C).whiskerLeft (h.uniqueUpToIso h').hom) =
    CategoryTheory.MonoidalCategory.DayConvolution.unit F G