mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Nonsingular P → P 2 = 0 → IsUnit (P 1)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b} {𝕝 : Type u_4} [inst_5 : RCLike 𝕝] [inst_6 : NormedSpace 𝕝 F] [inst_7 : SMulCommClass 𝕜 𝕝 F] {c : 𝕝},
  CurveIntegrable ω γ → CurveIntegrable (c • ω) γ
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Config.mk.injEq : ∀ (maxSteps maxSteps_1 : ℕ), ({ maxSteps := maxSteps } = { maxSteps := maxSteps_1 }) = (maxSteps = maxSteps_1)
-- Mathlib.Algebra.Homology.BifunctorShift
/-- The canonical isomorphism `mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧`.
This isomorphism does not involve signs.  -/
CochainComplex.mapBifunctorShift₁Iso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Preadditive C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                [inst_5 : CategoryTheory.Preadditive D] →
                  (K₁ : CochainComplex C₁ ℤ) →
                    (K₂ : CochainComplex C₂ ℤ) →
                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                        [inst_6 : F.Additive] →
                          [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                            (x : ℤ) →
                              [inst_8 : K₁.HasMapBifunctor K₂ F] →
                                ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctor K₂ F ≅
                                  (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).obj (K₁.mapBifunctor K₂ F)
-- Aesop.Builder.Cases
/-- `decl` is either the name of the inductive type described by `info`, or a
type synonym for it at transparency `default` or `md` (whichever is larger).  -/
Aesop.RuleBuilder.casesCore : Lean.Name →
  Lean.InductiveVal →
    Array Aesop.CasesPattern →
      Option Aesop.IndexingMode →
        Lean.Meta.TransparencyMode → Lean.Meta.TransparencyMode → Aesop.PhaseSpec → Lean.MetaM Aesop.LocalRuleSetMember
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S_equiv : Mathlib.Deriving.Encodable.S✝ ≃ ℕ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.entryAtIdx?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {i : ℕ}, t₁.entryAtIdx? i = t₂.entryAtIdx? i
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m),
  0 < m →
    ∀ (a : A) (i : ℕ),
      ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f)) ''
          Subtype.val ⁻¹' ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑(((DirectSum.decompose 𝒜) a) i)) =
        (PrimeSpectrum.basicOpen
            (HomogeneousLocalization.mk
              { deg := m * i, num := ⟨↑(((DirectSum.decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ })).carrier
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.restrictedYoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v))
  (η : CategoryTheory.Over A),
  (CategoryTheory.OverPresheafAux.restrictedYoneda A).obj η = CategoryTheory.OverPresheafAux.restrictedYonedaObj η.hom
-- Mathlib.Algebra.Group.Defs
InvolutiveNeg.mk : {A : Type u_2} → [toNeg : Neg A] → (∀ (x : A), - -x = x) → InvolutiveNeg A
-- Mathlib.Probability.Kernel.Defs
/-- A class for kernels which are zero or a Markov kernel.  -/
ProbabilityTheory.IsZeroOrMarkovKernel : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → ProbabilityTheory.Kernel α β → Prop
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntInfo.default : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
MeasureTheory.VectorMeasure.semivariation_mono : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s t : Set X}, s ⊆ t → μ.semivariation s ≤ μ.semivariation t
-- Lean.Elab.Command
Lean.Elab.Command.MacroExpandedSnapshot.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot) (macroDecl : Lean.Name) (newStx : Lean.Syntax) (newNextMacroScope : ℕ)
  (hasTraces : Bool) (next : Array (Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot)),
  sizeOf
      { toSnapshot := toSnapshot, macroDecl := macroDecl, newStx := newStx, newNextMacroScope := newNextMacroScope,
        hasTraces := hasTraces, next := next } =
    1 + sizeOf toSnapshot + sizeOf macroDecl + sizeOf newStx + sizeOf newNextMacroScope + sizeOf hasTraces + sizeOf next
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.moduleDocExt : Lean.SimplePersistentEnvExtension Lean.ModuleDoc (Lean.PersistentArray Lean.ModuleDoc)
-- Std.Do.SPred.DerivedLaws
/-- A proof that `P` and `φ` are equivalent.
 -/
