mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_sub_map_piecewise : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : LinearOrder ι] (a b : (i : ι) → M₁ i) (s : Finset ι),
  f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.Hom.id_eq_id : ∀ {J : CategoryTheory.Limits.MultispanShape} (X : CategoryTheory.Limits.WalkingMultispan J),
  CategoryTheory.Limits.WalkingMultispan.Hom.id X = CategoryTheory.CategoryStruct.id X
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.mk : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        (toSolution' : FermatLastTheoremForThreeGen.Solution'✝ hζ) →
          (hζ.toInteger - 1) ^ 2 ∣
              FermatLastTheoremForThreeGen.Solution'.a✝ toSolution' +
                FermatLastTheoremForThreeGen.Solution'.b✝ toSolution' →
            FermatLastTheoremForThreeGen.Solution✝ hζ
-- Mathlib.Order.CompleteLattice.Basic
iInf_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α}, ⨅ x ∈ Set.univ, f x = ⨅ x, f x
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sOppSide_iff_exists_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₂ : P},
  p₂ ∈ s → (s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
-- Mathlib.Analysis.Normed.Group.Basic
NormedGroup.tendsto_nhds_nhds : ∀ {E : Type u_5} {F : Type u_6} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {f : E → F} {x : E} {y : F},
  Filter.Tendsto f (nhds x) (nhds y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x'⁻¹ * x‖ < δ → ‖(f x')⁻¹ * y‖ < ε
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_injective : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, Function.Injective SimpleGraph.Walk.reverse
-- Mathlib.Data.Rat.Cast.Lemmas
Rat.cast_inv_nat : ∀ {α : Type u_1} [inst : DivisionRing α] (n : ℕ), ↑(↑n)⁻¹ = (↑n)⁻¹
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₁₂FunctorObj_map_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  {G G' : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} (φ : G ⟶ G') (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
  ((((CategoryTheory.bifunctorComp₁₂FunctorObj F₁₂).map φ).app X₁).app X₂).app X₃ = (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.mk.inj : ∀ {position : Lean.Lsp.Position} {label : Lean.Lsp.InlayHintLabel} {kind? : Option Lean.Lsp.InlayHintKind}
  {textEdits? : Option (Array Lean.Lsp.TextEdit)} {tooltip? : Option Lean.Lsp.InlayHintTooltip}
  {paddingLeft? paddingRight? : Option Bool} {data? : Option Lean.Json} {position_1 : Lean.Lsp.Position}
  {label_1 : Lean.Lsp.InlayHintLabel} {kind?_1 : Option Lean.Lsp.InlayHintKind}
  {textEdits?_1 : Option (Array Lean.Lsp.TextEdit)} {tooltip?_1 : Option Lean.Lsp.InlayHintTooltip}
  {paddingLeft?_1 paddingRight?_1 : Option Bool} {data?_1 : Option Lean.Json},
  { position := position, label := label, kind? := kind?, textEdits? := textEdits?, tooltip? := tooltip?,
        paddingLeft? := paddingLeft?, paddingRight? := paddingRight?, data? := data? } =
      { position := position_1, label := label_1, kind? := kind?_1, textEdits? := textEdits?_1, tooltip? := tooltip?_1,
        paddingLeft? := paddingLeft?_1, paddingRight? := paddingRight?_1, data? := data?_1 } →
    position = position_1 ∧
      label = label_1 ∧
        kind? = kind?_1 ∧
          textEdits? = textEdits?_1 ∧
            tooltip? = tooltip?_1 ∧ paddingLeft? = paddingLeft?_1 ∧ paddingRight? = paddingRight?_1 ∧ data? = data?_1
-- Mathlib.Order.RelIso.Basic
/-- The lexicographic sum of an empty relation plus `s` is isomorphic to `s`.  -/
RelIso.emptySumLex : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → [IsEmpty α] → Sum.Lex r s ≃r s
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddZeroClass.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : AddZeroClass M],
  Filter.Germ.instAddZeroClass =
    { toZero := Filter.Germ.instZero, toAdd := Filter.Germ.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D.eq_1 : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] [inst_2 : CategoryTheory.IsCofiltered I]
  [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f),
  A.𝒰D = CategoryTheory.Precoverage.ZeroHypercover.bind A.𝒰D₀ fun x => (A.𝒰D₀.X x).affineCover
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- If `e` is a linear equivalence, it induces a `ℤ`-linear equivalence between
`L` and `ZLattice.comap K L e`.  -/
ZLattice.comap_equiv : (K : Type u_1) →
  [inst : NormedField K] →
    {E : Type u_2} →
      {F : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace K E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace K F] → (L : Submodule ℤ E) → (e : F ≃ₗ[K] E) → ↥L ≃ₗ[ℤ] ↥(ZLattice.comap K L ↑e)
-- Mathlib.SetTheory.Lists
Lists.Equiv.below.antisymm : ∀ {α : Type u_1} {motive_1 : (a a_1 : Lists α) → a.Equiv a_1 → Prop}
  {motive_2 : (a a_1 : Lists' α true) → a.Subset a_1 → Prop} {l₁ l₂ : Lists' α true} (a : l₁.Subset l₂)
  (a_1 : l₂.Subset l₁), a.below → motive_2 l₁ l₂ a → a_1.below → motive_2 l₂ l₁ a_1 → ⋯.below
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coeOutMonoidHom : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → CoeOut (A →ₐ[R] B) (A →* B)
-- Std.Data.Iterators.Lemmas.Consumers.Set
_private.Std.Data.Iterators.Lemmas.Consumers.Set.0.Std.Iter.toExtTreeSet.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] (it : Std.Iter β)
  (cmp : β → β → Ordering) [inst_2 : Std.TransCmp cmp], it.toExtTreeSet cmp = (it.toIterM.toExtTreeSet cmp).run
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run `grind` at every step in proofs, reporting where it succeeds.  -/
linter.tacticAnalysis.tryAtEachStepGrind : Lean.Option Bool
-- Init.Data.Rat.Lemmas
Rat.sub_def : ∀ (a b : ℚ), a - b = Rat.normalize (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den) ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.getKey? (t.minKey he) = some (t.minKey he)
-- Mathlib.Order.SuccPred.Basic
Order.succ_pred_iterate_of_not_isMin : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : SuccOrder α] (i : α) (n : ℕ),
  ¬IsMin (Order.pred^[n - 1] i) → Order.succ^[n] (Order.pred^[n] i) = i
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_of_add_const : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f : α → M} (C : M), Filter.Tendsto (fun x => f x + C) l Filter.atTop → Filter.Tendsto f l Filter.atTop
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeFormEquiv_apply : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
  (a : CliffordAlgebra Q), (CliffordAlgebra.changeFormEquiv h) a = (CliffordAlgebra.changeForm h) a
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restrictionMap_f'_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsRelIff] {i : ι} {i' : ι'}
  (hi : e.f i = i') {Z : C} (h : (L.restriction e).X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HomologicalComplex.restrictionMap φ e).f i) h =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).hom
      (CategoryTheory.CategoryStruct.comp (φ.f i') (CategoryTheory.CategoryStruct.comp (L.restrictionXIso e hi).inv h))
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The action by a subalgebra is the action by the underlying algebra.  -/
Subalgebra.instMulActionSubtypeMem : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] → {α : Type u_1} → [MulAction A α] → (S : Subalgebra R A) → MulAction (↥S) α
-- Std.Data.DHashMap.Basic
/-- Returns the number of buckets in the internal representation of the hash map. This function may be
useful for things like monitoring system health, but it should be considered an internal
implementation detail.
 -/
Std.DHashMap.Internal.numBuckets : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → ℕ
-- Init.Data.Option.Lemmas
Option.map_apply : ∀ {α α_1 : Type u_1} {f : α → α_1} {x : Option α}, f <$> x = Option.map f x
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.uniformizingPolynomial.congr_simp : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v v_1 : Valuation (RatFunc K) Γ} (e_v : v = v_1) [inst_2 : v.IsNontrivial] [inst_3 : Valuation.IsTrivialOn K v]
  (hle : v RatFunc.X ≤ 1), RatFunc.uniformizingPolynomial hle = RatFunc.uniformizingPolynomial ⋯
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.ext_iff : ∀ {α : Type u_5} {ι : Type u_6} {x y : Combinatorics.Line α ι}, x = y ↔ x.idxFun = y.idxFun
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_zero : ∀ (a : ℤ), a.fmod 0 = a
-- Mathlib.Topology.DiscreteSubset
/-- **Alias** of `IsCompact.finite_sdiff_of_mem_codiscreteWithin`. -/
IsCompact.finite_diff_of_mem_codiscreteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s K : Set X}, IsCompact K → s ∈ Filter.codiscreteWithin K → (K \ s).Finite
-- Init.Data.Int.Order
Int.le_iff_eq_or_lt : ∀ {a b : ℤ}, a ≤ b ↔ a = b ∨ a < b
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ}
  [FiniteDimensional ℝ E], IsOpen C → ConcaveOn ℝ C f → ContinuousOn f C
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.natCast_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (n : ℕ), ↑n = Lean.Grind.Field.NormNum.ofRat ↑n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).getKey? k = if (f (Std.DTreeMap.Const.get? t k)).isSome = true then some k else none
-- Mathlib.Probability.CDF
MeasureTheory.Measure.cdf_eq_iff : ∀ (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν],
  ProbabilityTheory.cdf μ = ProbabilityTheory.cdf ν ↔ μ = ν
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
algNormFromConst_def : ∀ {K : Type u} [inst : NontriviallyNormedField K] {L : Type v} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] (h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1)
  {x y : L} (hx : x ≠ 0), (algNormFromConst h1 hx) y = (seminormFromConst h1 ⋯ ⋯) y
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.Const.beqModel : {α : Type u} → {β : Type v} → [BEq α] → [BEq β] → List ((_ : α) × β) → List ((_ : α) × β) → Bool
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousWithinAt_iInf_dom : ∀ {ι : Type u_1} {κ : Type u_2} {X' : Type u_4} {α : Type u_6} [uα : UniformSpace α] {t : κ → TopologicalSpace X'}
  {F : ι → X' → α} {S : Set X'} {x₀ : X'} {k : κ}, EquicontinuousWithinAt F S x₀ → EquicontinuousWithinAt F S x₀
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F) {X : C}
  (h : E.IsPointwiseRightKanExtensionAt (L.obj X)) [L.Full] [L.Faithful],
  CategoryTheory.IsIso ((CategoryTheory.CostructuredArrow.hom E).app X)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.erase.match_1.eq_1 : ∀ {α : Type u_1} (as : Array α) (motive : Option (Fin as.size) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (i : Fin as.size) → motive (some i)),
  (match none with
    | none => h_1 ()
    | some i => h_2 i) =
    h_1 ()
