mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Types
Lean.Elab.FVarAliasInfo.mk.sizeOf_spec : ∀ (userName : Lean.Name) (id baseId : Lean.FVarId),
  sizeOf { userName := userName, id := id, baseId := baseId } = 1 + sizeOf userName + sizeOf id + sizeOf baseId
-- Init.Data.Slice.Lemmas
Std.Slice.forIn_toList : ∀ {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [inst : Monad m] [LawfulMonad m] {δ : Type w}
  [inst_2 : Std.ToIterator (Std.Slice γ) Id α β] [inst_3 : Std.Iterator α Id β] [inst_4 : Std.IteratorLoop α Id m]
  [Std.LawfulIteratorLoop α Id m] [Std.Iterators.Finite α Id] {s : Std.Slice γ} {init : δ}
  {f : β → δ → m (ForInStep δ)}, forIn s.toList init f = forIn s init f
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- The underlying radius of a `logSizeBallStruct` (typically the log-size radius of the
underlying point in the underlying finite set)  -/
PairReduction.logSizeBallStruct.radius : {T : Type u_2} → PairReduction.logSizeBallStruct T → ℕ
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.HasRightDual.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X : C} → (rightDual : C) → [exact : CategoryTheory.ExactPairing X rightDual] → CategoryTheory.HasRightDual X
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- If `S` is dense and `x - y ∈ Kᗮ`, then `x = y`.  -/
Dense.eq_of_sub_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} {x y : E}, Dense ↑K → x - y ∈ Kᗮ → x = y
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then k else m.getKey a ⋯
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The transpose of an element in `SpecialLinearGroup R V`.  -/
SpecialLinearGroup.«term_ᵀ» : Lean.TrailingParserDescr
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_uIoo : ∀ {n : ℕ} (i j : Fin n), Fin.succ '' Set.uIoo i j = Set.uIoo i.succ j.succ
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mapAlgEquiv_id : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Polynomial.mapAlgEquiv AlgEquiv.refl = AlgEquiv.refl
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.map_preimage : ∀ {R S : CommRingCat} (f : AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R),
  AlgebraicGeometry.Spec.map (AlgebraicGeometry.Spec.preimage f) = f
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The natural isomorphism `t.truncGELE a b ≅ t.truncGELT a b'` when `b + 1 = b'`.  -/
CategoryTheory.Triangulated.TStructure.truncGELEIsoTruncGELT : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (a b b' : ℤ) → b + 1 = b' → (t.truncGELE a b ≅ t.truncGELT a b')
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.invRev : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
  FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
-- Mathlib.Algebra.Order.Group.End
RelEmbedding.one_apply : ∀ {α : Type u_1} {r : α → α → Prop} (a : α), 1 a = a
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.contDiff' : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (self : ContDiffMapSupportedIn E F n K),
  ContDiff ℝ (↑n) self.toFun
-- Mathlib.Algebra.FiveLemma
/-- A special case of one four lemma such that the left-most term is one in terms of
groups. For a diagram explaining the variables, see the module docstring.  -/
MonoidHom.surjective_of_surjective_of_injective_of_left_exact : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst : Group M₁]
  [inst_1 : Group M₂] [inst_2 : Group M₃] [inst_3 : Group N₁] [inst_4 : Group N₂] [inst_5 : Group N₃] (f₁ : M₁ →* M₂)
  (f₂ : M₂ →* M₃) (g₁ : N₁ →* N₂) (g₂ : N₂ →* N₃) (i₁ : M₁ →* N₁) (i₂ : M₂ →* N₂) (i₃ : M₃ →* N₃),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      Function.MulExact ⇑f₁ ⇑f₂ →
        Function.MulExact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₂ → Function.Injective ⇑i₃ → Function.Injective ⇑g₁ → Function.Surjective ⇑i₁
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.IsProper.mk : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing},
  (∀ (x : ↑P.II), (↑x).IsUniquelyCodimOneFace (↑(P.p x)).toS) → P.IsProper
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- If a category `C` has strong epi-mono factorization, for any `Y : C` and functor
`F : J ⥤ MonoOver Y`, there is a cocone under F.  -/
CategoryTheory.MonoOver.coconeOfHasStrongEpiMonoFactorisation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y : C} →
      [CategoryTheory.Limits.HasCoproducts C] →
        [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] →
          {J : Type u₂} →
            [inst_3 : CategoryTheory.Category.{v₂, u₂} J] →
              (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)) → CategoryTheory.Limits.Cocone F
