mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.isCardinalPresentable_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [CategoryTheory.IsCardinalPresentable X κ], CategoryTheory.IsCardinalPresentable Y κ
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.piAntidiag_empty_zero : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ], ∅.piAntidiag 0 = {0}
-- Mathlib.Data.EReal.Inv
EReal.div_right_distrib_of_nonneg : ∀ {a b c : EReal}, 0 ≤ a → 0 ≤ b → (a + b) / c = a / c + b / c
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that the intersection according to `Ric.HasRcoIntersection`
of two ranges contains exactly those elements that are contained in both ranges.
 -/
Std.Ric.LawfulRcoIntersection : (α : Type w) → [LT α] → [LE α] → [Std.Ric.HasRcoIntersection α] → Prop
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_surjective : ∀ {R : Type u_2} [inst : CommSemiring R] (σ : Type u_3) [IsEmpty σ], Function.Surjective ⇑MvPolynomial.C
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The codomain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.WhiskerLeft.tgtM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.WhiskerLeft → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Algebra.Lie.Abelian
/-- The linear equivalence between a trivial Lie module and its underlying `R`-module.  -/
TrivialLieModule.equiv : (R : Type u_1) →
  (L : Type u_2) →
    (M : Type u_3) →
      [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → TrivialLieModule R L M ≃ₗ[R] M
-- Mathlib.RingTheory.Ideal.Maps
/-- A ring isomorphism sends a prime ideal to a prime ideal.  -/
Ideal.map_isPrime_of_equiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {F' : Type u_4} [inst_2 : EquivLike F' R S]
  [RingEquivClass F' R S] (f : F') {I : Ideal R} [I.IsPrime], (Ideal.map f I).IsPrime
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.sectionMap_freeMap_freeSection : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {I J_1 : Type u} (f : I → J_1) (i : I),
  SheafOfModules.sectionsMap (SheafOfModules.freeMap f) (SheafOfModules.freeSection i) =
    SheafOfModules.freeSection (f i)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHint.fromJson : Lean.Json → Except String Lean.Lsp.InlayHint
-- Mathlib.Algebra.Algebra.Hom
AlgHomClass.commutes : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : Semiring B} {inst_3 : Algebra R A} {inst_4 : Algebra R B} {inst_5 : FunLike F A B}
  [self : AlgHomClass F R A B] (f : F) (r : R), f ((algebraMap R A) r) = (algebraMap R B) r
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.id_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.ω₁
-- Mathlib.RingTheory.Multiplicity
multiplicity_neg : ∀ {α : Type u_1} [inst : Ring α] (a b : α), multiplicity a (-b) = multiplicity a b
-- Mathlib.SetTheory.Ordinal.Notation
ONote.scale.eq_2 : ∀ (x e : ONote) (n : ℕ+) (a : ONote), x.scale (e.oadd n a) = (x + e).oadd n (x.scale a)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.foldl_filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} [inst_1 : SizeOf C] (A : C)
  (a : T.obj A ⟶ A)
  (unit :
    autoParam (CategoryTheory.CategoryStruct.comp (T.η.app A) a = CategoryTheory.CategoryStruct.id A)
      CategoryTheory.Monad.Algebra.unit._autoParam)
  (assoc :
    autoParam (CategoryTheory.CategoryStruct.comp (T.μ.app A) a = CategoryTheory.CategoryStruct.comp (T.map a) a)
      CategoryTheory.Monad.Algebra.assoc._autoParam),
  sizeOf { A := A, a := a, unit := unit, assoc := assoc } = 1 + sizeOf A + sizeOf a + sizeOf unit + sizeOf assoc
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittPow.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (n n_1 : ℕ),
  n = n_1 → ∀ (a a_1 : ℕ), a = a_1 → WittVector.wittPow p n a = WittVector.wittPow p_1 n_1 a_1
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isOpenEmbedding_inclusion_principal : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ {S : Set ι} (hS : Filter.cofinite ≤ Filter.principal S),
      Topology.IsOpenEmbedding (RestrictedProduct.inclusion R A hS)
