mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single_eq_same : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] [inst_1 : DecidableEq ι] (i : ι) (x : M i),
  Pi.single i x i = x
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypic.isotypicComponent : ∀ (R : Type u_2) (M : Type u) (S : Type u_4) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [IsSimpleModule R S], IsIsotypic R ↥(isotypicComponent R M S)
-- Mathlib.Data.Real.Star
instTrivialStarReal : TrivialStar ℝ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
/-- The cosine of a `Real.Angle`.  -/
Real.Angle.cos : Real.Angle → ℝ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.norm_toLp' : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [inst_5 : OpensMeasurableSpace E]
  [inst_6 : SecondCountableTopologyEither E F] {f : SchwartzMap E F} {p : ENNReal} {μ : MeasureTheory.Measure E},
  p ≠ 0 → p ≠ ⊤ → ∀ [hμ : μ.HasTemperateGrowth], ‖f.toLp p μ‖ = (∫ (x : E), ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.instCompleteLattice : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : CategoryTheory.Functor C MonCat} → CompleteLattice (CategoryTheory.SubmonoidFunctor M)
-- Mathlib.Topology.Connected.PathComponentOne
OpenNormalAddSubgroup.pathComponentZero.eq_1 : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : LocallyPathConnectedSpace G],
  OpenNormalAddSubgroup.pathComponentZero G =
    { toAddSubgroup := AddSubgroup.pathComponentZero G, isOpen' := ⋯, isNormal' := ⋯ }
-- Lean.MetavarContext
/-- A kind for the metavariable that determines its unification behaviour.
For more information see the large comment at the beginning of this file.  -/
Lean.MetavarKind : Type
-- Mathlib.Data.Finset.NAry
Finset.image₂_left_comm : ∀ {α : Type u_1} {β : Type u_3} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} [inst : DecidableEq δ']
  [inst_1 : DecidableEq ε] {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {γ : Type u_14} {u : Finset γ}
  {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε},
  (∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) →
    Finset.image₂ f s (Finset.image₂ g t u) = Finset.image₂ g' t (Finset.image₂ f' s u)
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Returns the smallest element in the heap, or `none` if the heap is empty.  -/
Batteries.BinomialHeap.head? : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le → Option α
-- Init.Data.String.Slice
/-- Creates a new slice that contains the longest prefix of `s` for which `pat` matched
\(potentially repeatedly\).

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".toSlice.takeWhile Char.isLower == "red".toSlice`

* `"red green blue".toSlice.takeWhile 'r' == "r".toSlice`

* `"red red green blue".toSlice.takeWhile "red " == "red red ".toSlice`

* `"red green blue".toSlice.takeWhile (fun (_ : Char) => true) == "red green blue".toSlice`
 -/
String.Slice.takeWhile : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → String.Slice
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
/-- The second marginal of a product probability measure is the second probability measure.  -/
MeasureTheory.ProbabilityMeasure.map_snd_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β), (μ.prod ν).map ⋯ = ν
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t) (j : J),
  CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).inv (s.π.app j) = t.π.app j
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
/-- The closure by isomorphisms of a predicate on objects in a category.  -/
CategoryTheory.ObjectProperty.isoClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.Finite.toFinset_one : ∀ {α : Type u_2} [inst : One α] (h : optParam (Set.Finite 1) ⋯), h.toFinset = 1
-- Mathlib.Order.Defs.Unbundled
/-- The carrier of a `RelUpperSet`.  -/
RelUpperSet.carrier : {α : Type u_1} → [inst : LE α] → {P : α → Prop} → RelUpperSet P → Set α
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIic_coe : ∀ {α : Type u_1} [inst : LinearOrder α] {b : α} (x : ↑(Set.Iic b)), Set.projIic b ↑x = x
-- Mathlib.Topology.Spectral.Basic
Topology.IsOpenEmbedding.spectralSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [SpectralSpace Y]
  [CompactSpace X], Topology.IsOpenEmbedding f → SpectralSpace X
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- `Pi.single` as a bundled continuous linear map.  -/
ContinuousLinearMap.single : (R : Type u_1) →
  [inst : Semiring R] →
    {ι : Type u_4} →
      (φ : ι → Type u_5) →
        [inst_1 : (i : ι) → TopologicalSpace (φ i)] →
          [inst_2 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_3 : (i : ι) → Module R (φ i)] → [DecidableEq ι] → (i : ι) → φ i →L[R] (i : ι) → φ i
