mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.MeanInequalities
/-- Hölder's inequality for functions `α → ℝ≥0∞`. The integral of the product of two functions
is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
exponents.  -/
ENNReal.lintegral_mul_le_Lp_mul_Lq : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {p q : ℝ},
  p.HolderConjugate q →
    ∀ {f g : α → ENNReal},
      AEMeasurable f μ →
        AEMeasurable g μ →
          ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.code.takeBackticksFn : ℕ → Lean.Parser.ParserFn
-- Init.Data.Order.Ord
Std.TransCmp.gt_of_eq_of_gt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.eq → cmp b c = Ordering.gt → cmp a c = Ordering.gt
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_of_le_neg_one : ∀ {x : ℝ}, x ≤ -1 → Real.arccos x = Real.pi
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.toFun_eq_coe : ∀ {R : Type u_1} [inst : NonAssocRing R] (p : MulRingSeminorm R), ⇑p.toAddGroupSeminorm = ⇑p
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.smul_eq : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {β : Type u_6} [inst : PartialOrder Γ]
  [inst_1 : PartialOrder Γ'] [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid R] [inst_4 : SMulWithZero R V]
  [inst_5 : VAdd Γ Γ'] [inst_6 : IsOrderedCancelVAdd Γ Γ'] {x : HahnSeries Γ R} {t : HahnSeries.SummableFamily Γ' V β},
  x • t = HahnSeries.SummableFamily.Equiv (Equiv.punitProd β) ((HahnSeries.SummableFamily.const Unit x).smul t)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.tendsto_nhds : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : Filter β} {u : β → α} {a : α},
  Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, dist (u x) a < ε
-- Mathlib.CategoryTheory.Localization.Prod
/-- Auxiliary definition for `prodLift`.  -/
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {E : Type u₅} →
              [inst_2 : CategoryTheory.Category.{v₅, u₅} E] →
                (F : CategoryTheory.Functor (C₁ × C₂) E) →
                  [W₂.ContainsIdentities] →
                    (W₁.prod W₂).IsInvertedBy F → CategoryTheory.Functor W₁.Localization (CategoryTheory.Functor C₂ E)
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dHomologyData_left_K : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7),
  (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).left.K =
    X.E f₂₃ f₄ f₅ n₁ n₂ n₃ ⋯ ⋯
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.Hom.ext_iff : ∀ {k : Type u} {G : Type v} {inst : TopologicalSpace k} {inst_1 : Ring k} {inst_2 : Monoid G} {A : TopRep k G}
  {B : TopRep k G} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Init.Data.Vector.Lemmas
Vector.toArray_swapIfInBounds : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ}, (xs.swapIfInBounds i j).toArray = xs.toArray.swapIfInBounds i j
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrLeftₗ_symm_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6} (R : Type u_7)
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid Z] [inst_4 : Module R Z] (e : X ≃ₜ Y) (a : LocallyConstant Y Z)
  (a_1 : X), ((LocallyConstant.congrLeftₗ R e).symm a) a_1 = a (e a_1)
-- Mathlib.Data.Finset.NoncommProd
/-- Fold of a `s : Multiset α` with an associative `op : α → α → α`, given a proofs that `op`
is commutative on all elements `x ∈ s`.  -/
Multiset.noncommFold : {α : Type u_3} →
  (op : α → α → α) →
    [assoc : Std.Associative op] → (s : Multiset α) → ({x | x ∈ s}.Pairwise fun x y => op x y = op y x) → α → α
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
/-- The zero locus of a set of sections over a compact open of a scheme is `X` if and only if
`s` is contained in the nilradical of `Γ(X, U)`.  -/
AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical : ∀ {X : AlgebraicGeometry.Scheme} [CompactSpace ↥X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))),
  X.zeroLocus s = Set.univ ↔ s ⊆ ↑(nilradical ↑(X.presheaf.obj (Opposite.op ⊤)))
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.id_hcomp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G H : CategoryTheory.Functor D E} (α : G ⟶ H), CategoryTheory.CategoryStruct.id F ◫ α = F.whiskerLeft α
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- Version of `tsum_eq_add_tsum_ite` for `AddCommMonoid` rather than `AddCommGroup`.
Requires a different convergence assumption involving `Function.update`.  -/
Summable.tsum_eq_add_tsum_ite' : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  [T2Space α] [ContinuousAdd α] [inst_4 : DecidableEq β] [L.LeAtTop] [L.NeBot] {f : β → α} (b : β),
  Summable (Function.update f b 0) L → ∑'[L] (x : β), f x = f b + ∑'[L] (x : β), if x = b then 0 else f x
