mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The pullback functor along `f`.  -/
CategoryTheory.ChosenPullbacksAlong.pullback : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {Y X : C} →
      (f : Y ⟶ X) →
        [self : CategoryTheory.ChosenPullbacksAlong f] →
          CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over Y)
-- Lean.Meta.Structure
Lean.Meta.StructProjDecl.mk.injEq : ∀ (ref : Lean.Syntax) (projName : Lean.Name) (paramInfoOverrides : List (Option Lean.BinderInfo)) (ref_1 : Lean.Syntax)
  (projName_1 : Lean.Name) (paramInfoOverrides_1 : List (Option Lean.BinderInfo)),
  ({ ref := ref, projName := projName, paramInfoOverrides := paramInfoOverrides } =
      { ref := ref_1, projName := projName_1, paramInfoOverrides := paramInfoOverrides_1 }) =
    (ref = ref_1 ∧ projName = projName_1 ∧ paramInfoOverrides = paramInfoOverrides_1)
-- Mathlib.Topology.Compactness.Compact
Quot.compactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] {r : X → X → Prop} [CompactSpace X], CompactSpace (Quot r)
-- Mathlib.Topology.Sheaves.Skyscraper
SkyscraperPresheafFunctor.map'_id : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{w, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] {a : C},
  SkyscraperPresheafFunctor.map' p₀ (CategoryTheory.CategoryStruct.id a) =
    CategoryTheory.CategoryStruct.id (skyscraperPresheaf p₀ a)
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.instSliceableRiiSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.instSliceableRiiSlice._auto_1) →
      Std.Rii.Sliceable (Std.DTreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.RiiSlice α β)
