mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.fundamentalInterior.eq_1 : ∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α),
  MeasureTheory.fundamentalInterior G s = s \ ⋃ g, ⋃ (_ : g ≠ 1), g • s
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.quasispectrum_eq_spectrum_inr : ∀ (R : Type u_3) {A : Type u_4} [inst : CommRing R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (a : A), quasispectrum R a = spectrum R ↑a
-- Std.Time.Format.Modifier
Std.Time.Modifier.s.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.s presentation = Std.Time.Modifier.s presentation_1 → presentation = presentation_1
-- Lean.Meta.SynthInstance
/-- See `getSubgoals` and `getSubgoalsAux`

We use the parameter `j` to reduce the number of `instantiate*` invocations.
It is the same approach we use at `forallTelescope` and `lambdaTelescope`.
Given `getSubgoalsAux args j subgoals instVal type`,
we have that `type.instantiateRevRange j args.size args` does not have loose bound variables.  -/
Lean.Meta.SynthInstance.SubgoalsResult : Type
-- Lean.Setup
Lean.instHashableImport.hash : Lean.Import → UInt64
-- Mathlib.MeasureTheory.Group.Measure
/-- In a noncompact locally compact group, a left-invariant measure which is positive
on open sets has infinite mass.  -/
MeasureTheory.measure_univ_of_isMulLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] [inst_3 : Group G]
  [IsTopologicalGroup G] [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : MeasureTheory.Measure G)
  [μ.IsOpenPosMeasure] [μ.IsMulLeftInvariant], μ Set.univ = ⊤
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- If two lifts of circle homeomorphisms have the same translation number, then they are
semiconjugate by a `CircleDeg1Lift`. This version uses assumptions `IsUnit f₁` and `IsUnit f₂`
to assume that `f₁` and `f₂` are homeomorphisms.  -/
CircleDeg1Lift.semiconj_of_isUnit_of_translationNumber_eq : ∀ {f₁ f₂ : CircleDeg1Lift},
  IsUnit f₁ → IsUnit f₂ → f₁.translationNumber = f₂.translationNumber → ∃ F, Function.Semiconj ⇑F ⇑f₁ ⇑f₂
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.Const.toList_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {a : α} {f : Option β → Option β}
  {l : Std.DHashMap.Internal.AssocList α fun x => β},
  (Std.DHashMap.Internal.AssocList.Const.alter a f l).toList.Perm (Std.Internal.List.Const.alterKey a f l.toList)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instRepr : {α : Type u} → {β : α → Type v} → [Repr α] → [(a : α) → Repr (β a)] → Repr (Std.DHashMap.Raw α β)
