mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.instDecidableEqKey.decEq : (x x_1 : Std.Tactic.BVDecide.BVExpr.Cache.Key) → Decidable (x = x_1)
-- Mathlib.Algebra.GroupWithZero.Basic
pow_mul_eq_zero_of_le : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a b : M₀} {m n : ℕ}, m ≤ n → a ^ m * b = 0 → a ^ n * b = 0
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_invOf : ∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Semiring R] [inst_2 : Module Rᵐᵒᵖ M] [inst_3 : Module R M]
  [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) [inst_5 : Invertible x] [inst_6 : Invertible x.fst],
  (⅟x).snd = -(MulOpposite.op ⅟x.fst • ⅟x.fst • x.snd)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- Naturality square for morphisms in the inverse direction.  -/
CategoryTheory.Limits.CategoricalPullback.Hom.w' : ∀ {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 y : CategoryTheory.Limits.CategoricalPullback F G} (f : x ⟶ y),
  CategoryTheory.CategoryStruct.comp (G.map f.snd) y.iso.inv =
    CategoryTheory.CategoryStruct.comp x.iso.inv (F.map f.fst)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.isColimit_coconeTypes : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)),
  F.coconeTypes.IsColimit
-- Lean.Server.InfoUtils
Lean.Elab.InfoWithCtx.mk.injEq : ∀ (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.Info) (children : Lean.PersistentArray Lean.Elab.InfoTree)
  (ctx_1 : Lean.Elab.ContextInfo) (info_1 : Lean.Elab.Info) (children_1 : Lean.PersistentArray Lean.Elab.InfoTree),
  ({ ctx := ctx, info := info, children := children } = { ctx := ctx_1, info := info_1, children := children_1 }) =
    (ctx = ctx_1 ∧ info = info_1 ∧ children = children_1)
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_max : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R),
  Tropical.untrop (max x y) = max (Tropical.untrop x) (Tropical.untrop y)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_alter_of_beq_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (k == k') = false → (m.alter k f).contains k' = m.contains k'
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} [inst_2 : Inhabited β],
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.ofList l cmp) k = default
-- Init.Data.SInt.Lemmas
Int32.mul_add : ∀ {a b c : Int32}, a * (b + c) = a * b + a * c
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instSupSet : {E : Type u_3} → [inst : Group E] → SupSet (GroupSeminorm E)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- **Alias** of `NNReal.finsetProd_rpow`.

---

`rpow` version of `Finset.prod_pow` for `ℝ≥0`.  -/
NNReal.finset_prod_rpow : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) (r : ℝ), ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
/-- **Alias** of `EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF`.

---

Eisenstein series are bounded at infinity.  -/
EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF : ∀ {N : ℕ} [NeZero N] (a : Fin 2 → ZMod N) {k : ℤ},
  3 ≤ k →
    ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ),
      UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k A ⇑(EisensteinSeries.eisensteinSeriesSIF a k))
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.mulI_sup : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S T : ClosedSubmodule ℝ H),
  (S ⊔ T).mulI = S.mulI ⊔ T.mulI
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_iff_has_add_complement : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment) (b : Bool),
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b assignment = true ↔
    Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b
        (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment (decide ¬b = true) assignment) =
      true
-- Mathlib.Logic.Equiv.List
/-- If `α` is denumerable, then so is `List α`.  -/
Denumerable.denumerableList : {α : Type u_1} → [Denumerable α] → Denumerable (List α)
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.preprocess.normLevels : Lean.Level → Array ℕ → List Lean.Level → ℕ → List Lean.Level
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.inclusionPathAux.eq_def : ∀ {B : Type u} [inst : Quiver B] {a : B} (x : B) (x_1 : Quiver.Path a x),
  CategoryTheory.FreeBicategory.inclusionPathAux x_1 =
    match x, x_1 with
    | .(a), Quiver.Path.nil => CategoryTheory.FreeBicategory.Hom.id a
    | x, p.cons f => (CategoryTheory.FreeBicategory.inclusionPathAux p).comp (CategoryTheory.FreeBicategory.Hom.of f)
-- Mathlib.Order.Compare
Ordering.compares_iff_of_compares_impl : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {a' b' : β},
  (∀ {o : Ordering}, o.Compares a b → o.Compares a' b') → ∀ (o : Ordering), o.Compares a b ↔ o.Compares a' b'
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instFaithfulTopCatToGeneratedByTopCat : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)], TopCat.toGeneratedByTopCat.Faithful
-- Mathlib.ModelTheory.Order
/-- A language is ordered if it has a symbol representing `≤`.  -/
FirstOrder.Language.IsOrdered : FirstOrder.Language → Type v
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- Returns `some (p, c, s)` if `s₁ == p ++ c` and `s₂ == c ++ s`
 -/
