mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₁ → (t₁ ∪ t₂)[k]! = t₂[k]!
-- Mathlib.Algebra.Group.TypeTags.Basic
toAdd_inv : ∀ {α : Type u} [inst : Neg α] (x : Multiplicative α), Multiplicative.toAdd x⁻¹ = -Multiplicative.toAdd x
-- Mathlib.Probability.IdentDistrib
MeasureTheory.AEStronglyMeasurable.identDistrib_mk : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α}
  {f : α → γ} [inst_2 : TopologicalSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [BorelSpace γ]
  (hf : MeasureTheory.AEStronglyMeasurable f μ),
  ProbabilityTheory.IdentDistrib f (MeasureTheory.AEStronglyMeasurable.mk f hf) μ μ
-- Mathlib.Order.BooleanAlgebra.Basic
codisjoint_iff_compl_le_right : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], Codisjoint x y ↔ xᶜ ≤ y
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- A non-unital subsemiring is a non-unital `ℕ`-subalgebra.  -/
nonUnitalSubalgebraOfNonUnitalSubsemiring : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → NonUnitalSubsemiring R → NonUnitalSubalgebra ℕ R
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.tryAssignUnassigned.go : Lean.Expr → Lean.Expr → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.Logic.Function.Basic
Function.swap_le : ∀ {α : Type u_4} [inst : LE α], (Function.swap fun x1 x2 => x1 ≤ x2) = fun x1 x2 => x1 ≥ x2
-- Mathlib.Topology.Algebra.Group.Pointwise
IsDiscrete.exists_nhds_eq_one_of_image_mulLeft_inter_nonempty : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (S : Subgroup G),
  IsDiscrete ↑S → ∃ U ∈ nhds 1, U⁻¹ = U ∧ ∀ g ∈ S, ((fun x => g * x) '' U ∩ U).Nonempty → g = 1
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The index of the root `2α + β` where `α` is the short root and `β` is the long root.  -/
RootPairing.EmbeddedG2.twoShortAddLong : {ι : 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.EmbeddedG2] → ι
-- Mathlib.Topology.Bases
/-- **Alias** of the reverse direction of `TopologicalSpace.isSeparable_closure`. -/
TopologicalSpace.IsSeparable.closure : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set α},
  TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable (closure s)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- More flexible variant of `mapComp`. (See `Bicategory.Functor.Strict`
for applications to strict bicategories.)  -/
CategoryTheory.OplaxFunctor.mapComp' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.OplaxFunctor B C) →
          {b₀ b₁ b₂ : B} →
            (f : b₀ ⟶ b₁) →
              (g : b₁ ⟶ b₂) →
                (fg : b₀ ⟶ b₂) →
                  autoParam (CategoryTheory.CategoryStruct.comp f g = fg) CategoryTheory.OplaxFunctor.mapComp'._auto_1 →
                    (F.map fg ⟶ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g))
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.comul_algebraMap : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (r : R),
  CoalgebraStruct.comul ((algebraMap R A) r) = (algebraMap R (TensorProduct R A A)) r
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.invalid.sizeOf_spec : sizeOf ByteArray.utf8DecodeChar?.FirstByte.invalid = 1
-- Mathlib.Algebra.Order.Monoid.TypeTags
Multiplicative.canonicallyOrderedMul : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α],
  CanonicallyOrderedMul (Multiplicative α)
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.anchor_derivation : ∀ {R : Type u_1} {A₁ : Type u_2} [inst : CommRing R] [inst_1 : CommRing A₁] [inst_2 : Algebra R A₁],
  LieRinehartAlgebra.anchor R A₁ (Derivation R A₁ A₁) = LieRinehartAlgebra.Hom.id
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α} {fallback : β a} {c : ℕ},
  (Std.DHashMap.emptyWithCapacity c).getD a fallback = fallback
