mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_subMulAction : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {S : Type u_4}
  [inst_5 : SetLike S E] [SMulMemClass S 𝕜 E] (m : S), B.polar ↑m = {y | ∀ x ∈ m, (B x) y = 0}
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift_of_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] (j : S →+* P),
  IsLocalization.lift ⋯ = j
-- Mathlib.Data.Sigma.Order
Sigma.Lex.noMaxOrder_of_nonempty : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)] [NoMaxOrder ι]
  [∀ (i : ι), Nonempty (α i)], NoMaxOrder (Σₗ (i : ι), α i)
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
/-- If `xs` are the varying parameters of the functions, partitions them into indices and major
arguments, and other parameters.
 -/
Lean.Elab.Structural.RecArgInfo.pickIndicesMajor : Lean.Elab.Structural.RecArgInfo → Array Lean.Expr → Array Lean.Expr × Array Lean.Expr
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link2.match_5.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.Balanced → Sort u_3) (szr : ℕ)
  (k'' : α) (v'' : β k'') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
  (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' = Std.DTreeMap.Internal.Impl.leaf →
        motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (szr_1 : ℕ) →
      (k''_1 : α) →
        (v''_1 : β k''_1) →
          (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).Balanced) →
              Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' =
                  Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1 →
                motive (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1) hr),
  (match hr' : Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'', hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr hr'
    | Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1, hr => h_2 szr_1 k''_1 v''_1 l''_1 r''_1 hr hr') =
    h_2 szr k'' v'' l'' r'' hr ⋯
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the largest element that is less than or equal to the
given element, returning `fallback` if no such element exists.
 -/
Std.TreeSet.getLED : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → α → α
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.firstDiff_le_longestPrefix : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  {s : Set ((n : ℕ) → E n)},
  IsClosed s → ∀ {x y : (n : ℕ) → E n}, x ∉ s → y ∈ s → PiNat.firstDiff x y ≤ PiNat.longestPrefix x s
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.biproductIsoPi_inv_comp_π_apply : ∀ {R : Type u} [inst : Ring R] {J : Type} [inst_1 : Finite J] (f : J → ModuleCat R) (j : J) (x : (j : J) → ↑(f j)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.biproduct.π f j))
      ((CategoryTheory.ConcreteCategory.hom (ModuleCat.biproductIsoPi f).inv) x) =
    x j
-- Mathlib.Data.ZMod.Basic
ZMod.cast_mul : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] {m : ℕ} [CharP R m], m ∣ n → ∀ (a b : ZMod n), (a * b).cast = a.cast * b.cast
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  (A : Matrix m n α), A.mulVec 0 = 0
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.coe_natCast : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (n : ℕ), ⇑↑n = ↑n
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.symm_comp_map_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid M'] [inst_8 : Module R M']
  [inst_9 : AddCommMonoid N'] [inst_10 : Module R N'] (f : M →ₗ[R] M') (g : N →ₗ[R] N')
  (h : P →ₗ[R] TensorProduct R M N),
  ↑(TensorProduct.comm R M' N') ∘ₗ TensorProduct.map f g ∘ₗ h =
    TensorProduct.map g f ∘ₗ ↑(TensorProduct.comm R M N) ∘ₗ h
-- Mathlib.RingTheory.Polynomial.GaussNorm
Polynomial.gaussNorm_zero_right : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) (p : Polynomial R)
  [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ], Polynomial.gaussNorm v 0 p = v (p.coeff 0)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (n : ℕ),
  Int.Internal.Linear.cooper_dvd_right_cert p₁ p₂ p₃ d n = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 →
        d ∣ Int.Internal.Linear.Poly.denote' ctx p₃ →
          Int.Internal.Linear.OrOver n (Int.Internal.Linear.cooper_dvd_right_split ctx p₁ p₂ p₃ d)
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `+` is an additive commutative semigroup, if it admits
a surjective map that preserves `+` from an additive commutative semigroup.  -/
Function.Surjective.addCommSemigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₂] →
      [inst_1 : AddCommSemigroup M₁] →
        (f : M₁ → M₂) → Function.Surjective f → (∀ (x y : M₁), f (x + y) = f x + f y) → AddCommSemigroup M₂