-- Init.Data.List.SplitOn.Lemmas
List.splitOnP_ne_nil : ∀ {α : Type u_1} (p : α → Bool) (xs : List α), List.splitOnP p xs ≠ []
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {k k' : α}, compare k k' = Ordering.eq → t.getKey! k = t.getKey! k'
-- Aesop.Index.Basic
Aesop.IndexingMode.brecOn_2.eq : ∀ {motive_1 : Aesop.IndexingMode → Sort u} {motive_2 : Array Aesop.IndexingMode → Sort u}
  {motive_3 : List Aesop.IndexingMode → Sort u} (t : List Aesop.IndexingMode)
  (F_1 : (t : Aesop.IndexingMode) → t.below → motive_1 t)
  (F_2 : (t : Array Aesop.IndexingMode) → Aesop.IndexingMode.below_1 t → motive_2 t)
  (F_3 : (t : List Aesop.IndexingMode) → Aesop.IndexingMode.below_2 t → motive_3 t),
  Aesop.IndexingMode.brecOn_2 t F_1 F_2 F_3 = F_3 t (Aesop.IndexingMode.brecOn_2.go t F_1 F_2 F_3).2
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.mem_inv_iff : ∀ {K : Type u_3} [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K},
  I ≠ 0 → ∀ {x : K}, x ∈ I⁻¹ ↔ ∀ y ∈ I, x * y ∈ 1
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- If `K ⊆ L`, the components outside of `L` are all contained in a single component outside of `K`.
 -/
SimpleGraph.ComponentCompl.hom : {V : Type u} → {G : SimpleGraph V} → {K L : Set V} → K ⊆ L → G.ComponentCompl L → G.ComponentCompl K
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.wf.match_1.eq_1 : ∀ {α : Type u_1} (γ : Type u_1) (Pl : α → γ → ForInStep γ → Prop) (acc : γ) (next : α)
  (motive : { s // Pl next acc s } → Sort u_2) (acc' : γ) (property : Pl next acc (ForInStep.yield acc'))
  (h_1 : (acc' : γ) → (property : Pl next acc (ForInStep.yield acc')) → motive ⟨ForInStep.yield acc', property⟩)
  (h_2 : (acc' : γ) → (property : Pl next acc (ForInStep.done acc')) → motive ⟨ForInStep.done acc', property⟩),
  (match ⟨ForInStep.yield acc', property⟩ with
    | ⟨ForInStep.yield acc', property⟩ => h_1 acc' property
    | ⟨ForInStep.done acc', property⟩ => h_2 acc' property) =
    h_1 acc' property
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasPDF.hasLaw : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} [h : MeasureTheory.HasPDF X P μ],
  ProbabilityTheory.HasLaw X (μ.withDensity (MeasureTheory.pdf X P μ)) P
-- Lean.Meta.Tactic.Grind.PropagatorAttr
_private.Lean.Meta.Tactic.Grind.PropagatorAttr.0.Lean.Meta.Grind.registerBuiltinPropagatorCore : Lean.Name → Bool → Lean.Meta.Grind.Propagator → IO Unit
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
/-- Applies the given variable permutation to `e`  -/
Nat.Internal.Linear.Expr.applyPerm : Lean.Perm → Nat.Internal.Linear.Expr → Nat.Internal.Linear.Expr
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
tprod_one_add : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommSemiring α] [inst_1 : TopologicalSpace α] {f : ι → α} [T2Space α],
  (Summable fun x => ∏ i ∈ x, f i) → ∏' (i : ι), (1 + f i) = ∑' (s : Finset ι), ∏ i ∈ s, f i
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_eq_zero : ∀ {α : Type u_1} [inst : Zero α] {a : αᵒᵈ}, OrderDual.ofDual a = 0 ↔ a = 0
-- Mathlib.Algebra.Ring.Int.Parity
Int.isSquare_natCast_iff : ∀ {n : ℕ}, IsSquare ↑n ↔ IsSquare n
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.regularTopology.instIsCoverDense : ∀ {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) [F.EffectivelyEnough]
  [inst_3 : CategoryTheory.Preregular D], F.IsCoverDense (CategoryTheory.regularTopology D)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_bot : ∀ {α : Type u_1} [inst : LE α] {a : α}, a ∈ ⊥
-- Mathlib.Order.SuccPred.Archimedean
exists_pred_iterate_iff_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [IsPredArchimedean α] {a b : α},
  (∃ n, Order.pred^[n] a = b) ↔ b ≤ a
-- Std.Data.TreeSet.Slice
Std.TreeSet.instSliceableRciSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.instSliceableRciSlice._auto_1) →
    Std.Rci.Sliceable (Std.TreeSet α cmp) α (Std.DTreeMap.Internal.Unit.RciSlice α)
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.genericMonicPolyHasRoot.eq_1 : ∀ (n : ℕ),
  FirstOrder.Field.genericMonicPolyHasRoot n =
    ((FirstOrder.Language.Term.relabel Sum.inr
              (FirstOrder.Ring.termOfFreeCommRing (FirstOrder.Field.genericMonicPoly n))).bdEqual
          0).ex.alls
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.neg_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Neg α] (A : Matrix m n α) (i : m) (j : n), (-A) i j = -A i j
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.centeredArc_eq_empty : ∀ {r : ℝ}, r ≤ 0 → Circle.centeredArc r = ∅
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The homogeneous components of an `MvPowerSeries`  -/
MvPowerSeries.homogeneousComponent : {σ : Type u_1} → {R : Type u_2} → [inst : Semiring R] → ℕ → MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- a morphism between the underlying presheaves of modules  -/
SheafOfModules.Hom.val : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} → {X Y : SheafOfModules R} → X.Hom Y → (X.val ⟶ Y.val)
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (N : ℕ) (f : AddMonoidAlgebra R ℕ),
  Polynomial.reflect N { toFinsupp := f } =
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.embDomain (Polynomial.revAt N) f.coeff) }
-- Mathlib.Tactic.Simps.NotationClass
Simps.instInhabitedAutomaticProjectionData.default : Simps.AutomaticProjectionData
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.tryCatch_MonadExcept : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε : Type u_1} {α : Type u}
  {post : α → Pred} {epost : EPred} [inst_4 : MonadExceptOf ε m] (x : m α) (h : ε → m α),
  ⦃ Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost ⦄ tryCatch x h ⦃ post; epost ⦄
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.cof_omega_one : (Ordinal.omega 1).cof = Cardinal.aleph 1
-- Mathlib.Order.Interval.Finset.Defs
/-- Left-infinite right-closed interval  -/
LocallyFiniteOrderBot.finsetIic : {α : Type u_1} → {inst : Preorder α} → [self : LocallyFiniteOrderBot α] → α → Finset α
-- Mathlib.Algebra.Group.Action.Pi
/-- Non-dependent version of `Pi.smul`. Lean gets confused by the dependent instance if this
is not present.  -/
Function.hasSMul : {ι : Type u_1} → {M : Type u_2} → {α : Type u_7} → [SMul M α] → SMul M (ι → α)
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.coeff_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : CommSemiring R]
  (p : MvPowerSeries σ R) (x : τ →₀ ℕ),
  (MvPowerSeries.coeff x) ((MvPowerSeries.rename f) p) = ∑ x ∈ ⋯.toFinset, (MvPowerSeries.coeff x) p
