mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- The multiplicity of `v` in `∏_v v^(val_v(I))` equals `val_v(I)`.  -/
Ideal.finprod_count : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (I : Ideal R),
  I ≠ 0 →
    (Associates.mk v.asIdeal).count
        (Associates.mk (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I)).factors =
      (Associates.mk v.asIdeal).count (Associates.mk I).factors
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mkEmptyEntriesArray : {α : Type u_1} → {β : Type u_2} → Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))
-- Lean.ErrorExplanation
Lean.ErrorExplanation.Metadata.mk : String → String → Lean.MessageSeverity → Option String → Lean.ErrorExplanation.Metadata
-- Lean.Elab.InfoTree.Types
Lean.Elab.TermInfo.expr : Lean.Elab.TermInfo → Lean.Expr
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.instMonoMapFourδ₁Toδ₀ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₁ i₂ i₃ i₄ i₅ : ι}
  (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  CategoryTheory.Mono
    (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
/-- If `g` is an upper triangular matrix with trace zero,
then `g` fixes the vertical line `re z = b / (2 * d)`.  -/
UpperHalfPlane.gl_smul_eq_self_iff_re_eq : ∀ {g : GL (Fin 2) ℝ} {z : UpperHalfPlane}, (↑g).trace = 0 → ↑g 1 0 = 0 → (g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1))
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.hasPointwiseRightKanExtension_of_preserves : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [L.HasPointwiseRightKanExtension F] [G.PreservesPointwiseRightKanExtension F L],
  L.HasPointwiseRightKanExtension (F.comp G)
-- Mathlib.Algebra.Order.Interval.Multiset
Multiset.map_add_left_Ioo : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Multiset.map (fun x => c + x) (Multiset.Ioo a b) = Multiset.Ioo (c + a) (c + b)
-- Lean.Server.Requests
Lean.FileMap.rangeIncludesRequestedRange : Lean.FileMap → Lean.Syntax.Range → Lean.Syntax.Range → optParam Bool false → optParam Bool false → Bool
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.le_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0), μ s ≤ (μ.trim hm) s
-- Mathlib.Topology.MetricSpace.Polish
instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.SeparableSpace α]
  [TopologicalSpace.IsCompletelyMetrizableSpace α], PolishSpace α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_union_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂), (t₁ ∪ t₂)[k] = t₂[k]
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instLeftDistribClass : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [LeftDistribClass R], LeftDistribClass Rᵒᵈ
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.hom_hom_ofHom : ∀ {X Y : Type u} [inst : PartialOrder X] [inst_1 : Fintype X] [inst_2 : PartialOrder Y] [inst_3 : Fintype Y]
  (f : X →o Y), PartOrd.Hom.hom (FinPartOrd.ofHom f).hom = f
-- Mathlib.Analysis.Normed.Group.Hom
/-- The inclusion of an `AddSubgroup`, as bounded group homomorphism.  -/
NormedAddGroupHom.incl : {V : Type u_1} → [inst : SeminormedAddCommGroup V] → (s : AddSubgroup V) → NormedAddGroupHom (↥s) V
-- Mathlib.Data.DFinsupp.Submonoid
AddSubmonoid.mem_bsupr_iff_exists_dfinsupp : ∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] (p : ι → Prop) [inst_1 : DecidablePred p] [inst_2 : AddCommMonoid γ]
  (S : ι → AddSubmonoid γ) (x : γ),
  x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ f, (DFinsupp.sumAddHom fun i => (S i).subtype) (DFinsupp.filter p f) = x
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- **Alias** of `Valuation.isOpen_closedBall`.

---