-- Mathlib.Order.Monotone.Basic
StrictAntiOn.eq_iff_eq : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → (f a = f b ↔ b = a)
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseActions : Std.Internal.Parsec.ByteArray.Parser (Array Std.Tactic.BVDecide.LRAT.IntAction)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.fract_eq_self_of_mem_fundamentalDomain : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] {x : ι → ℕ},
  x ∈ IsProperLinearSet.fundamentalDomain✝ hs → IsProperLinearSet.fract✝ hs x = x
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- `p` splits in the splitting field of `p ∘ q`, for `q` non-constant.  -/
Polynomial.Gal.splits_in_splittingField_of_comp : ∀ {F : Type u_1} [inst : Field F] (p q : Polynomial F),
  q.natDegree ≠ 0 → (Polynomial.map (algebraMap F (p.comp q).SplittingField) p).Splits
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂)[k]! = default
-- Mathlib.Computability.Partrec
Nat.Partrec.comp : ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → Nat.Partrec fun n => g n >>= f
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.mk_coe : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (inj : Function.Injective ⇑f), { toFun := ⇑f, inj' := inj } = f
-- Mathlib.Logic.Embedding.Basic
/-- `Quotient.out` as an embedding.  -/
Function.Embedding.quotientOut : (α : Sort u_1) → [s : Setoid α] → Quotient s ↪ α
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm.congr_simp : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : ∀ (x : B), Nonempty (E x)] (e e_1 : Bundle.Pretrivialization F Bundle.TotalSpace.proj),
  e = e_1 → ∀ (b : B) (y y_1 : F), y = y_1 → e.symm b y = e_1.symm b y_1
-- Mathlib.Data.FinEnum
List.Pi.mem_enum : ∀ {α : Type u_1} [inst : FinEnum α] {β : α → Type u_2} [inst_1 : (a : α) → FinEnum (β a)] (f : (a : α) → β a),
  f ∈ List.Pi.enum β
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_lt_one : ∀ {c : Cardinal.{u}}, Cardinal.toENat c < 1 ↔ c < 1
-- Mathlib.Analysis.Complex.Conformal
LinearMap.coe_complexOfReal : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {ℓ : ℂ →ₗ[ℝ] E}
  (h : ℓ Complex.I = Complex.I • ℓ 1), ⇑(ℓ.complexOfReal h) = ⇑ℓ
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.range_kerCotangentToTensor : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B],
  Function.Surjective ⇑(algebraMap A B) →
    (KaehlerDifferential.kerCotangentToTensor R A B).range =
      Submodule.restrictScalars A (KaehlerDifferential.mapBaseChange R A B).ker
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.coe_toNatAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S), ⇑f.toNatAlgEquiv = ⇑f
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RicSliceData.treeMap : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RicSliceData α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The canonical isomorphism `K.cycles 0 ≅ K.X 0` for a chain complex `K`
indexed by `ℕ`.  -/
ChainComplex.cycles₀Iso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (K : ChainComplex C ℕ) → [inst_2 : HomologicalComplex.HasHomology K 0] → HomologicalComplex.cycles K 0 ≅ K.X 0
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.interedges_mono : ∀ {α : Type u_4} {β : Type u_5} {r : α → β → Prop} [inst : (a : α) → DecidablePred (r a)] {s₁ s₂ : Finset α}
  {t₁ t₂ : Finset β}, s₂ ⊆ s₁ → t₂ ⊆ t₁ → Rel.interedges r s₂ t₂ ⊆ Rel.interedges r s₁ t₁
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.areaForm x) y ≤ ‖x‖ * ‖y‖
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.IsParabolic.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (m : Matrix (Fin 2) (Fin 2) R),
  m.IsParabolic = (m ∉ Set.range ⇑(Matrix.scalar (Fin 2)) ∧ m.discr = 0)
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNormClass.toMulRingNormClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {inst : SeminormedCommRing R} {S : outParam (Type u_3)} {inst_1 : Ring S}
  {inst_2 : Algebra R S} {inst_3 : FunLike F S ℝ} [self : MulAlgebraNormClass F R S], MulRingNormClass F S ℝ
