mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- **Alias** of `Valuation.isClopen_ball`.

---

For any valuation `v` compatible with the valuative relation on `R`, the open `r`-ball
around zero `{x | v.restrict x < r}` is clopen in the valuative topology.  -/
IsValuativeTopology.isClopen_ball : ∀ {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₀), IsClopen {x | v.restrict x < r}
-- Mathlib.Topology.Category.LightProfinite.EffectiveEpi
LightProfinite.instPreregular : CategoryTheory.Preregular LightProfinite
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- An `O(N)` formula for the sum of the number of divisors function.  -/
ArithmeticFunction.sum_Ioc_sigma0_eq_sum_div : ∀ (N : ℕ), ∑ n ∈ Finset.Ioc 0 N, (ArithmeticFunction.sigma 0) n = ∑ n ∈ Finset.Ioc 0 N, N / n
-- Mathlib.SetTheory.Ordinal.Notation
/-- Print an ordinal notation  -/
ONote.repr' : ℕ → ONote → Std.Format
-- Init.Meta.Defs
/-- Constructs a typed separated array from elements by adding suitable separators.
The provided array should not include the separators.

Like `Syntax.SepArray.ofElems` but for typed syntax.
 -/
Lean.Syntax.TSepArray.ofElems : {k : Lean.SyntaxNodeKinds} → {sep : String} → Array (Lean.TSyntax k) → Lean.Syntax.TSepArray k sep
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.toInvtRootSubmodule_mono : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [inst_5 : CharZero K]
  [inst_6 : LieAlgebra.IsKilling K L] [inst_7 : LieModule.IsTriangularizable K (↥H) L] {I J : LieIdeal K L},
  I ≤ J → I.toInvtRootSubmodule ≤ J.toInvtRootSubmodule
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.mul_def : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (e e' : X ≃ᵈ X), e * e' = e'.trans e
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.pure_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), PMF.map f (PMF.pure a) = PMF.pure (f a)
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Meta.Grind.Params.eraseInj : Lean.Meta.Grind.Params → Lean.Name → Lean.Meta.Grind.Params
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheorem.proof : Lean.Meta.Grind.EMatchTheorem → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.HasCountableProducts.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  (∀ (J : Type) [Countable J], CategoryTheory.Limits.HasProductsOfShape J C) →
    CategoryTheory.Limits.HasCountableProducts C
-- Lean.Expr
Lean.BinderInfo.noConfusionType : Sort v✝ → Lean.BinderInfo → Lean.BinderInfo → Sort v✝
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedSolverExtension : {a : Type} → Inhabited (Lean.Meta.Grind.SolverExtension a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_insertIfNew : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a : α} {fallback v : β},
      Std.DHashMap.Raw.Const.getD (m.insertIfNew k v) a fallback =
        if (k == a) = true ∧ k ∉ m then v else Std.DHashMap.Raw.Const.getD m a fallback
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_isRestriction : ∀ {α : Type u_1} (M : Matroid α), M.removeLoops.IsRestriction M
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The morphism between Day convolutions (provided they exist) induced by a pair of morphisms.  -/
CategoryTheory.MonoidalCategory.DayConvolution.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            {F G : CategoryTheory.Functor C V} →
              [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] →
                {F' G' : CategoryTheory.Functor C V} →
                  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F' G'] →
                    (F ⟶ F') →
                      (G ⟶ G') →
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G ⟶
                          CategoryTheory.MonoidalCategory.DayConvolution.convolution F' G')
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
tendsto_iff_of_dist : ∀ {α : Type u} {ι : Type u_2} [inst : PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α},
  Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0) →
    (Filter.Tendsto f₁ p (nhds a) ↔ Filter.Tendsto f₂ p (nhds a))
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- If two sequences of functions have a.e. equal conditional expectations at each step, converge
and verify dominated convergence hypotheses, then the conditional expectations of their limits are
a.e. equal.  -/
MeasureTheory.tendsto_condExp_unique : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (fs gs : ℕ → α → E) (f g : α → E),
  (∀ (n : ℕ), MeasureTheory.Integrable (fs n) μ) →
    (∀ (n : ℕ), MeasureTheory.Integrable (gs n) μ) →
      (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => fs n x) Filter.atTop (nhds (f x))) →
        (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => gs n x) Filter.atTop (nhds (g x))) →
          ∀ (bound_fs : α → ℝ),
            MeasureTheory.Integrable bound_fs μ →
              ∀ (bound_gs : α → ℝ),
                MeasureTheory.Integrable bound_gs μ →
                  (∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x) →
                    (∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x) →
                      (∀ (n : ℕ), μ[fs n | m] =ᵐ[μ] μ[gs n | m]) → μ[f | m] =ᵐ[μ] μ[g | m]
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.of_val : ∀ {M : Type u_1} (a : MulArchimedeanOrder M), MulArchimedeanOrder.of (MulArchimedeanOrder.val a) = a
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.IsPrincipal.iSup : ∀ {op : Ordinal.{u_2} → Ordinal.{u_2} → Ordinal.{u_2}} {ι : Sort u_1} {f : ι → Ordinal.{u_2}},
  (∀ (i : ι), Ordinal.IsPrincipal op (f i)) → Ordinal.IsPrincipal op (⨆ i, f i)