For any valuation `v` compatible with the valuative relation on `R`, the closed `r`-ball
around zero `{x | v.restrict x ≤ r}` is open in the valuative topology.  -/
IsValuativeTopology.isOpen_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₀}, r ≠ 0 → IsOpen {x | v.restrict x ≤ r}
-- Lean.Meta.CongrTheorems
Lean.Meta.instBEqCongrArgKind.beq : Lean.Meta.CongrArgKind → Lean.Meta.CongrArgKind → Bool
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.lt_one_iff_lt_one : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {x : R}, v₁ x < 1 ↔ v₂ x < 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        ∀ {h' : k' ∈ Std.DTreeMap.Const.insertMany t l}, (Std.DTreeMap.Const.insertMany t l).getKey k' h' = k
-- Mathlib.Algebra.Group.Defs
AddCommGroup.toDivisionAddCommMonoid : {G : Type u_1} → [AddCommGroup G] → SubtractionCommMonoid G
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.coe_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (f : M ≃+ N) (hf1 : Continuous f.toFun) (hf2 : Continuous f.invFun),
  ⇑{ toAddEquiv := f, continuous_toFun := hf1, continuous_invFun := hf2 } = ⇑f
-- Init.Data.Int.Gcd
Int.lcm_dvd_mul_self_right_iff_dvd_mul : ∀ {k m n : ℕ}, (↑n).lcm ↑k ∣ m * k ↔ n ∣ m * k
-- Init.Data.Array.MapIdx
Array.mapIdx_induction : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {xs : Array α} {motive : ℕ → Prop},
  motive 0 →
    ∀ {p : (i : ℕ) → β → i < xs.size → Prop},
      (∀ (i : ℕ) (h : i < xs.size), motive i → p i (f i xs[i]) h ∧ motive (i + 1)) →
        motive xs.size ∧
          ∃ (eq : (Array.mapIdx f xs).size = xs.size), ∀ (i : ℕ) (h : i < xs.size), p i (Array.mapIdx f xs)[i] h
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.getInductionPrinciplePostfix : Lean.Name → Bool → Lean.MetaM Lean.Name
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Alt.mk.inj : ∀ {σ : Type} {ref : Lean.Syntax} {vars : Array Lean.Elab.Term.Do.Var} {patterns : Lean.Syntax} {rhs : σ}
  {ref_1 : Lean.Syntax} {vars_1 : Array Lean.Elab.Term.Do.Var} {patterns_1 : Lean.Syntax} {rhs_1 : σ},
  { ref := ref, vars := vars, patterns := patterns, rhs := rhs } =
      { ref := ref_1, vars := vars_1, patterns := patterns_1, rhs := rhs_1 } →
    ref = ref_1 ∧ vars = vars_1 ∧ patterns = patterns_1 ∧ rhs = rhs_1
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The inverse functor used to define the equivalence `ofCommaSndEquivalence`.  -/
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor C T) →
              (G : CategoryTheory.Functor D T) →
                (c : C) →
                  CategoryTheory.Functor (CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G)
                    (CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G))
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_ne_top_of_diam_ne_zero : ∀ {α : Type u_1} {G : SimpleGraph α}, G.diam ≠ 0 → G.ediam ≠ ⊤
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.ext : ∀ {α : Type u_1} {f : α → α} {x y : IterateMulAct f}, x.val = y.val → x = y
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.instContinuousSup : ∀ {α : Type u_1} [inst : UniformSpace α], ContinuousSup (TopologicalSpace.Closeds α)
-- Mathlib.Tactic.NormNum.IsSquare
/-- `norm_num` extension for `IsSquare` on `ℕ`.  -/
Mathlib.Meta.NormNum.evalIsSquareNat : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_zero_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0) → MeasureTheory.setToFun μ T hT f = 0
-- Init.Data.String.Lemmas.Slice
String.Pos.get?_eq_none_iff : ∀ {s : String} {p : s.Pos}, p.get? = none ↔ p = s.endPos
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- A `WeierstrassCurve` is in normal form of characteristic = 2 and j ≠ 0, if its `a₁ = 1` and
`a₃, a₄ = 0`. In other words it is `Y² + XY = X³ + a₂X² + a₆`.  -/
WeierstrassCurve.IsCharTwoJNeZeroNF : {R : Type u_1} → [CommRing R] → WeierstrassCurve R → Prop
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isLocalization : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₅, u₅} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  [Φ.IsLocalizedEquivalence], (Φ.functor.comp L₂).IsLocalization W₁
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Cell.Const.get?.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option ((_ : α) × β) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (p : (_ : α) × β) → motive (some p)),
  (match none with
    | none => h_1 ()
    | some p => h_2 p) =
    h_1 ()
