mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Pointwise
Bornology.IsBounded.of_add : ∀ {E : Type u_1} [inst : SeminormedAddGroup E] {s t : Set E},
  Bornology.IsBounded (s + t) → Bornology.IsBounded s ∨ Bornology.IsBounded t
-- Init.Data.UInt.Lemmas
UInt8.toUSize_ofFin : ∀ {n : Fin UInt8.size}, (UInt8.ofFin n).toUSize = USize.ofNatLT ↑n ⋯
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagInfo.sources : Lean.Meta.Grind.EMatchDiagInfo → List Lean.Meta.Grind.EMatchDiagNode
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.truncGE'.homologyι_truncGE'XIsoOpcycles_inv_d : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (j k : ι) {j' : ι'} (hj' : e.f j = j') (hj : e.BoundaryGE j),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (K.homologyι j') (K.truncGE'XIsoOpcycles e hj' hj).inv)
      ((K.truncGE' e).d j k) =
    0
-- Mathlib.Algebra.Field.GeomSum
geom_sum_inv : ∀ {K : Type u_2} [inst : DivisionRing K] {x : K},
  x ≠ 1 → x ≠ 0 → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
-- Mathlib.Algebra.Order.Group.MinMax
max_sub_max_le_max : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c d : α),
  max a b - max c d ≤ max (a - c) (b - d)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj 𝒜 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 x ⋯ ⋯) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
        (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm'))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) h)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₂_app_two' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  (app₀ : f.obj' 0 _proof_245✝ ⟶ g.obj' 0 _proof_245✝) (app₁ : f.obj' 1 _proof_246✝ ⟶ g.obj' 1 _proof_246✝)
  (app₂ : f.obj' 2 _proof_247✝ ⟶ g.obj' 2 _proof_247✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝))
      _auto_266✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_247✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_247✝))
      _auto_268✝),
  (CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app
      ⟨2, CategoryTheory.ComposableArrows.homMk₂._proof_3⟩ =
    app₂
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_mk' : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (x : Polynomial K) (y : ↥(nonZeroDivisors (Polynomial K))),
  { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) x y } = IsLocalization.mk' (RatFunc K) x y
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sup_eq_right : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b : CauSeq α abs},
  a ≤ b → a ⊔ b ≈ b
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.sub'.match_1.eq_5 : ∀ (motive : PosNum → PosNum → Sort u_1) (a b : PosNum) (h_1 : (a : PosNum) → motive a PosNum.one)
  (h_2 : (b : PosNum) → motive PosNum.one b) (h_3 : (a b : PosNum) → motive a.bit0 b.bit0)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit1) (h_5 : (a b : PosNum) → motive a.bit1 b.bit0)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit1),
  (match a.bit1, b.bit0 with
    | a, PosNum.one => h_1 a
    | PosNum.one, b => h_2 b
    | a.bit0, b.bit0 => h_3 a b
    | a.bit0, b.bit1 => h_4 a b
    | a.bit1, b.bit0 => h_5 a b
    | a.bit1, b.bit1 => h_6 a b) =
    h_5 a b
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.ClusterState.filterPHashSet : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → (α → Bool) → Lean.PHashSet α → Lean.PHashSet α
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.orthogonalProjectionOnto.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], K.orthogonalProjectionOnto = K.orthogonalProjectionOnto
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.eqOnSource_refl : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e ≈ e
-- Lean.Parser.Term
Lean.Parser.Term.hygienicLParen : Lean.Parser.Parser
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.composableArrows₅_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, 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₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.composableArrows₅_exact._auto_1),
  (X.composableArrows₅ f g fg h n₀ n₁ hn₁).Exact
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst_prod_snd : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.fst.prod Monoid.Coprod.snd = Monoid.Coprod.toProd
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.measure_support_lt_top : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : Zero β] {μ : MeasureTheory.Measure α}
  (f : MeasureTheory.SimpleFunc α β), (∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤) → μ (Function.support ⇑f) < ⊤
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.realSize_toHeap.go : ∀ {α : Type u_1} {n : ℕ} {res : Batteries.BinomialHeap.Imp.Heap α} (s : Batteries.BinomialHeap.Imp.HeapNode α),
  (Batteries.BinomialHeap.Imp.HeapNode.toHeap.go s n res).realSize = s.realSize + res.realSize
-- Mathlib.Topology.PartitionOfUnity
/-- If `X` is a paracompact normal topological space and `U` is an open covering of a closed set
`s`, then there exists a `BumpCovering ι X s` that is subordinate to `U`. This version assumes that
`p : (X → ℝ) → Prop` is a predicate that satisfies Urysohn's lemma, and provides a
`BumpCovering` such that each function of the covering satisfies `p`.  -/
BumpCovering.exists_isSubordinate_of_prop : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X]
  (p : (X → ℝ) → Prop),
  (∀ (s t : Set X),
      IsClosed s →
        IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1) →
    IsClosed s →
      ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
