mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
/-- The SummationFilter on a locally finite order `G` corresponding to the symmetric
intervals `Icc (-N) N`·  -/
SummationFilter.symmetricIcc : (G : Type u_1) → [Neg G] → [inst : Preorder G] → [LocallyFiniteOrder G] → SummationFilter G
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.typesCartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory (Type u)
-- Mathlib.Order.Hom.CompleteLattice
OrderIsoClass.toCompleteLatticeHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [OrderIsoClass F α β], CompleteLatticeHomClass F α β
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_sum : ∀ (p : ENNReal) (V : Type u_4) [inst : AddCommGroup V] {ι : Type u_7} (s : Finset ι) (f : ι → WithLp p V),
  (∑ i ∈ s, f i).ofLp = ∑ i ∈ s, (f i).ofLp
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
coe_nonZeroDivisorsLeft_eq : ∀ (M₀ : Type u_1) [inst : MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀],
  ↑(nonZeroDivisorsLeft M₀) = {x | x ≠ 0}
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- A property of objects in the category `F.obj X` for all `X : B`.  -/
CategoryTheory.Pseudofunctor.ObjectProperty.prop : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} →
      F.ObjectProperty → (X : B) → CategoryTheory.ObjectProperty ↑(F.obj X)
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.ofDigits_modEq' : ∀ (b b' k : ℕ), b ≡ b' [MOD k] → ∀ (L : List ℕ), Nat.ofDigits b L ≡ Nat.ofDigits b' L [MOD k]
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.add_right : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r b c → RingQuot.Rel r (a + b) (a + c)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.not_mem_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α}, k ∉ ∅
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanIso.isAddFreimanHom : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {n : ℕ}, IsAddFreimanIso n A B f → IsAddFreimanHom n A B f
-- Std.Data.DTreeMap.Internal.Operations
/-- Inserts an element at the beginning of the tree.  -/
Std.DTreeMap.Internal.Impl.insertMin : {α : Type u} →
  {β : α → Type v} →
    (k : α) → β k → (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Std.DTreeMap.Internal.Impl.Tree α β (1 + t.size)
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.mul_lt_of_mul_inv_lt : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, b < 0 → a * b⁻¹ < c → c * b < a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) → aig.RefVec w → ℕ → (curr : ℕ) → curr ≤ w → aig.RefVec curr → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.ab_zero_apply : ∀ (S : CategoryTheory.ShortComplex Ab) (x : ↑S.X₁),
  (CategoryTheory.ConcreteCategory.hom S.g) ((CategoryTheory.ConcreteCategory.hom S.f) x) = 0
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.pow_succ : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n) (n_1 : ℕ), a ^ (n_1 + 1) = a ^ n_1 * a
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalStarSubalgebra.unitization_range : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : SetLike S A]
  [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] [inst_7 : StarMemClass S A] (s : S),
  (NonUnitalStarSubalgebra.unitization s).range = StarAlgebra.adjoin R ↑s
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Variant of `posLog_sum` for norms of elements in normed additive commutative
groups, using monotonicity of `log⁺` and the triangle inequality.
 -/
Real.posLog_norm_sum_le : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {α : Type u_2} (s : Finset α) (f : α → E),
  ‖∑ t ∈ s, f t‖.posLog ≤ Real.log ↑s.card + ∑ t ∈ s, ‖f t‖.posLog
-- Lean.Environment
Lean.Environment.mainModule : Lean.Environment → Lean.Name
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- The underlying type of the colimit of a diagram in `MonCat`.
 -/
MonCat.Colimits.ColimitType : {J : Type v} → [inst : CategoryTheory.Category.{u, v} J] → CategoryTheory.Functor J MonCat → Type v
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_of_contains_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = true → t.contains a = true
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (diag : CategoryTheory.Functor J C) (π : (CategoryTheory.Functor.const J).obj X ⟶ diag)
  (isLimit : CategoryTheory.Limits.IsLimit { pt := X, π := π }) (diag_1 : CategoryTheory.Functor J C)
  (π_1 : (CategoryTheory.Functor.const J).obj X ⟶ diag_1)
  (isLimit_1 : CategoryTheory.Limits.IsLimit { pt := X, π := π_1 }),
  ({ diag := diag, π := π, isLimit := isLimit } = { diag := diag_1, π := π_1, isLimit := isLimit_1 }) =
    (diag = diag_1 ∧ π ≍ π_1 ∧ isLimit ≍ isLimit_1)