-- Mathlib.Order.Interval.Finset.Nat
Nat.card_Ico : ∀ (a b : ℕ), (Finset.Ico a b).card = b - a
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.mk.inj : ∀ {R : Type u} {S : Type v} {ι : Type w} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S} {val : ι → S}
  {σ' : S → MvPolynomial ι R} {aeval_val_σ' : ∀ (s : S), (MvPolynomial.aeval val) (σ' s) = s}
  {algebra : Algebra (MvPolynomial ι R) S}
  {algebraMap_eq :
    autoParam (algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval val)) Algebra.Generators.algebraMap_eq._autoParam}
  {val_1 : ι → S} {σ'_1 : S → MvPolynomial ι R} {aeval_val_σ'_1 : ∀ (s : S), (MvPolynomial.aeval val_1) (σ'_1 s) = s}
  {algebra_1 : Algebra (MvPolynomial ι R) S}
  {algebraMap_eq_1 :
    autoParam (algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval val_1))
      Algebra.Generators.algebraMap_eq._autoParam},
  { val := val, σ' := σ', aeval_val_σ' := aeval_val_σ', algebra := algebra, algebraMap_eq := algebraMap_eq } =
      { val := val_1, σ' := σ'_1, aeval_val_σ' := aeval_val_σ'_1, algebra := algebra_1,
        algebraMap_eq := algebraMap_eq_1 } →
    val = val_1 ∧ σ' = σ'_1 ∧ algebra = algebra_1
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define a `NormalizedGCDMonoid` structure on a monoid just from the existence of an `lcm`.  -/
normalizedGCDMonoidOfExistsLCM : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [NormalizationMonoid α] →
        [DecidableEq α] → (∀ (a b : α), ∃ c, ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d) → NormalizedGCDMonoid α
-- Mathlib.Data.Multiset.ZeroCons
Multiset.coe_singleton : ∀ {α : Type u_1} (a : α), ↑[a] = {a}
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_unitIso_inv_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
  (X_1 : CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit.unitIso.inv.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id
      (X.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1})))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.name : Lean.Compiler.LCNF.CtorInfo → Lean.Name
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instDecidableLeOffset : {x y : Std.Time.Hour.Offset} → Decidable (x ≤ y)
-- Lean.HeadIndex
Lean.HeadIndex.mvar.sizeOf_spec : ∀ (mvarId : Lean.MVarId), sizeOf (Lean.HeadIndex.mvar mvarId) = 1 + sizeOf mvarId
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} [inst_1 : SizeOf C] [inst_2 : SizeOf ι]
  (obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }))
  (hom :
    ⦃Y : C⦄ →
      (q : Y ⟶ S) →
        ⦃i₁ i₂ : ι⦄ →
          (f₁ : Y ⟶ X i₁) →
            (f₂ : Y ⟶ X i₂) →
              autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                  CategoryTheory.Pseudofunctor.DescentData._auto_1 →
                autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
                    CategoryTheory.Pseudofunctor.DescentData._auto_3 →
                  ((F.map f₁.op.toLoc).toFunctor.obj (obj i₁) ⟶ (F.map f₂.op.toLoc).toFunctor.obj (obj i₂)))
  (pullHom_hom :
    autoParam
      (∀ ⦃Y' Y : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S) (hq : CategoryTheory.CategoryStruct.comp g q = q')
        ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) (gf₁ : Y' ⟶ X i₁) (gf₂ : Y' ⟶ X i₂)
        (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁) (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂),
        CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom q f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ =
          hom q' gf₁ gf₂ ⋯ ⋯)
      CategoryTheory.Pseudofunctor.DescentData.pullHom_hom._autoParam)
  (hom_self :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i) (x : CategoryTheory.CategoryStruct.comp g (f i) = q),
        hom q g g ⋯ ⋯ = CategoryTheory.CategoryStruct.id ((F.map g.op.toLoc).toFunctor.obj (obj i)))
      CategoryTheory.Pseudofunctor.DescentData.hom_self._autoParam)
  (hom_comp :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃)
        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
        (hf₃ : CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q),
        CategoryTheory.CategoryStruct.comp (hom q f₁ f₂ hf₁ hf₂) (hom q f₂ f₃ hf₂ hf₃) = hom q f₁ f₃ hf₁ hf₃)
      CategoryTheory.Pseudofunctor.DescentData.hom_comp._autoParam),
  sizeOf { obj := obj, hom := hom, pullHom_hom := pullHom_hom, hom_self := hom_self, hom_comp := hom_comp } = 1
-- Mathlib.Order.Monotone.Monovary
AntitoneOn.monovaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι} [inst_2 : LinearOrder ι], AntitoneOn f s → AntitoneOn g s → MonovaryOn f g s
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- An equivalence of bialgebras is an invertible bialgebra homomorphism.  -/
BialgEquiv : (R : Type u) →
  [inst : CommSemiring R] →
    (A : Type v) →
      (B : Type w) →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] → [CoalgebraStruct R A] → [CoalgebraStruct R B] → Type (max v w)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_eqOn_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), Set.EqOn (f ∘ ↑hf.localInverse.toPartialEquiv) id hf.localInverse.source
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.zero_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  (CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁ h₂).φH = 0
-- Mathlib.Data.Finset.Insert
Finset.mem_cons_of_mem : ∀ {α : Type u_1} {a b : α} {s : Finset α} {hb : b ∉ s}, a ∈ s → a ∈ Finset.cons b s hb
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_alter_of_compare_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ (f (t.get? k)).isSome = true)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.nat_card_ofStabilizer_eq : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] [Finite α] (a : α),
  Nat.card ↥(SubAddAction.ofStabilizer G a) = Nat.card α - 1
