mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.sSup_def : ∀ {M : Type u_1} [inst : AddZeroClass M] {f : Set (SaturatedAddSubmonoid M)},
  sSup f = (sSup (SaturatedAddSubmonoid.toAddSubmonoid '' f)).saturation
-- Mathlib.Algebra.Group.Subgroup.Map
/-- The image of a subgroup along a monoid homomorphism is a subgroup.  -/
Subgroup.map : {G : Type u_1} → [inst : Group G] → {N : Type u_5} → [inst_1 : Group N] → (G →* N) → Subgroup G → Subgroup N
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mem_coeIdeal_of_mem : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {x : R} {I : Ideal R}, x ∈ I → (algebraMap R P) x ∈ ↑I
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between a vector and the zero vector.  -/
InnerProductGeometry.angle_zero_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x : V),
  InnerProductGeometry.angle x 0 = Real.pi / 2
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.lattice_eq_span_range_basis : ∀ (L : PeriodPair), L.lattice = Submodule.span ℤ (Set.range ⇑L.basis)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_le_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : LE β] [l.NeBot] {x y : β}, ↑x ≤ ↑y ↔ x ≤ y
-- Lean.Meta.CongrTheorems
/-- Variant of `getCongrSimpKinds` for rewriting just argument 0.
If it is possible to rewrite, the 0th `CongrArgKind` is `.eq`,
and otherwise it is `.fixed`. This is used for the `arg` conv tactic.
 -/
Lean.Meta.getCongrSimpKindsForArgZero : Lean.Meta.FunInfo → Lean.MetaM (Array Lean.Meta.CongrArgKind)
-- Mathlib.Analysis.Normed.Group.Basic
NormedAddGroup.uniformity_basis_dist : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], (uniformity E).HasBasis (fun ε => 0 < ε) fun ε => {p | ‖-p.1 + p.2‖ < ε}
-- Lean.DocString.DeferredCheck
/-- The check-specific data. The name of the type in the `Dynamic` determines which checks are to be
performed.
  -/