-- Lean.DocString.Types
Lean.Doc.Block.code.inj : ∀ {i : Type u} {b : Type v} {content content_1 : String},
  Lean.Doc.Block.code content = Lean.Doc.Block.code content_1 → content = content_1
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.comp_tsnd : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] {F G : Type u → Type u} [inst_1 : Applicative F]
  [inst_2 : Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α β₀ β₁ β₂ : Type u}
  (g : β₀ → F β₁) (g' : β₁ → G β₂) (x : t α β₀),
  Functor.Comp.mk (Bitraversable.tsnd g' <$> Bitraversable.tsnd g x) =
    Bitraversable.tsnd (Functor.Comp.mk ∘ Functor.map g' ∘ g) x
-- Init.Data.Iterators.Lemmas.Combinators.ULift
Std.Iter.toArray_uLift : ∀ {α β : Type u} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id],
  it.uLift.toArray = Array.map ULift.up it.toArray
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- A square is a pullback square if its flip is.  -/
CategoryTheory.Limits.PullbackCone.isLimitOfFlip : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {t : CategoryTheory.Limits.PullbackCone f g} →
            CategoryTheory.Limits.IsLimit t.flip → CategoryTheory.Limits.IsLimit t
-- Mathlib.CategoryTheory.Limits.Sifted
CategoryTheory.IsSifted.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [toFinal : (CategoryTheory.Functor.diag C).Final]
  [nonempty : Nonempty C], CategoryTheory.IsSifted C
-- Lean.MetavarContext
/-- Modify the declaration of a metavariable. If the metavariable is not declared,
the `MetavarContext` is returned unchanged.

You must ensure that the modification is legal. In particular, expressions may
only be replaced with defeq expressions.
 -/
Lean.MetavarContext.modifyExprMVarDecl : Lean.MetavarContext → Lean.MVarId → (Lean.MetavarDecl → Lean.MetavarDecl) → Lean.MetavarContext
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableAt.smul_const_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {a : 𝕜}
  {s : (x : B) → E x} {x₀ : B}, MDiffAt (T% s) x₀ → (MDiffAt fun x => ⟨x, (a • s) x⟩) x₀
-- Mathlib.Topology.Order.SuccPred
PredOrder.isOpen_singleton_of_not_isPredPrelimit : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] {a : α} [PredOrder α],
  ¬Order.IsPredPrelimit a → IsOpen {a}
-- Lean.Data.Options
Lean.Option.registerOption : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_succ_of_lt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) {n : ℕ} (i j : Fin (n + 1)),
  j ≤ i →
    CategoryTheory.CategoryStruct.comp (self.h j) (Y.σ i.succ) =
      CategoryTheory.CategoryStruct.comp (X.σ i) (self.h j.castSucc)
-- Mathlib.Data.Fintype.Defs
Finset.nodup_map_iff_injOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Finset α}, (Multiset.map f s.val).Nodup ↔ Set.InjOn f ↑s
-- Lean.Meta.Match.Basic
Lean.Meta.Match.examplesToMessageData : List Lean.Meta.Match.Example → Lean.MessageData
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Equivalence.right_triangle : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} (e : CategoryTheory.Bicategory.Equivalence a b),
  CategoryTheory.Bicategory.rightZigzagIso e.unit e.counit =
    CategoryTheory.Bicategory.rightUnitor e.inv ≪≫ (CategoryTheory.Bicategory.leftUnitor e.inv).symm
-- Mathlib.CategoryTheory.Sites.Canonical
/-- `yoneda.obj X` is a sheaf for the canonical topology.  -/
CategoryTheory.Sheaf.isSheaf_yoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.canonicalTopology C) (CategoryTheory.yoneda.obj X)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- If the measurable space generated by `S` separates points,
then this is witnessed by sets in `S`.  -/
MeasurableSpace.separating_of_generateFrom : ∀ {α : Type u_1} (S : Set (Set α)) [h : MeasurableSpace.SeparatesPoints α] (x y : α), (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.coe_mapAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_5} [inst_1 : AddGroup H] (e : G ≃+ H),
  ⇑e.mapAddSubgroup = AddSubgroup.map e.toAddMonoidHom
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv.congr_simp : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T), hST.equiv = hST.equiv
-- Aesop.Stats.File
Aesop.StatsFileRecord.mk.inj : ∀ {toStats : Aesop.Stats} {«syntax» file : String} {position : Option Lean.Position} {declaration : Option Lean.Name}
  {goalSolved : Bool} {toStats_1 : Aesop.Stats} {syntax_1 file_1 : String} {position_1 : Option Lean.Position}
  {declaration_1 : Option Lean.Name} {goalSolved_1 : Bool},
  { toStats := toStats, «syntax» := «syntax», file := file, position := position, declaration := declaration,
        goalSolved := goalSolved } =
      { toStats := toStats_1, «syntax» := syntax_1, file := file_1, position := position_1,
        declaration := declaration_1, goalSolved := goalSolved_1 } →
    toStats = toStats_1 ∧
      «syntax» = syntax_1 ∧
        file = file_1 ∧ position = position_1 ∧ declaration = declaration_1 ∧ goalSolved = goalSolved_1