-- Mathlib.Data.EReal.Operations
EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal : ∀ (x : ℝ), ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal
-- Mathlib.RingTheory.Unramified.Locus
Algebra.unramifiedLocus_eq_univ_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.unramifiedLocus R A = Set.univ ↔ Algebra.FormallyUnramified R A
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
ModularForm.E₆_qExpansion_coeff_one : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₆) = -504
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.hasRightHomology_of_preserves : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [S.HasRightHomology]
  [F.PreservesRightHomologyOf S], (S.map F).HasRightHomology
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the first morphism in a triangle morphism  -/
CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂ → (T₁.obj₁ ⟶ T₂.obj₁)
-- Mathlib.RingTheory.NormalClosure
Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S],
  IsScalarTower R (Ring.NormalClosure R S)
    ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_filter_containsKey_le : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₂ →
    Std.Internal.List.DistinctKeys l₁ →
      (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁).length ≤ l₂.length
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.peek'.eq_1 : ∀ (k : Turing.PartrecToTM2.K'), Turing.PartrecToTM2.peek' k = Turing.TM2.Stmt.peek k fun x v => v
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
AlgebraicTopology.DoldKan.hσ'_eq' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {q n a : ℕ} (ha : n = a + q),
  AlgebraicTopology.DoldKan.hσ' q n (n + 1) ⋯ = (-1) ^ a • X.σ ⟨a, ⋯⟩
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.setInsert : (self : ShareCommon.StateFactoryImpl) → self.Set → ShareCommon.Object → self.Set
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input.sizeOf_spec : ∀ (p : Lean.Grind.CommRing.Poly), sizeOf (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input p) = 1 + sizeOf p
-- Init.Data.Array.Lemmas
Array.empty_eq_append_iff : ∀ {α : Type u_1} {xs ys : Array α}, #[] = xs ++ ys ↔ xs = #[] ∧ ys = #[]
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.instAddSubgroupClass : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroupClass (AddSubgroup G) G
-- Init.Data.Iterators.Consumers.Monadic.Access
Std.IterM.IsPlausibleNthOutputStep.brecOn : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β]
  {motive :
    (a : ℕ) →
      (a_1 : Std.IterM m β) →
        (a_2 : Std.IterStep (Std.IterM m β) β) → Std.IterM.IsPlausibleNthOutputStep a a_1 a_2 → Prop}
  {a : ℕ} {a_1 : Std.IterM m β} {a_2 : Std.IterStep (Std.IterM m β) β}
  (t : Std.IterM.IsPlausibleNthOutputStep a a_1 a_2),
  (∀ (a : ℕ) (a_3 : Std.IterM m β) (a_4 : Std.IterStep (Std.IterM m β) β)
      (t : Std.IterM.IsPlausibleNthOutputStep a a_3 a_4),
      Std.IterM.IsPlausibleNthOutputStep.below t → motive a a_3 a_4 t) →
    motive a a_1 a_2 t
-- Batteries.Tactic.Lint.Misc
/-- A linter for checking theorem doc strings.  -/
Batteries.Tactic.Lint.docBlameThm : Batteries.Tactic.Lint.Linter
-- Mathlib.Algebra.Group.AddChar
AddChar.one_eq_zero : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M], 1 = 0
-- Std.Http.Data.URI.Basic
Std.Http.URI.Builder.mk.sizeOf_spec : ∀ (scheme : Option Std.Http.URI.Scheme) (userInfo : Option Std.Http.URI.UserInfo) (host : Option Std.Http.URI.Host)
  (port : Std.Http.URI.Port) (pathSegments : Array String) (query : Array (String × Option String))
  (fragment : Option String),
  sizeOf
      { scheme := scheme, userInfo := userInfo, host := host, port := port, pathSegments := pathSegments,
        query := query, fragment := fragment } =
    1 + sizeOf scheme + sizeOf userInfo + sizeOf host + sizeOf port + sizeOf pathSegments + sizeOf query +
      sizeOf fragment
-- Std.Data.Internal.List.Associative
Std.Internal.List.alterKey.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k : α) (f f_1 : Option (β k) → Option (β k)),
  f = f_1 →
    ∀ (l l_1 : List ((a : α) × β a)), l = l_1 → Std.Internal.List.alterKey k f l = Std.Internal.List.alterKey k f_1 l_1