Lean.Doc.DeferredCheck.check : Lean.Doc.DeferredCheck → Dynamic
-- Mathlib.RingTheory.Ideal.Maps
Module.annihilator_finsupp : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  [Nonempty ι], Module.annihilator R (ι →₀ M) = Module.annihilator R M
-- Init.Data.Int.Order
Int.mul_neg_of_pos_of_neg : ∀ {a b : ℤ}, 0 < a → b < 0 → a * b < 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {hc : t.maxKey he ∈ t}, t.getKey (t.maxKey he) hc = t.maxKey he
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.toPiFork_π_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I)
  {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right}
  (hd : CategoryTheory.Limits.IsLimit d),
  (CategoryTheory.Limits.Multifork.toPiFork hc hd K).π.app CategoryTheory.Limits.WalkingParallelPair.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.fstPiMapOfIsLimit c hd)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_inter_le_size_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (m₁ ∩ m₂).size ≤ m₂.size
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {F : CategoryTheory.Limits.MonoFactorisation f} →
          (lift : (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I) →
            autoParam
                (∀ (F' : CategoryTheory.Limits.MonoFactorisation f),
                  CategoryTheory.CategoryStruct.comp (lift F') F'.m = F.m)
                CategoryTheory.Limits.IsImage.lift_fac._autoParam →
              CategoryTheory.Limits.IsImage F
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMon_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X Y : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N]
  (α : CategoryTheory.yonedaMonObj M ⟶ CategoryTheory.yonedaMonObj N) (f : X ⟶ Y) (g : Y ⟶ M),
  (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves finite limits, then `F.leftOp : Cᵒᵖ ⥤ D` preserves finite
colimits.  -/
CategoryTheory.Limits.preservesFiniteColimits_leftOp : ∀ {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.PreservesFiniteLimits F],
  CategoryTheory.Limits.PreservesFiniteColimits F.leftOp
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
_private.Mathlib.Algebra.SkewMonoidAlgebra.Basic.0.SkewMonoidAlgebra.add.match_1.splitter : {k : Type u_1} →
  {G : Type u_2} →
    [inst : AddMonoid k] →
      (motive : SkewMonoidAlgebra k G → SkewMonoidAlgebra k G → Sort u_3) →
        (x x_1 : SkewMonoidAlgebra k G) → ((a b : G →₀ k) → motive { coeff := a } { coeff := b }) → motive x x_1
-- Lean.Meta.Tactic.Split
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.generalizeMatchDiscrs.mkNewTarget : Lean.Name →
  Array Lean.Expr →
    Lean.Meta.MatcherInfo → ℕ → Array Lean.Expr → Array Lean.Expr → IO.Ref Bool → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The proposition that the function preserves multiplication  -/
MulDistribMulActionHom.map_mul' : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  (self : A →ₑ*[φ] B) (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.DTreeMap.Const.get? (Std.DTreeMap.Const.ofList l cmp) k' = some v
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instIsSmallOfHomsFinHAddNatOfNatιHorn : ∀ (n : ℕ),
  CategoryTheory.MorphismProperty.IsSmall.{u, u, u + 1}
    (CategoryTheory.MorphismProperty.ofHoms fun i => (SSet.horn (n + 1) i).ι)
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.r.match_1.splitter : (α : Type u_1) →
  (motive : α × α → α × α → Sort u_2) → (x x_1 : α × α) → ((a b c d : α) → motive (a, b) (c, d)) → motive x x_1
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.inverseCoeff.congr_simp : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (a a_1 : kˣ),
  a = a_1 →
    ∀ (A A_1 : WittVector p k),
      A = A_1 → ∀ (a_2 a_3 : ℕ), a_2 = a_3 → WittVector.inverseCoeff a A a_2 = WittVector.inverseCoeff a_1 A_1 a_3
-- Mathlib.Data.Seq.Defs
Stream'.Seq.get?_cons_succ : ∀ {α : Type u} (a : α) (s : Stream'.Seq α) (n : ℕ), (Stream'.Seq.cons a s).get? (n + 1) = s.get? n
-- Mathlib.LinearAlgebra.Multilinear.Curry
multilinearCurryLeftEquiv_symm_apply : ∀ (R : Type uR) {n : ℕ} (M : Fin n.succ → Type v) (M₂ : Type v₂) [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂]
  (f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂), (multilinearCurryLeftEquiv R M M₂).symm f = f.uncurryLeft
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toArray_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {f : (a : α) → β a → Option (γ a)},
  t.WF →
    (Std.DTreeMap.Internal.Impl.filterMap! f t).toArray =
      Array.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toArray
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.zipWith.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (x : List α) (x_1 : List β)
  (h_1 : (x : α) → (xs : List α) → (y : β) → (ys : List β) → motive (x :: xs) (y :: ys))
  (h_2 : (x : List α) → (x_2 : List β) → motive x x_2),
  (∀ (x_2 : α) (xs : List α) (y : β) (ys : List β), x = x_2 :: xs → x_1 = y :: ys → False) →
    (match x, x_1 with
      | x :: xs, y :: ys => h_1 x xs y ys
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.comap_toSubmonoid : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (s : Subsemiring S),
  (Subsemiring.comap f s).toSubmonoid = { carrier := ⇑f ⁻¹' ↑s, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Algebra.Order.UpperLower
lowerClosure_mul_distrib : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s t : Set α),
  lowerClosure (s * t) = lowerClosure s * lowerClosure t
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.equivOplax_apply : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G}
  (Γ : (CategoryTheory.Oplax.StrongTrans.toOplax η).Modification (CategoryTheory.Oplax.StrongTrans.toOplax θ)),
  CategoryTheory.Oplax.StrongTrans.Modification.equivOplax Γ = CategoryTheory.Oplax.StrongTrans.Modification.mkOfOplax Γ
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyonedaType_map_app : ∀ {X Y : Type uᵒᵖ} (f : X ⟶ Y) (N : CommMonCat),
  (CommMonCat.coyonedaType.map f).app N =
    CommMonCat.ofHom
      (MonoidHom.pi fun i => Pi.evalMonoidHom (fun a => ↑N) ((CategoryTheory.ConcreteCategory.hom f.unop) i))
-- Mathlib.Topology.Separation.Basic
/-- In an R₀ space, `Specializes` implies `Inseparable`.  -/
Specializes.inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R0Space X] {x y : X}, x ⤳ y → Inseparable x y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_insertListConst_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)}
  {k : α} {fallback : β},
  (List.map Prod.fst toInsert).contains k = false →
    Std.Internal.List.getValueD k (Std.Internal.List.insertListConst l toInsert) fallback =
      Std.Internal.List.getValueD k l fallback
