mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_sub_right : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Sub β] [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.IndepFun (f i) (f j - f k) μ
-- Mathlib.RingTheory.Polynomial.GaussNorm
/-- If `v` is a nonnegative nonarchimedean function with `v 0 = 0` and `c` is nonnegative, the
Gauss norm is nonarchimedean.  -/
Polynomial.isNonarchimedean_gaussNorm : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) [ZeroHomClass F R ℝ]
  [NonnegHomClass F R ℝ], IsNonarchimedean ⇑v → ∀ {c : ℝ}, 0 ≤ c → IsNonarchimedean (Polynomial.gaussNorm v c)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_cubic_le : ∀ {R : Type u} {a b c d : R} [inst : Semiring R],
  (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X +
        Polynomial.C d).degree ≤
    3
-- Mathlib.GroupTheory.CosetCover
Subspace.exists_eq_top_of_iUnion_eq_univ : ∀ {k : Type u_1} {E : Type u_2} [inst : DivisionRing k] [Infinite k] [inst_2 : AddCommGroup E] [inst_3 : Module k E]
  {ι : Sort u_3} [Finite ι] {p : ι → Subspace k E}, ⋃ i, ↑(p i) = Set.univ → ∃ i, p i = ⊤
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Functor.toReflPrefunctor.eq_1 : ∀ {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] (F : CategoryTheory.Functor C D),
  F.toReflPrefunctor = { obj := F.obj, map := @CategoryTheory.Functor.map C inst D inst_1 F, map_id := ⋯ }
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.norm_restrictScalars : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {𝕜' : Type u_1}
  [inst_6 : NontriviallyNormedField 𝕜'] [inst_7 : NormedAlgebra 𝕜' 𝕜] [inst_8 : NormedSpace 𝕜' F]
  [inst_9 : IsScalarTower 𝕜' 𝕜 F] [inst_10 : NormedSpace 𝕜' E] [inst_11 : IsScalarTower 𝕜' 𝕜 E],
  ‖ContinuousAlternatingMap.restrictScalars 𝕜' f‖ = ‖f‖
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.setTag.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (cidx : ℕ) (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_13) (fvarId_1 : Lean.FVarId)
  (cidx_1 : ℕ) (k_1 : Lean.Compiler.LCNF.Code pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_13),
  (Lean.Compiler.LCNF.Code.setTag fvarId cidx k h = Lean.Compiler.LCNF.Code.setTag fvarId_1 cidx_1 k_1 h_1) =
    (fvarId = fvarId_1 ∧ cidx = cidx_1 ∧ k = k_1)
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- A strong monomorphism that is an epimorphism is an isomorphism.  -/
CategoryTheory.isIso_of_epi_of_strongMono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} (f : Q ⟶ P) [CategoryTheory.Epi f]
  [CategoryTheory.StrongMono f], CategoryTheory.IsIso f
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.SemiCartesianMonoidalCategory.toUnit Y))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.fst X Y
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.vadd.eq_1 : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S),
  SetLike.vadd s = { vadd := fun r x => ⟨r +ᵥ ↑x, ⋯⟩ }
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Pull back a braiding along a fully faithful monoidal functor.  -/
CategoryTheory.BraidedCategory.ofFullyFaithful : {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] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [F.Monoidal] →
                [F.Full] → [F.Faithful] → [CategoryTheory.BraidedCategory D] → CategoryTheory.BraidedCategory C
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjectiveSpecialLinearGroup.toPGL_surj_of_roots : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R],
  (∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r) → Function.Surjective ⇑Matrix.ProjectiveSpecialLinearGroup.toPGL
