mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β}
  (f : (a : α) → β a → γ a), m₁.Equiv m₂ → (Std.DHashMap.map f m₁).Equiv (Std.DHashMap.map f m₂)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.insertVars : Lean.Elab.Term.Do.VarSet → Array Lean.Elab.Term.Do.Var → Lean.Elab.Term.Do.VarSet
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Functor.map_conj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (α : X ≅ Y) (f : CategoryTheory.End X),
  F.map (α.conj f) = (F.mapIso α).conj (F.map f)
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.isLocalization_atPrime_localization_atPrime : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (p : Ideal (Localization M)) [inst_1 : p.IsPrime],
  IsLocalization.AtPrime (Localization.AtPrime p) (Ideal.comap (algebraMap R (Localization M)) p)
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piRightInv.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] {ι : Type u_4}
  (M : ι → Type u_5) [inst_7 : (i : ι) → AddCommMonoid (M i)] [inst_8 : (i : ι) → Module R (M i)] [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι],
  TensorProduct.piRightInv R S N M =
    (LinearMap.lsum S (fun i => TensorProduct R N (M i)) S) fun i =>
      TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.single R M i)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ₀Iter_succ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (h : autoParam (n + i = m) CategoryTheory.SimplicialObject.δ₀Iter_succ._auto_1) {Z : C}
  (h_1 : X.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ₀Iter (i + 1) ⋯) h_1 =
    CategoryTheory.CategoryStruct.comp (X.δ 0) (CategoryTheory.CategoryStruct.comp (X.δ₀Iter i h) h_1)
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.inseparableSetoid_ring : ∀ (α : Type u_2) [inst : Ring α] [inst_1 : TopologicalSpace α] [inst_2 : IsTopologicalRing α],
  inseparableSetoid α = Submodule.quotientRel ⊥.closure
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_pos_of_mem_Ioo : ∀ {x : ℝ}, x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) → 0 < Real.cos x
-- Mathlib.RingTheory.WittVector.MulCoeff
/-- ```
(∑ i ∈ range n, (y.coeff i)^(p^(n-i)) * p^i.val) *
(∑ i ∈ range n, (y.coeff i)^(p^(n-i)) * p^i.val)
```
 -/
WittVector.wittPolyProd : ℕ → ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_conjugation_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') {Z_1 : C}
  (h_1 :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Y') Z' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h) h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' Y' Z').inv h_1))
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.toFun_eq_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  ↑e.toPartialEquiv = ↑e
-- Init.Data.Option.Array
Option.toArray_eq_empty_iff : ∀ {α : Type u_1} {o : Option α}, o.toArray = #[] ↔ o = none
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoalCore.mk : Array Lean.Widget.InteractiveHypothesisBundle →
  Lean.Widget.CodeWithInfos → Lean.Server.WithRpcRef Lean.Elab.ContextInfo → Lean.Widget.InteractiveGoalCore
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.WF.eraseManyEntries : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ ((a : α) × β a)]
  {m : Std.DHashMap.Raw α β} {l : ρ}, m.WF → (m.eraseManyEntries l).WF
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.functorPullback_monotone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C}, Monotone (CategoryTheory.Presieve.functorPullback F)
-- Mathlib.Algebra.Module.ULift
ULift.isScalarTower'' : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : SMul R M] [inst_1 : SMul M N] [inst_2 : SMul R N]
  [IsScalarTower R M N], IsScalarTower R M (ULift.{u_1, w} N)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.initial_fromPUnit_of_isInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {c : C} (hc : CategoryTheory.Limits.IsInitial c),
  (CategoryTheory.Functor.fromPUnit c).Initial
