mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Change of variable formula for differentiable functions: if a function `f` is
injective and differentiable on a measurable set `s`, then the Bochner integral of a function
`g : E → F` on `f '' s` coincides with the integral of `|(f' x).det| • g ∘ f` on `s`.  -/
MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E}
  [inst_5 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s → ∀ (g : E → F), ∫ (x : E) in f '' s, g x ∂μ = ∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ
-- Init.Data.String.Lemmas.Search
String.front?_eq : ∀ {s : String}, s.front? = s.toList.head?
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.min_eq_left : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {p q : (a : α) × β a}, (compare p.fst q.fst).isLE = true → p ⊓ q = p
-- Mathlib.Data.Num.Lemmas
Num.ofNat'.eq_1 : ∀ (n : ℕ), Num.ofNat' n = Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) n
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_mul : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (f₁ f₂ : (i : ι) → s i →ₗ[R] s i),
  (PiTensorProduct.map fun i => f₁ i * f₂ i) = PiTensorProduct.map f₁ * PiTensorProduct.map f₂
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.union : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  e₁.AreComplementary e₂ → ∀ (i : ι), (∃ i₁, e₁.f i₁ = i) ∨ ∃ i₂, e₂.f i₂ = i
-- Mathlib.GroupTheory.Commutator.Basic
conjugate_commutatorElement : ∀ {G : Type u_1} [inst : Group G] (g₁ g₂ g₃ : G), g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆
-- Mathlib.Algebra.GroupWithZero.Associated
associated_mul_isUnit_left_iff : ∀ {N : Type u_2} [inst : Monoid N] {a u b : N}, IsUnit u → (Associated (a * u) b ↔ Associated a b)
-- Mathlib.Data.Int.ModEq
/-- **Alias** of `AddCommGroup.modEq_iff_intModEq`. -/
AddCommGroup.modEq_iff_int_modEq : ∀ {a b z : ℤ}, a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.parameter : Lean.Lsp.SemanticTokenType
-- Mathlib.Computability.TuringMachine.Computable
/-- the input alphabet is equivalent to `Γ₀`  -/
Turing.TM2ComputableAux.inputAlphabet : {Γ₀ Γ₁ : Type} → (self : Turing.TM2ComputableAux Γ₀ Γ₁) → self.tm.Γ self.tm.k₀ ≃ Γ₀
-- Mathlib.Order.Heyting.Basic
le_compl_iff_disjoint_left : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ bᶜ ↔ Disjoint b a
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedCancelVAdd.mk : ∀ {G : Type u_3} {P : Type u_4} [inst : LE G] [inst_1 : LE P] [inst_2 : VAdd G P] [toIsOrderedVAdd : IsOrderedVAdd G P],
  (∀ (a : G) (b c : P), a +ᵥ b ≤ a +ᵥ c → b ≤ c) →
    (∀ (a b : G) (c : P), a +ᵥ c ≤ b +ᵥ c → a ≤ b) → IsOrderedCancelVAdd G P
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular, then any measurable set can be approximated by a compact subset.
See also `MeasurableSet.exists_isCompact_lt_add_of_ne_top`.  -/
MeasurableSet.exists_lt_isCompact : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.InnerRegular]
  ⦃A : Set α⦄, MeasurableSet A → ∀ {r : ENNReal}, r < μ A → ∃ K ⊆ A, IsCompact K ∧ r < μ K
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.div_tendsto_atTop_zero_of_degree_lt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  P.degree < Q.degree → Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (nhds 0)
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
uniformContinuous_dist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α], UniformContinuous fun p => dist p.1 p.2
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_ofNat : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (n : ℕ) [inst_3 : OfNat F n], HasDerivAt (OfNat.ofNat n) 0 x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameParams.mk.inj : ∀ {toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams} {newName : String}
  {toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams} {newName_1 : String},
  { toTextDocumentPositionParams := toTextDocumentPositionParams, newName := newName } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1, newName := newName_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1 ∧ newName = newName_1
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_append_append_eq_shiftLeft_setWidth_or : ∀ {w w' w'' w''' : ℕ} {b : BitVec w} {b' : BitVec w'} {b'' : BitVec w''},
  BitVec.setWidth w''' (b ++ b' ++ b'') =
    BitVec.setWidth w''' b <<< (w' + w'') ||| BitVec.setWidth w''' b' <<< w'' ||| BitVec.setWidth w''' b''
-- Mathlib.Topology.Constructions.SumProd
instTopologicalSpaceProd : {X : Type u} → {Y : Type v} → [t₁ : TopologicalSpace X] → [t₂ : TopologicalSpace Y] → TopologicalSpace (X × Y)
-- Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.Linter.mk.sizeOf_spec : ∀ (test : Lean.Name → Lean.MetaM (Option Lean.MessageData)) (noErrorsFound errorsFound : Lean.MessageData)
  (isFast : Bool),
  sizeOf { test := test, noErrorsFound := noErrorsFound, errorsFound := errorsFound, isFast := isFast } =
    1 + sizeOf noErrorsFound + sizeOf errorsFound + sizeOf isFast
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.radius_regularizedGaussHGFunSeries_eq_top_of_left : ∀ (b c : ℂ) (k : ℕ), ((-↑k).regularizedGaussHGFunSeries b c).radius = ⊤
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.State.mk.inj : ∀ {found : Lean.NameSet} {vars : Array Lean.Elab.Term.PatternVar} {found_1 : Lean.NameSet}
  {vars_1 : Array Lean.Elab.Term.PatternVar},
  { found := found, vars := vars } = { found := found_1, vars := vars_1 } → found = found_1 ∧ vars = vars_1
-- Mathlib.Topology.CompactOpen
ContinuousMap.instT3Space : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T3Space Y], T3Space C(X, Y)
-- Mathlib.Algebra.Quandle
Quandle.mk : {α : Type u_1} → [toRack : Rack α] → (∀ {x : α}, Shelf.act x x = x) → Quandle α
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM.sizeOf_spec : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : Semiring 𝕜₁] [inst_1 : Semiring 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : SizeOf 𝕜₁]
  [inst_9 : SizeOf 𝕜₂] [inst_10 : SizeOf E] [inst_11 : SizeOf F] (toCLM : E →SL[σ] F),
  sizeOf (ContinuousLinearMapWOT.ofCLM toCLM) = 1 + sizeOf toCLM
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.ematch.injEq : ∀ (k k_1 : Lean.Meta.Grind.EMatchTheoremKind),
  (Lean.Meta.Grind.AttrKind.ematch k = Lean.Meta.Grind.AttrKind.ematch k_1) = (k = k_1)