-- Std.Internal.Do.WP.Basic
/-- Soundness for `ReaderM`: if `wp prog P r` holds, then `P` holds of `(prog.run r)`.  -/
Std.Internal.Do.ReaderM.of_wp_run_eq : ∀ {α ρ : Type} {x : α} {prog : ReaderM ρ α} {r : ρ},
  ReaderT.run prog r = x → ∀ (P : α → Prop), Std.Internal.Do.wp prog (fun a x => P a) epost⟨⟩ r → P x
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- Stereographic projection from the unit sphere in `E`, centred at a unit vector `v` in `E`;
this is the version as an open partial homeomorphism.  -/
stereographic : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] → {v : E} → ‖v‖ = 1 → OpenPartialHomeomorph ↑(Metric.sphere 0 1) ↥(ℝ ∙ v)ᗮ
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.of_finite : ∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] [inst_2 : Module R S] [IsScalarTower R S S]
  [IsArtinianRing R] [Module.Finite R S], IsArtinianRing S
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsFilteredOrEmptyProd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsFilteredOrEmpty C] [CategoryTheory.IsFilteredOrEmpty D], CategoryTheory.IsFilteredOrEmpty (C × D)
-- Mathlib.Algebra.Homology.Homotopy
/-- The composition of `C.d i (c.next i) ≫ f (c.next i) i`.  -/
dNext : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → (i : ι) → ((i j : ι) → C.X i ⟶ D.X j) →+ (C.X i ⟶ D.X i)
-- Init.Data.Float.Float
/-- Obtains the `Float` whose value is the same as the given `UInt16`.  -/
UInt16.toFloat : UInt16 → Float
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Functor.essImageDistTriang_mem_of_iso : ∀ {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] (L : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_6 : CategoryTheory.Pretriangulated C] [inst_7 : CategoryTheory.HasShift D ℤ] [inst_8 : L.CommShift ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle D} (e : T₂ ≅ T₁),
  T₁ ∈ L.essImageDistTriang → T₂ ∈ L.essImageDistTriang
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instZero : {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] → Zero (LieDerivation R L M)
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] {f g : sSupHom α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
MeasureTheory.instSFiniteForallValNatMemFinsetInducedFamilyOfForallIic : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)) [∀ (n : ℕ), MeasureTheory.SFinite (μ n)]
  (I : Finset ℕ), MeasureTheory.SFinite (MeasureTheory.inducedFamily μ I)
-- Mathlib.Analysis.Complex.Norm
Complex.norm_mul_self_eq_normSq : ∀ (z : ℂ), ‖z‖ * ‖z‖ = Complex.normSq z
-- Mathlib.Algebra.WithConv
WithConv.toAddEquiv_linearEquiv : ∀ {R : Type u_1} {A : Type u_2} [inst : AddCommMonoid A] [inst_1 : Semiring R] [inst_2 : Module R A],
  (WithConv.linearEquiv R A).toAddEquiv = WithConv.addEquiv A