-- Mathlib.Topology.Algebra.ConstMulAction
ProperlyDiscontinuousVAdd.exists_nhds_image_vadd_eq_self : ∀ (Γ : Type u_4) {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : VAdd Γ T] [ProperlyDiscontinuousVAdd Γ T]
  [T2Space T] [LocallyCompactSpace T] [ContinuousConstVAdd Γ T] (x : T),
  ∃ U ∈ nhds x, ∀ (γ : Γ), ((fun x => γ +ᵥ x) '' U ∩ U).Nonempty → γ +ᵥ x = x
-- Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
SSet.horn.primitiveTriangle.congr_simp : ∀ {n : ℕ} (i : Fin (n + 4)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (k k_1 : ℕ) (e_k : k = k_1) (h : k < n + 2),
  SSet.horn.primitiveTriangle i h₀ hₙ k h = SSet.horn.primitiveTriangle i h₀ hₙ k_1 ⋯
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- The **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  -/
MeasureTheory.«term∫⁻_In_,_» : Lean.ParserDescr
-- Mathlib.Topology.Closure
Dense.nonempty_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Dense s → (s.Nonempty ↔ Nonempty X)
-- Mathlib.Probability.Density
MeasureTheory.pdf.lintegral_eq_measure_univ : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ],
  ∫⁻ (x : E), MeasureTheory.pdf X ℙ μ x ∂μ = ℙ Set.univ
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The constant factor occurring in the conclusion of `eLpNorm_le_eLpNorm_fderiv_of_le`.
It only depends on `F`, `μ`, `s`, `p` and `q`.  -/
MeasureTheory.eLpNormLESNormFDerivOfLeConst : (F : Type u_6) →
  [inst : NormedAddCommGroup F] →
    [inst_1 : NormedSpace ℝ F] →
      {E : Type u_7} →
        [inst_2 : NormedAddCommGroup E] →
          [inst_3 : NormedSpace ℝ E] →
            [inst_4 : MeasurableSpace E] →
              [BorelSpace E] →
                [FiniteDimensional ℝ E] →
                  (μ : MeasureTheory.Measure E) →
                    [μ.IsAddHaarMeasure] → [FiniteDimensional ℝ F] → Set E → NNReal → NNReal → NNReal
-- Mathlib.Algebra.Field.Subfield.Defs
/-- Reinterpret a `Subfield` as a `Subring`.  -/
Subfield.toSubring : {K : Type u} → [inst : DivisionRing K] → Subfield K → Subring K
-- Lean.Parser.Term
Lean.Parser.Term.namedArgument.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.WithBot
WithBot.unbotA_lt_iff : ∀ {α : Type u_1} {a : α} [inst : LT α] {x : WithBot α} [inst_1 : Nonempty α], x ≠ ⊥ → (x.unbotA < a ↔ x < ↑a)
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piCongr_apply : ∀ {ι₁ : Type u_7} {ι₂ : Type u_8} {Y₁ : ι₁ → Type u_9} {Y₂ : ι₂ → Type u_10}
  [inst : (i₁ : ι₁) → TopologicalSpace (Y₁ i₁)] [inst_1 : (i₂ : ι₂) → TopologicalSpace (Y₂ i₂)] (e : ι₁ ≃ ι₂)
  (F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)) (a : (i : ι₁) → Y₁ i) (i₂ : ι₂),
  (Homeomorph.piCongr e F) a i₂ = (Equiv.piCongrLeft Y₂ e) ((Equiv.piCongrRight fun i => (F i).toEquiv) a) i₂
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.map_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : Opposite.op U' ⟶ Opposite.op U),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.map i) (AlgebraicGeometry.Scheme.Hom.appLE f U V e) =
    AlgebraicGeometry.Scheme.Hom.appLE f U' V ⋯
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_restrictScalars : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
  [inst_6 : SMul R R₂] [inst_7 : Module R₂ M] [inst_8 : Module R M₂] [inst_9 : LinearMap.CompatibleSMul M M₂ R R₂]
  [inst_10 : IsScalarTower R R₂ M₂] (f : M →ₗ[R₂] M₂), (↑R f).range = Submodule.restrictScalars R f.range
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.isEqv.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → (α → α → Bool) → Sort u_2) (x : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] [] x)
  (h_2 : (a : α) → (as : List α) → (b : α) → (bs : List α) → (eqv : α → α → Bool) → motive (a :: as) (b :: bs) eqv)
  (h_3 : (x x_1 : List α) → (x_2 : α → α → Bool) → motive x x_1 x_2),
  (match [], [], x with
    | [], [], x => h_1 x
    | a :: as, b :: bs, eqv => h_2 a as b bs eqv
    | x, x_1, x_2 => h_3 x x_1 x_2) =
    h_1 x
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Extends `PolynomialLaw.isCompat` to all universes  -/
PolynomialLaw.isCompat : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {S : Type v} [inst_5 : CommSemiring S] [inst_6 : Algebra R S]
  (f : M →ₚₗ[R] N) {T : Type w} [inst_7 : CommSemiring T] [inst_8 : Algebra R T] (h : S →ₐ[R] T),
  ⇑(LinearMap.rTensor N h.toLinearMap) ∘ PolynomialLaw.toFun S f =
    PolynomialLaw.toFun T f ∘ ⇑(LinearMap.rTensor M h.toLinearMap)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If an epimorphism in to `Y` is zero, then `Y ≅ 0`.  -/