Std.Do.SPred.Tactic.IsPure.to_pure : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs} {φ : outParam Prop} [self : Std.Do.SPred.Tactic.IsPure P φ], P ⊣⊢ₛ ⌜φ⌝
-- Lean.Data.Lsp.Workspace
Lean.Lsp.WorkspaceFolder.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (name : String), sizeOf { uri := uri, name := name } = 1 + sizeOf uri + sizeOf name
-- Mathlib.Tactic.DefEqTransformations
/-- Recursively unfold all the projection applications for class instances.  -/
Mathlib.Tactic.unfoldProjs : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.maxKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxKey! = t₂.maxKey!
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of an integer `m` is one iff `p` doesn't divide `m`.  -/
padicNorm.int_eq_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℤ), padicNorm p ↑m = 1 ↔ ¬↑p ∣ m
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
/-- If a localizer morphism `Φ` is a localized equivalence, then it is a right
derivability structure if the categories of right resolutions are connected and the
categories of right resolutions of arrows are nonempty.  -/
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  [∀ (X₂ : C₂), CategoryTheory.IsConnected (Φ.RightResolution X₂)] [Φ.arrow.HasRightResolutions] [W₂.ContainsIdentities]
  [Φ.IsLocalizedEquivalence], Φ.IsRightDerivabilityStructure
