mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Injective
/-- Collects all components of a nested `And`, as projections.
(Avoids the binders that `MVarId.casesAnd` would introduce.)
 -/
_private.Lean.Meta.Injective.0.Lean.Meta.andProjections : Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜}, f₁ =ᶠ[nhds x] f → deriv f₁ =ᶠ[nhds x] deriv f
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_map_eq_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [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₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f → ∀ (p : Submodule R M), Submodule.comap f (Submodule.map f p) = p
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (n : ℤ) (X : C) {Z : C} (h : (t.truncLT n).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncLT n).map ((t.truncLTι n).app X)) h =
    CategoryTheory.CategoryStruct.comp ((t.truncLTι n).app ((t.truncLT n).obj X)) h
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.reindex_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'}
  (e : ι ≃ E.I₀) (a : ι), (E.reindex e).X a = E.X (e a)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` creates finite limits, then `F : C ⥤ Dᵒᵖ` creates finite
colimits.  -/
CategoryTheory.Limits.createsFiniteColimitsOfLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteLimits F.leftOp] → CategoryTheory.Limits.CreatesFiniteColimits F
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoX₂.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hf : S.f = 0),
  S.opcyclesIsoX₂ hf = S.opcyclesIsoX₂ hf
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticWith.severity? : {α : Type} → Lean.Lsp.DiagnosticWith α → Option Lean.Lsp.DiagnosticSeverity
-- Batteries.Tactic.Exact
/-- **Alias** of `Lean.MVarId.assignIfDefEq`.

---

`MetaM` version of `Lean.Elab.Tactic.evalExact`: add `mvarId := x` to the metavariable assignment.
This method wraps `Lean.MVarId.assign`, checking whether `mvarId` is already assigned, and whether
the expression has the right type.  -/
Lean.MVarId.assignIfDefeq : Lean.MVarId → Lean.Expr → Lean.MetaM Unit
-- Init.Data.Slice.Array.Lemmas
Subarray.size_mkSlice_rcc : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.size (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = min (hi + 1) (Std.Slice.size xs) - lo
-- Std.Sync.StreamMap
/-- Create a StreamMap from an array of named streams
 -/
Std.StreamMap.ofArray : {α β : Type} → [BEq α] → Array (α × Std.AnyAsyncStream β) → Std.StreamMap α β
-- Batteries.Util.ProofWanted
/-- Which flavour of wanted-declaration a `❰foo❱` reference resolved to. The accessor and
binder-name prefix depend on the *referenced* declaration's kind, not the enclosing command's.  -/
_private.Batteries.Util.ProofWanted.0.WantedRefKind : Type
-- Mathlib.Topology.Order.IsLUB
isLUB_of_mem_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {s : Set α} {a : α}
  {f : Filter α}, a ∈ upperBounds s → s ∈ f → ∀ [(f ⊓ nhds a).NeBot], IsLUB s a
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.instUnique : {R : Type u_1} → [inst : Field R] → Unique (PrimeSpectrum R)
-- Aesop.Forward.State
/-- The sources of all pattern substitutions present in the
`clusterStates`. Invariant: each pattern substitution in the cluster states
is associated with a nonempty set.  -/
Aesop.RuleState.patSubstSources : Aesop.RuleState → Lean.PHashMap Aesop.Substitution (Lean.PHashSet Aesop.PatSubstSource)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_ne_zero_iff : ∀ {x : ℝ}, Real.sin x ≠ 0 ↔ ∀ (n : ℤ), ↑n * Real.pi ≠ x
-- Batteries.Recycling.RBTree.WF
/-- The `append` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.append : ∀ {α : Type u_1} {cmp : α → α → Ordering} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp x v) l →
    RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp v x) r →
      RBTree.RBNode.Ordered cmp l → RBTree.RBNode.Ordered cmp r → RBTree.RBNode.Ordered cmp (l.append r)
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.repeat_eq_repeatTR.go : ∀ (α : Type u_1) (f : α → α) (init : α) (m n : ℕ),
  Nat.repeatTR.loop✝ f m (Nat.repeat f n init) = Nat.repeat f (m + n) init
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Sentence.realize_top : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M], M ⊨ ⊤
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_orbit_self : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] (a : α), a ∈ AddAction.orbit M a
-- Mathlib.Algebra.Divisibility.Basic
dvd_def : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b ↔ ∃ c, b = a * c
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instReprBodyState.repr : Std.Http.Protocol.H1.Reader.BodyState → ℕ → Std.Format
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_vlt_mul_of_vlt_of_vle : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {a b c d : R}, a <ᵥ b → c ≤ᵥ d → 0 <ᵥ d → a * c <ᵥ b * d
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.inter_ae_eq_right_of_ae_eq_univ : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s =ᵐ[μ] Set.univ → s ∩ t =ᵐ[μ] t
-- Init.Data.Vector.Basic
/-- Syntax for `Vector α n` 

Conventions for notations in identifiers:

 * The recommended spelling of `#v[]` in identifiers is `empty`.

 * The recommended spelling of `#v[x]` in identifiers is `singleton`. -/