Lean.Grind.AC.Seq.superpose? : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Option (Lean.Grind.AC.Seq × Lean.Grind.AC.Seq × Lean.Grind.AC.Seq)
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
complex normed space.  Let `f : E → F` be a function that is complex differentiable on `U`. Suppose
that `‖f x‖` takes its maximum value on `U` at `c ∈ U`. Then `f x = f c` for all `x ∈ U`.

TODO: change assumption from `IsMaxOn` to `IsLocalMax`.  -/
Complex.eqOn_of_isPreconnected_of_isMaxOn_norm : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [StrictConvexSpace ℝ F] {f : E → F} {U : Set E} {c : E},
  IsPreconnected U →
    IsOpen U → DifferentiableOn ℂ f U → c ∈ U → IsMaxOn (norm ∘ f) U c → Set.EqOn f (Function.const E (f c)) U
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableAtom.eq_1 : ∀ {β : Type u_2} [inst : MeasurableSpace β] (x : β), measurableAtom x = ⋂ s, ⋂ (_ : x ∈ s), ⋂ (_ : MeasurableSet s), s
-- Init.Data.String.Pattern.Basic
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.SearchStep.ofSliceFrom.eq_2 : ∀ {s : String.Slice} {p : s.Pos} (l r : (s.sliceFrom p).Pos),
  (String.Slice.Pattern.SearchStep.matched l r).ofSliceFrom =
    String.Slice.Pattern.SearchStep.matched (String.Slice.Pos.ofSliceFrom l) (String.Slice.Pos.ofSliceFrom r)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F` which is generated by
`S` as an `F`-module, then `E[L]` is generated by `S` as an `E`-module.  -/
Subalgebra.adjoin_eq_span_of_eq_span : ∀ {F : Type u_1} (E : Type u_2) {K : Type u_3} [inst : CommSemiring E] [inst_1 : Semiring K] [inst_2 : SMul F E]
  [inst_3 : Algebra E K] [inst_4 : CommSemiring F] [inst_5 : Algebra F K] [IsScalarTower F E K] (L : Subalgebra F K)
  {S : Set K},
  Subalgebra.toSubmodule L = Submodule.span F S → Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E S
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `v` belongs to the interior of the interval `integrableExpSet X μ`,
then `X ^ n * exp (v * X)` is integrable for all `n : ℕ`.  -/
ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ), MeasureTheory.Integrable (fun ω => X ω ^ n * Real.exp (v * X ω)) μ
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The red and the blue arrows in ![this diagram](https://i.imgur.com/0GiBUh6.png) commute.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.V (i, j))) {Z : C}
  (h :
    ((TopCat.Presheaf.pushforward C (D.f i k).base).obj (D.V (i, k)).presheaf).obj
        (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f i j)).obj U)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (D.f i j) U)
      (CategoryTheory.CategoryStruct.comp
        ((D.f i k).c.app
          (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f i j)).obj U)))
        h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
          (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))
          ((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).base).1 U))
        (CategoryTheory.CategoryStruct.comp ((D.V (i, k)).presheaf.map (CategoryTheory.eqToHom ⋯)) h))
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_right_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  nndist p₂ ((AffineMap.lineMap p₁ p₂) c) = ‖1 - c‖₊ * nndist p₁ p₂
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.symm.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'), equiv.symm = { toAddEquiv := equiv.symm, inl_comm := ⋯, rightHom_comm := ⋯ }
-- Mathlib.Tactic.CrossRefAttribute
/-- The external database the entry belongs to.  -/
Mathlib.CrossRef.Tag.database : Mathlib.CrossRef.Tag → Mathlib.CrossRef.Database
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.setTR.eq_1 : ∀ {α : Type u_1} (l : List α) (n : ℕ) (a : α), l.setTR n a = List.setTR.go✝ l a l n #[]
-- Lean.MetavarContext
Lean.MetavarKind.isNatural : Lean.MetavarKind → Bool
-- Mathlib.CategoryTheory.Sites.Pullback
/-- Construction of the pullback of sheaves using a left Kan extension.  -/
CategoryTheory.Functor.sheafPullbackConstruction.sheafPullback : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        (G : CategoryTheory.Functor C D) →
          (A : Type u₁) →
            [inst_2 : CategoryTheory.Category.{v₁, u₁} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] →
                    [CategoryTheory.HasWeakSheafify K A] →
                      CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf K A)
-- Mathlib.Combinatorics.Graph.Maps
Graph.IsSubgraph.map : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G H : Graph α β} (f : α → α'), G ≤ H → Graph.map f G ≤ Graph.map f H
-- Mathlib.Topology.DerivedSet
mem_derivedSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {A : Set X} {x : X}, x ∈ derivedSet A ↔ AccPt x (Filter.principal A)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.X_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {i : σ}, MvPowerSeries.HasSubst ![MvPowerSeries.X i, 0]
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.transitivity₁_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.TransitiveRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_1 : CategoryTheory.ConcreteCategory C F]
  (x : carrier self.c.pt),
  (CategoryTheory.ConcreteCategory.hom p₁) ((CategoryTheory.ConcreteCategory.hom self.t) x) =
    (CategoryTheory.ConcreteCategory.hom p₁) ((CategoryTheory.ConcreteCategory.hom self.c.fst) x)
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.Category.{t, v} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections],
  Small.{w, max v w} ↥(ModuleCat.sectionsSubmodule F)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Iso.symm_apply_reachable : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {u : V} {v : V'},
  G.Reachable (φ.symm v) u ↔ G'.Reachable v (φ u)
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {a : α}, t.WF → (t.erase a).WF
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listEncode_sigma_injective : ∀ {L : FirstOrder.Language} {α : Type u'}, Function.Injective fun φ => φ.snd.listEncode
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.divAll.eq_def : ∀ (k : ℤ) (x : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.divAll k x =
    match x with
    | Int.Internal.Linear.Poly.num k' => k' % k == 0
    | Int.Internal.Linear.Poly.add k' v p => k' % k == 0 && Int.Internal.Linear.Poly.divAll k p
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Answer.mk.injEq : ∀ (result : Lean.Meta.AbstractMVarsResult) (resultType : Lean.Expr) (size : ℕ)
  (result_1 : Lean.Meta.AbstractMVarsResult) (resultType_1 : Lean.Expr) (size_1 : ℕ),
  ({ result := result, resultType := resultType, size := size } =
      { result := result_1, resultType := resultType_1, size := size_1 }) =
    (result = result_1 ∧ resultType = resultType_1 ∧ size = size_1)
-- Mathlib.Data.FunLike.Group
FunLike.monoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : Monoid β] [inst_5 : IsOneApply F α β] [inst_6 : IsMulApply F α β]
  [inst_7 : IsPowApply ℕ F α β], FunLike.monoid = Function.Injective.monoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidates_dist_inr : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.ProdSpaceFun✝ X Y},
  f ∈ GromovHausdorff.candidates X Y → ∀ (x y : Y), f (Sum.inr x, Sum.inr y) = dist x y
-- Std.Do.Triple.SpecLemmas
/-- Advances the cursor by one position, moving the current element from the suffix to the prefix.

Requires that the cursor is not already at the end of the list.
 -/
List.Cursor.tail : {α : Type u_1} → {l : List α} → (s : l.Cursor) → autoParam (0 < s.suffix.length) List.Cursor.tail._auto_1 → l.Cursor
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.ext : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.Clopens α}, ↑s = ↑t → s = t
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
MetricSpace.toIsCompletelyMetrizableSpace : ∀ {X : Type u_1} [inst : MetricSpace X] [CompleteSpace X], TopologicalSpace.IsCompletelyMetrizableSpace X
-- Mathlib.Analysis.Analytic.ChangeOrigin
HasFPowerSeriesOnBall.analyticOnNhd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → AnalyticOnNhd 𝕜 f (Metric.eball x r)
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.coe_inv_val_mul_coe_val : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {x : (↥S)ˣ}, ↑↑x⁻¹ * ↑↑x = 1
-- Mathlib.CategoryTheory.Action.Monoidal
Action.instLeftRigidCategoryFunctorSingleObj : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (H : Type u_3) →
        [inst_2 : Group H] →
          [CategoryTheory.LeftRigidCategory V] →
            CategoryTheory.LeftRigidCategory (CategoryTheory.Functor (CategoryTheory.SingleObj H) V)
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveExprProps : Type
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.basicOpen_zero : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], ProjectiveSpectrum.basicOpen 𝒜 0 = ⊥
-- Mathlib.Control.Bitraversable.Instances
_private.Mathlib.Control.Bitraversable.Instances.0.Prod.bitraverse.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} → (motive : α × β → Sort u_3) → (x : α × β) → ((x : α) → (y : β) → motive (x, y)) → motive x
-- Mathlib.Analysis.InnerProductSpace.Semisimple
/-- Symmetric operators are semisimple on finite-dimensional subspaces.  -/
LinearMap.IsSymmetric.isFinitelySemisimple : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : Module.End 𝕜 E}, LinearMap.IsSymmetric T → T.IsFinitelySemisimple
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.source_subset_preimage_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x), h.domChart.source ⊆ f ⁻¹' h.codChart.source
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.AnalyzeResult.mk.inj : ∀ {maxS? : Option FBinopElab.SRec} {hasUncomparable : Bool} {maxS?_1 : Option FBinopElab.SRec}
  {hasUncomparable_1 : Bool},
  { maxS? := maxS?, hasUncomparable := hasUncomparable } = { maxS? := maxS?_1, hasUncomparable := hasUncomparable_1 } →
    maxS? = maxS?_1 ∧ hasUncomparable = hasUncomparable_1
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.not_isAddCyclic : ∀ {G : Type u_1} [inst : AddGroup G] [IsAddKleinFour G], ¬IsAddCyclic G
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.CaseArraySizesSubgoal.mk.inj : ∀ {mvarId : Lean.MVarId} {elems diseqs : Array Lean.FVarId} {subst : Lean.Meta.FVarSubst} {mvarId_1 : Lean.MVarId}
  {elems_1 diseqs_1 : Array Lean.FVarId} {subst_1 : Lean.Meta.FVarSubst},
  { mvarId := mvarId, elems := elems, diseqs := diseqs, subst := subst } =
      { mvarId := mvarId_1, elems := elems_1, diseqs := diseqs_1, subst := subst_1 } →
    mvarId = mvarId_1 ∧ elems = elems_1 ∧ diseqs = diseqs_1 ∧ subst = subst_1
-- Mathlib.Data.Rel
SetRel.image_union : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (s₁ s₂ : Set α), R.image (s₁ ∪ s₂) = R.image s₁ ∪ R.image s₂
-- Mathlib.Data.Stream.Init
Stream'.inits_tail : ∀ {α : Type u} (s : Stream' α), s.tail.inits = Stream'.initsCore [s.tail.head] s.tail.tail
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
RingEquiv.nonUnitalSubsemiringMap_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] (e : R ≃+* S)
  (s : NonUnitalSubsemiring R) (x : ↑↑s.toAddSubmonoid), ↑((e.nonUnitalSubsemiringMap s) x) = e ↑x
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_aleph_add_one : ∀ (o : Ordinal.{u_1}), (Cardinal.aleph (o + 1)).IsRegular
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → t.get? t.min! = some t.min!
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.exists_add_nnrealPart_add_eq : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f g : CompactlySupportedContinuousMap α ℝ),
  ∃ h,
    (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
-- Mathlib.Topology.Category.Born
Born.of.inj : ∀ {carrier : Type u_1} {str : Bornology carrier} {carrier_1 : Type u_1} {str_1 : Bornology carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.unbot_le_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithZero α} {b : α} (hx : x ≠ 0), WithZero.unzero hx ≤ b ↔ x ≤ ↑b
-- Init.Grind.AC
Lean.Grind.AC.superpose_ac_cert : Lean.Grind.AC.Seq →
  Lean.Grind.AC.Seq →
    Lean.Grind.AC.Seq →
      Lean.Grind.AC.Seq →
        Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card
Cardinal.mk_smul_set₀ : ∀ {G₀ : Type u_1} {M₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Zero M₀] [inst_2 : MulActionWithZero G₀ M₀]
  {a : G₀}, a ≠ 0 → ∀ (s : Set M₀), Cardinal.mk ↑(a • s) = Cardinal.mk ↑s
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sum_map_seq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ] (f : β → γ),
  (ProbabilityTheory.Kernel.sum fun n => (κ.seq n).map f) = κ.map f
-- Mathlib.LinearAlgebra.Contraction
TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse : ∀ {R : Type u_7} {M : Type u_8} {N : Type u_9} {ι : Type u_10} {κ : Type u_11} [inst : DecidableEq ι]
  [inst_1 : DecidableEq κ] [inst_2 : Fintype ι] [inst_3 : Fintype κ] [inst_4 : CommSemiring R]
  [inst_5 : AddCommMonoid M] [inst_6 : AddCommMonoid N] [inst_7 : Module R M] [inst_8 : Module R N]
  (b : Module.Basis ι R M) (c : Module.Basis κ R N),
  TensorProduct.dualDistribInvOfBasis b c ∘ₗ TensorProduct.dualDistrib R M N = LinearMap.id
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.CombinatorAttribute.ext : Lean.ParserCompiler.CombinatorAttribute →
  Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (n curr : ℕ) (hcurr : curr ≤ n)
  (input : aig.RefVec w) (s : aig.RefVec (w * curr)) (idx : ℕ) (hidx : idx < w * curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go n input curr hcurr s).get idx ⋯ = s.get idx hidx
-- Std.Http.Data.URI.Basic
/-- Fragment identifier (will be encoded when building).
 -/
Std.Http.URI.Builder.fragment : Std.Http.URI.Builder → Option String
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b