CategoryTheory.Limits.isoZeroOfEpiEqZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {X Y : C} → {f : X ⟶ Y} → [CategoryTheory.Epi f] → f = 0 → (Y ≅ 0)
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
cthickening_thickening : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 ≤ ε → 0 < δ → ∀ (s : Set E), Metric.cthickening ε (Metric.thickening δ s) = Metric.cthickening (ε + δ) s
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
/-- The function `L → ℝ` sending `x : L` to the maximum of `algNormOfAlgEquiv hna σ` over
all `σ : L ≃ₐ[K] L` is an algebra norm on `L`.  -/
IsUltrametricDist.invariantExtension : (K : Type u_1) →
  [inst : NormedField K] →
    (L : Type u_2) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → [h_fin : FiniteDimensional K L] → [hu : IsUltrametricDist K] → AlgebraNorm K L
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.mem_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x : α}, x ∈ f.support ↔ f x ≠ x
-- Mathlib.Analysis.Convex.Function
ConvexOn.convex_epigraph : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulMono 𝕜 β] {s : Set E} {f : E → β}, ConvexOn 𝕜 s f → Convex 𝕜 {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepNormal.eq_7 : ∀ (f : Turing.ToPartrec.Code),
  Turing.ToPartrec.stepNormal f.fix = fun k v => Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) v
-- Mathlib.RingTheory.EssentialFiniteness
/-- An `R`-algebra is essentially of finite type if
it is the localization of an algebra of finite type.
See `essFiniteType_iff_exists_subalgebra`.

For field extensions, this is equivalent to being finitely generated as a field.
See `IntermediateField.fg_top_iff`.
 -/
Algebra.EssFiniteType : (R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indToCoindAux.eq_1 : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep.{w, u, v} k ↥S) (g : G),
  A.indToCoindAux g = LinearMap.pi fun g₁ => if h : (QuotientGroup.rightRel S) g₁ g then A.ρ ⟨g₁ * g⁻¹, ⋯⟩ else 0
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.incidence_other_neighbor_edge : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] {v w : V} (h : w ∈ G.neighborSet v),
  G.otherVertexOfIncident ⋯ = w
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_eq_of_equiv_const : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv] {f : CauSeq β abv}
  {x : β}, f ≈ CauSeq.const abv x → f.lim = x