-- Mathlib.Data.Multiset.DershowitzManna
/-- `TransGen OneStep` and `IsDershowitzMannaLT` are equivalent.  -/
_private.Mathlib.Data.Multiset.DershowitzManna.0.Multiset.transGen_oneStep_eq_isDershowitzMannaLT : ∀ {α : Type u_1} [inst : Preorder α], Relation.TransGen Multiset.OneStep✝ = Multiset.IsDershowitzMannaLT
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescaleAlgHom.eq_1 : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (a : σ → R),
  MvPowerSeries.rescaleAlgHom a = MvPowerSeries.substAlgHom ⋯
-- Mathlib.SetTheory.ZFC.Class
Class.mem_of_mem_sInter : ∀ {x y z : Class.{u_1}}, y ∈ x.sInter → z ∈ x → y ∈ z
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The `logSpace` is defined as `{w : InfinitePlace K // w ≠ w₀} → ℝ` where `w₀` is the
distinguished infinite place.  -/
NumberField.Units.dirichletUnitTheorem.logSpace : (K : Type u_1) → [inst : Field K] → [NumberField K] → Type (max 0 u_1)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.height_add_zsmul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R] {i j k : ι} {z : ℤ},
  P.root k = P.root i + z • P.root j → b.height k = b.height i + z • b.height j
