mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galLift.congr_simp : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : IsFractionRing A K] [inst_10 : Algebra K L]
  [inst_11 : Algebra A L] [inst_12 : IsScalarTower A K L] [inst_13 : Algebra K L₂] [inst_14 : Algebra A L₂]
  [inst_15 : IsScalarTower A K L₂] [inst_16 : Algebra B L] [inst_17 : IsScalarTower A B L]
  [inst_18 : IsIntegralClosure B A L] [inst_19 : Algebra B₂ L₂] [inst_20 : IsScalarTower A B₂ L₂]
  [inst_21 : Algebra.IsAlgebraic K L] (σ σ_1 : B →ₐ[A] B₂), σ = σ_1 → galLift K L L₂ σ = galLift K L L₂ σ_1
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Result.mk : Lean.Expr → Option Lean.Expr → Lean.Meta.LetToHave.Result✝
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.sOppSide_affineSpan_pair_excenter_singleton_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ → i₂ ≠ i₃ → line[ℝ, t.points i₂, t.points i₃].SOppSide (Affine.Simplex.excenter t {i₁}) (t.points i₁)
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.comp_sub : ∀ {M : Type u_2} {G : Type u_5} {H : Type u_6} [inst : AddZeroClass M] [inst_1 : AddCommGroup G]
  [inst_2 : AddCommGroup H] (f : G →+ H) (g h : M →+ G), f.comp (g - h) = f.comp g - f.comp h
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_neg_linearMap : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (D : LieDerivation R L M), ↑(-D) = -↑D
-- Mathlib.RingTheory.Perfection
PreTilt.instPerfectRing : ∀ (O : Type u₂) [inst : CommRing O] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p],
  PerfectRing (PreTilt O p) p
-- Mathlib.LinearAlgebra.Finsupp.Pi
LinearMap.prodOfFinsuppNat.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (f : P × M →ₗ[R] M),
  f.prodOfFinsuppNat = (Finsupp.lsum ℕ) fun n => ((LinearMap.inr R P M ∘ₗ f) ^ n) ∘ₗ LinearMap.inl R P M
-- Std.Data.ExtDHashMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
 -/
Std.ExtDHashMap.Const.getD : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} → {β : Type v} → [EquivBEq α] → [LawfulHashable α] → (Std.ExtDHashMap α fun x => β) → α → β → β
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.indicator : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β],
  MeasureTheory.StronglyMeasurable f → ∀ {s : Set α}, MeasurableSet s → MeasureTheory.StronglyMeasurable (s.indicator f)
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.Hom.match_1.eq_4 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D]
  (motive : CategoryTheory.Join C D → CategoryTheory.Join C D → Sort u_5) (a : D) (a_1 : C)
  (h_1 : (x y : C) → motive (CategoryTheory.Join.left x) (CategoryTheory.Join.left y))
  (h_2 : (x y : D) → motive (CategoryTheory.Join.right x) (CategoryTheory.Join.right y))
  (h_3 : (a : C) → (a_2 : D) → motive (CategoryTheory.Join.left a) (CategoryTheory.Join.right a_2))
  (h_4 : (a : D) → (a_2 : C) → motive (CategoryTheory.Join.right a) (CategoryTheory.Join.left a_2)),
  (match CategoryTheory.Join.right a, CategoryTheory.Join.left a_1 with
    | CategoryTheory.Join.left x, CategoryTheory.Join.left y => h_1 x y
    | CategoryTheory.Join.right x, CategoryTheory.Join.right y => h_2 x y
    | CategoryTheory.Join.left a, CategoryTheory.Join.right a_2 => h_3 a a_2
    | CategoryTheory.Join.right a, CategoryTheory.Join.left a_2 => h_4 a a_2) =
    h_4 a a_1
-- Mathlib.RingTheory.Smooth.Fiber
/-- Let `(R, m, k)` be a local ring, `S` be a local `R`-algebra that is flat,
essentially of finite presentation, and `k ⊗[R] S` is `k`-formally smooth.
Then `S` is `R`-formally smooth.