-- LeanSearchClient.Syntax
LeanSearchClient.getStateSearchQueryJson : String → optParam ℕ 6 → String → Lean.CoreM (Array Lean.Json)
-- Mathlib.Order.Hom.Bounded
BotHom.coe_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : LE β] [inst_2 : OrderBot β], ⇑⊥ = ⊥
-- Init.Data.String.Lemmas.Search
String.back?_toSlice : ∀ {s : String}, s.toSlice.back? = s.back?
-- Mathlib.Order.Interval.Set.Disjoint
Set.Iio_disjoint_Ici : ∀ {α : Type v} [inst : Preorder α] {a b : α}, a ≤ b → Disjoint (Set.Iio a) (Set.Ici b)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaAddGrp =
    { obj := fun G => CategoryTheory.yonedaAddGrpObj G.X,
      map := fun {G H} ψ =>
        { app := fun Y => AddGrpCat.ofHom (AddMonCat.Hom.hom ((CategoryTheory.yonedaAddMon.map ψ.hom).app Y)),
          naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.coe_eq_of_mem_split_of_lt_mem : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {i : ι} {x : ℝ} {y : ι → ℝ},
  J ∈ BoxIntegral.Prepartition.split I i x → y ∈ J → x < y i → ↑J = ↑I ∩ {y | x < y i}
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Complex.summable_log_one_add_of_summable : ∀ {ι : Type u_1} {f : ι → ℂ}, Summable f → Summable fun i => Complex.log (1 + f i)
-- Init.Grind.Norm
Lean.Grind.bool_eq_to_prop : ∀ (a b : Bool), (a = b) = ((a = true) = (b = true))
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.zero_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S₁ S₂ : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.Hom.τ₂ 0 = 0
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.ComonadicLeftAdjoint.eqv : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {L : CategoryTheory.Functor C D} [self : CategoryTheory.ComonadicLeftAdjoint L],
  (CategoryTheory.Comonad.comparison CategoryTheory.ComonadicLeftAdjoint.adj).IsEquivalence
-- Lean.Data.AssocList
Lean.AssocList.instEmptyCollection : {α : Type u} → {β : Type v} → EmptyCollection (Lean.AssocList α β)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.all_eq_allTR.go : ∀ (m n : ℕ) (f : (i : ℕ) → i < m + n → Bool),
  (m + n).all f = ((n.all fun i h => f i ⋯) && Nat.allTR.loop✝ (m + n) f m ⋯)
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.coe_pow : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : Preorder α] [inst_2 : ZeroLEOneClass α] [inst_3 : PosMulMono α]
  (a : { x // 0 ≤ x }) (n : ℕ), ↑(a ^ n) = ↑a ^ n
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_three_mul : ∀ (x : ℂ), Complex.sinh (3 * x) = 4 * Complex.sinh x ^ 3 + 3 * Complex.sinh x
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber_mono : Monotone Nat.fermatNumber
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {T₁ T₂ : CategoryTheory.Monad C}
  {x y : CategoryTheory.MonadHom T₁ T₂}, x.app = y.app → x = y
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β}, MeasureTheory.AEStronglyMeasurable f μ → f =ᵐ[μ] g → MeasureTheory.AEStronglyMeasurable g μ
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Ioi_ae_eq_Ici : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a : α}, Set.Ioi a =ᵐ[μ] Set.Ici a
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquivClass.toSemilinearEquivClass : ∀ {F : Type u_5} {R : outParam (Type u_6)} {A : outParam (Type u_7)} {B : outParam (Type u_8)} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B]
  [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B] [inst_7 : EquivLike F A B]
  [self : CoalgEquivClass F R A B], SemilinearEquivClass F (RingHom.id R) A B
