mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError.mk.inj : ∀ {srcNat : ℕ} {srcEndPos : String.Pos.Raw} {fmtPos : ℕ} {msg : String} {length : ℕ} {srcStartPos : String.Pos.Raw}
  {srcNat_1 : ℕ} {srcEndPos_1 : String.Pos.Raw} {fmtPos_1 : ℕ} {msg_1 : String} {length_1 : ℕ}
  {srcStartPos_1 : String.Pos.Raw},
  { srcNat := srcNat, srcEndPos := srcEndPos, fmtPos := fmtPos, msg := msg, length := length,
        srcStartPos := srcStartPos } =
      { srcNat := srcNat_1, srcEndPos := srcEndPos_1, fmtPos := fmtPos_1, msg := msg_1, length := length_1,
        srcStartPos := srcStartPos_1 } →
    srcNat = srcNat_1 ∧
      srcEndPos = srcEndPos_1 ∧ fmtPos = fmtPos_1 ∧ msg = msg_1 ∧ length = length_1 ∧ srcStartPos = srcStartPos_1
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.lift.congr_simp : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (self self_1 : F.WellOrderInductionData),
  self = self_1 →
    ∀ (j : J) (hj : Order.IsSuccLimit j) (x x_1 : ↑(⋯.functor.op.comp F).sections),
      x = x_1 → self.lift j hj x = self_1.lift j hj x_1
-- Mathlib.RingTheory.Binomial
Ring.choose_succ_succ : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (r : R) (k : ℕ),
  Ring.choose (r + 1) (k + 1) = Ring.choose r k + Ring.choose r (k + 1)
-- Lean.ResolveName
/-- Resolves the name `n` in the local context.  -/
Lean.resolveLocalName : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] →
            [Lean.AddMessageContext m] → [Lean.MonadLCtx m] → Lean.Name → m (Option (Lean.Expr × List String))
-- Init.Data.Array.Lemmas
Array.foldr_hom : ∀ {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) {g₁ : α → β₁ → β₁} {g₂ : α → β₂ → β₂} {xs : Array α}
  {init : β₁}, (∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) → Array.foldr g₂ (f init) xs = f (Array.foldr g₁ init xs)
-- Init.Data.SInt.Lemmas
ISize.instIsLinearOrder : Std.IsLinearOrder ISize
-- Batteries.Data.Stream
/-- Drop up to `n` values from the stream `s`.  -/
Std.Stream.drop : {σ : Type u_1} → {α : Type u_2} → [Std.Stream σ α] → σ → ℕ → σ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is nonzero, the vectors are not equal.  -/
Orientation.ne_of_oangle_ne_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y ≠ 0 → x ≠ y
-- Lean.Widget.UserWidget
Lean.Widget.ToModule.toModule : {α : Type u} → [self : Lean.Widget.ToModule α] → α → Lean.Widget.Module
-- Mathlib.Algebra.Group.Units.Defs
/-- Additive units have decidable equality
if the base `AddMonoid` has decidable equality.  -/
AddUnits.instDecidableEq : {α : Type u} → [inst : AddMonoid α] → [DecidableEq α] → DecidableEq (AddUnits α)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.coe_range : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S),
  ↑f.range = Set.range ⇑f
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_sumPiEquivProdPi : ∀ {δ : Type u_4} {δ' : Type u_5} (α : δ ⊕ δ' → Type u_8) [inst : (i : δ ⊕ δ') → MeasurableSpace (α i)],
  ⇑(MeasurableEquiv.sumPiEquivProdPi α) = ⇑(Equiv.sumPiEquivProdPi α)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.lift_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : AddCommGroup γ] (f : α → β) (g : β → γ) (x : FreeAbelianGroup α),
  (FreeAbelianGroup.lift (g ∘ f)) x = (FreeAbelianGroup.lift g) ((FreeAbelianGroup.map f) x)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryLE? : {α : Type u} → {β : Type v} → [Ord α] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.isUnit_toLin_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) {M : Matrix n n R},
  IsUnit ((Matrix.toLin v₁ v₁) M) ↔ IsUnit M
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Pro-Coyoneda lemma: morphisms from colimit of coyoneda of diagram `D` to `F` is limit
of `F` evaluated at `D`. This variant is for contravariant diagrams, see
`colimitCoyonedaHomIsoLimit'` for a covariant version.  -/
CategoryTheory.Limits.colimitCoyonedaHomIsoLimitLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (D : CategoryTheory.Functor I Cᵒᵖ) →
          (F : CategoryTheory.Functor C (Type u₂)) →
            [inst_2 : CategoryTheory.Limits.HasColimit (D.comp CategoryTheory.coyoneda)] →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] →
                (CategoryTheory.Limits.colimit (D.comp CategoryTheory.coyoneda) ⟶ F) ≅
                  CategoryTheory.Limits.limit (D.leftOp.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂}))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_eq_getValueCast? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.getEntry? a l = Option.map (fun v => ⟨a, v⟩) (Std.Internal.List.getValueCast? a l)