-- Mathlib.GroupTheory.Solvable
IsSimpleGroup.comm_iff_isSolvable : ∀ {G : Type u_1} [inst : Group G] [IsSimpleGroup G], (∀ (a b : G), a * b = b * a) ↔ Group.IsSolvable G
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.mem_ordConnectedComponent_ordConnectedProj : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α) (x : ↑s), ↑x ∈ s.ordConnectedComponent (s.ordConnectedProj x)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get? k = none
-- Mathlib.Logic.Relation
Relation.reflTransGen_iff_eq : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, (∀ (b : α), ¬r a b) → (Relation.ReflTransGen r a b ↔ b = a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The class of the element `X - x` in `R[W]` for some `x` in `R`.  -/
WeierstrassCurve.Affine.CoordinateRing.XClass : {R : Type r} → [inst : CommRing R] → (W' : WeierstrassCurve.Affine R) → R → W'.CoordinateRing
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableAdd.measurable_add_const : ∀ {M : Type u_2} {inst : MeasurableSpace M} {inst_1 : Add M} [self : MeasurableAdd M] (c : M), Measurable fun x => x + c
-- Mathlib.Computability.Halting
/-- The Halting problem is recursively enumerable  -/
ComputablePred.halting_problem_re : ∀ (n : ℕ), REPred fun c => (c.eval n).Dom
-- Init.Data.Array.Extract
Array.extract_append : ∀ {α : Type u_1} {as bs : Array α} {i j : ℕ},
  (as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size)
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.toList.eq_1 : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} (m : Std.HashMap α β),
  m.toList = Std.DHashMap.Const.toList m.inner
-- Init.Data.UInt.Lemmas
UInt16.zero_ne_one : 0 ≠ 1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_leadingTerm : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.withBotDegree (m.leadingTerm f) = m.withBotDegree f
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- `I ⊔ J` is the least box that includes both `I` and `J`. Since `↑I ∪ ↑J` is usually not a box,
`↑(I ⊔ J)` is larger than `↑I ∪ ↑J`.  -/
BoxIntegral.Box.instSemilatticeSup : {ι : Type u_1} → SemilatticeSup (BoxIntegral.Box ι)
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- The same-universe version of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`.  -/
Field.sepDegree_mul_sepDegree_of_isAlgebraic : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E],
  Field.sepDegree F E * Field.sepDegree E K = Field.sepDegree F K
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.PreservesLeftKanExtension.mk : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {G : CategoryTheory.Functor B D} {F : CategoryTheory.Functor A B}
  {L : CategoryTheory.Functor A C},
  (∀ (F' : CategoryTheory.Functor C B) (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α],
      (F'.comp G).IsLeftKanExtension
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α G) (L.associator F' G).hom)) →
    G.PreservesLeftKanExtension F L
-- Lean.Namespace
/-- Returns an iterator over all namespaces in `env`.  -/
Lean.Environment.getNamespaces : Lean.Environment → Std.Iter Lean.Name
-- Mathlib.Topology.Bornology.Basic
Set.Finite.isBounded : ∀ {α : Type u_2} [inst : Bornology α] {s : Set α}, s.Finite → Bornology.IsBounded s
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.irrelevant_le : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] {P : HomogeneousIdeal 𝒜},
  HomogeneousIdeal.irrelevant 𝒜 ≤ P ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P.toAddSubmonoid
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.mk.sizeOf_spec : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] [inst_4 : SizeOf ι] [inst_5 : SizeOf k] [inst_6 : SizeOf V]
  [inst_7 : SizeOf P] (toFun : ι → P) (ind' : AffineIndependent k toFun) (tot' : affineSpan k (Set.range toFun) = ⊤),
  sizeOf { toFun := toFun, ind' := ind', tot' := tot' } = 1 + sizeOf tot'
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.instInhabitedSimpCongrTheorem.default : Lean.Meta.SimpCongrTheorem
-- Mathlib.RingTheory.Algebraic.Defs
Algebra.transcendental_iff_not_isAlgebraic : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  Algebra.Transcendental R A ↔ ¬Algebra.IsAlgebraic R A
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.coe_mul : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A B : SpecialLinearGroup R V), ↑(A * B) = ↑A * ↑B
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k fallback : α},
      m.contains k = true →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Topology.Clopen
IsClopen.diff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClopen s → IsClopen t → IsClopen (s \ t)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.zero_ne_of : ∀ {α : Type u} (x : α), 0 ≠ FreeAbelianGroup.of x
-- Lean.SubExpr
/-- monad-fold over the position starting at the root and heading to the leaf  -/
Lean.SubExpr.Pos.foldlM : {α : Type} → [Inhabited α] → {M : Type → Type u_1} → [Monad M] → (α → ℕ → M α) → α → Lean.SubExpr.Pos → M α
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instOrderTop : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [inst_1 : LE β] → [OrderTop β] → OrderTop (MeasureTheory.SimpleFunc α β)
-- Mathlib.Order.SupClosed
isSublattice_pi : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → Lattice (α i)] {s : Set ι} {t : (i : ι) → Set (α i)},
  (∀ i ∈ s, IsSublattice (t i)) → IsSublattice (s.pi t)