-- Mathlib.Data.Nat.PrimeFin
/-- A version of `Nat.Prime.mem_primeFactors` using `[NeZero n]` instead of an explicit argument.  -/
Nat.Prime.mem_primeFactors' : ∀ {n p : ℕ}, Nat.Prime p → p ∣ n → ∀ [NeZero n], p ∈ n.primeFactors
-- Mathlib.RingTheory.Multiplicity
multiplicity_map_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Monoid β] {F : Type u_3} [inst_2 : EquivLike F α β]
  [MulEquivClass F α β] (f : F) {a b : α}, multiplicity (f a) (f b) = multiplicity a b
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If `C` has limits and `G` preserves limits, then if `G` reflects isomorphisms then it reflects
limits.
 -/
CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G : CategoryTheory.Functor C D} [G.ReflectsIsomorphisms] [CategoryTheory.Limits.HasLimitsOfSize.{w', w, v₁, u₁} C]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_eq_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {a : α} {h' : a ∈ m}, m.get a h' = m.get! a
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk_assoc : ∀ {X : AlgebraicGeometry.Scheme} {x y : ↥X} (h : x ⤳ y) {Z : AlgebraicGeometry.Scheme} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h))
      (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk y) h_1) =
    CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) h_1
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instRing : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} →
          [inst : SMul M X] →
            [inst_1 : Monoid N] → [inst_2 : Ring Y] → [inst_3 : MulSemiringAction N Y] → Ring (X →ₑ[σ] Y)
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_eq_update : ∀ {α : Sort u_1} [inst : DecidableEq α] (i j : α), ⇑(Equiv.swap i j) = Function.update (Function.update id j i) i j
-- Mathlib.NumberTheory.FermatPsp
/-- Given a prime `p` which does not divide `b * (b ^ 2 - 1)`, we can produce a number `n` which is
larger than `p` and pseudoprime to base `b`. We do this by defining
`n = ((b ^ p - 1) / (b - 1)) * ((b ^ p + 1) / (b + 1))`

The primary purpose of this definition is to help prove `exists_infinite_pseudoprimes`. For a proof
that `n` is actually pseudoprime to base `b`, see `psp_from_prime_psp`, and for a proof that `n` is
greater than `p`, see `psp_from_prime_gt_p`.

This lemma is intended to be used when `2 ≤ b`, `2 < p`, `p` is prime, and `¬p ∣ b * (b ^ 2 - 1)`,
because those are the hypotheses for `psp_from_prime_psp`.
 -/
_private.Mathlib.NumberTheory.FermatPsp.0.Nat.psp_from_prime : ℕ → ℕ → ℕ
-- Mathlib.Algebra.Group.Invertible.Defs
/-- If `r` is invertible and `s = r` and `si = ⅟r`, then `s` is invertible with `⅟s = si`.  -/
Invertible.copy' : {α : Type u} → [inst : MulOneClass α] → {r : α} → (hr : Invertible r) → (s si : α) → s = r → si = ⅟r → Invertible s
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The n-coskeleton as a functor `SimplicialObject.Truncated C n ⥤ SimplicialObject C`.  -/
CategoryTheory.SimplicialObject.Truncated.cosk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
            (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] →
        CategoryTheory.Functor (CategoryTheory.SimplicialObject.Truncated C n) (CategoryTheory.SimplicialObject C)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.topologicalSpaceCoconePtOfCoconeForget : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J TopCat} →
      (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat))) →
        TopologicalSpace (TopCat.coconePtOfCoconeForget c)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_zpow_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_target_eventuallyEq : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {y : M},
  y ∈ f.source → (f.extend I).target =ᶠ[nhds (↑(f.extend I) y)] Set.range ↑I