-- Init.Data.SInt.Bitwise
Int64.or_not_self : ∀ {a : Int64}, a ||| ~~~a = -1
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.constructors.injEq : ∀ (constructorNames : Array Lean.Name) (md : Lean.Meta.TransparencyMode) (constructorNames_1 : Array Lean.Name)
  (md_1 : Lean.Meta.TransparencyMode),
  (Aesop.RuleTacDescr.constructors constructorNames md = Aesop.RuleTacDescr.constructors constructorNames_1 md_1) =
    (constructorNames = constructorNames_1 ∧ md = md_1)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.mk : {E : Type u_1} → {c : E} → (rIn rOut : ℝ) → 0 < rIn → rIn < rOut → ContDiffBump c
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix_mul_diagonal_eq : ∀ {ι : 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] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [inst_6 : CharZero R] [inst_7 : Fintype ι] [inst_8 : DecidableEq ι] [P.IsRootSystem],
  (b.cartanMatrix * Matrix.diagonal fun i => ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)) =
    2 • (LinearMap.BilinForm.toMatrix b.toWeightBasisInt) (P.posRootForm ℤ).posForm
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittNeg.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittNeg p = wittStructureInt p (-MvPolynomial.X 0)
-- Mathlib.CategoryTheory.Galois.Examples
/-- The category of finite sets has quotients by finite groups in arbitrary universes.  -/
CategoryTheory.FintypeCat.instHasColimitsOfShapeSingleObjFintypeCatOfFinite : ∀ (G : Type u) [inst : Group G] [Finite G],
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) FintypeCat
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_univ : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X], (Convexity.convexHull R) Set.univ = Set.univ
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
Module.Relations.Solution.IsPresentation.linearMapEquiv.congr_simp : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution solution_1 : relations.Solution M} (e_solution : solution = solution_1)
  (h : solution.IsPresentation) {N : Type v'} [inst_3 : AddCommGroup N] [inst_4 : Module A N],
  h.linearMapEquiv = ⋯.linearMapEquiv
-- Std.Http.Protocol.H1.Writer
/-- Adds user data chunks to the writer's buffer if the writer can accept data.

Empty chunks (zero bytes of data) are accepted here but will be silently dropped
during the chunked-encoding write step — see `writeChunkedBody`.
 -/
Std.Http.Protocol.H1.Writer.addUserData : {dir : Std.Http.Protocol.H1.Direction} →
  Array Std.Http.Chunk → Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Writer dir
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CaseTrace.mk : Lean.Expr → ℕ → ℕ → Lean.Meta.Grind.SplitSource → Lean.Meta.Grind.CaseTrace
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (y, x + y)` sends the measure `μ × ν` to `ν × μ`.  -/
MeasureTheory.measurePreserving_prod_add_swap_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 + z.2)) (μ.prod ν) (ν.prod μ)
-- Mathlib.LinearAlgebra.Ray
/-- A nonzero vector is in the same ray as a multiple of itself if and only if that multiple
is positive.  -/
sameRay_smul_right_iff_of_ne : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.IsTorsionFree R M] {v : M},
  v ≠ 0 → ∀ {r : R}, r ≠ 0 → (SameRay R v (r • v) ↔ 0 < r)
-- Init.SizeOf
EStateM.Result.ok.sizeOf_spec : ∀ {ε σ α : Type u} [inst : SizeOf ε] [inst_1 : SizeOf σ] [inst_2 : SizeOf α] (a : α) (a_1 : σ),
  sizeOf (EStateM.Result.ok a a_1) = 1 + sizeOf a + sizeOf a_1
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
panicking if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryGT! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap.Raw α (fun x => β) cmp → α → α × β
-- Mathlib.Analysis.SpecialFunctions.Arsinh
HasFDerivWithinAt.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a : E}
  {f' : StrongDual ℝ E},
  HasFDerivWithinAt f f' s a → HasFDerivWithinAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') s a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_periodic : Function.Periodic Real.sin (2 * Real.pi)
-- Init.Control.Lawful.MonadLift.Instances
Except.pure.eq_1 : ∀ {ε : Type u} {α : Type u_1} (a : α), Except.pure a = Except.ok a
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` is an additive group, then any function from `α` to `α` extends uniquely
to an additive homomorphism from the additive free group over `α` to `α`.  -/
FreeAddGroup.sum : {α : Type u} → [inst : AddGroup α] → FreeAddGroup α →+ α
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Centers of the balls  -/
Besicovitch.BallPackage.c : {β : Type u_1} → {α : Type u_2} → Besicovitch.BallPackage β α → β → α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_insertList_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      ∀ (contains : Std.Internal.List.containsKey k toInsert = true)
        {h : Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true},
        Std.Internal.List.getValueCast k (Std.Internal.List.insertList l toInsert) h =
          Std.Internal.List.getValueCast k toInsert contains
-- Std.Http.Data.Status
Std.Http.Status.lengthRequired.sizeOf_spec : sizeOf Std.Http.Status.lengthRequired = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.of_iso : ∀ {X : SSet} {x y : X.S},
  x.IsUniquelyCodimOneFace y →
    ∀ {Y : SSet} (e : X ≅ Y),
      { dim := x.dim,
            simplex :=
              (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := x.dim })))
                x.simplex }.IsUniquelyCodimOneFace
        { dim := y.dim,
          simplex := (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := y.dim }))) y.simplex }
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.middle.injEq : ∀ (p s p_1 s_1 : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.SubseqResult.middle p s = Lean.Grind.AC.SubseqResult.middle p_1 s_1) = (p = p_1 ∧ s = s_1)
-- Mathlib.Algebra.Homology.Double
/-- Constructor for morphisms from a homological complex `double f hi₀₁`.  -/
HomologicalComplex.mkHomFromDouble : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X₀ X₁ : C} →
          {f : X₀ ⟶ X₁} →
            {ι : Type u_2} →
              {c : ComplexShape ι} →
                {i₀ i₁ : ι} →
                  (hi₀₁ : c.Rel i₀ i₁) →
                    i₀ ≠ i₁ →
                      {K : HomologicalComplex C c} →
                        (φ₀ : X₀ ⟶ K.X i₀) →
                          (φ₁ : X₁ ⟶ K.X i₁) →
                            CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) =
                                CategoryTheory.CategoryStruct.comp f φ₁ →
                              (∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0) →
                                (HomologicalComplex.double f hi₀₁ ⟶ K)
