mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.cofan_inj_naturality_symm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  (Φ : S₁ ⟶ S₂) {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  CategoryTheory.CategoryStruct.comp ((S₁.s.cofan Δ).inj A) (Φ.F.app Δ) =
    CategoryTheory.CategoryStruct.comp (Φ.f (Opposite.unop A.fst).len) ((S₂.s.cofan Δ).inj A)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β}
  (f : (a : α) → β a → Option (γ a)), m₁.Equiv m₂ → (Std.DHashMap.filterMap f m₁).Equiv (Std.DHashMap.filterMap f m₂)
-- Mathlib.Algebra.Order.Group.PartialSups
partialSups_mul_const : ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeSup α] [inst_1 : Group α] [inst_2 : Preorder ι]
  [inst_3 : LocallyFiniteOrderBot ι] [MulRightMono α] (f : ι → α) (c : α) (i : ι),
  (partialSups fun x => f x * c) i = (partialSups f) i * c
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.TheoremForm.uncurried.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.TheoremForm.uncurried = 1
-- Mathlib.ModelTheory.Types
/-- **Alias** of `FirstOrder.Language.Theory.CompleteType.setOfPred_subset_eq_empty_iff`. -/
FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_empty_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (S : (L.withConstants α).Theory),
  {p | S ⊆ ↑p} = ∅ ↔ ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.instLocallyBoundedMapClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β],
  LocallyBoundedMapClass (LocallyBoundedMap α β) α β