-- Mathlib.Topology.Semicontinuity.Basic
IsClosed.lowerSemicontinuous_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {y : β} [inst_1 : Zero β] [inst_2 : Preorder β],
  IsClosed s → y ≤ 0 → LowerSemicontinuous (s.indicator fun _x => y)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_union_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) (s t : Set α),
  ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in t, f a ∂μ
-- Init.Data.UInt.Lemmas
USize.ofNatTruncate_uInt16ToNat : ∀ (n : UInt16), USize.ofNatClamp n.toNat = n.toUSize
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_toArray_roo : ∀ {m n : ℤ}, (m<...n).toArray.toList = (m<...n).toList
-- Mathlib.CategoryTheory.Square
/-- The bottom-right evaluation `Square C ⥤ C`.  -/
CategoryTheory.Square.evaluation₄ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.Square C) C
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.smul_unit_iff : ∀ {M₁ : Type u_3} {M₂ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {S : Type u_6} [inst_4 : Monoid S]
  [inst_5 : DistribMulAction S M₂] [ContinuousConstSMul S M₂] {f : M₁ → M₂} {c : Sˣ},
  IsCompactOperator (c • f) ↔ IsCompactOperator f
-- Mathlib.Analysis.SpecificLimits.Basic
NNRat.tendsto_inv_atTop_nhds_zero_nat : Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `true` if `e` is `instLENat`  -/
Lean.Meta.Grind.Arith.isInstLENat : Lean.Expr → Bool
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₁ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₁
-- Mathlib.RingTheory.Ideal.Height
Ideal.exists_ltSeries_length_eq_height : ∀ {R : Type u_1} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsPrime] [p.FiniteHeight],
  ∃ l, RelSeries.last l = { asIdeal := p, isPrime := ⋯ } ∧ ↑l.length = p.height