-- Mathlib.Topology.Constructions
ContinuousAt.update : ∀ {X : Type u} {ι : Type u_5} {A : ι → Type u_6} [inst : TopologicalSpace X] [T : (i : ι) → TopologicalSpace (A i)]
  {f : X → (i : ι) → A i} [inst_1 : DecidableEq ι] {x : X},
  ContinuousAt f x → ∀ (i : ι) {g : X → A i}, ContinuousAt g x → ContinuousAt (fun a => Function.update (f a) i (g a)) x
-- Mathlib.Data.Set.Card
Set.encard_pi_eq_prod_encard : ∀ {α : Type u_1} [h : Fintype α] {ι : α → Type u_3} {s : (i : α) → Set (ι i)},
  (Set.univ.pi s).encard = ∏ i, (s i).encard
-- Mathlib.Analysis.Meromorphic.NormalForm
MeromorphicNFOn.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {x : 𝕜},
  AnalyticAt 𝕜 f x → MeromorphicNFAt g x → g x ≠ 0 ∨ f x ≠ 0 → MeromorphicNFAt (f / g) x
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.eq_zero_of_infinite_isRoot : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] (p : Polynomial R), {x | p.IsRoot x}.Infinite → p = 0
-- Aesop.Options.Public
Aesop.Strategy.noConfusionType : Sort v✝ → Aesop.Strategy → Aesop.Strategy → Sort v✝
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.natCast_log : ∀ {n : ℕ}, ↑(Real.log ↑n) = Complex.log ↑n
-- Init.Data.Range.Polymorphic.PRange
/-- This type class allows taking the intersection of two left-closed right-open ranges, resulting in
another left-closed right-open range.
 -/
Std.Rco.HasRcoIntersection : Type w → Type w
-- Init.Data.BitVec.Lemmas
BitVec.fill_eq : ∀ {w : ℕ} {v : Bool}, BitVec.fill w v = if v = true then BitVec.allOnes w else 0#w
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
/-- An exception in the `SimplexAlgorithmM` monad.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException : Type
-- Lean.DocString.Types
Lean.Doc.Block.blockquote.injEq : ∀ {i : Type u} {b : Type v} (items items_1 : Array (Lean.Doc.Block i b)),
  (Lean.Doc.Block.blockquote items = Lean.Doc.Block.blockquote items_1) = (items = items_1)
-- Init.Data.Order.Ord
Std.ReflCmp.cmp_eq_of_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.ReflCmp cmp] {a b : α}, a = b → cmp a b = Ordering.eq
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Additively isomorphic rings have additively isomorphic additive monoid algebras.

`AddMonoidAlgebra.map` as an `AddEquiv`.  -/
AddMonoidAlgebra.mapAddEquiv : {R : Type u_3} →
  {S : Type u_4} →
    (M : Type u_6) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : Add M] → R ≃+ S → AddMonoidAlgebra R M ≃+ AddMonoidAlgebra S M
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.fromOpcycles.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ), X.fromOpcycles f g fg h n = X.fromOpcycles f g fg h n
-- Mathlib.Logic.Relation
Relation.transitive_reflTransGen : ∀ {α : Type u_1} {r : α → α → Prop}, IsTrans α (Relation.ReflTransGen r)
-- Lean.DefEqAttrib
/-- For automatically generated theorems (equational theorems etc.), we tag the theorem with
the `defeq`/`backward_defeq` attributes based on its `rfl` proof:

* If the equation holds at `.implicit` transparency (matching the transparency at which
  `dsimp` operates), we tag it with `@[defeq]`.
* Independently, if the equation holds under the more permissive legacy check (equivalent
  to `validateDefEqAttr`, i.e. at `.default` or `.all` transparency), we tag it with
  `@[backward_defeq]`.

In particular, every theorem that would have been tagged `@[defeq]` before the stricter
inference rules were introduced is now tagged `@[backward_defeq]`. Local backwards
compatibility can be restored with `set_option backward.defeqAttrib.useBackward true`.
 -/