-- Mathlib.Algebra.Regular.Pi
Pi.isRightRegular_iff : ∀ {ι : Type u_1} {R : ι → Type u_3} [inst : (i : ι) → Mul (R i)] {a : (i : ι) → R i},
  IsRightRegular a ↔ ∀ (i : ι), IsRightRegular (a i)
-- Mathlib.Data.Int.ModEq
Int.modEq_modulus_add_iff : ∀ {n a b : ℤ}, a ≡ n + b [ZMOD n] ↔ a ≡ b [ZMOD n]
-- Mathlib.NumberTheory.Transcendental.Liouville.Basic
/-- Let `Z, N` be types, let `R` be a metric space, let `α : R` be a point and let
`j : Z → N → R` be a function.  We aim to estimate how close we can get to `α`, while staying
in the image of `j`.  The points `j z a` of `R` in the image of `j` come with a "cost" equal to
`d a`.  As we get closer to `α` while staying in the image of `j`, we are interested in bounding
the quantity `d a * dist α (j z a)` from below by a strictly positive amount `1 / A`: the intuition
is that approximating well `α` with the points in the image of `j` should come at a high cost.  The
hypotheses on the function `f : R → R` provide us with sufficient conditions to ensure our goal.
The first hypothesis is that `f` is Lipschitz at `α`: this yields a bound on the distance.
The second hypothesis is specific to the Liouville argument and provides the missing bound
involving the cost function `d`.

This lemma collects the properties used in the proof of `exists_pos_real_of_irrational_root`.
It is stated in more general form than needed: in the intended application, `Z = ℤ`, `N = ℕ`,
`R = ℝ`, `d a = (a + 1) ^ f.nat_degree`, `j z a = z / (a + 1)`, `f ∈ ℤ[x]`, `α` is an irrational
root of `f`, `ε` is small, `M` is a bound on the Lipschitz constant of `f` near `α`, `n` is
the degree of the polynomial `f`.
 -/
Liouville.exists_one_le_pow_mul_dist : ∀ {Z : Type u_1} {N : Type u_2} {R : Type u_3} [inst : PseudoMetricSpace R] {d : N → ℝ} {j : Z → N → R} {f : R → R}
  {α : R} {ε M : ℝ},
  (∀ (a : N), 1 ≤ d a) →
    0 < ε →
      (∀ ⦃y : R⦄, y ∈ Metric.closedBall α ε → dist (f α) (f y) ≤ dist α y * M) →
        (∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ Metric.closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))) →
          ∃ A, 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_insertEntry_of_key_ne : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [LawfulBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)}
  (p : (a : α) × β a), p.fst ≠ a → (p ∈ Std.Internal.List.insertEntry a b l ↔ p ∈ l)
-- Mathlib.Order.Cover
apply_wcovBy_apply_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} {E : Type u_3}
  [inst_2 : EquivLike E α β] [OrderIsoClass E α β] (e : E), e a ⩿ e b ↔ a ⩿ b
-- Init.Data.Float.Model.Float
Float.Model.instLT : LT Float.Model
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'.congr_simp : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₁.HasTensor X₂]
  [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] (i₁ i₂ i₃ j : I)
  (h : i₁ + i₂ + i₃ = j),
  CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h =
    CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h