-- Mathlib.Logic.Equiv.Sum
Equiv.sumSumSumComm_apply : ∀ (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) (a : (α ⊕ β) ⊕ γ ⊕ δ),
  (Equiv.sumSumSumComm α β γ δ) a =
    (⇑(Equiv.sumAssoc (α ⊕ γ) β δ) ∘
        Sum.map (⇑(Equiv.sumAssoc α γ β).symm) id ∘
          Sum.map (Sum.map id ⇑(Equiv.sumComm β γ)) id ∘
            Sum.map (⇑(Equiv.sumAssoc α β γ)) id ∘ ⇑(Equiv.sumAssoc (α ⊕ β) γ δ).symm)
      a
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.EStateM.adaptExcept.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s : σ)
  (h_1 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s))
  (h_2 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s)),
  (match EStateM.Result.ok a s with
    | EStateM.Result.error e s => h_1 e s
    | EStateM.Result.ok a s => h_2 a s) =
    h_2 a s
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.liftLinear.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
  (f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β)
  (hf : ∀ (μ : MeasureTheory.Measure α), inst ≤ (f μ.toOuterMeasure).caratheodory),
  MeasureTheory.Measure.liftLinear f hf =
    { toFun := fun μ => (f μ.toOuterMeasure).toMeasure ⋯, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.max_min : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (S₁ S₂ T : CategoryTheory.Subfunctor F), (S₁ ⊔ S₂) ⊓ T = S₁ ⊓ T ⊔ S₂ ⊓ T
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum.eq_1 : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M),
  s.sum f = (Multiset.map f s.val).sum
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.a.injEq : ∀ {n : ℕ} (a a_1 : ZMod (2 * n)), (QuaternionGroup.a a = QuaternionGroup.a a_1) = (a = a_1)
-- Mathlib.Data.List.Basic
/-- **Alias** of the reverse direction of `List.length_pos_iff`. -/
List.length_pos_of_ne_nil : ∀ {α : Type u_1} {l : List α}, l ≠ [] → 0 < l.length
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The new subexpression.  -/
Mathlib.Tactic.ClickSuggestions.GrwKey.replacement : Mathlib.Tactic.ClickSuggestions.GrwKey → Lean.Meta.AbstractMVarsResult
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.pullback_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (f : X ⟶ Y) (g : CategoryTheory.MonoOver Y),
  ((CategoryTheory.MonoOver.pullback f).obj g).obj.left = CategoryTheory.Limits.pullback g.arrow f
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.sUnion : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {T : Set (Set α)},
  T.Finite → (∀ t ∈ T, Absorbs M s t) → Absorbs M s (⋃₀ T)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ioi_add_Ici_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b : α),
  Set.Ioi a + Set.Ici b ⊆ Set.Ioi (a + b)