-- Lean.ResolveName
/-- Add alias `a` for `e`  -/
Lean.addAlias : Lean.Environment → Lean.Name → Lean.Name → Lean.Environment
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Composition of continuous linear maps.  -/
ContinuousLinearMap.comp : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    {R₃ : Type u_3} →
      [inst : Semiring R₁] →
        [inst_1 : Semiring R₂] →
          [inst_2 : Semiring R₃] →
            {σ₁₂ : R₁ →+* R₂} →
              {σ₂₃ : R₂ →+* R₃} →
                {σ₁₃ : R₁ →+* R₃} →
                  {M₁ : Type u_4} →
                    [inst_3 : TopologicalSpace M₁] →
                      [inst_4 : AddCommMonoid M₁] →
                        {M₂ : Type u_6} →
                          [inst_5 : TopologicalSpace M₂] →
                            [inst_6 : AddCommMonoid M₂] →
                              {M₃ : Type u_7} →
                                [inst_7 : TopologicalSpace M₃] →
                                  [inst_8 : AddCommMonoid M₃] →
                                    [inst_9 : Module R₁ M₁] →
                                      [inst_10 : Module R₂ M₂] →
                                        [inst_11 : Module R₃ M₃] →
                                          [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                            (M₂ →SL[σ₂₃] M₃) → (M₁ →SL[σ₁₂] M₂) → M₁ →SL[σ₁₃] M₃
-- Init.Data.List.Find
List.Sublist.lookup_eq_none : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)},
  l₁.Sublist l₂ → List.lookup k l₂ = none → List.lookup k l₁ = none
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
/-- The inclusion of a submonoid functor `S` to the original functor of monoids `M`.  -/
CategoryTheory.SubmonoidFunctor.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : CategoryTheory.Functor C MonCat} → (S : CategoryTheory.SubmonoidFunctor M) → S.toFunctor ⟶ M
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.mk.sizeOf_spec : ∀ {G : Type u_6} [inst : AddGroup G] [inst_1 : SizeOf G] (toFun : G → ℝ) (map_zero' : toFun 0 = 0)
  (add_le' : ∀ (r s : G), toFun (r + s) ≤ toFun r + toFun s) (neg' : ∀ (r : G), toFun (-r) = toFun r),
  sizeOf { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' } = 1 + sizeOf map_zero'
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instAddCommMonoid : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → AddCommMonoid (QuadraticMap R M N)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The universal property of the graded tensor product; every algebra morphism uniquely factors
as a pair of algebra morphisms that anticommute with respect to the grading.  -/
GradedTensorProduct.liftEquiv : {R : Type u_1} →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              [inst_9 : Module ι (Additive ℤˣ)] →
                                {C : Type u_5} →
                                  [inst_10 : Ring C] →
                                    [inst_11 : Algebra R C] →
                                      { fg //
                                          ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                                            fg.1 ↑a * fg.2 ↑b = (-1) ^ (j * i) • (fg.2 ↑b * fg.1 ↑a) } ≃
                                        (GradedTensorProduct R 𝒜 ℬ →ₐ[R] C)
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Multiset.prod_map_le_pow_card : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
  {F : Type u_2} {L : Type u_3} [inst_4 : FunLike F L R] {f : F} {r : R} {t : Multiset L},
  (∀ x ∈ t, 0 ≤ f x) → (∀ x ∈ t, f x ≤ r) → (Multiset.map (⇑f) t).prod ≤ r ^ t.card
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isNone_maxKey?_eq_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey?.isNone = t.isEmpty
-- Mathlib.Algebra.Group.TypeTags.Basic
ofAdd_nsmul : ∀ {α : Type u} [inst : AddMonoid α] (n : ℕ) (a : α), Multiplicative.ofAdd (n • a) = Multiplicative.ofAdd a ^ n
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the signs of two nondegenerate oriented angles between points are equal, the oriented
angles are equal if and only if the unoriented angles are equal.  -/
EuclideanGeometry.angle_eq_iff_oangle_eq_of_sign_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  p₁ ≠ p₂ →
    p₃ ≠ p₂ →
      p₄ ≠ p₅ →
        p₆ ≠ p₅ →
          (EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₄ p₅ p₆).sign →
            (EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆ ↔
              EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₄ p₅ p₆)
-- Mathlib.Topology.Connected.LocallyConnected
/-- A topological space is **locally connected** if each neighborhood filter admits a basis
of connected *open* sets. Note that it is equivalent to each point having a basis of connected
(not necessarily open) sets but in a non-trivial way, so we choose this definition and prove the
equivalence later in `locallyConnectedSpace_iff_connected_basis`.  -/
LocallyConnectedSpace : (α : Type u_3) → [TopologicalSpace α] → Prop
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- A variant of `measure_eq_iInf` which has a single `iInf`. This is useful when applying a
lemma next that only works for non-empty infima, in which case you can use
`nonempty_measurable_superset`.  -/
MeasureTheory.measure_eq_iInf' : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α), μ s = ⨅ t, μ ↑t
-- Mathlib.Order.Filter.Finite
Finset.eventuallyLE_iUnion : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f g : ι → Set α},
  (∀ i ∈ s, f i ≤ᶠ[l] g i) → ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} ⦃X₁ X₂ : C⦄
  ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄
  (φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂) ⦃Y' : C⦄ (g : Y' ⟶ Y)
  (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁)
  (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂),
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ g gf₁ gf₂ hgf₁ hgf₂ =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app M₁)
      (CategoryTheory.CategoryStruct.comp ((F.map g.op.toLoc).toFunctor.map φ)
        ((F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app M₂))
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.singleAddHom.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] (a : G),
  SkewMonoidAlgebra.singleAddHom a = { toFun := SkewMonoidAlgebra.single a, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Order.Floor.Semifield
Nat.ceil_le_mul : ∀ {K : Type u_2} [inst : Field K] [inst_1 : LinearOrder K] [IsOrderedRing K] [inst_3 : FloorSemiring K] {a b : K},
  1 < b → ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a → ↑⌈a⌉₊ ≤ b * a
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
AlternatingMap.alternatizeUncurryFin.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N),
  AlternatingMap.alternatizeUncurryFin f =
    { toMultilinearMap := ∑ p, (-1) ^ ↑p • LinearMap.uncurryMid p (AlternatingMap.toMultilinearMapLM ∘ₗ f),
      map_eq_zero_of_eq' := ⋯ }
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.size_eq_length_iter : ∀ {γ : Type u} {α β : Type v} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  {s : Std.Slice γ} [Std.Iterators.Finite α Id] [inst_3 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id]
  [inst_5 : Std.Slice.SliceSize γ] [Std.Slice.LawfulSliceSize γ], s.size = s.iter.length
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Fintype.prod_ite_zero : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoidWithZero M₀] {p : ι → Prop}
  [inst_2 : DecidablePred p] {f : ι → M₀}, (∏ i, if p i then f i else 0) = if ∀ (i : ι), p i then ∏ i, f i else 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Given an isomorphism `e : L ⋙ G ≅ L'`, a left extension of `F` along `L'` is universal