-- Mathlib.Data.Rel
SetRel.isTrans_preimage : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : β → α} [R.IsTrans], SetRel.IsTrans (Prod.map f f ⁻¹' R)
-- Mathlib.Order.Ideal
Order.Ideal.IsMaximal.isCoatom' : ∀ {P : Type u_1} [inst : LE P] [inst_1 : IsDirectedOrder P] [inst_2 : Nonempty P] {I : Order.Ideal P} [I.IsMaximal],
  IsCoatom I
-- Mathlib.Analysis.Calculus.DSlope
differentiableWithinAt_dslope_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} {s : Set 𝕜},
  b ≠ a → (DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a k : α} {v : β k}, (m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a
-- Mathlib.MeasureTheory.Measure.Prod
/-- The reversed version of **Tonelli's Theorem**. In this version `f` is in curried form, which
makes it easier for the elaborator to figure out `f` automatically.  -/
MeasureTheory.lintegral_lintegral : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] ⦃f : α → β → ENNReal⦄,
  AEMeasurable (Function.uncurry f) (μ.prod ν) →
    ∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (z : α × β), f z.1 z.2 ∂μ.prod ν
-- Mathlib.LinearAlgebra.Orientation
Module.Basis.det_adjustToOrientation : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  [inst_7 : Nonempty ι] (e : Module.Basis ι R M) (x : Orientation R M ι),
  (e.adjustToOrientation x).det = e.det ∨ (e.adjustToOrientation x).det = -e.det
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsRefl.neg : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B : LinearMap.BilinForm R₁ M₁}, B.IsRefl → (-B).IsRefl
-- Lean.Elab.DeprecatedSyntax
Lean.Elab.SyntaxDeprecationEntry.mk.sizeOf_spec : ∀ (kind : Lean.SyntaxNodeKind) (text? since? : Option String),
  sizeOf { kind := kind, text? := text?, since? := since? } = 1 + sizeOf kind + sizeOf text? + sizeOf since?
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {R : Type u_2} [inst_3 : Monoid R]
  [inst_4 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  HasStrictDerivAt f f' x → HasStrictDerivAt (c • f) (c • f') x
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.symm.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : ∀ (x : B), Nonempty (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (b : B) (y : F), e.symm b y = e.toPretrivialization.symm b y
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- a functor between the two categories  -/
CategoryTheory.LocalizerMorphism.functor : {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₂} →
            CategoryTheory.LocalizerMorphism W₁ W₂ → CategoryTheory.Functor C₁ C₂
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_eq_none : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, a ∉ m → m.getKey? a = none
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.forget₂RingObjCat_map_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.CommRingObjCat C} (f : X ⟶ Y),
  ((CategoryTheory.CommRingObjCat.forget₂RingObjCat C).map f).hom = f.hom