Vector.«term#v[_,]» : Lean.ParserDescr
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.lowerCrossingTime_le : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ}
  {ω : Ω}, MeasureTheory.lowerCrossingTime a b f N n ω ≤ N
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.localizationAway_val : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S] (x : Unit),
  (Algebra.Generators.localizationAway S r).val x = IsLocalization.Away.invSelf r
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqAssignment : DecidableEq Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ι_D₃_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : ⋯ = j)
  [inst_23 : ⋯], ⋯
-- Mathlib.Order.Antisymmetrization
not_antisymmRel_of_gt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], b < a → ¬AntisymmRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
Prod.instLieAddGroup : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] [LieAddGroup I n G] {E' : Type u_5}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_10 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_11 : TopologicalSpace G'] [inst_12 : ChartedSpace H' G']
  [inst_13 : AddGroup G'] [LieAddGroup I' n G'], LieAddGroup (I.prod I') n (G × G')
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_nonneg : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α)
  (r : ℝ), 0 ≤ ↑(hf.stieltjesFunction a) r
-- Mathlib.Algebra.MvPolynomial.Basic
/-- See note [partially-applied ext lemmas].

We set the priority higher than that of `AddMonoidAlgebra.algHom_ext`.  -/
MvPolynomial.algHom_ext' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} {B : Type u_3} [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f g : MvPolynomial σ A →ₐ[R] B},
  f.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) = g.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) →
    (∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) → f = g
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_ofNat : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ) [inst_1 : n.AtLeastTwo], (OfNat.ofNat n).imJ = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Mathlib.Data.Set.Countable
/-- **Alias** of `Set.Countable.of_sdiff`. -/
Set.Countable.of_diff : ∀ {α : Type u} {s t : Set α}, (s \ t).Countable → t.Countable → s.Countable
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_inter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k (m₁.inter! m₂) =
          (Std.DTreeMap.Internal.Impl.contains k m₁ && Std.DTreeMap.Internal.Impl.contains k m₂)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.unitOfList_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {k : α}, Std.DHashMap.Const.unitOfList [k] = ∅.insertIfNew k ()
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.instAlgebraRing : {R : Type u_1} → [inst : CommRing R] → (P : StandardEtalePair R) → Algebra R P.Ring
-- Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
/-- The limit of the number of integral ideals of norm `≤ s` divided by `s` when `s → +∞`.
 -/
