mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.coe_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] (f : X → Y)
  (h : Function.support f ⊆ U) (h' : ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support f).Finite),
  ⇑{ toFun := f, supportWithinDomain' := h, supportLocallyFiniteWithinDomain' := h' } = f
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousAt.add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (f + g) x
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
/-- If `‖f x‖ₑ ≤ c * ‖g x‖ₑ` a.e., `eLpNorm' f p μ ≤ c * eLpNorm' g p μ` for all `p ∈ (0, ∞)`.  -/
MeasureTheory.eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_6} [inst : TopologicalSpace ε']
  [inst_1 : ContinuousENorm ε'] {ε : Type u_7} [inst_2 : TopologicalSpace ε] [inst_3 : ESeminormedAddMonoid ε]
  {f : α → ε} {c : ENNReal} {g : α → ε'} {p : ℝ},
  MeasureTheory.AEStronglyMeasurable g μ →
    (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ) → 0 < p → MeasureTheory.eLpNorm' f p μ ≤ c * MeasureTheory.eLpNorm' g p μ
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.nontrivial_of_nontrivial : ∀ (σ : Type u_2) (R : Type u_3) [inst : CommSemiring R] [Nontrivial R], Nontrivial (MvPolynomial σ R)
-- Mathlib.Topology.Compactness.Compact
/-- For every family of closed sets whose intersection avoids a compact set,
there exists a finite subfamily whose intersection avoids this compact set.  -/
IsCompact.elim_finite_subfamily_closed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
  IsCompact s → ∀ (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.forget.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.AddMonObj A],
  CategoryTheory.AddMod.forget A = { obj := fun A_1 => A_1.X, map := fun {X Y} f => f.hom, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.apply_le_one : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω), μ s ≤ 1
-- Mathlib.Topology.Algebra.ConstMulAction
Inseparable.const_smul : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α] {x y : α},
  Inseparable x y → ∀ (c : M), Inseparable (c • x) (c • y)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.unitOfList_eq_insertManyIfNewUnit! : ∀ {α : Type u} {instOrd : Ord α} {l : List α},
  Std.DTreeMap.Internal.Impl.Const.unitOfList l =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! Std.DTreeMap.Internal.Impl.empty l)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_le_mul_of_le_one_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b c : α}, a ≤ b * c → b ≤ 1 → a ≤ c
-- Std.Time.Time.Unit.Second
Std.Time.Second.instLawfulEqOrdOrdinal : ∀ {leap : Bool}, Std.LawfulEqOrd (Std.Time.Second.Ordinal leap)
-- Mathlib.Data.PFunctor.Multivariate.M
_private.Mathlib.Data.PFunctor.Multivariate.M.0.TypeVec.append1.match_1.splitter : {n : ℕ} →
  (motive : Fin2 (n + 1) → Sort u_1) →
    (x : Fin2 (n + 1)) → ((i : Fin2 n) → motive i.fs) → (Unit → motive Fin2.fz) → motive x
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.add_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a : X ⟶ Y), a + 0 = a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.rightHomologyMap_nullHomotopic : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology]
  (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂)
  (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  CategoryTheory.ShortComplex.rightHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.instIsIsoEqualizerComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasEqualizer f g]
  [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.equalizerComparison f g G)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.invert_comp_C : ∀ {R : Type u_3} [inst : CommSemiring R], ⇑LaurentPolynomial.invert ∘ ⇑LaurentPolynomial.C = ⇑LaurentPolynomial.C
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D}
  (h : E.IsPointwiseRightKanExtensionAt Y)
  [inst_3 : CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)]
  (g : CategoryTheory.StructuredArrow Y L),
  CategoryTheory.CategoryStruct.comp h.isoLimit.hom
      (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y L).comp F) g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map g.hom)
      ((CategoryTheory.CostructuredArrow.hom E).app g.right)
-- Mathlib.Algebra.Group.Prod
AddSemiconjBy.prod : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] {x y z : M × N},
  AddSemiconjBy x.1 y.1 z.1 → AddSemiconjBy x.2 y.2 z.2 → AddSemiconjBy x y z
-- Mathlib.RingTheory.PowerBasis
PowerBasis.lift.congr_simp : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb pb_1 : PowerBasis A S) (e_pb : pb = pb_1) (y y_1 : S') (e_y : y = y_1)
  (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0), pb.lift y hy = pb_1.lift y_1 ⋯
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] (F : ι → α → β) (f : α → β) (p : Filter ι)
  (s : Set α), TendstoUniformlyOn F f p s = ∀ u ∈ uniformity β, ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