-- Mathlib.Data.Finset.Basic
Finset.filter_inter_distrib : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] (s t : Finset α),
  Finset.filter p (s ∩ t) = Finset.filter p s ∩ Finset.filter p t
-- Lean.Elab.SyntheticMVars
/-- Auxiliary type for `synthesizeSyntheticMVars`. It specifies
whether pending synthetic metavariables can be postponed or not.
 -/
Lean.Elab.Term.PostponeBehavior : Type
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurePreserving_id : ∀ {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  (g : β →ₘ[ν] γ), g.compMeasurePreserving id ⋯ = g
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
/-- The equivalence from coherent sheaves on `C` to coherent sheaves on `D`, given a fully faithful
functor `F : C ⥤ D` to a precoherent category, which preserves and reflects effective epimorphic
families, and satisfies `F.EffectivelyEnough`.
 -/
CategoryTheory.coherentTopology.equivalence : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.PreservesFiniteEffectiveEpiFamilies] →
            [inst_3 : F.ReflectsFiniteEffectiveEpiFamilies] →
              [inst_4 : F.Full] →
                [inst_5 : F.Faithful] →
                  [inst_6 : CategoryTheory.Precoherent D] →
                    [inst_7 : F.EffectivelyEnough] →
                      (A : Type u₃) →
                        [inst_8 : CategoryTheory.Category.{v₃, u₃} A] →
                          [∀ (X : Dᵒᵖ),
                                CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X F.op) A] →
                            CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A ≌
                              CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A
-- Batteries.Tactic.Lint.Frontend
/-- Traces via `IO.println` if `inIO` is `true`, and via `trace[...]` otherwise. It seems that
`trace` messages in a running `CoreM` are not propagated through to `IO` in the current setup. We
use `IO.println` directly instead of running `printTraces` at the end of our `CoreM` action so that
trace messages are printed to stdout immediately, and are not lost if any part of the action hangs.

This declaration is `macro_inline`, so it should have the same thunky behavior as `trace[...]`.  -/
Batteries.Tactic.Lint.traceLintCore : String → Bool → Lean.CoreM Unit
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.toPoly'.go.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_2 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_3 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b))
  (h_5 : (k : ℤ) → (a : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k a))
  (h_6 : (a : Int.Internal.Linear.Expr) → (k : ℤ) → motive (a.mulR k))
  (h_7 : (a : Int.Internal.Linear.Expr) → motive a.neg),
  (match Int.Internal.Linear.Expr.num k with
    | Int.Internal.Linear.Expr.num k => h_1 k
    | Int.Internal.Linear.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Int.Internal.Linear.Expr.mulL k a => h_5 k a
    | a.mulR k => h_6 a k
    | a.neg => h_7 a) =
    h_1 k
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.zero.eq_1 : Turing.ToPartrec.Code.zero = Turing.ToPartrec.Code.zero'.cons Turing.ToPartrec.Code.nil
-- Lean.Meta.Iterator
/-- Find the first value in the iterator while resetting state or call `failure`
if empty.
 -/
Lean.Meta.Iterator.head : {α : Type} → Lean.Meta.Iterator α → Lean.MetaM α
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R],
  RootPairing.EmbeddedG2.allRoots P =
    List.map (⇑(Fintype.linearCombination ℤ ![RootPairing.EmbeddedG2.shortRoot P, RootPairing.EmbeddedG2.longRoot P]))
      RootPairing.EmbeddedG2.allCoeffs
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- If c is a cycle, a ∈ c.support and c is a cycle of f, then `c = f.cycleOf a`  -/
Equiv.Perm.cycle_is_cycleOf : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f c : Equiv.Perm α} {a : α},
  a ∈ c.support → c ∈ f.cycleFactorsFinset → c = f.cycleOf a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} {obj : (X : Cᵒᵖ) → Submodule ↑(R.obj X) ↑(M.obj X)}
  {map : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj X ≤ Submodule.comap (M.restrictₛₗ f) (obj Y)}
  {obj_1 : (X : Cᵒᵖ) → Submodule ↑(R.obj X) ↑(M.obj X)}
  {map_1 : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj_1 X ≤ Submodule.comap (M.restrictₛₗ f) (obj_1 Y)},
  { obj := obj, map := map } = { obj := obj_1, map := map_1 } → obj = obj_1