-- Mathlib.Data.NNReal.Defs
Real.nnabs_pos : ∀ {x : ℝ}, 0 < Real.nnabs x ↔ x ≠ 0
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.isShared.injEq : ∀ (x x_1 : Lean.IR.VarId), (Lean.IR.Expr.isShared x = Lean.IR.Expr.isShared x_1) = (x = x_1)
-- Mathlib.MeasureTheory.Constructions.Pi
/-- `OuterMeasure.pi m` is the finite product of the outer measures `{m i | i : ι}`.
It is defined to be the maximal outer measure `n` with the property that
`n (pi univ s) ≤ ∏ i, m i (s i)`, where `pi univ s` is the product of the sets
`{s i | i : ι}`.  -/
MeasureTheory.OuterMeasure.pi : {ι : Type u_1} →
  {α : ι → Type u_3} →
    [Fintype ι] → ((i : ι) → MeasureTheory.OuterMeasure (α i)) → MeasureTheory.OuterMeasure ((i : ι) → α i)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instIntCastCoeOfSubringClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Ring (R i)] →
              [∀ (i : ι), SubringClass (S i) (R i)] → IntCast (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.algebraMap_isUnit_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {x : R}, IsUnit ((algebraMap R S) x) ↔ ∃ m ∈ M, x ∣ m
-- Mathlib.Data.Multiset.Bind
Multiset.filterMap_join : ∀ {α : Type u_1} {β : Type v} (S : Multiset (Multiset α)) (f : α → Option β),
  Multiset.filterMap f S.join = (Multiset.map (Multiset.filterMap f) S).join
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instInhabited.eq_1 : ∀ {α : Type u_1} [inst : LE α], UpperSet.instInhabited = { default := ⊥ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (t.alter k f).isEmpty = false →
        ∀ {fallback : α},
          (t.alter k f).maxKeyD fallback = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Lean.Meta.SynthInstance
/-- Return `true` if a type of the form `(a_1 : A_1) → ... → (a_n : A_n) → B` has an unused argument `a_i`.

Remark: This is syntactic check and no reduction is performed.
 -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.SynthInstance.hasUnusedArguments : Lean.Expr → Bool
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.hasPushoutsAgainst_top_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.HasPushoutsAgainst ⊤ ↔ P.HasPushouts
-- Init.Prelude
Lean.Macro.instMonadRefMacroM : Lean.MonadRef Lean.MacroM
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.inter_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁ ∩ m₃).Equiv (m₂ ∩ m₃)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- For a function `f` and a measurable set `s`, the integral of `indicator s f`
over the whole space is equal to `∫ x in s, f x ∂μ` defined as `∫ x, f x ∂(μ.restrict s)`.  -/
MeasureTheory.integral_indicator : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet s → ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.Data.Nat.GCD.Basic
/-- If `k:ℕ` divides coprime `a` and `b` then `k = 1`  -/
Nat.eq_one_of_dvd_coprimes : ∀ {a b k : ℕ}, a.Coprime b → k ∣ a → k ∣ b → k = 1
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram.mk.sizeOf_spec : ∀ (diagram : CategoryTheory.Functor ℕᵒᵖ FintypeCat)
  (cone : CategoryTheory.Limits.Cone (diagram.comp FintypeCat.toProfinite))
  (isLimit : CategoryTheory.Limits.IsLimit cone),
  sizeOf { diagram := diagram, cone := cone, isLimit := isLimit } = 1 + sizeOf diagram + sizeOf cone + sizeOf isLimit
-- Std.Http.Protocol.H1
/-- Signals that the socket is not sending data anymore.
 -/
Std.Http.Protocol.H1.Machine.noMoreInput : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.RingTheory.Derivation.ToSquareZero
/-- Given a tower of algebras `R → A → B`, and a square-zero `I : Ideal B`,
there is a 1-1 correspondence between `R`-derivations from `A` to `I` and
lifts `A →ₐ[R] B` of the canonical map `A →ₐ[R] B ⧸ I`.  -/
derivationToSquareZeroEquivLift : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (I : Ideal B) →
                  [inst_5 : Algebra A B] →
                    I ^ 2 = ⊥ →
                      [inst_6 : IsScalarTower R A B] →
                        Derivation R A ↥I ≃
                          { f // (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I) }
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  k ∈ t → (cmp t.min! k).isLE = true
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_ofList_le : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  (Std.HashMap.Raw.ofList l).size ≤ l.length
-- Mathlib.Analysis.Complex.RemovableSingularity
/-- **Removable singularity** theorem, weak version. If `f : ℂ → E` is differentiable in a punctured
neighborhood of a point and is continuous at this point, then it is analytic at this point.  -/
Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ},
  (∀ᶠ (z : ℂ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℂ f z) → ContinuousAt f c → AnalyticAt ℂ f c
-- Mathlib.Computability.Primrec.List
/-- `List.modifyHead` by a primitive recursive function is primitive recursive.  -/
Primrec.list_modifyHead : ∀ {α : Type u_1} [inst : Primcodable α] {f : α → α}, Primrec f → Primrec (List.modifyHead f)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Ordering.then.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (a : Ordering) (h_1 : Unit → motive Ordering.eq) (h_2 : (a : Ordering) → motive a),
  (a = Ordering.eq → False) →
    (match a with
      | Ordering.eq => h_1 ()
      | a => h_2 a) =
      h_2 a
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_div : ∀ (a b : BitVec 16), { toBitVec := a / b } = { toBitVec := a } / { toBitVec := b }
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.run_seq.match_1.splitter : {ε σ α β : Type u_1} →
  (motive : EStateM.Result ε σ (α → β) → Sort u_2) →
    (x : EStateM.Result ε σ (α → β)) →
      ((g : α → β) → (s : σ) → motive (EStateM.Result.ok g s)) →
        ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) → motive x
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.utf8GetAux.match_1.eq_2 : ∀ (motive : List Char → String.Pos.Raw → String.Pos.Raw → Sort u_1) (c : Char) (cs : List Char) (i p : String.Pos.Raw)
  (h_1 : (x x_1 : String.Pos.Raw) → motive [] x x_1)
  (h_2 : (c : Char) → (cs : List Char) → (i p : String.Pos.Raw) → motive (c :: cs) i p),
  (match c :: cs, i, p with
    | [], x, x_1 => h_1 x x_1
    | c :: cs, i, p => h_2 c cs i p) =
    h_2 c cs i p
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.map.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (f : R →+* S),
  PowerSeries.map f = MvPowerSeries.map f
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.ConfigItem.prevRoot : Lean.Elab.ConfigEval.ConfigItem → Lean.Syntax
-- Mathlib.GroupTheory.Finiteness
/-- An additive group is finitely generated iff there exists a surjective homomorphism
from a `FreeAddGroup` on finitely many generators.  -/
AddGroup.fg_iff_exists_freeAddGroup_hom_surjective : ∀ {G : Type u_3} [inst : AddGroup G], AddGroup.FG G ↔ ∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_sub_eq_sum : ∀ {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ π : Ω → ℕ∞} [inst : AddCommGroup β],
  τ ≤ π →
    (∀ (ω : Ω), ↑(π ω) ≠ ⊤) →
      MeasureTheory.stoppedValue u π - MeasureTheory.stoppedValue u τ = fun ω =>
        (∑ i ∈ Finset.Ico (WithTop.untopA (τ ω)) (WithTop.untopA (π ω)), (u (i + 1) - u i)) ω
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hasSum_nat_sinKernel : ∀ (a : ℝ) {t : ℝ},
  0 < t →
    HasSum (fun n => 2 * ↑n * Real.sin (2 * Real.pi * a * ↑n) * Real.exp (-Real.pi * ↑n ^ 2 * t))
      (HurwitzZeta.sinKernel (↑a) t)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminators : Type
-- Mathlib.Order.SymmDiff
symmDiff_symmDiff_cancel_right : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), symmDiff (symmDiff b a) a = b
-- Mathlib.Probability.ProductMeasure
/-- Let `μ (i + 1) : Measure (X (i + 1))` be a measure. Up to an equivalence,
`μ i = ⨂ j : Ioc i (i + 1), μ i`, where `⊗` denotes the product of measures.  -/
MeasureTheory.Measure.map_piSingleton : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [∀ (n : ℕ), MeasureTheory.SigmaFinite (μ n)] (n : ℕ),
  MeasureTheory.Measure.map (⇑(MeasurableEquiv.piSingleton n)) (μ (n + 1)) = MeasureTheory.Measure.pi fun i => μ ↑i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mapArrowRight_left : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ : CategoryTheory.Arrow C₁}
  {f₃ f₃' : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom)
  (sq : f₃ ⟶ f₃'),
  (sq₁₃.mapArrowRight sq₁₃' sq).left = (G.obj (Opposite.op f₁.right)).map (CategoryTheory.Arrow.Hom.left sq)
-- Mathlib.Topology.Order.LawsonTopology
/-- A recursor for `WithLawson`. Use as `induction x`.  -/
Topology.WithLawson.rec : {α : Type u_1} →
  {β : Topology.WithLawson α → Sort u_2} →
    ((a : α) → β (Topology.WithLawson.toLawson a)) → (a : Topology.WithLawson α) → β a
-- Init.Meta.Defs
/-- Syntax that represents a sequence of `do` elements.
 -/
Lean.Syntax.DoSeq : Type
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is a separable field extension of exponential characteristic `q`, then
`F⟮a⟯ = F⟮a ^ q ^ n⟯` for any subset `a : E` and any natural number `n`.  -/
IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable' : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E] (a : E)
  (q : ℕ) [ExpChar F q] (n : ℕ), F⟮a⟯ = F⟮a ^ q ^ n⟯
-- Init.Data.UInt.Lemmas
UInt16.le_iff_toFin_le : ∀ {a b : UInt16}, a ≤ b ↔ a.toFin ≤ b.toFin
-- Mathlib.Order.Sublocale
Sublocale.ext_iff : ∀ {X : Type u_1} [inst : Order.Frame X] {S T : Sublocale X}, S = T ↔ ∀ (x : X), x ∈ S ↔ x ∈ T
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.fieldNotation : Lean.Option Bool
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.map_exp_comap_re_atBot : Filter.map Complex.exp (Filter.comap Complex.re Filter.atBot) = nhdsWithin 0 {0}ᶜ
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.homotopicRel_liftPath : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {γ₀ γ₁ : C(↑unitInterval, X)},
  γ₀.HomotopicRel γ₁ {0, 1} →
    ∀ (e : E) (h₀ : γ₀ 0 = p e) (h₁ : γ₁ 0 = p e), (cov.liftPath γ₀ e h₀).HomotopicRel (cov.liftPath γ₁ e h₁) {0, 1}
-- Mathlib.Algebra.Group.Hom.Basic
/-- If `f` is a monoid homomorphism to a commutative group, then `f⁻¹` is the homomorphism sending
`x` to `(f x)⁻¹`.  -/
MonoidHom.instInv : {M : Type u_2} → {G : Type u_5} → [inst : MulOneClass M] → [inst_1 : CommGroup G] → Inv (M →* G)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_ne_empty_iff : ∀ {m n : ℤ}, (m...n).toArray ≠ #[] ↔ m < n
-- Mathlib.Algebra.Free
FreeMagma.brecOn.go : {α : Type u} →
  {motive : FreeMagma α → Sort u_1} →
    (t : FreeMagma α) → ((t : FreeMagma α) → FreeMagma.below t → motive t) → motive t ×' FreeMagma.below t
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- If `m : ℕ` is coprime with `n`,
then the minimal polynomial of a primitive `n`-th root of unity `μ`
has `μ ^ m` as root.  -/
IsPrimitiveRoot.pow_isRoot_minpoly : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [IsDomain K] [CharZero K] {m : ℕ}, m.Coprime n → (Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.eq_one_or_self_of_dvd : ∀ {p : ℕ}, Nat.Prime p → ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- `AddMonoidAlgebra.single 0` as an `AlgHom`  -/
AddMonoidAlgebra.singleZeroAlgHom : {R : Type u_1} →
  {A : Type u_4} →
    {M : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : AddMonoid M] → A →ₐ[R] AddMonoidAlgebra A M
-- Mathlib.NumberTheory.PrimeCounting
/-- A linear upper bound on the size of the `primeCounting'` function  -/
Nat.primeCounting'_add_le : ∀ {a k : ℕ}, a ≠ 0 → a < k → ∀ (n : ℕ), (k + n).primeCounting' ≤ k.primeCounting' + a.totient * (n / a + 1)
-- Lean.Parser.Syntax
Lean.Parser.Command.optNamedName.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_const_left_of_ne : ∀ {α : Type u_1} {F : Type u_4} {E'' : Type u_9} [inst : Norm F] [inst_1 : NormedAddCommGroup E''] {g : α → F}
  {l : Filter α} {c : E''}, c ≠ 0 → ((fun _x => c) =o[l] g ↔ Filter.Tendsto (fun x => ‖g x‖) l Filter.atTop)
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.coe_measurableEquivPiIoc_apply : ∀ {ι : Type u_2} (b : ι → ℝ) (x : UnitAddTorus ι),
  (UnitAddTorus.measurableEquivPiIoc b) x = ⟨fun i => ↑((AddCircle.equivIoc 1 (b i)) (x i)), ⋯⟩
-- Lean.Parser.Do
Lean.Parser.Term.doIfProp.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The `AddSubgroup` generated by a set  -/
AddSubgroup.closure : {G : Type u_1} → [inst : AddGroup G] → Set G → AddSubgroup G
-- Mathlib.Analysis.InnerProductSpace.l2Space
OrthogonalFamily.linearIsometry.congr_simp : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V V_1 : (i : ι) → G i →ₗᵢ[𝕜] E}
  (e_V : V = V_1) (hV : OrthogonalFamily 𝕜 G V), hV.linearIsometry = ⋯.linearIsometry
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.rewrite?.diagnoseWhenNoIndex.unsafe_1 : Lean.Meta.SimpTheorem → Lean.Meta.SimpTheorem → Bool
-- Lean.Meta.Tactic.Revert
/-- Reverts all local declarations after `fvarId`.  -/
Lean.MVarId.revertAfter : Lean.MVarId → Lean.FVarId → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.Data.Finset.SDiff
Finset.insert_sdiff_self_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∈ s → insert a (s \ {a}) = s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableSemanticTokenType : Hashable Lean.Lsp.SemanticTokenType
-- Aesop.Search.Expansion
Aesop.runFirstSafeRule : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.GoalRef → Aesop.SearchM Q Aesop.SafeRulesResult
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.liftInitialSeg_toFun : ∀ (c : Cardinal.{u}), Cardinal.liftInitialSeg c = Cardinal.lift.{v, u} c
-- Lean.Meta.Sym.ExprPtr
_private.Lean.Meta.Sym.ExprPtr.0.Lean.Meta.Sym.isSameExpr.unsafe_1 : Lean.Expr → Lean.Expr → Bool
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.inj_left : ∀ {α : Type u_1} [inst : Mul α] [IsMulCommutative α] [inst_2 : PartialOrder α] {a b c : α},
  MulLECancellable c → (a * c = b * c ↔ a = b)
-- Mathlib.Data.Multiset.Replicate
Multiset.Nodup.pairwise : ∀ {α : Type u_1} {r : α → α → Prop} {s : Multiset α},
  (∀ a ∈ s, ∀ b ∈ s, a ≠ b → r a b) → s.Nodup → Multiset.Pairwise r s
-- Std.Http.Protocol.H1.Message
/-- Client perspective: writing outgoing requests and reading incoming responses.
 -/
Std.Http.Protocol.H1.Direction.sending : Std.Http.Protocol.H1.Direction
-- Mathlib.Tactic.Translate.Core
/-- The argument used to determine whether this constant should be translated.  -/
Mathlib.Tactic.Translate.TranslationInfo.relevantArg : Mathlib.Tactic.Translate.TranslationInfo → Mathlib.Tactic.Translate.RelevantArg
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `norm_nonneg`.  -/
hammingNorm_nonneg : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] {x : (i : ι) → β i}, 0 ≤ hammingNorm x
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] (U : ↑Y.affineOpens) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Scheme.Hom.normalization f ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).ι
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f) h) =
    CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).toSpecΓ
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map
          (CommRingCat.ofHom
            (integralClosure ↑(Y.presheaf.obj (Opposite.op ↑U))
                  ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ↑U)))).val.toRingHom))
        (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Hom.normalizationOpenCover f).f U) h))
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.smul_mem_iff : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : DivisionSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : SMul S R] [inst_5 : Module S M] [IsScalarTower S R M] (p : Submodule R M) {s : S}
  {x : M}, s ≠ 0 → (s • x ∈ p ↔ x ∈ p)