-- Mathlib.Topology.Category.Compactum
Compactum.join_distrib : ∀ (X : Compactum) (uux : Ultrafilter (Ultrafilter X.A)), X.str (X.join uux) = X.str (Ultrafilter.map X.str uux)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.maxKey! ∈ t
-- Lean.CoreM
Lean.Core.modifyCache : (Lean.Core.Cache → Lean.Core.Cache) → Lean.CoreM Unit
-- Mathlib.Data.Seq.Defs
Stream'.Seq.BisimO.eq_1 : ∀ {α : Type u} (R : Stream'.Seq α → Stream'.Seq α → Prop), Stream'.Seq.BisimO R none none = True
-- Mathlib.ModelTheory.Ultraproducts
FirstOrder.Language.Ultraproduct.term_realize_cast : ∀ {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [inst : (a : α) → L.Structure (M a)]
  {β : Type u_3} (x : β → (a : α) → M a) (t : L.Term β),
  FirstOrder.Language.Term.realize (fun i => Quotient.mk' (x i)) t =
    Quotient.mk' fun a => FirstOrder.Language.Term.realize (fun i => x i a) t
-- Mathlib.Data.Num.Lemmas
Num.lt_to_nat : ∀ {m n : Num}, ↑m < ↑n ↔ m < n
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNat_default : Turing.PartrecToTM2.trNat default = []
-- Mathlib.Analysis.Normed.Group.ControlledClosure
/-- Given `f : NormedAddGroupHom G H` for some complete `G` and a subgroup `K` of `H`, if every
element `x` of `K` has a preimage under `f` whose norm is at most `C*‖x‖` then the same holds for
elements of the (topological) closure of `K` with constant `C+ε` instead of `C`, for any
positive `ε`.
 -/
controlled_closure_of_complete : ∀ {G : Type u_1} [inst : NormedAddCommGroup G] [CompleteSpace G] {H : Type u_2} [inst_2 : NormedAddCommGroup H]
  {f : NormedAddGroupHom G H} {K : AddSubgroup H} {C ε : ℝ},
  0 < C → 0 < ε → f.SurjectiveOnWith K C → f.SurjectiveOnWith K.topologicalClosure (C + ε)
-- Mathlib.RingTheory.Invariant.Galois
instSMulDistribClassAlgEquiv : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Field K] [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra A B] [inst_8 : Algebra K L] [inst_9 : Algebra A L] [inst_10 : IsScalarTower A K L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L],
  have this := IsIntegralClosure.MulSemiringAction A K L B;
  SMulDistribClass Gal(L/K) B L
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  UpperSet.instCommMonoid =
    { toSemigroup := UpperSet.commSemigroup.toSemigroup, toOne := UpperSet.instOne, one_mul := ⋯, mul_one := ⋯,
      npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.isBounded_range : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (f : BoundedContinuousFunction α β), Bornology.IsBounded (Set.range ⇑f)
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.superFactorial_dvd_vandermonde_det : ∀ {n : ℕ} (v : Fin (n + 1) → ℤ), ↑n.superFactorial ∣ (Matrix.vandermonde v).det
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instRightCancelSemigroup : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [RightCancelSemigroup M] → RightCancelSemigroup (l.Germ M)
-- Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
LinearMap.toContinuousBilinearMap_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2} [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [inst_5 : IsTopologicalAddGroup E] [inst_6 : ContinuousSMul 𝕜 E]
  [inst_7 : FiniteDimensional 𝕜 E] [inst_8 : T2Space E] {F : Type u_3} [inst_9 : AddCommGroup F] [inst_10 : Module 𝕜 F]
  [inst_11 : TopologicalSpace F] [inst_12 : IsTopologicalAddGroup F] [inst_13 : ContinuousSMul 𝕜 F]
  [inst_14 : FiniteDimensional 𝕜 F] [inst_15 : T2Space F] {G : Type u_4} [inst_16 : AddCommGroup G]
  [inst_17 : Module 𝕜 G] [inst_18 : TopologicalSpace G] [inst_19 : IsTopologicalAddGroup G]
  [inst_20 : ContinuousSMul 𝕜 G] (f : E →ₗ[𝕜] F →ₗ[𝕜] G) (x : E) (y : F), (f.toContinuousBilinearMap x) y = (f x) y
-- Mathlib.Order.Filter.Extr
IsMinOn.bddBelow : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}, IsMinOn f s a → BddBelow (f '' s)
-- Lean.Parser.Basic
Lean.Parser.ParserCategory.mk : Lean.Name →
  Lean.Parser.SyntaxNodeKindSet →
    Lean.Parser.PrattParsingTables → Lean.Parser.LeadingIdentBehavior → Lean.Parser.ParserCategory
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.restrict_points_coe : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) (S : AffineSubspace k P)
  (hS : affineSpan k (Set.range s.points) ≤ S) (i : Fin (n + 1)), ↑((s.restrict S hS).points i) = s.points i
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_add_left_left_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime (y * z + x) y ↔ IsRelPrime x y
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.toOption.match_1.splitter : {ρ : Type} →
  {σ : String.Slice → Type} →
    {pat : ρ} →
      [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
        {s : String.Slice} →
          (motive : String.Slice.SplitIterator pat s → Sort u_1) →
            (x : String.Slice.SplitIterator pat s) →
              ((currPos : s.Pos) →
                  (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                    motive (String.Slice.SplitIterator.operating currPos s_1)) →
                (Unit → motive String.Slice.SplitIterator.atEnd) → motive x
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.postcomp_var : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M) {N : Type v'} [inst_3 : AddCommGroup N] [inst_4 : Module A N]
  (f : M →ₗ[A] N) (g : relations.G), (solution.postcomp f).var g = f (solution.var g)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.φ₁ f.f₂.τ₁ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f) S₂.φ₁
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) =
    CategoryTheory.SemiCartesianMonoidalCategory.fst X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)