-- Mathlib.Data.Fintype.Perm
AddEquiv.instFintype.eq_1 : ∀ {α : Type u_4} {β : Type u_5} [inst : Add α] [inst_1 : Add β] [inst_2 : DecidableEq α] [inst_3 : DecidableEq β]
  [inst_4 : Fintype α] [inst_5 : Fintype β],
  AddEquiv.instFintype =
    {
      elems :=
        Finset.filterMap
          (fun e => if h : ∀ (a b : α), e (a + b) = e a + e b then some { toEquiv := e, map_add' := h } else none)
          Fintype.elems ⋯,
      complete := ⋯ }
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.Equiv.fold_eq : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} [Std.Iterator α₁ m β] [Std.Iterator α₂ m β] [inst : Std.Iterator α₁ m β]
  [inst_1 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m] [inst_4 : Monad m]
  [inst_5 : LawfulMonad m] [inst_6 : Std.IteratorLoop α₁ m m] [Std.LawfulIteratorLoop α₁ m m]
  [inst_8 : Std.IteratorLoop α₂ m m] [Std.LawfulIteratorLoop α₂ m m] {init : γ} {f : γ → β → γ} {ita : Std.IterM m β}
  {itb : Std.IterM m β}, ita.Equiv itb → Std.IterM.fold f init ita = Std.IterM.fold f init itb
-- Mathlib.Algebra.Group.Equiv.Basic
/-- A family of multiplicative equivalences `Π j, (Ms j ≃* Ns j)` generates a
multiplicative equivalence between `Π j, Ms j` and `Π j, Ns j`.

This is the `MulEquiv` version of `Equiv.piCongrRight`, and the dependent version of
`MulEquiv.arrowCongr`.
 -/
MulEquiv.piCongrRight : {η : Type u_16} →
  {Ms : η → Type u_17} →
    {Ns : η → Type u_18} →
      [inst : (j : η) → Mul (Ms j)] →
        [inst_1 : (j : η) → Mul (Ns j)] → ((j : η) → Ms j ≃* Ns j) → ((j : η) → Ms j) ≃* ((j : η) → Ns j)
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateReturnImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.FVarId → Lean.Compiler.LCNF.Code pu
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.InvariantForm.apply_eq_or_of_apply_ne : ∀ {ι : 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} [Finite ι]
  [CharZero R] [P.IsCrystallographic] {i j : ι} [IsDomain R] [P.IsReduced] (B : P.InvariantForm) [P.IsIrreducible],
  (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j) →
    ∀ (k : ι),
      (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
        (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.mk.inj : ∀
  {userTime systemTime maxRSS ixRSS idRSS isRSS minFlt majFlt nSwap inBlock outBlock msgSent msgRecv signals voluntaryCS
    involuntaryCS userTime_1 systemTime_1 maxRSS_1 ixRSS_1 idRSS_1 isRSS_1 minFlt_1 majFlt_1 nSwap_1 inBlock_1
    outBlock_1 msgSent_1 msgRecv_1 signals_1 voluntaryCS_1 involuntaryCS_1 : UInt64},
  { userTime := userTime, systemTime := systemTime, maxRSS := maxRSS, ixRSS := ixRSS, idRSS := idRSS, isRSS := isRSS,
        minFlt := minFlt, majFlt := majFlt, nSwap := nSwap, inBlock := inBlock, outBlock := outBlock,
        msgSent := msgSent, msgRecv := msgRecv, signals := signals, voluntaryCS := voluntaryCS,
        involuntaryCS := involuntaryCS } =
      { userTime := userTime_1, systemTime := systemTime_1, maxRSS := maxRSS_1, ixRSS := ixRSS_1, idRSS := idRSS_1,
        isRSS := isRSS_1, minFlt := minFlt_1, majFlt := majFlt_1, nSwap := nSwap_1, inBlock := inBlock_1,
        outBlock := outBlock_1, msgSent := msgSent_1, msgRecv := msgRecv_1, signals := signals_1,
        voluntaryCS := voluntaryCS_1, involuntaryCS := involuntaryCS_1 } →
    userTime = userTime_1 ∧
      systemTime = systemTime_1 ∧
        maxRSS = maxRSS_1 ∧
          ixRSS = ixRSS_1 ∧
            idRSS = idRSS_1 ∧
              isRSS = isRSS_1 ∧
                minFlt = minFlt_1 ∧
                  majFlt = majFlt_1 ∧
                    nSwap = nSwap_1 ∧
                      inBlock = inBlock_1 ∧
                        outBlock = outBlock_1 ∧
                          msgSent = msgSent_1 ∧
                            msgRecv = msgRecv_1 ∧
                              signals = signals_1 ∧ voluntaryCS = voluntaryCS_1 ∧ involuntaryCS = involuntaryCS_1
-- Init.Data.Rat.Lemmas
Rat.divInt_self' : ∀ {n : ℤ}, n ≠ 0 → Rat.divInt n n = 1
-- Mathlib.Logic.Function.Basic
Function.injective_comp_right_iff_surjective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {γ : Type u_4} [Nontrivial γ],
  (Function.Injective fun g => g ∘ f) ↔ Function.Surjective f
-- Mathlib.LinearAlgebra.Dimension.Constructions
Subalgebra.rank_toSubmodule : ∀ {F : Type u_2} {E : Type u_3} [inst : CommSemiring F] [inst_1 : Semiring E] [inst_2 : Algebra F E]
  (S : Subalgebra F E), Module.rank F ↥(Subalgebra.toSubmodule S) = Module.rank F ↥S
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.mk.inj : ∀ {X : SSet} {spineToSimplex : {n : ℕ} → X.Path n → X.obj (Opposite.op { len := n })}
  {spine_spineToSimplex : ∀ (n : ℕ), X.spine n ∘ spineToSimplex = id}
  {spineToSimplex_spine : ∀ (n : ℕ), spineToSimplex ∘ X.spine n = id}
  {spineToSimplex_1 : {n : ℕ} → X.Path n → X.obj (Opposite.op { len := n })}
  {spine_spineToSimplex_1 : ∀ (n : ℕ), X.spine n ∘ spineToSimplex_1 = id}
  {spineToSimplex_spine_1 : ∀ (n : ℕ), spineToSimplex_1 ∘ X.spine n = id},
  { spineToSimplex := spineToSimplex, spine_spineToSimplex := spine_spineToSimplex,
        spineToSimplex_spine := spineToSimplex_spine } =
      { spineToSimplex := spineToSimplex_1, spine_spineToSimplex := spine_spineToSimplex_1,
        spineToSimplex_spine := spineToSimplex_spine_1 } →
    spineToSimplex = spineToSimplex_1
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.TreeMap.getEntryLED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α × β → α × β
-- Mathlib.SetTheory.Cardinal.NatCard
/-- If `f` is injective, then `Nat.card α ≤ Nat.card β`. We must also assume
`Nat.card β = 0 → Nat.card α = 0` since `Nat.card` is defined to be `0` for infinite types.  -/
Finite.card_le_of_injective' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Injective f → (Nat.card β = 0 → Nat.card α = 0) → Nat.card α ≤ Nat.card β
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.fold : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (β → α → β) → β → Lean.PersistentHashSet α → β
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.empty_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β}, ∅ = m ↔ m = ∅
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.eval_germ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] {R : Type u}
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (U : TopologicalSpace.Opens M) (x : M) (hx : x ∈ U)
  (f : ↑((smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op U))),
  (smoothSheafCommRing.eval IM I M R x)
      ((CategoryTheory.ConcreteCategory.hom ((smoothSheafCommRing IM I M R).presheaf.germ U x hx)) f) =
    ↑f ⟨x, hx⟩
-- Mathlib.Data.Finset.Sum
Finset.disjSum_strictMono_left : ∀ {α : Type u_1} {β : Type u_2} (t : Finset β), StrictMono fun s => s.disjSum t
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adjunction.ofCat_comp : ∀ {C D E : CategoryTheory.Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : CategoryTheory.Bicategory.Adjunction F G) {F' : D ⟶ E}
  {G' : E ⟶ D} (adj' : CategoryTheory.Bicategory.Adjunction F' G'),
  CategoryTheory.Adjunction.ofCat (adj.comp adj') =
    (CategoryTheory.Adjunction.ofCat adj).comp (CategoryTheory.Adjunction.ofCat adj')
-- Mathlib.Logic.Relation
/-- **Alias** of `Std.Refl.comap`. -/
Reflexive.comap : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [Std.Refl r] (f : α → β), Std.Refl (Function.onFun r f)
-- Lean.Util.Trace
Lean.inheritedTraceOptions : IO.Ref (Std.HashSet Lean.Name)
-- Mathlib.Data.Matrix.Diagonal
Matrix.submatrix_diagonal_embedding : ∀ {l : Type u_1} {m : Type u_2} {α : Type v} [inst : Zero α] [inst_1 : DecidableEq m] [inst_2 : DecidableEq l]
  (d : m → α) (e : l ↪ m), (Matrix.diagonal d).submatrix ⇑e ⇑e = Matrix.diagonal (d ∘ ⇑e)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.count_edges_eq_one : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v},
  p.IsTrail → ∀ {e : Sym2 V}, e ∈ p.edges → List.count e p.edges = 1
-- Init.Data.Nat.Bitwise.Lemmas
Nat.not_decide_mod_two_eq_one : ∀ (x : ℕ), (!decide (x % 2 = 1)) = decide (x % 2 = 0)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.mk' : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [inst_1 : Ring R] (v : Valuation R Γ)
  [IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup] [Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup],
  v.IsRankOneDiscrete
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.shiftFunctor₂XXIso_refl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (a b y : ℤ),
  K.shiftFunctor₂XXIso a b y (b + y) ⋯ =
    CategoryTheory.Iso.refl ((((HomologicalComplex₂.shiftFunctor₂ C y).obj K).X a).X b)
-- Init.Data.Ord.SInt
Int32.instLawfulEqOrd : Std.LawfulEqOrd Int32
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.HasLeftKanExtension.mk : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c},
  CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftExtension f g) →
    CategoryTheory.Bicategory.HasLeftKanExtension f g
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulRightMap_eq_mulMap_comp : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M : Submodule R S)
  {N : Submodule R S} {ι : Type u_1} [inst_3 : DecidableEq ι] (n : ι → ↥N),
  M.mulRightMap n =
    M.mulMap N ∘ₗ
      LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ ↑(TensorProduct.finsuppScalarRight R R (↥M) ι).symm