-- Mathlib.Data.Quot
Quot.liftOn_mk : ∀ {α : Sort u_1} {γ : Sort u_4} {r : α → α → Prop} (a : α) (f : α → γ) (h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂),
  (Quot.mk r a).liftOn f h = f a
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_toCoalgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₐc[R] B), ⇑↑f = ⇑f
-- Lean.HeadIndex
Lean.HeadIndex.fvar.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Lean.HeadIndex.fvar fvarId) = 1 + sizeOf fvarId
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.coe_inj : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (f g : α →𝒄 β), ⇑f = ⇑g → f = g
-- Mathlib.Analysis.Complex.Norm
Complex.nnnorm_ratCast : ∀ (q : ℚ), ‖↑q‖₊ = ‖↑q‖₊
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- If a monic polynomial `p : R[X]` factors into a product of coprime monic polynomials `p = f * g`
in the residue field `κ(P)` of some `P : Spec R`,
then there exists an etale algebra `R'` of `R` and a prime `Q` of `R'` lying over `P`,
such that `κ(P) = κ(Q)` and that the factorization lifts to `R'`.  -/
Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime : ∀ {R : Type u} [inst : CommRing R] (P : Ideal R) [inst_1 : P.IsPrime] (p : Polynomial R)
  (f g : Polynomial P.ResidueField),
  p.Monic →
    f.Monic →
      g.Monic →
        Polynomial.map (algebraMap R P.ResidueField) p = f * g →
          IsCoprime f g →
            ∃ R' x x_1,
              ∃ (_ : Algebra.Etale R R'),
                ∃ Q,
                  ∃ (x_3 : Q.IsPrime) (x_4 : Q.LiesOver P),
                    ∃ f' g',
                      Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯) ∧
                        f'.Monic ∧
                          g'.Monic ∧
                            Polynomial.map (algebraMap R R') p = f' * g' ∧
                              IsCoprime f' g' ∧
                                Polynomial.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom f =
                                    Polynomial.map (algebraMap R' Q.ResidueField) f' ∧
                                  Polynomial.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom g =
                                    Polynomial.map (algebraMap R' Q.ResidueField) g'
-- Mathlib.Algebra.Group.Center
Set.addCentralizer.eq_1 : ∀ {M : Type u_1} (S : Set M) [inst : Add M], S.addCentralizer = {c | ∀ m ∈ S, m + c = c + m}
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Var.denote : {α : Type u_1} → Lean.Grind.Linarith.Context α → Lean.Grind.Linarith.Var → α
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.opEquiv_symm_apply : ∀ {X : SSet} {A : X.Subcomplex} (y : A.N),
  (RelIso.symm SSet.Subcomplex.N.opEquiv) y = { toN := SSet.N.opEquiv.symm y.toN, notMem := ⋯ }
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.toMulPosStrictMono : ∀ {α : Type u_5} (self : ConditionallyCompleteLinearOrderedField α), MulPosStrictMono α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_some_get!_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {a : α},
  m.contains a = true → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.get! m a)
-- Init.Data.UInt.Bitwise
UInt64.zero_xor : ∀ {a : UInt64}, 0 ^^^ a = a
-- Mathlib.Algebra.Algebra.Subalgebra.Rank
Subalgebra.rank_sup_eq_rank_right_mul_rank_of_free : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  [Module.Free R ↥B] [Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)],
  Module.rank R ↥(A ⊔ B) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B ↑A)
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.app_p_comp : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J),
  CategoryTheory.CategoryStruct.comp (P.p.app X) (f.f.app X) = f.f.app X
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertMany_append : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {l₁ l₂ : List (α × β)}, m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is a `SubNegOneMonoid` if `β` is a `SubNegOneMonoid`.  -/
FunLike.subNegZeroMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : Neg F] →
                [inst_5 : Sub F] →
                  [inst_6 : SMul ℤ F] →
                    [inst_7 : SubNegZeroMonoid β] →
                      [IsZeroApply F α β] →
                        [IsAddApply F α β] →
                          [IsNegApply F α β] →
                            [IsSubApply F α β] → [IsSMulApply ℕ F α β] → [IsSMulApply ℤ F α β] → SubNegZeroMonoid F
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_add : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A}
  {x y : NNReal}, 0 < x → 0 < y → a ^ (x + y) = a ^ x * a ^ y
-- Mathlib.GroupTheory.Torsion
AddCommGroup.map_torsion_le : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] (f : G →+ H),
  AddSubgroup.map f (AddCommGroup.torsion G) ≤ AddCommGroup.torsion H