-- Init.Data.List.Lemmas
List.and_any_distrib_left : ∀ {α : Type u_1} {l : List α} {p : α → Bool} {q : Bool}, (q && l.any p) = l.any fun a => q && p a
-- Mathlib.Data.Matrix.Basic
Matrix.entryAddMonoidHom_toAddHom : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : AddZeroClass α] {i : m} {j : n},
  ↑(Matrix.entryAddMonoidHom α i j) = Matrix.entryAddHom α i j
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.isIso_fromOpcycles : ∀ {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 : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g)) →
    CategoryTheory.IsIso (X.fromOpcycles f g fg h n)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Mathlib.Analysis.LocallyConvex.Separation
geometric_hahn_banach_open_point : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s : Set E} {x : E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], Convex ℝ s → IsOpen s → x ∉ s → ∃ f, ∀ a ∈ s, f a < f x
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.Theory.simpleGraph.eq_1 : FirstOrder.Language.Theory.simpleGraph = {FirstOrder.Language.adj.irreflexive, FirstOrder.Language.adj.symmetric}
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.inv_eqToHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : X = Y),
  CategoryTheory.inv (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.coe_top : ∀ {K : Type u} [inst : DivisionRing K], ↑⊤ = Set.univ
-- Aesop.Tree.Data
Aesop.instInhabitedRappId.default : Aesop.RappId
-- Mathlib.GroupTheory.Congruence.Hom
/-- The homomorphism induced on the quotient of an `AddMonoid` by the kernel
of an `AddMonoid` homomorphism.  -/
AddCon.kerLift : {M : Type u_1} →
  {P : Type u_3} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass P] → (f : M →+ P) → (AddCon.ker f).Quotient →+ P
-- Batteries.Recycling.MonadSatisfying.Basic
/-- If `p` is always true, then every `x` satisfies it.  -/
SatisfiesM.of_true : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} [inst : Functor m] [LawfulFunctor m] {x : m α},
  (∀ (a : α), p a) → SatisfiesM p x
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.IsExtensionBy_trans_right : ∀ {aig : Std.Sat.AIG ℕ} {cnf1 cnf2 cnf3 : Std.Sat.CNF ℕ} {new1 : ℕ} {hnew1 : new1 < aig.decls.size} {new2 : ℕ}
  {hnew2 : new2 < aig.decls.size} (cache1 : Std.Sat.AIG.toCNF.Cache✝ aig cnf1)
  (cache2 : Std.Sat.AIG.toCNF.Cache✝ aig cnf2) (cache3 : Std.Sat.AIG.toCNF.Cache✝ aig cnf3),
  Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache1 cache2 new1 hnew1 →
    Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache2 cache3 new2 hnew2 →
      Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache1 cache3 new2 hnew2
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {n : ℕ}
  (F : CategoryTheory.ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (CategoryTheory.homOfLE ⋯))),
  (CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows W F hF).F = F
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.equivalence_functor : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  ContinuousGeneratedByCat.equivalence.functor = ContinuousGeneratedByCat.fromGeneratedByTopCat
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousWithinAt.const_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ∀ (b : M), ContinuousWithinAt (fun x => b + f x) s x
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inr_zero : ∀ (R : Type u_3) {A : Type u_4} [inst : Zero R] [inst_1 : Zero A], ↑0 = 0
-- Mathlib.Order.KrullDimension
LTSeries.longestOf.congr_simp : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : FiniteDimensionalOrder α], LTSeries.longestOf α = LTSeries.longestOf α
-- Mathlib.Analysis.Convex.Gauge
one_le_gauge_of_notMem : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E},
  StarConvex ℝ 0 s → Absorbs ℝ s {x} → x ∉ s → 1 ≤ gauge s x