-- Mathlib.Algebra.Module.PID
/-- **Structure theorem of finitely generated modules over a PID** : A finitely generated
module over a PID is isomorphic to the product of a free module and a direct sum of some
`R ⧸ R ∙ (p i ^ e i)` where the `p i ^ e i` are prime powers.  -/
Module.equiv_free_prod_directSum : ∀ (R : Type u) [inst : CommRing R] [IsPrincipalIdealRing R] (M : Type v) [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] [h' : Module.Finite R M],
  ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (M ≃ₗ[R] (Fin n →₀ R) × DirectSum ι fun i => R ⧸ R ∙ p i ^ e i)
-- Init.Data.Array.Lemmas
Array.flatten_toArray : ∀ {α : Type u_1} {l : List (Array α)}, l.toArray.flatten = (List.map Array.toList l).flatten.toArray
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap : ∀ {𝕜 : Type u_1} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] {ι : Type u_5} {Em : ι → Type u_6} {Fm : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (Em i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Fm i)] [inst_7 : Fintype ι]
  {t : Set (((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G)}
  {q : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G},
  AnalyticWithinAt 𝕜 (fun p => p.2.compContinuousLinearMap p.1) t q
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.coe_center : ∀ (M : Type u_1) [inst : MulOneClass M], ↑(Submonoid.center M) = Set.center M
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_neg_add_iff_add_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, b < -a + c ↔ a + b < c
-- Std.Http.Data.Method
Std.Http.instBEqMethod.beq : Std.Http.Method → Std.Http.Method → Bool
-- Lean.Parser.Command
Lean.Parser.Command.omit.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Char.Lemmas
Char.ltTrans : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
-- Init.Data.Vector.Lemmas
Vector.toArray_mapFinIdx : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {f : (i : ℕ) → α → i < n → β} {xs : Vector α n},
  (xs.mapFinIdx f).toArray = xs.toArray.mapFinIdx fun i a h => f i a ⋯
-- Init.Data.Nat.Lemmas
Nat.instIdempotentOpMax : Std.IdempotentOp max
-- Mathlib.RingTheory.RegularLocalRing.Polynomial
Polynomial.isRegularLocalRing_localization_atPrime_of_comap_eq_maximalIdeal : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsRegularLocalRing R] (p : Ideal (Polynomial R)) [inst_2 : p.IsPrime],
  Ideal.comap Polynomial.C p = IsLocalRing.maximalIdeal R → IsRegularLocalRing (Localization.AtPrime p)
-- Lean.Declaration
Lean.instInhabitedTheoremVal.default : Lean.TheoremVal
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS_nc : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.DimacsState.maxLit : Std.Sat.CNF.DimacsState✝ → ℕ
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra' : ∀ {ι : 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}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι], IsLieAbelian ↥(RootPairing.GeckConstruction.cartanSubalgebra' b)
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.image_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (f : F ⟶ F') (i : C),
  (G.image f).obj i = ⇑(CategoryTheory.ConcreteCategory.hom (f.app i)) '' G.obj i
-- Mathlib.Data.ENNReal.Inv
ENNReal.zpow_pos : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → ∀ (n : ℤ), 0 < a ^ n
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- When a function has a limit at infinity `l`, and its derivative is nonpositive, then the
integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see
`integrable_on_Ioi_deriv_of_nonneg'`). Version assuming differentiability on `[a, +∞)`.  -/
MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos' : ∀ {g g' : ℝ → ℝ} {a l : ℝ},
  (∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x) →
    (∀ x ∈ Set.Ioi a, g' x ≤ 0) → Filter.Tendsto g Filter.atTop (nhds l) → ∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.mem_uIcc_of_ge : ∀ {α : Type u_1} [inst : Lattice α] {a b x : α}, b ≤ x → x ≤ a → x ∈ Set.uIcc a b
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.setOfPred_finite : ∀ {α : Type u_1} [Countable α], MeasurableSet {s | s.Finite}
-- Mathlib.Geometry.Manifold.Algebra.SMul
Diffeomorph.vadd_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : AddGroup G]
  [inst_12 : AddAction G M] {n : WithTop ℕ∞} [inst_13 : ContMDiffVAdd I I' n G M] (g : G) (x : M),
  (Diffeomorph.vadd I I' n g) x = g +ᵥ x
-- Lean.Data.DeclarationRange
Lean.DeclarationRange.pos : Lean.DeclarationRange → Lean.Position
-- Mathlib.Order.Partition.Basic
Partition.partOf_rep : ∀ {α : Type u_1} {u s : Set α} {P : Partition u} (hs : s ∈ P), P.partOf (P.rep hs) = s
-- Mathlib.Algebra.CharP.Invertible
/-- When two is invertible, every element is `Even`.  -/
Even.all : ∀ {R : Type u_1} [inst : Semiring R] [Invertible 2] (a : R), Even a
-- Mathlib.Analysis.Normed.Operator.Completeness
/-- A closed ball is closed in the weak-\* topology. We don't have a name for `E →SL[σ] F` with
weak-\* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`).  -/
ContinuousLinearMap.is_weak_closed_closedBall : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6}
  [inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂] (f₀ : E' →SL[σ₁₂] F)
  (r : ℝ) ⦃f : E' →SL[σ₁₂] F⦄, ⇑f ∈ closure (DFunLike.coe '' Metric.closedBall f₀ r) → f ∈ Metric.closedBall f₀ r
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.embDomainRingHom_apply : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  {Γ' : Type u_6} [inst_3 : AddCommMonoid Γ'] [inst_4 : PartialOrder Γ'] [inst_5 : IsOrderedCancelAddMonoid Γ']
  [inst_6 : NonAssocSemiring R] (f : Γ →+ Γ') (hfi : Function.Injective ⇑f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g')
  (a : HahnSeries Γ R),
  (HahnSeries.embDomainRingHom f hfi hf) a = HahnSeries.embDomain { toFun := ⇑f, inj' := hfi, map_rel_iff' := ⋯ } a
-- Lean.Data.Position
Lean.instFromJsonPosition : Lean.FromJson Lean.Position
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_eq_fallback : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → ∀ {fallback : α}, t.minKeyD fallback = fallback
-- Mathlib.Algebra.Polynomial.Div
Polynomial.X_dvd_iff : ∀ {R : Type u} [inst : Semiring R] {f : Polynomial R}, Polynomial.X ∣ f ↔ f.coeff 0 = 0
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.eq_of_not_blt_eq_true : ∀ {x y : ℕ}, ¬x.blt y = true → ¬y.blt x = true → x = y
-- Mathlib.Analysis.Normed.MulAction
NormMulClass.toNormSMulClass_op : ∀ {α : Type u_1} [inst : SeminormedRing α] [NormMulClass α], NormSMulClass αᵐᵒᵖ α
-- Lean.Meta.Closure
Lean.Meta.Closure.Context : Type
-- Init.Data.SInt.Bitwise
Int32.toUInt32_not : ∀ (a : Int32), (~~~a).toUInt32 = ~~~a.toUInt32
-- Mathlib.FieldTheory.Galois.NormalBasis
exists_linearIndependent_algEquiv_apply : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L],
  ∃ x, LinearIndependent K fun σ => σ x
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.genWeightSpaceOf.eq_1 : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : R) (x : L),
  LieModule.genWeightSpaceOf M χ x = { toSubmodule := ((LieModule.toEnd R L M) x).maxGenEigenspace χ, lie_mem := ⋯ }
-- Lean.Meta.Basic
/-- Get the local declaration associated to the given `Expr` in the current local
context. Fails if the given expression is not a fvar or if no such declaration exists.  -/
Lean.Meta.getFVarLocalDecl : Lean.Expr → Lean.MetaM Lean.LocalDecl
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.alter : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        (a : α) →
          (Option (β a) → Option (β a)) → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.MemLp.condExpL2_ae_eq_condExp : ∀ {α : Type u_1} {E : Type u_3} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m m₀ : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → E} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : CompleteSpace E] [inst_4 : InnerProductSpace 𝕜 E] (hm : m ≤ m₀) (hf : MeasureTheory.MemLp f 2 μ)
  [MeasureTheory.IsFiniteMeasure μ],
  ↑↑↑((MeasureTheory.condExpL2 E 𝕜 hm) (MeasureTheory.MemLp.toLp f hf)) =ᵐ[μ] μ[f | m]
-- Std.Internal.Do.Order.Basic
Lean.Order.join_prop_eq_or : ∀ (a b : Prop), Lean.Order.join a b = (a ∨ b)
-- Init.Data.Array.Find
Array.findSome?_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {b : β},
  Array.findSome? f xs = some b ↔ ∃ ys a zs, xs = ys.push a ++ zs ∧ f a = some b ∧ ∀ x ∈ ys, f x = none
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Get the discrimination tree matches from `tree`.  -/
Mathlib.Tactic.ClickSuggestions.getMatches : {α : Type} → Lean.Meta.RefinedDiscrTree α → Lean.Expr → Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult α)
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
/-- Graded version of  `Algebra.TensorProduct.includeRight`, i.e. the inclusion from a graded
`R`-algebra `𝒜` to its base change to `S` and then restricted back to `R`. (The restriction does
not change the actual sets).

In categorical terms, this is the unit of the adjunction `GradedAlgHom.liftEquiv`.  -/
GradedAlgHom.includeRight : {ι : Type u_1} →
  {R : Type u_2} →
    (S : Type u_3) →
      {A : Type u_4} →
        [inst : DecidableEq ι] →
          [inst_1 : AddMonoid ι] →
            [inst_2 : CommSemiring R] →
              [inst_3 : CommSemiring S] →
                [inst_4 : Semiring A] →
                  [inst_5 : Algebra R A] →
                    (𝒜 : ι → Submodule R A) →
                      [inst_6 : GradedAlgebra 𝒜] →
                        [inst_7 : Algebra R S] →
                          𝒜 →ₐᵍ[R] fun x => Submodule.restrictScalars R (Submodule.baseChange S (𝒜 x))
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOp_smul : ∀ {R : Type u_4} {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] {n : ℕ} (m : Fin n → V) [inst_1 : SMul R E]
  [LineDerivSMul R V E E] (r : R) (x : E),
  LineDeriv.iteratedLineDerivOp m (r • x) = r • LineDeriv.iteratedLineDerivOp m x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_sSup : ∀ {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph), (sSup s).edgeSet = ⋃ G' ∈ s, G'.edgeSet
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.instIsAddMonHomWhiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z : C} [inst_3 : CategoryTheory.AddMonObj X]
  [inst_4 : CategoryTheory.AddMonObj Y] [inst_5 : CategoryTheory.AddMonObj Z] {f : Y ⟶ Z}
  [CategoryTheory.IsAddMonHom f], CategoryTheory.IsAddMonHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isNone_minKey?_eq_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.minKey?.isNone = t.isEmpty
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
WfDvdMonoid.of_wfDvdMonoid_associates : ∀ {α : Type u_1} [inst : CommMonoidWithZero α], WfDvdMonoid (Associates α) → WfDvdMonoid α
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.instIsEquivalenceOppositeUnopFunctor : CategoryTheory.RelCat.unopFunctor.IsEquivalence
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regOfFamily_pos : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ},
  NumberField.Units.IsMaxRank u → 0 < NumberField.Units.regOfFamily u
-- Mathlib.Algebra.Group.Defs
npowRec_eq : ∀ {M : Type u_2} [inst : Semigroup M] [inst_1 : One M] (k : ℕ) (m : M), npowRec (k + 1) m = 1 * npowRec' (k + 1) m
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.of_sConvexComb_mem : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X},
  (∀ (w : Convexity.StdSimplex R X), ↑w.weights.support ⊆ s → Convexity.sConvexComb w ∈ s) → Convexity.IsConvexSet R s
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_union_of_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → k ∈ t₁ ∪ t₂
-- Mathlib.Order.UpperLower.Basic
isUpperSet_compl : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsUpperSet sᶜ ↔ IsLowerSet s
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.BohrMollerup.tendsto_logGammaSeq_of_le_one : ∀ {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ (Set.Ioi 0) f →
    (∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y) →
      0 < x → x ≤ 1 → Filter.Tendsto (Real.BohrMollerup.logGammaSeq x) Filter.atTop (nhds (f x - f 1))
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `norm_ne_zero_iff`.  -/
hammingNorm_ne_zero_iff : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] {x : (i : ι) → β i}, hammingNorm x ≠ 0 ↔ x ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inl_comp_pushoutSymmetry_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inl f g))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushoutSymmetry f g).hom) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inr g f)
-- Mathlib.Algebra.GroupWithZero.Defs
isCancelMulZero_iff : ∀ (M₀ : Type u) [inst : Mul M₀] [inst_1 : Zero M₀],
  IsCancelMulZero M₀ ↔ IsLeftCancelMulZero M₀ ∧ IsRightCancelMulZero M₀
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.integrable_tilted_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → ℝ},
  MeasureTheory.Integrable (fun x => Real.exp (f x)) μ →
    ∀ (g : α → E), MeasureTheory.Integrable g (μ.tilted f) ↔ MeasureTheory.Integrable (fun x => Real.exp (f x) • g x) μ
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- Elements of `Δ` lie in the commensurator of the left subgroup.  -/
IsHeckeTriple.mem_commensurator_left : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ : Subgroup G} (H₂ : Subgroup G) [IsHeckeTriple Δ H₁ H₂]
  (g : ↥Δ), ↑g ∈ Subgroup.Commensurable.commensurator H₁
-- Mathlib.Topology.Compactification.OnePoint.Sphere
/-- A homeomorphism from the one-point compactification of a hyperplane in Euclidean space to the
sphere.  -/
onePointHyperplaneHomeoUnitSphere : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [FiniteDimensional ℝ E] → {v : E} → ‖v‖ = 1 → OnePoint ↥(ℝ ∙ v)ᗮ ≃ₜ ↑(Metric.sphere 0 1)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsFilteredSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ),
  CategoryTheory.IsFiltered (Subtype J.PropSet)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.Ω₀`.

---

Notation for the `Ω₀` in an arbitrary choice of a subobject classifier  -/
CategoryTheory.HasClassifier.Ω₀ : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.HasSubobjectClassifier C] → C
-- Mathlib.Data.Setoid.Partition
Setoid.rel_iff_exists_classes : ∀ {α : Type u_1} (r : Setoid α) {x y : α}, r x y ↔ ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
-- Mathlib.Order.RelIso.Basic
/-- For a `β`-relation `r`, a function `f : α → β` induces a relation homomorphism from `r.onFun f`
to `r`.  -/
RelHom.ofOnFun : {α : Type u_1} → {β : Type u_2} → (r : β → β → Prop) → (f : α → β) → Function.onFun r f →r r
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.addGroupWithOne : {R : Type u} → {M : Type v} → [AddGroupWithOne R] → [AddGroup M] → AddGroupWithOne (TrivSqZeroExt R M)
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_zpow' : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a : ℚ},
  ↑a.den ≠ 0 → ∀ (n : ℤ), Lean.Grind.Field.NormNum.ofRat (a ^ n) = Lean.Grind.Field.NormNum.ofRat a ^ n
-- Init.Data.String.Lemmas.Pattern.Find.String
_private.Init.Data.String.Lemmas.Pattern.Find.String.0.String.Slice.contains.match_1.eq_1 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (startPos endPos : s.Pos)
  (h_1 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos))
  (h_2 : (x : String.Slice.Pattern.SearchStep s) → motive x),
  (match String.Slice.Pattern.SearchStep.matched startPos endPos with
    | String.Slice.Pattern.SearchStep.matched startPos endPos => h_1 startPos endPos
    | x => h_2 x) =
    h_1 startPos endPos