-- Mathlib.Topology.Algebra.ConstMulAction
Prod.continuousConstSMul : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  [inst_3 : TopologicalSpace β] [inst_4 : SMul M β] [ContinuousConstSMul M β], ContinuousConstSMul M (α × β)
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofString : String → Lean.LeanOptionValue
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.step_take.match_1.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (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 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, 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, h⟩ => h_3 h) =
    h_1 it' out h
-- Init.Data.SInt.Basic
instMinISize : Min ISize
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_const_smul : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι} {𝕜 : Type u_4}
  [inst_1 : SMul 𝕜 β] (c : 𝕜), MeasureTheory.stoppedValue (c • u) τ = c • MeasureTheory.stoppedValue u τ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α}
  {k fallback : α}, k ∈ t → (t.insertManyIfNewUnit l).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Order.Types.Defs
OrderType.type_ulift : ∀ {α : Type u} [inst : LinearOrder α], OrderType.type (ULift.{v, u} α) = OrderType.lift.{v, u} (OrderType.type α)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_mono : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  s₁ ⊆ s₂ → autoParam (μ s₂ ≠ ⊤) MeasureTheory.measureReal_mono._auto_1 → μ.real s₁ ≤ μ.real s₂
-- Mathlib.Order.Bounds.Basic
upperBounds_Ioo : ∀ {γ : Type u_3} [inst : SemilatticeInf γ] [DenselyOrdered γ] {a b : γ}, b < a → upperBounds (Set.Ioo b a) = Set.Ici a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_insert_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insert k v).contains k = true
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffAt_infty : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, ContDiffAt 𝕜 (↑⊤) f x ↔ ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) f x
-- Mathlib.Algebra.GCDMonoid.Nat
Int.abs_eq_normalize : ∀ (z : ℤ), |z| = normalize z
-- Mathlib.Data.Sym.Sym2
Set.mk_preimage_sym2 : ∀ {α : Type u_1} {s : Set α}, Function.uncurry Sym2.mk ⁻¹' s.sym2 = s ×ˢ s
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
List.iSup_mem_map_of_exists_sSup_empty_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {l : List ι} (f : ι → α),
  (∃ x ∈ l, sSup ∅ ≤ f x) → ⨆ x ∈ l, f x ∈ List.map f l
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.clift_apply_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : FreeAddMonoid (M ⊕ N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0)
  (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0)
  (hM :
    ∀ (x y : M),
      f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y)))
  (hN :
    ∀ (x y : N),
      f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y)))
  (x : M), (AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.inl x) = f (FreeAddMonoid.of (Sum.inl x))
-- Mathlib.Data.Subtype
Subtype.restrict_injective : ∀ {α : Sort u_4} {β : Type u_5} {f : α → β} (p : α → Prop),
  Function.Injective f → Function.Injective (Subtype.restrict p f)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_le_unop_iff : ∀ {M : Type u_2} [inst : Mul M] {S₁ S₂ : Subsemigroup Mᵐᵒᵖ}, S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