-- Mathlib.Order.Disjoint
Disjoint.inf_left' : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α} (c : α), Disjoint a b → Disjoint (c ⊓ a) b
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.insert : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] [inst_2 : TopologicalSpace α] {x : α}
  {s : Set α} {C : ℝ} {g : α → E} {g' : α → F},
  Asymptotics.IsBigOWith C (nhdsWithin x s) g g' →
    ‖g x‖ ≤ C * ‖g' x‖ → Asymptotics.IsBigOWith C (nhdsWithin x (insert x s)) g g'
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
algebraMap_galRestrictHom_apply : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L]
  (σ : L →ₐ[K] L) (x : B), (algebraMap B L) (((galRestrictHom A K L B) σ) x) = σ ((algebraMap B L) x)
-- Mathlib.Topology.Maps.Basic
isClosedMap_iff_comap_nhds_le : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f ↔ ∀ {y : Y}, Filter.comap f (nhds y) ≤ nhdsSet (f ⁻¹' {y})
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∈ t₂ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Init.Data.SInt.Lemmas
Int8.le_maxValue : ∀ (a : Int8), a ≤ Int8.maxValue
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.erase_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R),
  AddMonoidAlgebra.erase m (AddMonoidAlgebra.single m r) = 0
-- Mathlib.Algebra.Polynomial.Identities
/-- A polynomial `f` evaluated at `x + y` can be expressed as
the evaluation of `f` at `x`, plus `y` times the (polynomial) derivative of `f` at `x`,
plus some element `k : R` times `y^2`.
 -/
Polynomial.binomExpansion : {R : Type u} →
  [inst : CommRing R] →
    (f : Polynomial R) →
      (x y : R) →
        { k //
          Polynomial.eval (x + y) f =
            Polynomial.eval x f + Polynomial.eval x (Polynomial.derivative f) * y + k * y ^ 2 }
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- The Bochner integral  -/
MeasureTheory.«term∫_In_,_» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.inter!_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁.inter! m₂).Equiv (m₁.inter! m₃)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_derivative_mul_X_sq : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (p : Polynomial R),
  (⇑Polynomial.derivative)^[n] ((⇑Polynomial.derivative)^[2] p * Polynomial.X ^ 2) =
    (⇑Polynomial.derivative)^[n + 2] p * Polynomial.X ^ 2 +
        (2 * n) • (⇑Polynomial.derivative)^[n + 1] p * Polynomial.X +
      (n * (n - 1)) • (⇑Polynomial.derivative)^[n] p
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y),
  AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f y =
    CategoryTheory.Limits.pullback.snd f (Y.fromSpecResidueField y)
