mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.IsBounded
Monotone.isBoundedUnder_ge_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [inst : LinearOrder β] [inst_1 : Preorder γ] [NoMinOrder γ]
  {g : β → γ} {f : α → β} {l : Filter α},
  Monotone g →
    Filter.Tendsto g Filter.atBot Filter.atBot →
      (Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l f)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A product of meromorphic functions in normal form is in normal form if at most one of the factors
vanishes.
 -/
meromorphicNFOn_fun_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜},
  (∀ i ∈ s, MeromorphicNFOn (f i) U) →
    (∀ x ∈ U, {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton) → MeromorphicNFOn (fun x => ∏ i ∈ s, f i x) U
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.getKey? k (Std.Internal.List.insertList l toInsert) =
        (Std.Internal.List.getKey? k toInsert).or (Std.Internal.List.getKey? k l)
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- An arbitrarily chosen final functor `FinalModel J ⥤ J`.  -/
CategoryTheory.fromFinalModel : (J : Type u) →
  [inst : CategoryTheory.Category.{v, u} J] →
    [inst_1 : CategoryTheory.FinallySmall J] → CategoryTheory.Functor (CategoryTheory.FinalModel J) J
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- A pretransitivity criterion.  -/
SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α},
  MulAction.IsPretransitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s) →
    ∀ {g : M},
      s ∪ g • s ≠ ⊤ →
        MulAction.IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup M (s ∩ g • s))
-- Mathlib.Topology.Category.Profinite.Nobeling.Induction
/-- **Nöbeling's theorem**. The `ℤ`-module `LocallyConstant S ℤ` is free for every
`S : Profinite`.  -/
LocallyConstant.freeOfProfinite : ∀ (S : Profinite), Module.Free ℤ (LocallyConstant ↑S.toTop ℤ)
-- Mathlib.RepresentationTheory.Invariants
Rep.instPreservesZeroMorphismsModuleCatInvariantsFunctor : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G], (Rep.invariantsFunctor k G).PreservesZeroMorphisms
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If a function `f` tends to negative infinity along a filter,
then `f` multiplied by a negative constant (on the left) tends to positive infinity.  -/
Filter.Tendsto.const_mul_atBot_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => r * f x) l Filter.atTop
-- Batteries.Data.List.Lemmas
List.set_eq_take_cons_drop : ∀ {α : Type u_1} (a : α) {n : ℕ} {l : List α}, n < l.length → l.set n a = List.take n l ++ a :: List.drop (n + 1) l
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
CategoryTheory.instSmallCategoryI : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} → (P : CategoryTheory.IndParallelPairPresentation f g) → CategoryTheory.SmallCategory P.I
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.map_apply : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} {E : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : CommRing R]
  [inst_6 : TopologicalSpace R] [inst_7 : IsTopologicalRing R] [inst_8 : Module R E] [inst_9 : ContinuousSMul R E]
  (f : C(X, Y)) (μ : AbstractMeasure X R E) (g : C(Y, R)), ((AbstractMeasure.map f) μ) g = μ (g.comp f)
