mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.foldM_mapWithPostcondition : ∀ {α β γ δ : Type w} {ps : Std.Do.PostShape} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o]
  [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [inst_8 : Std.Do.WPMonad o ps] [inst_9 : Std.IteratorLoop α m n]
  [inst_10 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o]
  [inst_13 : MonadLiftT m n] [inst_14 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
  {f : β → Std.Iterators.PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Std.IterM m β} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let c ← liftM (f b).run
          g d c)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.IterM.mapWithPostcondition f it) ⦃Q⦄
-- Mathlib.Data.Finset.Sups
Finset.mem_sups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t : Finset α} {c : α},
  c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.IsLimit.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} {k l : W ⟶ s.pt},
  CategoryTheory.CategoryStruct.comp k s.base = CategoryTheory.CategoryStruct.comp l s.base →
    (∀ (i : ι), CategoryTheory.CategoryStruct.comp k (s.π i) = CategoryTheory.CategoryStruct.comp l (s.π i)) → k = l
-- Mathlib.Topology.Semicontinuity.Basic
/-- A lower semicontinuous function is bounded below on a compact set.  -/
LowerSemicontinuousOn.bddBelow_of_isCompact : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} [inst_1 : LinearOrder β] [Nonempty β]
  {s : Set α}, IsCompact s → LowerSemicontinuousOn f s → BddBelow (f '' s)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- Descend to the explicit cokernel.  -/
SemiNormedGrp.explicitCokernelDesc : {X Y Z : SemiNormedGrp} →
  {f : X ⟶ Y} → {g : Y ⟶ Z} → CategoryTheory.CategoryStruct.comp f g = 0 → (SemiNormedGrp.explicitCokernel f ⟶ Z)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Given three nonzero vectors, the angle between the first and the third minus the angle
between the first and the second equals the angle between the second and the third.  -/
Orientation.oangle_sub_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y z : V}, x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle x z - o.oangle x y = o.oangle y z
-- Mathlib.Algebra.Group.Equiv.Defs
/-- A multiplicative isomorphism of monoids sends `1` to `1` (and is hence a monoid isomorphism).  -/
MulEquiv.map_one : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (h : M ≃* N), h 1 = 1
-- Init.Ext
Sigma.ext_iff : ∀ {α : Type u} {β : α → Type v} {x y : Sigma β}, x = y ↔ x.fst = y.fst ∧ x.snd ≍ y.snd
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.toExpr' : {n : ℕ} → BitVec n → Lean.Meta.SimpM Lean.Expr
-- Lean.ResolveName
/-- Like `Lean.unresolveNameGlobal?`, but also ensures that the unresolved name does not conflict
with the names of any local declarations. Returns `none` if the name cannot be referred to.
For example, the name may be private and not accessible to the current module, or it may have macro scopes. -/
Lean.unresolveNameGlobalAvoidingLocals? : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] →
            [Lean.AddMessageContext m] → [Lean.MonadLCtx m] → Lean.Name → optParam Bool false → m (Option Lean.Name)
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.GuitartExact.hComp'_iff_of_essSurj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {V₁ : CategoryTheory.Functor C₁ D₁} {T₁ : CategoryTheory.Functor C₁ C₂} {B₁ : CategoryTheory.Functor D₁ D₂}
  {V₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) {T₂ : CategoryTheory.Functor C₂ C₃}
  {B₂ : CategoryTheory.Functor D₂ D₃} {V₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare T₂ V₂ V₃ B₂)
  {T₁₂ : CategoryTheory.Functor C₁ C₃} {B₁₂ : CategoryTheory.Functor D₁ D₃} (eT : T₁.comp T₂ ≅ T₁₂)
  (eB : B₁.comp B₂ ≅ B₁₂) [B₁.EssSurj] [w.GuitartExact], (w.hComp' w' eT eB).GuitartExact ↔ w'.GuitartExact
-- Lean.Parser.Term
/-- Termination hints are `termination_by` and `decreasing_by`, in that order.
 -/
