mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.restrictScalars_toLinearEquiv : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : TopologicalSpace M] [inst_6 : LinearMap.CompatibleSMul M M R S]
  (f : M ≃L[S] M), ↑(ContinuousLinearEquiv.restrictScalars R f) = LinearEquiv.restrictScalars R ↑f
-- Mathlib.Data.List.Sublists
List.sublists'Aux.eq_1 : ∀ {α : Type u} (a : α) (r₁ r₂ : List (List α)), List.sublists'Aux a r₁ r₂ = List.foldl (fun r l => r ++ [a :: l]) r₂ r₁
-- Mathlib.Data.Set.Finite.Range
Finite.Set.finite_replacement : ∀ {α : Type u} {β : Type v} [Finite α] (f : α → β), Finite ↑{x | ∃ x_1, f x_1 = x}
-- Mathlib.Tactic.ApplyAt
/-- `apply t at i` uses forward reasoning with `t` at the hypothesis `i`.
Explicitly, if `t : α₁ → ⋯ → αᵢ → ⋯ → αₙ` and `i` has type `αᵢ`, then this tactic adds
metavariables/goals for any terms of `αⱼ` for `j = 1, …, i-1`,
then replaces the type of `i` with `αᵢ₊₁ → ⋯ → αₙ` by applying those metavariables and the
original `i`.
 -/
