mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_1.go : {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  {motive_2 :
      Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
        Sort u} →
    {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
      {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
        {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
          {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
            {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
              {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
                (t :
                    Lean.Language.TransformedSnap
                      (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
                  ((t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t) →
                    ((t :
                          Lean.Language.TransformedSnap
                            (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
                        Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t) →
                      ((t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                          Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t) →
                        ((t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
                            Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t) →
                          ((t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                              Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t) →
                            ((t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                                Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t) →
                              ((t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                                  Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t) →
                                ((t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                                    Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t) →
                                  motive_2 t ×' Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coe_mul : ∀ {R : Type u_1} [inst : Semiring R] (f g : PowerSeries R),
  (HahnSeries.ofPowerSeries ℤ R) (f * g) = (HahnSeries.ofPowerSeries ℤ R) f * (HahnSeries.ofPowerSeries ℤ R) g
-- Lean.DefEqAttrib
/-- Marks a theorem as a definitional equality under the permissive transparency rules that
predated the stricter `@[defeq]` inference (i.e. an equality that holds at `.default` or
`.all` transparency, but possibly not at `.instances` transparency as required by `dsimp`).

Such theorems are inferred automatically by `inferDefEqAttr`: any theorem that the old
`:= rfl` inference would have accepted is tagged `@[backward_defeq]`, and additionally
tagged `@[defeq]` when it also passes the stricter check at instance transparency.

`dsimp` ignores `@[backward_defeq]` theorems by default. Setting
`set_option backward.defeqAttrib.useBackward true` (typically scoped to a single proof
with `set_option ... in`) makes `dsimp` treat them like `@[defeq]` theorems, which
provides a local backwards-compatibility escape hatch for proofs broken by the stricter
inference.
 -/
Lean.backwardDefeqAttr : Lean.TagAttribute
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncOptions.openClose : Lean.Lsp.TextDocumentSyncOptions → Bool
-- Mathlib.Topology.UniformSpace.Basic
uniformity_eq_uniformity_closure : ∀ {α : Type ua} [inst : UniformSpace α], uniformity α = (uniformity α).lift' closure
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- The Fréchet derivative on Schwartz space as a continuous `𝕜`-linear map.  -/
SchwartzMap.fderivCLM : (𝕜 : Type u_2) →
  (E : Type u_5) →
    (F : Type u_8) →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace ℝ F] →
            [inst_3 : NormedSpace ℝ E] →
              [inst_4 : RCLike 𝕜] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] → SchwartzMap E F →L[𝕜] SchwartzMap E (E →L[ℝ] F)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator.congr_simp : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v v_1 : Valuation A Γ)
  (e_v : v = v_1) [inst_2 : v.IsRankOneDiscrete],
  Valuation.IsRankOneDiscrete.generator v = Valuation.IsRankOneDiscrete.generator v_1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_roo_eq_add : ∀ {m n i fallback : ℕ}, i < n - (m + 1) → (m<...n).toArray.getD i fallback = m + 1 + i
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a localization map `f : M →+ N`, the surjection sending `(x, y) : M × S` to
`f x - f y`.  -/
AddSubmonoid.LocalizationMap.mk' : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} → {N : Type u_2} → [inst_1 : AddCommMonoid N] → S.LocalizationMap N → M → ↥S → N
-- Init.Data.Array.Basic
Array.findIdx?.loop.eq_def : ∀ {α : Type u} (p : α → Bool) (as : Array α) (j : ℕ),
  Array.findIdx?.loop p as j =
    if h : j < as.size then if p as[j] = true then some j else Array.findIdx?.loop p as (j + 1) else none
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.toMeasurable μ s =ᵐ[μ] s
-- Lean.Elab.Tactic.Location
/-- Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given `loc`.
* If `loc` is a list of locations, runs at each specified hypothesis (and finally the goal if `⊢` is included),
  and fails if any of the tactic applications fail.
* If `loc` is `*`, runs at the target first and then the hypotheses in reverse order.
  If `atTarget` closes the main goal, `withLocation` does not run `atLocal`.
  If all tactic applications fail, `withLocation` with call `failed` with the main goal mvar.
 -/
Lean.Elab.Tactic.withLocation : Lean.Elab.Tactic.Location →
  (Lean.FVarId → Lean.Elab.Tactic.TacticM Unit) →
    Lean.Elab.Tactic.TacticM Unit → (Lean.MVarId → Lean.Elab.Tactic.TacticM Unit) → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Order.Interval.Set.OrdConnected
OrderEmbedding.image_Ioc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β),
  (Set.range ⇑e).OrdConnected → ∀ (x y : α), ⇑e '' Set.Ioc x y = Set.Ioc (e x) (e y)
-- Std.Internal.Do.WP.Basic
/-- `OptionT` lifts a `WPMonad` instance by adding a `PUnit` exception postcondition layer.  -/
Std.Internal.Do.OptionT.instWPMonad : {m : Type u → Type z} →
  {EPred : Type u_1} →
    {Pred : Type u} →
      [inst : Monad m] →
        [inst_1 : Std.Internal.Do.Assertion Pred] →
          [inst_2 : Std.Internal.Do.Assertion EPred] →
            [Std.Internal.Do.WPMonad m Pred EPred] → Std.Internal.Do.WPMonad (OptionT m) Pred (EPost.Cons✝ Pred EPred)
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.instSMulOfModule : {ι : Type v} →
  {β : ι → Type w} →
    {R : Type u} →
      [inst : Semiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (β i)] → [(i : ι) → Module R (β i)] → SMul R (DirectSum ι fun i => β i)
-- Mathlib.Algebra.Module.Defs
sub_smul : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r s : R) (y : M),
  (r - s) • y = r • y - s • y
-- Mathlib.RingTheory.Ideal.UFD
Ideal.isPrincipal_of_isPrincipal_localizationAway_of_prime : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [WfDvdMonoid R] {x : R},
  Prime x →
    ∀ {p : Ideal R} [p.IsPrime],
      x ∉ p → Submodule.IsPrincipal (Ideal.map (algebraMap R (Localization.Away x)) p) → Submodule.IsPrincipal p
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} {α β : F ⟶ G} (h : α = β)
  (X : CategoryTheory.Endofunctor.Algebra G),
  ((CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq h).inv.app X).f = CategoryTheory.CategoryStruct.id X.a
-- Mathlib.Data.Opposite
Opposite.op.inj : ∀ {α : Sort u} {unop unop_1 : α}, Opposite.op unop = Opposite.op unop_1 → unop = unop_1
-- Mathlib.Dynamics.Ergodic.Action.Basic
ErgodicVAdd.toVAddInvariantMeasure : ∀ {G : Type u_1} {α : Type u_2} {inst : VAdd G α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [self : ErgodicVAdd G α μ], MeasureTheory.VAddInvariantMeasure G α μ
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- If `M` and `M'` are free, then the rank of `M × M'` is
`(Module.rank R M).lift + (Module.rank R M').lift`.  -/
rank_prod : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [StrongRankCondition R] [Module.Free R M] [Module.Free R M'],
  Module.rank R (M × M') = Cardinal.lift.{v', v} (Module.rank R M) + Cardinal.lift.{v, v'} (Module.rank R M')
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- If `P` is induced by `Locally Q`, it suffices to check `Q` on affine open sets locally around
points of the source.  -/
AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {X Y : AlgebraicGeometry.Scheme}
  {f : X ⟶ Y},
  (RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
      ∀
        [AlgebraicGeometry.HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] =>
            RingHom.Locally fun {R S} [CommRing R] [CommRing S] => Q],
        P f ↔
          ∀ (x : ↥X),
            ∃ U V,
              ∃ (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U),
                Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e))
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_toLinearIsometry : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑e.toLinearIsometry = ⇑e
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
AddCommGroup.toAddCommMonoid.hcongr_2 : ∀ (G G' : Type u),
  G = G' →
    ∀ (self : AddCommGroup G) (self' : AddCommGroup G'), self ≍ self' → self.toAddCommMonoid ≍ self'.toAddCommMonoid
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.map_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} {f'' : X'' ⟶ Y''} {g'' : X'' ⟶ Z''} (i₁ : X ⟶ X') (j₁ : X' ⟶ X'') (i₂ : Y ⟶ Y')
  (j₂ : Y' ⟶ Y'') (i₃ : Z ⟶ Z') (j₃ : Z' ⟶ Z'') [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' g'] [inst_3 : CategoryTheory.Limits.HasPushout f'' g'']
  (e₁ : CategoryTheory.CategoryStruct.comp f i₂ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₁ g')
  (e₃ : CategoryTheory.CategoryStruct.comp f' j₂ = CategoryTheory.CategoryStruct.comp j₁ f'')
  (e₄ : CategoryTheory.CategoryStruct.comp g' j₃ = CategoryTheory.CategoryStruct.comp j₁ g'') {Z_1 : C}
  (h : CategoryTheory.Limits.pushout f'' g'' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.map f g f' g' i₂ i₃ i₁ e₁ e₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.map f g f'' g'' (CategoryTheory.CategoryStruct.comp i₂ j₂)
        (CategoryTheory.CategoryStruct.comp i₃ j₃) (CategoryTheory.CategoryStruct.comp i₁ j₁) ⋯ ⋯)
      h
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.Equivalence.fullyFaithfulFunctor.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (e : C ≌ E),
  e.fullyFaithfulFunctor =
    {
      preimage := fun {X Y} f =>
        CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X)
          (CategoryTheory.CategoryStruct.comp (e.inverse.map f) (e.unitIso.inv.app Y)),
      map_preimage := ⋯, preimage_map := ⋯ }
-- Mathlib.Algebra.Lie.SkewAdjoint
/-- The Lie subalgebra of skew-adjoint square matrices corresponding to a square matrix `J`.  -/
skewAdjointMatricesLieSubalgebra : {R : Type u} →
  {n : Type w} →
    [inst : CommRing R] →
      [inst_1 : Fintype n] → Matrix n n R → [inst_2 : DecidableEq n] → LieSubalgebra R (Matrix n n R)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_sum : ∀ {R : Type u_1} {M : Type u_4} {ι : Type u_7} [inst : Semiring R] (s : Finset ι) (f : ι → MonoidAlgebra R M),
  (∑ i ∈ s, f i).coeff = ∑ i ∈ s, (f i).coeff
-- Init.Data.String.Defs
String.Pos.Raw.offsetBy_sliceRawEndPos_right : ∀ {p : String.Pos.Raw} {s : String.Slice}, p.offsetBy s.rawEndPos = s + p
-- Std.Data.DHashMap.Internal.Defs
_private.Std.Data.DHashMap.Internal.Defs.0.Std.DHashMap.Internal.numBucketsForCapacity : ℕ → ℕ
-- Mathlib.CategoryTheory.Square
/-- The top-right evaluation `Square C ⥤ C`.  -/
CategoryTheory.Square.evaluation₂ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.Square C) C
-- Lean.Meta.Sym.SymM
/-- `true` if this argument is a type class instance.  -/
Lean.Meta.Sym.ProofInstArgInfo.isInstance : Lean.Meta.Sym.ProofInstArgInfo → Bool
-- Mathlib.Data.Part
/-- `Part` extensionality  -/
Part.ext : ∀ {α : Type u_1} {o p : Part α}, (∀ (a : α), a ∈ o ↔ a ∈ p) → o = p
-- Init.Data.Iterators.Basic
/-- The type of the step object returned by `IterM.step`, containing an `IterStep`
and a proof that this is a plausible step for the given iterator.
 -/
Std.IterM.Step : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → [Std.Iterator α m β] → Std.IterM m β → Type (max 0 w)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxcIterator.step : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.DTreeMap.Internal.RxcIterator α β → Std.IterStep (Std.IterM Id ((a : α) × β a)) ((a : α) × β a)
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.shiftIso_add'_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n m mn : A) (hnm : m + n = mn)
  (a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C),
  (F.shiftIso mn a a'' ⋯).hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D m n mn hnm).hom.app ((F.functor a'').obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X))
        ((F.shiftIso n a a' ha').hom.app X))
-- Mathlib.Data.Finset.Image
/-- If a `Finset` of a subtype is converted to the main type with
`Embedding.subtype`, the result is a subset of the set giving the
subtype.  -/
Finset.map_subtype_subset : ∀ {α : Type u_1} {t : Set α} (s : Finset ↑t), ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ t) s) ⊆ t
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `k.right` is an epimorphism, then `k` is an epimorphism. In other words, `Under.forget X`
reflects epimorphisms.
The converse of `CategoryTheory.Under.epi_right_of_epi`.

This lemma is not an instance, to avoid loops in type class inference.
 -/
CategoryTheory.Under.epi_of_epi_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (k : f ⟶ g)
  [hk : CategoryTheory.Epi (CategoryTheory.Under.Hom.right k)], CategoryTheory.Epi k
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.mul_lt_omega0_opow : ∀ {a b c : Ordinal.{u}}, 0 < c → a < Ordinal.omega0 ^ c → b < Ordinal.omega0 → a * b < Ordinal.omega0 ^ c
-- Mathlib.Algebra.GradedMonoid
/-- Multiplication is commutative  -/
GradedMonoid.GCommMonoid.mul_comm : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddCommMonoid ι} [self : GradedMonoid.GCommMonoid A] (a b : GradedMonoid A),
  a * b = b * a
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.ExportedAxiomsState.importedModuleEntries : Lean.ExportedAxiomsState✝ → Array (Array (Lean.Name × Array Lean.Name))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.isEmpty = true → t.contains a = false
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintParams.toWorkDoneProgressParams : Lean.Lsp.InlayHintParams → Lean.Lsp.WorkDoneProgressParams
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.Const.alter.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : Option ((_ : α) × β) → Sort u_3) →
      (x : Option ((_ : α) × β)) → (Unit → motive none) → ((fst : α) → (v' : β) → motive (some ⟨fst, v'⟩)) → motive x
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.instLeAtTopComap : ∀ {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) [L.LeAtTop] (f : γ ↪ β), (L.comap f).LeAtTop
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffWithinAt.clm_precomp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₁ →L[𝕜] F₂}
  {s : Set M} {x : M},
  ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n f s x →
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) n
      (fun y => ContinuousLinearMap.precomp F₃ (f y)) s x
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfOrdArgs.max : {α : Type u} →
  (self : Std.Packages.LinearOrderOfOrdArgs α) →
    let this := self.ord;
    Max α
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierInv_eq_fourier_comp_neg : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : V → E), FourierTransformInv.fourierInv f = FourierTransform.fourier fun x => f (-x)
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.dual_univ : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair] [IsTopologicalRing R] [inst_13 : T1Space N],
  ProperCone.dual p Set.univ = ⊥
-- Init.Data.Fin.Lemmas
/-- A case analysis operator for `i : Fin (m + n)` that separately handles the cases where `i < m` and
where `m ≤ i < m + n`.

The first case, where `i < m`, is handled by `left`. In this case, `i` can be represented as
`Fin.castAdd n (j : Fin m)`.

The second case, where `m ≤ i < m + n`, is handled by `right`. In this case, `i` can be represented
as `Fin.natAdd m (j : Fin n)`.
 -/
Fin.addCases : {m n : ℕ} →
  {motive : Fin (m + n) → Sort u} →
    ((i : Fin m) → motive (Fin.castAdd n i)) → ((i : Fin n) → motive (Fin.natAdd m i)) → (i : Fin (m + n)) → motive i
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c) (n : ι),
  (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).p.f n = (K.X n).p
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If all the binary fans involved a limit cones, `BinaryFan.assoc` produces another limit cone.  -/
CategoryTheory.Limits.IsLimit.assoc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {sXY : CategoryTheory.Limits.BinaryFan X Y} →
        {sYZ : CategoryTheory.Limits.BinaryFan Y Z} →
          CategoryTheory.Limits.IsLimit sXY →
            (Q : CategoryTheory.Limits.IsLimit sYZ) →
              {s : CategoryTheory.Limits.BinaryFan sXY.pt Z} →
                CategoryTheory.Limits.IsLimit s →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.assoc Q s)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Spec.algebraMap_stalkIso_inv : ∀ {R : CommRingCat} (x : PrimeSpectrum ↑R),
  CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)))
      (AlgebraicGeometry.Spec.stalkIso R x).inv =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
      ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ x trivial)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited γ] {f : α → β → Option γ} {k : α} (h : m.WF),
  (Std.HashMap.Raw.filterMap f m)[k]! = (m[k]?.pbind fun x h' => f (m.getKey k ⋯) x).get!
-- Mathlib.SetTheory.Cardinal.Basic
/-- The cardinality of a set is an upper-bound for the amount of elements before the set's mex
(minimum excluded value)  -/
WellFounded.cardinalMk_subtype_lt_min_compl_le : ∀ {α : Type u} {r : α → α → Prop} (wf : WellFounded r) {s : Set α} (hs : sᶜ.Nonempty),
  Cardinal.mk { x // r x (wf.min sᶜ hs) } ≤ Cardinal.mk ↑s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyGE?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getKeyGE? k = t₂.getKeyGE? k
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_eq_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, k ∈ t → t.get! k = k
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- A correspondence `f : α → Set β` has open lower sections if and only if its *upper inverse*
(i.e., `b : β ↦ f ⁻¹' (Iic {b}ᶜ) = {x | b ∉ f x}`) sends every point to a closed set.  -/
hasOpenLowerSections_iff_isClosed_preimage_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β},
  HasOpenLowerSections f ↔ ∀ (b : β), IsClosed (f ⁻¹' Set.Iic {b}ᶜ)