mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData'_right_H : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hk : c.next j = k) (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData' K e hj' hi hk h).right.H = h.right.H
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_choice : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] (x : α), |x|ₘ = x ∨ |x|ₘ = x⁻¹
-- Mathlib.Util.Delaborators
/-- Override the Lean 4 pi notation delaborator with one that uses `Π` and prints
cute binders such as `∀ ε > 0`.
Note that this takes advantage of the fact that `(x : α) → p x` notation is
never used for propositions, so we can match on this result and rewrite it.  -/
PiNotation.delabPi' : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Order.AddTorsor
Monotone.vadd : ∀ {G : Type u_1} {P : Type u_2} {γ : Type u_3} [inst : Preorder G] [inst_1 : Preorder P] [inst_2 : Preorder γ]
  [inst_3 : VAdd G P] [IsOrderedVAdd G P] {f : γ → G} {g : γ → P},
  Monotone f → Monotone g → Monotone fun x => f x +ᵥ g x
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.toOpposite_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N)
  (hf : ∀ (x y : M), AddCommute (f x) (f y)), ⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsPushout.isAlgebraic' : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] (R' : Type u_4) [inst_3 : CommRing R'] [inst_4 : Algebra R R'] [NoZeroDivisors R']
  [FaithfulSMul R R'] (S' : Type u_5) [inst_7 : CommRing S'] [inst_8 : Algebra R S'] [inst_9 : Algebra S S']
  [inst_10 : Algebra R' S'] [inst_11 : IsScalarTower R R' S'] [inst_12 : IsScalarTower R S S']
  [Algebra.IsPushout R R' S S'], Algebra.IsAlgebraic R' S'
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The base ring is a left identity for the tensor product of algebra, up to algebra isomorphism.
 -/
Algebra.TensorProduct.lid : (R : Type uR) →
  (A : Type uA) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → TensorProduct R R A ≃ₐ[R] A
-- Mathlib.Topology.Separation.Regular
/-- A regular topological space with a Lindelöf topology is a normal space. A consequence of e.g.
Corollaries 20.8 and 20.10 of [Willard's *General Topology*][zbMATH02107988] (without the
assumption of Hausdorff).  -/
NormalSpace.of_regularSpace_lindelofSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] [LindelofSpace X], NormalSpace X
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Piecewise modified version of `f` with optimal asymptotics. We deliberately choose intervals
which don't quite join up, so the function is `0` at `x = 1`, in order to maintain symmetry;
there is no "good" choice of value at `1`.  -/
WeakFEPair.f_modif : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → ℝ → E
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Reduction step for the additive free group relation: `w + x + (-x) + v ~> w + v`  -/
FreeAddGroup.Red.Step : {α : Type u} → List (α × Bool) → List (α × Bool) → Prop
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.range_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A],
  Set.range DoubleCentralizer.toProd = {lr | ∀ (x y : A), lr.2 x * y = x * lr.1 y}
-- Init.Data.Int.Linear
Int.Internal.Linear.le_combine_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.nil_iff_eq_nil : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v}, p.Nil ↔ p = SimpleGraph.Walk.nil
-- Mathlib.Topology.Closure
/-- **Alias** of the reverse direction of `frontier_subset_iff_isClosed`. -/
IsClosed.frontier_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → frontier s ⊆ s
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.affineCombinationLineMapWeights_apply_right : ∀ {k : Type u_1} [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] {i j : ι},
  i ≠ j → ∀ (c : k), Finset.affineCombinationLineMapWeights i j c j = c
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.operator.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.operator = 1
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedComponent.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α) (x : α), s.ordConnectedComponent x = {y | Set.uIcc x y ⊆ s}
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.beq.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] [inst_2 : (k : α) → BEq (β k)]
  (t₁ t₂ : Std.DTreeMap.Internal.Impl α β),
  t₁.beq t₂ = if t₁.size ≠ t₂.size then false else t₁.all fun k v => t₂.get? k == some v
-- Mathlib.Order.Bounds.Basic
bddAbove_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, BddAbove (Set.Ico a b)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Right duals are isomorphic.  -/
CategoryTheory.rightDualIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y₁ Y₂ : C} → CategoryTheory.ExactPairing X Y₁ → CategoryTheory.ExactPairing X Y₂ → (Y₁ ≅ Y₂)
-- Mathlib.Order.LiminfLimsup
Filter.limsup_piecewise : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} {s : Set β}
  [inst_1 : DecidablePred fun x => x ∈ s] {v : β → α},
  Filter.limsup (s.piecewise u v) f = (Filter.blimsup u f fun x => x ∈ s) ⊔ Filter.blimsup v f fun x => x ∉ s
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_subset_Ioc_union_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a c ⊆ Set.Ioc a b ∪ Set.Icc b c
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.unop_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.NatTrans.unop (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.unop β) (CategoryTheory.NatTrans.unop α)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_subset_sdiv_left : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t₁ t₂ : Set β}, t₁ ⊆ t₂ → s /ₛ t₁ ⊆ s /ₛ t₂
-- Init.Data.Option.Lemmas
Option.filter_pfilter : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} {q : α → Bool},
  Option.filter q (o.pfilter p) = o.pfilter fun a h => p a h && q a
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- If two additive homomorphisms from `R[M]` are equal on each `single r m`, then they are equal.

