mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isLE_shift : ∀ {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 a n' : ℤ),
  autoParam (a + n' = n) CategoryTheory.Triangulated.TStructure.isLE_shift._auto_1 →
    ∀ [t.IsLE X n], t.IsLE ((CategoryTheory.shiftFunctor C a).obj X) n'
-- Mathlib.Algebra.Star.Unitary
Units.unitary_eq : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R], unitary Rˣ = Submonoid.comap (Units.coeHom R) (unitary R)
-- Init.Data.BitVec.Lemmas
BitVec.umod_one : ∀ {w : ℕ} {x : BitVec w}, x % 1#w = 0#w
-- Mathlib.Algebra.Star.Pointwise
Set.star_preimage : ∀ {α : Type u_1} {s : Set α} [inst : Star α], star ⁻¹' s = star s
-- Mathlib.Data.List.Basic
List.foldl_concat : ∀ {α : Type u} {β : Type v} (f : β → α → β) (b : β) (x : α) (xs : List α),
  List.foldl f b (xs ++ [x]) = f (List.foldl f b xs) x
-- Mathlib.MeasureTheory.Covering.DensityTheorem
/-- A version of **Lebesgue differentiation theorem** for a sequence of closed balls whose
centers are not required to be fixed.  -/
IsUnifLocDoublingMeasure.ae_tendsto_average : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {E : Type u_2} [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℝ E] [CompleteSpace E] {f : α → E},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ (K : ℝ),
      ∀ᵐ (x : α) ∂μ,
        ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
          Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) →
            (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) →
              Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), f y ∂μ) l (nhds (f x))
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.instIsArtinianSchemeSpecOfIsArtinianRingCarrier : ∀ {R : CommRingCat} [IsArtinianRing ↑R], AlgebraicGeometry.IsArtinianScheme (AlgebraicGeometry.Spec R)
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_sdiff_eq_sdiff_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, u ⊆ s → s \ (t \ u) = s \ t ∪ u
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
PUnit.instMeasurableSpace : MeasurableSpace PUnit.{u_1 + 1}
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_g : ∀ {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.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_3),
  (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g =
    CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.natAddLEFunctor_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n k l : ℕ} (h : k + l ≤ n)
  (F : CategoryTheory.ComposableArrows C n) (X : Fin (l + 1)),
  ((CategoryTheory.ComposableArrows.natAddLEFunctor h).obj F).obj X = F.obj ((Fin.natAddLEFunctor h).obj X)
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
CommGrpCat.binaryProductLimitCone_cone_pt : ∀ (G H : CommGrpCat), (G.binaryProductLimitCone H).cone.pt = CommGrpCat.of (↑G × ↑H)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.grind.debug : Lean.Option Bool
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.RightLift.IsKan.fac : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {t : CategoryTheory.Bicategory.RightLift f g} (H : t.IsKan) (s : CategoryTheory.Bicategory.RightLift f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (H.desc s) f) t.counit = s.counit
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntry.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β)
  (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l l_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_2 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l_1 = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r))
                          h),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l l_1@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r), h_3 =>
      h_2 size k v l l_1 size_1 k_1 v_1 l_2 r h h_3) =
    h_1 size k v l x
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.μ_inv_natural_right : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X Y₁).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map g)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))
      (CategoryTheory.Localization.Monoidal.μ L W ε X Y₂).inv
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] {E : Type u₃}
  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] [inst_7 : CategoryTheory.CartesianMonoidalCategory E]
  [inst_8 : CategoryTheory.BraidedCategory E] {F : CategoryTheory.Functor C D} [inst_9 : F.Braided]
  {G : CategoryTheory.Functor D E} [inst_10 : G.Braided] (X : CategoryTheory.CommGrp C),
  (CategoryTheory.Functor.mapCommGrpCompIso.inv.app X).hom.hom.hom =
    CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : Cᵒᵖ} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z}, CategoryTheory.IsPushout g.unop f.unop snd.unop fst.unop ↔ CategoryTheory.IsPullback fst snd f g
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPi_aux.map_smul : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] (p : (i : ι) → Submodule R (Ms i)) (r : R)
  (x : ((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p),
  Submodule.quotientPi_aux.toFun p (r • x) = (RingHom.id R) r • Submodule.quotientPi_aux.toFun p x
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.index.congr_simp : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v v_1 : VitaliFamily μ} (e_v : v = v_1) {f f_1 : X → Set (Set X)} (e_f : f = f_1) {s s_1 : Set X} (e_s : s = s_1)
  (h : v.FineSubfamilyOn f s) (a a_1 : X × Set X), a = a_1 → h.index a = ⋯.index a_1
-- Mathlib.Tactic.Translate.Core
/-- The argument used to determine whether this constant should be translated.  -/
Mathlib.Tactic.Translate.Config.relevantArg? : Mathlib.Tactic.Translate.Config → Option Mathlib.Tactic.Translate.RelevantArg
-- Mathlib.Algebra.Ring.Shrink
Shrink.instNonUnitalNonAssocRing : {α : Type u_1} → [inst : Small.{v, u_1} α] → [NonUnitalNonAssocRing α] → NonUnitalNonAssocRing (Shrink.{v, u_1} α)
-- Mathlib.FieldTheory.PrimitiveElement
Field.isAlgebraic_of_finite_intermediateField : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [Finite (IntermediateField F E)], Algebra.IsAlgebraic F E
-- Mathlib.RingTheory.Morita.Matrix
/-- Auxiliary isomorphism showing that compose two functors gives `id` on objects.  -/
fromModuleCatToModuleCatLinearEquiv : (R : Type u) →
  {ι : Type v} →
    [inst : Ring R] →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] →
          (M : Type u_1) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → (i : ι) → ↥(MatrixModCat.toModuleCatObj R (ι → M) i) ≃ₗ[R] M