-- Mathlib.Order.Category.BddOrd
BddOrd.Iso.mk_hom : ∀ {α β : BddOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd), (BddOrd.Iso.mk e).hom = BddOrd.ofHom ↑e
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq_hom_counit_assoc : ∀ {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] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G') {Z : CategoryTheory.Functor D D} (h : CategoryTheory.Functor.id D ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (adj1.rightAdjointUniq adj2).hom F)
      (CategoryTheory.CategoryStruct.comp adj2.counit h) =
    CategoryTheory.CategoryStruct.comp adj1.counit h
-- Aesop.Search.SearchM
Aesop.SearchM.State.mk.inj : ∀ {Q : Type} {inst : Aesop.Queue Q} {iteration : Aesop.Iteration} {queue : Q} {maxRuleApplicationDepthReached : Bool}
  {iteration_1 : Aesop.Iteration} {queue_1 : Q} {maxRuleApplicationDepthReached_1 : Bool},
  { iteration := iteration, queue := queue, maxRuleApplicationDepthReached := maxRuleApplicationDepthReached } =
      { iteration := iteration_1, queue := queue_1,
        maxRuleApplicationDepthReached := maxRuleApplicationDepthReached_1 } →
    iteration = iteration_1 ∧ queue = queue_1 ∧ maxRuleApplicationDepthReached = maxRuleApplicationDepthReached_1
-- Lean.Meta.Tactic.Congr
/-- Preprocessor before applying congruence theorem.
Tries to close new goals using `Eq.refl`, `HEq.refl`, and `assumption`.
It also tries to apply `heq_of_eq`.
 -/
Lean.MVarId.congrPre : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.mk.inj : ∀ {offset : Std.Time.TimeZone.Offset} {name abbreviation : String} {isDST : Bool} {offset_1 : Std.Time.TimeZone.Offset}
  {name_1 abbreviation_1 : String} {isDST_1 : Bool},
  { offset := offset, name := name, abbreviation := abbreviation, isDST := isDST } =
      { offset := offset_1, name := name_1, abbreviation := abbreviation_1, isDST := isDST_1 } →
    offset = offset_1 ∧ name = name_1 ∧ abbreviation = abbreviation_1 ∧ isDST = isDST_1
-- Mathlib.GroupTheory.Transfer
MonoidHom.transferSylow_eq_pow : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G) (hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P)
  [inst_1 : Fact (Nat.Prime p)] [inst_2 : Finite (Sylow p G)] [inst_3 : (↑P).FiniteIndex] (g : G) (hg : g ∈ P),
  (MonoidHom.transferSylow P hP) g = ⟨g ^ (↑P).index, ⋯⟩
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubsemigroup.coe_even : ∀ {S : Type u_1} [inst : AddCommSemigroup S], ↑(AddSubsemigroup.even S) = {s | Even s}
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_one_div : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {K' : Type u_5} [inst_5 : Field K'] [inst_6 : Algebra R₁ K']
  [inst_7 : IsFractionRing R₁ K'] (I : FractionalIdeal (nonZeroDivisors R₁) K) (h : K ≃ₐ[R₁] K'),
  FractionalIdeal.map (↑h) (1 / I) = 1 / FractionalIdeal.map (↑h) I
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
/-- Bijection between a subalgebra `S` and its opposite.  -/
Subalgebra.linearEquivOp : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → ↥S ≃ₗ[R] ↥S.op
-- Init.Data.Vector.Lemmas
/-- Variant of `all_bne` with `!=` reversed.  -/
Vector.all_bne' : ∀ {α : Type u_1} {n : ℕ} {a : α} [inst : BEq α] [PartialEquivBEq α] {xs : Vector α n},
  (xs.all fun x => x != a) = !xs.contains a
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.comp_toPrelaxFunctor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.LaxFunctor B C) (G : CategoryTheory.LaxFunctor C D),
  (F.comp G).toPrelaxFunctor = F.comp G.toPrelaxFunctor
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsLEOfNat : ∀ {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 : ℤ), t.IsLE 0 n
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.support_pure : ∀ {α : Type u_1} (a : α), (PMF.pure a).support = {a}
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.setBernoulli_zero : ∀ {ι : Type u_1} (u : Set ι), ProbabilityTheory.setBernoulli u 0 = MeasureTheory.Measure.dirac ∅
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_natCast : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ), (↑n).valuation = ↑(padicValNat p n)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F),
  (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).comp
      (CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.lift F hF) =
    F