-- Mathlib.Data.PFun
PFun.restrict.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) {p : Set α} (H : p ⊆ f.Dom) (x : α),
  f.restrict H x = Part.restrict (x ∈ p) (f x) ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.Flat
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {combined w n : ℕ}
  {inner : aig.RefVec w} {h : combined = w * n} {w_1 n_1 : ℕ} {inner_1 : aig.RefVec w_1} {h_1 : combined = w_1 * n_1},
  { w := w, n := n, inner := inner, h := h } = { w := w_1, n := n_1, inner := inner_1, h := h_1 } →
    w = w_1 ∧ n = n_1 ∧ inner ≍ inner_1
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.propagateDiseqs.go.eq_def : ∀ (lhsTerms rhsTerms : Lean.Meta.Grind.SolverTerms),
  Lean.Meta.Grind.Solvers.propagateDiseqs.go✝ lhsTerms rhsTerms =
    match lhsTerms, rhsTerms with
    | Lean.Meta.Grind.SolverTerms.nil, x => pure ()
    | x, Lean.Meta.Grind.SolverTerms.nil => pure ()
    | Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms =>
      if (id₁ == id₂) = true then do
        let __do_lift ← ST.Ref.get Lean.Meta.Grind.solverExtensionsRef✝
        __do_lift[id₁]!.newDiseq lhs rhs
        Lean.Meta.Grind.Solvers.propagateDiseqs.go✝ lhsTerms rhsTerms
      else
        if id₁ < id₂ then
          Lean.Meta.Grind.Solvers.propagateDiseqs.go✝ lhsTerms (Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms)
        else Lean.Meta.Grind.Solvers.propagateDiseqs.go✝ (Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms) rhsTerms
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.iSup_natCast_lt_top`. -/
ENat.iSup_coe_lt_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨆ i, ↑(f i) < ⊤ ↔ BddAbove (Set.range f)
-- Mathlib.Algebra.Opposites
MulOpposite.instDecidableEq.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α], MulOpposite.instDecidableEq = ⋯.decidableEq
-- Init.Data.Nat.Div.Basic
Nat.add_mul_div_left : ∀ (x z : ℕ) {y : ℕ}, 0 < y → (x + y * z) / y = x / y + z
-- Mathlib.NumberTheory.Pell
/-- An element of `ℤ√d` has norm one (i.e., `a.re^2 - d*a.im^2 = 1`) if and only if
it is contained in the submonoid of unitary elements.

TODO: merge this result with `Pell.isPell_iff_mem_unitary`.  -/
Pell.is_pell_solution_iff_mem_unitary : ∀ {d : ℤ} {a : ℤ√d}, a.re ^ 2 - d * a.im ^ 2 = 1 ↔ a ∈ unitary (ℤ√d)
-- Mathlib.Topology.Spectral.Prespectral
/-- A space is prespectral if it has a basis consisting of compact opens.
This is the variant with an indexed basis instead.  -/
PrespectralSpace.of_isTopologicalBasis' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {b : ι → Set X},
  TopologicalSpace.IsTopologicalBasis (Set.range b) → (∀ (i : ι), IsCompact (b i)) → PrespectralSpace X
-- Init.Prelude
/-- A (named) nullary parser, like `ppSpace`  -/
Lean.ParserDescr.const : Lean.Name → Lean.ParserDescr
-- Mathlib.Analysis.Complex.Poisson
_private.Mathlib.Analysis.Complex.Poisson.0.poissonKernel_eq_re_herglotzRieszKernel_aux : ∀ {a b : ℂ}, ((a + b) / (a - b)).re = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.one_mem_dilatransvections : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  1 ∈ LinearEquiv.dilatransvections R V
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.EssImageSubcategory.lift_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Full] [inst_5 : F.Faithful]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteProducts F] {T X Y : F.EssImageSubcategory} (f : T ⟶ X) (g : T ⟶ Y),
  CategoryTheory.CartesianMonoidalCategory.lift f g =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom)
-- Mathlib.Data.FinEnum
FinEnum.punit : FinEnum PUnit.{u_1 + 1}
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.IsLE.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {t : CategoryTheory.Triangulated.TStructure C} {X : C} {n : ℤ}, t.le n X → t.IsLE X n
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) {y z : D} (f : y ≅ z) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f.hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f.inv) h) =
    h
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.top_iff : ∀ {G : Type u_1} {A : Type u_2} {B : Type u_4} [inst : Group G] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B], IsGaloisGroup (↥⊤) A B ↔ IsGaloisGroup G A B
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.e_assoc_assoc : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] (W X Y Z : C) {Z_1 : V} (h : (W ⟶[V] Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W Y Z) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W X Z) h)
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
CategoryTheory.Bundled.mk : {c : Type u → Type v} → (α : Type u) → autoParam (c α) CategoryTheory.Bundled.str._autoParam → CategoryTheory.Bundled c
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mk : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  (toFun : ((i : ι) → M₁ i) → M₂) →
                    (∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
                        toFun (Function.update m i (x + y)) =
                          toFun (Function.update m i x) + toFun (Function.update m i y)) →
                      (∀ [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
                          toFun (Function.update m i (c • x)) = c • toFun (Function.update m i x)) →
                        MultilinearMap R M₁ M₂