-- Lean.Meta.Tactic.Simp.Arith.Int.Simp
Lean.Meta.Simp.Arith.Int.simpDvd? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Init.Data.SInt.Bitwise
instIdempotentOpInt8HAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.opLaxMonoidalPi'_η : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : (i : I) → CategoryTheory.Functor D (C i)) [inst_4 : (i : I) → (F i).OplaxMonoidal] (i : I),
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Functor.pi' F) i = CategoryTheory.Functor.OplaxMonoidal.η (F i)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.compQuadraticMap'.congr_simp : ∀ {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : CommSemiring S] [inst_7 : Algebra S R] [inst_8 : Module S N]
  [inst_9 : Module S M] [inst_10 : IsScalarTower S R N] [inst_11 : IsScalarTower S R M] [inst_12 : Module S P]
  (f f_1 : N →ₗ[S] P),
  f = f_1 → ∀ (Q Q_1 : QuadraticMap R M N), Q = Q_1 → f.compQuadraticMap' Q = f_1.compQuadraticMap' Q_1
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.instInhabitedSymM : {α : Type} → Inhabited (Lean.Meta.Sym.SymM α)
-- Mathlib.SetTheory.Cardinal.Free
instCountableFreeCommRing : ∀ (α : Type u) [Countable α], Countable (FreeCommRing α)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndep.eq_1 : ∀ {Ω : Type u_1} (m' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ =
    ProbabilityTheory.Kernel.Indep m₁ m₂ (ProbabilityTheory.condExpKernel μ m') (μ.trim hm')
-- Mathlib.Topology.UniformSpace.Separation
t0Space_iff_ker_uniformity : ∀ {α : Type u} [inst : UniformSpace α], T0Space α ↔ (uniformity α).ker = Set.diagonal α
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.tensorUnit_snd_β : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (U : C),
  CategoryTheory.Center.tensorUnit.snd.β U =
    CategoryTheory.MonoidalCategoryStruct.leftUnitor U ≪≫ (CategoryTheory.MonoidalCategoryStruct.rightUnitor U).symm
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given three points in strict order on the same line, and a fourth point, the angles at the
fourth point between the first and second or second and third points have the same sign.  -/
Sbtw.oangle_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),
  Sbtw ℝ p₁ p₂ p₃ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₂ p₄ p₃).sign
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] {g : BoundedLatticeHom β γ}
  {f₁ f₂ : BoundedLatticeHom α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.bvar.sizeOf_spec : ∀ (deBruijnIndex nargs : ℕ),
  sizeOf (Lean.Meta.RefinedDiscrTree.Key.bvar deBruijnIndex nargs) = 1 + sizeOf deBruijnIndex + sizeOf nargs
-- Mathlib.Order.LiminfLimsup
Filter.le_liminf_of_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.le_liminf_of_le._auto_1 →
    (∀ᶠ (n : β) in f, a ≤ u n) → a ≤ Filter.liminf u f
-- Init.Data.Vector.Algebra
Vector.instHMul : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {n : ℕ} → [HMul α β γ] → HMul α (Vector β n) (Vector γ n)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.le_iff_exists : ∀ {α : Type u} {x : Std.PRange.UpwardEnumerable α} {a b : α},
  Std.PRange.UpwardEnumerable.LE a b ↔ ∃ n, Std.PRange.succMany? n a = some b
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.invFun_eq_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {f : M ≃ₜ+ N}, f.invFun = ⇑f.symm
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider `C^n` maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is `C^n`.

We give here a version of this statement within a set at a point.  -/
ContMDiffWithinAt.clm_bundle_apply₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} {M : Type u_6}
  [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8}
  [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_9} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)] {EB : Type u_10}
  [inst_19 : NormedAddCommGroup EB] [inst_20 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_21 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_22 : TopologicalSpace B] [inst_23 : ChartedSpace HB B] {EM : Type u_12}
  [inst_24 : NormedAddCommGroup EM] [inst_25 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_26 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_27 : TopologicalSpace M] [inst_28 : ChartedSpace HM M]
  [inst_29 : FiberBundle F₁ E₁] [inst_30 : VectorBundle 𝕜 F₁ E₁] [inst_31 : FiberBundle F₂ E₂]
  [inst_32 : VectorBundle 𝕜 F₂ E₂] [inst_33 : FiberBundle F₃ E₃] [inst_34 : ⋯], ⋯
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
/-- An integral domain is a Dedekind domain if every fractional ideal has an inverse.
This is an auxiliary definition used to
prove `isDedekindDomain_iff_mul_inv_cancel` and `FractionalIdeal.semifield`.  -/
_private.Mathlib.RingTheory.DedekindDomain.Ideal.Basic.0.IsDedekindDomainInv : (A : Type u_2) → [inst : CommRing A] → [IsDomain A] → Prop
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- Split a box along many hyperplanes `{y | y i = x}`; each hyperplane is given by the pair
`(i x)`.  -/
BoxIntegral.Prepartition.splitMany : {ι : Type u_1} → (I : BoxIntegral.Box ι) → Finset (ι × ℝ) → BoxIntegral.Prepartition I
-- Mathlib.SetTheory.Ordinal.Notation
/-- Calculate division and remainder of `o` mod `ω`:

`split o = (a, n)` means `o = a + n`, where `ω ∣ a`.  -/
ONote.split : ONote → ONote × ℕ
-- Std.Time.Format.Modifier
/-- `OffsetX` represents different offset formats based on the number of pattern letters.
The output will vary between the number of pattern letters, whether it's the hour, minute, second,
and whether colons are used.
 -/
Std.Time.OffsetX : Type
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_compatible : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C}
  {I : Type u_1} {X : I → C} {π : (i : I) → X i ⟶ B} {x : (i : I) → P.obj (Opposite.op (X i))}
  (hx : CategoryTheory.Presieve.Arrows.Compatible P π x), hx.familyOfElements.Compatible
