mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.loopless_iff_forall_isNonloop : ∀ {α : Type u_1} {M : Matroid α}, M.Loopless ↔ ∀ e ∈ M.E, M.IsNonloop e
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- If `s` is a transcendence basis and `j` is algebraic over `s ∪ {i} \ {j}`,
then `s ∪ {i} \ {j}` is also a transcendence basis.  -/
IsTranscendenceBasis.of_isAlgebraic_adjoin_insert_sdiff : ∀ {ι : Type u} {R : Type u_1} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [FaithfulSMul R S] [NoZeroDivisors S] (s : Set ι) (i j : ι) (v : ι → S),
  j ∈ insert i s →
    (IsTranscendenceBasis R fun x => v ↑x) →
      IsAlgebraic (↥(Algebra.adjoin R (v '' (insert i s \ {j})))) (v j) → IsTranscendenceBasis R fun x => v ↑x
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.listToPath.eq_def : ∀ {α : Type u_1} (x : List α),
  Quiver.SingleObj.listToPath x =
    match x with
    | [] => Quiver.Path.nil
    | a :: l => (Quiver.SingleObj.listToPath l).cons a
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.inv_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Inv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant], μ.inv = μ
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_non_aestronglyMeasurable : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → G}, ¬MeasureTheory.AEStronglyMeasurable f μ → ∫ (a : α), f a ∂μ = 0
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integrable_continuousLinearMap_prod' : ∀ {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {mE : MeasurableSpace E} [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.Measure E}
  [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure F} [MeasureTheory.IsProbabilityMeasure ν]
  {L : E × F →L[ℝ] G},
  MeasureTheory.Integrable (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F)) μ →
    MeasureTheory.Integrable (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F)) ν → MeasureTheory.Integrable (⇑L) (μ.prod ν)
-- Mathlib.Algebra.Group.Defs
/-- Auxiliary tail-recursive implementation for `nsmulBinRec`.  -/
nsmulBinRec.go : {M : Type u_2} → [Add M] → ℕ → M → M → M
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.id.eq_1 : ∀ (M : Type u_1) [inst : Monoid M] {A : Type u_4} [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A],
  MulDistribMulActionHom.id M = { toMulActionHom := MulActionHom.id M, map_one' := ⋯, map_mul' := ⋯ }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_rco_eq_fallback : ∀ {m n i fallback : ℕ}, n ≤ i + m → (m...n).toArray.getD i fallback = fallback
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.isSymmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsPositive → T.IsSymmetric
-- Lean.Elab.Command.Scope
Lean.Elab.Command.Scope.mk.injEq : ∀ (header : String) (opts : Lean.Options) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl)
  (levelNames : List Lean.Name) (varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder))
  (varUIds : Array Lean.Name) (includedVars omittedVars : List Lean.Name) (isNoncomputable isPublic isMeta : Bool)
  (attrs : List (Lean.TSyntax `Lean.Parser.Term.attrInstance)) (header_1 : String) (opts_1 : Lean.Options)
  (currNamespace_1 : Lean.Name) (openDecls_1 : List Lean.OpenDecl) (levelNames_1 : List Lean.Name)
  (varDecls_1 : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (varUIds_1 : Array Lean.Name)
  (includedVars_1 omittedVars_1 : List Lean.Name) (isNoncomputable_1 isPublic_1 isMeta_1 : Bool)
  (attrs_1 : List (Lean.TSyntax `Lean.Parser.Term.attrInstance)),
  ({ header := header, opts := opts, currNamespace := currNamespace, openDecls := openDecls, levelNames := levelNames,
        varDecls := varDecls, varUIds := varUIds, includedVars := includedVars, omittedVars := omittedVars,
        isNoncomputable := isNoncomputable, isPublic := isPublic, isMeta := isMeta, attrs := attrs } =
      { header := header_1, opts := opts_1, currNamespace := currNamespace_1, openDecls := openDecls_1,
        levelNames := levelNames_1, varDecls := varDecls_1, varUIds := varUIds_1, includedVars := includedVars_1,
        omittedVars := omittedVars_1, isNoncomputable := isNoncomputable_1, isPublic := isPublic_1, isMeta := isMeta_1,
        attrs := attrs_1 }) =
    (header = header_1 ∧
      opts = opts_1 ∧
        currNamespace = currNamespace_1 ∧
          openDecls = openDecls_1 ∧
            levelNames = levelNames_1 ∧
              varDecls = varDecls_1 ∧
                varUIds = varUIds_1 ∧
                  includedVars = includedVars_1 ∧
                    omittedVars = omittedVars_1 ∧
                      isNoncomputable = isNoncomputable_1 ∧ isPublic = isPublic_1 ∧ isMeta = isMeta_1 ∧ attrs = attrs_1)