NumberField.Ideal.tendsto_norm_le_div_atTop : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Filter.Tendsto (fun s => ↑(Nat.card { I // ↑(Ideal.absNorm I) ≤ s }) / s) Filter.atTop
    (nhds
      (2 ^ NumberField.InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
            NumberField.Units.regulator K *
          ↑(NumberField.classNumber K) /
        (↑(NumberField.Units.torsionOrder K) * √|↑(NumberField.discr K)|)))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.eraseKey.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (x : List ((a : α) × β a)),
  Std.Internal.List.eraseKey k x =
    match x with
    | [] => []
    | ⟨k', v'⟩ :: l => bif k' == k then l else ⟨k', v'⟩ :: Std.Internal.List.eraseKey k l
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.polynomialY_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R},
  W'.polynomialY =
    MvPolynomial.C 2 * MvPolynomial.X 1 + MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 2 +
      MvPolynomial.C W'.a₃ * MvPolynomial.X 2 ^ 3
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of `SimpleGraph.Hom.minDegree_mono`. -/
SimpleGraph.Hom.minDegree_le : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableRel H.Adj] {f : G →g H},
  Function.Bijective ⇑f → G.minDegree ≤ H.minDegree
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
instOrderTopologyReal : OrderTopology ℝ
-- Mathlib.Data.TypeVec
TypeVec.prod.diag.eq_2 : ∀ (n : ℕ) (x_4 : TypeVec.{u} n.succ) (x_5 : x_4 Fin2.fz), TypeVec.prod.diag Fin2.fz x_5 = (x_5, x_5)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a}, (Std.ExtDHashMap.map f m).size = m.size
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_eq_of_lt : ∀ {a b : ℤ}, 0 ≤ a → a < b → a.tmod b = a
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.seq_eq : ∀ {α : Type u_1} {β : Type u_2} {m : ℕ} (f : Fin m → α → β) (v : Fin m → α), FinVec.seq f v = fun i => f i (v i)
-- Aesop.Tree.Data
Aesop.GoalData.isForcedUnprovable : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Bool
-- Lean.Parser.Types
Lean.Parser.FirstTokens.toOptional : Lean.Parser.FirstTokens → Lean.Parser.FirstTokens
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RioSliceData.mk : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → Std.Rio α → Std.DTreeMap.Internal.RioSliceData α β
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- An infinite place is unramified in a field extension if the restriction has the same multiplicity.
 -/
NumberField.InfinitePlace.IsUnramified : (k : Type u_1) →
  [inst : Field k] → {K : Type u_2} → [inst_1 : Field K] → [Algebra k K] → NumberField.InfinitePlace K → Prop
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.toCols₂_apply : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₂),
  A.toCols₂ i j = A i (Sum.inr j)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] [P.RespectsIso],
  P.diagonal.IsStableUnderBaseChange
-- Batteries.Data.List.Basic
/-- Optimized version of `product`.  -/
List.productTR : {α : Type u_1} → {β : Type u_2} → List α → List β → List (α × β)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_balanceL : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size),
  (Std.DTreeMap.Internal.Impl.balanceL k v l r hlb hrb hlr).size = l.size + 1 + r.size