-- Batteries.Classes.Order
/-- `LawfulBCmp cmp` asserts that the `LE`, `LT`, `Eq` are all coherent with each other
and with `cmp`, describing a linear order.  -/
Std.LawfulCmp : {α : Type u_1} → [LE α] → [LT α] → (α → α → Ordering) → Prop
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a fallback : α} {c : ℕ},
  (Std.HashSet.Raw.emptyWithCapacity c).getD a fallback = fallback
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.toList.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Std.DHashMap.Internal.AssocList α β → Sort u_3) →
      (x : Std.DHashMap.Internal.AssocList α β) →
        (Unit → motive Std.DHashMap.Internal.AssocList.nil) →
          ((a : α) →
              (b : β a) →
                (es : Std.DHashMap.Internal.AssocList α β) → motive (Std.DHashMap.Internal.AssocList.cons a b es)) →
            motive x
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- The stitched together cocones each project down to the original given cocones (up to iso).  -/
CategoryTheory.Limits.evaluateCombinedCocones : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) →
                (k : K) →
                  ((CategoryTheory.evaluation K C).obj k).mapCocone (CategoryTheory.Limits.combineCocones F c) ≅
                    (c k).cocone
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prodComparisonNatTrans_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] [inst_3 : CategoryTheory.Limits.HasBinaryProducts D]
  (F : CategoryTheory.Functor C D) (A B : C),
  (CategoryTheory.Limits.prodComparisonNatTrans F A).app B = CategoryTheory.Limits.prodComparison F A B
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulC.go.induct_unfolding : ∀ (p₂ : Lean.Grind.CommRing.Poly) (c : ℕ)
  (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ),
      motive (Lean.Grind.CommRing.Poly.num k) acc (acc.combineC (Lean.Grind.CommRing.Poly.mulConstC k p₂ c) c)) →
    (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC k m p₂ c) c)
            (Lean.Grind.CommRing.Poly.mulC.go p₂ c p (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC k m p₂ c) c)) →
          motive (Lean.Grind.CommRing.Poly.add k m p) acc
            (Lean.Grind.CommRing.Poly.mulC.go p₂ c p (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC k m p₂ c) c))) →
      ∀ (p₁ acc : Lean.Grind.CommRing.Poly), motive p₁ acc (Lean.Grind.CommRing.Poly.mulC.go p₂ c p₁ acc)
-- Batteries.Data.List.Perm
List.Perm.idxBij_symm_idxBij : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) {i : Fin xs.length},
  ⋯.idxBij (h.idxBij i) = i
-- Mathlib.Logic.Basic
Ne.dite_eq_right_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {b : α} {A : P → α},
  (∀ (h : P), A h ≠ b) → ((dite P A fun x => b) = b ↔ ¬P)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.radical : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, I.IsPrime → I.radical = I
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Use the axiom of choice to extract a left adjoint from an `IsRightAdjoint` instance.  -/
CategoryTheory.Bicategory.getLeftAdjoint : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} → (f : b ⟶ a) → [CategoryTheory.Bicategory.IsRightAdjoint f] → CategoryTheory.Bicategory.LeftAdjoint f
-- Mathlib.FieldTheory.Finiteness
/-- In a Noetherian module over a division ring, there exists a finite basis.
This is indexed by the `Finset` `IsNoetherian.finsetBasisIndex`.
This is in contrast to the result `finite_basis_index (Basis.ofVectorSpace K V)`,
which provides a set and a `Set.Finite`.
 -/
IsNoetherian.finsetBasis : (K : Type u) →
  (V : Type v) →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → [inst_3 : IsNoetherian K V] → Module.Basis (↥(IsNoetherian.finsetBasisIndex K V)) K V
-- Std.Tactic.BVDecide.Syntax
/-- Run the normalization procedure of `bv_decide` only. Sometimes this is enough to solve basic
`BitVec` goals already.

Note: include `import Std.Tactic.BVDecide`
 -/
Lean.Parser.Tactic.bvNormalize : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Group.Abelian
/-- A proper geometrically integral group scheme over a field is commutative.  -/
AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral : ∀ {K : Type u} [inst : Field K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of K)))
  [AlgebraicGeometry.IsProper G.hom] [AlgebraicGeometry.GeometricallyIntegral G.hom] [inst_3 : CategoryTheory.GrpObj G],
  CategoryTheory.IsCommMonObj G
-- Mathlib.Algebra.Group.Semiconj.Defs
AddSemiconjBy.addConj_iff : ∀ {G : Type u_3} [inst : AddGroup G] {a x y b : G},
  AddSemiconjBy (b + a + -b) (b + x + -b) (b + y + -b) ↔ AddSemiconjBy a x y