-- Aesop.Script.CtorNames
Aesop.CtorNames.ctor : Aesop.CtorNames → Lean.Name
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ioc_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b : α) {c : α},
  c < 0 → (fun x => x * c) ⁻¹' Set.Ioc a b = Set.Ico (b / c) (a / c)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_union_of_contains_eq_false_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        m₂.contains k = false →
          Std.DHashMap.Internal.Raw₀.Const.get! (m₁.union m₂) k = Std.DHashMap.Internal.Raw₀.Const.get! m₁ k
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.of_inter_support : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α} {ε' : Type u_7}
  [inst : TopologicalSpace ε'] [inst_1 : ENormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] {f : α → ε'},
  MeasurableSet s → MeasureTheory.IntegrableOn f (s ∩ Function.support f) μ → MeasureTheory.IntegrableOn f s μ
-- Mathlib.Analysis.Convolution
/-- The definition of convolution where the bilinear operator is multiplication.  -/
MeasureTheory.convolution_mul : ∀ {𝕜 : Type u𝕜} {G : Type uG} {x : G} [inst : NontriviallyNormedField 𝕜] [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : Sub G] [inst_3 : NormedSpace ℝ 𝕜] {f g : G → 𝕜},
  MeasureTheory.convolution f g (ContinuousLinearMap.mul 𝕜 𝕜) μ x = ∫ (t : G), f t * g (x - t) ∂μ
-- Mathlib.Order.Atoms
/-- Every atomic complete Boolean algebra is completely atomic.

This is not made an instance to avoid typeclass loops.  -/
CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra : {α : Type u_4} → [inst : CompleteBooleanAlgebra α] → [IsAtomic α] → CompleteAtomicBooleanAlgebra α
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_le_iff_of_dvd_of_pos : ∀ {a b c : ℤ}, 0 < b → b ∣ a → (a / b ≤ c ↔ a ≤ b * c)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.card_filter_mk_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w : NumberField.InfinitePlace K),
  {φ | NumberField.InfinitePlace.mk φ = w}.card = w.mult
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.isChain_cons_cons`. -/
List.chain_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α},
  List.IsChain R (a :: b :: l) ↔ R a b ∧ List.IsChain R (b :: l)
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.mk.inj : ∀ {X : Type u} {toProd : X × X} {X_1 : Type u} {toProd_1 : X_1 × X_1},
  { X := X, toProd := toProd } = { X := X_1, toProd := toProd_1 } → X = X_1 ∧ toProd ≍ toProd_1
-- Mathlib.RingTheory.Smooth.Quotient
_private.Mathlib.RingTheory.Smooth.Quotient.0.comap_ker_eq_sup_of_ker_eq_map : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {R' : Type u_3} {S' : Type u_4}
  [inst_2 : CommRing R'] [inst_3 : CommRing S'] [inst_4 : Algebra R S] [inst_5 : Algebra R R'] [inst_6 : Algebra R' S']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [IsScalarTower R S S'] [IsScalarTower R R' S'],
  Function.Surjective ⇑(algebraMap R S) →
    RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R')) →
      Ideal.comap (algebraMap R R') (RingHom.ker (algebraMap R' S')) =
        RingHom.ker (algebraMap R R') ⊔ RingHom.ker (algebraMap R S)
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The setoid on `Δ` identifying elements with the same double coset `H₁gH₂ = H₁hH₂`, pulled
back from `DoubleCoset.setoid` along the inclusion `Δ ↪ G`.

This is an `abbrev` rather than a global instance: the subgroups `H₁, H₂` cannot be inferred
from the submonoid `Δ`, so this cannot participate in instance search (and a global instance
would also create a `Setoid` diamond on `↥Δ` with the left-coset setoid). The quotient map is
`HeckeCoset.mk`.  -/
HeckeCoset.setoid : {G : Type u_1} → [inst : Group G] → (Δ : Submonoid G) → Subgroup G → Subgroup G → Setoid ↥Δ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertMany!_cons : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {l : List ((a : α) × β a)}
  {k : α} {v : β k}, ↑(t.insertMany! (⟨k, v⟩ :: l)) = ↑((Std.DTreeMap.Internal.Impl.insert! k v t).insertMany! l)
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.LE.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (a b : α),
  Std.PRange.UpwardEnumerable.LE a b = ∃ n, Std.PRange.succMany? n a = some b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.mk.sizeOf_spec : ∀ (name : String) (kind : Lean.Lsp.SymbolKind) (tags? : Option (Array Lean.Lsp.SymbolTag)) (detail? : Option String)
  (uri : Lean.Lsp.DocumentUri) (range selectionRange : Lean.Lsp.Range) (data? : Option Lean.Json),
  sizeOf
      { name := name, kind := kind, tags? := tags?, detail? := detail?, uri := uri, range := range,
        selectionRange := selectionRange, data? := data? } =
    1 + sizeOf name + sizeOf kind + sizeOf tags? + sizeOf detail? + sizeOf uri + sizeOf range + sizeOf selectionRange +
      sizeOf data?
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.hasStrictFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i)
  [inst_6 : DecidableEq ι], HasStrictFDerivAt (⇑f) (f.linearDeriv x) x
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.instInhabitedState : Inhabited Lean.Meta.Match.Extension.State
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
_private.Mathlib.RingTheory.Coalgebra.CoassocSimps.0.CoassocSimps.«termρ⁻¹» : Lean.ParserDescr
-- Mathlib.Data.Finset.NAry
Finset.le_inf_image₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
  {t : Finset β} [inst_1 : SemilatticeInf δ] [inst_2 : OrderTop δ] {g : γ → δ} {a : δ},
  a ≤ (Finset.image₂ f s t).inf g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.topology_eq_scott : ∀ {α : Type u_1} {D : Set (Set α)} {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : Topology.IsScott α D],
  inst_1 = Topology.scott α D
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.under_iso_iff : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] (P : CategoryTheory.MorphismProperty T) [P.RespectsIso]
  {X : T} {f g : CategoryTheory.Under X} (e : f ≅ g), P f.hom ↔ P g.hom
-- Lean.Linter.UnusedVariables
/-- Get the current list of `IgnoreFunction`s.  -/
Lean.Linter.getUnusedVariablesIgnoreFns : Lean.Elab.Command.CommandElabM (Array Lean.Linter.IgnoreFunction)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
/-- The Cech construction for `FormalCoproduct` is isomorphic
to the general `Arrow.cechNerve` construction applied to the morphism
to the terminal object.  -/
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      (U : CategoryTheory.Limits.FormalCoproduct C) →
        {T : C} →
          (hT : CategoryTheory.Limits.IsTerminal T) →
            U.cech ≅
              (CategoryTheory.Arrow.mk ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).cechNerve
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
IsLocalRing.of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [IsLocalRing R] [inst_2 : Semiring S] [Nontrivial S]
  (f : R →+* S) [IsLocalHom f], Function.Surjective ⇑f → IsLocalRing S
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_natCast : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ), ↑↑n = ↑n
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mulPosMono_iff_mulPosStrictMono : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : PartialOrder α] [IsRightCancelMulZero α],
  MulPosMono α ↔ MulPosStrictMono α
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.mk_reindex_fin_cast : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n m : ℕ}
  (h : n = m) (x : TensorPower R n M),
  GradedMonoid.mk m ((PiTensorProduct.reindex R (fun x => M) (finCongr h)) x) = GradedMonoid.mk n x
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.ext' : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  {I J : HomogeneousIdeal 𝒜}, (∀ (i : ι), ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ J) → I = J
-- Std.Do.Triple.SpecLemmas
List.lt_of_range'_eq_append_cons : ∀ {s n step : ℕ} {xs : List ℕ} {i : ℕ} {ys : List ℕ} {j : ℕ},
  List.range' s n step = xs ++ i :: ys → 0 < step → j ∈ ys → i < j
-- Lean.Meta.Basic
Lean.Meta.AbstractMVarsResult.mvars : Lean.Meta.AbstractMVarsResult → Array Lean.Expr
-- Mathlib.Topology.Algebra.Monoid.Defs
continuous_mul_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] (m : M),
  Continuous fun x => x * m
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.subcategoryAcyclic C).IsClosedUnderIsomorphisms
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.of_forall_mem_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [LawfulBEq α],
  (∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) → m₁.Equiv m₂
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- If one simple graph satisfies `p`, then there exists an extremal graph satisfying `p`.  -/
SimpleGraph.exists_isExtremal_iff_exists : ∀ {V : Type u_1} [inst : Fintype V] (p : SimpleGraph V → Prop), (∃ G x, G.IsExtremal p) ↔ ∃ G, p G
-- Mathlib.Topology.Compactness.Compact
Finset.isCompact_biUnion : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] (s : Finset ι) {f : ι → Set X},
  (∀ i ∈ s, IsCompact (f i)) → IsCompact (⋃ i ∈ s, f i)