-- Mathlib.CategoryTheory.IsConnected
/-- We define a connected category as a _nonempty_ category for which every
functor to a discrete category is constant.

NB. Some authors include the empty category as connected, we do not.
We instead are interested in categories with exactly one 'connected
component'.

This allows us to show that the functor X ⨯ - preserves connected limits.  -/
CategoryTheory.IsConnected : (J : Type u₁) → [CategoryTheory.Category.{v₁, u₁} J] → Prop
-- Mathlib.AlgebraicTopology.TopologicalSimplex
/-- The functor `SimplexCategory ⥤ TopCat.{u}`
associating the topological `n`-simplex to `⦋n⦌ : SimplexCategory`.  -/
SimplexCategory.toTop : CategoryTheory.Functor SimplexCategory TopCat
-- Lean.Parser.Extra
/-- The parser `optional(p)`, or `(p)?`, parses `p` if it succeeds,
otherwise it succeeds with no value.

Note that because `?` is a legal identifier character, one must write `(p)?` or `p ?` for
it to parse correctly. `ident?` will not work; one must write `(ident)?` instead.

This parser has arity 1: it produces a `nullKind` node containing either zero arguments
(for the `none` case) or the list of arguments produced by `p`.
(In particular, if `p` has arity 0 then the two cases are not differentiated!)  -/
Lean.Parser.optional : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Analysis.Calculus.Deriv.ZPow
differentiableOn_zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (m : ℤ) (s : Set 𝕜),
  0 ∉ s ∨ 0 ≤ m → DifferentiableOn 𝕜 (fun x => x ^ m) s