-- Mathlib.Order.Interval.Finset.Defs
/-- `LocallyFiniteOrder.mk'` is the dual of `LocallyFiniteOrder.mk`, which we need for `to_dual`.
Please avoid using this directly.  -/
LocallyFiniteOrder.mk' : {α : Type u_1} →
  [inst : Preorder α] →
    (finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α) →
      (∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x) →
        (∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x) →
          (∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x) →
            (∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x) → LocallyFiniteOrder α
-- Mathlib.Logic.Relation
Relation.EqvGen.trans : ∀ {α : Type u_1} {r : α → α → Prop} (x y z : α), Relation.EqvGen r x y → Relation.EqvGen r y z → Relation.EqvGen r x z
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- The pair `f,g` is a `G`-cosplit pair if there is an `h : W ⟶ G X` so that `G f, G g, h` forms a
split equalizer in `D`.
 -/
CategoryTheory.Functor.IsCosplitPair : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → {X Y : C} → (X ⟶ Y) → (X ⟶ Y) → Prop
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.range_eq_top : ∀ {G : Type u_1} [inst : Group G] {N : Type u_7} [inst_1 : Group N] {f : G →* N}, f.range = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.Topology.Constructions.SumProd
nhds_swap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X) (y : Y),
  nhds (x, y) = Filter.map Prod.swap (nhds (y, x))
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.lTensor_surjective_iff_surjective : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_4}
  {N' : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N] [inst_6 : Module R N']
  (f : N →ₗ[R] N') [Module.FaithfullyFlat R M], Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑f
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.induction_on_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {motive : MvPolynomial σ R → Prop},
  (∀ (a : R), motive (MvPolynomial.C a)) →
    (∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * MvPolynomial.X n)) →
      ∀ (s : σ →₀ ℕ) (a : R), motive ((MvPolynomial.monomial s) a)
-- Mathlib.Data.TwoPointing
TwoPointing.to_nontrivial : ∀ {α : Type u_1} (p : TwoPointing α), Nontrivial α
-- Mathlib.Topology.ContinuousMap.Ideals
WeakDual.CharacterSpace.continuousMapEval.congr_simp : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : CommRing 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : IsTopologicalRing 𝕜] [inst_4 : Nontrivial 𝕜] [inst_5 : NoZeroDivisors 𝕜],
  WeakDual.CharacterSpace.continuousMapEval X 𝕜 = WeakDual.CharacterSpace.continuousMapEval X 𝕜
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.resRec.match_3.eq_1 : ∀ {w : ℕ} (motive : (s : ℕ) → s < w → 0 < s → Sort u_1) (hs : 0 < w) (hslt : 0 < 0)
  (h_1 : (hs : 0 < w) → (hslt : 0 < 0) → 0 = 0 → motive 0 hs hslt)
  (h_2 : (s' : ℕ) → (hs : s' + 1 < w) → (hslt : 0 < s' + 1) → 0 = s'.succ → motive s'.succ hs hslt),
  (match hs0 : 0, hs, hslt with
    | 0, hs, hslt => h_1 hs hslt hs0
    | s'.succ, hs, hslt => h_2 s' hs hslt hs0) =
    h_1 hs hslt ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- A subsemigroup `S` includes `closure s` if and only if it includes `s`.  -/
Subsemigroup.closure_le : ∀ {M : Type u_1} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, Subsemigroup.closure s ≤ S ↔ s ⊆ ↑S
-- Mathlib.Data.Nat.Cast.Defs
Nat.binCast.eq_2 : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R] [inst_2 : Add R] (n : ℕ),
  n.succ.binCast =
    if (n + 1) % 2 = 0 then ((n + 1) / 2).binCast + ((n + 1) / 2).binCast
    else ((n + 1) / 2).binCast + ((n + 1) / 2).binCast + 1
-- Mathlib.Data.Set.Basic
Set.sep_eq_of_subset : ∀ {α : Type u} {s t : Set α}, s ⊆ t → {x | x ∈ t ∧ x ∈ s} = s
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_σ : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : autoParam (n + (i + 1) = m + 1) SimplexCategory.δ₀Iter_σ._auto_1),
  autoParam (↑j ≤ i) SimplexCategory.δ₀Iter_σ._auto_3 →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter (i + 1) hi) (SimplexCategory.σ j) =
      SimplexCategory.δ₀Iter i ⋯
-- Init.Data.Nat.Dvd
Nat.dvd_mul_left_of_dvd : ∀ {a b : ℕ}, a ∣ b → ∀ (c : ℕ), a ∣ c * b
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the sphere of radius `r`
around zero `{x | v.restrict x = r}` is closed in the valuative topology.  -/
Valuation.isClosed_sphere : ∀ {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.Module.Submodule.RestrictScalars
Submodule.restrictScalars_mem : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (V : Submodule R M)
  (m : M), m ∈ Submodule.restrictScalars S V ↔ m ∈ V