Mathlib.Tactic.tacticApply_At_ : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Group.Affine
CategoryTheory.OverClass.asOverHom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] (f : X ⟶ Y) [inst_3 : CategoryTheory.HomIsOver f S],
  CategoryTheory.OverClass.asOverHom S f = CategoryTheory.Over.homMk f ⋯
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.extendScalars_toSubfield : ∀ {L : Type u_2} [inst : Field L] {F E : Subfield L} (h : F ≤ E), (Subfield.extendScalars h).toSubfield = E
-- Mathlib.Analysis.Normed.Module.Convex
/-- The norm on a real normed space is convex on any convex set. See also `Seminorm.convexOn`
and `convexOn_univ_norm`.  -/
convexOn_norm : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
  Convex ℝ s → ConvexOn ℝ s norm
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- a triangle that is isomorphic to a distinguished triangle is distinguished  -/
CategoryTheory.Pretriangulated.isomorphic_distinguished : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.HasShift C ℤ} {inst_3 : CategoryTheory.Preadditive C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} [self : CategoryTheory.Pretriangulated C],
  ∀ T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (T₂ : CategoryTheory.Pretriangulated.Triangle C) (x : T₂ ≅ T₁),
      T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.insertIfNew : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ (k : α) (v : β), m₁.Equiv m₂ → (m₁.insertIfNew k v).Equiv (m₂.insertIfNew k v)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.instMax : {α : Type u_2} → [inst : TopologicalSpace α] → {x : α} → Max (TopologicalSpace.OpenNhdsOf x)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.Simps.symm_apply.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (equiv : S.Equiv S'), AddGroupExtension.Equiv.Simps.symm_apply equiv = ⇑equiv.symm
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.mk.sizeOf_spec : ∀ (p : Int.Internal.Linear.Poly) (h : Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof),
  sizeOf { p := p, h := h } = 1 + sizeOf p + sizeOf h
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_le_ker_coord_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  [Nontrivial R] (b : Module.Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n},
  b.flag k ≤ (b.coord l).ker ↔ k ≤ l.castSucc
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.any_eq_not_all_not : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {p : α → Bool},
  m.WF → m.any p = !m.all fun a => !p a
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation_apply : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) (hf : MeasureTheory.IsSigmaSubadditiveSetFun f)
  (hf' : f ∅ = 0) (s : Set X),
  (MeasureTheory.preVariation f hf hf') s = (MeasureTheory.ennrealPreVariation f hf hf').ennrealToMeasure s
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
/-- The algebra structure on a monoid object.
This instance is dangerous as it doesn't round trip from a ring to a monoid object and then back
to a ring, since the `npow` field is lost in the middle. Therefore, it is scoped.  -/
ModuleCat.MonModuleEquivalenceAlgebra.Algebra_of_Mon_ : {R : Type u} → [inst : CommRing R] → (A : ModuleCat R) → [inst_1 : CategoryTheory.MonObj A] → Algebra R ↑A
-- Std.Data.DTreeMap.Internal.Cell
/-- Create a cell with a matching key. Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.of : {α : Type u} → {β : α → Type v} → [inst : Ord α] → (k : α) → β k → Std.DTreeMap.Internal.Cell α β (compare k)
-- Init.Data.Slice.Notation
/-- Slices `carrier` from `range.lower` \(exclusive\) to `range.upper` \(inclusive\).
   -/
Std.Roc.Sliceable.mkSlice : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → [self : Std.Roc.Sliceable α β γ] → α → Std.Roc β → γ
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.mk.injEq : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommMonoid G] {C : Set (Set α)} (toFun : Set α → G) (empty' : toFun ∅ = 0)
  (sUnion' : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun (⋃₀ ↑I) = ∑ u ∈ I, toFun u)
  (toFun_1 : Set α → G) (empty'_1 : toFun_1 ∅ = 0)
  (sUnion'_1 :
    ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun_1 (⋃₀ ↑I) = ∑ u ∈ I, toFun_1 u),
  ({ toFun := toFun, empty' := empty', sUnion' := sUnion' } =
      { toFun := toFun_1, empty' := empty'_1, sUnion' := sUnion'_1 }) =
    (toFun = toFun_1)
-- Mathlib.Data.FunLike.Graded
Graded.equiv_symm_apply_coe : ∀ {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [inst : SetLike σ A]
  [inst_1 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_2 : EquivLike E A B] [inst_3 : GradedEquivLike E 𝒜 ℬ] (e : E)
  (i : ι) (y : ↥(ℬ i)), ↑((Graded.equiv e i).symm y) = EquivLike.inv e ↑y
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toList_filterMapWithPostcondition_filterMapWithPostcondition'.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (__do_lift : Option γ) → (Unit → motive none) → ((fb : γ) → motive (some fb)) → motive __do_lift
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.inhabitedLiftableCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {K : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone (K.comp (CategoryTheory.Functor.id C))) →
            Inhabited (CategoryTheory.LiftableCocone K (CategoryTheory.Functor.id C) c)
-- Mathlib.Topology.Separation.Basic
R1Space.specializes_or_disjoint_nhds : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : R1Space X] (x y : X), x ⤳ y ∨ Disjoint (nhds x) (nhds y)
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.ofBijective_apply : ∀ {M : Type u_9} {N : Type u_10} {F : Type u_11} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) (a : M), (MulEquiv.ofBijective f hf) a = f a
-- Mathlib.Order.Interval.Set.Basic
Set.self_mem_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, a ∈ Set.Iic a
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.center.commMonoid'.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M],
  Submonoid.center.commMonoid' =
    { toMul := (Submonoid.center M).toMulOneClass.toMul, mul_assoc := ⋯,
      toOne := (Submonoid.center M).toMulOneClass.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto,
      npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.card_right : ∀ {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [inst : DecidableEq α] {v w₁ w₂ : α} {t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → t.card = r
-- Init.Data.List.Lemmas
List.getLast_tail : ∀ {α : Type u_1} {l : List α} (h : l.tail ≠ []), l.tail.getLast h = l.getLast ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- The cofork induced by a split coequalizer is a coequalizer, justifying the name. In some cases it
is more convenient to show a given cofork is a coequalizer by showing it is split.
 -/
CategoryTheory.IsSplitCoequalizer.isCoequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        {Z : C} →
          {h : Y ⟶ Z} → (t : CategoryTheory.IsSplitCoequalizer f g h) → CategoryTheory.Limits.IsColimit t.asCofork
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- Taking the negative commutes with taking `meromorphicTrailingCoeffAt`.
 -/
meromorphicTrailingCoeffAt_fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E},
  meromorphicTrailingCoeffAt (fun z => -f z) x = -meromorphicTrailingCoeffAt f x
-- Mathlib.GroupTheory.IsSubnormal
/-- A subnormal additive subgroup of a simple additive group is normal.  -/
AddSubgroup.IsSubnormal.normal_of_isSimpleAddGroup : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, IsSimpleAddGroup G → H.IsSubnormal → H.Normal
-- Mathlib.Order.WithBot
WithBot.ofDual_le_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithBot αᵒᵈ} {y : WithTop α}, WithBot.ofDual x ≤ y ↔ WithTop.toDual y ≤ x
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap : ∀ {R : Type u_1} [inst : CommRing R] (f : R),
  AlgebraicGeometry.IsOpenImmersion
    (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuousOn_empty : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] [h : IsEmpty ι]
  (F : ι → β → α) (S : Set β), UniformEquicontinuousOn F S
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.toGermMonoidHom_apply : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Monoid γ] [inst_3 : ContinuousMul γ] (f : α →ₘ[μ] γ), MeasureTheory.AEEqFun.toGermMonoidHom f = f.toGerm
-- Mathlib.Order.UpperLower.Relative
isRelLowerSet_empty : ∀ {α : Type u_1} {P : α → Prop} [inst : LE α], IsRelLowerSet ∅ P
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_conjTranspose : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A : Matrix n n α), A.adjugate.conjTranspose = A.conjTranspose.adjugate
-- Mathlib.CategoryTheory.Enriched.Basic
/-- `app` is a natural transformation.  -/
CategoryTheory.GradedNatTrans.naturality_assoc : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D}
  (self : CategoryTheory.GradedNatTrans A F G) (X Y : C) {Z : V} (h : (F.obj X ⟶[V] G.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (self.app Y))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y)) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.app X) (G.map X Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y)) h)