-- Mathlib.Algebra.BigOperators.ModEq
Int.sum_modEq_single : ∀ {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Finset α} {a : α},
  (a ∉ s → f a ≡ 0 [ZMOD n]) → (∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]) → ∑ x ∈ s, f x ≡ f a [ZMOD n]
-- Mathlib.Algebra.Homology.Opposite
/-- Auxiliary definition for `unopEquivalence`.  -/
HomologicalComplex.unopUnitIso : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          CategoryTheory.Functor.id (HomologicalComplex Vᵒᵖ c)ᵒᵖ ≅
            (HomologicalComplex.unopFunctor V c).comp (HomologicalComplex.unopInverse V c)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.inv_smul_mem_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {s : Finset β} {a : α} {b : β}, a ≠ 0 → (a⁻¹ • b ∈ s ↔ b ∈ a • s)
-- Mathlib.Analysis.Normed.Group.Constructions
norm_le_pi_norm : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i)
  (i : ι), ‖f i‖ ≤ ‖f‖
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the signs of two oriented angles between nonzero vectors are equal, the oriented angles are
equal if and only if the unoriented angles are equal.  -/
Orientation.angle_eq_iff_oangle_eq_of_sign_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {w x y z : V},
  w ≠ 0 →
    x ≠ 0 →
      y ≠ 0 →
        z ≠ 0 →
          (o.oangle w x).sign = (o.oangle y z).sign →
            (InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z)
-- Mathlib.Order.Filter.Basic
Filter.le_generate_iff : ∀ {α : Type u} {s : Set (Set α)} {f : Filter α}, f ≤ Filter.generate s ↔ s ⊆ f.sets
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.tendsto_iff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {l₁ : Filter α} {l₂ : Filter β} (L₁ : l₁.Realizer) (L₂ : l₂.Realizer),
  Filter.Tendsto f l₁ l₂ ↔ ∀ (b : L₂.σ), ∃ a, ∀ x ∈ L₁.F.f a, f x ∈ L₂.F.f b