Lean.Parser.Termination.suffix : Lean.Parser.Parser
-- Mathlib.RingTheory.LinearDisjoint
/-- If a basis of `A` is also `B`-linearly independent, if elements in `A` and `B` commute,
then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_basis_left_of_commute : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  {ι : Type u_1} (a : Module.Basis ι R ↥A),
  LinearIndependent (↥B) (⇑A.val ∘ ⇑a) → (∀ (a : ↥A) (b : ↥B), Commute ↑a ↑b) → A.LinearDisjoint B
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] {f g : α →+o β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Control.Basic
joinM_pure : ∀ {m : Type u → Type u} [inst : Monad m] [LawfulMonad m] {α : Type u} (a : m α), joinM (pure a) = a
-- Mathlib.RingTheory.SimpleModule.Basic
/-- A binary product of semisimple rings is semisimple.  -/
instIsSemisimpleRingProd : ∀ {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : Ring S] [hR : IsSemisimpleRing R] [hS : IsSemisimpleRing S],
  IsSemisimpleRing (R × S)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.andthen.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Array.Count
Array.count_set : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {i : ℕ} {a b : α} (h : i < xs.size),
  Array.count b (xs.set i a h) =
    (Array.count b xs - if (xs[i] == b) = true then 1 else 0) + if (a == b) = true then 1 else 0
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- Over the real numbers, we can register the previous statement as an instance as it will not
cause problems in instance resolution since the properness of `ℝ` is already known.  -/
FiniteDimensional.proper_real : ∀ (E : Type u) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E], ProperSpace E
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.ofHom_apply : ∀ {X Y : Type u} [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] (f : X →+ Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (AddCommGrpCat.ofHom f)) x = f x
-- Batteries.Data.Fin.Lemmas
Fin.findSomeRev?_eq_some_iff : ∀ {n : ℕ} {α : Type u_1} {a : α} {f : Fin n → Option α},
  Fin.findSomeRev? f = some a ↔ ∃ i, f i = some a ∧ ∀ (j : Fin n), i < j → f j = none
-- Batteries.Data.List.Lemmas
List.swap_cons : ∀ {α : Type u_1} {a : α} {xs : List α} {i j : ℕ}, (a :: xs).swap (i + 1) (j + 1) = a :: xs.swap i j
-- Mathlib.CategoryTheory.Sites.Closed
CategoryTheory.GrothendieckTopology.close_close : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
  (S : CategoryTheory.Sieve X), J₁.close (J₁.close S) = J₁.close S
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.List.toArrayAux.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : Array α),
  x.toArrayAux x_1 =
    match x, x_1 with
    | [], xs => xs
    | a :: as, xs => as.toArrayAux (xs.push a)
-- Mathlib.Data.Tree.Basic
BinaryTree.brecOn.go : {α : Type u} →
  {motive : BinaryTree α → Sort u_1} →
    (t : BinaryTree α) → ((t : BinaryTree α) → BinaryTree.below t → motive t) → motive t ×' BinaryTree.below t
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_mul : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R}, (p * q).degree = p.degree + q.degree
-- Init.Data.String.Basic
String.utf8Encode_toList : ∀ {b : String}, b.toList.utf8Encode = b.toByteArray
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval_2 : ∀ {a0 a1 a2 : ℤ} {t : List ℤ},
  (Lean.Omega.LinearCombo.coordinate 2).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: t)) = a2
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiAlgebra_eq_mkPiAlgebraFin : ∀ (R : Type u) (A : Type u_1) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace A] [inst_4 : ContinuousMul A] {n : ℕ},
  ContinuousMultilinearMap.mkPiAlgebra R (Fin n) A = ContinuousMultilinearMap.mkPiAlgebraFin R n A
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.isQueueEmpty : Lean.Meta.Grind.Arith.CommRing.RingM Bool
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalSeminormedRing.toSeminormedAddCommGroup : {α : Type u_2} → [NonUnitalSeminormedRing α] → SeminormedAddCommGroup α
-- Lean.ParserCompiler
Lean.ParserCompiler.Context.combinatorAttr : {α : Type} → Lean.ParserCompiler.Context α → Lean.ParserCompiler.CombinatorAttribute
-- Lean.Parser.Term
/-- Logs an error, tagging the message as a named error with the specified name and validating that an
associated error explanation exists. The error name must be followed by a `Syntax` at which the
error is to be logged. The message is the final argument and may be passed as an interpolated string
or a `MessageData` term.
 -/