We formulate this using equality of `AddMonoidHom`s so that `ext` tactic can apply a type-specific
extensionality lemma after this one.  E.g., if the fiber `M` is `ℕ` or `ℤ`, then it suffices to
verify `f (single a 1) = g (single a 1)`.

TODO: Rename to `addMonoidHom_ext'`.  -/
AddMonoidAlgebra.addHom_ext' : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {N : Type u_8} [inst_1 : AddZeroClass N]
  ⦃f g : AddMonoidAlgebra R M →+ N⦄,
  (∀ (m : M), f.comp (AddMonoidAlgebra.singleAddHom m) = g.comp (AddMonoidAlgebra.singleAddHom m)) → f = g
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.inv : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f : β → α}, Multipliable f L → Multipliable (fun b => (f b)⁻¹) L
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Mon C),
  CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F =
    CategoryTheory.Iso.refl
      (((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).comp
              (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C)).obj
          F).X
-- Init.Data.SInt.Lemmas
Int16.add_right_neg : ∀ (a : Int16), a + -a = 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.lift_cof_congr_of_strictMono : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  StrictMono f → IsCofinal (Set.range f) → Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, v} (Order.cof β)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.comp_hom'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N K : CategoryTheory.Mon C} (f : M ⟶ N) (g : N ⟶ K) {Z : C} (h : K.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.root.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), AdjoinRoot.root f = (AdjoinRoot.mk f) Polynomial.X
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.map_inf : ∀ {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] [inst_7 : IsScalarTower R A A] [inst_8 : SMulCommClass R A A]
  [inst_9 : IsScalarTower R B B] [inst_10 : SMulCommClass R B B] (f : F),
  Function.Injective ⇑f →
    ∀ (S T : NonUnitalSubalgebra R A),
      NonUnitalSubalgebra.map f (S ⊓ T) = NonUnitalSubalgebra.map f S ⊓ NonUnitalSubalgebra.map f T
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.zsmul_sub_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddCommGroup α] [inst_1 : SubtractionMonoid β],
  Function.Antiperiodic f c → ∀ (n : ℤ), f (n • c - x) = ↑n.negOnePow • f (-x)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.erase : Lean.Meta.Origin → Lean.Elab.Tactic.ElabSimpArgResult
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.cons.sizeOf_spec : sizeOf Turing.PartrecToTM2.Γ'.cons = 1
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.nextCoeff_C_eq_zero : ∀ {R : Type u} [inst : Semiring R] (c : R), (Polynomial.C c).nextCoeff = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Homeomorph.measurableEmbedding : ∀ {γ : Type u_3} {γ₂ : Type u_4} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ]
  [inst_3 : TopologicalSpace γ₂] [inst_4 : MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂), MeasurableEmbedding ⇑h
-- Mathlib.Analysis.Calculus.Deriv.Pow
deriv_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {f : 𝕜 → 𝔸} {x : 𝕜},
  DifferentiableAt 𝕜 f x → ∀ (n : ℕ), deriv (f ^ n) x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * deriv f x * f x ^ i
-- Mathlib.GroupTheory.Commutator.Basic
/-- **The Hall-Witt identity**  -/
conj_commutatorElement_right_commutatorElement_mul : ∀ {G : Type u_1} [inst : Group G] (a b c : G),
  b * ⁅a, ⁅b⁻¹, c⁆⁆ * b⁻¹ * c * ⁅b, ⁅c⁻¹, a⁆⁆ * c⁻¹ * a * ⁅c, ⁅a⁻¹, b⁆⁆ * a⁻¹ = 1
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
_private.Std.Tactic.BVDecide.LRAT.Internal.Convert.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_6.splitter : {n : ℕ} →
  (motive : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → Sort u_1) →
    (acc : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool)) →
      (Unit → motive none) →
        ((map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → motive (some map)) → motive acc
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.instCoeTC : {M : Type u_1} →
  [inst : Monoid M] → {X : Type u} → [inst_1 : MulAction M X] → CoeTC X (CategoryTheory.ActionCategory M X)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.toMethodsRefImpl : Lean.Meta.Simp.Methods → Lean.Meta.Simp.MethodsRef
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.j_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] [CharP R 2],
  W.j = ↑W.Δ'⁻¹ * W.a₁ ^ 12
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = (t.isEmpty || t.size == 1 && t.contains k)
-- Init.Data.Nat.Basic
Nat.not_le_of_lt : ∀ {a b : ℕ}, a < b → ¬b ≤ a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.ExtDHashMap.Const.unitOfList l).getKeyD k fallback = fallback
-- Mathlib.Analysis.Calculus.VectorField
Filter.EventuallyEq.lieBracket_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {x : E},
  V₁ =ᶠ[nhds x] V → W₁ =ᶠ[nhds x] W → VectorField.lieBracket 𝕜 V₁ W₁ =ᶠ[nhds x] VectorField.lieBracket 𝕜 V W
