mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.prod.inl_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inl X Y)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    h
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_X : ∀ {R : Type u} {n : ℕ} [inst : Semiring R], Polynomial.X.coeff n = if 1 = n then 1 else 0
-- Mathlib.RepresentationTheory.Basic
Representation.norm_comp_self : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : Fintype G]
  [inst_3 : AddCommMonoid V] [inst_4 : Module k V] (ρ : Representation k G V) (g : G), ρ.norm ∘ₗ ρ g = ρ.norm
-- Mathlib.FieldTheory.Extension
AlgEquiv.ofInjectiveField.congr_simp : ∀ {R : Type u} [inst : CommSemiring R] {E : Type u_1} {F : Type u_2} [inst_1 : DivisionRing E] [inst_2 : Semiring F]
  [inst_3 : Nontrivial F] [inst_4 : Algebra R E] [inst_5 : Algebra R F] (f : E →ₐ[R] F),
  AlgEquiv.ofInjectiveField f = AlgEquiv.ofInjectiveField f
-- Mathlib.Combinatorics.Additive.Dissociation
/-- **Alias** of the reverse direction of `mulDissociated_inv`. -/
MulDissociated.inv : ∀ {α : Type u_1} [inst : CommGroup α] {s : Set α}, MulDissociated s → MulDissociated s⁻¹
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v},
  (m.insert k v)[a] = if h₂ : (k == a) = true then v else m[a]
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.sup : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {l l' : Filter α},
  Asymptotics.IsBigOWith c l f g → Asymptotics.IsBigOWith c l' f g → Asymptotics.IsBigOWith c (l ⊔ l') f g
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangle_mor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), h.triangle.mor₁ = h.m₁
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- `ContMDiffWithinAt.comp₂`, with a separate argument for point equality.  -/
ContMDiffWithinAt.comp₂_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_12}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {s : Set M} {n : WithTop ℕ∞} {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M}
  {y : M' × N'} {t : Set (M' × N')},
  ContMDiffWithinAt (I'.prod J') J n h t y →
    ContMDiffWithinAt I I' n f s x →
      ContMDiffWithinAt I J' n g s x → (f x, g x) = y → Set.MapsTo (fun x => (f x, g x)) s t → ⋯
-- Mathlib.RingTheory.TensorProduct.Basic
TensorProduct.Algebra.moduleAux.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Module A M] [inst_6 : Module B M]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M],
  TensorProduct.Algebra.moduleAux = TensorProduct.Algebra.moduleAux
-- Mathlib.Computability.Reduce
isTrans_oneOneReducible : ∀ {α : Type u_1} [inst : Primcodable α], IsTrans (α → Prop) OneOneReducible
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.ofMeasurableSpace_le_ofMeasurableSpace_iff : ∀ {α : Type u_3} {m₁ m₂ : MeasurableSpace α},
  MeasurableSpace.DynkinSystem.ofMeasurableSpace m₁ ≤ MeasurableSpace.DynkinSystem.ofMeasurableSpace m₂ ↔ m₁ ≤ m₂
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.ghDist_le_nonemptyCompacts_dist : ∀ {X : Type u} [inst : MetricSpace X] (p q : TopologicalSpace.NonemptyCompacts X),
  dist p.toGHSpace q.toGHSpace ≤ dist p q
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Limits.exists_eq_of_preservesColimit_yoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J C} [CategoryTheory.IsCofiltered J]
  {c : CategoryTheory.Limits.Cone D} (hc : CategoryTheory.Limits.IsLimit c) {X : C}
  [CategoryTheory.Limits.PreservesColimit D.op (CategoryTheory.yoneda.obj X)] {i j : J} (f : D.obj i ⟶ X)
  (g : D.obj j ⟶ X),
  CategoryTheory.CategoryStruct.comp (c.π.app i) f = CategoryTheory.CategoryStruct.comp (c.π.app j) g →
    ∃ k u v, CategoryTheory.CategoryStruct.comp (D.map u) f = CategoryTheory.CategoryStruct.comp (D.map v) g
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.sigmaFixedByEquivOrbitsProdAddGroup.eq_1 : ∀ (G : Type u) (X : Type v) [inst : AddGroup G] [inst_1 : AddAction G X],
  AddAction.sigmaFixedByEquivOrbitsProdAddGroup G X =
    Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans
                (Trans.trans
                  (Trans.trans (Equiv.subtypeProdEquivSigmaSubtype fun g => Membership.mem (AddAction.fixedBy X g)).symm
                    ((Equiv.prodComm G X).subtypeEquiv ⋯))
                  (Equiv.subtypeProdEquivSigmaSubtype fun b a => a ∈ AddAction.stabilizer G b))
                (AddAction.selfEquivSigmaOrbits G X).sigmaCongrLeft')
              (Equiv.sigmaAssoc fun ω b => ↥(AddAction.stabilizer G ↑b)))
            (Equiv.sigmaCongrRight fun x =>
              Equiv.sigmaCongrRight fun x_1 =>
                match x_1 with
                | ⟨val, hb⟩ => (AddAction.stabilizerEquivStabilizerOfOrbitRel hb).toEquiv))
          (Equiv.sigmaCongrRight fun x =>
            Equiv.sigmaEquivProd ↑(AddAction.orbit G x.out) ↥(AddAction.stabilizer G x.out)))
        (Equiv.sigmaCongrRight fun ω => AddAction.orbitProdStabilizerEquivAddGroup G ω.out))
      (Equiv.sigmaEquivProd (Quotient (AddAction.orbitRel G X)) G)