-- Lean.Meta.Sym.SymM
/-- Returns all accumulated issues without clearing them.  -/
Lean.Meta.Sym.getIssues : Lean.Meta.Sym.SymM (List Lean.MessageData)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.self_eq_add_right : ∀ {w : ℕ} (a b : BitVec w), (a == a + b) = (b == 0#w)
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- The point at infinity  -/
OnePoint.infty : {X : Type u_1} → OnePoint X
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.addCommMonoidObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommMonCat) →
      (j : J) → AddCommMonoid ((F.comp (CategoryTheory.forget AddCommMonCat)).obj j)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Option.getD.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (opt : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive opt
-- Mathlib.GroupTheory.CosetCover
Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ι → G},
  ⋃ i ∈ s, g i • ↑H = Set.univ → H.index = s.card → (↑s).PairwiseDisjoint fun x => g x • ↑H
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
/-- An expression $\sum_i m_i \otimes n_i$ in $M \otimes N$
*vanishes trivially* if there exist a finite index type $\kappa$ = `Fin k`,
elements $(y_j)_{j \in \kappa}$ of $N$, and elements $(a_{ij})_{i \in \iota, j \in \kappa}$ of $R$
such that for all $i$,
$$n_i = \sum_j a_{ij} y_j$$
and for all $j$,
$$\sum_i a_{ij} m_i = 0.$$
Note that this condition is not symmetric in $M$ and $N$.
(The terminology "trivial" comes from [Stacks 00HK](https://stacks.math.columbia.edu/tag/00HK).)  -/
TensorProduct.VanishesTrivially : (R : Type u_1) →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommGroup N] → [Module R N] → {ι : Type u_4} → [Fintype ι] → (ι → M) → (ι → N) → Prop
-- Mathlib.Algebra.BigOperators.Pi
Finset.univ_prod_mulSingle : ∀ {I : Type u_7} [inst : DecidableEq I] {M : I → Type u_8} [inst_1 : (i : I) → CommMonoid (M i)] [inst_2 : Fintype I]
  (f : (i : I) → M i), ∏ i, Pi.mulSingle i (f i) = f
-- Batteries.Data.AssocList
Batteries.AssocList.foldlM_eq : ∀ {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : δ → α → β → m δ)
  (init : δ) (l : Batteries.AssocList α β),
  Batteries.AssocList.foldlM f init l =
    List.foldlM
      (fun d x =>
        match x with
        | (a, b) => f d a b)
      init l.toList
-- Mathlib.Data.Finsupp.Order
Finsupp.sum_pos' : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedCancelAddMonoid β] [AddLeftStrictMono β] {f : ι →₀ α} {g : ι → α → β},
  (∀ i ∈ f.support, 0 ≤ g i (f i)) → (∃ i ∈ f.support, 0 < g i (f i)) → 0 < f.sum g
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.coe_finsetWalkLength_eq : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] [inst_1 : G.LocallyFinite] (n : ℕ) (u v : V),
  ↑(G.finsetWalkLength n u v) = {p | p.length = n}
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.List.findCell_inner : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : List ((a : α) × β a)) (k : α → Ordering),
  (Std.DTreeMap.Internal.List.findCell l k).inner = List.find? (fun x => k x.fst == Ordering.eq) l
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
CategoryTheory.IsSplitCoequalizer.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        {Z : C} →
          {π : Y ⟶ Z} →
            (rightSection : Z ⟶ Y) →
              (leftSection : Y ⟶ X) →
                autoParam (CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
                    CategoryTheory.IsSplitCoequalizer.condition._autoParam →
                  autoParam (CategoryTheory.CategoryStruct.comp rightSection π = CategoryTheory.CategoryStruct.id Z)
                      CategoryTheory.IsSplitCoequalizer.rightSection_π._autoParam →
                    autoParam (CategoryTheory.CategoryStruct.comp leftSection g = CategoryTheory.CategoryStruct.id Y)
                        CategoryTheory.IsSplitCoequalizer.leftSection_bottom._autoParam →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp leftSection f =
                            CategoryTheory.CategoryStruct.comp π rightSection)
                          CategoryTheory.IsSplitCoequalizer.leftSection_top._autoParam →
                        CategoryTheory.IsSplitCoequalizer f g π