Lean.Parser.Term.logNamedErrorAtMacro : Lean.Parser.Parser
-- Mathlib.Algebra.BigOperators.Expect
Fintype.expect_ite_eq' : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Module ℚ≥0 M]
  [inst_3 : DecidableEq ι] (i : ι) (f : ι → M),
  (Finset.univ.expect fun j => if j = i then f j else 0) = (↑(Fintype.card ι))⁻¹ • f i
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- Open immersions are smooth.  -/
AlgebraicGeometry.instSmoothOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f], AlgebraicGeometry.Smooth f
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.zero_comp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.comp 0 p = 0
-- Mathlib.Topology.ContinuousMap.Polynomial
/-- The algebra map from `R[X]` to continuous functions `C(X, R)`, for any subset `X` of `R`.
 -/
Polynomial.toContinuousMapOnAlgHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : TopologicalSpace R] → [inst_2 : IsTopologicalSemiring R] → (X : Set R) → Polynomial R →ₐ[R] C(↑X, R)
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_eq_empty_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc a b = ∅ ↔ ¬a ≤ b
-- Lean.Elab.DocString
/-- A provider of suggestions for code elements.
 -/
Lean.Doc.CodeBlockSuggester : Type
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Nonempty.mk : ∀ {α : Type u_1} {M : Matroid α}, M.E.Nonempty → M.Nonempty
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_Iic : ∀ {n : ℕ} (i : Fin n), Fin.succ '' Set.Iic i = Set.Ioc 0 i.succ
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Finset.measurable_restrict₂_apply : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] {s t : Finset α} (hst : s ⊆ t)
  {f : ↥t → γ}, Measurable f → Measurable (Finset.restrict₂ hst f)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.curry.inj : ∀ {ak : Mathlib.Tactic.ITauto.AndKind} {p : Mathlib.Tactic.ITauto.Proof} {ak_1 : Mathlib.Tactic.ITauto.AndKind}
  {p_1 : Mathlib.Tactic.ITauto.Proof},
  Mathlib.Tactic.ITauto.Proof.curry ak p = Mathlib.Tactic.ITauto.Proof.curry ak_1 p_1 → ak = ak_1 ∧ p = p_1
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.Presheaf.IsSheaf.isSeparated : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ A} {FA : A → A → Type u_1}
  {CA : A → Type u_2} [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_3 : CategoryTheory.ConcreteCategory A FA] [J.HasSheafCompose (CategoryTheory.forget A)],
  CategoryTheory.Presheaf.IsSheaf J F → CategoryTheory.Presheaf.IsSeparated J F
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.internalHom_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.MonoidalClosed.internalHom.map f = CategoryTheory.MonoidalClosed.pre f.unop
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.divMonomial_mul_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (a : σ →₀ ℕ) (x : MvPolynomial σ R),
  (x * (MvPolynomial.monomial a) 1).divMonomial a = x
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.serreDerivative.eq_1 : ∀ (k : ℂ) (F : UpperHalfPlane → ℂ) (z : UpperHalfPlane),
  Derivative.serreDerivative k F z = Derivative.normalizedDerivOfComplex F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z