-- Mathlib.Algebra.Group.Defs
/-- Any `AddLeftCancelSemigroup` satisfies `IsLeftCancelAdd`.  -/
AddLeftCancelSemigroup.toIsLeftCancelAdd : ∀ {G : Type u} [self : AddLeftCancelSemigroup G], IsLeftCancelAdd G
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_eq_bot : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} [IsReduced R] {n : ℕ}, n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instIsCentralScalar : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_2} [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : PseudoMetricSpace β] [inst_3 : Zero 𝕜] [inst_4 : Zero β] [inst_5 : SMul 𝕜 β] [inst_6 : IsBoundedSMul 𝕜 β]
  [inst_7 : SMul 𝕜ᵐᵒᵖ β] [inst_8 : IsCentralScalar 𝕜 β], IsCentralScalar 𝕜 (BoundedContinuousFunction α β)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_refl_left : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} (g' : α → F') (l : Filter α), (fun x => f' x - f' x) =O[l] g'
-- Mathlib.Analysis.Real.Spectrum
SpectrumRestricts.nnreal_iff : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] {a : A},
  SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.instInhabitedMorApplication.default : Mathlib.Meta.FunProp.MorApplication
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- `G.IndepSetFree n` means that `G` has no `n`-independent sets.  -/
SimpleGraph.IndepSetFree : {α : Type u_1} → SimpleGraph α → ℕ → Prop
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instAddZeroClassQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : SMul S M] → [inst_1 : AddZeroClass M] → (c : ModuleCon S M) → AddZeroClass (ModuleCon.Quotient M c)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
AlgebraicTopology.DoldKan.N₂_map_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)} (f : X ⟶ Y) (i : ℕ),
  (AlgebraicTopology.DoldKan.N₂.map f).f.f i =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f i) (f.f.app (Opposite.op { len := i }))
-- Mathlib.Order.Filter.Prod
Filter.prod_assoc_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Filter α) (g : Filter β) (h : Filter γ),
  Filter.map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