-- Mathlib.Algebra.Algebra.Defs
RingHom.algebraMap_toAlgebra' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] (i : R →+* S)
  (h : ∀ (c : R) (x : S), i c * x = x * i c), algebraMap R S = i
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_le_iff_le_cons : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} {a : α}, s.erase a ≤ t ↔ s ≤ a ::ₘ t
-- Mathlib.Analysis.Normed.Ring.Basic
/-- In a seminormed ring, the left-multiplication `AddMonoidHom` is bounded.  -/
mulLeft_bound : ∀ {α : Type u_2} [inst : NonUnitalSeminormedRing α] (x y : α), ‖(AddMonoidHom.mulLeft x) y‖ ≤ ‖x‖ * ‖y‖
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.support_neg_subset : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : NegZeroClass R] (x : HahnSeries Γ R),
  (-x).support ⊆ x.support
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.toSupBotHom : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] →
        [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → BoundedLatticeHom α β → SupBotHom α β
-- Lean.Compiler.LCNF.Basic
/-- Allocating a constructor.
 -/
Lean.Compiler.LCNF.LetValue.ctor : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.CtorInfo →
    Array (Lean.Compiler.LCNF.Arg pu) →
      autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_5 →
        Lean.Compiler.LCNF.LetValue pu
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey!_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] [inst_2 : Inhabited α] {β : Type v} {f : α → β → Bool}
  {l : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k (List.filter (fun p => f p.fst p.snd) l) =
      ((Std.Internal.List.getKey? k l).pfilter fun x h => f x (Std.Internal.List.getValue x l ⋯)).get!
-- Mathlib.GroupTheory.Commutator.Basic
/-- **The Hall-Witt identity**  -/
commutatorElement_conj_commutatorElement_mul : ∀ {G : Type u_1} [inst : Group G] (a b c : G), ⁅a * b * a⁻¹, ⁅c, a⁆⁆ * ⁅c * a * c⁻¹, ⁅b, c⁆⁆ * ⁅b * c * b⁻¹, ⁅a, b⁆⁆ = 1
-- Lean.Structure
Lean.StructureResolutionOrderResult.resolutionOrder : Lean.StructureResolutionOrderResult → Array Lean.Name
-- Aesop.RuleSet
Aesop.GlobalRuleSet.contains : Aesop.GlobalRuleSet → Aesop.RuleName → Bool
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_toReal_le_pi : ∀ (θ : Real.Angle), |θ.toReal| ≤ Real.pi
-- Mathlib.Data.Num.Lemmas
Num.succ.eq_1 : ∀ (n : Num), n.succ = Num.pos n.succ'
-- Init.Data.Int.Lemmas
Int.mul_neg_one : ∀ (a : ℤ), a * -1 = -a
-- Mathlib.Dynamics.Ergodic.Ergodic
PreErgodic.ae_mem_or_ae_notMem : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  PreErgodic f μ → MeasurableSet s → f ⁻¹' s = s → (∀ᵐ (x : α) ∂μ, x ∈ s) ∨ ∀ᵐ (x : α) ∂μ, x ∉ s
-- Mathlib.Data.NNReal.Basic
NNReal.toReal_lt : ∀ (a b : NNReal), a < b ↔ ↑a < ↑b
-- Init.Data.Char.Ordinal
/-- The number of surrogate code points.  -/
Char.numSurrogates : ℕ
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.insert.match_3.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G) (a : ↑A),
  ((fun₀ | g⁻¹ => (A.ρ g⁻¹) a) + fun₀ | g => a) ∈ groupHomology.boundaries₁ A
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_singleton_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  Module.IsTorsionBySet R M {a} ↔ Module.IsTorsionBy R M a
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization.eq_1 : ∀ (n : ℕ),
  n.factorization =
    { support := n.primeFactors, toFun := fun p => if Nat.Prime p then padicValNat p n else 0, mem_support_toFun := ⋯ }
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.regularity : ∀ (x : ZFSet.{u}), x ≠ ∅ → ∃ y ∈ x, x ∩ y = ∅
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom₂.ext_iff : ∀ {B : Type u_1} {C : Type u_2} {inst : CategoryTheory.Bicategory C} {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y}
  {x y : CategoryTheory.Bicategory.InducedBicategory.Hom₂ f g}, x = y ↔ x.hom = y.hom
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.neg_Y : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.neg P 1 = W'.negY P
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.funMap_sumInr : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M]
  [inst_1 : (L'.sum L).Structure M] [FirstOrder.Language.LHom.sumInr.IsExpansionOn M] {n : ℕ} {f : L.Functions n}
  {x : Fin n → M}, FirstOrder.Language.Structure.funMap (Sum.inr f) x = FirstOrder.Language.Structure.funMap f x
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_int16ToInt : ∀ (x : Int16), ISize.ofIntLE x.toInt ⋯ ⋯ = x.toISize
-- Mathlib.Order.Interval.Set.Disjoint
iUnion_Iio_eq_univ_iff : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {f : ι → α}, ⋃ i, Set.Iio (f i) = Set.univ ↔ ¬BddAbove (Set.range f)
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.instBEqConfig.beq : Mathlib.Tactic.AtomM.Recurse.Config → Mathlib.Tactic.AtomM.Recurse.Config → Bool
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousWithinAt.const_smul : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {b : β} {s : Set β},
  ContinuousWithinAt g s b → ∀ (c : M), ContinuousWithinAt (c • g) s b
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocExtensionMap : Type
-- Mathlib.Order.Bounds.Image
MonotoneOn.mem_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {a : α},
  MonotoneOn f t → s ⊆ t → a ∈ lowerBounds s → a ∈ t → f a ∈ lowerBounds (f '' s)