-- Mathlib.RingTheory.Bialgebra.Hom
/-- **Alias** of `BialgHom.coe_toAlgHom_injective`. -/
BialgHom.coe_algHom_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  Function.Injective BialgHom.toAlgHom
-- Mathlib.Order.BoundedOrder.Basic
Pi.top_apply : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Top (α' i)] (i : ι), ⊤ i = ⊤
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- Let `T / S / R` be a tower of algebras, `T` is an integral `R`-algebra, then it is integral
as an `S`-algebra.  -/
Algebra.IsIntegral.tower_top : ∀ (R : Type u_1) {S : Type u_4} {T : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  [h : Algebra.IsIntegral R T], Algebra.IsIntegral S T
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.boundary.eq_1 : ∀ {n : ℕ} (c : CompositionAsSet n), c.boundary = c.boundaries.orderEmbOfFin ⋯
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.id_b : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ) (i : Fin (n + 1)),
  (AlgebraicTopology.DoldKan.MorphComponents.id X n).b i = X.σ i
-- Batteries.Data.Fin.Basic
/-- Compute `i / n`, where `n` is a `Nat` and inferred the type of `i`.  -/
Fin.divNat : {m n : ℕ} → Fin (m * n) → Fin m
-- Mathlib.Data.Finset.Prod
Finset.offDiag_filter_lt_eq_filter_le : ∀ {ι : Type u_4} [inst : PartialOrder ι] [inst_1 : DecidableLE ι] [inst_2 : DecidableLT ι] (s : Finset ι),
  {i ∈ s.offDiag | i.1 < i.2} = {i ∈ s.offDiag | i.1 ≤ i.2}
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.δ_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.AddGrp.forget₂Mon C) G H =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.AddGrp.forget₂Mon C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj G H))
-- Mathlib.Data.Set.Insert
Set.eq_singleton_iff_nonempty_unique_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyData.op_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), h.op.Q = Opposite.op h.K
-- Init.Data.UInt.Lemmas
UInt16.sub_neg : ∀ {a b : UInt16}, a - -b = a + b
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
/-- Auxiliary definition for `Homotopy.extend`  -/
Homotopy.extend.homAux : {ι : Type u_1} →
  {c : ComplexShape ι} →
    {C : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_3} C] →
        [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_2 : CategoryTheory.Preadditive C] →
            {K L : HomologicalComplex C c} →
              ((i j : ι) → K.X i ⟶ L.X j) →
                (i' j' : Option ι) → HomologicalComplex.extend.X K i' ⟶ HomologicalComplex.extend.X L j'
-- Mathlib.Dynamics.Flow
/-- Given flows `ϕ` by `τ` on `α` and `ψ` by `τ` on `β`, a function `π : α → β` is called a
*semiconjugacy* from `ϕ` to `ψ` if `π` is continuous and surjective, and `π ∘ (ϕ t) = (ψ t) ∘ π` for
all `t : τ`.  -/
Flow.IsSemiconjugacy : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] →
      [inst_1 : TopologicalSpace α] →
        [inst_2 : AddMonoid τ] → {β : Type u_3} → [inst_3 : TopologicalSpace β] → (α → β) → Flow τ α → Flow τ β → Prop
-- Mathlib.RingTheory.WittVector.Defs
WittVector.constantCoeff_wittSub : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), MvPolynomial.constantCoeff (WittVector.wittSub p n) = 0
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given congruence relations `c, d` on a monoid such that `d` contains `c`, `d`'s quotient
map induces a homomorphism from the quotient by `c` to the quotient by `d`.  -/
Con.map : {M : Type u_1} → [inst : MulOneClass M] → (c d : Con M) → c ≤ d → c.Quotient →* d.Quotient
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry?_eq_getEntry?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β),
  l.getEntry? k = l.getEntry?ₘ k
-- Mathlib.RingTheory.Algebraic.Integral
MvPolynomial.exists_dvd_map_of_isAlgebraic : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] {σ : Type u_4} [NoZeroDivisors S] {f : MvPolynomial σ S},
  f ≠ 0 → ∃ g, g ≠ 0 ∧ f ∣ (MvPolynomial.map (algebraMap R S)) g
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isReal_smul_iff : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Gal(K/k)}
  {w : NumberField.InfinitePlace K}, (σ • w).IsReal ↔ w.IsReal
-- Mathlib.Geometry.Manifold.VectorField.Pullback
instIsManifoldMinSmoothnessOfNatWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 3) M],
  IsManifold I (minSmoothness 𝕜 2) M