-- Mathlib.Dynamics.PeriodicPts.Lemmas
/-- The backward direction of `minimalPeriod_eq_prime_iff`.  -/
Function.minimalPeriod_eq_prime : ∀ {α : Type u_1} {f : α → α} {x : α} {p : ℕ} [hp : Fact (Nat.Prime p)],
  Function.IsPeriodicPt f p x → ¬Function.IsFixedPt f x → Function.minimalPeriod f x = p
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_deleteEdges : ∀ {V : Type u_1} {G : SimpleGraph V} (s s' : Set (Sym2 V)), (G.deleteEdges s).deleteEdges s' = G.deleteEdges (s ∪ s')
-- Mathlib.Order.Ideal
Order.isIdeal_iff : ∀ {P : Type u_2} [inst : LE P] (I : Set P),
  Order.IsIdeal I ↔ IsLowerSet I ∧ I.Nonempty ∧ DirectedOn (fun x1 x2 => x1 ≤ x2) I
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The composition of the right maps in the associativity hexagon.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPost F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPrePre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPostPost' F)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.normalizedChainComplex_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} {T : C}
  {f g : (X.normalizedChainComplex R).X n ⟶ T},
  (∀ x ∈ X.nonDegenerate n,
      CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) f =
        CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) g) →
    f = g
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.toMLList.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Sort u_2) (a : α) (s' : Stream'.Seq α) (h_1 : Unit → motive none)
  (h_2 : (a : α) → (s' : Stream'.Seq α) → motive (some (a, s'))),
  (match some (a, s') with
    | none => h_1 ()
    | some (a, s') => h_2 a s') =
    h_2 a s'
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFiniteAt.eq_of_le_of_under_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P Q : Ideal S}
  [P.IsPrime] [inst_4 : Q.IsPrime], P ≤ Q → Ideal.under R P = Ideal.under R Q → ∀ [Algebra.QuasiFiniteAt R Q], P = Q
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- Given `t : X ×[S] Y`, it maps to `X` and `Y` with same image in `S`, yielding a
`Triplet f g`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} → {g : Y ⟶ S} → ↥(CategoryTheory.Limits.pullback f g) → AlgebraicGeometry.Scheme.Pullback.Triplet f g
-- Init.Data.Fin.Lemmas
/-- Restatement of `Fin.mk.injEq` as an `iff`.  -/
Fin.mk.inj_iff : ∀ {n a b : ℕ} {ha : a < n} {hb : b < n}, ⟨a, ha⟩ = ⟨b, hb⟩ ↔ a = b
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  ↑(Subalgebra.toSubmodule S) = ↑S
-- Mathlib.Algebra.Free
FreeAddSemigroup.length_map : ∀ {α : Type u} {β : Type v} (f : α → β) (x : FreeAddSemigroup α), ((FreeAddSemigroup.map f) x).length = x.length
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.toDataValue : Lean.LeanOptionValue → Lean.DataValue
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_filter_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool} {k k' : α},
  m.getKey? k = some k' →
    Std.DHashMap.Const.get? (Std.DHashMap.filter f m) k = Option.filter (fun x => f k' x) (Std.DHashMap.Const.get? m k)
-- Mathlib.Order.Interval.Basic
Interval.dual_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : BoundedOrder α], Interval.dual ⊤ = ⊤
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.hasTemperateGrowth_inner_right : ∀ {H : Type u_8} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℝ H] (c : H),
  Function.HasTemperateGrowth fun x => inner ℝ c x
-- Lean.LoadDynlib
_private.Lean.LoadDynlib.0.Lean.loadPlugin.unsafe_4 : Lean.Dynlib → BaseIO Lean.Dynlib
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticOnNhd.eval_mvPolynomial : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {σ : Type u_5} [CompleteSpace 𝕜] [inst_2 : Fintype σ]
  (p : MvPolynomial σ 𝕜), AnalyticOnNhd 𝕜 (fun x => (MvPolynomial.eval x) p) Set.univ
-- Mathlib.GroupTheory.Sylow
/-- The type of Sylow `p`-subgroups depends only on the prime factors of `p`.  -/
Sylow.equivProdPrimeFactors : {p : ℕ} → {G : Type u_1} → [inst : Group G] → p ≠ 0 → Sylow p G ≃ Sylow (p.primeFactors.prod id) G
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k k' : α},
  (k == k') = true →
    k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertManyIfNewUnit l).getKey? k' = some k
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.induction : ∀ {p : Ordinal.{u} → Prop} (i : Ordinal.{u}), (∀ (j : Ordinal.{u}), (∀ k < j, p k) → p j) → p i
-- Mathlib.RingTheory.Etale.Basic
/-- The localization of a formally étale map is formally étale.  -/
Algebra.FormallyEtale.localization_map : ∀ {R : Type u_2} {S : Type u_3} {Rₘ : Type u_4} {Sₘ : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing Rₘ] [inst_3 : CommRing Sₘ] (M : Submonoid R) [inst_4 : Algebra R S] [inst_5 : Algebra R Sₘ]
  [inst_6 : Algebra S Sₘ] [inst_7 : Algebra R Rₘ] [inst_8 : Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ]
  [IsScalarTower R S Sₘ] [IsLocalization M Rₘ] [IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ]
  [Algebra.FormallyEtale R S], Algebra.FormallyEtale Rₘ Sₘ
-- Init.Data.String.Substring
/-- Returns the first character in the substring.

If the substring is empty, but the substring's start position is a valid position in the underlying
string, then the character at the start position is returned. If the substring's start position is
not a valid position in the string, the fallback value `(default : Char)`, which is `'A'`, is
returned.  Does not panic.
 -/
Substring.Raw.front : Substring.Raw → Char
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  t.WF →
    ((Std.DTreeMap.Raw.filter f t).isEmpty = false ↔
      ∃ k, ∃ (h : k ∈ t), f (t.getKey k h) (Std.DTreeMap.Raw.Const.get t k h) = true)
-- Mathlib.Tactic.Polynomial.Basic
/-- Normalize a polynomial expression into standard form. Used by `polynomial_nf`.  -/
Mathlib.Tactic.Polynomial.evalExprPoly : Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result