Since we don't have an "essentially of finite presentation" type class yet, we explicitly require a
`P` that is of finite presentation over `R` and that `S` is a localization of it.
 -/
Algebra.FormallySmooth.of_formallySmooth_residueField_tensor : ∀ {R : Type u_1} {S : Type u_2} {P : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Module.Flat R S] [inst_4 : CommRing P] [inst_5 : Algebra R P] [inst_6 : Algebra P S] [IsScalarTower R P S]
  [inst_8 : IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)]
  [Algebra.FormallySmooth (IsLocalRing.ResidueField R) (TensorProduct R (IsLocalRing.ResidueField R) S)]
  (M : Submonoid P) [IsLocalization M S] [Algebra.FinitePresentation R P], Algebra.FormallySmooth R S
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The universal factorization ring represents
`S ↦ "factorizations of p into (monic deg m) * (monic deg k) in S"`.  -/
Polynomial.UniversalFactorizationRing.homEquiv : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {n : ℕ} →
            (m k : ℕ) →
              (hn : n = m + k) →
                (p : Polynomial.MonicDegreeEq R n) →
                  (Polynomial.UniversalFactorizationRing m k hn p →ₐ[R] S) ≃
                    { q // ↑q.1 * ↑q.2 = Polynomial.map (algebraMap R S) ↑p }
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the composition of the two given morphisms is zero  -/
CategoryTheory.ShortComplex.zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (self : CategoryTheory.ShortComplex C), CategoryTheory.CategoryStruct.comp self.f self.g = 0
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_insert : ∀ {α : Type u} {s : Set α} {a : α}, a ∉ s → Cardinal.mk ↑(insert a s) = Cardinal.mk ↑s + 1
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasStrictFDerivAt.add` -/
HasStrictFDerivAt.fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt g g' x → HasStrictFDerivAt (fun i => f i + g i) (f' + g') x
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit.match_3.eq_1 : ∀ {n : ℕ}
  (motive :
    Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) ×
        Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Bool →
      Sort u_1)
  (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (foundContradiction : Bool)
  (h_1 :
    (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
      (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
        (foundContradiction : Bool) → motive (units, assignments, foundContradiction)),
  (match (units, assignments, foundContradiction) with
    | (units, assignments, foundContradiction) => h_1 units assignments foundContradiction) =
    h_1 units assignments foundContradiction
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.brecOn.eq : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : L.Term α → Sort u_1} (t : L.Term α)
  (F_1 : (t : L.Term α) → FirstOrder.Language.Term.below t → motive t),
  FirstOrder.Language.Term.brecOn t F_1 = F_1 t (FirstOrder.Language.Term.brecOn.go t F_1).2
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- **Alias** of `DyckWord.numNodes_toTree`. -/
DyckWord.semilength_eq_numNodes_equivTree : ∀ (p : DyckWord), p.toTree.numNodes = p.semilength
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.mem_conductorSet_iff : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {x : ℕ},
  x ∈ χ.conductorSet ↔ χ.FactorsThrough x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → t.maxKey? = t_1.maxKey?
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
/-- The multilinear map that takes `ι`-indexed elements of `M` and
returns their symmetric tensor power. Denoted `⨂ₛ[R] i, f i`.  -/
SymmetricPower.«term⨂ₛ[_]_,_» : Lean.ParserDescr
-- Mathlib.Topology.Category.LightProfinite.Limits
/-- A one-element space is terminal in `Profinite`  -/
LightProfinite.isTerminalPUnit : CategoryTheory.Limits.IsTerminal (LightProfinite.of PUnit.{u + 1})
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
toAdd_multiset_sum : ∀ {M : Type u_3} [inst : AddCommMonoid M] (s : Multiset (Multiplicative M)),
  Multiplicative.toAdd s.prod = (Multiset.map (⇑Multiplicative.toAdd) s).sum
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- `qrSign` is symmetric when both arguments are odd.  -/
qrSign.symm : ∀ {m n : ℕ}, Odd m → Odd n → qrSign m n = qrSign n m
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.dz_val : ∀ {a : ℕ} (a1 : 1 < a), ↑(Pell.d✝ a1) = Pell.az a * Pell.az a - 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : StarRing R}
  {inst_2 : MetricSpace R} {inst_3 : IsTopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A}
  {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A}
  [self : ClosedEmbeddingContinuousFunctionalCalculus R A p], ContinuousFunctionalCalculus R A p
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to infinity along a nontrivial filter,
`fun x ↦ f x * r` tends to negative infinity if and only if `r < 0`.  -/
Filter.tendsto_mul_const_atBot_iff_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atTop → (Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ r < 0)
-- Batteries.Data.ByteSlice
_private.Batteries.Data.ByteSlice.0.ByteSlice.size.eq_1 : ∀ (s : ByteSlice), s.size = s.stop - s.start
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CStarAlgebra.linear_combination_nonneg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℂ A] [inst_2 : SMulCommClass ℂ A A]
  [inst_3 : IsScalarTower ℂ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A] [inst_6 : StarModule ℂ A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (x : A),
  (↑(realPart x))⁺ - (↑(realPart x))⁻ + (Complex.I • (↑(imaginaryPart x))⁺ - Complex.I • (↑(imaginaryPart x))⁻) = x
-- Init.Data.Array.Lemmas
Array.reverse_append : ∀ {α : Type u_1} {xs ys : Array α}, (xs ++ ys).reverse = ys.reverse ++ xs.reverse
-- Init.Data.Array.Subarray
/-- Returns a subarray of an array, with the given bounds.

If `start` or `stop` are not valid bounds for a subarray, then they are clamped to array's size.
Additionally, the starting index is clamped to the ending index.
 -/
Array.toSubarray : {α : Type u} → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → Subarray α
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.IsBipartiteWith.disjoint : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → Disjoint s t
-- Mathlib.Data.List.Perm.Subperm
List.Subperm.append : ∀ {α : Type u_1} {l₁ l₂ r₁ r₂ : List α}, l₁.Subperm l₂ → r₁.Subperm r₂ → (l₁ ++ r₁).Subperm (l₂ ++ r₂)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `g` and `h` commute, then `g` moves `h +ᵥ x` iff `g` moves `x`.
This is equivalent to say that the set `(fixedBy α g)ᶜ` is fixed by `h`.  -/
AddAction.movedBy_mem_fixedBy_of_addCommute : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g h : G},
  AddCommute g h → (AddAction.fixedBy α g)ᶜ ∈ AddAction.fixedBy (Set α) h
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.degree_U_natCast : ∀ (R : Type u_1) [inst : CommRing R] [IsDomain R] [NeZero 2] (n : ℕ), (Polynomial.Chebyshev.U R ↑n).degree = ↑n
-- Mathlib.RepresentationTheory.Invariants
Representation.le_comap_invariants : ∀ {k : Type u_1} {G : Type u_2} [inst : CommRing k] [inst_1 : Group G] {V : Type u_5} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] (g : G),
  Representation.invariants (MonoidHom.comp ρ S.subtype) ≤
    Submodule.comap (ρ g) (Representation.invariants (MonoidHom.comp ρ S.subtype))
-- Mathlib.MeasureTheory.Integral.Marginal
/-- Peel off a single integral from a `lmarginal` integral at the beginning (compare with
`lmarginal_insert'`, which peels off an integral at the end).  -/
MeasureTheory.lmarginal_insert : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] {s : Finset δ} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] (f : ((i : δ) → X i) → ENNReal),
  Measurable f →
    ∀ {i : δ},
      i ∉ s →
        ∀ (x : (i : δ) → X i), (∫⋯∫⁻_insert i s, f ∂μ) x = ∫⁻ (xᵢ : X i), (∫⋯∫⁻_s, f ∂μ) (Function.update x i xᵢ) ∂μ i
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The map `Fin (n + 1 + 1) → C` which "shifts" `F.obj'` to the right and inserts `X` in
the zeroth position.  -/
CategoryTheory.ComposableArrows.Precomp.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} → CategoryTheory.ComposableArrows C n → C → Fin (n + 1 + 1) → C
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_monotoneOn : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  MonotoneOn ArchimedeanClass.mk (Set.Iic 0)
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.instReflectsLimitsOfShapeFunctorObjWhiskeringRightOfHasLimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J E]
  (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsLimitsOfShape J F],
  CategoryTheory.Limits.ReflectsLimitsOfShape J ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