-- Mathlib.Order.Filter.Map
Filter.comap_eval_neBot : ∀ {ι : Type u_6} {α : ι → Type u_7} [∀ (j : ι), Nonempty (α j)] (i : ι) (f : Filter (α i)) [f.NeBot],
  (Filter.comap (Function.eval i) f).NeBot
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- `MonoidAlgebra.single 1` as an `AlgHom`  -/
MonoidAlgebra.singleOneAlgHom : {R : Type u_1} →
  {A : Type u_4} →
    {M : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : Monoid M] → A →ₐ[R] MonoidAlgebra A M
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.val_addUnit : ∀ {M : Type u_6} [inst : AddMonoid M] {x : M} (hx : IsOfFinAddOrder x), ↑hx.addUnit = x
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- If `f` is absolute continuous on `uIcc a b`, then `f'` exists a.e. on `uIcc a b`.  -/
AbsolutelyContinuousOnInterval.ae_differentiableAt : ∀ {f : ℝ → ℝ} {a b : ℝ}, AbsolutelyContinuousOnInterval f a b → ∀ᵐ (x : ℝ), x ∈ Set.uIcc a b → DifferentiableAt ℝ f x
-- Mathlib.RingTheory.LittleWedderburn
/-- We prove that if every subring of `D` is central, then so is `D`.  -/
_private.Mathlib.RingTheory.LittleWedderburn.0.LittleWedderburn.InductionHyp.center_eq_top : ∀ {D : Type u_1} [inst : DivisionRing D] [Finite D], LittleWedderburn.InductionHyp✝ D → Subring.center D = ⊤
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_le_minKey!_erase : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (compare (Std.Internal.List.minKey! l) (Std.Internal.List.minKey! (Std.Internal.List.eraseKey k l))).isLE = true
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
tendsto_pow_div_pow_atTop_zero : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {p q : ℕ}, p < q → Filter.Tendsto (fun x => x ^ p / x ^ q) Filter.atTop (nhds 0)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
_private.Mathlib.RingTheory.Extension.Presentation.Submersive.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_₁₁_det : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_7 : Fintype σ] [inst_8 : Fintype σ'],
  (MvPolynomial.aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det = Q.jacobian
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Internal.Raw₀.union.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  m₁.union m₂ = if (↑m₁).size ≤ (↑m₂).size then ↑(m₂.insertManyIfNew ↑m₁) else ↑(m₁.insertMany ↑m₂)
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F F_1 : TopCat.Presheaf C X),
  F = F_1 →
    ∀ {ι : Type v'} (U U_1 : ι → TopologicalSpace.Opens ↑X),
      U = U_1 →
        TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U =
          TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F_1 U_1
-- Mathlib.Analysis.Normed.Group.Basic
norm_nonneg' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), 0 ≤ ‖a‖
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.leibnizPullback_obj_map : ∀ {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₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) [inst_3 : CategoryTheory.Limits.HasPullbacks C₂]
  (f₁ : (CategoryTheory.Arrow C₁)ᵒᵖ) {X Y : CategoryTheory.Arrow C₃} (sq : X ⟶ Y),
  (G.leibnizPullback.obj f₁).map sq =
    (CategoryTheory.Functor.PullbackObjObj.ofHasPullback G (Opposite.unop f₁).hom X.hom).mapArrowRight
      (CategoryTheory.Functor.PullbackObjObj.ofHasPullback G (Opposite.unop f₁).hom Y.hom) sq
-- Init.MetaTypes
Lean.Meta.TransparencyMode.default.sizeOf_spec : sizeOf Lean.Meta.TransparencyMode.default = 1
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.mem_ae_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s : Set α}, s ∈ MeasureTheory.ae μ ↔ μ sᶜ = 0
-- Mathlib.NumberTheory.LSeries.Deriv
/-- The L-series of `f` is holomorphic on its open half-plane of absolute convergence.  -/
LSeries_analyticOnNhd : ∀ (f : ℕ → ℂ), AnalyticOnNhd ℂ (LSeries f) {s | LSeries.abscissaOfAbsConv f < ↑s.re}
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- The coordinate ring of a component in the `affine_basis_cover`.  -/
AlgebraicGeometry.Scheme.affineBasisCoverRing : (X : AlgebraicGeometry.Scheme) → X.affineBasisCover.I₀ → CommRingCat
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.mono_of_nonDegenerate : ∀ (X : SSet) {n : ℕ} (x : ↑(X.nonDegenerate n)) {m : SimplexCategory} (f : { len := n } ⟶ m)
  (y : X.obj (Opposite.op m)), (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y = ↑x → CategoryTheory.Mono f
-- Aesop.Script.StructureDynamic
_private.Aesop.Script.StructureDynamic.0.Aesop.Script.goalsToMessageData : Lean.Meta.SavedState → Array Lean.MVarId → Lean.MetaM Lean.MessageData
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [ν.HaveLebesgueDecomposition μ],
  μ.AbsolutelyContinuous ν → μ.AbsolutelyContinuous (μ.withDensity (ν.rnDeriv μ))
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedAdd.toExistsAddOfLE : ∀ {α : Type u_1} {inst : Add α} {inst_1 : LE α} [self : CanonicallyOrderedAdd α], ExistsAddOfLE α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst : Inhabited β], k ∉ t₂ → (t₁ ∪ t₂).get! k = t₁.get! k
-- Mathlib.Logic.Function.DependsOn
/-- **Alias** of `Set.dependsOn_domRestrict`. -/
Set.dependsOn_restrict : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι), DependsOn s.domRestrict s
-- Mathlib.Order.CompleteLattice.Defs
isGLB_iff_sInf_eq : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, IsGLB s a ↔ sInf s = a
-- Mathlib.Data.List.ModifyLast
List.modifyLast.go.eq_2 : ∀ {α : Type u_1} (f : α → α) (a : Array α) (x_2 : α), List.modifyLast.go f [x_2] a = a.toListAppend [f x_2]
-- Mathlib.RepresentationTheory.Irreducible
Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] {ρ : Representation k G V} [ρ.IsIrreducible] [FiniteDimensional k V] [IsAlgClosed k],
  Function.Bijective ⇑(algebraMap k (ρ.IntertwiningMap ρ))