-- Lean.Meta.Constructions.CasesOn
Lean.mkCasesOnImp : Lean.Kernel.Environment → Lean.Name → Except Lean.Kernel.Exception Lean.Declaration
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.toList_insert_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp], t.WF → ∀ {k : α}, (t.insert k).toList.Perm (if k ∈ t then t.toList else k :: t.toList)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The center is commutative and associative.  -/
NonUnitalSubsemiring.center.instNonUnitalCommSemiring : (R : Type u) → [inst : NonUnitalNonAssocSemiring R] → NonUnitalCommSemiring ↥(NonUnitalSubsemiring.center R)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.EMatchTheoremKind.toAttribute : Lean.Meta.Grind.EMatchTheoremKind → Bool → String
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.sInf_mem : ∀ {α : Type u_2} [inst : CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {s : Set α}, s.Finite → s ⊆ ↑L → sInf s ∈ L
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.RightHomologyData.exact_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [S.HasHomology] (h : S.RightHomologyData),
  S.Exact ↔ CategoryTheory.Limits.IsZero h.H
-- Mathlib.Algebra.GCDMonoid.Basic
exists_associated_pow_of_mul_eq_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c : α},
  IsUnit (gcd a b) → ∀ {k : ℕ}, a * b = c ^ k → ∃ d, Associated (d ^ k) a
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_eq_measureReal_of_null_sdiff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  s ⊆ t →
    μ.real (t \ s) = 0 →
      autoParam (μ (t \ s) ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_of_null_sdiff._auto_1 → μ.real s = μ.real t
-- Lean.Language.Basic
Lean.Language.instTypeNameSnapshotTree : TypeName Lean.Language.SnapshotTree
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.esymm.eq_1 : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] (n : ℕ),
  MvPolynomial.esymm σ R n = ∑ t ∈ Finset.powersetCard n Finset.univ, ∏ i ∈ t, MvPolynomial.X i
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coe_coe : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj), ↑e.toOpenPartialHomeomorph = ↑e
-- Mathlib.Data.Set.Insert
Set.preimage_fst_singleton_eq_range : ∀ {α : Type u_3} {β : Type u_4} {a : α}, Prod.fst ⁻¹' {a} = Set.range fun x => (a, x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_add_le_of_nonneg_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b c : α}, a + b ≤ c → 0 ≤ a → b ≤ c
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Std.Do.PredTrans.pushExcept.match_1.splitter : {α ε : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.Dynamics.Ergodic.RadonNikodym
/-- The singular part of a finite invariant measure of a self-map
with respect to a σ-finite invariant measure is an invariant measure.  -/
MeasureTheory.MeasurePreserving.singularPart : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.SigmaFinite ν] {f : X → X},
  MeasureTheory.MeasurePreserving f μ μ →
    MeasureTheory.MeasurePreserving f ν ν → MeasureTheory.MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν)
-- Lean.Data.Lsp.Extra
Lean.Lsp.DependencyBuildMode.noConfusionType : Sort v✝ → Lean.Lsp.DependencyBuildMode → Lean.Lsp.DependencyBuildMode → Sort v✝
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A), ↑S.toNonUnitalSubalgebra = ↑S
-- Mathlib.Data.W.Basic
WType.depth_lt_depth_mk : ∀ {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → Fintype (β a)] (a : α) (f : β a → WType β) (i : β a),
  (f i).depth < (WType.mk a f).depth
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Finsupp.iConvexComb_apply : ∀ {I : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  {ι : Type u_3} {X : Type u_4} [inst_3 : Zero X] [inst_4 : Convexity.ConvexSpace R X] (w : Convexity.StdSimplex R I)
  (f : I → ι →₀ X) (i : ι), (Convexity.iConvexComb w f) i = Convexity.iConvexComb w fun j => (f j) i
-- Init.Grind.AC
Lean.Grind.AC.norm_ac : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} {x : Std.Commutative ctx.op}
  (e : Lean.Grind.AC.Expr) (s : Lean.Grind.AC.Seq),
  e.toSeq.sort.beq' s = true → Lean.Grind.AC.Expr.denote ctx e = Lean.Grind.AC.Seq.denote ctx s
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Reinterpret an ordered monoid isomorphism as an order isomorphism.  -/
OrderMonoidIso.toOrderIso : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Mul α] → [inst_3 : Mul β] → (α ≃*o β) → α ≃o β
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- Implicit function `ψ` defined by `f (x, ψ x) = f u`.  -/
ContDiffAt.implicitFunction : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {E₁ : Type u_2} →
      [inst_1 : NormedAddCommGroup E₁] →
        [inst_2 : NormedSpace 𝕜 E₁] →
          [CompleteSpace E₁] →
            {E₂ : Type u_3} →
              [inst_4 : NormedAddCommGroup E₂] →
                [inst_5 : NormedSpace 𝕜 E₂] →
                  [CompleteSpace E₂] →
                    {F : Type u_4} →
                      [inst_7 : NormedAddCommGroup F] →
                        [inst_8 : NormedSpace 𝕜 F] →
                          [CompleteSpace F] →
                            {u : E₁ × E₂} →
                              {f : E₁ × E₂ → F} →
                                {n : WithTop ℕ∞} →
                                  ContDiffAt 𝕜 n f u →
                                    n ≠ 0 → (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible → E₁ → E₂
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.ofExtend_hom : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} {f g : K ⟶ L} {e : c.Embedding c'}
  [inst_3 : e.IsRelIff] (h : Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e)) (i j : ι),
  h.ofExtend.hom i j =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e ⋯).inv
      (CategoryTheory.CategoryStruct.comp (h.hom (e.f i) (e.f j)) (L.extendXIso e ⋯).hom)