-- Mathlib.LinearAlgebra.Projection
Submodule.range_projectionOnto : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q), (p.projectionOnto q h).range = ⊤
-- Mathlib.Tactic.MinImports
/-- `previousInstName nm` takes as input a name `nm`, assuming that it is the name of an
auto-generated "nameless" `instance`.
If `nm` ends in `..._n`, where `n` is a number, it returns the same name, but with `_n` replaced
by `_(n-1)`, unless `n ≤ 1`, in which case it simply removes the `_n` suffix.
 -/
Mathlib.Command.MinImports.previousInstName : Lean.Name → Lean.Name
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBVBitBVVarBlastVar : Std.Sat.AIG.LawfulVecOperator Std.Tactic.BVDecide.BVBit (fun x w => Std.Tactic.BVDecide.BVExpr.bitblast.BVVar w)
  fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastVar
-- Std.Data.Iterators.Lemmas.Consumers.Set
Std.Iter.toTreeSet_equiv_ofList : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {cmp : β → β → Ordering},
  (it.toTreeSet cmp).Equiv (Std.TreeSet.ofList it.toList cmp)
-- Mathlib.Data.Finset.Pi
Finset.pi_empty : ∀ {α : Type u_1} {β : α → Type u} [inst : DecidableEq α] {t : (a : α) → Finset (β a)}, ∅.pi t = {Finset.Pi.empty β}
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.linearization_obj_ρ : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] (X : Action (Type w) G),
  ((Rep.linearization k G).obj X).ρ = Representation.linearize k G X
-- Mathlib.Algebra.Algebra.Tower
AlgHom.extendScalarsOfSurjective_apply : ∀ {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A →ₐ[R] B),
  (AlgHom.extendScalarsOfSurjective h) f = { toRingHom := ↑f, commutes' := ⋯ }