iff the corresponding left extension of `L` along `L` is.  -/
CategoryTheory.Functor.LeftExtension.isUniversalPostcomp₁Equiv : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {L : CategoryTheory.Functor C D} →
                  {L' : CategoryTheory.Functor C D'} →
                    (G : CategoryTheory.Functor D D') →
                      [G.IsEquivalence] →
                        (e : L.comp G ≅ L') →
                          (F : CategoryTheory.Functor C H) →
                            (ex : L'.LeftExtension F) →
                              CategoryTheory.StructuredArrow.IsUniversal ex ≃
                                CategoryTheory.StructuredArrow.IsUniversal
                                  ((CategoryTheory.Functor.LeftExtension.postcomp₁ G e.inv F).obj ex)
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffWithinAt_Ioi : ∀ (a : ℝ), UniqueDiffWithinAt ℝ (Set.Ioi a) a
-- Init.Data.String.Lemmas.Splits
String.copy_slice_next : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, (s.slice p (p.next h) ⋯).copy = String.singleton (p.get h)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsCycles.toSimpleGraph : ∀ {V : Type u_1} {G : SimpleGraph V} (c : G.ConnectedComponent), G.IsCycles → c.toSimpleGraph.spanningCoe.IsCycles
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqRhs.sizeOf_spec : ∀ (gen : Bool), sizeOf (Lean.Meta.Grind.EMatchTheoremKind.eqRhs gen) = 1 + sizeOf gen
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_sep : ∀ {p : PSet.{u_1} → Prop},
  (∀ (x y : PSet.{u_1}), x.Equiv y → p x → p y) → ∀ {x y : PSet.{u_1}}, y ∈ PSet.sep p x ↔ y ∈ x ∧ p y
-- Lean.Server.Rpc.Basic
Lean.Server.RpcEncodable.rpcDecode : {α : Type} → [self : Lean.Server.RpcEncodable α] → Lean.Json → ExceptT String (ReaderT Lean.Server.RpcObjectStore Id) α
-- Init.Data.Option.Lemmas
Option.bind_guard : ∀ {α : Type u_1} (x : Option α) (p : α → Bool), x.bind (Option.guard p) = Option.filter p x
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.coe_copy : ∀ {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (entry' : ℕ → ℕ → ℕ) (h : entry' = ⇑T),
  ⇑(T.copy entry' h) = entry'
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubgroup.coe_even : ∀ {G : Type u_1} [inst : AddCommGroup G], ↑(AddSubgroup.even G) = {s | Even s}
-- Lean.Meta.ForEachExpr
/-- Given an expression `e =  (x₁ : α₁) → .. (xₙ : αₙ) → b`, runs `f` on each `αᵢ` and `b`.  -/
Lean.Meta.visitForall : {m : Type → Type u_1} → [Monad m] → [MonadControlT Lean.MetaM m] → (Lean.Expr → m Unit) → Lean.Expr → m Unit
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.toList_nil : ∀ {α : Type u} {β : α → Type v}, Std.DHashMap.Internal.AssocList.nil.toList = []
-- Lean.Meta.LetToHave
/-- Cached results for `visit`.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.State.results : Lean.Meta.LetToHave.State✝ → Std.HashMap Lean.ExprStructEq Lean.Meta.LetToHave.Result✝
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (r₁ r₂ : ℤ) (x : M) {l₁ l₂ l : Mathlib.Tactic.FieldSimp.NF M},
  l₁.eval / l₂.eval = l.eval → ((r₁, x) ::ᵣ l₁).eval / ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval
-- Mathlib.Topology.Sets.Compacts
/-- Reinterpret a positive compact as a nonempty compact.  -/
TopologicalSpace.PositiveCompacts.toNonemptyCompacts : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.PositiveCompacts α → TopologicalSpace.NonemptyCompacts α
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.d_comp_XIsoOfEq_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι}
  (h : p₂ = p₃) (p₁ : ι), CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (K.XIsoOfEq h).hom = K.d p₁ p₃
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.algHomUnitsEquiv_apply_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (f : (S →ₐ[R] S)ˣ)
  (a : S), ((AlgEquiv.algHomUnitsEquiv R S) f) a = (↑↑(↑f).toRingHom).toFun a
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.IsEquivalence],
  CategoryTheory.IsIso h.counit
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.imageSieve_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {FA : A → A → Type u_1} {CA : A → Type w'} [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_3 : CategoryTheory.ConcreteCategory A FA] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C}
  (s : CategoryTheory.ToType (G.obj (Opposite.op U))) (V : C) (i : V ⟶ U),
  (CategoryTheory.Presheaf.imageSieve f s).arrows i =
    ∃ t,
      (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op V))) t =
        (CategoryTheory.ConcreteCategory.hom (G.map i.op)) s
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
instSeparatingDualRealOfIsTopologicalAddGroupOfContinuousSMulOfLocallyConvexSpaceOfT1Space : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [IsTopologicalAddGroup E] [inst_3 : Module ℝ E]
  [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T1Space E], SeparatingDual ℝ E
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- `eval` is an additive homomorphism except when a denominator evaluates to `0`.

Counterexample: `eval _ 1 (X / (X-1)) + eval _ 1 (-1 / (X-1)) = 0`
`... ≠ 1 = eval _ 1 ((X-1) / (X-1))`.

See also `RatFunc.eval₂_denom_ne_zero` to make the hypotheses simpler but less general.
 -/
RatFunc.eval_add : ∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] (f : K →+* L) (a : L) {x y : RatFunc K},
  Polynomial.eval₂ f a x.denom ≠ 0 →
    Polynomial.eval₂ f a y.denom ≠ 0 → RatFunc.eval f a (x + y) = RatFunc.eval f a x + RatFunc.eval f a y
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))),
  x = Std.DTreeMap.Internal.Impl.leaf →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
      | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
        h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) ≍
      h_1 ()
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.map_comp_smul_assoc : ∀ {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U V : X.Opens} (i : U ⟶ V) (r : ↑(X.presheaf.obj (Opposite.op V)))
  {Z : Ab} (h : M.presheaf.obj (Opposite.op U) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r)
      (CategoryTheory.CategoryStruct.comp (M.presheaf.map i.op) h) =
    CategoryTheory.CategoryStruct.comp (M.presheaf.map i.op)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Modules.smul ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) r)) h)
-- Mathlib.Topology.Defs.Filter
/-- If `f` is a filter in `α` and `g : α → X` is a function, then `Filter.limUnder f g` is a limit
of `g` at `f`, if it exists.  -/
Filter.limUnder : {X : Type u_1} → [TopologicalSpace X] → {α : Type u_3} → [Nonempty X] → Filter α → (α → X) → X
-- Init.Control.Basic
/-- Left-to-right composition of Kleisli arrows. 

Conventions for notations in identifiers:

 * The recommended spelling of `>=>` in identifiers is `kleisliRight`. -/
Bind.kleisliRight : {α : Type u} → {m : Type u_1 → Type u_2} → {β γ : Type u_1} → [Bind m] → (α → m β) → (β → m γ) → α → m γ
-- Mathlib.ModelTheory.Ultraproducts
FirstOrder.Language.Ultraproduct.setoidPrestructure : {α : Type u_1} →
  (M : α → Type u_2) →
    (u : Ultrafilter α) →
      {L : FirstOrder.Language} → [(a : α) → L.Structure (M a)] → L.Prestructure ((↑u).productSetoid M)
-- Mathlib.Data.Multiset.UnionInter
Multiset.inter_add_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Multiset α), s ∩ t + u = (s + u) ∩ (t + u)