-- Mathlib.Algebra.Order.Ring.Abs
/-- `2` is not a factor of an odd natural number.  -/
Odd.ne_two_of_dvd_nat : ∀ {m n : ℕ}, Odd n → m ∣ n → m ≠ 2
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.restrict_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) (W : Submodule R M) (m : ↥W), (B.restrict W) m = (B ↑m).domRestrict W
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
/-- Eta-expanded form of `InnerProductSpace.HarmonicContOnCl.const_sub` -/
InnerProductSpace.HarmonicContOnCl.fun_const_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ∀ (c : F), InnerProductSpace.HarmonicContOnCl (fun i => c - f i) s
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.alls.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (φ : L.BoundedFormula α 0), φ.alls = φ
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.instRingOfIsScalarTower : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (P : Algebra.Extension R S) →
            {R₀ : Type u_1} →
              [inst_3 : CommRing R₀] →
                [inst_4 : Algebra R₀ R] → [inst_5 : Algebra R₀ S] → [IsScalarTower R₀ R S] → Algebra R₀ P.Ring
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_ofIsHomeomorph : ∀ {S : Type u_1} [inst : Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [inst_1 : Semiring S₁]
  {σ : S →+* S₁} {σ' : S₁ →+* S} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
  [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M] [inst_6 : Module S M] [inst_7 : TopologicalSpace M₁]
  [inst_8 : AddCommMonoid M₁] [inst_9 : Module S₁ M₁] {f : M ≃ₛₗ[σ] M₁} (hf : IsHomeomorph ⇑f),
  ⇑(ContinuousLinearEquiv.ofIsHomeomorph f hf) = ⇑f
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.isLittleO_log_re_re : ∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → (fun z => Real.log z.re) =o[l] Complex.re
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.functor_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] (X : C)
  {x x_1 : C} (g : x ⟶ x_1),
  (CategoryTheory.Limits.prod.functor.obj X).map g =
    CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) g
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.arcosh_surjOn : Set.SurjOn Real.arcosh (Set.Ici 1) (Set.Ici 0)
-- Mathlib.CategoryTheory.Square
/-- The functor `(Square Cᵒᵖ)ᵒᵖ ⥤ Square Cᵒᵖ`.  -/
CategoryTheory.Square.unopFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Square Cᵒᵖ)ᵒᵖ (CategoryTheory.Square C)
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.toRingHom_toOpposite : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)),
  ↑(f.toOpposite hf) = (↑f).toOpposite hf