Lean.inferDefEqAttr : Lean.Name → Lean.MetaM Unit
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {fallback : β} {f : β → β},
  (m.modify k f).getD k' fallback = if (k == k') = true then (Option.map f m[k]?).getD fallback else m.getD k' fallback
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The proposition that a sequence indexed by `ℤ` is an elliptic sequence.  -/
IsEllipticSequence : {R : Type u_1} → [CommRing R] → (ℤ → R) → Prop
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.symm_addMonoidHomCongrLeftEquiv : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : AddZeroClass M₁] [inst_1 : AddZeroClass M₂]
  [inst_2 : AddMonoid N] (e : M₁ ≃+ M₂), e.addMonoidHomCongrLeftEquiv.symm = e.symm.addMonoidHomCongrLeftEquiv
-- Mathlib.RingTheory.TensorProduct.Quotient
/-- Let `e` be an element of `R' ⊗[R] S`. Then `R'' ⊗[R'] ((R' ⊗[R] S) / e)` is isomorphic to
`(R'' ⊗[R] S) / e` as `R''`-algebras.  -/
Algebra.tensorQuotientTensorEquiv : {R : Type u_1} →
  {R' : Type u_2} →
    (R'' : Type u_3) →
      {S : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing R'] →
            [inst_2 : CommRing R''] →
              [inst_3 : CommRing S] →
                [inst_4 : Algebra R R'] →
                  [inst_5 : Algebra R R''] →
                    [inst_6 : Algebra R' R''] →
                      [inst_7 : IsScalarTower R R' R''] →
                        [inst_8 : Algebra R S] →
                          (e : TensorProduct R R' S) →
                            TensorProduct R' R'' (TensorProduct R R' S ⧸ Ideal.span {e}) ≃ₐ[R'']
                              TensorProduct R R'' S ⧸
                                Ideal.span {(Algebra.TensorProduct.rTensor S (Algebra.ofId R' R'')) e}
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.rightOp_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor Cᵒᵖ D} (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.NatTrans.rightOp (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightOp β) (CategoryTheory.NatTrans.rightOp α)
-- Mathlib.Algebra.Order.Module.Defs
nonpos_of_smul_nonpos_of_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosReflectLE α β], a • b ≤ 0 → 0 < b → a ≤ 0
-- Mathlib.Algebra.Ring.Aut
RingAut.inv_apply : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] (f : R ≃+* R) (x : R), f⁻¹ x = f.symm x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
/-- The linear equivalence `Ext X Y 0 ≃ₜ[R] (X ⟶ Y)`.  -/
CategoryTheory.Abelian.Ext.linearEquiv₀ : {R : Type t} →
  [inst : Ring R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.Linear R C] →
            [inst_4 : CategoryTheory.HasExt C] → {X Y : C} → CategoryTheory.Abelian.Ext X Y 0 ≃ₗ[R] X ⟶ Y
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.withTopOrderIso_symm_apply : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M} (h : a ≠ 0),
  (FiniteArchimedeanClass.withTopOrderIso M).symm (ArchimedeanClass.mk a) = ↑(FiniteArchimedeanClass.mk a h)
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues_of_lt : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 E = n) {i : ℕ} (hi : i < n),
  T.singularValues i = √(⋯.eigenvalues hn ⟨i, hi⟩)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_le_nsmul : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] {a b : M},
  a ≤ b → 0 ≤ b → ∀ {m n : ℕ}, m ≤ n → m • a ≤ n • b
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.insertReplacementForLetRecs : Lean.Elab.Term.MutualClosure.Replacement →
  List Lean.Elab.Term.MutualClosure.LetRecClosure → Lean.Elab.Term.MutualClosure.Replacement
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.isSymmetric_esymmAlgHomMonomial : ∀ {σ : Type u_1} {R : Type u_3} {n : ℕ} [inst : CommSemiring R] [inst_1 : Fintype σ] (t : Fin n →₀ ℕ) (r : R),
  (MvPolynomial.esymmAlgHomMonomial σ t r).IsSymmetric