-- Mathlib.Data.Finset.Fold
Finset.fold_op_distrib : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {s : Finset α}
  {f g : α → β} {b₁ b₂ : β},
  Finset.fold op (op b₁ b₂) (fun x => op (f x) (g x)) s = op (Finset.fold op b₁ f s) (Finset.fold op b₂ g s)
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionParams.fromJson : Lean.Json → Except String Lean.Lsp.CodeActionParams
-- Mathlib.Algebra.Group.Hom.Defs
/-- Any type satisfying `AddHomClass` can be cast into `AddHom` via
`AddHomClass.toAddHom`.  -/
instCoeTCAddHomOfAddHomClass : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} →
      [inst : Add M] → [inst_1 : Add N] → [inst_2 : FunLike F M N] → [AddHomClass F M N] → CoeTC F (M →ₙ+ N)
-- Lean.Util.Recognizers
Lean.Expr.notNot? : Lean.Expr → Option Lean.Expr
-- Mathlib.Data.Nat.Factors
/-- `primeFactorsList n` is the prime factorization of `n`, listed in increasing order.  -/
Nat.primeFactorsList : ℕ → List ℕ
-- Mathlib.Analysis.Calculus.TangentCone.Pi
UniqueDiffWithinAt.univ_pi : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] [inst_3 : (i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)]
  [∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] {s : (i : ι) → Set (E i)} {x : (i : ι) → E i},
  (∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)) → UniqueDiffWithinAt 𝕜 (Set.univ.pi s) x
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.mul_one_sub_self : ∀ {R : Type u_1} {p : R} [inst : NonAssocRing R] [inst_1 : Star R], IsStarProjection p → p * (1 - p) = 0
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddZeroClass.eq_1 : ∀ {α : Type u_1} [inst : AddZeroClass α],
  OrderDual.instAddZeroClass =
    { toZero := OrderDual.instZero, toAdd := OrderDual.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.opEquiv_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A B : Cᵒᵖ) (g : Opposite.unop B ⟶ Opposite.unop A),
  (CategoryTheory.opEquiv A B).symm g = g.op
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The main induction in the proof of Chevalley's theorem for `R →+* R[X]`.
See the docstring of `induction_structure` for the overview.  -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.statement : ∀ {R₀ : Type u_1} {R : Type u_2} [inst : CommRing R₀] [inst_1 : CommRing R] [inst_2 : Algebra R₀ R] {n : ℕ}
  (S : ChevalleyThm.PolynomialC.InductionObj✝ R n), ChevalleyThm.PolynomialC.InductionObj.Statement✝ R₀ R n S
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.precompose : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes},
  c.IsColimit →
    ∀ {G : CategoryTheory.Functor J (Type w₀')} (e : (j : J) → G.obj j ≃ F.obj j)
      (naturality :
        ∀ {j j' : J} (f : j ⟶ j'),
          ⇑(e j') ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) =
            ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)),
      (c.precompose (fun {j'} => ⇑(e j')) ⋯).IsColimit