-- Mathlib.Data.Set.Lattice
Set.nonempty_iInter_Ici_iff : ∀ {α : Type u_1} {ι : Sort u_5} [inst : Preorder α] {f : ι → α}, (⋂ i, Set.Ici (f i)).Nonempty ↔ BddAbove (Set.range f)
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.hom_ext : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} {f g : X ⟶ Y}, f.hom = g.hom → f = g
-- Aesop.Stats.Basic
Aesop.GoalKind.preNorm.sizeOf_spec : sizeOf Aesop.GoalKind.preNorm = 1
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParams.Info.addSelfCalls : Lean.Elab.FixedParams.Info → Lean.Elab.FixedParams.Info
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  (m.insertManyIfNewUnit l).contains k = (m.contains k || l.contains k)
-- Mathlib.AlgebraicGeometry.Noetherian
/-- A scheme `X` is locally Noetherian if `𝒪ₓ(U)` is Noetherian for all affine `U`.  -/
AlgebraicGeometry.IsLocallyNoetherian : AlgebraicGeometry.Scheme → Prop
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.HasSheafify.mk' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {F : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)}
  (adj : F ⊣ CategoryTheory.sheafToPresheaf J A) [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.HasSheafify J A
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1` and `∀ (1 ≤ n), μ (x ^ n) = μ x ^ n`, then `smoothingFun μ x = μ x`.  -/
smoothingFun_of_powMul : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 → ∀ {x : R}, (∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n) → smoothingFun μ x = μ x
-- Init.Data.String.Slice
/-- Interprets a slice as the decimal representation of a natural number, returning it. Panics if the
slice does not contain a decimal natural number.

A slice can be interpreted as a decimal natural number if it is not empty and all the characters in
it are digits. Underscores \(`_`\) are allowed as digit separators and are ignored during parsing.

Use `isNat` to check whether `toNat!` would return a value. `toNat?` is a safer
alternative that returns `none` instead of panicking when the string is not a natural number.

Examples:

* `"0".toSlice.toNat! = 0`

* `"5".toSlice.toNat! = 5`

* `"587".toSlice.toNat! = 587`

* `"1_000".toSlice.toNat! = 1000`
 -/
String.Slice.toNat! : String.Slice → ℕ
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- A natural transformation induces a natural transformation between the `map_presheaf` functors.
 -/
CategoryTheory.NatTrans.onPresheaf : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F G : CategoryTheory.Functor C D} → (F ⟶ G) → (G.mapPresheaf ⟶ F.mapPresheaf)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsometricContinuousFunctionalCalculus.norm_spectrum_le : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) ⦃x : 𝕜⦄,
  x ∈ spectrum 𝕜 a → autoParam (p a) IsometricContinuousFunctionalCalculus.norm_spectrum_le._auto_1 → ‖x‖ ≤ ‖a‖
-- Mathlib.GroupTheory.Nilpotent
Subgroup.is_ascending_rev_series_of_is_descending : ∀ (G : Type u_1) [inst : Group G] {H : ℕ → Subgroup G} {n : ℕ},
  H n = ⊥ → Subgroup.IsDescendingCentralSeries H → Subgroup.IsAscendingCentralSeries fun m => H (n - m)
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
contDiff_one_iff_deriv : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F}, ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous (deriv f)
-- Mathlib.ModelTheory.Satisfiability
/-- A theory models a (bounded) formula when any of its nonempty models realizes that formula on all
inputs.  -/
FirstOrder.Language.Theory.ModelsBoundedFormula : {L : FirstOrder.Language} → L.Theory → {α : Type w} → {n : ℕ} → L.BoundedFormula α n → Prop
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β),
  ((HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V).inv.app X).f i =
    CategoryTheory.CategoryStruct.id (X.X i)
-- Mathlib.Algebra.Field.Basic
div_sub_same : ∀ {K : Type u_1} [inst : DivisionRing K] {a b : K}, b ≠ 0 → (a - b) / b = a / b - 1
-- Mathlib.Analysis.Real.Pi.Chudnovsky
_private.Mathlib.Analysis.Real.Pi.Chudnovsky.0.chudnovskySum_eq_pi_inv : ProofWanted (chudnovskySum = Real.pi⁻¹)
-- Mathlib.Topology.UniformSpace.Basic
tendsto_of_uniformContinuous_subtype : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α} {a : α},
  (UniformContinuous fun x => f ↑x) → s ∈ nhds a → Filter.Tendsto f (nhds a) (nhds (f a))
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : SizeOf R] [inst_6 : SizeOf M] [inst_7 : SizeOf N]
  (toFun' :
    (S : Type u) → [inst_8 : CommSemiring S] → [inst_9 : Algebra R S] → TensorProduct R S M → TensorProduct R S N)
  (isCompat' :
    autoParam
      (∀ {S : Type u} [inst_8 : CommSemiring S] [inst_9 : Algebra R S] {S' : Type u} [inst_10 : CommSemiring S']
        [inst_11 : Algebra R S'] (φ : S →ₐ[R] S'),
        ⇑(LinearMap.rTensor N φ.toLinearMap) ∘ toFun' S = toFun' S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap))
      PolynomialLaw.isCompat'._autoParam),
  sizeOf { toFun' := toFun', isCompat' := isCompat' } = 1
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.le_weightedTotalDegree : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : SemilatticeSup M] [inst_3 : OrderBot M] (w : σ → M) {φ : MvPolynomial σ R} {d : σ →₀ ℕ},
  d ∈ φ.support → (Finsupp.weight w) d ≤ MvPolynomial.weightedTotalDegree w φ
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instZero : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] → [inst_7 : ContMDiffMul I (↑⊤) G] → Zero (LeftInvariantDerivation I G)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_alter_of_not_compare_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, ¬cmp k k' = Ordering.eq → (k' ∈ Std.DTreeMap.Const.alter t k f ↔ k' ∈ t)
-- Init.Data.List.TakeDrop
List.takeWhile_cons_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, ¬p a = true → List.takeWhile p (a :: l) = []
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.ApplyResult.goals : List Lean.MVarId → Lean.Meta.Sym.ApplyResult
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- The *principle of isolated zeros* for an analytic function, global version: if a function is
analytic on a connected set `U` and vanishes in arbitrary neighborhoods of a point `z₀ ∈ U`, then
it is identically zero in `U`.
For higher-dimensional versions requiring that the function vanishes in a neighborhood of `z₀`,
see `AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero`.  -/
AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜},
  AnalyticOnNhd 𝕜 f U → IsPreconnected U → z₀ ∈ U → (∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) → Set.EqOn f 0 U
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsEulerian.edgesFinset_eq : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype ↑G.edgeSet] {u v : V} {p : G.Walk u v}
  (h : p.IsEulerian), ⋯.edgesFinset = G.edgeFinset
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.lintegral_bind_le : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : β → ENNReal)
  (m : MeasureTheory.Measure α) (μ : α → MeasureTheory.Measure β),
  ∫⁻ (x : β), f x ∂m.bind μ ≤ ∫⁻ (a : α), ∫⁻ (x : β), f x ∂μ a ∂m
-- Mathlib.Algebra.GroupWithZero.Invertible
inv_mul_cancel_of_invertible : ∀ {α : Type u} [inst : GroupWithZero α] (a : α) [Invertible a], a⁻¹ * a = 1
-- Mathlib.Data.EReal.Operations
EReal.le_sub_iff_add_le : ∀ {a b c : EReal}, b ≠ ⊥ ∨ c ≠ ⊥ → b ≠ ⊤ ∨ c ≠ ⊤ → (a ≤ c - b ↔ a + b ≤ c)
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_univ₂_eventually₂ : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] [PreconnectedSpace X] {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] {f g : X → α},
  Continuous f → Continuous g → f ≤ᶠ[l₁] g → g ≤ᶠ[l₂] f → ∃ x, f x = g x
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedFunctionTheorems.default : Mathlib.Meta.FunProp.FunctionTheorems
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] [inst_5 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β k → β k},
      Std.Internal.List.maxKey! (Std.Internal.List.modifyKey k f l) = Std.Internal.List.maxKey! l
-- Batteries.Lean.LawfulMonad
instLawfulMonadBaseIO_batteries : LawfulMonad BaseIO
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Let `M` be an `A`-module. Every `A`-linear map `Mⁿ → Mⁿ` corresponds to a `n×n`-matrix whose entries
are `A`-linear maps `M → M`. In another word, we have `End(Mⁿ) ≅ Matₙₓₙ(End(M))` defined by:
`(f : Mⁿ → Mⁿ) ↦ (x ↦ f (0, ..., x at j-th position, ..., 0) i)ᵢⱼ` and
`m : Matₙₓₙ(End(M)) ↦ (v ↦ ∑ⱼ mᵢⱼ(vⱼ))`.

See also `LinearMap.toMatrix'`
 -/
endVecRingEquivMatrixEnd : (ι : Type u_1) →
  [inst : Fintype ι] →
    [DecidableEq ι] →
      (A : Type u_3) →
        [inst_2 : Semiring A] →
          (M : Type u_4) →
            [inst_3 : AddCommMonoid M] → [inst_4 : Module A M] → Module.End A (ι → M) ≃+* Matrix ι ι (Module.End A M)
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageParams.type : Lean.Lsp.ShowMessageParams → Lean.Lsp.MessageType
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.isDetpBalanced_transpose_iff : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {a b : R}, A.transpose.IsDetpBalanced a b ↔ A.IsDetpBalanced a b
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_C_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) {c : R},
  c ≠ 0 → (SkewPolynomial.C c * SkewPolynomial.X ^ n).support = {n}