-- Mathlib.SetTheory.Ordinal.Notation
ONote.oadd.inj : ∀ {a : ONote} {a_1 : ℕ+} {a_2 a_3 : ONote} {a_4 : ℕ+} {a_5 : ONote},
  a.oadd a_1 a_2 = a_3.oadd a_4 a_5 → a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.Retract.hasInjectiveDimensionLT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (h : CategoryTheory.Retract X Y) (n : ℕ) [CategoryTheory.HasInjectiveDimensionLT Y n],
  CategoryTheory.HasInjectiveDimensionLT X n
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.IndepFun.charFun_map_add_eq_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {E : Type u_2}
  {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : Ω → E}
  [inst_3 : InnerProductSpace ℝ E] {Y : Ω → E},
  AEMeasurable X P →
    AEMeasurable Y P →
      ProbabilityTheory.IndepFun X Y P →
        MeasureTheory.charFun (MeasureTheory.Measure.map (X + Y) P) =
          MeasureTheory.charFun (MeasureTheory.Measure.map X P) * MeasureTheory.charFun (MeasureTheory.Measure.map Y P)
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.bijective : ∀ {R : Type u} {M : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : Module.Invertible R M], Function.Bijective ⇑(contractLeft R M)
-- Mathlib.Data.Finset.Grade
CovBy.exists_finset_erase : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s ⋖ t → ∃ a ∈ t, t.erase a = s
-- Mathlib.Algebra.Group.Units.Defs
Units.val_inj : ∀ {α : Type u} [inst : Monoid α] {a b : αˣ}, ↑a = ↑b ↔ a = b
-- Mathlib.RingTheory.Jacobson.Radical
Submodule.jacobson_smul_lt_top : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M]
  [IsCoatomic (Submodule R M)] (N : Submodule R M), Ring.jacobson R • N < ⊤
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.const_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.SimplicialObject.Augmented.const.map f).left = (CategoryTheory.SimplicialObject.const C).map f
-- Mathlib.Probability.Process.Adapted
/-- A sequence of functions `u` is strongly adapted to a filtration `f` if for all `i`,
`u i` is `f i`-strongly measurable.  -/
MeasureTheory.StronglyAdapted : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        {β : ι → Type u_3} →
          [(i : ι) → TopologicalSpace (β i)] → MeasureTheory.Filtration ι m → ((i : ι) → Ω → β i) → Prop
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.one_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] (X : C), CategoryTheory.MonObj.one = 0
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.nontrivial_of_degree_ne_zero : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V} [inst : Fintype ↑(G.neighborSet v)], G.degree v ≠ 0 → Nontrivial V
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.beq.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  [inst_3 : (k : α) → BEq (β k)] (m₁ m₁_1 : Std.DHashMap.Raw α β),
  m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.DHashMap.Raw α β), m₂ = m₂_1 → m₁.beq m₂ = m₁_1.beq m₂_1
-- Mathlib.Data.Multiset.MapFold
Multiset.attach_cons : ∀ {α : Type u_1} (a : α) (m : Multiset α), (a ::ₘ m).attach = ⟨a, ⋯⟩ ::ₘ Multiset.map (fun p => ⟨↑p, ⋯⟩) m.attach
-- Mathlib.Algebra.Polynomial.Eval.Subring
Polynomial.notMem_map_range : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {p : Polynomial S},
  p ∉ (Polynomial.mapRingHom f).range ↔ ∃ n, p.coeff n ∉ f.range
-- Mathlib.CategoryTheory.Equivalence
/-- Construct an isomorphism in `C ≌ D` from a natural isomorphism between the functors
of the equivalences.  -/
CategoryTheory.Equivalence.mkIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → {e f : C ≌ D} → (e.functor ≅ f.functor) → (e ≅ f)
-- Mathlib.Analysis.Asymptotics.TVS
/-- `f =O[𝕜; l] g` (`IsBigOTVS 𝕜 l f g`) is a generalization of `f =O[l] g` (`IsBigO l f g`)
that works in topological `𝕜`-vector spaces.

Given two functions `f` and `g` taking values in topological vector spaces
over a normed field `𝕜`,
we say that $f = O(g)$ if for any neighborhood of zero `U` in the codomain of `f`
there exists a neighborhood of zero `V` in the codomain of `g`
such that $\operatorname{gauge}_{K, U} (f(x)) \le \operatorname{gauge}_{K, V} (g(x))$,
where $\operatorname{gauge}_{K, U}(y) = \inf \{‖c‖ \mid y ∈ c • U\}$.
 -/
Asymptotics.«term_=O[_;_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.Set.Function
Function.Semiconj.mapsTo_image_right : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β} {s : Set α} {t : Set β},
  Function.Semiconj f fa fb → Set.MapsTo f s t → Set.MapsTo f (fa '' s) (fb '' t)
-- Mathlib.Order.Fin.Tuple
strictAnti_vecEmpty : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, StrictAnti ![a]
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.decl : Array Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m.WF → ∀ {l : List α} {k : α}, k ∈ m → (m.insertManyIfNewUnit l).getKey! k = m.getKey! k
-- Batteries.Tactic.PrintPrefix
/-- Options to control `#print prefix` command and `getMatchingConstants`.
 -/