-- Mathlib.Data.Finset.Fin
Finset.card_attachFin : ∀ {n : ℕ} (s : Finset ℕ) (h : ∀ m ∈ s, m < n), (s.attachFin h).card = s.card
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.im_ne_zero : ∀ (z : UpperHalfPlane), z.im ≠ 0
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.leftUnitor_def : ∀ {C : Type u} [inst : CategoryTheory.Bicategory C] (X : C) (f : X ⟶ X),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor f = CategoryTheory.Bicategory.leftUnitor f
-- Mathlib.Topology.Algebra.Module.Star
continuous_decomposeProdAdjoint_symm : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] [inst_8 : TopologicalSpace A] [ContinuousAdd A],
  Continuous ⇑(StarModule.decomposeProdAdjoint R A).symm
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comapₗ_eq_comap : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β),
  Function.Injective f →
    (∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)) →
      ∀ (μ : MeasureTheory.Measure β),
        MeasurableSet s → ((MeasureTheory.Measure.comapₗ f) μ) s = (MeasureTheory.Measure.comap f μ) s
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.comap_top : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), (MeasureTheory.OuterMeasure.comap f) ⊤ = ⊤
-- Mathlib.Data.Finset.Basic
Finset.disjoint_erase_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α},
  a ∉ s → (Disjoint (insert a s) (t.erase a) ↔ Disjoint s t)
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- Some approximation of the least fixed point starting from `⊥` is the least fixed point.  -/
OrdinalApprox.lfp_mem_range_lfpApprox : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), OrderHom.lfp f ∈ Set.range (OrdinalApprox.lfpApprox f ⊥)
-- Mathlib.RingTheory.PowerSeries.CoeffMulMem
PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' : ∀ {A : Type u_1} [inst : Semiring A] {I J : Ideal A} {f g : PowerSeries A},
  (∀ (i : ℕ), (PowerSeries.coeff i) f ∈ I) →
    (∀ (i : ℕ), (PowerSeries.coeff i) g ∈ J) → ∀ (i : ℕ), (PowerSeries.coeff i) (f * g) ∈ I * J
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negDblY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P : Fin 3 → R),
  W'.negDblY P = -W'.dblU P * (W'.dblX P - P 0 * (P 1 - W'.negY P) ^ 2) + P 1 * (P 1 - W'.negY P) ^ 3
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkGroup.flb : Std.Format.WorkGroup✝ → Std.Format.FlattenBehavior
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
conditionallyCompleteLatticeOfsSup.eq_1 : ∀ (α : Type u_5) [H1 : PartialOrder α] [H2 : SupSet α] (bddAbove_pair : ∀ (a b : α), BddAbove {a, b})
  (bddBelow_pair : ∀ (a b : α), BddBelow {a, b})
  (isLUB_sSup : ∀ (s : Set α), BddAbove s → s.Nonempty → IsLUB s (sSup s)),
  conditionallyCompleteLatticeOfsSup α bddAbove_pair bddBelow_pair isLUB_sSup =
    { toLattice := Lattice.ofIsLUBofIsGLB (fun a b => sSup {a, b}) (fun a b => sSup (lowerBounds {a, b})) ⋯ ⋯,
      toSupSet := H2, sInf := fun s => sSup (lowerBounds s), isLUB_csSup := ⋯, isGLB_csInf := ⋯ }
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioc_pred_right_eq_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] (a b : α), Set.Ioc a (Order.pred b) = Set.Ioo a b
-- Lean.Data.JsonRpc
Lean.JsonRpc.Request.mk.inj : ∀ {α : Type u} {id : Lean.JsonRpc.RequestID} {method : String} {param : α} {id_1 : Lean.JsonRpc.RequestID}
  {method_1 : String} {param_1 : α},
  { id := id, method := method, param := param } = { id := id_1, method := method_1, param := param_1 } →
    id = id_1 ∧ method = method_1 ∧ param = param_1
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_inv : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (a : M),
  MulArchimedeanClass.mk a⁻¹ = MulArchimedeanClass.mk a
-- Mathlib.Analysis.InnerProductSpace.NormPow
contDiff_norm_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {p : ℝ},
  1 < p → ContDiff ℝ 1 fun x => ‖x‖ ^ p
-- Mathlib.Algebra.Regular.Prod
Prod.isRegular_mk : ∀ {R : Type u_2} {S : Type u_3} [inst : Mul R] [inst_1 : Mul S] {a : R} {b : S},
  IsRegular (a, b) ↔ IsRegular a ∧ IsRegular b
-- Mathlib.Analysis.Distribution.FourierMultiplier
SchwartzMap.fourierMultiplierCLM_compL_fourierMultiplierCLM : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : NormedSpace ℂ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℂ 𝕜 F] [inst_7 : FiniteDimensional ℝ E] [inst_8 : MeasurableSpace E] [inst_9 : BorelSpace E]
  [CompleteSpace F] {g₁ g₂ : E → 𝕜},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      SchwartzMap.fourierMultiplierCLM F g₁ ∘SL SchwartzMap.fourierMultiplierCLM F g₂ =
        SchwartzMap.fourierMultiplierCLM F (g₁ * g₂)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- For `K < 1` and finite nonempty `S ⊆ G`, there exists a finite subgroup `H ≤ G` that is also
an atom for `K` and `S`.  -/
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.exists_subgroup_isAtom : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {S : Finset G},
  K < 1 → S.Nonempty → ∃ H x, Finset.IsAtom✝ K S (↑H).toFinset
