mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffine_of_equiv : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  P ≈ Q → WeierstrassCurve.Jacobian.Point.toAffine W P = WeierstrassCurve.Jacobian.Point.toAffine W Q
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.eventually_differentiableAt_cuspFunction_nhds_ne_zero : ∀ {h : ℝ} {f : ℂ → ℂ},
  0 < h →
    Function.Periodic f ↑h →
      (∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) →
        ∀ᶠ (q : ℂ) in nhdsWithin 0 {0}ᶜ, DifferentiableAt ℂ (Function.Periodic.cuspFunction h f) q
-- Mathlib.RingTheory.Localization.Basic
/-- For an algebra homomorphism `f : A →ₐ[R] B`, if `A` and `B` are algebras over a localization
`S` of `R`, then `f` is automatically an `S`-algebra homomorphism.  -/
AlgHom.extendScalarsOfIsLocalization : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            (S : Type u_4) →
              [inst_3 : CommSemiring S] →
                [inst_4 : Algebra R S] →
                  (M : Submonoid R) →
                    [IsLocalization M S] →
                      [inst_6 : Algebra R A] →
                        [inst_7 : Algebra S A] →
                          [IsScalarTower R S A] →
                            [inst_9 : Algebra R B] →
                              [inst_10 : Algebra S B] → [IsScalarTower R S B] → (A →ₐ[R] B) → A →ₐ[S] B
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.mkₐ_comp_liftAlgHom : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (I : Ideal S) [inst_3 : IsAdicComplete I S] [inst_4 : CommRing A] [inst_5 : Algebra R A]
  (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m)
  (n : ℕ), (Ideal.Quotient.mkₐ R (I ^ n)).comp (IsAdicComplete.liftAlgHom I f ⋯) = f n
