mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousConstVAdd.toMeasurableConstVAdd : ∀ {M : Type u_7} {α : Type u_8} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α]
  [inst_3 : VAdd M α] [ContinuousConstVAdd M α], MeasurableConstVAdd M α
-- Std.Http.Data.Status
Std.Http.CustomStatus.mk.sizeOf_spec : ∀ (code : UInt16) (phrase : String)
  (validReasonPhrase :
    autoParam (Std.Http.IsValidReasonPhrase phrase) Std.Http.CustomStatus.validReasonPhrase._autoParam)
  (validCode : autoParam (100 ≤ code ∧ code ≤ 999) Std.Http.CustomStatus.validCode._autoParam)
  (validUnknown : autoParam (¬Std.Http.isKnownStatusCode code = true) Std.Http.CustomStatus.validUnknown._autoParam),
  sizeOf
      { code := code, phrase := phrase, validReasonPhrase := validReasonPhrase, validCode := validCode,
        validUnknown := validUnknown } =
    1 + sizeOf code + sizeOf phrase + sizeOf validReasonPhrase + sizeOf validCode
-- Mathlib.Topology.Order.AtTopBotIxx
/-- A family of closed intervals bounded by diverging limits is locally finite.  -/
locallyFinite_Icc_of_tendsto : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {α : Type u_2}
  [inst_3 : LinearOrder α] [LocallyFiniteOrder α] [NoMaxOrder X] [NoMinOrder X] {f g : α → X},
  Filter.Tendsto f Filter.atTop Filter.atTop →
    Filter.Tendsto g Filter.atBot Filter.atBot → LocallyFinite fun n => Set.Icc (f n) (g n)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_mem_neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] {s : Finset α} {a : α}, a ∈ s → -a ∈ -s
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < im z < b}`.
Let `f : ℂ → E` be a function such that

* `f` is differentiable on `U` and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * exp(c * |re z|))` on `U` for some `c < π / (b - a)`;
* `f z = 0` on the boundary of `U`.

Then `f` is equal to zero on the closed strip `{z : ℂ | a ≤ im z ≤ b}`.
 -/
PhragmenLindelof.eq_zero_on_horizontal_strip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f : ℂ → E},
  DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b) →
    (∃ c < Real.pi / (b - a),
        ∃ B,
          f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)] fun z =>
            Real.exp (B * Real.exp (c * |z.re|))) →
      (∀ (z : ℂ), z.im = a → f z = 0) → (∀ (z : ℂ), z.im = b → f z = 0) → Set.EqOn f 0 (Complex.im ⁻¹' Set.Icc a b)
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.sup : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] {f : Filter β} {u v : β → α},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.SparseCasesOnKey.isPrivate : Lean.Meta.SparseCasesOnKey✝ → Bool
-- Mathlib.Order.Filter.Pointwise
Filter.HasBasis.inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {f : Filter α} {ι : Sort u_7} {p : ι → Prop} {s : ι → Set α},
  f.HasBasis p s → f⁻¹.HasBasis p fun i => (s i)⁻¹
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesMap_comp_descOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} {i : ι} [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] {A : C} (k : L.X i ⟶ A) (j : ι) (hj : c.prev i = j)
  (hk : CategoryTheory.CategoryStruct.comp (L.d j i) k = 0) (φ : K ⟶ L),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (L.descOpcycles k j hj hk) =
    K.descOpcycles (CategoryTheory.CategoryStruct.comp (φ.f i) k) j hj ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_univ_of_zero_mem : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α} [inst_2 : Fintype α],
  0 ∈ s → s + Finset.univ = Finset.univ
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
mem_balancedHull_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s : Set E} {x : E},
  x ∈ balancedHull 𝕜 s ↔ ∃ r, ‖r‖ ≤ 1 ∧ x ∈ r • s