-- Mathlib.RingTheory.Artinian.Module
/-- The quotient of a commutative Artinian ring by a power of its nilradical is isomorphic to
a finite product of local rings, namely the quotients by the powers of the maximal ideals.  -/
IsArtinianRing.quotNilradicalPowEquivPi : (R : Type u_1) →
  [inst : CommRing R] →
    [IsArtinianRing R] → (n : ℕ) → (R ⧸ nilradical R ^ n) ≃ₐ[R] (I : MaximalSpectrum R) → R ⧸ I.asIdeal ^ n
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
LinearMap.range_localizedMap_eq_localized₀_range : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] {P : Type u_5} [inst_6 : AddCommMonoid P] [inst_7 : Module R P] {Q : Type u_6}
  [inst_8 : AddCommMonoid Q] [inst_9 : Module R Q] (f' : P →ₗ[R] Q) [inst_10 : IsLocalizedModule p f'] (g : M →ₗ[R] P),
  ((IsLocalizedModule.map p f f') g).range = Submodule.localized₀ p f' g.range
-- Init.Data.BitVec.Lemmas
BitVec.add_ofFin : ∀ {n : ℕ} (x : BitVec n) (y : Fin (2 ^ n)), x + { toFin := y } = { toFin := x.toFin + y }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α} {k : α} {fallback : Unit},
  Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.Const.unitOfList l) k fallback = ()
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse.  -/
EuclideanGeometry.dist_div_sin_oangle_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → dist p₃ p₂ / (EuclideanGeometry.oangle p₃ p₁ p₂).sin = dist p₁ p₃
-- Mathlib.RingTheory.Kaehler.Basic
instInhabitedKaehlerDifferential : (R : Type u_2) →
  (S : Type u_1) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Inhabited Ω[S⁄R]