-- Init.Data.Fin.Basic
/-- Bitwise and.
 -/
Fin.land : {n : ℕ} → Fin n → Fin n → Fin n
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.inst : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (i : ι), Topology.IsGeneratedBy X (X i)
-- Lean.Meta.InferType
Lean.Meta.typeFormerTypeLevelQuick : Lean.Expr → Option Lean.Level
-- Init.Data.Array.Range
Array.take_range : ∀ {i n : ℕ}, (Array.range n).take i = Array.range (min i n)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The `MorphismProperty C` satisfied by regular monomorphisms in `C`.  -/
CategoryTheory.MorphismProperty.regularMono : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.MorphismProperty C
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.sort.loop.match_1.eq_2 : ∀ (motive : List ℕ → List ℕ → Sort u_1) (acc : List ℕ) (x : ℕ) (xs : List ℕ) (h_1 : (acc : List ℕ) → motive acc [])
  (h_2 : (acc : List ℕ) → (x : ℕ) → (xs : List ℕ) → motive acc (x :: xs)),
  (match acc, x :: xs with
    | acc, [] => h_1 acc
    | acc, x :: xs => h_2 acc x xs) =
    h_2 acc x xs
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instVAddCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd N α] [VAddCommClass M N α],
  VAddCommClass (Lex M) N α
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.mem_iff_of_adj : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β},
  G.Adj x y → H.IsClosedSubgraph G → (x ∈ H.vertexSet ↔ y ∈ H.vertexSet)
-- Mathlib.Order.Interval.Finset.Defs
WithBot.some_mem_insertBot : ∀ {α : Type u_1} {s : Finset α} {a : α}, ↑a ∈ WithBot.insertBot s ↔ a ∈ s
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.funMap_zero : ∀ {M : Type u_2} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] {v : Fin 0 → M},
  FirstOrder.Language.Structure.funMap FirstOrder.presburgerFunc.zero v = 0
-- Lean.Elab.App
/-- * `fPreCoercion?` keeps track of what `f` was originally, if there was a coercion. For error reporting.
* `argIdx` is the position into `args` for the next place an explicit argument can be inserted.
* `remainingNamedArgs` keeps track of named arguments that haven't been visited yet,
  for handling the case where multiple parameters have the same name.
* `unusableNamedArgs` keeps track of names that can't be used as named arguments. This is initialized with user-provided named arguments.
* `allowNamed` is whether or not to allow using named arguments.
  Disabled after using `CoeFun` since those parameter names unlikely to be meaningful,
  and otherwise whether dot notation works or not could feel random.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.addLValArg.go : Lean.Name →
  Lean.Expr →
    Array Lean.Elab.Term.Arg →
      Array Lean.Elab.Term.NamedArg →
        Bool →
          Option Lean.Expr →
            Lean.Expr →
              Lean.Expr →
                ℕ →
                  Array Lean.Elab.Term.NamedArg →
                    Array Lean.Name → Bool → Lean.MetaM (Array Lean.Elab.Term.Arg × Array Lean.Elab.Term.NamedArg)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coe_powers : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x : HahnSeries Γ R}, 0 < x.orderTop → ⇑(HahnSeries.SummableFamily.powers x) = HPow.hPow x
-- Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
CategoryTheory.NatTrans.epi_iff_epi_app : ∀ {K : Type u} [inst : CategoryTheory.Category.{v, u} K] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F G : CategoryTheory.Functor K C} (f : F ⟶ G) [CategoryTheory.Limits.HasPushouts C],
  CategoryTheory.Epi f ↔ ∀ (k : K), CategoryTheory.Epi (f.app k)
-- Lean.Elab.Term.TermElabM
/-- Throws `Exception.postpone`, if `expectedType?` contains unassigned metavariables.
It is a noop if `mayPostpone == false`.
 -/
Lean.Elab.Term.tryPostponeIfHasMVars? : Option Lean.Expr → Lean.Elab.TermElabM (Option Lean.Expr)
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
/-- **Alias** of `HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic`. -/
HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) = (HomotopyCategory.subcategoryAcyclic C).trW