-- Mathlib.Analysis.Calculus.VectorField
VectorField.pullback_eq_of_fderiv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {M : E ≃L[𝕜] F} {x : E}, ↑M = fderiv 𝕜 f x → ∀ (V : F → F), VectorField.pullback 𝕜 f V x = M.symm (V (f x))
-- Init.NotationExtra
«term∃_,_» : Lean.ParserDescr
-- Mathlib.Topology.Sheaves.Presheaf
/-- If `f '' U` is open, then `f⁻¹ℱ U ≅ ℱ (f '' U)`.  -/
TopCat.Presheaf.pullbackObjObjOfImageOpen : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} →
        (f : X ⟶ Y) →
          (ℱ : TopCat.Presheaf C Y) →
            (U : TopologicalSpace.Opens ↑X) →
              (H : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U)) →
                ((TopCat.Presheaf.pullback C f).obj ℱ).obj (Opposite.op U) ≅
                  ℱ.obj (Opposite.op { carrier := ⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U, is_open' := H })
-- Mathlib.Data.Set.Lattice
Function.Surjective.iUnion_comp : ∀ {α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {f : ι → ι₂},
  Function.Surjective f → ∀ (g : ι₂ → Set α), ⋃ x, g (f x) = ⋃ y, g y
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Antitone.add_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} [AddRightMono α],
  Antitone f → ∀ (a : α), Antitone fun x => f x + a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- A commutative monoid object is a commutative monoid object in the category of monoid objects.  -/
CategoryTheory.Mon.instIsCommMonObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M : CategoryTheory.Mon C} [inst_3 : CategoryTheory.IsCommMonObj M.X],
  CategoryTheory.IsCommMonObj M
-- Lean.Linter.Init
Lean.Linter.getEnvLinterSnapshotEntry? : Lean.Environment → Lean.Name → Lean.Name → Option Bool
-- Mathlib.RingTheory.Regular.RegularSequence
Ideal.map_ofList : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (rs : List R),
  Ideal.map f (Ideal.ofList rs) = Ideal.ofList (List.map (⇑f) rs)
-- Lean.Server.FileWorker.Utils
/-- Initial processing snapshot.  -/
Lean.Server.FileWorker.EditableDocumentCore.initSnap : Lean.Server.FileWorker.EditableDocumentCore → Lean.Language.Lean.InitialSnapshot
-- Mathlib.Order.Filter.Pointwise
Filter.add.instNeBot : ∀ {α : Type u_2} [inst : Add α] {f g : Filter α} [f.NeBot] [g.NeBot], (f + g).NeBot
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_mul_C : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R],
  a ≠ 0 → (p * Polynomial.C a).natDegree = p.natDegree
-- Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
GenContFract.contsAux_recurrence : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K] {gp ppred pred : GenContFract.Pair K},
  g.s.get? n = some gp →
    g.contsAux n = ppred →
      g.contsAux (n + 1) = pred →
        g.contsAux (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.coe_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P) [inst_4 : Nonempty ↥s] (a b : ↥s), ↑(a -ᵥ b) = ↑a -ᵥ ↑b
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_le_self : ∀ (n : ℕ), n.sqrt ≤ n
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Pos.Raw.get?.match_1.eq_1 : ∀ (motive : String → String.Pos.Raw → Sort u_1) (s : String) (p : String.Pos.Raw)
  (h_1 : (s : String) → (p : String.Pos.Raw) → motive s p),
  (match s, p with
    | s, p => h_1 s p) =
    h_1 s p
-- Mathlib.Order.Bounds.Basic
upperBounds_mono_set : ∀ {α : Type u_1} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → upperBounds t ⊆ upperBounds s
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.mk : {A : Type u_1} →
  {B : Type u_2} →
    [inst : Add A] →
      [inst_1 : Add B] →
        [inst_2 : Mul A] →
          [inst_3 : Mul B] →
            [inst_4 : Star A] →
              [inst_5 : Star B] →
                (toRingEquiv : A ≃+* B) →
                  (∀ (a : A), toRingEquiv.toFun (star a) = star (toRingEquiv.toFun a)) → A ≃⋆+* B
-- Mathlib.Algebra.Order.Group.Action.Flag
Flag.instMulActionOrderIso : {α : Type u_1} → [inst : Preorder α] → MulAction (α ≃o α) (Flag α)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- A morphism of additive monoid objects induces a "restriction" or "comap" functor
between the categories of additive module objects.  -/
CategoryTheory.AddMod.comap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A B : C} →
              [inst_4 : CategoryTheory.AddMonObj A] →
                [inst_5 : CategoryTheory.AddMonObj B] →
                  (f : A ⟶ B) →
                    [CategoryTheory.IsAddMonHom f] →
                      CategoryTheory.Functor (CategoryTheory.AddMod D B) (CategoryTheory.AddMod D A)
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiff.differentiable_deriv_two : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F}, ContDiff 𝕜 2 f → Differentiable 𝕜 (deriv f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_le_size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List ((a : α) × β a)}, t.size ≤ (t.insertMany l).size
-- Mathlib.Data.List.Lookmap
List.lookmap_id' : ∀ {α : Type u_1} (f : α → Option α), (∀ (a b : α), b ∈ f a → a = b) → ∀ (l : List α), List.lookmap f l = l
-- Mathlib.Data.Num.Lemmas
PosNum.testBit.eq_def : ∀ (x : PosNum) (x_1 : ℕ),
  x.testBit x_1 =
    match x, x_1 with
    | PosNum.one, 0 => true
    | PosNum.one, x => false
    | a.bit0, 0 => false
    | p.bit0, n.succ => p.testBit n
    | a.bit1, 0 => true
    | p.bit1, n.succ => p.testBit n
-- Init.Data.List.MinMax
List.isSome_max?_iff : ∀ {α : Type u_1} [inst : Max α] {xs : List α}, xs.max?.isSome = true ↔ xs ≠ []
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasGoodReduction.not_hasAdditiveReduction : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K},
  WeierstrassCurve.HasGoodReduction R W → ¬WeierstrassCurve.HasAdditiveReduction R W
-- Mathlib.Data.Nat.SuccPred
withBotSucc_zero : WithBot.succ 0 = 1
-- Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal
Submodule.le_orthogonalBilin_orthogonalBilin : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_4} {M₁ : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring R₁]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁] {I₁ : R₁ →+* R}
  {S : Submodule R₁ M₁} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M},
  B.IsRefl → S ≤ Submodule.orthogonalBilin B (Submodule.orthogonalBilin B S)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A cokernel cofork for the cokernel of `BinaryBicone.inr`. It consists of the morphism
`BinaryBicone.fst`.  -/
CategoryTheory.Limits.BinaryBicone.inrCokernelCofork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (c : CategoryTheory.Limits.BinaryBicone X Y) → CategoryTheory.Limits.CokernelCofork c.inr
-- Mathlib.Combinatorics.Matroid.Circuit
/-- For an independent set `I` and some `e ∈ M.closure I \ I`,
`M.fundCircuit e I` is the unique circuit contained in `insert e I`.
For the fact that this is a circuit, see `Matroid.Indep.fundCircuit_isCircuit`,
and the fact that it is unique, see `Matroid.IsCircuit.eq_fundCircuit_of_subset`.
Has the junk value `{e}` if `e ∈ I` or `e ∉ M.E`, and `insert e I` if `e ∈ M.E \ M.closure I`.  -/
Matroid.fundCircuit : {α : Type u_1} → Matroid α → α → Set α → Set α
-- Mathlib.Algebra.MvPolynomial.Rename
/-- `MvPolynomial.rename e` is an equivalence when `e` is.  -/
MvPolynomial.renameEquiv : {σ : Type u_1} →
  {τ : Type u_2} → (R : Type u_4) → [inst : CommSemiring R] → σ ≃ τ → MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift'_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : ℕ × M → A} (hf_zero : ∀ (m : M), f (0, m) = 1)
  (hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m))
  (hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m))
  (hf_add :
    ∀ (n : ℕ) (u v : M),
      f (n, u + v) =
        ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
          match x with
          | (k, l) => f (k, u) * f (l, v))
  (p : MvPolynomial (ℕ × M) R), (DividedPowerAlgebra.lift' hf_zero hf_smul hf_mul hf_add) ↑p = (MvPolynomial.aeval f) p
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.iUnion_smul_eq_ofPred_exists : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s : Set β}, ⋃ g, g • s = {a | ∃ g, g • a ∈ s}
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.instSurjectiveOfGeometricallyIrreducible : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyIrreducible f],
  AlgebraicGeometry.Surjective f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (k : α),
  t.getEntry? k =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => none
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match compare k k' with
      | Ordering.lt => l.getEntry? k
      | Ordering.gt => r.getEntry? k
      | Ordering.eq => some ⟨k', v'⟩
-- Mathlib.Tactic.Linter.Style
/-- The `dollarSyntax` linter flags uses of `<|` that are achieved by typing `$`.
These are disallowed by the mathlib style guide, as using `<|` pairs better with `|>`.  -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.dollarSyntax.dollarSyntaxLinter : Lean.Linter
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.Scheme.affineOpens.eq_1 : ∀ (X : AlgebraicGeometry.Scheme), X.affineOpens = {U | AlgebraicGeometry.IsAffineOpen U}
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The converse: if the additive character takes the value `1` only at `0`,
then it is primitive.  -/
AddChar.zmod_char_primitive_of_eq_one_only_at_zero : ∀ {C : Type v} [inst : CommMonoid C] (n : ℕ) (ψ : AddChar (ZMod n) C), (∀ (a : ZMod n), ψ a = 1 → a = 0) → ψ.IsPrimitive
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum.preimage_algebraMap : ∀ (S : Type u_3) {R : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Algebra R S] [inst_4 : Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [inst_7 : Module R A]
  [IsScalarTower R S A] {a : A}, ⇑(algebraMap R S) ⁻¹' quasispectrum S a = quasispectrum R a
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.add.match_3.eq_2 : ∀ (motive : Dyadic → Dyadic → Sort u_1) (x : Dyadic) (h_1 : (y : Dyadic) → motive Dyadic.zero y)
  (h_2 : (x : Dyadic) → motive x Dyadic.zero)
  (h_3 :
    (n₁ k₁ : ℤ) →
      (hn₁ : n₁ % 2 = 1) → (n₂ k₂ : ℤ) → (hn₂ : n₂ % 2 = 1) → motive (Dyadic.ofOdd n₁ k₁ hn₁) (Dyadic.ofOdd n₂ k₂ hn₂)),
  (x = Dyadic.zero → False) →
    (match x, Dyadic.zero with
      | Dyadic.zero, y => h_1 y
      | x, Dyadic.zero => h_2 x
      | Dyadic.ofOdd n₁ k₁ hn₁, Dyadic.ofOdd n₂ k₂ hn₂ => h_3 n₁ k₁ hn₁ n₂ k₂ hn₂) =
      h_2 x
-- Init.Tactics
/-- * `symm` applies to a goal whose target has the form `t ~ u` where `~` is a symmetric relation,
  that is, a relation which has a symmetry lemma tagged with the attribute [symm].
  It replaces the target with `u ~ t`.
* `symm at h` will rewrite a hypothesis `h : t ~ u` to `h : u ~ t`.
 -/
Lean.Parser.Tactic.symm : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- `∫⁻ a in s, f a ∂μ` is defined as the supremum of integrals of simple functions
`φ : α →ₛ ℝ≥0∞` such that `φ ≤ f`. This lemma says that it suffices to take
functions `φ : α →ₛ ℝ≥0`.  -/
MeasureTheory.lintegral_eq_nnreal : ∀ {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal) (μ : MeasureTheory.Measure α),
  ∫⁻ (a : α), f a ∂μ =
    ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ
-- Mathlib.Tactic.Push
/-- Run the `push` tactic.  -/
Mathlib.Tactic.Push.push : Mathlib.Tactic.Push.Config →
  Option Lean.Meta.Simp.Discharge →
    Mathlib.Tactic.Push.Head →
      Lean.Elab.Tactic.Location →
        optParam Mathlib.Tactic.BehaviorIfUnchanged Mathlib.Tactic.BehaviorIfUnchanged.error →
          Lean.Elab.Tactic.TacticM Unit