-- Mathlib.Probability.ProbabilityMassFunction.Monad
/-- The measure of a set under `p.bindOnSupport f` is the sum over `a : α`
of the probability of `a` under `p` times the measure of the set under `f a _`.
The additional if statement is needed since `f` is only a partial function.  -/
PMF.toMeasure_bindOnSupport_apply : ∀ {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β) (s : Set β)
  [inst : MeasurableSpace β],
  MeasurableSet s → (p.bindOnSupport f).toMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toMeasure s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {k : α} {v : β k}, (m.getThenInsertIfNew? k v).1 = m.get? k
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.isEmpty_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₂ → m₁.isEmpty = m₂.isEmpty
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.IsUnitTrinomial.irreducible_aux2 : ∀ {p q : Polynomial ℤ} {k m m' n : ℕ},
  k < m →
    m < n →
      k < m' →
        m' < n →
          ∀ (u v w : ℤˣ),
            p = Polynomial.trinomial k m n ↑u ↑v ↑w →
              q = Polynomial.trinomial k m' n ↑u ↑v ↑w → p * p.mirror = q * q.mirror → q = p ∨ q = p.mirror
-- Mathlib.Order.Filter.Prod
Filter.sup_prod : ∀ {α : Type u_1} {β : Type u_2} (f₁ f₂ : Filter α) (g : Filter β), (f₁ ⊔ f₂) ×ˢ g = f₁ ×ˢ g ⊔ f₂ ×ˢ g
-- Mathlib.Algebra.BigOperators.Finprod
Nat.cast_finprod_mem : ∀ {ι : Type u_3} {s : Set ι},
  s.Finite →
    ∀ {R : Type u_7} [inst : CommSemiring R] (f : ι → ℕ),
      ↑(∏ᶠ (x : ι) (_ : x ∈ s), f x) = ∏ᶠ (x : ι) (_ : x ∈ s), ↑(f x)
-- Mathlib.Order.UpperLower.Closure
upperClosure_eq_bot : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, ¬BddBelow s → upperClosure s = ⊥
-- Lean.Elab.DocString
Lean.Doc.instFromDocArgNat : Lean.Doc.FromDocArg ℕ
-- Init.Data.String.Defs
String.Pos.mk.sizeOf_spec : ∀ {s : String} (offset : String.Pos.Raw) (isValid : String.Pos.Raw.IsValid s offset),
  sizeOf { offset := offset, isValid := isValid } = 1 + sizeOf offset + sizeOf isValid
-- Init.Data.SInt.Lemmas
Int64.ne_iff_toBitVec_ne : ∀ {a b : Int64}, a ≠ b ↔ a.toBitVec ≠ b.toBitVec
-- Mathlib.NumberTheory.NumberField.Discriminant.Different
NumberField.discr_mem_differentIdeal : ∀ (K : Type u_1) (𝒪 : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsFractionRing 𝒪 K] [inst_5 : IsDedekindDomain 𝒪] [inst_6 : CharZero 𝒪] [Module.Finite ℤ 𝒪],
  ↑(NumberField.discr K) ∈ differentIdeal ℤ 𝒪
-- Mathlib.Probability.Kernel.Invariance
ProbabilityTheory.Kernel.Invariant.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel α α) (μ : MeasureTheory.Measure α),
  κ.Invariant μ = (μ.bind ⇑κ = μ)
-- Init.Data.Nat.Power2.Basic
_private.Init.Data.Nat.Power2.Basic.0.Nat.nextPowerOfTwo.go : ℕ → (power : ℕ) → power > 0 → ℕ
-- Mathlib.CategoryTheory.Bicategory.SingleObj
/-- The equivalence between the endomorphisms of the single object
when we promote a monoidal category to a single object bicategory,
and the original monoidal category.
 -/
CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C) ≌ C
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpace_neg_zsmul_add_ne_bot : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) {n : ℕ},
  n ≤ LieModule.chainBotCoeff α β → LieModule.genWeightSpace M (-↑n • α + ⇑β) ≠ ⊥