-- Mathlib.Algebra.Order.Module.Defs
smul_pos_iff_of_neg_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] [PosSMulReflectLT α β], a < 0 → (0 < a • b ↔ b < 0)
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`, then `X` is integrable.  -/
ProbabilityTheory.integrable_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  0 ∈ interior (ProbabilityTheory.integrableExpSet X μ) → MeasureTheory.Integrable X μ
-- Mathlib.Topology.Instances.Rat
Rat.uniformContinuous_abs : UniformContinuous abs
-- Mathlib.Algebra.BigOperators.Field
Finset.sum_div : ∀ {ι : Type u_1} {K : Type u_2} [inst : DivisionSemiring K] (s : Finset ι) (f : ι → K) (a : K),
  (∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Hom.c : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : AlgebraicGeometry.PresheafedSpace C} →
      (self : X.Hom Y) → Y.presheaf ⟶ (TopCat.Presheaf.pushforward C self.base).obj X.presheaf
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nhds_basis_ball_pow : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {r : ℝ},
  0 < r → r < 1 → (nhds x).HasBasis (fun x => True) fun n => Metric.ball x (r ^ n)
-- Mathlib.Order.Filter.Pointwise
/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of
`Filter α` on `Filter β`.  -/
Filter.mulAction : {α : Type u_2} → {β : Type u_3} → [inst : Monoid α] → [MulAction α β] → MulAction (Filter α) (Filter β)
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- Eta-expanded form of `HasStrictDerivAt.smul` -/
HasStrictDerivAt.fun_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'}
  {c' : 𝕜'},
  HasStrictDerivAt c c' x → HasStrictDerivAt f f' x → HasStrictDerivAt (fun i => c i • f i) (c x • f' + c' • f x) x
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_zero : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : M), f.mk' x 0 = f x
-- Mathlib.Data.Set.Countable
Set.range_enumerateCountable_subset : ∀ {α : Type u} {s : Set α} (h : s.Countable) (default : α),
  Set.range (Set.enumerateCountable h default) ⊆ insert default s
-- Mathlib.Order.Iterate
Monotone.seq_pos_lt_seq_of_lt_of_le : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x y : ℕ → α},
  Monotone f →
    ∀ {n : ℕ}, 0 < n → x 0 ≤ y 0 → (∀ k < n, x (k + 1) < f (x k)) → (∀ k < n, f (y k) ≤ y (k + 1)) → x n < y n
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- A good path object `P` is very good if `P.ι` is a (trivial) cofibration.  -/
HomotopicalAlgebra.PathObject.IsVeryGood : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.PathObject A →
          [CategoryTheory.Limits.HasBinaryProduct A A] →
            [HomotopicalAlgebra.CategoryWithFibrations C] → [HomotopicalAlgebra.CategoryWithCofibrations C] → Prop
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.map_eq_top_of_not_subset : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {I : Ideal R}, ¬↑I ⊆ (↑M)ᶜ → Ideal.map (algebraMap R S) I = ⊤
-- Mathlib.LinearAlgebra.Ray
SameRay.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (v₁ v₂ : M),
  SameRay R v₁ v₂ = (v₁ = 0 ∨ v₂ = 0 ∨ ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • v₁ = r₂ • v₂)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.preconnected_iff_reachable_eq_top : ∀ {V : Type u} (G : SimpleGraph V), G.Preconnected ↔ G.Reachable = ⊤
-- Mathlib.RingTheory.Polynomial.Basic
/-- If every coefficient of a polynomial is in an ideal `I`, then so is the polynomial itself,
multivariate version.  -/
MvPolynomial.mem_ideal_of_coeff_mem_ideal : ∀ {R : Type u} {σ : Type v} [inst : CommRing R] (I : Ideal (MvPolynomial σ R)) (p : MvPolynomial σ R),
  (∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p ∈ Ideal.comap MvPolynomial.C I) → p ∈ I
-- Mathlib.RepresentationTheory.Coinvariants
Rep.desc.congr_simp : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} [inst_2 : B.ρ.IsTrivial]
  (f f_1 : A ⟶ B), f = f_1 → Rep.desc f = Rep.desc f_1
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.insertManyIfNewUnit.eq_1 : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ α]
  (m : Std.DHashMap.Raw α fun x => Unit) (l : ρ),
  Std.DHashMap.Raw.Const.insertManyIfNewUnit m l =
    if h : 0 < m.buckets.size then ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit ⟨m, h⟩ l) else m
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_pi_Ioo : ∀ {ι : Type u_1} [inst : Fintype ι] {a b : ι → ℝ},
  MeasureTheory.volume (Set.univ.pi fun i => Set.Ioo (a i) (b i)) = ∏ i, ENNReal.ofReal (b i - a i)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentationCore.desc_var : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentationCore) {N : Type w'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N) (g : relations.G),
  (h.desc s) (solution.var g) = s.var g
-- Init.Tactics
/-- If true (the default), star-indexed lemmas (with overly-general discrimination keys
like `[*]`) are searched as a fallback when no concrete-keyed lemmas are found.
Use `-star` to disable this fallback.  -/
Lean.Parser.Tactic.LibrarySearchConfig.star : Lean.Parser.Tactic.LibrarySearchConfig → Bool
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the reverse direction of `isMaxOn_dual_iff`. -/
IsMinOn.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMinOn f s a → IsMaxOn (⇑OrderDual.toDual ∘ f) s a
-- Mathlib.Order.PiLex
Pi.toLex_strictMono : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedLT ι],
  StrictMono ⇑toLex
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.withPatternVars.loop : {α : Type} →
  Array Lean.Elab.Term.PatternVar →
    (Array Lean.Elab.Term.PatternVarDecl → Lean.Elab.TermElabM α) →
      ℕ → Array Lean.Elab.Term.PatternVarDecl → Array Lean.Name → Lean.Elab.TermElabM α
-- Init.Data.List.Impl
List.intercalate_eq_intercalateTR : @List.intercalate = @List.intercalateTR
-- Mathlib.Topology.Algebra.Group.Basic
Filter.Tendsto.const_div' : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Div G] [ContinuousDiv G] (b : G) {c : G} {f : α → G}
  {l : Filter α}, Filter.Tendsto f l (nhds c) → Filter.Tendsto (fun x => b / f x) l (nhds (b / c))
-- Mathlib.Analysis.Real.Pi.Irrational
/-- The sequence of integrals used for Cartwright's proof of irrationality of `π`.  -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.I : ℕ → ℝ → ℝ
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.commSemiring.sizeOf_spec : ∀ (id : ℕ), sizeOf (Lean.Meta.Sym.Arith.ClassifyResult.commSemiring id) = 1 + sizeOf id
-- Mathlib.Order.Interval.Basic
instLEInterval : (α : Type u_1) → [inst : LE α] → LE (Interval α)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_sup_of_normal_left : ∀ {G : Type u_1} [inst : AddGroup G] {s t : AddSubgroup G} [hs : s.Normal] {x : G},
  x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
-- Mathlib.CategoryTheory.Localization.Adjunction
CategoryTheory.Adjunction.Localization.ε_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁)
  [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (G' : CategoryTheory.Functor D₁ D₂)
  (F' : CategoryTheory.Functor D₂ D₁) [inst_5 : CategoryTheory.CatCommSq G L₁ L₂ G']
  [inst_6 : CategoryTheory.CatCommSq F L₂ L₁ F'] (X₁ : C₁),
  (CategoryTheory.Adjunction.Localization.ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) =
    CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁))
        (F'.map ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').hom.app X₁)))
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A map is a homeomorphism iff it is a surjective embedding.  -/
isHomeomorph_iff_isEmbedding_surjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f ↔ Topology.IsEmbedding f ∧ Function.Surjective f
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.prop_of_isColimit_cokernelCofork : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderCokernels] {X Y : C} {f : X ⟶ Y}
  {k : CategoryTheory.Limits.CokernelCofork f} (hk : CategoryTheory.Limits.IsColimit k), P X → P Y → P k.pt
-- Mathlib.Algebra.Module.Pi
IsSMulRegular.pi : ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → SMul α (f i)] {k : α},
  (∀ (i : I), IsSMulRegular (f i) k) → IsSMulRegular ((i : I) → f i) k
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.comp_map : ∀ {C D E : CategoryTheory.Cat} (F : C ⟶ D) (G : D ⟶ E) {X Y : ↑C} (f : X ⟶ Y),
  (CategoryTheory.CategoryStruct.comp F G).toFunctor.map f = G.toFunctor.map (F.toFunctor.map f)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Methods.propagateUp : Lean.Meta.Grind.Methods → Lean.Meta.Grind.Propagator
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- The data of a Fredholm package for `u` determines a canonical quasi-inverse of `u`.  -/
ContinuousLinearMap.FredholmPackage.quasiInverse : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] → {u : E →L[𝕜] F} → u.FredholmPackage → F →L[𝕜] E
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatOpcyclesIso.eq_1 : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  S.moduleCatOpcyclesIso = S.opcyclesIsoCokernel ≪≫ ModuleCat.cokernelIsoRangeQuotient S.f
-- Mathlib.Topology.Connected.Basic
IsConnected.prod : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {t : Set β},
  IsConnected s → IsConnected t → IsConnected (s ×ˢ t)
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.mem_localized₀ : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] (M' : Submodule R M) (x : N),
  x ∈ Submodule.localized₀ p f M' ↔ ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x
-- Aesop.RuleSet
/-- A cache of the names of all rules registered in this rule set. Invariant:
`ruleNames` contains exactly the names of the rules present in `normRules`,
`unsafeRules`, `safeRules`, `forwardRules` and `unfoldRules` and not present
in `erased`. We use this cache (a) to quickly determine whether a rule is
present in the rule set and (b) to find the full rule names associated with
the fvar or const identified by a name.
 -/
Aesop.BaseRuleSet.ruleNames : Aesop.BaseRuleSet → Lean.PHashMap Lean.Name (Aesop.UnorderedArraySet Aesop.RuleName)
-- Mathlib.Algebra.Category.CommBialgCat
/-- **Alias** of `CommBialgCat.ofIsoSelf`.

---

Forgetting to the underlying type and then building the bundled object returns the original
bialgebra.  -/
CommBialgCat.ofSelfIso : {R : Type u} → [inst : CommRing R] → (M : CommBialgCat R) → CommBialgCat.of R ↑M ≅ M
-- Init.Data.SInt.Lemmas
Int32.sub_add_cancel : ∀ (a b : Int32), a - b + b = a
-- Init.Data.List.Nat.Sum
List.sum_eq_zero_iff_forall_eq_nat : ∀ {xs : List ℕ}, xs.sum = 0 ↔ ∀ x ∈ xs, x = 0
-- Init.Data.Bool
Bool.coe_true_iff_false : ∀ {a b : Bool}, (a = true ↔ b = false) ↔ a = !b
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.map_η_comp_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.Monoidal] [adj.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.OplaxMonoidal.η G))
      (CategoryTheory.Functor.OplaxMonoidal.η F) =
    adj.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)
-- Mathlib.Data.Set.Basic
Set.eq_univ_of_forall : ∀ {α : Type u} {s : Set α}, (∀ (x : α), x ∈ s) → s = Set.univ
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.instAlgebraSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          (S : IntermediateField K L) → {E : Type u_4} → [inst_3 : Semiring E] → [Algebra L E] → Algebra (↥S) E
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.mem_iff_map_id : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {f : M →ₗ[S] M}, LinearMap.IsProj m f → ∀ {x : M}, x ∈ m ↔ f x = x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_diff_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂
-- Mathlib.NumberTheory.Cyclotomic.Basic
instCommRingCyclotomicRing : (n : ℕ) →
  (A : Type u_2) →
    (K : Type u_1) → [inst : CommRing A] → [inst_1 : Field K] → [inst_2 : Algebra A K] → CommRing (CyclotomicRing n A K)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.prod_top : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (s : Subsemigroup M),
  s.prod ⊤ = Subsemigroup.comap (MulHom.fst M N) s
-- Mathlib.Data.Sym.Basic
Sym.mem_replicate : ∀ {α : Type u_1} {n : ℕ} {a b : α}, b ∈ Sym.replicate n a ↔ n ≠ 0 ∧ b = a
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.toList_rcc : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.toList_rcc._auto_1) [Std.TransCmp cmp]
  {t : Std.DTreeMap α β cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Rcc.Sliceable.mkSlice t lowerBound...=upperBound) =
    List.filter (fun e => decide ((cmp e.fst lowerBound).isGE = true ∧ (cmp e.fst upperBound).isLE = true)) t.toList
-- Mathlib.Topology.Defs.Basic
/-- An open quotient map is surjective.  -/
IsOpenQuotientMap.surjective : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenQuotientMap f → Function.Surjective f
-- Mathlib.GroupTheory.SpecificGroups.Alternating
two_mul_nat_card_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α],
  2 * Nat.card ↥(alternatingGroup α) = Nat.card (Equiv.Perm α)
-- Init.Data.Int.Lemmas
Int.cast_ofNat_Int : ∀ {n : ℕ}, ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Pretty-prints a constant `c` as `c.{<levels>} <params> : <type>`.

If `universes` is `false`, then the universe level parameters are omitted.
 -/
Lean.PrettyPrinter.Delaborator.delabConstWithSignature : optParam Bool true → Lean.PrettyPrinter.Delaborator.Delab