-- Mathlib.Order.SuccPred.Basic
Order.succ_strictMono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α], StrictMono Order.succ
-- Init.Notation
/-- `a <|> b` executes `a` and returns the result, unless it fails in which
case it executes and returns `b`. Because `b` is not always executed, it
is passed as a thunk so it can be forced only when needed.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `<|>` in identifiers is `orElse`. -/
«term_<|>_» : Lean.TrailingParserDescr
-- Mathlib.Order.Hom.Bounded
TopHom.instLE : {α : Type u_2} → {β : Type u_3} → [inst : Top α] → [LE β] → [inst_2 : Top β] → LE (TopHom α β)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The identity between the iterated `SubAddAction`
of the `fixingAddSubgroup` and the `SubAddAction` of the `fixingAddSubgroup`
of the union, as an equivariant map.  -/
SubAddAction.map_ofFixingAddSubgroupUnion : (M : Type u_1) →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        (s t : Set α) →
          have ψ := fun m => ⟨⟨↑m, ⋯⟩, ⋯⟩;
          ↥(SubAddAction.ofFixingAddSubgroup M (s ∪ t)) →ₑ[ψ]
            ↥(SubAddAction.ofFixingAddSubgroup (↥(fixingAddSubgroup M s)) (Subtype.val ⁻¹' t))
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.maximalIdeal_eq_map_of_fg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (fg : (IsLocalRing.maximalIdeal R).FG),
  IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R) =
    Ideal.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (IsLocalRing.maximalIdeal R)
-- Lean.Elab.Do.PatternVar
Lean.Elab.Do.getLetDeclVars : Lean.TSyntax `Lean.Parser.Term.letDecl → Lean.Elab.TermElabM (Array Lean.Ident)
-- Init.PropLemmas
ite_eq_left_iff : ∀ {α : Sort u_1} {p : Prop} [inst : Decidable p] {x y : α}, (if p then x else y) = x ↔ ¬p → y = x
-- Mathlib.Algebra.Order.Monoid.NatCast
one_le_two' : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : LE α] [ZeroLEOneClass α] [AddRightMono α], 1 ≤ 2
-- Mathlib.Tactic.FBinop
FBinopElab.instInhabitedSRec.default : FBinopElab.SRec
-- Lean.Parser.Term
Lean.Parser.Term.subst.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.Spanning.eRk_eq : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Spanning X → M.eRk X = M.eRank
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- The linear equivalence corresponding to an injective endomorphism.  -/
LinearEquiv.ofInjectiveEndo : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → [FiniteDimensional K V] → (f : V →ₗ[K] V) → Function.Injective ⇑f → V ≃ₗ[K] V
-- Mathlib.Dynamics.FixedPoints.Basic
Function.IsFixedPt.preimage_iterate : ∀ {α : Type u_1} {f : α → α} {s : Set α},
  Function.IsFixedPt (Set.preimage f) s → ∀ (n : ℕ), Function.IsFixedPt (Set.preimage f^[n]) s
-- Mathlib.RepresentationTheory.Induced
/-- Given a group homomorphism `φ : G →* H` and a `G`-representation `(A, ρ)`, this is the
`H → A →ₗ[k] (k[H] ⊗[k] A)_G` sending `h, a` to `⟦h ⊗ₜ a⟧`.  -/
Representation.IndV.mk : {k : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : Group H] →
            (φ : G →* H) →
              {A : Type u_4} →
                [inst_3 : AddCommGroup A] →
                  [inst_4 : Module k A] → (ρ : Representation k G A) → H → A →ₗ[k] Representation.IndV φ ρ
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.semiring : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [inst_3 : Module Rᵐᵒᵖ M] → [SMulCommClass R Rᵐᵒᵖ M] → Semiring (TrivSqZeroExt R M)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mul_top : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), I * ⊤ = I
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_map_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n γ} {g : γ → δ} {it : Std.IterM m β},
  (Std.IterM.map g (Std.IterM.mapM f it)).toArray =
    (Std.IterM.mapM
        (fun b => do
          let __do_lift ← f b
          pure (g __do_lift))
        it).toArray
-- Init.Coe
CoeTC.mk : {α : Sort u} → {β : Sort v} → (α → β) → CoeTC α β
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.isLittleO_smoothingFn_one : AkraBazziRecurrence.smoothingFn =o[Filter.atTop] fun x => 1
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- The quotient map `(R ⧸ a • I) →ₗ[R] (R ⧸ Ideal.span {a})`.
 -/
Ideal.quotOfMul : {R : Type u_1} → [inst : CommRing R] → (a : R) → (I : Ideal R) → R ⧸ a • I →ₗ[R] R ⧸ Ideal.span {a}
-- Mathlib.Tactic.Order.Graph.Basic
/-- If `g` is a `Graph`, then for a vertex with index `v`, `g[v]` is an array containing
the edges starting from this vertex.  -/
Mathlib.Tactic.Order.Graph : Type
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {w : ℕ} {vec : aig.BinaryRefVec w}
  {cin : aig.Ref} {w_1 : ℕ} {vec_1 : aig.BinaryRefVec w_1} {cin_1 : aig.Ref},
  { w := w, vec := vec, cin := cin } = { w := w_1, vec := vec_1, cin := cin_1 } → w = w_1 ∧ vec ≍ vec_1 ∧ cin = cin_1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.all_eq_true_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.all pat = true ↔ String.Slice.Pattern.Model.IsLongestMatchAtChain pat s.startPos s.endPos
-- Mathlib.CategoryTheory.Limits.Fubini
/-- For each object, a cone.  -/
CategoryTheory.Limits.DiagramOfCones.obj : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              CategoryTheory.Limits.DiagramOfCones F → (j : J) → CategoryTheory.Limits.Cone (F.obj j)
-- Mathlib.Algebra.Field.Basic
inv_sub_inv : ∀ {K : Type u_1} [inst : Field K] {a b : K}, a ≠ 0 → b ≠ 0 → a⁻¹ - b⁻¹ = (b - a) / (a * b)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.mk.injEq : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (carrier : Set (Projectivization K V))
  (mem_add' :
    ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
      Projectivization.mk K v hv ∈ carrier →
        Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier)
  (carrier_1 : Set (Projectivization K V))
  (mem_add'_1 :
    ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
      Projectivization.mk K v hv ∈ carrier_1 →
        Projectivization.mk K w hw ∈ carrier_1 → Projectivization.mk K (v + w) hvw ∈ carrier_1),
  ({ carrier := carrier, mem_add' := mem_add' } = { carrier := carrier_1, mem_add' := mem_add'_1 }) =
    (carrier = carrier_1)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.free_obj_a : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C),
  (T.free.obj X).a = T.μ.app X
-- Mathlib.Tactic.NormNum.BigOperators
/-- Either show the expression `s : Q(Multiset α)` is Zero, or remove one element from it.

Fails if we cannot determine which of the alternatives apply to the expression.
 -/
Mathlib.Meta.Multiset.proveZeroOrCons : {u : Lean.Level} → {α : Q(Type u)} → (s : Q(Multiset «$α»)) → Lean.MetaM (Mathlib.Meta.Multiset.ProveZeroOrConsResult s)
-- Lean.Data.SSet
Lean.SSet.empty : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SSet α
-- Mathlib.Data.UInt
UInt16.toBitVec_injective : Function.Injective UInt16.toBitVec
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.instHasInitialObjOfFaithfulOfFull : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  {G : CategoryTheory.Functor A T} [G.Faithful] [G.Full] {Y : A},
  CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow (G.obj Y) G)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_apply_le : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s t : Set α), (μ.restrict s) t ≤ μ t
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.liftTruncLT.congr_simp : ∀ {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) {X Y : C} (f f_1 : X ⟶ Y),
  f = f_1 →
    ∀ (n₀ n₀_1 : ℤ) (e_n₀ : n₀ = n₀_1) (n₁ : ℤ) (h : n₀ + 1 = n₁) [inst_6 : t.IsLE X n₀],
      t.liftTruncLT f n₀ n₁ h = t.liftTruncLT f_1 n₀_1 n₁ ⋯
-- Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
/-- A global integral curve is injective xor periodic with positive period.  -/
IsMIntegralCurve.periodic_xor_injective : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} [T2Space M] [BoundarylessManifold I M],
  IsMIntegralCurve γ v →
    (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) → Xor (∃ T > 0, Function.Periodic γ T) (Function.Injective γ)
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.shift_unit_app : ∀ {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 : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (X : C),
  (CategoryTheory.shiftFunctor C a).map (adj.unit.app X) =
    CategoryTheory.CategoryStruct.comp (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Functor.commShiftIso F a).hom.app X))
        ((CategoryTheory.Functor.commShiftIso G a).hom.app (F.obj X)))