-- Init.Data.List.Lemmas
List.foldrRecOn_cons : ∀ {β : Type u_1} {α : Type u_2} {b : β} {x : α} {l : List α} {motive : β → Sort u_3} {op : α → β → β} (hb : motive b)
  (hl : (b : β) → motive b → (a : α) → a ∈ x :: l → motive (op a b)),
  List.foldrRecOn (x :: l) op hb hl = hl (List.foldr op b l) (List.foldrRecOn l op hb fun b c a m => hl b c a ⋯) x ⋯
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_right : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b c : R}, a ≤ b → 0 ≤ c → a * c ≤ b * c
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
IsValuativeTopology.hasBasis_nhds : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [IsValuativeTopology R]
  (x : R), (nhds x).HasBasis (fun x => True) fun γ => {z | (ValuativeRel.valuation R) (z - x) < ↑γ}
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x y : α},
  x ≠ 0 →
    y ≠ 0 →
      (Associated x y ↔ UniqueFactorizationMonoid.normalizedFactors x = UniqueFactorizationMonoid.normalizedFactors y)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.inter_sdiff_distrib_right`. -/
Set.inter_diff_distrib_right : ∀ {α : Type u_1} (s t u : Set α), s \ t ∩ u = (s ∩ u) \ (t ∩ u)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_map_image : ∀ {α β : Type u} {f : α → β} (M : Matroid α) (hf : Set.InjOn f M.E) (X : Set α),
  autoParam (X ⊆ M.E) Matroid.cRk_map_image._auto_1 → (M.map f hf).cRk (f '' X) = M.cRk X
-- Std.Internal.Parsec.ByteArray
/-- Parse an octal digit `0-7` as a `Char`.
 -/
Std.Internal.Parsec.ByteArray.octDigit : Std.Internal.Parsec.ByteArray.Parser Char
-- Mathlib.LinearAlgebra.Determinant
LinearEquiv.det_trans : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f g : M ≃ₗ[R] M),
  LinearEquiv.det (f ≪≫ₗ g) = LinearEquiv.det g * LinearEquiv.det f
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap.congr_point : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (x x' : ↑↑X) (h : x = x'),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x) (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x')
-- Mathlib.Data.Seq.Computation
/-- Recursion principle for computations, compare with `List.recOn`.  -/
Computation.recOn : {α : Type u} →
  {motive : Computation α → Sort v} →
    (s : Computation α) → ((a : α) → motive (Computation.pure a)) → ((s : Computation α) → motive s.think) → motive s
-- Mathlib.NumberTheory.Divisors
Nat.filter_dvd_eq_properDivisors : ∀ {n : ℕ}, n ≠ 0 → {d ∈ Finset.range n | d ∣ n} = n.properDivisors
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inl_comp_pushoutSymmetry_hom_assoc : ∀ {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) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q (CategoryTheory.Limits.pushout g f) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inl f g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushoutSymmetry f g).hom) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inr g f)) h
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.Stained.name : Lean.Name → Mathlib.Linter.Flexible.Stained✝
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero₂_of_isFirstQuadrant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Y : CategoryTheory.Abelian.SpectralObject C EInt) [Y.IsFirstQuadrant] (i j : EInt) (hij : i ≤ j) (n : ℤ),
  WithBotTop.coe n < i →
    CategoryTheory.Limits.IsZero ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- If the inner product of two vectors is equal to the product of their norms, then the two vectors
are multiples of each other. One form of the equality case for Cauchy-Schwarz.
Compare `inner_eq_norm_mul_iff`, which takes the stronger hypothesis `⟪x, y⟫ = ‖x‖ * ‖y‖`.  -/
norm_inner_eq_norm_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, x ≠ 0 → y ≠ 0 → (‖inner 𝕜 x y‖ = ‖x‖ * ‖y‖ ↔ ∃ r, r ≠ 0 ∧ y = r • x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_right : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) (adj₂ : F ⊣₂ G) (X₁ : CategoryTheory.Arrow C₁)
  [inst_3 : CategoryTheory.Limits.HasPullbacks C₂] [inst_4 : CategoryTheory.Limits.HasPushouts C₃]
  (X₂ : CategoryTheory.Arrow C₂),
  ((CategoryTheory.Functor.LeibnizAdjunction.adj F G adj₂ X₁).unit.app X₂).right =
    CategoryTheory.Limits.pullback.lift
      (adj₂.homEquiv (CategoryTheory.Limits.pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
      (adj₂.homEquiv (CategoryTheory.CategoryStruct.id ((F.obj X₁.right).obj X₂.right))) ⋯
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
SimpleGraph.ConnectedComponent.Represents.ncard_eq : ∀ {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V},
  SimpleGraph.ConnectedComponent.Represents s C → s.ncard = C.ncard
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqPoly.beq_spec_1 : ∀ (a b : ℤ), (Int.Internal.Linear.Poly.num a == Int.Internal.Linear.Poly.num b) = (a == b)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_nhds_of_boundaryless : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] [I.Boundaryless] (x : M),
  Filter.map (↑(extChartAt I x)) (nhds x) = nhds (↑(extChartAt I x) x)
-- Lean.Elab.AssertExists
Lean.Elab.Command.instHashableAssertExists.hash : Lean.Elab.Command.AssertExists → UInt64
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.brecOn : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)}
  {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1 → Prop} {a : ℕ}
  {a_1 : Std.HashMap α ℕ} (t : Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1),
  (∀ (a : ℕ) (a_2 : Std.HashMap α ℕ) (t : Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_2),
      Std.Sat.AIG.RelabelNat.State.Inv2.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R), f.Separable = IsCoprime f (Polynomial.derivative f)
-- Mathlib.FieldTheory.KummerExtension
autAdjoinRootXPowSubCEquiv.eq_1 : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [inst_1 : NeZero n],
  autAdjoinRootXPowSubCEquiv hζ H =
    { toFun := (↑(autAdjoinRootXPowSubC n a)).toFun, invFun := AdjoinRootXPowSubCEquivToRootsOfUnity hζ H,
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Init.Data.UInt.Basic
instOrOpUInt32 : OrOp UInt32
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.IsCompletelyMetrizableSpace.mk : ∀ {X : Type u_3} [t : TopologicalSpace X],
  (∃ m, PseudoMetricSpace.toUniformSpace.toTopologicalSpace = t ∧ CompleteSpace X) →
    TopologicalSpace.IsCompletelyMetrizableSpace X
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_apply_one : ∀ {R : Type u_1} [inst : Semiring R] (k : ℕ), 0 < k → (Polynomial.hasseDeriv k) 1 = 0
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeffLinearEquiv_apply : ∀ (R : Type u_2) {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Type u_5)
  [inst_3 : CommSemiring S] [inst_4 : Module S M] (a : PolynomialModule R M),
  (PolynomialModule.coeffLinearEquiv R S) a = a.coeff
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km : α}, t.minKey? = some km → km ∈ t
-- Mathlib.Data.Finset.Defs
Finset.coe_inj : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, ↑s₁ = ↑s₂ ↔ s₁ = s₂
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
/-- **The Law of Quadratic Reciprocity**: if `p` and `q` are distinct odd primes, then
`(q / p) * (p / q) = (-1)^((p-1)(q-1)/4)`.  -/
legendreSym.quadratic_reciprocity : ∀ {p q : ℕ} [inst : Fact (Nat.Prime p)] [inst_1 : Fact (Nat.Prime q)],
  p ≠ 2 → q ≠ 2 → p ≠ q → legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.op_vadd_finset_vadd_eq_vadd_vadd_finset : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq β] [inst_1 : DecidableEq γ] [inst_2 : VAdd αᵃᵒᵖ β]
  [inst_3 : VAdd β γ] [inst_4 : VAdd α γ] (a : α) (s : Finset β) (t : Finset γ),
  (∀ (a : α) (b : β) (c : γ), (AddOpposite.op a +ᵥ b) +ᵥ c = b +ᵥ a +ᵥ c) → (AddOpposite.op a +ᵥ s) +ᵥ t = s +ᵥ a +ᵥ t
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.IsHadamard.mul_conjTranspose : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  {A : Matrix n n R}, A.IsHadamard → A * A.conjTranspose = ↑(Fintype.card n) • 1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_succ_succ : ∀ {m n : ℤ}, ((m + 1)...=n + 1).toList = List.map (fun x => x + 1) (m...=n).toList
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.range_arctan : Set.range Real.arctan = Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.inverse.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {A : Type u_4} [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] {B₁ : Type u_6}
  [inst_3 : AddMonoid B₁] [inst_4 : DistribMulAction M B₁] (f : A →+[M] B₁) (g : B₁ → A)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f),
  f.inverse g h₁ h₂ = { toFun := g, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.zipWith_apply : ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β i)]
  [inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i → β i)
  (hf : ∀ (i : ι), f i 0 0 = 0) (g₁ : Π₀ (i : ι), β₁ i) (g₂ : Π₀ (i : ι), β₂ i) (i : ι),
  (DFinsupp.zipWith f hf g₁ g₂) i = f i (g₁ i) (g₂ i)
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- **Alias** of the forward direction of `hasDerivAt_iff_tendsto_slope`. -/
HasDerivAt.tendsto_slope : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x → Filter.Tendsto (slope f x) (nhdsWithin x {x}ᶜ) (nhds f')
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof → Sort u} (t : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof)
  (F_1 : (t : Lean.Meta.Grind.Arith.CommRing.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_2 t (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.brecOn.go t F_1 F_2).2
-- Mathlib.GroupTheory.Transfer
AddMonoidHom.transfer_def : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {A : Type u_2} [inst_1 : AddCommGroup A] (ϕ : ↥H →+ A)
  (T : H.LeftTransversal) [inst_2 : H.FiniteIndex] (g : G),
  ϕ.transfer g = AddSubgroup.leftTransversals.diff ϕ T (g +ᵥ T)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k)
-- Mathlib.Topology.Order.WithTop
WithTop.continuousOn_untopD : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] (d : ι),
  ContinuousOn (WithTop.untopD d) {a | a ≠ ⊤}
-- Mathlib.RingTheory.Valuation.Integral
Valuation.Integers.mem_of_integral : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R], v.Integers O → ∀ {x : R}, IsIntegral O x → x ∈ v.integer
-- Mathlib.Data.ENNReal.Inv
/-- An order isomorphism between the extended nonnegative real numbers and the unit interval.  -/
ENNReal.orderIsoUnitIntervalBirational : ENNReal ≃o ↑(Set.Icc 0 1)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isIso_iCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology], S.g = 0 → CategoryTheory.IsIso S.iCycles
-- Mathlib.Analysis.Meromorphic.Order
/-- `meromorphicOrderAt` is invariant under translation.  -/
meromorphicOrderAt_comp_add_const_eq_meromorphicOrderAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E},
  meromorphicOrderAt (f ∘ fun x => x + c) x = meromorphicOrderAt f (x + c)
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.nextn_add_one : ∀ {n : ℕ} {s : String.Slice} {p : s.Pos}, p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.mk.congr_simp : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (carrier carrier_1 : Ideal A)
  (e_carrier : carrier = carrier_1) (isSubideal : carrier ≤ I)
  (dpow_mem : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier, hI.dpow n j ∈ carrier),
  { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem } =
    { carrier := carrier_1, isSubideal := ⋯, dpow_mem := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- Given a simplicial set `X`, `n : ℕ` and `x : X _⦋0⦌`, this is the type
of morphisms `Δ[n] ⟶ X` which are constant with value `x` on the boundary.  -/
SSet.PtSimplex : (X : SSet) → ℕ → X.obj (Opposite.op { len := 0 }) → Type u
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.map_alternatingFaceMapComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  (AlgebraicTopology.alternatingFaceMapComplex C).comp (F.mapHomologicalComplex (ComplexShape.down ℕ)) =
    ((CategoryTheory.SimplicialObject.whiskering C D).obj F).comp (AlgebraicTopology.alternatingFaceMapComplex D)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_of_isOpen_eq_iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜},
  IsOpen s → Set.EqOn (iteratedDerivWithin n f s) (deriv^[n] f) s
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.coe_currySumEquiv_symm : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)], ⇑MultilinearMap.currySumEquiv.symm = MultilinearMap.uncurrySum
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- A multiseries `ms` is `Sorted` when the exponents at each of its levels are sorted.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted : {basis : Tactic.ComputeAsymptotics.Basis} → Tactic.ComputeAsymptotics.MultiseriesExpansion basis → Prop
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_erase_eq_of_not_compare_minKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α},
  t.erase k ≠ ∅ → ¬cmp k (t.minKeyD fallback) = Ordering.eq → (t.erase k).minKeyD fallback = t.minKeyD fallback
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMon_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X Y : CategoryTheory.AddMon C} (f : X ⟶ Y),
  (F.mapAddMon.map f).hom = F.map f.hom
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.GaloisCategory C}
  {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  {x y : A.Hom B}, x = y ↔ x.val = y.val
-- Init.Control.StateCps
StateCpsT.runK_bind_pure : ∀ {α σ : Type u} {m : Type u → Type v} {β γ : Type u} (a : α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ),
  (pure a >>= f).runK s k = (f a).runK s k
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {X x x_1 : F.Grothendieck}
  (f : X.Hom x) (g : x.Hom x_1),
  (CategoryTheory.CategoryStruct.comp f g).fiber =
    CategoryTheory.CategoryStruct.comp ((F.mapComp f.base.toLoc g.base.toLoc).hom.toNatTrans.app X.fiber)
      (CategoryTheory.CategoryStruct.comp ((F.map g.base.toLoc).toFunctor.map f.fiber) g.fiber)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.map_comp : ∀ (p : ENNReal) {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} (f : V' → V'') (g : V → V'),
  WithLp.map p (f ∘ g) = WithLp.map p f ∘ WithLp.map p g
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsPureImpPureForall : ∀ {φ ψ : Prop} (σs : List (Type u_1)), Std.Do.SPred.Tactic.IsPure spred(⌜φ⌝ → ⌜ψ⌝) (φ → ψ)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
Equiv.pointReflection_midpoint_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), (Equiv.pointReflection (midpoint R x y)) y = x
-- Mathlib.Algebra.Group.Action.Faithful
instFaithfulVAddOfSubsingleton : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α] [Subsingleton M], FaithfulVAdd M α