-- Init.Data.Rat.Lemmas
Rat.ceil_intCast : ∀ (a : ℤ), (↑a).ceil = a
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.le_add_self : ∀ (p q : DyckWord), q ≤ p + q
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities.mk.injEq : ∀ (textDocument? : Option Lean.Lsp.TextDocumentClientCapabilities) (window? : Option Lean.Lsp.WindowClientCapabilities)
  (workspace? : Option Lean.Lsp.WorkspaceClientCapabilities) (lean? : Option Lean.Lsp.LeanClientCapabilities)
  (textDocument?_1 : Option Lean.Lsp.TextDocumentClientCapabilities)
  (window?_1 : Option Lean.Lsp.WindowClientCapabilities) (workspace?_1 : Option Lean.Lsp.WorkspaceClientCapabilities)
  (lean?_1 : Option Lean.Lsp.LeanClientCapabilities),
  ({ textDocument? := textDocument?, window? := window?, workspace? := workspace?, lean? := lean? } =
      { textDocument? := textDocument?_1, window? := window?_1, workspace? := workspace?_1, lean? := lean?_1 }) =
    (textDocument? = textDocument?_1 ∧ window? = window?_1 ∧ workspace? = workspace?_1 ∧ lean? = lean?_1)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.associator_hom_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) (β : b ⟶ c)
  (γ : c ⟶ d),
  (CategoryTheory.Bicategory.Adj.Bicategory.associator α β γ).hom.τl =
    (CategoryTheory.Bicategory.associator α.l β.l γ.l).hom
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.nonsing_inv_apply_not_isUnit : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  ¬IsUnit A.det → A⁻¹ = 0
-- Mathlib.CategoryTheory.Limits.Types.Colimits
/-- (internal implementation) the fact that the proposed colimit cocone is the colimit  -/
CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type (max v u))) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.TypeMax.colimitCocone F)
-- Mathlib.GroupTheory.Focal
Subgroup.commutator_le_focalSubgroupOf : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), commutator ↥H ≤ H.focalSubgroupOf
-- Mathlib.Data.Num.Bitwise
instDecidableEqNzsNum : DecidableEq NzsNum
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.locallyFinite : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s),
  LocallyFinite fun i => Function.support ⇑(f i)
-- Mathlib.Topology.Algebra.Monoid
tendsto_mul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {a b : M},
  Filter.Tendsto (fun p => p.1 * p.2) (nhds (a, b)) (nhds (a * b))
-- Mathlib.RingTheory.AdicCompletion.Noetherian
IsHausdorff.of_isTorsionFree : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsNoetherianRing R] [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M], I ≠ ⊤ → IsHausdorff I M
-- Mathlib.Tactic.Peel
Mathlib.Tactic.Peel.eventually_imp : ∀ {α : Type u_1} {p q : α → Prop} {f : Filter α}, (∀ (x : α), p x → q x) → (∀ᶠ (x : α) in f, p x) → ∀ᶠ (x : α) in f, q x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.prod_fiberwise : ∀ {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid M]
  [inst_3 : DecidableEq κ] (g : ι → κ) (f : ι → M), ∏ j, ∏ i, f ↑i = ∏ i, f i
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.mono_inr_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.Limits.HasPushouts C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Mono f]
  {s : CategoryTheory.Limits.PushoutCocone f g} (hs : CategoryTheory.Limits.IsColimit s), CategoryTheory.Mono s.inr
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.mapCoconeEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C}
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) {c : CategoryTheory.Limits.Cocone K}
  (t : CategoryTheory.Limits.IsColimit (F.mapCocone c)),
  CategoryTheory.Limits.IsColimit.mapCoconeEquiv h t =
    (CategoryTheory.Limits.IsColimit.precomposeHomEquiv (K.isoWhiskerLeft h) (G.mapCocone c))
      (t.ofIsoColimit (CategoryTheory.Functor.precomposeWhiskerLeftMapCocone h.symm c).symm)
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.measure_symmDiff_eq_zero_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, μ (symmDiff s t) = 0 ↔ s =ᵐ[μ] t
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor_obj : ∀ (Y : AlgebraicGeometry.Scheme) (I : Y.IdealSheafDataᵒᵖ),
  (AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor Y).obj I =
    CategoryTheory.Over.mk (Opposite.unop I).subschemeι
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- The fibrant resolution functor `HoCat.resolution`, as a localizer morphism.  -/
HomotopicalAlgebra.FibrantObject.HoCat.localizerMorphismResolution : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.LocalizerMorphism (HomotopicalAlgebra.weakEquivalences C)
        (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject.HoCat C))
