mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.IsPrimary
Ideal.IsPrimary.inf : ∀ {R : Type u_1} [inst : CommSemiring R] {I J : Ideal R},
  I.IsPrimary → J.IsPrimary → I.radical = J.radical → (I ⊓ J).IsPrimary
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (l : List ((a : α) × β a)), (t₁.insertMany l).Equiv (t₂.insertMany l)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
Lean.Meta.Grind.Arith.Linear.isZeroInst : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr → Bool
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiable.clm_postcomp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {f : M → F₂ →L[𝕜] F₃},
  MDiff f → MDiff fun y => ContinuousLinearMap.postcomp F₁ (f y)
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev?_eq_none : ∀ {s : String.Slice} {p : s.Pos}, p = s.startPos → p.prev? = none
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.tr.match_1.splitter : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        (motive : Turing.TM2to1.Λ' K Γ Λ σ → Sort u_5) →
          (x : Turing.TM2to1.Λ' K Γ Λ σ) →
            ((q : Λ) → motive (Turing.TM2to1.Λ'.normal q)) →
              ((k : K) →
                  (s : Turing.TM2to1.StAct K Γ σ k) →
                    (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2to1.Λ'.go k s q)) →
                ((q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2to1.Λ'.ret q)) → motive x
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.coordChange_linear_comp : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i j k : ι),
  ∀ x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k, Z.coordChange j k x ∘SL Z.coordChange i j x = Z.coordChange i k x
-- Mathlib.Data.ENat.Lattice
ENat.finite_of_sSup_lt_top : ∀ {s : Set ℕ∞}, sSup s < ⊤ → s.Finite
-- Lean.Meta.Tactic.FVarSubst
/-- Constructs a substitution consisting of `s` followed by `t`.
This satisfies `(s.append t).apply e = t.apply (s.apply e)`
 -/
Lean.Meta.FVarSubst.append : Lean.Meta.FVarSubst → Lean.Meta.FVarSubst → Lean.Meta.FVarSubst
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.multisetSum_map_zero : ∀ {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Multiset α}, (∀ x ∈ s, f x ≡ 0 [MOD n]) → (Multiset.map f s).sum ≡ 0 [MOD n]
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instModule : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] →
                          {S : Type u_5} →
                            [inst_8 : Semiring S] →
                              [inst_9 : Module S F] →
                                [SMulCommClass 𝕜₂ S F] →
                                  [ContinuousConstSMul S F] →
                                    [inst_12 : IsTopologicalAddGroup F] → Module S (E →SWOT[σ] F)
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- For any element `x : A` and any set `B` in the submodule basis on `A`,
there is another basis element `B'` such that `B' * x` is in `B`.  -/
RingSubgroupsBasis.leftMul : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] {B : ι → AddSubgroup A},
  RingSubgroupsBasis B → ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(B i)
-- Mathlib.Computability.Language
Language.reverse.eq_1 : ∀ {α : Type u_1} (l : Language α), l.reverse = {w | w.reverse ∈ l}
-- Mathlib.SetTheory.Cardinal.Divisibility
Cardinal.prime_of_aleph0_le : ∀ {a : Cardinal.{u}}, Cardinal.aleph0 ≤ a → Prime a
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mem_closure : ∀ {K : Type u} [inst : DivisionRing K] {x : K} {s : Set K}, x ∈ Subfield.closure s ↔ ∀ (S : Subfield K), s ⊆ ↑S → x ∈ S
-- Mathlib.Order.Hom.Basic
OrderIso.orderEmbeddingCongr_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ]
  [inst_3 : LE δ] (f : α ≃o γ) (g : β ≃o δ) (h : α ↪o β),
  (f.orderEmbeddingCongr g) h = ((RelIso.toRelEmbedding f.symm).trans h).trans (RelIso.toRelEmbedding g)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.MonOpOpToComon_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ),
  (CategoryTheory.Comon.MonOpOpToComon C).obj A = CategoryTheory.Comon.MonOpOpToComonObj (Opposite.unop A)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_roo : ∀ {m n : ℤ} {i : ℕ}, (m<...n).toList[i]? = if i < (n - (m + 1)).toNat then some (m + 1 + ↑i) else none
-- Mathlib.Data.Set.Basic
Set.subset_univ : ∀ {α : Type u} (s : Set α), s ⊆ Set.univ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceNe : Lean.Meta.Simp.Simproc
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.evariance_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {f : α → ℝ} {g : β → ℝ},
  ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.evariance f μ = ProbabilityTheory.evariance g ν
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.mk : Lean.Lsp.Position →
  Lean.Lsp.InlayHintLabel →
    Option Lean.Lsp.InlayHintKind →
      Option (Array Lean.Lsp.TextEdit) →
        Option Lean.Lsp.InlayHintTooltip → Option Bool → Option Bool → Option Lean.Json → Lean.Lsp.InlayHint
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_nextn_startPos : ∀ (s : String.Slice) (n : ℕ),
  (s.startPos.nextn n).Splits (String.ofList (List.take n s.copy.toList)) (String.ofList (List.drop n s.copy.toList))
-- Mathlib.Topology.Order.Compact
ContinuousOn.le_sSup_image_Icc : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : TopologicalSpace β] [DenselyOrdered α] [inst_5 : ConditionallyCompleteLinearOrder β]
  [OrderTopology β] {f : α → β} {a b c : α},
  ContinuousOn f (Set.Icc a b) → c ∈ Set.Icc a b → f c ≤ sSup (f '' Set.Icc a b)
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.val_inv_unitsEquivUnitsType_symm_apply_coe : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (x : (↥S)ˣ), ↑(↑(S.unitsEquivUnitsType.symm x))⁻¹ = ↑↑x⁻¹
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat.eq_zero_of_not_dvd : ∀ {p n : ℕ}, ¬p ∣ n → padicValNat p n = 0
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.trans_refl : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), f.trans (OrderMonoidIso.refl β) = f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.erase_empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {k : α}, ∅.erase k = ∅
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticOn.zpow`

---

ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
AnalyticOn.fun_zpow : ∀ {𝕜 : 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} {n : ℤ}, AnalyticOn 𝕜 f s → (∀ z ∈ s, f z ≠ 0) → AnalyticOn 𝕜 (fun i => f i ^ n) s
-- Lean.DocString.Extension
/-- Returns all snippets of the Verso module docs from the indicated module, if they exist.
 -/
Lean.getVersoModuleDoc? : Lean.Environment → Lean.Name → Option (Array Lean.VersoModuleDocs.Snippet)
-- Mathlib.Logic.Equiv.Set
/-- A set `s` in `α × β` is equivalent to the sigma-type `Σ x, {y | (x, y) ∈ s}`.  -/
Equiv.setProdEquivSigma : {α : Type u_3} → {β : Type u_4} → (s : Set (α × β)) → ↑s ≃ (x : α) × ↑{y | (x, y) ∈ s}
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.unitOfList_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α},
  (Std.TreeMap.Raw.unitOfList l cmp).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.unop_w : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ}
  (L : Φ.op.RightResolution X₂), L.unop.w = L.w.unop
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.exists_path_of_dist : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Reachable u v → ∃ p, p.IsPath ∧ p.length = G.dist u v
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.IsRepresentable.has_representation : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {F : CategoryTheory.Functor Cᵒᵖ (Type v)}
  [self : F.IsRepresentable], ∃ Y, Nonempty (F.RepresentableBy Y)
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_ne_of_ne : ∀ {a b : UInt32}, a ≠ b → a.toBitVec ≠ b.toBitVec
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_iso_inv : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (x : X),
  (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).obj x).iso.inv = S.iso.inv.app x
-- Lean.Elab.PreDefinition.TerminationHint
/-- Logs warnings when the `TerminationHints` are unexpectedly present.   -/
Lean.Elab.TerminationHints.ensureNone : Lean.Elab.TerminationHints → String → Lean.CoreM Unit
-- Mathlib.Data.Fintype.Pi
Finset.univ_pi_univ : ∀ {α : Type u_3} {β : α → Type u_4} [inst : DecidableEq α] [inst_1 : Fintype α] [inst_2 : (a : α) → Fintype (β a)],
  (Finset.univ.pi fun a => Finset.univ) = Finset.univ
-- Mathlib.Analysis.Normed.Group.Basic
add_mem_ball_add_iff : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ} {c : E},
  a + c ∈ Metric.ball (b + c) r ↔ a ∈ Metric.ball b r
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofNat.sizeOf_spec : ∀ (n : ℕ), sizeOf (Lean.LeanOptionValue.ofNat n) = 1 + sizeOf n
-- Mathlib.Order.Filter.Tendsto
Set.MapsTo.tendsto : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.MapsTo f s t → Filter.Tendsto f (Filter.principal s) (Filter.principal t)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_diff!_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false →
          Std.DTreeMap.Internal.Impl.Const.getD (m₁.diff! m₂) k fallback = fallback
-- Init.Data.Array.Lemmas
Array.flatMap_id : ∀ {α : Type u_1} {xss : Array (Array α)}, Array.flatMap id xss = xss.flatten
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- **Alias** of `Valuation.isClosed_closedBall`.

---

For any valuation `v` compatible with the valuative relation on `R`, the closed `r`-ball
around zero `{x | v.restrict x ≤ r}` is closed in the valuative topology.  -/
IsValuativeTopology.isClosed_closedBall : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  (r : (MonoidWithZeroHom.ofClass v).ValueGroup₀), IsClosed {x | v.restrict x ≤ r}
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring of a `CommSemiring` is a `CommSemiring`.  -/
SubsemiringClass.toCommSemiring : {S : Type v} →
  (s : S) → {R : Type u_1} → [inst : CommSemiring R] → [inst_1 : SetLike S R] → [SubsemiringClass S R] → CommSemiring ↥s
-- Mathlib.Data.Nat.Find
Nat.findGreatest_eq : ∀ {P : ℕ → Prop} [inst : DecidablePred P] {n : ℕ}, P n → Nat.findGreatest P n = n
-- Mathlib.Analysis.Convex.BetweenList
Function.Injective.list_sbtw_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {l : List P} {f : P →ᵃ[R] P'},
  Function.Injective ⇑f → (List.Sbtw R (List.map (⇑f) l) ↔ List.Sbtw R l)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.lift_apply : ∀ {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 : Monoid M] (F : M →* A) (f : MonoidAlgebra R M),
  ((MonoidAlgebra.lift R A M) F) f = f.coeff.sum fun a b => b • F a
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePushoutShapeOpEquiv_unitIso : ∀ (J : Type w),
  (CategoryTheory.Limits.widePushoutShapeOpEquiv J).unitIso = (CategoryTheory.Limits.widePushoutShapeOpUnop J).symm
-- Init.SimpLemmas
dite_cond_eq_true : ∀ {α : Sort u} {c : Prop} {x : Decidable c} {t : c → α} {e : ¬c → α} (h : c = True), dite c t e = t ⋯
-- Mathlib.Data.List.Destutter
List.mem_destutter' : ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α), a ∈ List.destutter' R a l
-- Mathlib.Order.RelClasses
instAntisymmGt : ∀ {α : Type u} [inst : Preorder α], Std.Antisymm fun x1 x2 => x2 < x1
-- Mathlib.Data.Set.Prod
Set.offDiag.eq_1 : ∀ {α : Type u} (s : Set α), s.offDiag = {x | x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2}
-- Mathlib.Data.ENat.Basic
ENat.natCast_mul : ∀ (m n : ℕ), ↑(m * n) = ↑m * ↑n
-- Mathlib.Order.Ideal
Order.Ideal.mk.injEq : ∀ {P : Type u_2} [inst : LE P] (toLowerSet : LowerSet P) (nonempty' : toLowerSet.carrier.Nonempty)
  (directed' : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet.carrier) (toLowerSet_1 : LowerSet P)
  (nonempty'_1 : toLowerSet_1.carrier.Nonempty) (directed'_1 : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet_1.carrier),
  ({ toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' } =
      { toLowerSet := toLowerSet_1, nonempty' := nonempty'_1, directed' := directed'_1 }) =
    (toLowerSet = toLowerSet_1)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  (s : TopologicalSpace.Closeds α) (t : TopologicalSpace.Closeds β), ↑(s ×ˢ t) = ↑s ×ˢ ↑t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.isEmpty = true → t.getKeyD a fallback = fallback
-- Mathlib.Data.Complex.Basic
Complex.normSq_nonneg : ∀ (z : ℂ), 0 ≤ Complex.normSq z
-- Std.Internal.Do.Triple.Basic
/-- The weakest precondition entailment witnessing the triple.  -/
Std.Internal.Do.Triple.le_wp : ∀ {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] {x : Prog} [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {pre : Pred}
  {post : Value → Pred} {epost : EPred},
  ⦃ pre ⦄ x ⦃ post; epost ⦄ → Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post epost)
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
Ideal.asIdeal_toTwoSided : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided], TwoSidedIdeal.asIdeal I.toTwoSided = I
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.IsDominant.isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.IsDominant
-- Mathlib.Algebra.Polynomial.CancelLeads
Polynomial.cancelLeads.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (p q : Polynomial R),
  p.cancelLeads q =
    Polynomial.C p.leadingCoeff * Polynomial.X ^ (p.natDegree - q.natDegree) * q -
      Polynomial.C q.leadingCoeff * Polynomial.X ^ (q.natDegree - p.natDegree) * p
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_left_Ico : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → ∀ (b c : G₀), (fun x => a * x) '' Set.Ico b c = Set.Ico (a * b) (a * c)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instSeminormedAddCommGroup : {α : Type u_1} →
  {E : Type u_3} →
    [inst : TopologicalSpace α] →
      [CompactSpace α] → [inst_2 : SeminormedAddCommGroup E] → SeminormedAddCommGroup C(α, E)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addLECancellable_of_lt_bot : ∀ {α : Type u} [inst : Add α] {x : WithBot α} [inst_1 : Preorder α] [AddLeftReflectLE α], x < ⊥ → AddLECancellable x
-- Mathlib.Computability.Primrec.Basic
Primcodable.toEncodable : {α : Type u_1} → [self : Primcodable α] → Encodable α
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.instEquivLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Mul α] →
      [inst_1 : Add α] →
        [inst_2 : LE α] → [inst_3 : Mul β] → [inst_4 : Add β] → [inst_5 : LE β] → EquivLike (α ≃+*o β) α β
-- Mathlib.Dynamics.Ergodic.AddCircle
AddCircle.ergodic_nsmul_add : ∀ {T : ℝ} [hT : Fact (0 < T)] (x : AddCircle T) {n : ℕ}, 1 < n → Ergodic (fun y => n • y + x) MeasureTheory.volume
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instIsIsoRight : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {R : CategoryTheory.Functor B T}
  {L : CategoryTheory.Functor A T} {X Y : CategoryTheory.Comma L R} (e : Y ⟶ X) [CategoryTheory.IsIso e],
  CategoryTheory.IsIso e.right
-- Mathlib.Data.Set.Insert
Set.singleton_eq_singleton_iff : ∀ {α : Type u_1} {x y : α}, {x} = {y} ↔ x = y
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.mk : {𝕜 : Type u} →
  {A : Type v} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] →
              (toProd : (A →L[𝕜] A) × (A →L[𝕜] A)) →
                (∀ (x y : A), toProd.2 x * y = x * toProd.1 y) → DoubleCentralizer 𝕜 A
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.mk : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (f : P.toExtension.Cotangent → ↥P.toExtension.ker) →
                    (∀ (b : P.toExtension.Cotangent), Algebra.Extension.Cotangent.mk (f b) = b) →
                      (g : P.Ring) →
                        g - 1 ∈ P.ker →
                          g • P.ker ≤ Ideal.span (Set.range (Subtype.val ∘ f ∘ ⇑b)) →
                            Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.instMin : Min YoungDiagram
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.sylvester_zero_left_deg : ∀ {R : Type u_1} [inst : Semiring R] (f g : Polynomial R) (m : ℕ),
  f.sylvester g 0 m = Matrix.diagonal fun x => f.coeff 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapId_inv_app_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (Y : T) (X : CategoryTheory.Over Y),
  ((CategoryTheory.Over.mapId Y).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- The self product of `X` indexed by its fiber.  -/
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.selfProd : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [CategoryTheory.GaloisCategory C] → CategoryTheory.Functor C FintypeCat → C → C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.sin_arcsin : ∀ {x : ℝ}, -1 ≤ x → x ≤ 1 → Real.sin (Real.arcsin x) = x
-- Mathlib.Topology.Closure
/-- The frontier of a set is closed.  -/
isClosed_frontier : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed (frontier s)
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLike_star : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] (f : C(X, ℝ)),
  ContinuousMap.realToRCLike 𝕜 (star f) = star (ContinuousMap.realToRCLike 𝕜 f)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActivateNextGuardResult : Type
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The real inner product of two vectors, divided by the product of their
norms, has absolute value at most 1.  -/
abs_real_inner_div_norm_mul_norm_le_one : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  |inner ℝ x y / (‖x‖ * ‖y‖)| ≤ 1
-- Mathlib.Analysis.Distribution.Distribution
Distribution.lineDerivCLM_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] {n k : ℕ∞}
  [inst_5 : IsTopologicalAddGroup F] [inst_6 : ContinuousSMul ℝ F] {v : E} {T : Distribution Ω F k}
  {f : TestFunction Ω ℝ n}, ((Distribution.lineDerivCLM v) T) f = -T ((TestFunction.lineDerivCLM ℝ v) f)
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.expandIfNecessary.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DHashMap.Internal.Raw₀ α β → Sort u_3) →
      (m : Std.DHashMap.Internal.Raw₀ α β) →
        ((size : ℕ) →
            (buckets : Array (Std.DHashMap.Internal.AssocList α β)) →
              (hm : 0 < { size := size, buckets := buckets }.buckets.size) →
                motive ⟨{ size := size, buckets := buckets }, hm⟩) →
          motive m
-- Lean.Elab.Do.Basic
Lean.Elab.Do.MutVar.mk.injEq : ∀ (ident : Lean.Ident) (baseId : Lean.FVarId) (ident_1 : Lean.Ident) (baseId_1 : Lean.FVarId),
  ({ ident := ident, baseId := baseId } = { ident := ident_1, baseId := baseId_1 }) =
    (ident = ident_1 ∧ baseId = baseId_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Filter.Tendsto.rpow : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℝ} {x y : ℝ},
  Filter.Tendsto f l (nhds x) →
    Filter.Tendsto g l (nhds y) → x ≠ 0 ∨ 0 < y → Filter.Tendsto (fun t => f t ^ g t) l (nhds (x ^ y))
-- Lean.Declaration
Lean.TheoremVal.mk.injEq : ∀ (toConstantVal : Lean.ConstantVal) (value : Lean.Expr) (all : List Lean.Name) (toConstantVal_1 : Lean.ConstantVal)
  (value_1 : Lean.Expr) (all_1 : List Lean.Name),
  ({ toConstantVal := toConstantVal, value := value, all := all } =
      { toConstantVal := toConstantVal_1, value := value_1, all := all_1 }) =
    (toConstantVal = toConstantVal_1 ∧ value = value_1 ∧ all = all_1)