-- Mathlib.Algebra.Group.Defs
CancelCommMonoid.toCancelMonoid.eq_1 : ∀ (M : Type u) [inst : CancelCommMonoid M],
  CancelCommMonoid.toCancelMonoid M = { toLeftCancelMonoid := inst.toLeftCancelMonoid, toIsRightCancelMul := ⋯ }
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.down_closed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s t : Finset E},
  s ∈ K.faces → t ⊆ s → t.Nonempty → t ∈ K.faces
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.norm_equiv_le_norm_pi : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [StarOrderedRing A]
  (x : WithCStarModule A ((i : ι) → E i)), ‖(WithCStarModule.equiv A ((i : ι) → E i)) x‖ ≤ ‖x‖
-- Mathlib.Algebra.Group.Units.Defs
isUnit_iff_exists_inv' : ∀ {M : Type u_1} [inst : Monoid M] [IsDedekindFiniteMonoid M] {a : M}, IsUnit a ↔ ∃ b, b * a = 1
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
List.iterM.eq_1 : ∀ {α : Type w} (l : List α) (m : Type w → Type w') [inst : Pure m], l.iterM m = { internalState := { list := l } }
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.cotangentExtendScalarsEquiv_symm_toLinearMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), ↑P.cotangentExtendScalarsEquiv.symm = Algebra.Extension.Cotangent.map P.toExtendScalars
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- If the neighbor set of a vertex `v` is a subset of `s`, then the degree of the vertex in the
induced subgraph of `s` is the same as in `G`.  -/
SimpleGraph.degree_induce_of_neighborSet_subset : ∀ {V : Type u_1} {s : Set V} [inst : DecidablePred fun x => x ∈ s] [inst_1 : Fintype V] {G : SimpleGraph V}
  [inst_2 : DecidableRel G.Adj] {v : ↑s}, G.neighborSet ↑v ⊆ s → (SimpleGraph.induce s G).degree v = G.degree ↑v
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.sub_iff_right : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₁ =o[l] g → ((fun x => f₁ x - f₂ x) =o[l] g ↔ f₂ =o[l] g)
-- Mathlib.Order.CompleteBooleanAlgebra
OrderDual.instCompleteBooleanAlgebra : {α : Type u} → [CompleteBooleanAlgebra α] → CompleteBooleanAlgebra αᵒᵈ
-- Mathlib.Topology.Maps.Basic
/-- **Alias** of the forward direction of `isClosedMap_iff_comap_nhds_le`. -/
IsClosedMap.comap_nhds_le : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f → ∀ {y : Y}, Filter.comap f (nhds y) ≤ nhdsSet (f ⁻¹' {y})
-- Lean.Data.SMap
Lean.SMap.mk : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Bool → Std.HashMap α β → Lean.PHashMap α β → Lean.SMap α β
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.stabilizer_of_subAdd : ∀ {R : Type u} {M : Type v} [inst : AddGroup R] [inst_1 : AddAction R M] {p : SubAddAction R M} (m : ↥p),
  AddAction.stabilizer R m = AddAction.stabilizer R ↑m
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.IsReduced.nil : ∀ {α : Type u}, FreeGroup.IsReduced []
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_mul_const : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {𝕜 : Type u_8} [inst : RCLike 𝕜] (r : 𝕜) (f : ℝ → 𝕜),
  ∫ (x : ℝ) in a..b, f x * r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) * r
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_ker_self : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), AddSubgroup.map f f.ker = ⊥
-- Init.Data.SInt.Lemmas
ISize.toBitVec_ofIntLE : ∀ (x : ℤ) (h₁ : ISize.minValue.toInt ≤ x) (h₂ : x ≤ ISize.maxValue.toInt),
  (ISize.ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt System.Platform.numBits x
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.mk.sizeOf_spec : ∀ {m : Type w → Type w'} {α : Type v} [inst : (a : Type w) → SizeOf (m a)] [inst_1 : SizeOf α] (Property : α → Prop)
  (small : Std.Internal.Small (Subtype Property)) (operation : m (Std.Internal.USquash (Subtype Property))),
  sizeOf { Property := Property, small := small, operation := operation } = 1 + sizeOf small + sizeOf operation
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, List.find? (fun x => x.fst == k) m.toList = none ↔ m.contains k = false
-- Batteries.Tactic.Lint.Misc
/-- Return a list of unused `let_fun` terms in an expression that introduce proofs.
 -/
Batteries.Tactic.Lint.findUnusedHaves : Lean.Expr → Lean.MetaM (Array Lean.MessageData)
-- Mathlib.Logic.Equiv.Set
Equiv.image_apply_coe : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (x : ↑s), ↑((e.image s) x) = e ↑x
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mk.sizeOf_spec : ∀ {G : Type u_3} [inst : Group G] [inst_1 : SizeOf G] (toSubmonoid : Submonoid G)
  (inv_mem' : ∀ {x : G}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier),
  sizeOf { toSubmonoid := toSubmonoid, inv_mem' := inv_mem' } = 1 + sizeOf toSubmonoid
-- Init.Data.Vector.Zip
Vector.zip_eq_append_iff : ∀ {α : Type u_1} {n m : ℕ} {β : Type u_2} {as : Vector α (n + m)} {bs : Vector β (n + m)} {xs : Vector (α × β) n}
  {ys : Vector (α × β) m},
  as.zip bs = xs ++ ys ↔ ∃ as₁ as₂ bs₁ bs₂, as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = as₁.zip bs₁ ∧ ys = as₂.zip bs₂
-- Lean.Data.Json.Basic
Lean.Json.brecOn_4.go : {motive_1 : Lean.Json → Sort u} →
  {motive_2 : Array Lean.Json → Sort u} →
    {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} →
      {motive_4 : List Lean.Json → Sort u} →
        {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u} →
          {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u} →
            (t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) →
              ((t : Lean.Json) → t.below → motive_1 t) →
                ((t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t) →
                  ((t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t) →
                    ((t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t) →
                      ((t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t) →
                        ((t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) →
                            Lean.Json.below_5 t → motive_6 t) →
                          motive_5 t ×' Lean.Json.below_4 t
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_eq_of_le : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  {s : Set M}, s ⊆ ↑p → p ≤ Submodule.span R s → Submodule.span R s = p
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.toNonUnitalSubsemiring_mono : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], Monotone NonUnitalSubring.toNonUnitalSubsemiring
-- Batteries.Data.Float.Lemmas
_private.Batteries.Data.Float.Lemmas.0.Float.Model.UnpackedFloat.isNaN.match_1.splitter : (motive : Float.Model.UnpackedFloat → Sort u_1) →
  (x : Float.Model.UnpackedFloat) →
    (Unit → motive Float.Model.UnpackedFloat.notANumber) →
      ((x : Float.Model.UnpackedFloat) → (x = Float.Model.UnpackedFloat.notANumber → False) → motive x) → motive x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_get? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (h : m.WF) {a : α} {h' : (m.get? a).isSome = true}, (m.get? a).get h' = m.get a ⋯
-- Mathlib.RingTheory.PowerSeries.NoZeroDivisors
PowerSeries.rescale_injective : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {a : R}, a ≠ 0 → Function.Injective ⇑(PowerSeries.rescale a)
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.instCategoryTransportEnrichment : {V : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u) →
        [CategoryTheory.Category.{v, u} C] →
          {W : Type u''} →
            [inst_3 : CategoryTheory.Category.{v'', u''} W] →
              [inst_4 : CategoryTheory.MonoidalCategory W] →
                (F : CategoryTheory.Functor V W) →
                  [inst_5 : F.LaxMonoidal] → CategoryTheory.Category.{v, u} (CategoryTheory.TransportEnrichment F C)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcompose₂_obj_left_map : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  (X : CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F))
  {X_1 Y : D} (f : X_1 ⟶ Y),
  ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj X).left.map f = G.map (X.left.map f)
-- Mathlib.Analysis.Calculus.Gradient.Basic
Filter.EventuallyEq.gradient_eq : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {f₁ : F → 𝕜}, f₁ =ᶠ[nhds x] f → gradient f₁ x = gradient f x
-- Mathlib.Data.Finset.Interval
/-- A function `f` from `Finset α` is antitone if and only if `f (cons a s ha) ≤ f s` for all
`s` and `a ∉ s`.  -/
Finset.antitone_iff_forall_cons_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β},
  Antitone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f (Finset.cons a s ha) ≤ f s
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.braiding_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C), (β_ G H).hom.hom.hom = (β_ G.X H.X).hom
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.δ_liftCochain : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m)
  (m' : ℤ) (hm' : m + 1 = m'),
  CochainComplex.HomComplex.δ n m (CochainComplex.mappingCone.liftCochain φ α β h) =
    -(CochainComplex.HomComplex.δ m m' α).comp (CochainComplex.mappingCone.inl φ) ⋯ +
      (CochainComplex.HomComplex.δ n m β + α.comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯).comp
        (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)) ⋯
-- Mathlib.Order.Filter.Basic
Filter.instTransForallEventuallyLE : {α : Type u} →
  {β : Type v} →
    [inst : Preorder β] →
      {l : Filter α} → Trans (fun x1 x2 => x1 ≤ᶠ[l] x2) (fun x1 x2 => x1 ≤ᶠ[l] x2) fun x1 x2 => x1 ≤ᶠ[l] x2