-- Mathlib.Topology.Algebra.Module.PerfectSpace
instPerfectSpace : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜], PerfectSpace 𝕜
-- Mathlib.Topology.NhdsKer
nhdsKer_empty : ∀ {X : Type u_2} [inst : TopologicalSpace X], nhdsKer ∅ = ∅
-- Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
/-- The embedding of `X` into the free algebra with coefficients in `R`.  -/
FreeNonUnitalNonAssocAlgebra.of : (R : Type u_1) → {X : Type u_2} → [inst : Semiring R] → X → FreeNonUnitalNonAssocAlgebra R X
-- Mathlib.Algebra.Group.Subgroup.Map
/-- The image of an `AddSubgroup` along an `AddMonoid` homomorphism
is an `AddSubgroup`.  -/
AddSubgroup.map : {G : Type u_1} → [inst : AddGroup G] → {N : Type u_5} → [inst_1 : AddGroup N] → (G →+ N) → AddSubgroup G → AddSubgroup N
-- Mathlib.Algebra.Ring.Prod
Prod.instNonUnitalNonAssocRing : {R : Type u_1} → {S : Type u_3} → [NonUnitalNonAssocRing R] → [NonUnitalNonAssocRing S] → NonUnitalNonAssocRing (R × S)
-- Mathlib.Analysis.Complex.Basic
/-- **Alias** of `Complex.uniformContinuous_re`. -/
Complex.uniformlyContinuous_re : UniformContinuous Complex.re
-- Mathlib.Tactic.PNatToNat
Mathlib.Tactic.PNatToNat.sub_coe : ∀ (a b : ℕ+), ↑(a - b) = ↑a - 1 - ↑b + 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constMinEntry!_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited (α × β)],
  t₁.WF →
    t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Internal.Impl.Const.minEntry! t₁ = Std.DTreeMap.Internal.Impl.Const.minEntry! t₂
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionUnitIso`, the structural isomorphism `𝟙_ C ⊙ₗ - ≅ -`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.«termλₗ» : Lean.ParserDescr
-- Mathlib.Algebra.Ring.BooleanRing
toBoolAlg_symm_eq : ∀ {α : Type u_1}, toBoolAlg.symm = ofBoolAlg
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparated_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.QuasiSeparated f]
  [AlgebraicGeometry.QuasiSeparated g], AlgebraicGeometry.QuasiSeparated (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Algebra.Operations
SubMulAction.mem_one' : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A},
  x ∈ 1 ↔ ∃ y, (algebraMap R A) y = x
-- Init.Data.Nat.Lemmas
Nat.mul_sub_div_of_dvd : ∀ {b c : ℕ}, c ≠ 0 → c ∣ b → ∀ (a : ℕ), (c * a - b) / c = a - b / c
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.instOne : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → One (SpecialLinearGroup R V)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
spectrum_imaginaryPart : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) spectrum_imaginaryPart._auto_1 →
    spectrum ℂ ↑(imaginaryPart a) = (fun x => ↑x.im) '' spectrum ℂ a
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instVAddSubtypeMem : {R : Type u} → {M : Type v} → [inst : VAdd R M] → (p : SubAddAction R M) → VAdd R ↥p
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatNatCiOfNatInt : Lean.Grind.ToInt.OfNat ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.liftp_iff : ∀ {F : Type u → Type v} [q : QPF F] {α : Type u} (p : α → Prop) (x : F α),
  Functor.Liftp p x ↔ ∃ a f, x = QPF.abs ⟨a, f⟩ ∧ ∀ (i : (QPF.P F).B a), p (f i)
-- Mathlib.Topology.Irreducible
preimage_mem_irreducibleComponents_of_isPreirreducible_fiber : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {t : Set X},
  t ∈ irreducibleComponents X →
    ∀ {f : Y → X},
      Continuous f →
        IsOpenMap f →
          (∀ (x : X), IsPreirreducible (f ⁻¹' {x})) → (t ∩ Set.range f).Nonempty → f ⁻¹' t ∈ irreducibleComponents Y
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.tr.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (d : Turing.Dir) (q : Λ),
  Turing.TM0to1.tr M (Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.move d) q) =
    Turing.TM1.Stmt.move d (Turing.TM1.Stmt.goto fun x x_1 => Turing.TM0to1.Λ'.normal q)
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticOnNhd.inv`