-- Mathlib.Algebra.Order.Kleene
add_le : ∀ {α : Type u_1} [inst : IdemSemiring α] {a b c : α}, a ≤ c → b ≤ c → a + b ≤ c
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.insert : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
  s.PairwiseDisjoint f → ∀ {i : ι}, (∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)) → (insert i s).PairwiseDisjoint f
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.Homotopy.wr_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (self : CategoryTheory.PreOneHypercover.Homotopy f g)
  (i : E.I₀) {Z : C} (h : F.X (g.s₀ i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.a i) (CategoryTheory.CategoryStruct.comp (F.p₂ (self.H i)) h) =
    CategoryTheory.CategoryStruct.comp (g.h₀ i) h
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
/-- The natural `ℤ`-algebra homomorphism from the unitization of a non-unital subring to
its `Subring.closure`.  -/
NonUnitalSubring.unitization : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] → [inst_1 : SetLike S R] → [hSR : NonUnitalSubringClass S R] → (s : S) → Unitization ℤ ↥s →ₐ[ℤ] R
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.find?_char_eq_find?_beq : ∀ {c : Char} {s : String}, s.find? c = s.find? fun x => x == c
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.associator_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (P Q R : C),
  (CategoryTheory.Limits.coprod.associator P Q R).inv =
    CategoryTheory.Limits.coprod.desc
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl)
      (CategoryTheory.Limits.coprod.desc
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl)
        CategoryTheory.Limits.coprod.inr)
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instSemilatticeInfClosedAddSubgroup : (G : Type u) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → SemilatticeInf (ClosedAddSubgroup G)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.lt_map_of_comap_lt_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {p : Submodule R M} {q : Submodule R₂ M₂} [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Surjective ⇑f → Submodule.comap f q < p → q < Submodule.map f p
-- Mathlib.Topology.Bornology.Basic
/-- **Alias** of the reverse direction of `Bornology.isCobounded_compl_iff`. -/
Bornology.IsBounded.compl : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsBounded s → Bornology.IsCobounded sᶜ
-- Init.Data.BitVec.Folds
BitVec.iunfoldr_replace_snd : ∀ {w : ℕ} {α : Type u_1} {f : Fin w → α → α × Bool} (state : ℕ → α) (value : BitVec w) (a : α),
  state 0 = a → (∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value[↑i])) → (BitVec.iunfoldr f a).2 = value
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.finite_co_support' : ∀ {Γ : Type u_8} {R : Type u_9} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {α : Type u_7}
  (self : HahnSeries.SummableFamily Γ R α) (g : Γ), {a | (self.toFun a).coeff g ≠ 0}.Finite
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_succ_of_some : ∀ {n : ℕ} {α : Type u_1} {x : α} {f : Fin (n + 1) → Option α}, f 0 = some x → Fin.findSome? f = some x
-- Mathlib.Dynamics.Ergodic.Action.Basic
MeasureTheory.aeconst_of_forall_preimage_vadd_ae_eq : ∀ (G : Type u_1) {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : VAdd G α]
  [ErgodicVAdd G α μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    (∀ (g : G), (fun x => g +ᵥ x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsRegular.mk : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular M rs → ⊤ ≠ Ideal.ofList rs • ⊤ → RingTheory.Sequence.IsRegular M rs
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastShiftLeftConst : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst