mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.toAddGroupSeminorm : {R : Type u_2} → [inst : NonAssocRing R] → MulRingSeminorm R → AddGroupSeminorm R
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.eraseSimproc : Lean.Name → Lean.Elab.Tactic.ElabSimpArgResult
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.not_even_and_odd : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) [NeZero 2], ¬(ψ.Even ∧ ψ.Odd)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type w)},
  CategoryTheory.shrinkYonedaEquiv =
    {
      toFun := fun τ =>
        (CategoryTheory.ConcreteCategory.hom (τ.app (Opposite.op X)))
          ((equivShrink ((CategoryTheory.yoneda.obj X).obj (Opposite.op X))) (CategoryTheory.CategoryStruct.id X)),
      invFun := fun x =>
        {
          app := fun Y =>
            TypeCat.ofHom fun f =>
              (CategoryTheory.ConcreteCategory.hom
                  (P.map (Quiver.Hom.op ((equivShrink ((CategoryTheory.yoneda.obj X).obj Y)).symm f))))
                x,
          naturality := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.move_right_left : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ),
  Turing.Tape.move Turing.Dir.left (Turing.Tape.move Turing.Dir.right T) = T
-- Mathlib.GroupTheory.Torsion
AddCommGroup.isAddTorsionFree_iff_torsion_eq_bot : ∀ {G : Type u_1} [inst : AddCommGroup G], IsAddTorsionFree G ↔ AddCommGroup.torsion G = ⊥
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_filter_mul_prod_filter_not : ∀ {M : Type u_5} [inst : CommMonoid M] {s : Multiset M} (p : M → Prop) [inst_1 : DecidablePred p],
  (Multiset.filter p s).prod * (Multiset.filter (fun a => ¬p a) s).prod = s.prod
-- Init.BinderPredicates
/-- Declare `∃ x > y, ...` as syntax for `∃ x, x > y ∧ ...`  -/
Lean.«binderPred>_» : Lean.ParserDescr
-- Init.Omega.Int
Lean.Omega.Int.ofNat_pow : ∀ (a b : ℕ), ↑(a ^ b) = ↑a ^ b
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char.0.Char.reduceUnary : {α : Type u_1} →
  [Lean.ToExpr α] → Lean.Name → (Char → α) → optParam ℕ 1 → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.infinite_of_infinite : ∀ (σ : Type u_2) (R : Type u_3) [inst : CommSemiring R] [Infinite R], Infinite (MvPolynomial σ R)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
  [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {f : MeasureTheory.Filtration ι m}
  [DenselyOrdered ι] [NoMaxOrder ι] {τ : Ω → WithTop ι} [f.IsRightContinuous],
  (∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}) → MeasureTheory.IsStoppingTime f τ
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} →
      {p₁ p₂ : R ⟶ X} →
        CategoryTheory.JointlyMono₂ p₁ p₂ →
          (c : CategoryTheory.Limits.PullbackCone p₂ p₁) →
            CategoryTheory.Limits.IsLimit c →
              (t : c.pt ⟶ R) →
                autoParam (CategoryTheory.CategoryStruct.comp t p₁ = CategoryTheory.CategoryStruct.comp c.fst p₁)
                    CategoryTheory.TransitiveRelation.transitivity₁._autoParam →
                  autoParam (CategoryTheory.CategoryStruct.comp t p₂ = CategoryTheory.CategoryStruct.comp c.snd p₂)
                      CategoryTheory.TransitiveRelation.transitivity₂._autoParam →
                    CategoryTheory.TransitiveRelation p₁ p₂
-- Mathlib.Order.Types.Defs
OrderType.type_of_isEmpty : ∀ {α : Type u} [inst : LinearOrder α] [IsEmpty α], OrderType.type α = 0
-- Mathlib.Logic.Basic
Or.imp3 : ∀ {a b d e c f : Prop}, (a → d) → (b → e) → (c → f) → a ∨ b ∨ c → d ∨ e ∨ f
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.foldlM.eq_2 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (x : δ) (a : α) (b : β a) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldlM f x (Std.DHashMap.Internal.AssocList.cons a b es) = do
    let d ← f x a b
    Std.DHashMap.Internal.AssocList.foldlM f d es
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {fallback : α}, t.getKeyD t.minKey! fallback = t.minKey!
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.leftHomologyMap_smul : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (φ : S₁ ⟶ S₂) (a : R) [inst_4 : S₁.HasLeftHomology] [inst_5 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.leftHomologyMap (a • φ) = a • CategoryTheory.ShortComplex.leftHomologyMap φ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.cancelVar : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Var → Lean.Grind.CommRing.Mon
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.tsum_sigma' : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousAdd α] [T3Space α]
  {γ : β → Type u_4} {f : (b : β) × γ b → α},
  (∀ (b : β), Summable fun c => f ⟨b, c⟩) → Summable f → ∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f ⟨b, c⟩
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
/-- Eta-expanded form of `ProbabilityTheory.BrownianReal.covariance_projectiveFamily` -/
ProbabilityTheory.BrownianReal.covariance_fun_projectiveFamily : ∀ (I : Finset NNReal) (f g : (↥I → ℝ) → ℝ),
  ProbabilityTheory.covariance f g (ProbabilityTheory.BrownianReal.projectiveFamily I) =
    ProbabilityTheory.covariance (fun x => f x.ofLp) (fun x => g x.ofLp)
      (ProbabilityTheory.multivariateGaussian 0 (ProbabilityTheory.BrownianReal.covMatrix I))
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- We do not get `ae_fin_strongly_measurable f (μ.trim hm)`, since we don't have
`f =ᵐ[μ.trim hm] Lp_meas_to_Lp_trim F 𝕜 p μ hm f` but only the weaker
`f =ᵐ[μ] Lp_meas_to_Lp_trim F 𝕜 p μ hm f`.  -/
MeasureTheory.lpMeas.ae_fin_strongly_measurable' : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
  (f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)),
  p ≠ 0 → p ≠ ⊤ → ∃ g, MeasureTheory.FinStronglyMeasurable g (μ.trim hm) ∧ ↑↑↑f =ᵐ[μ] g
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_of_finite : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (s : Set A),
  (∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val) → AlgebraicIndependent R Subtype.val
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.List.range_succ_eq_map' : ∀ {n nn n' : ℕ}, Mathlib.Meta.NormNum.IsNat n nn → nn = n'.succ → List.range n = 0 :: List.map Nat.succ (List.range n')
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- This is the reversed definition of `mu`, which is equal to `mu` but easiest to prove equal by
showing that `zeta * mu = 1` and `mu' * zeta = 1`.  -/
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.mu' : (𝕜 : Type u_2) →
  {α : Type u_5} →
    [inst : AddCommGroup 𝕜] →
      [One 𝕜] → [inst_2 : Preorder α] → [LocallyFiniteOrder α] → [DecidableEq α] → IncidenceAlgebra 𝕜 α
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement'_top_left : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ⊤.IsComplement' H ↔ H = ⊥
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t₁ t₂ : Finset α}, s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂
-- Init.Data.Array.Lex.Lemmas
Array.not_lt : ∀ {α : Type u_1} [inst : LT α] {xs ys : Array α}, ¬xs < ys ↔ ys ≤ xs
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- In a Noetherian ring, every ideal contains a product of prime ideals
([samuel1967, § 3.3, Lemma 3]).  -/
PrimeSpectrum.exists_primeSpectrum_prod_le : ∀ (R : Type u) [inst : CommRing R] [IsNoetherianRing R] (I : Ideal R),
  ∃ Z, (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
-- Mathlib.Order.Heyting.Basic
sup_sdiff_eq_sup : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, c ≤ a → a ⊔ b \ c = a ⊔ b
-- Lean.Meta.Tactic.Revert
/-- Revert free variables `fvarIds` at goal `mvarId`.
 -/
Lean.MVarId.revert : Lean.MVarId →
  Array Lean.FVarId → optParam Bool false → optParam Bool false → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Init.Data.Function
Function.LeftInverse.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} (g : β → α) (f : α → β), Function.LeftInverse g f = ∀ (x : α), g (f x) = x
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_of_get?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k k' : α}, m.get? k = some k' → k' ∈ m
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.associated_of_irreducible : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] {a b : R},
  Irreducible a → Irreducible b → Associated a b
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
EuclideanGeometry.angle_smul_right_of_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ : P) {p₂ p₃ p₄ : P} {r : ℝ},
  0 < r → r • (p₄ -ᵥ p₂) = p₃ -ᵥ p₂ → EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₂ p₄
-- Mathlib.Analysis.InnerProductSpace.l2Space
IsHilbertSum.linearIsometryEquiv.eq_1 : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  (hV : IsHilbertSum 𝕜 G V), hV.linearIsometryEquiv = (LinearIsometryEquiv.ofSurjective ⋯.linearIsometry ⋯).symm
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.findSome?`.

Examples:
 * `[7, 6, 5, 8, 1, 2, 6].iter.ensureTermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
 * `[7, 6, 5, 8, 1, 2, 6].iter.ensureTermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
Std.Iter.Total.findSome? : {α β : Type w} →
  {γ : Type x} →
    [inst : Std.Iterator α Id β] →
      [Std.IteratorLoop α Id Id] → [Std.Iterators.Finite α Id] → Std.Iter.Total β → (β → Option γ) → Option γ
-- Mathlib.Order.RelSeries
LTSeries.longestOf_is_longest : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : FiniteDimensionalOrder α] (x : LTSeries α),
  x.length ≤ (LTSeries.longestOf α).length
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.arithExt : Lean.Meta.Sym.SymExtension Lean.Meta.Sym.Arith.State
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsAffineMap.sub : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M]
  [inst_9 : Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] {f g : M → N},
  Convexity.IsAffineMap R f → Convexity.IsAffineMap R g → Convexity.IsAffineMap R (f - g)
-- Mathlib.Analysis.Convex.Approximation
/-- The real version of `sSup_affine_eq`.  -/
ConvexOn.real_sSup_affine_eq : ∀ {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E],
  IsClosed s →
    LowerSemicontinuousOn φ s →
      ConvexOn ℝ s φ →
        sSup {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict ⇑l + Function.const (↑s) c} = s.domRestrict φ
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapDomain.toLinearMap_linearEquiv : ∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_9} (f : α ≃ α'), ↑(Finsupp.mapDomain.linearEquiv M R f) = Finsupp.lmapDomain M R ⇑f
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.forIn'_eq_match_step.match_3.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- As for products, any functor between categories with binary biproducts gives rise to a
morphism `F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y`.  -/
CategoryTheory.Functor.biprodComparison : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              (X Y : C) →
                [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
                  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] →
                    F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y
-- Mathlib.Logic.Relation
Relation.map_equivalence : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop},
  Equivalence r →
    ∀ (f : α → β), Function.Surjective f → (∀ (x y : α), f x = f y → r x y) → Equivalence (Relation.Map r f f)
-- Mathlib.Order.Filter.Basic
/-- Weaker version of `Filter.iInter_mem` that assumes `Subsingleton β` rather than `Finite β`.  -/
Filter.iInter_mem' : ∀ {α : Type u} {f : Filter α} {β : Sort v} {s : β → Set α} [Subsingleton β], ⋂ i, s i ∈ f ↔ ∀ (i : β), s i ∈ f
-- Mathlib.LinearAlgebra.Span.TensorProduct
/-- If `A` is a flat epi `R`-algebra and `p` is an `R`-submodule of an `A`-module `M` then the
natural surjection from `A ⊗[R] p` to `span A p` is an equivalence.  -/
Submodule.tensorEquivSpan : {R : Type u_1} →
  (A : Type u_2) →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module A M] →
                  [IsScalarTower R A M] →
                    (p : Submodule R M) →
                      [Algebra.IsEpi R A] → [Module.Flat R A] → TensorProduct R A ↥p ≃ₗ[A] ↥(Submodule.span A ↑p)
-- Lean.Environment
Lean.ConstantKind.thm : Lean.ConstantKind
-- Mathlib.Algebra.Module.LinearMap.Defs
SemilinearMapClass.mk : ∀ {F : Type u_14} {R : outParam (Type u_15)} {S : outParam (Type u_16)} [inst : Semiring R] [inst_1 : Semiring S]
  {σ : outParam (R →+* S)} {M : outParam (Type u_17)} {M₂ : outParam (Type u_18)} [inst_2 : AddCommMonoid M]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] [inst_6 : FunLike F M M₂]
  [toAddHomClass : AddHomClass F M M₂] [toMulActionSemiHomClass : MulActionSemiHomClass F (⇑σ) M M₂],
  SemilinearMapClass F σ M M₂
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainOfBialgHom.congr_simp : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H] (f f_1 : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H),
  f = f_1 → MonoidAlgebra.mapDomainOfBialgHom f = MonoidAlgebra.mapDomainOfBialgHom f_1
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (n : ℤ) {e : M},
  e ≠ 0 →
    ∀ {L l l' : Mathlib.Tactic.FieldSimp.NF M},
      L.eval * l.eval = l'.eval → ((n, e) ::ᵣ L).eval * ((-n, e) ::ᵣ l).eval = l'.eval
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget₂CommMon_obj_one : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C),
  CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
-- Lean.Elab.InfoTree.Types
Lean.Elab.TermInfo.mk.injEq : ∀ (toElabInfo : Lean.Elab.ElabInfo) (lctx : Lean.LocalContext) (expectedType? : Option Lean.Expr) (expr : Lean.Expr)
  (isBinder isDisplayableTerm : Bool) (toElabInfo_1 : Lean.Elab.ElabInfo) (lctx_1 : Lean.LocalContext)
  (expectedType?_1 : Option Lean.Expr) (expr_1 : Lean.Expr) (isBinder_1 isDisplayableTerm_1 : Bool),
  ({ toElabInfo := toElabInfo, lctx := lctx, expectedType? := expectedType?, expr := expr, isBinder := isBinder,
        isDisplayableTerm := isDisplayableTerm } =
      { toElabInfo := toElabInfo_1, lctx := lctx_1, expectedType? := expectedType?_1, expr := expr_1,
        isBinder := isBinder_1, isDisplayableTerm := isDisplayableTerm_1 }) =
    (toElabInfo = toElabInfo_1 ∧
      lctx = lctx_1 ∧
        expectedType? = expectedType?_1 ∧
          expr = expr_1 ∧ isBinder = isBinder_1 ∧ isDisplayableTerm = isDisplayableTerm_1)
-- Mathlib.RingTheory.Polynomial.Quotient
/-- If `I` is an ideal of `R`, then the ring `MvPolynomial σ I.quotient` is isomorphic as an
`R`-algebra to the quotient of `MvPolynomial σ R` by the ideal generated by `I`.  -/
MvPolynomial.quotientEquivQuotientMvPolynomial : {R : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing R] → (I : Ideal R) → MvPolynomial σ (R ⧸ I) ≃ₐ[R] MvPolynomial σ R ⧸ Ideal.map MvPolynomial.C I
-- Mathlib.RingTheory.Ideal.Quotient.Defs
/-- Two `RingHom`s from the quotient by an ideal are equal if their
compositions with `Ideal.Quotient.mk'` are equal.

See note [partially-applied ext lemmas].  -/
Ideal.Quotient.ringHom_ext : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} {S : Type v} [inst_1 : I.IsTwoSided] [inst_2 : NonAssocSemiring S]
  ⦃f g : R ⧸ I →+* S⦄, f.comp (Ideal.Quotient.mk I) = g.comp (Ideal.Quotient.mk I) → f = g
-- Init.Data.Option.Lemmas
Option.pelim_pfilter : ∀ {α : Type u_1} {β : Sort u_2} {o : Option α} {b : β} {p : (a : α) → o = some a → Bool}
  {f : (a : α) → o.pfilter p = some a → β},
  (o.pfilter p).pelim b f = o.pelim b fun a ha => if hp : p a ha = true then f a ⋯ else b
-- Init.Data.UInt.Lemmas
UInt64.toFin_ofBitVec : ∀ {b : BitVec 64}, { toBitVec := b }.toFin = b.toFin
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Submodule.tmul_mem_baseChange_of_mem : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {p : Submodule R M} (a : A) {m : M},
  m ∈ p → a ⊗ₜ[R] m ∈ Submodule.baseChange A p
-- Init.Data.BitVec.Basic
/-- Bitwise and for bitvectors. Usually accessed via the `&&&` operator.

SMT-LIB name: `bvand`.

Example:
* `0b1010#4 &&& 0b0110#4 = 0b0010#4`
 -/
BitVec.and : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.associator_inv_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F₁ F₂ F₃ : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.MonoidalCategoryStruct.associator F₁ F₂ F₃).inv.app j =
    (CategoryTheory.MonoidalCategoryStruct.associator (F₁.obj j) (F₂.obj j) (F₃.obj j)).inv
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
fderiv_clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {x : E}
  {H : Type u_5} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G},
  DifferentiableAt 𝕜 c x →
    DifferentiableAt 𝕜 u x → fderiv 𝕜 (fun y => (c y) (u y)) x = c x ∘SL fderiv 𝕜 u x + (fderiv 𝕜 c x).flip (u x)
-- Mathlib.Topology.Constructions.SumProd
Continuous.prodMk : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : Z → X} {g : Z → Y}, Continuous f → Continuous g → Continuous fun x => (f x, g x)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- If every element belongs to exactly `n` Finsets, then the sum of their sizes is `n` times how
many they are.  -/
Finset.sum_card_inter : ∀ {α : Type u_2} [inst : DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ},
  (∀ a ∈ s, {b ∈ B | a ∈ b}.card = n) → ∑ t ∈ B, (s ∩ t).card = s.card * n
-- Mathlib.RingTheory.Unramified.Field
Algebra.FormallyUnramified.isReduced_of_field : ∀ (K : Type u_1) (A : Type u_2) [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A]
  [Algebra.FormallyUnramified K A] [Algebra.EssFiniteType K A], IsReduced A
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.gp_le : ∀ {l : BoxIntegral.IntegrationParams}, BoxIntegral.IntegrationParams.GP ≤ l
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.trans : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet.Raw α cmp}, t₁.Equiv t₂ → t₂.Equiv t₃ → t₁.Equiv t₃
-- Mathlib.Algebra.Group.Int.Defs
Int.instAddGroup : AddGroup ℤ
-- Mathlib.Data.List.TakeDrop
List.takeD_left : ∀ {α : Type u} (l₁ l₂ : List α) (a : α), List.takeD l₁.length (l₁ ++ l₂) a = l₁
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.mem_extended_iff : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  (I : FractionalIdeal M K) (x : L),
  x ∈ FractionalIdeal.extended L hf I ↔ x ∈ Submodule.span B (⇑(IsLocalization.map L f hf) '' ↑I)
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
/-- A root pairing is irreducible if it is non-trivial and contains no proper invariant submodules.
 -/
RootPairing.IsIrreducible : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → Prop
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion.sizeOf_spec : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} [inst_5 : SizeOf R]
  [inst_6 : SizeOf K] (toCompletion : (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion),
  sizeOf { toCompletion := toCompletion } = 1 + sizeOf toCompletion