-- Mathlib.Order.CompleteLattice.Basic
/-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
See `ciSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in conditionally complete
lattices.  -/
iSup_eq_of_forall_le_of_forall_lt_exists_gt : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {b : α} {f : ι → α},
  (∀ (i : ι), f i ≤ b) → (∀ w < b, ∃ i, w < f i) → ⨆ i, f i = b
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_id_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {Q : Type u_5} [inst_4 : CommSemiring Q] [inst_5 : Algebra R Q]
  [inst_6 : IsLocalization M Q] (x : R) (y : ↥M),
  (IsLocalization.map Q (RingHom.id R) ⋯) (IsLocalization.mk' S x y) = IsLocalization.mk' Q x y
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex)
  (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) {Z_1 : C} (h : Q.complex.X 0 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm)
      (CategoryTheory.CategoryStruct.comp (Q.complex.d 1 0) h) =
    CategoryTheory.CategoryStruct.comp (f.f 0) h
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_lt_encard_of_dep_of_finite : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, X.Finite → M.Dep X → M.eRk X < X.encard
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.toAlgHom_convPow : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R C] [inst_5 : Coalgebra.IsCocomm R C] (f : WithConv (C →ₐc[R] A))
  (n : ℕ), WithConv.toConv ↑(f ^ n).ofConv = WithConv.toConv ↑f.ofConv ^ n
-- Lean.Meta.Tactic.Generalize
Lean.Meta.instInhabitedGeneralizeArg : Inhabited Lean.Meta.GeneralizeArg
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃}
  {chosenPullback : CategoryTheory.Limits.ChosenPullback h₁₂.p₂ h₂₃.p₁} {p : chosenPullback.pullback ⟶ S}
  {p₁ : chosenPullback.pullback ⟶ X₁} {p₃ : chosenPullback.pullback ⟶ X₃} {l : h₁₃.LiftStruct p₁ p₃ p}
  {hp₁ :
    autoParam (CategoryTheory.CategoryStruct.comp chosenPullback.p₁ h₁₂.p₁ = p₁)
      CategoryTheory.Limits.ChosenPullback₃.hp₁._autoParam}
  {hp₃ :
    autoParam (CategoryTheory.CategoryStruct.comp chosenPullback.p₂ h₂₃.p₂ = p₃)
      CategoryTheory.Limits.ChosenPullback₃.hp₃._autoParam}
  {chosenPullback_1 : CategoryTheory.Limits.ChosenPullback h₁₂.p₂ h₂₃.p₁} {p_1 : chosenPullback_1.pullback ⟶ S}
  {p₁_1 : chosenPullback_1.pullback ⟶ X₁} {p₃_1 : chosenPullback_1.pullback ⟶ X₃} {l_1 : h₁₃.LiftStruct p₁_1 p₃_1 p_1}
  {hp₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp chosenPullback_1.p₁ h₁₂.p₁ = p₁_1)
      CategoryTheory.Limits.ChosenPullback₃.hp₁._autoParam}
  {hp₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp chosenPullback_1.p₂ h₂₃.p₂ = p₃_1)
      CategoryTheory.Limits.ChosenPullback₃.hp₃._autoParam},
  { chosenPullback := chosenPullback, p := p, p₁ := p₁, p₃ := p₃, l := l, hp₁ := hp₁, hp₃ := hp₃ } =
      { chosenPullback := chosenPullback_1, p := p_1, p₁ := p₁_1, p₃ := p₃_1, l := l_1, hp₁ := hp₁_1, hp₃ := hp₃_1 } →
    chosenPullback = chosenPullback_1 ∧ p ≍ p_1 ∧ p₁ ≍ p₁_1 ∧ p₃ ≍ p₃_1 ∧ l ≍ l_1
-- Mathlib.RingTheory.Multiplicity
multiplicity_eq_of_associated_left : ∀ {α : Type u_1} [inst : CommMonoid α] {a b c : α}, Associated a b → multiplicity b c = multiplicity a c
-- Mathlib.Topology.Category.CompactlyGenerated
/-- The fully faithful embedding of `CompactlyGenerated` in `TopCat`.  -/
CompactlyGenerated.compactlyGeneratedToTop : CategoryTheory.Functor CompactlyGenerated TopCat
-- Init.Data.SInt.Bitwise
Int64.neg_eq_not_add : ∀ (a : Int64), -a = ~~~a + 1
-- Mathlib.RingTheory.DedekindDomain.Basic
IsPrincipalIdealRing.isDedekindDomain : ∀ (A : Type u_2) [inst : CommRing A] [IsDomain A] [IsPrincipalIdealRing A], IsDedekindDomain A
-- Mathlib.RingTheory.RingHom.OpenImmersion
RingHom.IsStandardOpenImmersion.stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardOpenImmersion
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal
/-- If `F : C ⥤ D` is such that `F.obj X` is initial for any `X : C`,
then `F` is an initial object.  -/
CategoryTheory.Functor.isInitial : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor C D} →
          ((X : C) → CategoryTheory.Limits.IsInitial (F.obj X)) → CategoryTheory.Limits.IsInitial F
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.comapRight_id : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β),
  κ.comapRight ⋯ = κ
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.smul_zero : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : Zero X] [inst_3 : SMulZeroClass M X] [ContinuousSMul M X] {f : α → M} {g : α → X} {l : Filter α} {c : M},
  Filter.Tendsto f l (nhds c) → Filter.Tendsto g l (nhds 0) → Filter.Tendsto (fun x => f x • g x) l (nhds 0)
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.not_isUnit_of_natDegree_pos : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] (p : Polynomial R), 0 < p.natDegree → ¬IsUnit p
-- Mathlib.RingTheory.Congruence.Basic
RingCon.isScalarTower_right : ∀ {α : Type u_1} {R : Type u_3} [inst : Add R] [inst_1 : MulOneClass R] [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R] (c : RingCon R), IsScalarTower α c.Quotient c.Quotient
-- Mathlib.Algebra.Central.TensorProduct
/-- Let `B` and `C` be two algebras over a field `K`, if `B ⊗[K] C` is central and `C` is
non-trivial, then `B` is central.  -/
Algebra.IsCentral.left_of_tensor_of_field : ∀ (K : Type u_4) (B : Type u_5) (C : Type u_6) [inst : Field K] [inst_1 : Ring B] [inst_2 : Ring C] [Nontrivial C]
  [inst_4 : Algebra K B] [inst_5 : Algebra K C] [Algebra.IsCentral K (TensorProduct K B C)], Algebra.IsCentral K B
-- Mathlib.Data.Multiset.Count
Multiset.count.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), Multiset.count a = Multiset.countP fun x => a = x
-- Mathlib.RingTheory.Finiteness.Subalgebra
Submodule.fg_of_isUnit : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {I : Submodule R A}, IsUnit I → I.FG
-- Std.Net.Addr
Std.Net.SocketAddressV4.mk : Std.Net.IPv4Addr → UInt16 → Std.Net.SocketAddressV4
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.reindex_hom_π_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C)
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β) {Z : C}
  (h : f (ε b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (ε b)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b) h
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair_map : ∀ {X Y : CategoryTheory.Limits.WalkingParallelPair} (f : X ⟶ Y),
  CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.map f =
    match Y, X, f with
    | .(CategoryTheory.Limits.WalkingParallelPair.one), .(CategoryTheory.Limits.WalkingParallelPair.zero),
      CategoryTheory.Limits.WalkingParallelPairHom.left => CategoryTheory.Limits.WalkingReflexivePair.Hom.left
    | .(CategoryTheory.Limits.WalkingParallelPair.one), .(CategoryTheory.Limits.WalkingParallelPair.zero),
      CategoryTheory.Limits.WalkingParallelPairHom.right => CategoryTheory.Limits.WalkingReflexivePair.Hom.right
    | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) =>
      CategoryTheory.CategoryStruct.id
        (match x with
        | CategoryTheory.Limits.WalkingParallelPair.one => CategoryTheory.Limits.WalkingReflexivePair.zero
        | CategoryTheory.Limits.WalkingParallelPair.zero => CategoryTheory.Limits.WalkingReflexivePair.one)
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.inducedOuterMeasure_zero : ∀ {α : Type u_1} {P : Set α → Prop} {P0 : P ∅},
  (∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)) →
    P Set.univ →
      MeasureTheory.inducedOuterMeasure (fun x x_1 => 0) P0 MeasureTheory.inducedOuterMeasure_zero._proof_1 = 0
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.sigmaEquiv_symm_apply : ∀ {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [inst : TopologicalSpace A]
  [inst_1 : (i : I) → TopologicalSpace (X i)] (f : C((i : I) × X i, A)) (i : I),
  (ContinuousMap.sigmaEquiv A X).symm f i = f.comp (ContinuousMap.sigmaMk i)
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The image of the normalizer is contained in the normalizer of the image.  -/
AddSubgroup.le_normalizer_map : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N),
  AddSubgroup.map f (AddSubgroup.normalizer ↑H) ≤ AddSubgroup.normalizer ↑(AddSubgroup.map f H)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_zsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocDiv hp (a - m • p) b = toIocDiv hp a b + m
-- Lean.Expr
/-- If the expression is a constant, return that name.
Otherwise return `Option.none`.
 -/
Lean.Expr.constName? : Lean.Expr → Option Lean.Name
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Finset.pluennecke_petridis_inequality_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A B : Finset G} (C : Finset G),
  (∀ A' ⊆ A, (A + B).card * A'.card ≤ (A' + B).card * A.card) → (C + A + B).card * A.card ≤ (A + B).card * (C + A).card
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.eraseManyEntries!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap.Internal.Impl α β) (l : ρ),
  t.eraseManyEntries! l =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, snd⟩ =>
              have r := ⟨Std.DTreeMap.Internal.Impl.erase! a ↑r, ⋯⟩;
              pure (ForInStep.yield r)
      have r : t.IteratedSlowErasureFrom := __s
      pure r).run
-- Mathlib.Analysis.Distribution.Sobolev
/-- A tempered distribution belongs to the Sobolev space of order `s` and `p = 2` if and only if
its Fourier transform multiplied by `(1 + ‖x‖ ^ 2) ^ (s / 2)` is in `Lp`.  -/
TemperedDistribution.memSobolev_iff_exists_smulLeftCLM_fourier : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : InnerProductSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ} {f : TemperedDistribution E F},
  TemperedDistribution.MemSobolev s 2 f ↔
    ∃ f',
      (TemperedDistribution.smulLeftCLM F fun x => ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (FourierTransform.fourier f) =
        MeasureTheory.Lp.toTemperedDistribution f'
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_eq_tsum_of_hasSum_iff_hasSum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [T2Space α]
  {f : β → α} {g : γ → α}, (∀ {a : α}, HasSum f a ↔ HasSum g a) → ∑' (b : β), f b = ∑' (c : γ), g c
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The isomorphism `(K.extend e).opcycles j' ≅ K.opcycles j` when `e.f j = j'`.  -/
HomologicalComplex.extendOpcyclesIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {j : ι} →
                      {j' : ι'} →
                        e.f j = j' →
                          [inst_3 : K.HasHomology j] →
                            [inst_4 : (K.extend e).HasHomology j'] → (K.extend e).opcycles j' ≅ K.opcycles j
-- Mathlib.Data.Matrix.Mul
Matrix.mul_mul_left : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Semiring α] [inst_1 : Fintype n] (M : Matrix m n α)
  (N : Matrix n o α) (a : α), (Matrix.of fun i j => a * M i j) * N = a • (M * N)
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_prod : ∀ {α : Type u_1} {ι : Type u_3} {β : Type u_4} [inst : CommMonoid β] {f : ι → α → β} (I : Finset ι),
  UniformFun.toFun (∏ i ∈ I, f i) = ∏ i ∈ I, UniformFun.toFun (f i)
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.Functor.IsIso.mk : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D},
  autoParam F.Faithful CategoryTheory.Functor.IsIso.faithful._autoParam →
    autoParam F.Full CategoryTheory.Functor.IsIso.full._autoParam → Function.Bijective F.obj → F.IsIso
-- Mathlib.Logic.Equiv.Fin.Basic
Fin.castLEquiv_symm_apply : ∀ {n m : ℕ} (h : n ≤ m) (i : { i // ↑i < n }), (Fin.castLEquiv h).symm i = ⟨↑↑i, ⋯⟩
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.deterministic_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f)
  (a : α), (ProbabilityTheory.Kernel.deterministic f hf) a = MeasureTheory.Measure.dirac (f a)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.I₁'.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {a b : E.I₁'}
  (left : a.fst.1 = b.fst.1) (right : a.fst.2 = b.fst.2),
  (CategoryTheory.PreOneHypercover.congrIndexOneOfEq left right) a.snd = b.snd → a = b
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.symm_dual_id : ∀ {α : Type u_2} [inst : Min α] [inst_1 : Top α], InfTopHom.dual.symm (SupBotHom.id αᵒᵈ) = InfTopHom.id α
-- Mathlib.RingTheory.GradedAlgebra.Radical
HomogeneousIdeal.coe_radical : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : CommRing A] [inst_1 : AddCommMonoid ι] [inst_2 : LinearOrder ι]
  [inst_3 : IsOrderedCancelAddMonoid ι] [inst_4 : SetLike σ A] [inst_5 : AddSubmonoidClass σ A] {𝒜 : ι → σ}
  [inst_6 : GradedRing 𝒜] (I : HomogeneousIdeal 𝒜), I.radical.toIdeal = I.toIdeal.radical
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.card.eq_1 : ∀ (L : FirstOrder.Language), L.card = Cardinal.mk L.Symbols
-- Batteries.Data.Array.Match
/-- Make a KMP matcher for a given pattern array  -/
Array.Matcher.ofArray : {α : Type u_1} → [BEq α] → Array α → Array.Matcher α
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- The elements in `pinGroup Q` embed into (CliffordAlgebra Q)ˣ.  -/
pinGroup.toUnits : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {Q : QuadraticForm R M} → ↥(pinGroup Q) →* (CliffordAlgebra Q)ˣ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.mk.injEq : ∀ (left : Bool) (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (c₃? : Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr)
  (left_1 : Bool) (c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr)
  (c₃?_1 : Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  ({ left := left, c₁ := c₁, c₂ := c₂, c₃? := c₃? } = { left := left_1, c₁ := c₁_1, c₂ := c₂_1, c₃? := c₃?_1 }) =
    (left = left_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1 ∧ c₃? = c₃?_1)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.revSkipWhile_eq_iff : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} (startPos endPos : s.Pos),
  endPos.revSkipWhile pat = startPos ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat startPos endPos ∧
      (¬String.Slice.Pattern.Model.RevMatchesAt pat startPos ∨
        String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos startPos)
-- Mathlib.Algebra.Algebra.Bilinear
SemilinearMapClass.semilinearMap.congr_simp : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} {F : Type u_14} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M]
  [inst_5 : Module S M₃] {σ : R →+* S} (f f_1 : F),
  f = f_1 → ∀ [inst_6 : FunLike F M M₃] [inst_7 : SemilinearMapClass F σ M M₃], ↑f = ↑f_1
-- Mathlib.Analysis.Normed.Ring.Lemmas
SeparationQuotient.instNormedRing : {α : Type u_1} → [inst : SeminormedRing α] → NormedRing (SeparationQuotient α)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Nonsingular P → P 2 = 0 → P ≈ ![0, 1, 0]
-- Init.Control.ExceptCps
ExceptCpsT.runCatch.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x : ExceptCpsT α m α), x.runCatch = x α pure pure
-- Mathlib.Data.Set.Card
Set.ncard_insert_of_notMem : ∀ {α : Type u_1} {s : Set α} {a : α},
  a ∉ s → autoParam s.Finite Set.ncard_insert_of_notMem._auto_1 → (insert a s).ncard = s.ncard + 1
-- Mathlib.Topology.Constructions
Topology.IsEmbedding.uliftDown : ∀ {X : Type u} [inst : TopologicalSpace X], Topology.IsEmbedding ULift.down
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A `C^n` local diffeomorphism is `C^n`.  -/
IsLocalDiffeomorph.contMDiff : ∀ {𝕜 : 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},
  IsLocalDiffeomorph I J n f → ContMDiff I J n f
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_insert_of_mem : ∀ {y z : ZFSet.{u_1}} (x : ZFSet.{u_1}), z ∈ y → z ∈ insert x y
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Init.Meta
/-- `dsimp!` is shorthand for `dsimp` with `autoUnfold := true`.
This will unfold applications of functions defined by pattern matching, when one of the patterns applies.
This can be used to partially evaluate many definitions.  -/
Lean.Parser.Tactic.dsimpAutoUnfold : Lean.ParserDescr
-- Mathlib.RingTheory.Prime
/-- If `x * y = a * ∏ i ∈ s, p i` where `p i` is always prime, then
`x` and `y` can both be written as a divisor of `a` multiplied by
a product over a subset of `s`  -/
mul_eq_mul_prime_prod : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {α : Type u_2} [inst_2 : DecidableEq α] {x y a : R}
  {s : Finset α} {p : α → R},
  (∀ i ∈ s, Prime (p i)) →
    x * y = a * ∏ i ∈ s, p i →
      ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
-- Lean.Parser.Term.Basic
Lean.Parser.Term.bracketedBinder.parenthesizer : optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- Interpret a `CatCommSqOver F G X` as a `CatCommSq`.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.asSquare : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                (X : Type u₄) →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) →
                      CategoryTheory.CatCommSq S.fst S.snd F G
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.symm_f₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E), P.symm.f₀ = P.g₀