-- Mathlib.Data.Seq.Basic
/-- The statement of `length_le_iff` assumes that the sequence terminates. For a
statement of the where the sequence is not known to terminate see `length_le_iff'`.  -/
Stream'.Seq.lt_length_iff : ∀ {α : Type u} {s : Stream'.Seq α} {n : ℕ} {h : s.Terminates}, n < s.length h ↔ ∃ a, a ∈ s.get? n
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.isParam : Lean.IR.LocalContext → Lean.IR.Index → Bool
-- Mathlib.Data.FinEnum
FinEnum.card_punit : FinEnum.card PUnit.{u_1 + 1} = 1
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv_mul_add_emod : ∀ (a b : ℤ), a / b * b + a % b = a
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.mem_cylinder_iff_dist_le : ∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ}, y ∈ PiNat.cylinder x n ↔ dist y x ≤ (1 / 2) ^ n
-- Init.Data.String.Basic
String.Pos.offset_add_slice : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}, p₀.offset + s.slice p₀ p₁ h = p₁.offset
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.chartAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (p : TangentBundle I M),
  chartAt (ModelProd H E) p =
    ((tangentBundleCore I M).toFiberBundleCore.localTriv (achart H p.proj)).trans
      ((chartAt H p.proj).prod (OpenPartialHomeomorph.refl E))
-- Mathlib.Combinatorics.Matroid.Basic
/-- There is a finite base  -/
Matroid.RankFinite.exists_finite_isBase : ∀ {α : Type u_1} {M : Matroid α} [self : M.RankFinite], ∃ B, M.IsBase B ∧ B.Finite
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.sndSigmaMapOfIsColimit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c),
  I.sndSigmaMapOfIsColimit d hc =
    CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i =>
      CategoryTheory.CategoryStruct.comp (I.snd i) (d.inj (J.snd i))
-- Init.Data.Nat.Lemmas
Nat.max_left_comm : ∀ (a b c : ℕ), max a (max b c) = max b (max a c)
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.height.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.height i = dist (s.points i) (s.altitudeFoot i)
-- Aesop.Forward.State
/-- Add a hypothesis `hyp`. Precondition: `hyp` matches the premise of slot
`slot` with substitution `hyp.subst` (and hence `hyp.subst` contains a mapping
for each variable in `slot.common`). Returns `true` if the variable map
changed.  -/
Aesop.VariableMap.addHyp : Aesop.VariableMap → Aesop.Slot → Aesop.Hyp → Aesop.BaseM (Aesop.VariableMap × Bool)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α}
  {lhs rhs cin lhs_1 rhs_1 cin_1 : aig.Ref},
  { lhs := lhs, rhs := rhs, cin := cin } = { lhs := lhs_1, rhs := rhs_1, cin := cin_1 } →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ cin = cin_1
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.isUnsatEq.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Sort u_1) (x : Int.Internal.Linear.Poly)
  (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Poly.num k)) (h_2 : (x : Int.Internal.Linear.Poly) → motive x),
  (∀ (k : ℤ), x = Int.Internal.Linear.Poly.num k → False) →
    (match x with
      | Int.Internal.Linear.Poly.num k => h_1 k
      | x => h_2 x) =
      h_2 x
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.edist_lt_top : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ {x y : α}, edist x y ≠ ⊤ → edist (f x) (f y) < ⊤
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.zeroThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Mathlib.Data.PFun
_private.Mathlib.Data.PFun.0.PFun.fix.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : β ⊕ α → Sort u_3) (a' : α)
  (h_1 : (b : β) → Sum.inr a' = Sum.inl b → motive (Sum.inl b))
  (h_2 : (a'_1 : α) → Sum.inr a' = Sum.inr a'_1 → motive (Sum.inr a'_1)),
  (match e : Sum.inr a' with
    | Sum.inl b => h_1 b e
    | Sum.inr a'_1 => h_2 a'_1 e) =
    h_2 a' ⋯
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_pre_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C} (X : C)
  {Y : C} [inst_2 : CategoryTheory.Closed A] [inst_3 : CategoryTheory.Closed B] (f : Y ⟶ A ⟹ X) (g : B ⟶ A) {Z : C}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalClosed.uncurry
        (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.MonoidalClosed.pre g).app X)))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry f) h)