-- Mathlib.Tactic.Ring.PNat
Mathlib.Tactic.Ring.instCSLiftValPNatNatOfNatHAdd : ∀ {n : ℕ}, Mathlib.Tactic.Ring.CSLiftVal (OfNat.ofNat (n + 1)) (n + 1)
-- Batteries.Data.String.Lemmas
String.Pos.Raw.valid_zero : ∀ {s : String}, String.Pos.Raw.Valid s 0
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.range_path : ∀ (x y : Circle), Set.range ⇑(x.path y) = ⇑Circle.exp '' Set.Icc (↑x).arg (x.angleDiff y + (↑x).arg)
-- Mathlib.Algebra.Ring.Ext
Ring.toNonAssocRing_injective : ∀ {R : Type u}, Function.Injective (@Ring.toNonAssocRing R)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Construct a natural isomorphism between functors out of the walking parallel pair from
its components.  -/
CategoryTheory.Limits.parallelPair.ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} →
      (zero :
          F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero) →
        (one :
            F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one) →
          autoParam
              (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) one.hom =
                CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
              CategoryTheory.Limits.parallelPair.ext._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) one.hom =
                  CategoryTheory.CategoryStruct.comp zero.hom
                    (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
                CategoryTheory.Limits.parallelPair.ext._auto_3 →
              (F ≅ G)
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_sub_of_right_invariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1 - p.2) (μ.prod ν) μ
-- Mathlib.Analysis.Convex.Side
/-- The points `x` and `y` are weakly on opposite sides of `s`.  -/
AffineSubspace.WOppSide : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : PartialOrder R] →
          [IsStrictOrderedRing R] →
            [inst_3 : AddCommGroup V] →
              [inst_4 : Module R V] → [inst_5 : AddTorsor V P] → AffineSubspace R P → P → P → Prop
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.whiskerRight_app_snd : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  {F₁ F₁' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (F₂ : CategoryTheory.Functor J C) (j : J),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.whiskerRight f F₂).app j)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (F₁'.obj j) (F₂.obj j)) =
    CategoryTheory.SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mulPow : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.isPullback_map : ∀ {n : Type u} {S T : AlgebraicGeometry.Scheme} (f : S ⟶ T),
  CategoryTheory.IsPullback (AlgebraicGeometry.AffineSpace.map n f) (AlgebraicGeometry.AffineSpace n S ↘ S)
    (AlgebraicGeometry.AffineSpace n T ↘ T) f
-- Mathlib.RingTheory.Nilpotent.Basic
Commute.isNilpotent_mul_right_iff : ∀ {R : Type u_1} {x y : R} [inst : Semiring R],
  Commute x y → y ∈ nonZeroDivisorsRight R → (IsNilpotent (x * y) ↔ IsNilpotent x)
-- Mathlib.Topology.UniformSpace.Defs
/-- This core description of a uniform space is outside of the type class hierarchy. It is useful
for constructions of uniform spaces, when the topology is derived from the uniform space.  -/
UniformSpace.Core : Type u → Type u
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The residue of `completedHurwitzZetaEven a s` at `s = 0` is equal to `-1` if `a = 0`, and `0`
otherwise.  -/
HurwitzZeta.completedHurwitzZetaEven_residue_zero : ∀ (a : UnitAddCircle),
  Filter.Tendsto (fun s => s * HurwitzZeta.completedHurwitzZetaEven a s) (nhdsWithin 0 {0}ᶜ)
    (nhds (if a = 0 then -1 else 0))