-- Mathlib.MeasureTheory.Group.Arithmetic
MulOpposite.instMeasurableMul : ∀ {M : Type u_2} [inst : Mul M] [inst_1 : MeasurableSpace M] [MeasurableMul M], MeasurableMul Mᵐᵒᵖ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.ofIso_index : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {Y : SSet} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B)
  (x : ↑P.II) {d : ℕ} (hd : (↑x).dim = d) [inst : P.IsProper], ⋯.index hd = ⋯.index hd
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.hasHomology_of_zeros : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y Z : C), { X₁ := X, X₂ := Y, X₃ := Z, f := 0, g := 0, zero := ⋯ }.HasHomology
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
/-- The directed system of finitely generated submodules of `M`  -/
Submodule.FG.directedSystem : ∀ {R : Type u} [inst : Semiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  DirectedSystem (fun P => ↥↑P) fun ⦃P Q⦄ h => ⇑(Submodule.inclusion h)
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.isIrreducible_iff : ∀ {ι : 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),
  P.IsIrreducible ↔
    Nontrivial M ∧
      Nontrivial N ∧
        (∀ (q : Submodule R M), (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤) ∧
          ∀ (q : Submodule R N), (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.coreflection i)) → q ≠ ⊥ → q = ⊤
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ},
  (Std.DHashMap.emptyWithCapacity c).getKey? a = none
-- Lean.Message
Lean.instToJsonSerialMessage : Lean.ToJson Lean.SerialMessage
-- Mathlib.Order.Fin.Basic
Fin.succOrderEmb_toEmbedding : ∀ {n : ℕ}, (Fin.succOrderEmb n).toEmbedding = Fin.succEmb n
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.pure.eq_1 : ∀ {m : Type w → Type w'} [inst : Pure m] {α : Type v} (a : α),
  Std.Iterators.HetT.pure a =
    { Property := fun x => a = x, small := ⋯, operation := pure (Std.Internal.USquash.deflate ⟨a, ⋯⟩) }
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
/-- `ExteriorAlgebra.liftAlternating` is an equivalence.  -/
ExteriorAlgebra.liftAlternatingEquiv : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- `quotQuotToQuotSup` and `liftSupQuotQuotMk` are inverse isomorphisms. In the case where
`I ≤ J`, this is the Third Isomorphism Theorem (see `quotQuotEquivQuotOfLe`).  -/
DoubleQuot.quotQuotEquivQuotSup : {R : Type u} → [inst : CommRing R] → (I J : Ideal R) → (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* R ⧸ I ⊔ J
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (t.insertMany l).get? k = t.get? k
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.ofSubsingleton_symm_apply_apply : ∀ (R : Type uR) {ι : 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₃] [inst_5 : Subsingleton ι] (i : ι)
  (f : MultilinearMap R (fun x => M₂) M₃) (x : M₂),
  ((MultilinearMap.ofSubsingleton R M₂ M₃ i).symm f) x = f fun x_1 => x
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.zero_add_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (h : CategoryTheory.ShiftMkCore C A) (n : A) (X : C),
  (h.add 0 n).inv.app X = CategoryTheory.CategoryStruct.comp ((h.F n).map (h.zero.hom.app X)) (CategoryTheory.eqToHom ⋯)