-- Lean.Meta.HaveTelescope
Lean.Meta.ZetaUnusedMode.no.sizeOf_spec : sizeOf Lean.Meta.ZetaUnusedMode.no = 1
-- Mathlib.GroupTheory.Index
Subgroup.finiteIndex_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.FiniteIndex ↔ H.index ≠ 0
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.IsGeneratedBy.generatedBy_eq`. -/
eq_deltaGenerated : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y}
  [Topology.IsGeneratedBy X Y], TopologicalSpace.generatedBy X = tY
-- Mathlib.Data.ENat.Lattice
ENat.iInf_eq_zero : ∀ {ι : Sort u_1} {f : ι → ℕ∞}, ⨅ i, f i = 0 ↔ ∃ i, f i = 0
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.map_not_measurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {M : Type u_3}
  [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) {f : α → β},
  ¬Measurable f → v.map f = 0
-- Init.Data.String.Lemmas.Pattern.Memcmp
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.Internal.memcmpStr.go.induct_unfolding : ∀ (lhs rhs : String) (lstart rstart len : String.Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos)
  (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) (motive : String.Pos.Raw → Bool → Prop),
  (∀ x < len,
      ∀ (hl : x.offsetBy lstart < lhs.rawEndPos) (hr : x.offsetBy rstart < rhs.rawEndPos),
        (lhs.getUTF8Byte (x.offsetBy lstart) hl == rhs.getUTF8Byte (x.offsetBy rstart) hr) = true →
          motive x.inc (String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 x.inc) →
            motive x (String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 x.inc)) →
    (∀ x < len,
        ∀ (hl : x.offsetBy lstart < lhs.rawEndPos) (hr : x.offsetBy rstart < rhs.rawEndPos),
          ¬(lhs.getUTF8Byte (x.offsetBy lstart) hl == rhs.getUTF8Byte (x.offsetBy rstart) hr) = true → motive x false) →
      (∀ (x : String.Pos.Raw), ¬x < len → motive x true) →
        ∀ (curr : String.Pos.Raw),
          motive curr (String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 curr)
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.instCategory : (R : Type u) → [inst : Ring R] → CategoryTheory.Category.{u, u} (FGModuleRepr R)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.isUnit_inr_iff : ∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Semiring R] [inst_2 : Module Rᵐᵒᵖ M] [inst_3 : Module R M]
  [inst_4 : SMulCommClass R Rᵐᵒᵖ M] {m : M}, IsUnit (TrivSqZeroExt.inr m) ↔ Subsingleton R
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.logEmbeddingQuot_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : (NumberField.RingOfIntegers K)ˣ),
  (NumberField.Units.logEmbeddingQuot K) (Additive.ofMul ↑x) = (NumberField.Units.logEmbedding K) (Additive.ofMul x)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₂'_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.ShortComplex.SnakeInput.functorL₂'.obj S = S.L₂'
-- Mathlib.GroupTheory.OrderOfElement
Function.Injective.isOfFinAddOrder_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] {x : G} [inst_1 : AddMonoid H] {f : G →+ H},
  Function.Injective ⇑f → (IsOfFinAddOrder (f x) ↔ IsOfFinAddOrder x)
-- Std.Sync.CancellationToken
/-- Consumers that are blocked waiting for cancellation.
- -/
Std.CancellationToken.State.consumers : Std.CancellationToken.State → Std.Queue Std.CancellationToken.Consumer
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Linear maps `(n → R) →ₗ[R] (m → R)` are linearly equivalent to `Matrix m n R`.  -/
LinearMap.toMatrix' : {R : Type u_1} →
  [inst : CommSemiring R] →
    {m : Type u_4} → {n : Type u_5} → [DecidableEq n] → [Fintype n] → ((n → R) →ₗ[R] m → R) ≃ₗ[R] Matrix m n R
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- The characteristic function of a Gaussian measure `μ` has value
`exp (μ[L] * I - Var[L; μ] / 2)` at `L : Dual ℝ E`.  -/
ProbabilityTheory.IsGaussian.charFunDual_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] (L : StrongDual ℝ E),
  MeasureTheory.charFunDual μ L =
    Complex.exp ((∫ (x : E), ↑(L x) ∂μ) * Complex.I - ↑(ProbabilityTheory.variance (⇑L) μ) / 2)
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Std.IterStep.successor.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Std.IterStep α β → Sort u_3) →
      (x : Std.IterStep α β) →
        ((it : α) → (out : β) → motive (Std.IterStep.yield it out)) →
          ((it : α) → motive (Std.IterStep.skip it)) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Data.List.Perm.Subperm
/-- **Alias** of the reverse direction of `List.map_subperm_map_iff`. -/
List.Subperm.map : ∀ {α : Type u_2} {β : Type u_3} {l₁ l₂ : List α} {f : α → β},
  Function.Injective f → l₁.Subperm l₂ → (List.map f l₁).Subperm (List.map f l₂)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_cpow_of_imp : ∀ {z w : ℂ}, (z = 0 → w.re = 0 → w = 0) → ‖z ^ w‖ = ‖z‖ ^ w.re / Real.exp (z.arg * w.im)
-- Init.Data.List.Erase
List.eraseP_eq_iff : ∀ {α : Type u_1} {l' : List α} {p : α → Bool} {l : List α},
  List.eraseP p l = l' ↔
    (∀ a ∈ l, ¬p a = true) ∧ l = l' ∨
      ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂
-- Init.Data.Bool
Bool.not_xor_not : ∀ (x y : Bool), (!x ^^ !y) = (x ^^ y)
-- Lean.Language.Lean.Types
/-- State after a command has been parsed.  -/
Lean.Language.Lean.CommandParsedSnapshot : Type
-- Mathlib.Combinatorics.SimpleGraph.Density
/-- Finset of edges of a relation between two finsets of vertices.  -/
SimpleGraph.interedges : {α : Type u_4} → (G : SimpleGraph α) → [DecidableRel G.Adj] → Finset α → Finset α → Finset (α × α)
-- Mathlib.Topology.UniformSpace.Separation
/-- Factoring functions to a separated space through the separation quotient.

TODO: unify with `SeparationQuotient.lift`.  -/
SeparationQuotient.lift' : {α : Type u} →
  {β : Type v} → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → [T0Space β] → (α → β) → SeparationQuotient α → β
-- Mathlib.RingTheory.Extension.Generators
/-- Transport generators along an algebra isomorphism.  -/
Algebra.Generators.ofAlgEquiv : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            Algebra.Generators R S ι →
              {T : Type u_1} → [inst_3 : CommRing T] → [inst_4 : Algebra R T] → (S ≃ₐ[R] T) → Algebra.Generators R T ι
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unopMap_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} (φ : S₁ ⟶ S₂), (CategoryTheory.ShortComplex.unopMap φ).τ₁ = φ.τ₃.unop
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.setFind? : (self : ShareCommon.StateFactoryBuilder) →
  {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → self.Set α → α → Option α
-- Mathlib.RingTheory.Polynomial.RationalRoot
/-- **Rational root theorem** part 1:
if `r : f.codomain` is a root of a polynomial over the ufd `A`,
then the numerator of `r` divides the constant coefficient  -/
num_dvd_of_is_root : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A]
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {p : Polynomial A} {r : K},
  (Polynomial.aeval r) p = 0 → IsFractionRing.num A r ∣ p.coeff 0
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.fun.inj : ∀ {depth depth_1 : ℕ}, Mathlib.Tactic.Conv.Path.fun depth = Mathlib.Tactic.Conv.Path.fun depth_1 → depth = depth_1
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linearMapAt_def_of_mem : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] {b : B}
  (hb : b ∈ e.baseSet), Bundle.Pretrivialization.linearMapAt R e b = ↑(Bundle.Pretrivialization.linearEquivAt R e b hb)
-- Mathlib.Order.WellFounded
WellFounded.not_leftTotal : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded (Function.swap r) → ∀ [Nonempty α], ¬Relator.LeftTotal r
-- Std.Data.DTreeMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.DTreeMap.Const.modify : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → (β → β) → Std.DTreeMap α (fun x => β) cmp
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.ExprWithAnchor.mk.inj : ∀ {e : Lean.Expr} {anchor : UInt64} {e_1 : Lean.Expr} {anchor_1 : UInt64},
  { e := e, anchor := anchor } = { e := e_1, anchor := anchor_1 } → e = e_1 ∧ anchor = anchor_1
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_of_mem_sInter : ∀ {x y z : ZFSet.{u_1}}, y ∈ x.sInter → z ∈ x → y ∈ z
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.mul_transpose_self_isDiag_iff_hasOrthogonalRows : ∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : Fintype n] [inst_1 : Mul α] [inst_2 : AddCommMonoid α]
  {A : Matrix m n α}, (A * A.transpose).IsDiag ↔ A.HasOrthogonalRows
-- Mathlib.CategoryTheory.Comma.Arrow
/-- We can also build a morphism in the arrow category out of any commutative square in `T`.  -/
CategoryTheory.Arrow.homMk' : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    {X Y : T} →
      {f : X ⟶ Y} →
        {P Q : T} →
          {g : P ⟶ Q} →
            (u : X ⟶ P) →
              (v : Y ⟶ Q) →
                autoParam (CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v)
                    CategoryTheory.Arrow.homMk'._auto_1 →
                  (CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.intersecting_insert : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α} {a : α},
  (insert a s).Intersecting ↔ s.Intersecting ∧ a ≠ ⊥ ∧ ∀ b ∈ s, ¬Disjoint a b
-- ProofWidgets.Data.Html
ProofWidgets.LayoutKind.block.sizeOf_spec : sizeOf ProofWidgets.LayoutKind.block = 1
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_comp_to_continuous_fun : ∀ {β : Type v} {γ : Type w} {δ : Type u_2} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace δ] [inst_3 : Zero δ] (f : ZeroAtInftyContinuousMap γ δ) (g : CocompactMap β γ),
  ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Init.Data.SInt.Lemmas
Int32.toBitVec_minValue : Int32.minValue.toBitVec = BitVec.intMin 32
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.cosKernel_neg : ∀ (a : UnitAddCircle) (x : ℝ), HurwitzZeta.cosKernel (-a) x = HurwitzZeta.cosKernel a x
-- Mathlib.Data.Setoid.Partition
IndexedPartition.instInhabitedQuotient : {ι : Type u_1} → {α : Type u_2} → {s : ι → Set α} → (hs : IndexedPartition s) → [Inhabited α] → Inhabited hs.Quotient
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.single_le_prod : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] {s : Multiset α} [IsOrderedMonoid α],
  (∀ x ∈ s, 1 ≤ x) → ∀ x ∈ s, x ≤ s.prod
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_inf_mul_relIndex : ∀ {G : Type u_1} [inst : Group G] (H K L : Subgroup G), H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
-- Std.Internal.Do.WP.Lemmas
EStateM.set.eq_1 : ∀ {ε σ : Type u} (s x : σ), EStateM.set s x = EStateM.Result.ok PUnit.unit s