Batteries.Tactic.PrintPrefixConfig : Type
-- Mathlib.Data.ENNReal.Inv
ENNReal.eq_of_forall_nnreal_le_iff : ∀ {x y : ENNReal}, (∀ (r : NNReal), ↑r ≤ x ↔ ↑r ≤ y) → x = y
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.Context.mk.sizeOf_spec : ∀ (cat : Lean.Name) (forceParens : Bool),
  sizeOf { cat := cat, forceParens := forceParens } = 1 + sizeOf cat + sizeOf forceParens
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_compl₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → μ s ≠ ⊤ → μ sᶜ = μ Set.univ - μ s
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.continuousOn_isCompact_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X] {K : Set X},
  IsCompact K → ContinuousOn (⇑(CompactCoherentification.mk X)) K
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.equiv_inr : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) (i₂ : ι₂), ac.equiv (Sum.inr i₂) = e₂.f i₂
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.basisProd.eq_1 : ∀ (R : Type u_1) [inst : Semiring R] (m n : ℕ),
  Polynomial.degreeLT.basisProd R m n =
    ((Polynomial.degreeLT.basis R m).prod (Polynomial.degreeLT.basis R n)).reindex finSumFinEquiv
-- Mathlib.RingTheory.Perfection
Perfection.pthRoot_eq_symm_frobeniusEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p],
  Perfection.pthRoot R p = ↑(frobeniusEquiv (Perfection R p) p).symm
-- Mathlib.Algebra.Polynomial.Degree.Domain
Polynomial.natDegree_pow : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] (p : Polynomial R) (n : ℕ), (p ^ n).natDegree = n * p.natDegree
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfCharZero : ∀ (n : ℕ) (K : Type w) [inst : Field K] [CharZero K], IsCyclotomicExtension {n} K (CyclotomicField n K)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] {k fallback : α} {f : β → β}, (t.modify k f).getKeyD k fallback = if k ∈ t then k else fallback
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.IsInitial.le_ord_iff_card_le : ∀ {o : Ordinal.{u_1}}, o.IsInitial → ∀ (c : Cardinal.{u_1}), o ≤ c.ord ↔ o.card ≤ c
-- Mathlib.Data.Finset.Powerset
Finset.mem_powerset_self : ∀ {α : Type u_1} (s : Finset α), s ∈ s.powerset
-- Lean.Elab.Tactic.RCases
/-- format an `RCasesPatt` with the given precedence: 0 = lo, 1 = med, 2 = hi  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.instToMessageData.fmt : ℕ → Lean.Elab.Tactic.RCases.RCasesPatt → Lean.MessageData
-- Mathlib.Analysis.Seminorm
/-- Closed seminorm-balls are convex.  -/
Seminorm.convex_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul ℝ 𝕜] [NormSMulClass ℝ 𝕜]
  [inst_4 : Module 𝕜 E] [inst_5 : Module ℝ E] [IsScalarTower ℝ 𝕜 E] (p : Seminorm 𝕜 E) (x : E) (r : ℝ),
  Convex ℝ (p.closedBall x r)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The composite of the maps `R → (R/I)` and `(R/I) → (R/I)/J'`  -/
DoubleQuot.quotQuotMk : {R : Type u} → [inst : CommRing R] → (I J : Ideal R) → R →+* (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.le_max?_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k km : α}
  (hc : k ∈ t), t.max?.get ⋯ = km → (cmp k km).isLE = true
-- Mathlib.Algebra.Algebra.Operations
Submodule.instPowNat : {R : Type u} →
  [inst : Semiring R] →
    {A : Type v} → [inst_1 : Semiring A] → [inst_2 : Module R A] → [IsScalarTower R A A] → Pow (Submodule R A) ℕ
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb_ofNat : ∀ (x n hi lo : ℕ), BitVec.extractLsb hi lo (BitVec.ofNat n x) = BitVec.ofNat (hi - lo + 1) ((x % 2 ^ n) >>> lo)
-- Mathlib.MeasureTheory.PiSystem
piiUnionInter_mono_left : ∀ {α : Type u_3} {ι : Type u_4} {π π' : ι → Set (Set α)},
  (∀ (i : ι), π i ⊆ π' i) → ∀ (S : Set ι), piiUnionInter π S ⊆ piiUnionInter π' S
-- Std.Time.Date.Unit.Month
/-- Creates an `Offset` from an integer.
 -/
Std.Time.Month.Offset.ofInt : ℤ → Std.Time.Month.Offset
-- Mathlib.Topology.Order.Basic
instIsCountablyGenerated_atBot : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [TopologicalSpace.SeparableSpace α], Filter.atBot.IsCountablyGenerated