-- Mathlib.Order.SupClosed
infClosure_eq_self : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α}, infClosure s = s ↔ InfClosed s
-- Lean.Compiler.LCNF.Basic
/-- Low-level update `Param` function. It does not update the local context.
Consider using `Param.update : Param → Expr → CompilerM Param` if you want the local context
to be updated.
 -/
Lean.Compiler.LCNF.Param.updateCore : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Param pu → Lean.Expr → Lean.Compiler.LCNF.Param pu
-- Mathlib.GroupTheory.OreLocalization.OreSet
OreLocalization.oreNum.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r : R) (s : ↥S),
  OreLocalization.oreNum r s = OreLocalization.OreSet.oreNum r s
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
OnePoint.equivProjectivization_smul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] {g : GL (Fin 2) K} (x : OnePoint K),
  (OnePoint.equivProjectivization K) (g • x) = g • (OnePoint.equivProjectivization K) x
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.toPartOrd_map_apply : ∀ {n m : SimplexCategory} (f : n ⟶ m) (i : Fin (n.len + 1)),
  (CategoryTheory.ConcreteCategory.hom (SimplexCategory.toPartOrd.map f)) { down := i } =
    { down := (CategoryTheory.ConcreteCategory.hom f) i }
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.FunctorCategory.tensorHom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F G F' G' : CategoryTheory.Functor C D} (α : F ⟶ G) (β : F' ⟶ G')
  (X : C),
  (CategoryTheory.Monoidal.FunctorCategory.tensorHom α β).app X =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X)
-- Init.Data.List.Nat.InsertIdx
List.length_insertIdx_le_succ : ∀ {α : Type u} {l : List α} {x : α} {i : ℕ}, (l.insertIdx i x).length ≤ l.length + 1
-- Mathlib.Data.Set.Prod
Set.diagonal_subset_iff : ∀ {α : Type u_1} {s : Set (α × α)}, Set.diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Assumption.left : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊢ₛ R) → P ∧ Q ⊢ₛ R