-- Aesop.Search.SearchM
Aesop.popGoal? : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q (Option Aesop.GoalRef)
-- Mathlib.Analysis.Complex.JensenFormula
_private.Mathlib.Analysis.Complex.JensenFormula.0.norm_herglotzLogIntegrand_circleMap_le : ∀ {w ρ : ℂ} {R r₀ r : ℝ},
  0 < R →
    ‖ρ‖ = R →
      0 < r₀ →
        ‖w‖ < r₀ →
          r₀ ≤ r →
            r ≤ R →
              ∀ (θ : ℝ),
                0 < ‖circleMap 0 R θ - ρ‖ →
                  ‖herglotzLogIntegrand✝ w ρ (circleMap 0 r θ)‖ ≤
                    (R + ‖w‖) / (r₀ - ‖w‖) *
                      (|Real.log (2 * R)| + |Real.log √(r₀ / R)| + |Real.log ‖circleMap 0 R θ - ρ‖|)
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The submersive presentation on `P.ModelOfHasCoeffs R₀` provided `P.HasCoeffs R₀`.  -/
Algebra.SubmersivePresentation.ofHasCoeffs : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                (P : Algebra.SubmersivePresentation R S ι σ) →
                  (R₀ : Type u_5) →
                    [inst_4 : CommRing R₀] →
                      [inst_5 : Algebra R₀ R] →
                        [inst_6 : Algebra R₀ S] →
                          [inst_7 : IsScalarTower R₀ R S] →
                            [inst_8 : P.HasCoeffs R₀] →
                              [FaithfulSMul R₀ R] →
                                Algebra.SubmersivePresentation R₀ (Algebra.Presentation.ModelOfHasCoeffs R₀) ι σ
-- Init.Meta.Defs
Lean.Meta.instReprConfig_1 : Repr Lean.Meta.Simp.Config
-- Mathlib.RingTheory.Valuation.Integers
Valuation.ltSubmodule_monotone : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  Monotone v.ltSubmodule
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.coe_equiv_euclideanSpace : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E),
  ⇑((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) = fun x => ∑ i, x.ofLp i • b i
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.symm : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M}, x ≡ y [SMOD U] → y ≡ x [SMOD U]
-- Mathlib.Order.Filter.Extr
IsMinFilter.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → ∀ {g : β → γ}, Monotone g → IsMinFilter (g ∘ f) l a
-- Mathlib.Algebra.Group.Basic
one_div_mul_eq_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), 1 / a * b = b / a
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.mk.injEq : ∀ {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}
  {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (inverts : W.IsInvertedBy L) (lift : (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → CategoryTheory.Functor D E)
  (fac : ∀ (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F), L.comp (lift F hF) = F)
  (uniq : ∀ (F₁ F₂ : CategoryTheory.Functor D E), L.comp F₁ = L.comp F₂ → F₁ = F₂) (inverts_1 : W.IsInvertedBy L)
  (lift_1 : (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → CategoryTheory.Functor D E)
  (fac_1 : ∀ (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F), L.comp (lift_1 F hF) = F)
  (uniq_1 : ∀ (F₁ F₂ : CategoryTheory.Functor D E), L.comp F₁ = L.comp F₂ → F₁ = F₂),
  ({ inverts := inverts, lift := lift, fac := fac, uniq := uniq } =
      { inverts := inverts_1, lift := lift_1, fac := fac_1, uniq := uniq_1 }) =
    (lift = lift_1)
-- Mathlib.Control.Bifunctor
/-- Right map of a bifunctor.  -/
Bifunctor.snd : {F : Type u₀ → Type u₁ → Type u₂} → [Bifunctor F] → {α : Type u₀} → {β β' : Type u₁} → (β → β') → F α β → F α β'
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
find a basis for `S` and `I` such that the inclusion map is a square diagonal
matrix.

See also `Ideal.smithNormalForm` for a version of this theorem that returns
a `Basis.SmithNormalForm`.

The definitions `Ideal.ringBasis`, `Ideal.selfBasis`, `Ideal.smithCoeffs` are (noncomputable)
choices of values for this existential quantifier.
 -/
Ideal.exists_smith_normal_form : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4}
  [inst_3 : CommRing S] [IsDomain S] [inst_5 : Algebra R S] [Finite ι] (b : Module.Basis ι R S) (I : Ideal S),
  I ≠ ⊥ → ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i
-- Lean.Expr
/-- `mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ]` ==> the expression `f a_i ... a_{j-1}`  -/
Lean.mkAppRange : Lean.Expr → ℕ → ℕ → Array Lean.Expr → Lean.Expr
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_le_size_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.size ≤ (t.erase k).size + 1
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_comp : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} {W : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] [inst_6 : NormedAddCommGroup W] [inst_7 : InnerProductSpace 𝕜 W] (f : U →ₗ[𝕜] V)
  (g : V →ₗ[𝕜] W), (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet