mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.Quotient
Ideal.Quotient.algHom_ext_iff : ∀ {R₁ : Type u_1} {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I : Ideal A}
  [inst_3 : I.IsTwoSided] {S : Type u_5} [inst_4 : Semiring S] [inst_5 : Algebra R₁ S] {f g : A ⧸ I →ₐ[R₁] S},
  f = g ↔ f.comp (Ideal.Quotient.mkₐ R₁ I) = g.comp (Ideal.Quotient.mkₐ R₁ I)
-- Lean.Elab.DocString
/-- The user is currently editing the doc comment and can react to suggestions as code actions.
 -/
Lean.Doc.SuggestionMode.interactive : Lean.Doc.SuggestionMode
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise* along some nontrivial filter, and if the
family `𝓕` is equicontinuous, then the limit is continuous.  -/
Filter.Tendsto.continuous_of_equicontinuous : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι} [l.NeBot]
  {F : ι → X → α} {f : X → α}, Filter.Tendsto F l (nhds f) → Equicontinuous F → Continuous f
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm`  -/
CliffordAlgebra.changeForm.add_proof : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' Q'' : QuadraticForm R M} {B B' : LinearMap.BilinForm R M},
  LinearMap.BilinMap.toQuadraticMap B = Q' - Q →
    LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q' → LinearMap.BilinMap.toQuadraticMap (B + B') = Q'' - Q
-- Mathlib.Data.W.Basic
WType.infinite_of_nonempty_of_isEmpty : ∀ {α : Type u_1} {β : α → Type u_2} (a b : α) [ha : Nonempty (β a)] [he : IsEmpty (β b)], Infinite (WType β)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Natural transformations between functors lift to additive group objects.  -/
CategoryTheory.Functor.mapAddGrpNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F F' : CategoryTheory.Functor C D} →
              [inst_4 : F.Monoidal] → [inst_5 : F'.Monoidal] → (F ⟶ F') → (F.mapAddGrp ⟶ F'.mapAddGrp)
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_one : Nat.minFac 1 = 1
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_inf : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (S T : Submonoid N) (f : F),
  Submonoid.comap f (S ⊓ T) = Submonoid.comap f S ⊓ Submonoid.comap f T
-- Init.Data.List.Zip
List.zip_unzip : ∀ {α : Type u_1} {β : Type u_2} (l : List (α × β)), l.unzip.1.zip l.unzip.2 = l
-- Mathlib.Analysis.Analytic.Basic
AnalyticOnNhd.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  IsOpen s → AnalyticOnNhd 𝕜 f s → Set.EqOn f g s → AnalyticOnNhd 𝕜 g s
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A preadditive category has an equalizer for `f` and `g` if it has a kernel for `f - g`.  -/
CategoryTheory.Preadditive.hasEqualizer_of_hasKernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (f g : X ⟶ Y)
  [CategoryTheory.Limits.HasKernel (f - g)], CategoryTheory.Limits.HasEqualizer f g
-- Init.Data.List.Basic
List.modifyHead_nil : ∀ {α : Type u} {f : α → α}, List.modifyHead f [] = []
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
/-- **Alias** of `MonoidAlgebra.coeff_mul_mul_of_uniqueMul`.

---

The coefficient of a monomial in a product `f * g` that can be reached in at most one way
as a product of monomials in the supports of `f` and `g` is a product.  -/
MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : Mul A] {f g : MonoidAlgebra R A} {a0 b0 : A},
  UniqueMul f.coeff.support g.coeff.support a0 b0 → (f * g).coeff (a0 * b0) = f.coeff a0 * g.coeff b0
-- Mathlib.Data.NNRat.Floor
NNRat.intCeil_cast : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorRing K] (x : ℚ≥0),
  ⌈↑x⌉ = ⌈↑x⌉
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_iSup : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] {ι : Sort u_4}
  (s : ι → Submodule R M), Submodule.restrictScalars S (iSup s) = ⨆ i, Submodule.restrictScalars S (s i)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.stalkAlgebra_map : ∀ (R : Type u) [inst : CommRing R] (p : PrimeSpectrum R) (r : R),
  (algebraMap R ↑((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalk p)) r =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.toStalk R p)) r
-- Lean.PrettyPrinter.Delaborator.SubExpr
/-- Assumes the `SubExpr` is a lambda or forall.
1. Creates a local declaration for this binder using the name `n`.
2. Evaluates `v` using the fvar for the local declaration.
3. Enters the binding body, and evaluates `x` using this result.
 -/
Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody' : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [MonadReaderOf Lean.SubExpr m] →
        [MonadWithReaderOf Lean.SubExpr m] →
          [MonadControlT Lean.MetaM m] → {β : Type} → Lean.Name → (Lean.Expr → m β) → (β → m α) → m α
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.ne_zero_iff : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) {x : R}, abv x ≠ 0 ↔ x ≠ 0
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_of_nonpos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], a ≤ 0 → ⌊a⌋₊ = 0
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.inter_right : ∀ {α : Type u_1} {G : SimpleGraph α} {s : Set α}, G.IsClique s → ∀ (t : Set α), G.IsClique (t ∩ s)
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instFourierInvAdd : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F], FourierInvAdd (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_zero : ∀ (a : Ordinal.{u_4}), a / 0 = 0
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_nonneg_of_nonpos_of_nonpos : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b : R}, a ≤ 0 → b ≤ 0 → 0 ≤ a * b
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.add.go.match_1.splitter : (motive : Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly → Sort u_1) →
  (p₁ p₂ : Nat.Internal.SOM.Poly) →
    ((p₁ : Nat.Internal.SOM.Poly) → motive p₁ []) →
      ((p₂ : Nat.Internal.SOM.Poly) → (p₂ = [] → False) → motive [] p₂) →
        ((k₁ : ℕ) →
            (m₁ : Nat.Internal.SOM.Mon) →
              (p₁ : List (ℕ × Nat.Internal.SOM.Mon)) →
                (k₂ : ℕ) →
                  (m₂ : Nat.Internal.SOM.Mon) →
                    (p₂ : List (ℕ × Nat.Internal.SOM.Mon)) → motive ((k₁, m₁) :: p₁) ((k₂, m₂) :: p₂)) →
          motive p₁ p₂
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.hasEval_def : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : TopologicalSpace S] (a : S),
  PowerSeries.HasEval a ↔ IsTopologicallyNilpotent a
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.IsReduced.not_step : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.IsReduced L₁ → ¬FreeAddGroup.Red.Step L₁ L₂
-- Lean.Compiler.NoncomputableAttr
/-- Returns `true` when the given declaration is tagged `noncomputable`.
 -/
Lean.isNoncomputable : Lean.Environment →
  Lean.Name → optParam Lean.EnvExtension.AsyncMode Lean.noncomputableExt.toEnvExtension.asyncMode → Bool
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instLinearOrderIdealOfDecidableLE : (A : Type u) → [inst : CommRing A] → [PreValuationRing A] → [DecidableLE (Ideal A)] → LinearOrder (Ideal A)
-- Std.Time.Format.Modifier
Std.Time.Modifier.W.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.W presentation = Std.Time.Modifier.W presentation_1 → presentation = presentation_1
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isRevMatch_iff_exists_splits : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch pat pos ↔
    ∃ t₁ t₂, pos.Splits t₁ t₂ ∧ String.Slice.Pattern.Model.PatternModel.Matches pat t₂
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) (X : J),
  ((d.trans hij).app X).left =
    CategoryTheory.Limits.pullback.map (D.obj X).hom (𝒰.f i) (D.obj X).hom (𝒰.f j)
      (CategoryTheory.CategoryStruct.id (D.obj X).left) (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)
      (CategoryTheory.CategoryStruct.id S) ⋯ ⋯
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt8HOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.integral_norm_prod_right : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite μ] ⦃f : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) → MeasureTheory.Integrable (fun y => ∫ (x : α), ‖f (x, y)‖ ∂μ) ν
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.splitMonoEquiv.eq_1 : ∀ {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} (f : Y ⟶ X) [inst_2 : F.Full] [inst_3 : F.Faithful],
  F.splitMonoEquiv f =
    { toFun := fun f_1 => f_1.map F, invFun := fun s => { retraction := F.preimage s.retraction, id := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.CountableSupClosed
/-- A set `s` is closed under countable supremum if for every nonempty countable subset of `s`, any
least upper bound of that subset is in `s`.  -/
CountableSupClosed : {α : Type u_2} → [LE α] → Set α → Prop
-- Lean.DocString.Markdown
Lean.Doc.MarkdownM.InlineCtx.mk.injEq : ∀ (inEmph inBold inLink inEmph_1 inBold_1 inLink_1 : Bool),
  ({ inEmph := inEmph, inBold := inBold, inLink := inLink } =
      { inEmph := inEmph_1, inBold := inBold_1, inLink := inLink_1 }) =
    (inEmph = inEmph_1 ∧ inBold = inBold_1 ∧ inLink = inLink_1)
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
/-- The binomial distribution with parameter `p` on simple graphs with vertices `V`.  -/
SimpleGraph.«termG(_,_)» : Lean.ParserDescr
-- Std.Data.String.ToInt
_private.Std.Data.String.ToInt.0.String.Slice.isInt.match_1.eq_2 : ∀ (motive : Option String.Slice → Sort u_1) (h_1 : (rest : String.Slice) → motive (some rest))
  (h_2 : Unit → motive none),
  (match none with
    | some rest => h_1 rest
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.mkD.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β)
  (default : C(α, β)),
  ContinuousMap.mkD f default = if h : Continuous f then { toFun := f, continuous_toFun := h } else default
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.toString : Std.Tactic.BVDecide.Gate → String
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `lowerHemicontinuous_iff_frequently`. -/
LowerHemicontinuous.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  (∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t) → LowerHemicontinuous f
-- Mathlib.RingTheory.Trace.Basic
AlgHom.domRestrict.eq_1 : ∀ {A : Type u_3} (B : Type u_4) {C : Type u_5} {D : Type u_6} [inst : CommSemiring A] [inst_1 : CommSemiring C]
  [inst_2 : CommSemiring D] [inst_3 : Algebra A C] [inst_4 : Algebra A D] [inst_5 : CommSemiring B]
  [inst_6 : Algebra A B] [inst_7 : Algebra B C] [inst_8 : IsScalarTower A B C] (f : C →ₐ[A] D),
  AlgHom.domRestrict B f = f.comp (IsScalarTower.toAlgHom A B C)
-- Init.Data.Array.Find
Array.findFinIdx?_push : ∀ {α : Type u_1} {xs : Array α} {a : α} {p : α → Bool},
  Array.findFinIdx? p (xs.push a) =
    (Option.map (Fin.castLE ⋯) (Array.findFinIdx? p xs)).or (if p a = true then some ⟨xs.size, ⋯⟩ else none)
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.instProd : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S], Algebra.Etale (R × S) S
-- Lean.Elab.App
/-- Construct the resulting application after all discriminants have been elaborated, and we have
consumed as many given arguments as possible.
 -/
Lean.Elab.Term.ElabElim.finalize : Lean.Elab.Term.ElabElim.M Lean.Expr
-- Lean.Elab.InfoTree.Types
/-- A completion is an item that appears in the [IntelliSense](https://code.visualstudio.com/docs/editor/intellisense)
box that appears as you type.  -/
Lean.Elab.CompletionInfo : Type
-- Mathlib.Topology.Order.IsLUB
isGLB_of_mem_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {s : Set α} {a : α},
  a ∈ lowerBounds s → a ∈ closure s → IsGLB s a
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (a : M), IsIdempotentElem a = (a * a = a)
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesColimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F)
      (CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).inv =
    CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₁ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Mathlib.Data.Prod.Basic
Prod.trichotomous : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Trichotomous r] [Std.Trichotomous s],
  Std.Trichotomous (Prod.Lex r s)
-- Batteries.Data.BinomialHeap.Basic
/-- The well formedness predicate for a `FindMin` value.
This is not actually a predicate, as it contains an additional data value
`rank` corresponding to the rank of the returned node, which is omitted from `findMin`.
 -/
Batteries.BinomialHeap.Imp.FindMin.WF : {α : Type u_1} → (α → α → Bool) → Batteries.BinomialHeap.Imp.FindMin α → Type
-- Lean.Meta.Tactic.Rewrite
Lean.Meta.RewriteResult.mk.sizeOf_spec : ∀ (eNew eqProof : Lean.Expr) (mvarIds : List Lean.MVarId),
  sizeOf { eNew := eNew, eqProof := eqProof, mvarIds := mvarIds } = 1 + sizeOf eNew + sizeOf eqProof + sizeOf mvarIds
-- Mathlib.Logic.Basic
decidableEq_of_subsingleton : {α : Sort u_1} → [Subsingleton α] → DecidableEq α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α},
  Std.DHashMap.Const.get! (m₁.inter m₂) k = if k ∈ m₂ then Std.DHashMap.Const.get! m₁ k else default
-- Mathlib.Order.WithBot
WithBot.unbot_inj : ∀ {α : Type u_1} {a b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥), a.unbot ha = b.unbot hb ↔ a = b
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.comap_inf : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (s t : NonUnitalSubring S) (f : F),
  NonUnitalSubring.comap f (s ⊓ t) = NonUnitalSubring.comap f s ⊓ NonUnitalSubring.comap f t
-- Init.Data.List.Lemmas
List.getElem_set_self : ∀ {α : Type u_1} {l : List α} {i : ℕ} {a : α} (h : i < (l.set i a).length), (l.set i a)[i] = a
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.norm_integral_le : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f : ↥(MeasureTheory.Lp E 1 μ)),
  ‖MeasureTheory.L1.integral f‖ ≤ ‖f‖
-- Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree
ContinuousCohomology.cocycles₀IsoAux : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G),
  ∀ σ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker, ↑σ 1 ∈ X.ρ.invariants
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyMap_of_isIso_opcyclesMap_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap φ) →
    CategoryTheory.Mono φ.τ₃ → CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- The power basis `1, x, ..., x ^ (d - 1)` for `K⟮x⟯`,
where `d` is the degree of the minimal polynomial of `x`.  -/
IntermediateField.adjoin.powerBasis : {K : Type u} →
  [inst : Field K] →
    {L : Type u_3} → [inst_1 : Field L] → [inst_2 : Algebra K L] → {x : L} → IsIntegral K x → PowerBasis K ↥K⟮x⟯
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.Set.univ_symm_apply_coe : ∀ (X : Type u_7) [inst : TopologicalSpace X] (a : X), ↑((Homeomorph.Set.univ X).symm a) = a
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.instTransIsContained : {α : Type u_4} →
  {β : Type u_5} → {γ : Type u_6} → Trans SimpleGraph.IsContained SimpleGraph.IsContained SimpleGraph.IsContained
-- Mathlib.Order.Heyting.Boundary
Coheyting.sdiff_boundary_self : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a : α}, a \ Coheyting.boundary a = ￢￢a
-- Mathlib.Data.Finsupp.Basic
Finsupp.eq_zero_of_comapDomain_eq_zero : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α → β) (l : β →₀ M)
  (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support), Finsupp.comapDomain f l ⋯ = 0 → l = 0
-- Std.Sync.Broadcast
/-- Errors that may be thrown while interacting with the broadcast channel API.
 -/
Std.Broadcast.Error : Type
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ordCompare_minKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtTreeMap α β compare}
  [inst_2 : Inhabited α] {k : α} {f : β → β}, compare (t.modify k f).minKey! t.minKey! = Ordering.eq
-- Mathlib.Order.LiminfLimsup
Filter.eventually_lt_of_limsup_lt : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} [inst : ConditionallyCompleteLinearOrder β] {u : α → β} {b : β},
  Filter.limsup u f < b →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.eventually_lt_of_limsup_lt._auto_1 →
      ∀ᶠ (a : α) in f, u a < b
-- Mathlib.Data.ENat.Basic
ENat.map_natCast_nonneg : ∀ {n : ℕ∞} {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α],
  0 ≤ ENat.map Nat.cast n
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RicSliceData.mk.injEq : ∀ {α : Type u} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit) (range : Std.Ric α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit) (range_1 : Std.Ric α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.CategoryTheory.Abelian.FunctorCategory
CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{z, w} D]
  [inst_2 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C),
  (CategoryTheory.Abelian.coimageImageComparison α).app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimageImageComparison (α.app X))
        (CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).inv)
-- Mathlib.RepresentationTheory.Intertwining
/-- The range of an intertwining map from `V` to `W` as a subrepresentation of `W`.  -/
Representation.IntertwiningMap.range : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → ρ.IntertwiningMap σ → Subrepresentation σ
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.ext_hom : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : IsFreeAddGroup G] {H : Type u_2} [inst_2 : AddGroup H] ⦃f g : G →+ H⦄,
  (∀ (a : IsFreeAddGroup.Generators G), f (IsFreeAddGroup.of a) = g (IsFreeAddGroup.of a)) → f = g
-- Mathlib.Algebra.Homology.BifunctorFlip
HomologicalComplex.mapBifunctorFlipIso_flip : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : TotalComplexShape c₂ c₁ c] [inst_10 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_11 : DecidableEq J]
  [inst_12 : K₁.HasMapBifunctor K₂ F c] [inst_13 : TotalComplexShapeSymmetry c₂ c₁ c]
  [TotalComplexShapeSymmetrySymmetry c₁ c₂ c], K₂.mapBifunctorFlipIso K₁ F.flip c = (K₁.mapBifunctorFlipIso K₂ F c).symm
-- Init.Data.Array.Lemmas
/-- Variant of `any_eq` in terms of membership rather than an array index.  -/
Array.any_eq' : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, xs.any p = decide (∃ x ∈ xs, p x = true)