-- Mathlib.Topology.UniformSpace.Compact
/-- Let `c : ι → Set α` be an open cover of a compact set `s`. Then there exists an entourage
`n` such that for each `x ∈ s` its `n`-neighborhood is contained in some `c i`.  -/
lebesgue_number_lemma : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {ι : Sort u_2} {U : ι → Set α},
  IsCompact K → (∀ (i : ι), IsOpen (U i)) → K ⊆ ⋃ i, U i → ∃ V ∈ uniformity α, ∀ x ∈ K, ∃ i, UniformSpace.ball x V ⊆ U i
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, List.find? (fun x => cmp x.1 k == Ordering.eq) t.toList = none ↔ t.contains k = false
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_incl_lt_iff_lt_top : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L ↥N},
  LieSubmodule.map N.incl N' < N ↔ N' < ⊤
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativePreorder.mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] [inst_2 : Preorder R],
  (∀ (x y : R), x ≤ᵥ y ↔ x ≤ y) → ValuativePreorder R
-- Mathlib.Topology.Compactness.SigmaCompact
/-- Countable unions of σ-compact sets are σ-compact.  -/
isSigmaCompact_sUnion : ∀ {X : Type u_1} [inst : TopologicalSpace X] (S : Set (Set X)),
  S.Countable → (∀ (s : ↑S), IsSigmaCompact ↑s) → IsSigmaCompact (⋃₀ S)