-- Mathlib.Data.Seq.Defs
/-- Folds a sequence using `f`, producing a sequence of intermediate values, i.e.
`[init, f init s.head, f (f init s.head) s.tail.head, ...]`.  -/
Stream'.Seq.fold : {α : Type u} → {β : Type v} → Stream'.Seq α → β → (β → α → β) → Stream'.Seq β
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    ∀ {h' : Std.Internal.List.containsKey k l = true} {h'' : Std.Internal.List.containsKey k' l = true},
      Std.Internal.List.getKey k l h' = Std.Internal.List.getKey k' l h''
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial_le_pow_add : ∀ (n k : ℕ), (n + 1).ascFactorial k ≤ (n + k) ^ k
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.copy_nil : ∀ {V : Type u} {G : SimpleGraph V} {u u' : V} (hu : u = u'), SimpleGraph.Walk.nil.copy hu hu = SimpleGraph.Walk.nil
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.map_slope : ∀ {F : Type u} {K : Type v} [inst : Field F] [inst_1 : Field K] {W : WeierstrassCurve.Affine F} [inst_2 : DecidableEq F]
  [inst_3 : DecidableEq K] (f : F →+* K) (x₁ x₂ y₁ y₂ : F),
  (W.map f).slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.intCastFn? : Lean.Meta.Grind.Arith.CommRing.Ring → Option Lean.Expr
-- Init.Data.BitVec.Lemmas
/-- Prove equality of bitvectors in terms of integer operations.  -/
BitVec.eq_of_toInt_eq : ∀ {n : ℕ} {x y : BitVec n}, x.toInt = y.toInt → x = y
-- Mathlib.Data.Set.Functor
Set.mem_image_val_of_mem : ∀ {α : Type u} {β : Set α} {γ : Set ↑β} {a : α} (ha : a ∈ β), ⟨a, ha⟩ ∈ γ → a ∈ Subtype.val '' γ
-- Std.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.Equiv.toListRev_eq : ∀ {α₁ β α₂ : Type u_1} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Finite α₁ Id]
  [Std.Iterators.Finite α₂ Id] {ita : Std.Iter β} {itb : Std.Iter β}, ita.Equiv itb → ita.toListRev = itb.toListRev