-- Mathlib.FieldTheory.KummerPolynomial
root_X_pow_sub_C_ne_zero' : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K}, 0 < n → a ≠ 0 → AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ≠ 0
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.ofBoolListBE.match_1.eq_2 : ∀ (motive : List Bool → Sort u_1) (b : Bool) (bs : List Bool) (h_1 : Unit → motive [])
  (h_2 : (b : Bool) → (bs : List Bool) → motive (b :: bs)),
  (match b :: bs with
    | [] => h_1 ()
    | b :: bs => h_2 b bs) =
    h_2 b bs
-- Mathlib.Data.Fin.Embedding
/-- `Fin.castSucc` as an `Embedding`, `castSuccEmb i` embeds `i : Fin n` in `Fin (n+1)`.  -/
Fin.castSuccEmb : {n : ℕ} → Fin n ↪ Fin (n + 1)
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- `includeLeftSubRight R S` vanishes at `algebraMap R S r`.  -/
Algebra.TensorProduct.includeLeftSubRight_algebraMap_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S] (r : R),
  (Algebra.TensorProduct.includeLeftSubRight R S) ((algebraMap R S) r) = 0
-- Mathlib.Data.Nat.ModEq
Nat.mod_lcm : ∀ {m n a b : ℕ}, a ≡ b [MOD n] → a ≡ b [MOD m] → a ≡ b [MOD n.lcm m]
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsSymm.add : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : R →+* R}
  {B C : M →ₛₗ[I] M →ₗ[R] R}, B.IsSymm → C.IsSymm → (B + C).IsSymm
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_monomial : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) {a : R}, a ≠ 0 → ((Polynomial.monomial n) a).support = {n}
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} {f : σ → τ},
  Function.Injective f → (((MvPolynomial.rename f) φ).IsHomogeneous n ↔ φ.IsHomogeneous n)
-- Mathlib.Geometry.Euclidean.Incenter
/-- An excenter of a triangle is either the incenter or the excenter opposite a vertex.  -/
Affine.Triangle.excenter_eq_incenter_or_excenter_singleton : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) (signs : Finset (Fin 3)),
  Affine.Simplex.excenter t signs = Affine.Simplex.incenter t ∨
    ∃ i, Affine.Simplex.excenter t signs = Affine.Simplex.excenter t {i}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.lipschitzWith_sin : LipschitzWith 1 Real.sin
-- Mathlib.Algebra.BigOperators.Finprod
MonoidHom.map_finprod_Prop : ∀ {M : Type u_2} {N : Type u_3} [inst : CommMonoid M] [inst_1 : CommMonoid N] {p : Prop} (f : M →* N) (g : p → M),
  f (∏ᶠ (x : p), g x) = ∏ᶠ (x : p), f (g x)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.nerve_hom_ext : ∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.Category.{u, u} C]
  {F G : X ⟶ (SSet.truncation 2).obj (CategoryTheory.nerve C)},
  SSet.OneTruncation₂.map F = SSet.OneTruncation₂.map G → F = G
-- Aesop.Builder.Basic
Aesop.instInhabitedRuleBuilderInput.default : Aesop.RuleBuilderInput
-- Mathlib.Analysis.Calculus.SmoothSeries
deriv_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [inst_4 : NormedSpace 𝕜 F] {g : α → 𝕜 → F} {y₀ : 𝕜},
  Summable u →
    (∀ (n : α), Differentiable 𝕜 (g n)) →
      (∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n) →
        (Summable fun n => g n y₀) → (deriv fun y => ∑' (n : α), g n y) = fun y => ∑' (n : α), deriv (g n) y
-- Mathlib.Order.Booleanisation
Booleanisation.LT.lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α},
  a < b → (Booleanisation.lift a).LT (Booleanisation.lift b)
-- Init.Data.Float.Float32
/-- Converts a floating-point number to a word-sized unsigned integer.

If the given `Float32` is non-negative, truncates the value to a positive integer, rounding down and
clamping to the range of `USize`. Returns `0` if the `Float32` is negative or `NaN`, and returns the
largest `USize` value (i.e. `USize.size - 1`) if the float is larger than it.

This function has a logical model in terms of `Float32.Model`.
 -/
Float32.toUSize : Float32 → USize