-- Init.Data.SInt.Basic
Int32.toBitVec.inj : ∀ {x y : Int32}, x.toBitVec = y.toBitVec → x = y
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeAPFree_pi : ∀ {ι : Type u_4} {α : ι → Type u_5} [inst : (i : ι) → AddMonoid (α i)] {s : (i : ι) → Set (α i)},
  (∀ (i : ι), ThreeAPFree (s i)) → ThreeAPFree (Set.univ.pi s)
-- Mathlib.Data.TypeVec
/-- cases distinction for (n+1)-length type vector  -/
TypeVec.casesCons : (n : ℕ) →
  {β : TypeVec.{u_2} (n + 1) → Sort u_1} →
    ((t : Type u_2) → (v : TypeVec.{u_2} n) → β (v ::: t)) → (v : TypeVec.{u_2} (n + 1)) → β v
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.norm_integral_le_norm : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] (μ : MeasureTheory.Measure X) {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [OpensMeasurableSpace X] [SecondCountableTopology E] [inst_5 : MeasurableSpace E]
  [BorelSpace E] [inst_7 : NormedSpace ℝ E] [MeasureTheory.IsProbabilityMeasure μ] (f : BoundedContinuousFunction X E),
  ‖∫ (x : X), f x ∂μ‖ ≤ ‖f‖
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.instDecidableRelAdjAddCayleyOfFintypeOfDecidableEqOfDecidablePredMemSet : {M : Type u_1} →
  (s : Set M) →
    [inst : Add M] →
      [Fintype M] → [DecidableEq M] → [DecidablePred fun x => x ∈ s] → DecidableRel (SimpleGraph.addCayley s).Adj
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.join_ret : ∀ {α : Type u} (s : Stream'.WSeq α), (Stream'.WSeq.ret s).join ~ʷ s
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piCongrRight_apply : ∀ {ι : Type u_7} {Y₁ : ι → Type u_8} {Y₂ : ι → Type u_9} [inst : (i : ι) → TopologicalSpace (Y₁ i)]
  [inst_1 : (i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) (a : (i : ι) → Y₁ i) (i : ι),
  (Homeomorph.piCongrRight F) a i = (F i) (a i)
-- Mathlib.Combinatorics.SetFamily.Intersecting
/-- A family `𝒜` of finite subsets of `α` is `L`-intersecting if the intersection size of every pair of
distinct members of `𝒜` belongs to `L ⊆ ℕ`.

That is, for all `s, t ∈ 𝒜` with `s ≠ t`, we have `|(s ∩ t)| ∈ L`.
 -/
Set.IsIntersectingOf : {α : Type u_1} → [DecidableEq α] → Set ℕ → Set (Finset α) → Prop
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.isOpen_preimage : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (A : Set (Quotient S.toSetoid)),
  IsOpen (S.proj ⁻¹' A)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_mul_monomial : ∀ {R : Type u_1} {n : ℕ} [inst : Semiring R] {a b : R} [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.C a * (SkewPolynomial.monomial n) b = (SkewPolynomial.monomial n) (a * b)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_le_size_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, m.size ≤ (m.insertIfNew k v).size
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instGCommRing : (Γ : Subgroup (GL (Fin 2) ℝ)) → [Γ.HasDetPlusMinusOne] → DirectSum.GCommRing (ModularForm Γ)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.Hom.eq_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (a : C),
  CategoryTheory.WithTerminal.star.Hom (CategoryTheory.WithTerminal.of a) = PEmpty.{v + 1}
-- Mathlib.Condensed.Discrete.Module
LightCondensed.discrete.congr_simp : ∀ (C : Type w) [inst : CategoryTheory.Category.{u, w} C]
  [inst_1 : CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C],
  LightCondensed.discrete C = LightCondensed.discrete C
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length.eq_1 : ∀ {α : Type u_1} (a : FreeAddMonoid α), a.length = (FreeAddMonoid.toList a).length
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_eq : ∀ {a b c : Ordinal.{u_4}}, b * c ≤ a → a < b * (c + 1) → a / b = c
-- Mathlib.Topology.Compactness.Lindelof
/-- A filter `l` with the countable intersection property is disjoint with the neighborhood
filter of a Lindelöf set if and only if it is disjoint with the neighborhood filter of each point
of this set.  -/
IsLindelof.disjoint_nhdsSet_right : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {l : Filter X} [CountableInterFilter l],
  IsLindelof s → (Disjoint l (nhdsSet s) ↔ ∀ x ∈ s, Disjoint l (nhds x))
-- Mathlib.Analysis.Matrix.Normed
Matrix.norm_def : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A‖ = ‖fun i j => A i j‖
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- **Alias** of `CompHausLike.LocallyConstant.functor_map_hom_app`. -/
CompHausLike.LocallyConstant.functor_map_hom : ∀ (P : TopCat → Prop) [inst : CompHausLike.HasExplicitFiniteCoproducts P] [inst_1 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  {X Y : Type (max u w)} (f : X ⟶ Y) (x : (CompHausLike P)ᵒᵖ),
  ((CompHausLike.LocallyConstant.functor P hs).map f).hom.app x =
    TypeCat.ofHom fun t => LocallyConstant.map (⇑(CategoryTheory.ConcreteCategory.hom f)) t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constMinEntryD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {fallback : α × β}, t₁.Equiv t₂ → Std.DTreeMap.Const.minEntryD t₁ fallback = Std.DTreeMap.Const.minEntryD t₂ fallback
-- Init.Data.Vector.Lemmas
Vector.getElem_swap_left : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (hi : i < n) (hj : j < n), (xs.swap i j hi hj)[i] = xs[j]
-- Mathlib.Order.Hom.Bounded
BotHom.instOrderBot : {α : Type u_2} → {β : Type u_3} → [inst : Bot α] → [inst_1 : LE β] → [inst_2 : OrderBot β] → OrderBot (BotHom α β)
-- Mathlib.Order.Interval.Set.Basic
/-- If `a ≤ b`, then `(-∞, a) ⊆ (-∞, b)`. In preorders, this is just an implication. If you need
the equivalence in linear orders, use `Iio_subset_Iio_iff`.  -/
Set.Iio_subset_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → Set.Iio a ⊆ Set.Iio b
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.asyncConstsMap : Lean.Environment → Lean.VisibilityMap✝ Lean.AsyncConsts✝
-- Lean.Meta.Match.CaseValues
Lean.Meta.CaseValuesSubgoal.mk.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (newHs : Array Lean.FVarId) (subst : Lean.Meta.FVarSubst),
  sizeOf { mvarId := mvarId, newHs := newHs, subst := subst } = 1 + sizeOf mvarId + sizeOf newHs + sizeOf subst
-- Mathlib.Order.ModularLattice
/-- An upper modular lattice, aka semimodular lattice, is a lattice where `a ⊔ b` covers `a` and `b`
if either `a` or `b` covers `a ⊓ b`.  -/
IsUpperModularLattice : (α : Type u_2) → [Lattice α] → Prop
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instPreadditive : (R : Type u) → [inst : Ring R] → [inst_1 : TopologicalSpace R] → CategoryTheory.Preadditive (TopModuleCat R)
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.val_apply : ∀ {X : TopCat} {x : ↑X} {U V : TopologicalSpace.OpenNhds x} (f : U ⟶ V) (y : ↥↑U), ↑(f y) = ↑y
-- Mathlib.Data.Finset.Prod
Finset.map_swap_product : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β),
  Finset.map { toFun := Prod.swap, inj' := ⋯ } (t ×ˢ s) = s ×ˢ t
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_push : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {a : α} {f : (i : ℕ) → α → i < n + 1 → β},
  (xs.push a).mapFinIdx f = (xs.mapFinIdx fun i a h => f i a ⋯).push (f n a ⋯)
-- Mathlib.Order.Hom.Bounded
TopHom.inf_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : SemilatticeInf β] [inst_2 : OrderTop β] (f g : TopHom α β)
  (a : α), (f ⊓ g) a = f a ⊓ g a
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a monoid inherits a 1.  -/
Submonoid.one : {M : Type u_4} → [inst : MulOneClass M] → (S : Submonoid M) → One ↥S
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.pi_empty : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] (H : (i : η) → Subgroup (f i)), Subgroup.pi ∅ H = ⊤
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to `EReal`. The unprimed version of
the lemma uses `[ContinuousAdd]`.  -/
LowerSemicontinuousAt.add' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_5} [inst_1 : AddCommMonoid γ] [inst_2 : LinearOrder γ]
  [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] {f g : α → γ},
  LowerSemicontinuousAt f x →
    LowerSemicontinuousAt g x →
      ContinuousAt (fun p => p.1 + p.2) (f x, g x) → LowerSemicontinuousAt (fun z => f z + g z) x
-- Mathlib.LinearAlgebra.Pi
LinearMap.pi_comp : ∀ {R : Type u} {M₂ : Type w} {M₃ : Type y} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₃] {φ : ι → Type i}
  [inst_5 : (i : ι) → AddCommMonoid (φ i)] [inst_6 : (i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i)
  (g : M₃ →ₗ[R] M₂), LinearMap.pi f ∘ₗ g = LinearMap.pi fun i => f i ∘ₗ g
-- Mathlib.RingTheory.WittVector.Defs
/-- Construct a Witt vector `mk p x : 𝕎 R` from a sequence `x` of elements of `R`.

This is preferred over `WittVector.mk'` because it has `p` explicit.
 -/
WittVector.mk : (p : ℕ) → {R : Type u_1} → (ℕ → R) → WittVector p R
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.del.match_1.eq_2 : ∀ (motive : RBTree.RBColor → Sort u_1) (h_1 : Unit → motive RBTree.RBColor.black)
  (h_2 : Unit → motive RBTree.RBColor.red),
  (match RBTree.RBColor.red with
    | RBTree.RBColor.black => h_1 ()
    | RBTree.RBColor.red => h_2 ()) =
    h_2 ()
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.map_addPolynomial : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S)
  (x y ℓ : R), (W'.map f).addPolynomial (f x) (f y) (f ℓ) = Polynomial.map f (W'.addPolynomial x y ℓ)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- A combination of two points expressed with `lineMap` lies in their affine span.  -/
AffineMap.lineMap_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), (AffineMap.lineMap p₁ p₂) r ∈ line[k, p₁, p₂]
-- Mathlib.Tactic.Abel
/-- The type of the ambient additive commutative group or monoid.  -/
Mathlib.Tactic.Abel.Context.α : Mathlib.Tactic.Abel.Context → Lean.Expr
-- Init.Control.Lawful.Instances
OptionT.run_lift : ∀ {m : Type u → Type v} {α : Type u} [inst : Monad m] (x : m α),
  (OptionT.lift x).run = do
    let __do_lift ← x
    pure (some __do_lift)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod.fst_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} (x : C),
  CategoryTheory.FunctorToTypes.prod.fst.app x = TypeCat.ofHom fun a => a.1
-- Mathlib.RingTheory.DividedPowers.Basic
/-- Variant of `DividedPowers.dpow_add` with a sum on `range (n + 1)`  -/
DividedPowers.dpow_add' : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {a b : A} (hI : DividedPowers I) {n : ℕ},
  a ∈ I → b ∈ I → hI.dpow n (a + b) = ∑ k ∈ Finset.range (n + 1), hI.dpow k a * hI.dpow (n - k) b
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_toInt64 : ∀ (n : ISize) (h : System.Platform.numBits = 64), n.toInt64.toBitVec = BitVec.signExtend 64 (n.toBitVec64 h)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_smul_apply : ∀ {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : Module S V]
  [inst_6 : ContinuousConstSMul S V] [inst_7 : AddCommMonoid W] [inst_8 : Module R W] [inst_9 : TopologicalSpace W]
  [inst_10 : Module S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : SMulCommClass R S W] [inst_13 : SMul S R]
  [inst_14 : IsScalarTower S R V] [inst_15 : IsScalarTower S R W] (e : V ≃L[R] W) (α : Sˣ) (x : W),
  (α • e).symm x = ↑α⁻¹ • e.symm x