---

`(f x)⁻¹` is analytic away from `f x = 0`  -/
AnalyticOnNhd.fun_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E}, AnalyticOnNhd 𝕜 f s → (∀ x ∈ s, f x ≠ 0) → AnalyticOnNhd 𝕜 (fun i => (f i)⁻¹) s
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_def : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α},
  s / t = Finset.image (fun p => p.1 / p.2) (s ×ˢ t)
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.methodSpecsSimpExtension : Lean.Meta.SimpExtension
-- Init.Grind.Lemmas
Lean.Grind.beq_eq_true_of_eq : ∀ {α : Type u} {x : BEq α} {x_1 : LawfulBEq α} {a b : α}, a = b → (a == b) = true
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackMap_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {Y' Z' X' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'}
  [inst_2 : CategoryTheory.ChosenPullbacksAlong g'] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X}
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f' γ₃ = CategoryTheory.CategoryStruct.comp γ₁ f)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_fst._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp g' γ₃ = CategoryTheory.CategoryStruct.comp γ₂ g)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_fst._auto_3),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂)
      (CategoryTheory.ChosenPullbacksAlong.fst f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst f' g') γ₁
-- Batteries.Data.List.Lemmas
List.findIdxs_cons : ∀ {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} {s : ℕ},
  List.findIdxs p (x :: xs) s = if p x = true then s :: List.findIdxs p xs (s + 1) else List.findIdxs p xs (s + 1)
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_of_le_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, a ≤ b → ¬IsMin a → Order.pred a < b