-- Mathlib.Data.PFunctor.Univariate.M
/-- `Agree' n` relates two trees of type `M F` that
are the same up to depth `n`  -/
PFunctor.M.Agree' : {F : PFunctor.{uA, uB}} → ℕ → F.M → F.M → Prop
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap.eq_1 : ∀ (x lo hi : ℤ), (Lean.Grind.IntInterval.co lo hi).wrap x = (x - lo) % (hi - lo) + lo
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.whiskeringRightCompEvaluation_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A)
  (X : CategoryTheory.Functor A B),
  (CategoryTheory.whiskeringRightCompEvaluation F a).inv.app X = CategoryTheory.CategoryStruct.id (F.obj (X.obj a))
-- Mathlib.RingTheory.RingHom.FinitePresentation
/-- Being finitely-presented is stable under composition.  -/
RingHom.finitePresentation_stableUnderComposition : RingHom.StableUnderComposition @RingHom.FinitePresentation
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isAddCyclic_iff_exists_zmultiples_eq_top : ∀ {α : Type u_1} [inst : AddGroup α], IsAddCyclic α ↔ ∃ g, AddSubgroup.zmultiples g = ⊤
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v fallback : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) l →
            (k, v) ∈ l → Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.Const.insertMany m l) k' fallback = v
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendMap_comp : ∀ {ι : 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.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M)
  (e : c.Embedding c'),
  HomologicalComplex.extendMap (CategoryTheory.CategoryStruct.comp φ φ') e =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.extendMap φ e) (HomologicalComplex.extendMap φ' e)
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β a → γ a},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l)
-- Mathlib.Topology.Algebra.Group.CompactOpen
/-- `ContinuousMonoidHom _ f` is a functor.  -/
ContinuousMonoidHom.compLeft : {A : Type u_2} →
  {B : Type u_3} →
    (E : Type u_6) →
      [inst : Monoid A] →
        [inst_1 : Monoid B] →
          [inst_2 : CommGroup E] →
            [inst_3 : TopologicalSpace A] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : TopologicalSpace E] → [inst_6 : IsTopologicalGroup E] → (A →ₜ* B) → (B →ₜ* E) →ₜ* A →ₜ* E
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.FundamentalSequenceProp.match_1.eq_2 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → Sort u_1) (a : ONote) (h_1 : Unit → motive (Sum.inl none))
  (h_2 : (a : ONote) → motive (Sum.inl (some a))) (h_3 : (f : ℕ → ONote) → motive (Sum.inr f)),
  (match Sum.inl (some a) with
    | Sum.inl none => h_1 ()
    | Sum.inl (some a) => h_2 a
    | Sum.inr f => h_3 f) =
    h_2 a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_neg_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [inst_6 : TopologicalSpace A]
  [inst_7 : NonUnitalRing A] [inst_8 : StarRing A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [inst_12 : NonUnitalContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) cfcₙ_neg_id._auto_1 → cfcₙ (fun x => -x) a = -a
-- Mathlib.Data.Set.Function
Set.LeftInvOn.image_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f' : β → α}, Set.LeftInvOn f' f s → f' '' f '' s = s
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.isCompact_cellFrontier`. -/
Topology.CWComplex.isCompact_cellFrontier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] {n : ℕ}
  {i : Topology.RelCWComplex.cell C n}, IsCompact (Topology.RelCWComplex.cellFrontier n i)
-- Mathlib.RingTheory.Ideal.Basic
Ideal.single_mem_pi : ∀ {ι : Type u_1} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] {I : (i : ι) → Ideal (R i)}
  [inst_1 : DecidableEq ι] {i : ι} {r : R i}, r ∈ I i → Pi.single i r ∈ Ideal.pi I
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- A family of MulHom's `f i : M i →ₙ* N i` defines a MulHom
`MulHom.piMap f : (Π i, M i) →ₙ* (Π i, N i)`
given by `MulHom.piMap f x i = f i x`. This is `Pi.map` for `MulHom`s.  -/
MulHom.piMap : {ι : Type u_1} →
  {M : ι → Type u_3} →
    {N : ι → Type u_4} →
      [inst : (i : ι) → Mul (M i)] →
        [inst_1 : (i : ι) → Mul (N i)] → ((i : ι) → M i →ₙ* N i) → ((i : ι) → M i) →ₙ* (i : ι) → N i
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.Simp.DischargeWrapper.default : Lean.Elab.Tactic.Simp.DischargeWrapper
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint of a bounded operator `A` from a Hilbert space `E` to another Hilbert space `F`,
denoted as `A†`.  -/
ContinuousLinearMap.adjoint : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : InnerProductSpace 𝕜 E] →
              [inst_4 : InnerProductSpace 𝕜 F] → [CompleteSpace E] → [CompleteSpace F] → (E →L[𝕜] F) ≃ₗᵢ⋆[𝕜] F →L[𝕜] E
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldlM_eq_foldlM_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.TreeMap.Raw.foldlM f init t = Array.foldlM (fun a b => f a b.1 b.2) init t.toArray
-- Mathlib.CategoryTheory.ObjectProperty.ClosureShift
CategoryTheory.ObjectProperty.instIsStableUnderShiftLimitsClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddGroup A] [inst_2 : CategoryTheory.HasShift C A] {α : Type u_3} {J : α → Type u_4}
  [inst_3 : (i : α) → CategoryTheory.Category.{u_5, u_4} (J i)] [P.IsStableUnderShift A],
  (P.limitsClosure J).IsStableUnderShift A
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} {G : Type u_2} [inst_2 : AddCommGroup G]
  (f f_1 : CochainComplex.HomComplex.Cocycle K L n →+ G) (e_f : f = f_1)
  (hf : CochainComplex.HomComplex.coboundaries K L n ≤ f.ker),
  CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom f hf =
    CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom f_1 ⋯
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.postcomp_desc : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N), solution.postcomp (h.desc s) = s
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.forall : ∀ {α : Type u} {p : WithOne α → Prop}, (∀ (x : WithOne α), p x) ↔ p 1 ∧ ∀ (a : α), p ↑a
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filterMap_eq_filterMapTR.go : ∀ (α : Type u_2) (β : Type u_1) (f : α → Option β) (as : List α) (acc : Array β),
  List.filterMapTR.go f as acc = acc.toList ++ List.filterMap f as
-- Lean.Data.Lsp.Utf16
/-- Computes the position of the Unicode codepoint at UTF-16 offset
`utf16pos` in the substring of `s` starting at UTF-8 offset `off`.  -/
Lean.String.utf16PosToCodepointPosFrom : String → ℕ → String.Pos.Raw → ℕ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' fallback : α}, cmp k k' = Ordering.eq → t.getKeyD k fallback = t.getKeyD k' fallback
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- The concatenation of two compatible walks.  -/
SimpleGraph.Walk.append : {V : Type u} → {G : SimpleGraph V} → {u v w : V} → G.Walk u v → G.Walk v w → G.Walk u w
-- Mathlib.Order.CountableDenseLinearOrder
Order.PartialIso.instInhabited : (α : Type u_1) → (β : Type u_2) → [inst : LinearOrder α] → [inst_1 : LinearOrder β] → Inhabited (Order.PartialIso α β)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.mem_orbit_iff : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K]
  {w w' : NumberField.InfinitePlace K},
  w' ∈ MulAction.orbit Gal(K/k) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.comp_continuous_iff : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) {α : Type u_14}
  [inst_9 : TopologicalSpace α] {g : α → P}, Continuous (⇑f ∘ g) ↔ Continuous g
-- Mathlib.Order.Lattice
/-- A distributive lattice is a lattice that satisfies any of four
equivalent distributive properties (of `sup` over `inf` or `inf` over `sup`,
on the left or right).

The definition here chooses `le_sup_inf`: `(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z)`. To prove distributivity
from the dual law, use `DistribLattice.of_inf_sup_le`.

A classic example of a distributive lattice
is the lattice of subsets of a set, and in fact this example is
generic in the sense that every distributive lattice is realizable
as a sublattice of a powerset lattice.  -/
DistribLattice : Type u_1 → Type u_1
-- Mathlib.Data.Finset.Insert
Finset.induction : ∀ {α : Type u_3} {motive : Finset α → Prop} [inst : DecidableEq α],
  motive ∅ → (∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) → ∀ (s : Finset α), motive s
-- Init.Data.Bool
Bool.max_eq_or : max = or
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedCommandInfo.default : Lean.Elab.CommandInfo
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod_ext' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (z w : (F ⨯ G).obj a),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a)) z =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a)) w →
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.snd.app a)) z =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.snd.app a)) w →
      z = w
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit_eq : ∀ {n : ℕ} (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit l).toList = [l]
-- Init.Data.SInt.Lemmas
ISize.le_of_eq : ∀ {a b : ISize}, a = b → a ≤ b