-- Init.Data.Rat.Lemmas
Rat.lt_of_le_of_ne : ∀ {a b : ℚ}, a ≤ b → a ≠ b → a < b
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
HasDerivAt.log : ∀ {f : ℝ → ℝ} {x f' : ℝ}, HasDerivAt f f' x → f x ≠ 0 → HasDerivAt (fun y => Real.log (f y)) (f' / f x) x
-- Mathlib.Data.Int.ModEq
Int.ModEq.add_right_cancel' : ∀ {n a b : ℤ} (c : ℤ), a + c ≡ b + c [ZMOD n] → a ≡ b [ZMOD n]
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context.mk : Bool → Bool → Bool → Bool → Lean.SubExpr → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- the cokernel condition for `π`  -/
CategoryTheory.ShortComplex.LeftHomologyData.wπ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (self : S.LeftHomologyData) {Z : C} (h : self.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯))
      (CategoryTheory.CategoryStruct.comp self.π h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.DelayedTheoremInstance.check : Lean.Meta.Grind.DelayedTheoremInstance → Lean.Meta.Grind.GoalM Unit
-- Init.Data.UInt.Lemmas
UInt32.sub_def : ∀ (a b : UInt32), a - b = { toBitVec := a.toBitVec - b.toBitVec }
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_sdiff_comm`. -/
Set.diff_diff_comm : ∀ {α : Type u_1} {s t u : Set α}, (s \ t) \ u = (s \ u) \ t
-- Mathlib.Data.Complex.Basic
Complex.normSq_I : Complex.normSq Complex.I = 1
-- Mathlib.Topology.Algebra.GroupWithZero
map_mul_right_nhds_one₀ : ∀ {G₀ : Type u_3} [inst : TopologicalSpace G₀] [inst_1 : GroupWithZero G₀] [SeparatelyContinuousMul G₀] {a : G₀},
  a ≠ 0 → Filter.map (fun x => x * a) (nhds 1) = nhds a
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainRingEquiv.eq_1 : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (e : M ≃+ N),
  AddMonoidAlgebra.mapDomainRingEquiv R e =
    RingEquiv.ofRingHom (AddMonoidAlgebra.mapDomainRingHom R ↑e) (AddMonoidAlgebra.mapDomainRingHom R ↑e.symm) ⋯ ⋯
-- Mathlib.Analysis.SumIntegralComparisons
AntitoneOn.sum_le_integral : ∀ {x₀ : ℝ} {a : ℕ} {f : ℝ → ℝ},
  AntitoneOn f (Set.Icc x₀ (x₀ + ↑a)) → ∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
-- Mathlib.Topology.DenseEmbedding
DenseRange.induction_on₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {e : α → β} {p : β → β → Prop},
  DenseRange e → IsClosed {q | p q.1 q.2} → (∀ (a₁ a₂ : α), p (e a₁) (e a₂)) → ∀ (b₁ b₂ : β), p b₁ b₂
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.HasZeroObject.instEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C] {X : C}
  (f : X ⟶ 0), CategoryTheory.Epi f
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.cases.inj : ∀ {eager eager_1 : Bool},
  Lean.Meta.Grind.AttrKind.cases eager = Lean.Meta.Grind.AttrKind.cases eager_1 → eager = eager_1
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y} (φ : W₁.MapFactorizationData W₂ f),
  CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv φ =
    CategoryTheory.MorphismProperty.MapFactorizationData.op W₁ W₂ φ
-- Lean.Parser.Term
Lean.Parser.Term.matchExpr.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.mk : ℕ →
  Lean.Expr →
    Lean.Level →
      Lean.Expr →
        Lean.Expr →
          Option (Lean.Expr × ℕ) →
            Option Lean.Expr →
              Option Lean.Expr →
                Option Lean.Expr →
                  Option Lean.Expr →
                    Option Lean.Expr → Option Lean.Expr → Option Lean.Expr → Option Lean.Expr → Lean.Meta.Sym.Arith.Ring
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- A rewrite lemma for `padicValRat p (q⁻¹)`.  -/
padicValRat.inv : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ), padicValRat p q⁻¹ = -padicValRat p q
-- Mathlib.Data.Finset.Sups
Finset.compls_sups : ∀ {α : Type u_2} [inst : BooleanAlgebra α] [inst_1 : DecidableEq α] (s t : Finset α),
  (s ⊻ t).compls = s.compls ⊼ t.compls
-- Mathlib.Topology.Irreducible
isPreirreducible_iff_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsPreirreducible (closure s) ↔ IsPreirreducible s
-- Mathlib.Data.PEquiv
PEquiv.ofSet_eq_refl : ∀ {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s], PEquiv.ofSet s = PEquiv.refl α ↔ s = Set.univ
-- Mathlib.Data.ENNReal.Operations
ENNReal.eq_top_of_pow : ∀ {a : ENNReal} (n : ℕ), a ^ n = ⊤ → a = ⊤
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t₁ t₂ : Finset α}, s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.ext_iff : ∀ {R : Type u} {S : Type v} {ι : Type w} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} {inst_3 : CommRing R'}
  {inst_4 : CommRing S'} {inst_5 : Algebra R' S'} {P' : Algebra.Generators R' S' ι'} {inst_6 : Algebra S S'}
  {x y : P.Hom P'}, x = y ↔ x.val = y.val
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfold_loop_succ : ∀ {n j : ℕ} {α : (i : ℕ) → autoParam (i ≤ n + 1) Nat.dfold_loop_succ._auto_5✝ → Type u}
  (f : (i : ℕ) → (h : i < n + 1) → α i ⋯ → α (i + 1) ⋯) (a : α (n + 1 - (j + 1)) ⋯) (w : j ≤ n),
  Nat.dfold.loop✝ (n + 1) f (j + 1) ⋯ a = f n ⋯ (Nat.dfold.loop✝ n (fun i h => f i ⋯) j w (Nat.dfoldCast✝ α ⋯ a))
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.opEquiv_counitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (CategoryTheory.ShortComplex.opEquiv C).counitIso =
    CategoryTheory.Iso.refl ((CategoryTheory.ShortComplex.unopFunctor C).comp (CategoryTheory.ShortComplex.opFunctor C))
-- Mathlib.Logic.Equiv.Defs
Equiv.equiv_subsingleton_cod : ∀ {α : Sort u} {β : Sort v} [Subsingleton β], Subsingleton (α ≃ β)
-- Mathlib.Algebra.Quandle
UnitalShelf.one_act : ∀ {α : Type u} [self : UnitalShelf α] (a : α), Shelf.act 1 a = a
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
InnerProductGeometry.continuousAt_angle : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x : V × V},
  x.1 ≠ 0 → x.2 ≠ 0 → ContinuousAt (fun y => InnerProductGeometry.angle y.1 y.2) x
-- Std.Data.Internal.List.Associative
Std.Internal.List.replaceEntry_cons_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'},
  (k' == k) = false →
    Std.Internal.List.replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: Std.Internal.List.replaceEntry k v l
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_shiftLeftZeroExtend : ∀ {m i : ℕ} (x : BitVec m) (n : ℕ), (x.shiftLeftZeroExtend n).getLsbD i = (!decide (i < n) && x.getLsbD (i - n))
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.IsRegularOfDegree.bot : ∀ {V : Type u_1} [inst : Fintype V], ⊥.IsRegularOfDegree 0
-- Mathlib.CategoryTheory.Limits.Cones
/-- The image of a cone in C under a functor G : C ⥤ D is a cone in D.  -/
CategoryTheory.Functor.mapCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (H : CategoryTheory.Functor C D) →
              {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cone F → CategoryTheory.Limits.Cone (F.comp H)
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.AddGrpCat.Hom.mk.injEq : ∀ {A B : AddGrpCat} (hom' hom'_1 : ↑A →+ ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
CategoryTheory.Limits.PreservesLimitsOfSize.overPost : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, max u₁ v₁, max u₂ v₂} (CategoryTheory.Over.post F)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons_ne_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl ≠
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.mk.inj : ∀ {n : ℕ} {parts : Multiset ℕ} {parts_pos : ∀ {i : ℕ}, i ∈ parts → 0 < i} {parts_sum : parts.sum = n}
  {parts_1 : Multiset ℕ} {parts_pos_1 : ∀ {i : ℕ}, i ∈ parts_1 → 0 < i} {parts_sum_1 : parts_1.sum = n},
  { parts := parts, parts_pos := parts_pos, parts_sum := parts_sum } =
      { parts := parts_1, parts_pos := parts_pos_1, parts_sum := parts_sum_1 } →
    parts = parts_1
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositions_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C}
  [Q.IsStableUnderTransfiniteComposition],
  CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u} P ≤ Q ↔ P ≤ Q
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabLetMVar : Lean.Elab.Term.TermElab
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.finiteDimensional_left : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  [FiniteDimensional K L], FiniteDimensional K ↥F
-- Mathlib.CategoryTheory.UnivLE
EssSurj.ofUnivLE : ∀ [UnivLE.{max u v, v}], CategoryTheory.uliftFunctor.{u, v}.EssSurj
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.Functor.mapDifferentialObject_map_f : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (D : Type u')
  [inst_4 : CategoryTheory.Category.{v', u'} D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_6 : CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D)
  (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1))
  (hF : ∀ (c c' : C), F.map 0 = 0) {X Y : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y),
  ((CategoryTheory.Functor.mapDifferentialObject D F η hF).map f).f = F.map f.f
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- An induction principle for additive closure membership, for
predicates with two arguments.  -/
AddSubgroup.closure_induction₂ : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G}
  {p : (x y : G) → x ∈ AddSubgroup.closure k → y ∈ AddSubgroup.closure k → Prop},
  (∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯) →
    (∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p 0 x ⋯ hx) →
      (∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p x 0 hx ⋯) →
        (∀ (x y z : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k)
            (hz : z ∈ AddSubgroup.closure k), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
          (∀ (y z x : G) (hy : y ∈ AddSubgroup.closure k) (hz : z ∈ AddSubgroup.closure k)
              (hx : x ∈ AddSubgroup.closure k), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) →
            (∀ (x y : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k),
                p x y hx hy → p (-x) y ⋯ hy) →
              (∀ (x y : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k),
                  p x y hx hy → p x (-y) hx ⋯) →
                ∀ {x y : G} (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k), p x y hx hy