-- Mathlib.Data.Finmap
/-- Erase a key from the map, and return the corresponding value, if found.  -/
Finmap.extract : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → Finmap β → Option (β a) × Finmap β
-- Mathlib.Topology.ClusterPt
/-- **Alias** of the reverse direction of `mapClusterPt_id_iff`. -/
ClusterPt.mapClusterPt_id : ∀ {α : Type u_1} {F : Filter α} [inst : TopologicalSpace α] {a : α}, ClusterPt a F → MapClusterPt a F id
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable.0.EisensteinSeries.one_div_linear_sub_one_div_linear_eq : ∀ (z : UpperHalfPlane) (a b m : ℤ),
  m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0 → 1 / (↑m * ↑z + ↑a) - 1 / (↑m * ↑z + ↑b) = (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ` is bounded.  -/
FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal}, ↑r < p.radius → ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
-- Lean.Environment
Lean.instInhabitedEnvExtension.default : {σ : Type} → Lean.EnvExtension σ
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] (F : CategoryTheory.Pseudofunctor B' B) (x : B'),
  ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).mapId x).inv.iso.hom = (F.mapId x).inv
-- Mathlib.Topology.MetricSpace.IsometricSMul
ULift.isIsometricVAdd' : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X] [IsIsometricVAdd M X],
  IsIsometricVAdd M (ULift.{u_2, w} X)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m.erase k).getKey? k = none
-- Mathlib.Order.CompleteBooleanAlgebra
le_iInf_iSup : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : CompleteLattice α] {f : (a : ι) → κ a → α},
  ⨆ g, ⨅ a, f a (g a) ≤ ⨅ a, ⨆ b, f a b
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.isLocalizingSequence_const_top : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : TopologicalSpace ι]
  [inst_2 : OrderTopology ι] (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω),
  ProbabilityTheory.IsLocalizingSequence 𝓕 (fun x x_1 => ⊤) P
-- Init.Data.BitVec.Lemmas
BitVec.self_eq_add_right : ∀ {w : ℕ} {x y : BitVec w}, x = x + y ↔ y = 0#w
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- A continuous linear equivalence between normed spaces is a diffeomorphism.  -/
ContinuousLinearEquiv.toDiffeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                (E ≃L[𝕜] E') → Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ↑⊤
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_eq_ofInt : ∀ {n : ℤ} (h₁ : ISize.minValue.toInt ≤ n) (h₂ : n ≤ ISize.maxValue.toInt), ISize.ofIntLE n h₁ h₂ = ISize.ofInt n
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.subLeft_symm_apply : ∀ {G : Type u_5} [inst : AddGroup G] (a b : G), (Equiv.subLeft a).symm b = -b + a
-- Mathlib.Data.Int.Init
Int.inductionOn'.pos.eq_def : ∀ {motive : ℤ → Sort u_1} (b : ℤ) (zero : motive b) (succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)) (n : ℕ),
  Int.inductionOn'.pos b zero succ n =
    match n with
    | 0 => cast ⋯ zero
    | n.succ => cast ⋯ (succ (b + ↑n) ⋯ (Int.inductionOn'.pos b zero succ n))
-- Mathlib.Control.EquivFunctor.Instances
EquivFunctorUnique : EquivFunctor Unique
-- Mathlib.Analysis.LocallyConvex.Basic
/-- Scalar multiplication (by possibly different types) of a balanced set is monotone.  -/
Balanced.smul_mono : ∀ {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {s : Set E} [inst_3 : NormedRing 𝕝] [inst_4 : Module 𝕜 𝕝] [NormSMulClass 𝕜 𝕝]
  [inst_6 : SMulWithZero 𝕝 E] [IsScalarTower 𝕜 𝕝 E] {b : 𝕜}, Balanced 𝕝 s → ∀ {a : 𝕝}, ‖a‖ ≤ ‖b‖ → a • s ⊆ b • s
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compPartialSumTargetSet.eq_1 : ∀ (m M N : ℕ),
  FormalMultilinearSeries.compPartialSumTargetSet m M N =
    {i | m ≤ i.snd.length ∧ i.snd.length < M ∧ ∀ (j : Fin i.snd.length), i.snd.blocksFun j < N}
-- Mathlib.RingTheory.LocalProperties.Exactness
surjective_of_localized_maximal : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  (∀ (J : Ideal R) [inst_5 : J.IsMaximal], Function.Surjective ⇑((LocalizedModule.map J.primeCompl) f)) →
    Function.Surjective ⇑f
-- Mathlib.Analysis.Complex.Basic
Complex.instRCLike : RCLike ℂ
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.lt : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α] {f g : δ → α},
  Measurable f → Measurable g → Measurable fun a => f a < g a
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_mod : ∀ {a b : UInt64}, (a % b).toBitVec = a.toBitVec % b.toBitVec
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.inverse_comp_equiv : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : TopologicalSpace M]
  [inst_1 : TopologicalSpace M₂] [inst_2 : TopologicalSpace M₃] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {e : M₃ ≃L[R] M} {f : M →L[R] M₂}, (f ∘SL ↑e).inverse = ↑e.symm ∘SL f.inverse
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.isNat_zero_eq : ∀ {A : Type u_2} [sA : CommSemiring A] {a : A}, Mathlib.Meta.NormNum.IsNat a 0 → a = 0
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_min : ∀ {a b : Cardinal.{v}}, Cardinal.lift.{u, v} (min a b) = min (Cardinal.lift.{u, v} a) (Cardinal.lift.{u, v} b)
-- Mathlib.Order.Hom.PowersetCard
Set.powersetCard.orderIsoOfFin_apply_coe : ∀ {n : ℕ} {I : Type u_2} [inst : LinearOrder I] (s : ↑(Set.powersetCard I n)) (a : Fin n),
  ↑((Set.powersetCard.orderIsoOfFin s) a) = ((↑s).sort fun a b => a ≤ b)[↑a]
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.unit_one : ∀ {M : Type u_1} [inst : Monoid M] (h : IsUnit 1), h.unit = 1
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- Local instance to help the typeclass system to figure out `1 + 1 = 2`.  -/
finrank_real_complex_fact' : Fact (Module.finrank ℝ ℂ = 1 + 1)
-- Init.Prelude
/-- Sequences two `EStateM ε σ` actions, running `x` before `y`. The first action's return value is
ignored.
 -/
EStateM.seqRight : {ε σ α β : Type u} → EStateM ε σ α → (Unit → EStateM ε σ β) → EStateM ε σ β