-- Init.Control.State
/-- Executes an action from a monad with added state in the underlying monad `m`. Given an initial
state, it returns a value, discarding the final state.
 -/
StateT.run' : {σ : Type u} → {m : Type u → Type v} → [Functor m] → {α : Type u} → StateT σ m α → σ → m α
-- Init.Data.Option.Lemmas
Option.isNone_choice_eq_false : ∀ {α : Type u_1} [Nonempty α], (Option.choice α).isNone = false
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₁_functor : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₁ hF).functor = F
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.CoeExpansionTrace.mk.injEq : ∀ (expandedCoeDecls expandedCoeDecls_1 : List Lean.Name),
  ({ expandedCoeDecls := expandedCoeDecls } = { expandedCoeDecls := expandedCoeDecls_1 }) =
    (expandedCoeDecls = expandedCoeDecls_1)
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
Measurable.measurePreserving : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
  Measurable f → ∀ (μa : MeasureTheory.Measure α), MeasureTheory.MeasurePreserving f μa (MeasureTheory.Measure.map f μa)
-- Mathlib.CategoryTheory.Iso
/-- Reinterpret a morphism `f : X ⟶ Y` with an `IsIso f` instance as `X ≅ Y`.  -/
CategoryTheory.asIso : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.IsIso f] → X ≅ Y
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_inv_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₂ : T₁.obj₂ ≅ T₂.obj₂)
  (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom T₂.mor₁),
  (CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).inv.hom₂ = e₂.inv
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.subtype_hom_toFun : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] (A : Rep.{u_1, u, v} k G) (W : Submodule k ↑A)
  (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) (self : ↥W), (Rep.Hom.hom (A.subtype W le_comap)) self = ↑self
-- Init.Core
BitVec.ofFin.inj : ∀ {w : ℕ} {toFin toFin_1 : Fin (2 ^ w)}, { toFin := toFin } = { toFin := toFin_1 } → toFin = toFin_1
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.step_cons_of_not_LE : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  {it : Std.DTreeMap.Internal.Zipper α β} [inst : Ord α] {upper : α} {h : (compare k upper).isLE = false},
  { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }.step = Std.IterStep.done