-- Mathlib.Algebra.Notation.Pi.Basic
/-- On non-dependent functions, `Pi.single` is symmetric in the two indices.  -/
Pi.single_comm : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : Type u_9} [inst_1 : Zero M] (i : ι) (x : M) (j : ι),
  Pi.single i x j = Pi.single j x i
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.forallMetaTelescopeReducingAux : Lean.Expr → Bool → Option ℕ → Lean.MetavarKind → Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)
-- Mathlib.Topology.Algebra.PontryaginDual
/-- The Pontryagin dual of `A` is the group of continuous homomorphism `A → Circle`.  -/
PontryaginDual : (A : Type u_1) → [Monoid A] → [TopologicalSpace A] → Type (max u_1 0)
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- The composition `C ⥤ Ind C ⥤ (Cᵒᵖ ⥤ Type v)` is just the Yoneda embedding.  -/
CategoryTheory.Ind.yonedaCompInclusion : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Ind.yoneda.comp (CategoryTheory.Ind.inclusion C) ≅ CategoryTheory.yoneda
-- Mathlib.Order.Filter.Pointwise
/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Filter`. See
Note [pointwise nat action].  -/
Filter.instNSMul : {α : Type u_2} → [Zero α] → [Add α] → SMul ℕ (Filter α)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set β} {a : α}, a • s = ∅ ↔ s = ∅
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toListRev_map : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → γ},
  (Std.Iter.map f it).toListRev = List.map f it.toListRev
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- Given `f : X.PtSimplex n x` and `i : Fin n` (note that this implies `n ≠ 0`),
this is the term in `MulStruct .const f f i` corresponding to
`stdSimplex.σ i.castSucc ≫ f.map`.  -/
SSet.PtSimplex.MulStruct.oneMul : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      (f : X.PtSimplex n x) → (i : Fin n) → SSet.PtSimplex.MulStruct SSet.RelativeMorphism.const f f i
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swapTR.go.match_1.eq_5 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Array α → Sort u_2) (a : α) (xs : List α) (i j : ℕ) (acc : Array α)
  (h_1 : (x x_1 : ℕ) → (x_2 : Array α) → motive [] x x_1 x_2)
  (h_2 : (head : α) → (tail : List α) → (x : Array α) → motive (head :: tail) 0 0 x)
  (h_3 : (a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) 0 i.succ acc)
  (h_4 : (a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) i.succ 0 acc)
  (h_5 : (a : α) → (xs : List α) → (i j : ℕ) → (acc : Array α) → motive (a :: xs) i.succ j.succ acc),
  (match a :: xs, i.succ, j.succ, acc with
    | [], x, x_1, x_2 => h_1 x x_1 x_2
    | head :: tail, 0, 0, x => h_2 head tail x
    | a :: xs, 0, i.succ, acc => h_3 a xs i acc
    | a :: xs, i.succ, 0, acc => h_4 a xs i acc
    | a :: xs, i.succ, j.succ, acc => h_5 a xs i j acc) =
    h_5 a xs i j acc
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.isTotallyDisconnected_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C),
  S.IsTotallyDisconnected ↔ ∀ (c d : C), (S.arrows c d).Nonempty → c = d
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.fromIdeal.eq_1 : ∀ {R : Type u_1} [inst : Ring R], TwoSidedIdeal.fromIdeal = { toFun := fun I => TwoSidedIdeal.span ↑I, monotone' := ⋯ }
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If `n ≠ -1` is an integer number, then the integral of `(z - w) ^ n` over the circle equals
zero.  -/
circleIntegral.integral_sub_zpow_of_ne : ∀ {n : ℤ}, n ≠ -1 → ∀ (c w : ℂ) (R : ℝ), ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0
-- Init.Grind.Ring.Field
Lean.Grind.Field.inv_eq_zero_iff : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a : α}, a⁻¹ = 0 ↔ a = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.mapN.eq_1 : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι} (x : (SSet.Subcomplex.range (f.m j)).N),
  f.mapN x =
    { dim := x.dim,
      simplex := ↑((CategoryTheory.ConcreteCategory.hom ((f.b j).app (Opposite.op { len := x.dim }))) x.simplex) }
-- Mathlib.Analysis.RCLike.Inner
/-- Compact inner product giving rise to the compact L2 norm.  -/
RCLike.«term⟪_,_⟫ₙ_[_]» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.toBlocks₂₁.eq_1 : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n ⊕ o) (l ⊕ m) α),
  M.toBlocks₂₁ = Matrix.of fun i j => M (Sum.inr i) (Sum.inl j)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.congr_refl : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N],
  TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl A M) (LinearEquiv.refl R N) =
    LinearEquiv.refl A (TensorProduct R M N)
-- Mathlib.Order.BooleanAlgebra.Basic
sup_inf_inf_sdiff : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z
-- Init.Data.List.Lemmas
List.all_eq_not_any_not : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, l.all p = !l.any fun x => !p x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsComplex.of_comap : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] (f : k →+* K) {w : NumberField.InfinitePlace K},
  (w.comap f).IsComplex → w.IsComplex
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.dual_rankPos_iff_exists_isCircuit : ∀ {α : Type u_1} {M : Matroid α}, M✶.RankPos ↔ ∃ C, M.IsCircuit C
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.coe_mapSubgroup : ∀ {G : Type u_1} [inst : Group G] {H : Type u_5} [inst_1 : Group H] (e : G ≃* H),
  ⇑e.mapSubgroup = Subgroup.map e.toMonoidHom
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates colimits of shape `J` and `F ≅ G`, then `G` creates colimits of shape `J`.  -/
CategoryTheory.createsColimitsOfShapeOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {F G : CategoryTheory.Functor C D} →
              (F ≅ G) → [CategoryTheory.CreatesColimitsOfShape J F] → CategoryTheory.CreatesColimitsOfShape J G
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimTargetInfo.mk : Lean.Elab.Tactic.ElimTargetView → Lean.Expr → Option Lean.Meta.GeneralizeArg → Lean.Elab.Tactic.ElimTargetInfo✝
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- A list of transvections such that multiplying on the left with these transvections will replace
the last column with zeroes.  -/
Matrix.Pivot.listTransvecCol : {𝕜 : Type u_3} →
  [Field 𝕜] → {r : ℕ} → Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 → List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Path.reverse_reverse : ∀ {V : Type u_2} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a b : V} (p : Quiver.Path a b),
  p.reverse.reverse = p
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_natCast_of_le_half : ∀ {n a : ℕ}, a ≤ n / 2 → (↑a).valMinAbs = ↑a
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.disjoint_of_disjoint_support : ∀ {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V), Disjoint G.support H.support → Disjoint G H
-- Lean.DocString.Extension
Lean.ModuleDoc.mk.sizeOf_spec : ∀ (doc : String) (declarationRange : Lean.DeclarationRange),
  sizeOf { doc := doc, declarationRange := declarationRange } = 1 + sizeOf doc + sizeOf declarationRange
-- Mathlib.Order.Category.BoolAlg
BoolAlg.hasForgetToHeytAlg : CategoryTheory.HasForget₂ BoolAlg HeytAlg
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of the inverse is the negative of the divisor.  -/
MeromorphicOn.divisor_fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜},
  MeromorphicOn.divisor (fun z => (f z)⁻¹) U = -MeromorphicOn.divisor f U
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalLeft : Lean.Elab.Tactic.Tactic